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://fstarlang.github.io/lowstar/
> -- 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://lists.gforge.inria.fr/mailman/listinfo/fstar-club
