Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

notations scopes bound to types not honoured for raw arguments #524

Open
gares opened this issue Oct 18, 2023 · 4 comments
Open

notations scopes bound to types not honoured for raw arguments #524

gares opened this issue Oct 18, 2023 · 4 comments

Comments

@gares
Copy link
Contributor

gares commented Oct 18, 2023

https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users-.26-devs/topic/syntax.20scopes.20in.20raw.20arguments.20for.20commands

@gares
Copy link
Contributor Author

gares commented Oct 19, 2023

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.

@gares
Copy link
Contributor Author

gares commented Oct 19, 2023

@lukovdm I'm a bit confused here. I guess you want to activate siPropScope on bar by binding the scope to the siProp type. But here I don't see where the type would be imposed on bar. If you write f (bar g) then you get f (f g) as expected,
since the outer f expects a siProp hence its argument is parsed in that scope. I guess you "broke" your test case by minimizing it.

@lukovdm
Copy link

lukovdm commented Oct 23, 2023

You are right, I think I fixed my test case.

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 .

Local Open Scope core.

PrintCommand
Inductive foo : siProp :=
    | test : bar foo.

Thus, the bar from core is taken here instead of the one from siPropScope. And when writing f (bar foo) in de inductive defintion to get coq to recognize the bound scope we do get the correct bar.

@gares
Copy link
Contributor Author

gares commented Oct 26, 2023

I'm still confused. Take this example where I cut elpi out of the picture:

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 .

Local Open Scope core.


Inductive foo : siProp :=
    | test : bar foo.

I get:

Error: In environment
foo : siProp
The term "(fun (H : siProp) (_ : ?T@{y:=H}) => True) foo" has type
"?T@{foo:=foo; y:=foo} -> Prop" which should be Set, Prop or Type.

So coq uses the notation from core.
I don't get why you expect elpi to pick the notation from siPropScope.
After all, the expected value for bar foo is siProp, while its expected type is a sort. The Bind Scope mechanisms attaches the scope to a type, and open it on terms of that expected type.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants