search

ocaml-gospel / gospel

A tool-agnostic formal specification language for OCaml.
https://ocaml-gospel.github.io/gospel
MIT License
123 stars 16 forks source link

Type-check module signature in ml files #366

Open n-osborne opened 9 months ago

n-osborne commented 9 months ago

Specifications in 

module type S = sig
...
end

are not read.

In addition, we could discuss type-checking of implementation's specification (for Cameleer) in gospel itself.

mariojppereira commented 9 months ago

Hi @n-osborne. Are you talking about type-checking only module signatures in .ml files or really pushing the barrier and type-check every piece of GOSPEL specification when might find in an OCaml implementation file?

n-osborne commented 9 months ago

Hi @mariojppereira.

The first use case that comes in mind is the type signature in .ml files. I came across this "problem" in ortac#183. You can't directly type-check these specifications: you have to extract them in a .mli file, which is not ideal when writing them.

Once we've open the .ml file, we can ask ourselves whether to look at implementation code. My understanding is that Cameleer does not type-check the specifications but rather work on the untyped AST. So we could at least parse the specifications in the implementation code (an occasion to merge the Cameleer's gospel into the main one).