So contrary to what I said, this works, and String.concat is correctly reduced:
module Test
open FStar.HyperStack.ST
let main (): St C.exit_code =
C.String.(print !$(normalize_term (String.concat ", " ["hello";
"world"])));
C.EXIT_SUCCESS
compile it with krml -no-prefix Test -add-include '"kremstr.h"'
I generally use meta-programming to refer to any partial program evaluation
that is performed by F* at type-checking time instead of being performed at
run-time, but perhaps that's an incorrect term... any suggestions for a better
term? 😊
~ jonathan
________________________________
From: Clément Pit-Claudel <cpitclau...@gmail.com>
Sent: Wednesday, May 2, 2018 9:02 AM
To: Jonathan Protzenko; Clément Pit-Claudel via fstar-club
Subject: Re: [fstar-club] Trying to use List.Tot.map with Kremlin
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
