ocaml-gospel / ortac

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

Check for out of scope variables. #175

Closed n-osborne closed 11 months ago

n-osborne commented 11 months ago

Fixes #171

This PR proposes to check for out of scope variables (returned values when building next_state function) in the subst_term function.

It can be argued that subst_term is now doing a lot of different things, but the added feature does not add lot of complexity, I used an optional arguement so that the change is transparent for user that does not need the new feature, and writing another function implementing this check would necessitate the same traversal of the term type.

Non compiling code is not generated anymore, but if the next_state function has not been generated, the user stay unaware of the why.

I didn't fix this last problem in this PR because it may necessitate a larger reflexion on which errors we want to display and which errors we want to forget about.