ocaml-gospel / ortac

Runtime assertion checking based on Gospel specifications
https://ocaml-gospel.github.io/ortac/
MIT License
36 stars 10 forks source link

Parsing mistake of arrows from Gospel to Ortac in case of function declaration #212

Closed Lucccyo closed 1 month ago

Lucccyo commented 5 months ago

When declaring the gospel model as a function (string -> string option), Ortac misinterprets it and separates the operator ->. It considers the arrow as a type constructor instead of the OCaml arrow, which is used for functions.

We have the type t modeling its content by a map of type string -> string option. Following is the code generated by Ortac.

[...]
  type nonrec state = {
      contents: (string, string option) (->) }
[...]

It should be :

[...]
  type nonrec state = {
      contents: (string -> string option) }
[...]
n-osborne commented 5 months ago

Thanks!

I believe the culprit is Ortac_core.Ocaml_of_gospel.core_type_of_tysymbol