search

ocaml-gospel / ortac

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

Add support for custom ghost type as model #228

Closed n-osborne closed 3 months ago

n-osborne commented 3 months ago

This PR proposes an answer to #209 by adding a translation for type_declarations in ortac-core and use it in ortac-qcheck-stm.

The translation doesn't support constructors with inlined records, as they are buggy in Gospel anyway and it is still an open question whether they will be fixed or removed there.

The use of translated gospel types in ortac-qcheck-stm is naive: the symbols for constructors or record fields as translated are they appears in the gospel ast and are not stored in the context (as it is the case for gospel functions).

n-osborne commented 3 months ago

CI failure is unrelated. Merging.