ocaml-gospel / gospel

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

Incomplete record pattern don't use OCaml syntax #417

Closed n-osborne closed 1 month ago

n-osborne commented 4 months ago

Given a type:

(*@ type t = {a: integer; b: integer}

In the current state of Gospel, one can write:

(*@ predicate p (x : t) =
    match x with
    | { a } -> a = 42

On the equivalent OCaml code, OCaml compiler would report some missing fields.

Also, Gospel fail with a syntax error if we use an OCaml-correct syntax:

(*@ predicate p (x : t) =
    match x with
    { a; _ } -> a = 42 *)

I propose to bring Gospel closer to OCaml. I already have some experiments in this direction.