Hi Frieder,
You have to be careful with the Platform.Bytes types, in particular
because the types of FStar.Char.char (which is the one used by single
quotes) and Platform.Bytes.byte are not the same after extraction. This
is a known limitation that will be adressed at some point, but in the
meantime you should use abyte, abytes, utf8/iutf8 to write constant
bytes in Platform.Bytes.
In your case, writing let bl = Platform.Bytes.utf8 "AAA" would work
Best,
Antoine Delignat-Lavaud
Le 23/05/2017 à 16:46, Frieder Steinmetz via fstar-club a écrit :
Hello Everybody,
I am working with FStar for a university project but do not have a lot
of experience yet.
Right now I'm struggling with a piece of code that typechecks just fine
with fstar but when extracted throws type mismatch erros in ocaml.
A simplified example still showing the same behavior is:
```
module Test
let main =
let bt: Platform.Bytes.byte = 'A'
in
let bl: Platform.Bytes.bytes = FStar.Seq.of_list [bt; bt; bt]
in
let conn = Platform.Udp.connect "8.8.8.8" 53
in
Platform.Udp.send conn bl
```
ocamlopt throws the following error:
```
File "out/Test.ml", line 6, characters 25-27:
Error: This expression has type char FStar_Seq_Base.seq
but an expression was expected of type Platform.Bytes.bytes
```
The extracted ocaml code (out/Test.ml) is:
```
open Prims
let main : (Prims.string,Prims.unit) Platform.Error.optResult =
let bt = 'A' in
let bl = FStar_Seq_Base.of_list [bt; bt; bt] in
let conn = Platform.Udp.connect "8.8.8.8" (Prims.parse_int "53") in
Platform.Udp.send conn bl
```
I find this especially confusing since Platform.Bytes.bytes is defined
as follows:
```
type bytes = Seq.seq byte
```
I am very grateful for any suggestions on whats going on!
Regards,
Frieder
_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
