syntax scopes in raw arguments for commands · Elpi users & devs

I'm working on a command interpreting Inductive statements that are not in Prop but in some other Prop like (Iris iProp, but that shouldn't matter). This other Prop has a notation scope bound to it and has fallbacks in the default notation scope for certain notations. Not I'm getting the problem that the fallback notation is used when interpreting the Inductive for Elpi. I have made a minimal example that should have thet same issue:

From elpi Require Import elpi.

#[arguments(raw)] Elpi Command PrintCommand.
Elpi Accumulate lp:{{

  % main is, well, the entry point
  main Arguments :- coq.say "PrintCommand" Arguments.

}}.
Elpi Typecheck.
Elpi Export PrintCommand.

Definition siProp := nat -> Prop.

Definition f : siProp -> siProp.
Admitted.

Declare Scope siPropScope.
Delimit Scope siPropScope with S.
Bind Scope siPropScope with siProp.

About f.

Notation "'bar'" := (fun n => True) : core .
Notation "'bar'" := (f) : siPropScope .

PrintCommand
Inductive foo : nat -> siProp :=
    | test g : bar g.

For this to work, you need to add a ( ... )%S around the bar g in the inductive, but I would like to forgo it. So I was wondering if there was a good solution for this?

Enrico Tassi (Oct 18 2023 at 21:10):

Luko van der Maas (Oct 19 2023 at 08:57):

I need an inductive with a type like nat -> siProp and coq gives the following error without raw arguments

Error: In environment
foo : nat -> siProp
g : siProp
The term "bar%S g" has type "siProp" which should be Set, Prop or Type.

Luko van der Maas (Oct 19 2023 at 08:59):

I am working on writing Iris fixpoints using the inductive notation using Elpi and the type of those predicates are always ... -> iProp

Paolo Giarrusso (Oct 19 2023 at 09:25):

"Iris fixpoint" can mean a bunch of things, but you might be talking about least fixpoints/inductive definitions?

So foo shouldn't become an inductive definition/least fixpoint in Coq's metalogic but in Iris's object logic (which can be done because it's a higher-order logic)

Luko van der Maas (Oct 19 2023 at 09:29):

Enrico Tassi (Oct 19 2023 at 14:14):

OK, you need ra arguments. For the scope thing, I guess it is a bug of mine. Especially for inductive types the various elaboration phases of Coq are mixed, and I had to write my own pipeline up to the lexical analysis part (notation unfolding and binder analysis). I've opened an issue, I'll look into it next week. For now I hope you are no blocked, at the cost of forcing scopes by hand.

Stream: Elpi users & devs

Topic: syntax scopes in raw arguments for commands