From daa28e6a32ef7e2481943dbb48cbb1748d72681c Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Sun, 12 Oct 2025 03:06:55 -0400 Subject: [PATCH 1/5] quantify over universes in build iota --- examples/example_record_expansion.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/examples/example_record_expansion.v b/examples/example_record_expansion.v index fb071970d..7100436f6 100644 --- a/examples/example_record_expansion.v +++ b/examples/example_record_expansion.v @@ -65,7 +65,9 @@ Elpi Accumulate lp:{{ pred build-iotared-clause i:term, i:(pair constant term), o:prop. build-iotared-clause T (pr Proj Var) C :- coq.env.global (const Proj) HD, % HD is the global term for Proj - C = (pi L AppVar\ expand(app [HD,T|L]) AppVar :- coq.mk-app Var L AppVar). + (HD = global _, !, C = (pi L AppVar\ expand(app [HD,T|L]) AppVar :- coq.mk-app Var L AppVar)); + (HD = pglobal _ _, !, C = (pi L AppVar U\ expand(app [(pglobal (const Proj) U),T|L]) AppVar :- coq.mk-app Var L AppVar)) + . % The core algorithm ---------------------------------------------------------- From 30847c42ccee83d0aceecad56f4fe2312574bad9 Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Sun, 12 Oct 2025 20:49:05 -0400 Subject: [PATCH 2/5] g works --- examples/example_record_expansion.v | 40 +++++++++++++++++++++-------- 1 file changed, 29 insertions(+), 11 deletions(-) diff --git a/examples/example_record_expansion.v b/examples/example_record_expansion.v index 7100436f6..24012cc01 100644 --- a/examples/example_record_expansion.v +++ b/examples/example_record_expansion.v @@ -146,9 +146,13 @@ pred expand-spine i:list prop, o:prop. % premises and final clause % if we find a lambda over the record R we expand -expand-spine (info R _ _ Projs K KTY as Info) (fun _ LTy Bo) Result AccL AccR Premises (pi r\ Clause r) :- coq.env.global (indt R) LTy, !, +expand-spine (info R _ _ Projs K KTY as Info) (fun _ LTy Bo) Result AccL AccR Premises (pi r\ Clause r) :- coq.env.global (indt R) LTy, LTy = global _, !, pi r\ expand-abstraction Info r KTY Projs (Bo r) Result {coq.env.global (indc K)} [] [r|AccL] AccR Premises (Clause r). +expand-spine (info R _ _ Projs K KTY as Info) (fun _ LTy Bo) Result AccL AccR Premises (pi r U\ Clause r U) :- + coq.env.global (indt R) LTy, LTy = pglobal _ _ , !, + pi r U\ expand-abstraction Info r KTY Projs (Bo r) Result (pglobal (indc K) U) [] [r|AccL] AccR Premises (Clause r U). + % otherwise we traverse the spine expand-spine Info (fun Name Ty Bo) (fun Name Ty1 Bo1) AccL AccR Premises (pi x y\ Clause x y) :- !, expand Ty Ty1, !, @@ -162,12 +166,18 @@ expand-spine Info (let Name Ty V Bo) (let Name Ty1 V1 Bo1) AccL AccR Premises (p expand-spine (info _ GR NGR _ _ _) X Y AccL AccR Premises Clause :- expand X Y, !, % we build "app[f,x1..xn|rest]" - (pi rest1\ coq.mk-app (global GR) {std.append {std.rev AccL} rest1} (L rest1)), - (pi rest2\ coq.mk-app (global NGR) {std.append {std.rev AccR} rest2} (R rest2)), - % we can now build the clause "expand (app[f,L1..Ln|Rest1]) (app[f1,R1..Rn|Rest2])" - % here we quantify only the tails, the other variables were quantified during - % expand-* - Clause = (pi rest1 rest2\ expand (L rest1) (R rest2) :- [!, std.map rest1 expand rest2 | Premises]). + if (coq.env.global GR (global _)) ( + (pi rest1\ coq.mk-app (global GR) {std.append {std.rev AccL} rest1} (L rest1)), + (pi rest2\ coq.mk-app (global NGR) {std.append {std.rev AccR} rest2} (R rest2)), + % we can now build the clause "expand (app[f,L1..Ln|Rest1]) (app[f1,R1..Rn|Rest2])" + % here we quantify only the tails, the other variables were quantified during + % expand-* + Clause = (pi rest1 rest2\ expand (L rest1) (R rest2) :- [!, std.map rest1 expand rest2 | Premises]) + ) ( + (pi rest1 U\ coq.mk-app (pglobal GR U) {std.append {std.rev AccL} rest1} (L' rest1 U)), + (pi rest2 U\ coq.mk-app (pglobal NGR U) {std.append {std.rev AccR} rest2} (R' rest2 U)), + Clause = (pi rest1 rest2 U1 U2\ expand (L' rest1 U1) (R' rest2 U2) :- [!, std.map rest1 expand rest2 | Premises]) + ). % The entry point of the main algorithm, just fetchs some data and passes initial % values for the accumulators. @@ -188,7 +198,9 @@ expand-gref Record (const C) Name Clause :- !, std.do! [ std.assert! (coq.env.const C (some Bo) _) "only transparent constants can be expanded", (pi nc\ expand-record Record (const C) nc Bo NewBo (NClause nc)), std.assert-ok! (coq.typecheck NewBo _) "illtyped", - coq.env.add-const Name NewBo _ _ NC, + if (coq.env.global (const C) (pglobal _ _ )) + (@univpoly! => coq.env.add-const Name NewBo _ _ NC) + (coq.env.add-const Name NewBo _ _ NC), Clause = NClause (const NC), ]. @@ -210,24 +222,30 @@ main [str R, str In, str Prefix] :- !, main _ :- coq.error "usage: Elpi record.expand record_name global_term prefix". }}. - +Set Universe Polymorphism. Record r := { T :> Type; X := T; op : T -> X -> bool }. Definition f b (t : r) (q := negb b) := fix rec (l1 l2 : list t) := match l1, l2 with | nil, nil => b - | cons x xs, cons y ys => andb (op _ x y) (rec xs ys) + | cons x xs, cons y ys => andb (op _ x y) (rec xs ys) | _, _ => q end. +Set Printing Universes. +Print T. +Print X. +Print op. + Elpi record.expand r f "expanded_". Print f. Print expanded_f. (* so that we can see the new "expand" clause *) -Elpi Print record.expand "elpi_examples/record.expand". +Elpi Print record.expand "elpi_examples/record.expand.poly". Definition g t l s h := (forall x y, op t x y = false) /\ f true t l s = h. +Elpi Trace Browser. Elpi record.expand r g "expanded_". Print expanded_g. From e2490fd28571458cd97af9a4a066928afbecb732 Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Mon, 13 Oct 2025 18:14:18 -0400 Subject: [PATCH 3/5] got rid of extraneous universes --- examples/example_record_expansion.v | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/examples/example_record_expansion.v b/examples/example_record_expansion.v index 24012cc01..ffca39b50 100644 --- a/examples/example_record_expansion.v +++ b/examples/example_record_expansion.v @@ -90,7 +90,6 @@ type info -> gref % the term being expanded and its expanded name -> list (option constant) % canonical projections -> constructor % record constructor - -> term % record constructor type -> info. % This predicate turns the OldBo in "fun x : r => OldBo" into @@ -146,11 +145,13 @@ pred expand-spine i:list prop, o:prop. % premises and final clause % if we find a lambda over the record R we expand -expand-spine (info R _ _ Projs K KTY as Info) (fun _ LTy Bo) Result AccL AccR Premises (pi r\ Clause r) :- coq.env.global (indt R) LTy, LTy = global _, !, +expand-spine (info R _ _ Projs K as Info) (fun _ LTy Bo) Result AccL AccR Premises (pi r\ Clause r) :- coq.env.global (indt R) LTy, LTy = global _, !, + coq.env.indt R _ _ _ _ _ [KTY], pi r\ expand-abstraction Info r KTY Projs (Bo r) Result {coq.env.global (indc K)} [] [r|AccL] AccR Premises (Clause r). -expand-spine (info R _ _ Projs K KTY as Info) (fun _ LTy Bo) Result AccL AccR Premises (pi r U\ Clause r U) :- - coq.env.global (indt R) LTy, LTy = pglobal _ _ , !, +expand-spine (info R _ _ Projs K as Info) (fun _ LTy Bo) Result AccL AccR Premises (pi r U\ Clause r U) :- + coq.env.global (indt R) LTy, LTy = pglobal _ UL , !, % U is a subset of the universes in the main term to be expanded. + (@uinstance! UL ==> coq.env.indt R _ _ _ _ _ [KTY]), % Be sure that K is instantiated with the same universe instance UL occurring in the binder LTy pi r U\ expand-abstraction Info r KTY Projs (Bo r) Result (pglobal (indc K) U) [] [r|AccL] AccR Premises (Clause r U). % otherwise we traverse the spine @@ -163,7 +164,7 @@ expand-spine Info (let Name Ty V Bo) (let Name Ty1 V1 Bo1) AccL AccR Premises (p pi x y\ expand x y ==> expand y y ==> expand-spine Info (Bo x) (Bo1 y) [x|AccL] [y|AccR] [expand x y|Premises] (Clause x y). % at the end of the spine we fire the iota redexes and complete the clause -expand-spine (info _ GR NGR _ _ _) X Y AccL AccR Premises Clause :- +expand-spine (info _ GR NGR _ _) X Y AccL AccR Premises Clause :- expand X Y, !, % we build "app[f,x1..xn|rest]" if (coq.env.global GR (global _)) ( @@ -176,16 +177,16 @@ expand-spine (info _ GR NGR _ _ _) X Y AccL AccR Premises Clause :- ) ( (pi rest1 U\ coq.mk-app (pglobal GR U) {std.append {std.rev AccL} rest1} (L' rest1 U)), (pi rest2 U\ coq.mk-app (pglobal NGR U) {std.append {std.rev AccR} rest2} (R' rest2 U)), - Clause = (pi rest1 rest2 U1 U2\ expand (L' rest1 U1) (R' rest2 U2) :- [!, std.map rest1 expand rest2 | Premises]) + Clause = (pi rest1 rest2 U\ expand (L' rest1 U) (R' rest2 U) :- [!, std.map rest1 expand rest2 | Premises]) ). % The entry point of the main algorithm, just fetchs some data and passes initial % values for the accumulators. pred expand-record i:inductive, i:gref, i:gref, i:term, o:term, o:prop. expand-record R GR NGR X Y Clause :- - std.assert! (coq.env.indt R tt 0 0 _ [K] [KTY]) "record is too complex for this example", + std.assert! (coq.env.indt R tt 0 0 _ [K] _) "record is too complex for this example", coq.env.projections R Projs, - expand-spine (info R GR NGR Projs K KTY) X Y [] [] [] Clause. + expand-spine (info R GR NGR Projs K) X Y [] [] [] Clause. % This simply dispatches between global references ---------------------------- From 6d9669cffff4585bbe7959f8185432ac0034ed1c Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Tue, 14 Oct 2025 04:41:33 -0400 Subject: [PATCH 4/5] discovered bug, fixed changes --- examples/example_record_expansion.v | 81 ++++++++++++++++++++--------- 1 file changed, 55 insertions(+), 26 deletions(-) diff --git a/examples/example_record_expansion.v b/examples/example_record_expansion.v index ffca39b50..cc4010bbc 100644 --- a/examples/example_record_expansion.v +++ b/examples/example_record_expansion.v @@ -63,11 +63,12 @@ Elpi Accumulate lp:{{ % This builds a clause to replace "proji (k y1..yn)" by "yi" pred build-iotared-clause i:term, i:(pair constant term), o:prop. -build-iotared-clause T (pr Proj Var) C :- - coq.env.global (const Proj) HD, % HD is the global term for Proj - (HD = global _, !, C = (pi L AppVar\ expand(app [HD,T|L]) AppVar :- coq.mk-app Var L AppVar)); - (HD = pglobal _ _, !, C = (pi L AppVar U\ expand(app [(pglobal (const Proj) U),T|L]) AppVar :- coq.mk-app Var L AppVar)) - . + +build-iotared-clause T (pr Proj Var) C :- coq.env.global (const Proj) (global _), !, + C = (pi L AppVar\ expand(app [(global (const Proj)),T|L]) AppVar :- coq.mk-app Var L AppVar). + +build-iotared-clause T (pr Proj Var) C :- coq.env.global (const Proj) (pglobal _ _), !, + C = (pi L AppVar U\ expand(app [(pglobal (const Proj) U),T|L]) AppVar :- coq.mk-app Var L AppVar). % The core algorithm ---------------------------------------------------------- @@ -223,30 +224,58 @@ main [str R, str In, str Prefix] :- !, main _ :- coq.error "usage: Elpi record.expand record_name global_term prefix". }}. -Set Universe Polymorphism. -Record r := { T :> Type; X := T; op : T -> X -> bool }. +Module WithoutPolymorphism. + Record r := { T :> Type; X := T; op : T -> X -> bool }. + + Definition f b (t : r) (q := negb b) := fix rec (l1 l2 : list t) := + match l1, l2 with + | nil, nil => b + | cons x xs, cons y ys => andb (op _ x y) (rec xs ys) + | _, _ => q + end. + + Elpi record.expand r f "expanded_". + Print f. + Print expanded_f. + + (* so that we can see the new "expand" clause *) + Elpi Print record.expand "elpi_examples/record.expand.poly". + + Definition g t l s h := (forall x y, op t x y = false) /\ f true t l s = h. + + Elpi record.expand r g "expanded_". + Print expanded_g. + + Definition id (t : r) := t. + Elpi record.expand r id "expanded_". + Print expanded_id. +End WithoutPolymorphism. + +Module WithPolymorphism. + Local Set Universe Polymorphism. + Record r := { T :> Type; X := T; op : T -> X -> bool }. + + Definition f b (t : r) (q := negb b) := fix rec (l1 l2 : list t) := + match l1, l2 with + | nil, nil => b + | cons x xs, cons y ys => andb (op _ x y) (rec xs ys) + | _, _ => q + end. -Definition f b (t : r) (q := negb b) := fix rec (l1 l2 : list t) := - match l1, l2 with - | nil, nil => b - | cons x xs, cons y ys => andb (op _ x y) (rec xs ys) - | _, _ => q - end. + Elpi record.expand r f "expanded_". + Print f. + Print expanded_f. -Set Printing Universes. -Print T. -Print X. -Print op. + (* so that we can see the new "expand" clause *) + Elpi Print record.expand "elpi_examples/record.expand.poly". -Elpi record.expand r f "expanded_". -Print f. -Print expanded_f. + Definition g t l s h := (forall x y, op t x y = false) /\ f true t l s = h. -(* so that we can see the new "expand" clause *) -Elpi Print record.expand "elpi_examples/record.expand.poly". + Elpi record.expand r g "expanded_". + Print expanded_g. -Definition g t l s h := (forall x y, op t x y = false) /\ f true t l s = h. + Definition id (t : r) := t. + Elpi record.expand r id "expanded_". + Print expanded_id. +End WithPolymorphism. -Elpi Trace Browser. -Elpi record.expand r g "expanded_". -Print expanded_g. From c348647c1affb69665faa835e42fdbfeabc43129 Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Tue, 14 Oct 2025 21:50:47 -0400 Subject: [PATCH 5/5] fixed identity --- examples/example_record_expansion.v | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/examples/example_record_expansion.v b/examples/example_record_expansion.v index cc4010bbc..ff41e0f0d 100644 --- a/examples/example_record_expansion.v +++ b/examples/example_record_expansion.v @@ -153,7 +153,8 @@ expand-spine (info R _ _ Projs K as Info) (fun _ LTy Bo) Result AccL AccR Premis expand-spine (info R _ _ Projs K as Info) (fun _ LTy Bo) Result AccL AccR Premises (pi r U\ Clause r U) :- coq.env.global (indt R) LTy, LTy = pglobal _ UL , !, % U is a subset of the universes in the main term to be expanded. (@uinstance! UL ==> coq.env.indt R _ _ _ _ _ [KTY]), % Be sure that K is instantiated with the same universe instance UL occurring in the binder LTy - pi r U\ expand-abstraction Info r KTY Projs (Bo r) Result (pglobal (indc K) U) [] [r|AccL] AccR Premises (Clause r U). + (pi r U\ expand-abstraction Info r KTY Projs (Bo r) (Result' U) (pglobal (indc K) U) [] [r|AccL] AccR Premises (Clause r U)), + Result = Result' UL. % otherwise we traverse the spine expand-spine Info (fun Name Ty Bo) (fun Name Ty1 Bo1) AccL AccR Premises (pi x y\ Clause x y) :- !, @@ -263,19 +264,27 @@ Module WithPolymorphism. end. Elpi record.expand r f "expanded_". + Section Universe. + Universe U. Print f. + Check f@{U}. Print expanded_f. + Check expanded_f@{U}. (* so that we can see the new "expand" clause *) Elpi Print record.expand "elpi_examples/record.expand.poly". Definition g t l s h := (forall x y, op t x y = false) /\ f true t l s = h. - Elpi record.expand r g "expanded_". + Check g@{U}. Print expanded_g. + Check expanded_g@{U}. Definition id (t : r) := t. Elpi record.expand r id "expanded_". Print expanded_id. + Check id@{U}. + Check expanded_id@{U}. + End Universe. End WithPolymorphism.