You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This PR required to have a Byte_sequence type which maps to the OCaml Byte_sequence_wrapper.byte_sequence for the OCaml target, and to list byte on all other targets. This doesn't seem too hard at first, let's try:
typebyte_sequence = listbyte
declare ocamltarget_reptypebyte_sequence = `Byte_sequence_wrapper.byte_sequence`
(* Let's try to add a function *)vallength : byte_sequence -> naturalletlengthbs=List.lengthbs
declare ocamltarget_repfunctionlength=`Byte_sequence_wrapper.big_num_length`
(* Works! *)(* Let's try to add another function, which works on all backends, and uses this length function we just defined *)valdo_stuff : byte_sequence -> naturalletdo_stuffbs=1+ (lengthbs)
(* Lem is happy, but ugh, OCaml isn't In fact the generated OCaml function takes a list of bytes as first argument, not our OCaml type *)
Let's try with another strategy:
typebyte_sequence
declare coqtarget_reptypebyte_sequence = listbyte(* Same for all other backends except… *)
declare ocamltarget_reptypebyte_sequence = `Byte_sequence_wrapper.byte_sequence`
vallength : byte_sequence -> natural
declare coqtarget_repfunctionlength=List.length
declare ocamltarget_repfunctionlength=`Byte_sequence_wrapper.big_num_length`
(* Err, the Coq line fails with: Type error: type mismatch: top-level expression Byte_sequence.byte_sequence and list _*)
It seems using the native list length function with backticks instead of Lem's List.length would work. But that would require copy-pasting a lot of list.lem from the stdlib and more importantly re-coding a lot of functions in each backend's language (basically creating one Byte_sequence_wrapper per backend). I don't want to write a whole file of Coq, so I decided to reject that solution.
I've tried other strategies, like defining separate types and then trying to merge them in the byte_sequence type, but this doesn't work either.
The text was updated successfully, but these errors were encountered:
I ran into this issue while working on rems-project/linksem#9
This PR required to have a
Byte_sequence
type which maps to the OCamlByte_sequence_wrapper.byte_sequence
for the OCaml target, and tolist byte
on all other targets. This doesn't seem too hard at first, let's try:Let's try with another strategy:
It seems using the native list length function with backticks instead of Lem's
List.length
would work. But that would require copy-pasting a lot oflist.lem
from the stdlib and more importantly re-coding a lot of functions in each backend's language (basically creating oneByte_sequence_wrapper
per backend). I don't want to write a whole file of Coq, so I decided to reject that solution.I've tried other strategies, like defining separate types and then trying to merge them in the
byte_sequence
type, but this doesn't work either.The text was updated successfully, but these errors were encountered: