Stream: Elpi users & devs

Topic: Undeclared macro exception

Cyril Cohen (Jan 04 2024 at 15:03):

I'm trying to define custom macros but I have an error that I reduced to the following snippet.

From elpi Require Import elpi.
Elpi Command test.
Elpi Accumulate lp:{{ macro @nil :- []. }}.
Elpi Typecheck.
Elpi Query lp:{{ coq.say @nil. }}.

On the last line, I get the following error:

Errors:
Anomaly "Uncaught exception Elpi__Compiler.CompileError(_, "Undeclared macro @nil")."
Please report at http://coq.inria.fr/bugs/.;

I'm using Coq 8.18.0, elpi 1.17.0 and coq-elpi 1.19.0 in this test.

Cyril Cohen (Jan 04 2024 at 15:03):

CC @Enrico Tassi

Enrico Tassi (Jan 04 2024 at 15:15):

The problem is that macros a still implemented as a hack, they are not hygienic (see https://github.com/LPCIC/elpi/blob/master/ELPI.md#caveat) so I did limit their scope to the current block.
This means that your macro does not escape the curly braces. There is one exception, macros declared in the prelude, and these are always present.

Enrico Tassi (Jan 04 2024 at 15:17):

Maybe I can suggest an alternative for you use case if you tell me what it is.

Cyril Cohen (Jan 04 2024 at 15:21):

I have two use cases:

1. to denote certain concrete lists of elements that we keep using all the time (namely [map0, map1, map2a, map2b, map3, map4] et al.) and
2. to abbreviate some specific grefs (eq, sym_rel) that I registered and can write {{:gref lib:foo}}but that I would like to abbreviate further.

Cyril Cohen (Jan 04 2024 at 15:21):

currently I have predicates instead:

pred map-classes o:class-kind, o:list map-class.
map-classes all [map0, map1, map2a, map2b, map3, map4].
map-classes low [map0, map1, map2a].
map-classes high [map2b, map3, map4].

pred sym-rel o:gref.
sym-rel {{:gref lib:trocq.sym_rel}}.

pred paths o:gref.
paths {{:gref lib:trocq.paths}}.

Cyril Cohen (Jan 04 2024 at 15:23):

but curiously I cannot write std.forall {map-classes all} x\ ... all the time, due to a strange Unification problem outside the pattern fragment.

Enrico Tassi (Jan 04 2024 at 15:23):

So doesn't {map-classes all} do what you want already?

Cyril Cohen (Jan 04 2024 at 15:23):

not under a binder...

Enrico Tassi (Jan 04 2024 at 15:24):

hum... that one I'd like to see

Cyril Cohen (Jan 04 2024 at 15:24):

e.g.

std.forall {map-classes all} (m\
    std.forall {map-classes all} (n\
      generate-module (pc m n) U L
    )
  ).

outputs

Unification problem outside the pattern fragment. ((Data.Term.AppUVar (
   { Data.Term.contents = please extend this printer; uid_private = 12651292
     },
   0, [(Data.Term.Const map0)])) == (Data.Term.Cons ((Data.Term.Const map0),
   (Data.Term.Cons ((Data.Term.Const map1),
      (Data.Term.Cons ((Data.Term.Const map2a),
         (Data.Term.Cons ((Data.Term.Const map2b),
            (Data.Term.Cons ((Data.Term.Const map3),
               (Data.Term.Cons ((Data.Term.Const map4), Data.Term.Nil))))
            ))
         ))
      ))
   ))) Pass -delay-problems-outside-pattern-fragment (elpi command line utility) or set delay_outside_fragment to true (Elpi_API) in order to delay (deprecated, for Teyjus compatibility).;

Cyril Cohen (Jan 04 2024 at 15:25):

Everything is fine if I do this instead:

  map-classes all Classes,
  std.forall {map-classes all} (m\
    std.forall Classes (n\
      generate-module (pc m n) U L
    )
  ).

Enrico Tassi (Jan 04 2024 at 15:28):

I see. There is no way out.
In this specific case I'd suggest a std.allpairs L1 L2 P

Cyril Cohen (Jan 04 2024 at 15:30):

:shrug:

Cyril Cohen (Jan 04 2024 at 15:30):

I wonder where the unification problem comes from

Cyril Cohen (Jan 04 2024 at 15:31):

and in this particular case we don't care about unhygenic macros, I have no possible capture

Enrico Tassi (Jan 04 2024 at 17:58):

That i can explain. After the first beta, m gets map0. The variable used for the spilling sees it, so one gets map-clauses all (TMP map0) hence the unif problem in the error message.

I think the language feature we miss is a way to declare the spilling destination, which would be outside the m\ and hence avoid the crazy unif problem.

Cyril Cohen (Jan 04 2024 at 18:05):

{map-clauses all}^

Cyril Cohen (Jan 04 2024 at 18:05):

:stuck_out_tongue_wink:

Cyril Cohen (Jan 04 2024 at 18:05):

Thanks for the explanation

Enrico Tassi (Jan 04 2024 at 20:20):

I had the converse in mind. Maybe the default should be the topmost conjunction (assuming std.do! becomes a primitive) and {foo bar|x y} the syntax to keep the spilling under x and y.

In your case it would just work, and in other cases it would be akin to sigma x\ in the sense that you explicitly put a thing under, rather than over, a binder

Cyril Cohen (Jan 04 2024 at 20:59):

you know what's best

Cyril Cohen (Jan 04 2024 at 21:00):

that would break lots of usercode though

Cyril Cohen (Jan 04 2024 at 21:01):

how about {foo bar|} for topmost {foo bar} (and {foo bar|*} ?) for closest (as before) and {foo bar|x y} to be specific

Cyril Cohen (Jan 04 2024 at 21:02):

(and {foo bar|*} as an alternative syntax for {foo bar})

Enrico Tassi (Jan 04 2024 at 21:34):

With a warning if {foo bar} is used under a binder... looks like a good compromise

Last updated: Oct 13 2024 at 01:02 UTC