ocaml-gospel/gospel

Syntax error for `(::)` notation in patterns

mariojppereira opened this issue · 3 comments

The following piece of code issues a syntax error:

  val f : int list -> int
  (*@ r = f l
            requires match l with
                          | _ :: x :: _ :: _ :: _ -> x >= 0
                          | _ -> false *)

The reason is that our parser only accepts pat_uni_ as (::) arguments. Thus, one way to fix the above is by doing the following:

    val f : int list -> int
  (*@ r = f l
            requires match l with
                          | _ :: (x :: (_ :: (_ :: _ ))) -> x >= 0
                          | _ -> false *)

This is tremendously inconvenient.

We have already fixed this with @paulpatault (in a branch still to be merged).

@mariojppereira Could you open a PR adding these as tests so we can detect this if it happens again?

Actually, I think @paulpatault added a test with this already here.
Don't hesitate to reopen this if it is not fixed.