Hmm, I don't think this involves meta-programming; normalize_term is a pure function with special support in the compiler.
The meta-programming version would look like this, rather: open FStar.Tactics let main () : int = C.print_string (C.string_of_literal (synth_by_tactic (fun () -> let body = `(String.concat ", " ["hello"; "world"]) in exact (norm_term [primops; delta; iota; zeta] body)))); C.exit_success Clément. On 2018-05-02 11:47, Jonathan Protzenko wrote: > Yes -- you can always meta-program as much as you want, although: > > * meta-programming support is limited for string functions -- I think only > String.length can be meta-evaluated > * the chapter on meta-programming Low* hasn't been written yet in the > tutorial 😊. > > > ~ jonathan > > ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ > *From:* fstar-club <fstar-club-boun...@lists.gforge.inria.fr> on behalf of > Clément Pit-Claudel via fstar-club <fstar-club@lists.gforge.inria.fr> > *Sent:* Wednesday, May 2, 2018 8:44 AM > *To:* fstar-club@lists.gforge.inria.fr > *Subject:* Re: [fstar-club] Trying to use List.Tot.map with Kremlin > > I'd expect the following to work, though. Does it? > > let main () = > C.print_string (C.string_of_literal (normalize_term (String.concat ", > " ["hello"; "world"]))); > C.exit_success > > … though maybe we don't apply `normalize_term` early enough. > > Clément. > > On 2018-05-02 11:08, Jonathan Protzenko via fstar-club wrote: >> Yes, this is something that has poor usability. Prims.string and >> FStar.String.concat are supported as transition mechanisms to help porting >> F* programs to Low* but I agree that it's confusing for beginners to have >> them work "by default". >> >> https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Ffstarlang.github.io%2Flowstar%2Fhtml%2FLowStar.html%23c-string-literals&data=02%7C01%7Cprotz%40microsoft.com%7C6270df4eb0a244eaac3908d5b043b2d5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636608727210614165&sdata=ffbZwtJJ2ud7JXMhD56SL3Kyv15X%2BEYQT87%2Bc%2BlLFgY%3D&reserved=0 >> has a note that explains it, my plan is to make it a warning that's fatal >> by default, and that can be disabled if you need these mechanisms >> >> ~ jonathan >> >> ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ >> *From:* Pierre Beaucamp <m...@pierrebeaucamp.com> >> *Sent:* Tuesday, May 1, 2018 4:38 PM >> *To:* Jonathan Protzenko; Pierre Beaucamp via fstar-club >> *Subject:* Re: [fstar-club] Trying to use List.Tot.map with Kremlin >> >> Thanks for the quick answer Jonathan. >> >> I already assumed that this is caused by limited inter-polarity between F* >> strings and their representation in Low*. What threw me off is that this >> code works: >> >> let main () = >> C.print_string (C.string_of_literal (String.concat ", " ["hello"; >> "world"])); >> C.exit_success >> >> Either way, I'm excited for the Low* tutorial - thank you for writing it. >> This is a very interesting language with unfortunately very little >> documentation for new-comers (I'm pretty much trying to learn F* and Low* at >> the same time, and I guess this is where a lot of the confusion is coming >> from). >> >> Thank you and best regards, >> >> -- >> Pierre Beaucamp >> >> On Tue, May 1, 2018, at 7:09 PM, Jonathan Protzenko wrote: >>> Hello Pierre, >>> >>> These are all excellent questions -- I am currently writing a tutorial >>> for Low* are these served as good inspiration for the introduction. If >>> CI goes through, a work-in-progress version of the tutorial should be >>> uploaded in the next few hours at >>> https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Ffstarlang.github.io%2Flowstar%2F&data=02%7C01%7Cprotz%40microsoft.com%7Cdb40113318a44ce8c0be08d5afbc9c55%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636608146970557404&sdata=aLvfTn4cd9Wrvck8prnVvnQfEA9I3BPpp1%2BE0PkjGpw%3D&reserved=0 >>> -- please read it and let me know whether after browsing it, your >>> questions have been answered. >>> >>> In case the CI doesn't perform the upload, or the tutorial is unclear, >>> the essence of your issue is that your code is not Low*. >>> >>> * the F* string and list types are F* values, i.e. concat has type >>> string -> string -> string; the only way to give you these semantics >>> without requiring the user to track allocations and lifetimes is to use >>> a garbage-collector, which C does not have >>> * the same goes for lists: compiling them to C with the current F* >>> value semantics would lead to a zillion uncollected list cell >>> allocations. >>> >>> What the C.String module provides is a bare-bones model of C string >>> literals, i.e. `const char *s = "my string literal";`, meaning that you >>> should provide an actual literal, e.g. `C.String.( print !$"hello, world >>> \n" );`. This is very limited, and does not allow you to do arbitrary >>> string manipulation. >>> >>> A proof-of-concept example exists that does that, in the test/ >>> subdirectory of KreMLin, and is called Server.fst. It models blitting >>> C.String.t's into a mutable buffer of C chars, tracking how much space >>> remains in your buffer, whether the buffer is live, etc. and rules out >>> buffer overflows. >>> >>> Naturally, it's a little involved for a hello world, but I guess that's >>> the reality of tracking temporal (liveness) and spatial safety (bounds) >>> in C. >>> >>> Let me know if that helps. >>> >>> Cheers, >>> >>> Jonathan >>> >>> >>> ~ jonathan >>> >>> ________________________________ >>> From: fstar-club <fstar-club-boun...@lists.gforge.inria.fr> on behalf of >>> Pierre Beaucamp via fstar-club <fstar-club@lists.gforge.inria.fr> >>> Sent: Tuesday, May 1, 2018 9:48 AM >>> To: fstar-club@lists.gforge.inria.fr >>> Subject: [fstar-club] Trying to use List.Tot.map with Kremlin >>> >>> Hi everyone, >>> >>> I'm just playing a bit around with F-Star and Kremlin and I seem to be >>> stuck at a simple problem. I don't know if I'm missing something obvious >>> or if this might be a bug. My code looks like this: >>> >>> let main () = >>> C.print_string (C.string_of_literal (String.concat ", >>> " (List.Tot.map string_of_int [1; 2; 3]))); >>> C.exit_success >>> >>> I expect this code to print `1, 2, 3` but instead I get the following >>> runtime error: >>> >>> KreMLin abort at ./Main.c:9 >>> This function was not extracted: >>> Failure("Cannot extract string_of_literal applied to a non-literal") >>> >>> I tried some variations of the above program to see if I can reverse- >>> engineer what is going on, but as soon as I introduce `List.Tot.map`, >>> the code breaks. I know that there is also `C.Loops.map`, but I don't >>> know if I really need to use buffers to make it work. >>> >>> Also, I'm generally interested in learning more about Kremlin / Low* / >>> F*. If there are any recommended resources or other helpful links, feel >>> free to share them with me. >>> >>> Thank you and best regards, >>> >>> -- >>> Pierre Beaucamp >>> _______________________________________________ >>> fstar-club mailing list >>> fstar-club@lists.gforge.inria.fr >>> https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gforge.inria.fr%2Fmailman%2Flistinfo%2Ffstar-club&data=02%7C01%7Cprotz%40microsoft.com%7C445acbbb8a104079b70808d5af83d2b8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636607903120375441&sdata=WkxhslLqaMBwupJazX4IDfRaWwsqX6IIiuWZT8YrwFc%3D&reserved=0 >> >> >> _______________________________________________ >> fstar-club mailing list >> fstar-club@lists.gforge.inria.fr >> https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gforge.inria.fr%2Fmailman%2Flistinfo%2Ffstar-club&data=02%7C01%7Cprotz%40microsoft.com%7C6270df4eb0a244eaac3908d5b043b2d5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636608727210624175&sdata=NfYXtrOcH1uADk53hQ4SU%2B0ZbpfLtPWUqDZI97EgCyA%3D&reserved=0 >> > > _______________________________________________ > fstar-club mailing list > fstar-club@lists.gforge.inria.fr > https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gforge.inria.fr%2Fmailman%2Flistinfo%2Ffstar-club&data=02%7C01%7Cprotz%40microsoft.com%7C6270df4eb0a244eaac3908d5b043b2d5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636608727210624175&sdata=NfYXtrOcH1uADk53hQ4SU%2B0ZbpfLtPWUqDZI97EgCyA%3D&reserved=0 _______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club