Stream: Coq users

Topic: Tactic notation and custom entries


view this post on Zulip Bas Spitters (Nov 07 2022 at 12:21):

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?

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Paolo Giarrusso (Nov 07 2022 at 12:29):

More precise quote:

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

view this post on Zulip 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.

view this post on Zulip Bas Spitters (Nov 07 2022 at 12:32):

Thanks! So, after this I can no longer use |- in to define new tactics ??

view this post on Zulip 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).

no other changes _should_ be required.

Minimized testcase:

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.

view this post on Zulip 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...

view this post on Zulip 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:

| -
|--
\|-

view this post on Zulip 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.

view this post on Zulip Yannick Forster (Nov 07 2022 at 15:33):

Bas Spitters said:

So, apparently, we'll need to change the notation into something like:

| -
|--
\|-

Or ?

view this post on Zulip 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.


Last updated: Feb 08 2023 at 22:03 UTC