Cannot do per-target type definitions
Opened this issue · 0 comments
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 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:
type byte_sequence = list byte
declare ocaml target_rep type byte_sequence = `Byte_sequence_wrapper.byte_sequence`
(* Let's try to add a function *)
val length : byte_sequence -> natural
let length bs = List.length bs
declare ocaml target_rep function length = `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 *)
val do_stuff : byte_sequence -> natural
let do_stuff bs = 1 + (length bs)
(* 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:
type byte_sequence
declare coq target_rep type byte_sequence = list byte
(* Same for all other backends except… *)
declare ocaml target_rep type byte_sequence = `Byte_sequence_wrapper.byte_sequence`
val length : byte_sequence -> natural
declare coq target_rep function length = List.length
declare ocaml target_rep function length = `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.