Ineol (Mar 22 2024 at 15:55): Ineol (Mar 22 2024 at 15:55):Hi, I am trying to match primitive projections but it does not work... is there an example somewhere of mathching, say, terms of the form x.(proj) t1 t2?
I tried {{ x.(proj) lp:t1 lp:t2 }} to no avail. And without quotations, I didn't manage to write terms of type projection to match on the argument to proj
Enrico Tassi (Mar 22 2024 at 19:09):The term constructor would beprimitive (proj _ _), hence app[primitive (proj _ _) X T1 T2
Ineol (Mar 22 2024 at 19:12):I got this far, but how do I specify which projection I want? e.g proj in the example above
Li-yao (Mar 22 2024 at 19:37):Here's an example:
From elpi Require Import elpi.
Set Primitive Projections.
Set Implicit Arguments.
Record Pair (a b : Type) : Type :=
{ p1 : a; p2 : b }.
Elpi Program bar lp:{{
pred m i:term.
m {{ lp:P.(p1) lp:X }} :- coq.say "P:" P, coq.say "X:" X.
}}.
Definition id2 : Pair (nat -> nat) nat := {| p1 := fun x => x ; p2 := 0 |}.
Elpi Query lp:{{
m {{ id2.(p1) 0 }}.
}}.
This was my test, but @Li-yao was faster ;-)
From elpi Require Import elpi.
#[projections(primitive)] Record r := { fst : nat -> nat; snd : bool }.
Axiom t : r.
Elpi Command test.
Elpi Query lp:{{
coq.say "quotation for primitive fst t" {{ t.(fst) 3 }},
coq.say "quotation for compat fst t" {{ fst t 3 }},
coq.locate "r" (indt I),
coq.env.projections I [some P1,some P2],
coq.say "compatibility constants" P1 P2,
coq.env.primitive-projections I [some (pr Q1 N1), some (pr Q2 N2)],
coq.say "fst primproj" Q1 N1,
coq.say "snd primproj" Q2 N2
}}.
Thank you to both of you!
Last updated: Oct 13 2024 at 01:02 UTC