Closed Lucccyo closed 4 months ago
Thank you! This is indeed a couple of problems.
I believe the first problem originates from the fact that unit
is encoded in Gospel as a tuple of length 0. It may be the condition in Ortac_core.Ocaml_of_gospel.core_type_of_ty_with_subst
line 232 that is too weak.
Regarding the second problem, it may come from Gospel itself.
As we can see in the following example, Gospel gives the name unit
to the value ()
, then when translating the Tterm.Tapp
, ortac
will look and uses the ls_name
.
$ cat > foo.mli << EOF
> val f : int -> int
> (*@ y = f x
> modifies () *)
> EOF
$ gospel dumpast foo.mli | awk "/sp_wr/,/sp_cs/"
sp_wr =
[{ Tterm.t_node =
(Tterm.Tapp (
{ Symbols.ls_name = unit; ls_args = [];
ls_value =
(Some { Ttypes.ty_node =
(Ttypes.Tyapp (
{ Ttypes.ts_ident = unit_1; ts_args = [];
ts_alias = None },
[]))
});
ls_constr = true; ls_field = false },
[]));
t_ty =
(Some { Ttypes.ty_node =
(Ttypes.Tyapp (
{ Ttypes.ts_ident = unit_1; ts_args = [];
ts_alias = None },
[]))
});
t_attrs = []; t_loc = /tmp/bob.mli:3:13 }
];
sp_cs = []; sp_diverge = false; sp_pure = false;
Modeling a type with
unit
and testing it with Ortac produces a code that swaps around the typeunit
and the value()
.()
at line 7 should beunit
, andunit
at line 12 should be()
.