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

Revise xposts internal representation #379

Open n-osborne opened 7 months ago

n-osborne commented 7 months ago

In the current version, exceptional post-conditions are represented with the type : (xsymbol * (pattern * term) list) list

This doesn't work well with exception that doesn't have any arguments. For example in:

exception E

val f : int -> int
(*@ y = f x
    raises E -> x = 42

the type checker has to fill for the pattern. It wil linsert a tuple0 pattern, I believe because the type of E is Exn_tuple [].

n-osborne commented 5 months ago

After further investigation, the tuple0 is placed by the parser. In case we have a pattern but no term (raises E _), the parser will insert a Ttrue.

I believe there are two ways to go:

  1. either flatten the type and go for somethin along the way of (xsymbol * pattern option * term) list
  2. add pattern for exceptions and go for (pattern * term) list which is even simpler