Tactic notation and custom entries · Coq users

I'm looking at defining a tactic to apply to some code for the simply typed lambda calculus (stlc in https://coq.vercel.app/ext/sf/plf/full/Stlc.html).
There is a conflict between the Ltac |- and the custom entry notation |-
I'd be inclined to tell it what notation scope to use, or just to close the custom entry scope, but I do not fully understand how either Tactic notations or custom entries relate to scopes. Is it documented somewhere?

Paolo Giarrusso (Nov 07 2022 at 12:26):

Custom entries affect the grammar and parsing, notation scopes only become relevant after parsing is complete, but notations can affect lexing.

Paolo Giarrusso (Nov 07 2022 at 12:27):

For instance, where "Gamma '|-' t '\in' T" := (has_type Gamma t T) in your link asks |- to be lexed differently. IIRC, that's active as soon as the containing definition is imported...

Paolo Giarrusso (Nov 07 2022 at 12:29):

Reserved Notation "Gamma '|-' t '\in' T"
            (at level 101,
             t custom stlc, T custom stlc at level 0).

Paolo Giarrusso (Nov 07 2022 at 12:31):

I haven't reverse-engineered custom entries as closely, but that command is also adding a new rule to parsing for expressions (not some custom entry). Regardless, the lexing affects everything.

Bas Spitters (Nov 07 2022 at 12:32):

Paolo Giarrusso (Nov 07 2022 at 12:55):

There's something I can't explain, but if the conflict is indeed at the lexing level yes. But there's a way to patch SF that should work:

Reserved Notation "Gamma | -  t '\in' T"
            (at level 101,
             t custom stlc, T custom stlc at level 0).

Ltac test_ltac := idtac.

Ltac test_ltac ::=
  match goal with
    | [ H : _ |- _ ] => clear H
  end.

Declare Custom Entry stlc.

(* This is safe. The space is not required by users, and should not be used in pretty-printing. *)
Reserved Notation "Gamma | -  t '\in' T"
            (at level 101,
             t custom stlc, T custom stlc at level 0).

Ltac test_ltac ::=
  repeat match goal with
           | [ H : _ |- _ ] => clear H
         end.

(** Breaks [test_ltac]; try commenting it in/out. *)
Reserved Notation "Gamma |-  t '\in' T"
            (at level 101,
             t custom stlc, T custom stlc at level 0).

Ltac test_ltac ::=
  repeat match goal with
           | [ H : _ |- _ ] => clear H
         end.

(** Breaks [test_ltac]; try commenting it in/out. *)
Reserved Notation "Gamma '|-' t '\in' T"
            (at level 101,
             t custom stlc, T custom stlc at level 0).

(* Parse error *)
Ltac test_ltac :=
  repeat match goal with
           | [ H : _ |- _ ] => clear H
         end.

Paolo Giarrusso (Nov 07 2022 at 13:07):

hmm, forgot to test whether ltac shadows this notation — but this worked in other cases and I'm in a hurry right now...

Bas Spitters (Nov 07 2022 at 13:43):

Thanks! This helps to understand the issue. However, this will break the existing code. The user will need to type the space.
So, apparently, we'll need to change the notation into something like:

| -
|--
\|-

Paolo Giarrusso (Nov 07 2022 at 14:14):

hmm, actually, my minimization isn't conclusive... I believe this should be a grammar problem, but since I lack the cycles to investigate, I feel I should tag @Hugo Herbelin instead.

Yannick Forster (Nov 07 2022 at 15:33):

Hugo Herbelin (Nov 07 2022 at 15:54):

Yes, it is a grammar overlap. In match goal with [ x : u |- v ] => ... end, u is parsed as a constr at (highest) level 200, so, this includes accepting the notation Gamma |- t \in T. Thus, after u, it eagerly assumes the |- t \in T to continue this u.

Stream: Coq users

Topic: Tactic notation and custom entries

Bas Spitters (Nov 07 2022 at 12:21):