quantify over universes in build iota

examples/example_record_expansion.v

@@ -63,9 +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
-  C = (pi L AppVar\ expand(app [HD,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 ----------------------------------------------------------
 
@@ -88,7 +91,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
@@ -144,9 +146,16 @@ 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 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 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' 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) :- !,
   expand Ty Ty1, !,
@@ -157,23 +166,29 @@ 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]"
-  (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 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 ----------------------------
 
@@ -186,7 +201,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),
 ].
 
@@ -208,24 +225,66 @@ main [str R, str In, str Prefix] :- !,
 main _ :- coq.error "usage: Elpi record.expand record_name global_term prefix".
 }}.
 
+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.
+
+  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.
 
-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".
-
-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.