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://fstarlang.github.io/lowstar/html/LowStar.html#c-string-literals 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
> *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=02%7C01%7Cprotz%40microsoft.com%7Cdb40113318a44ce8c0be08d5afbc9c55%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636608146970557404=aLvfTn4cd9Wrvck8prnVvnQfEA9I3BPpp1%2BE0PkjGpw%3D=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
>>
>>