universe polymoprhism

HB/common/database.elpi

@@ -12,7 +12,7 @@ pred from_mixin i:prop, o:mixinname.
 from_mixin (from _ X _) X.
 
 pred from_builder i:prop, o:term.
-from_builder (from _ _ X) (global X).
+from_builder (from _ _ X) R :- coq.env.global X R.
 
 pred mixin-src_mixin i:prop, o:mixinname.
 mixin-src_mixin (mixin-src _ M _) M.
@@ -59,7 +59,8 @@ instance-to-export_instance-nice (instance-to-export _ M _) M.
 pred abbrev-to-export_name i:prop, o:id.
 abbrev-to-export_name (abbrev-to-export _ N _) N.
 pred abbrev-to-export_body i:prop, o:term.
-abbrev-to-export_body (abbrev-to-export _ _ B) (global B).
+abbrev-to-export_body (abbrev-to-export _ _ B) R :-
+  coq.env.global B R.
 
 pred extract-builder i:prop, o:builder.
 extract-builder (builder-decl B) B.
@@ -114,7 +115,7 @@ factory-provides.one Params T B M (triple M PL T) :- std.do! [
 pred extract-conclusion-params i:term, i:term, o:list term.
 extract-conclusion-params TheType (prod _ S T) R :- !,
   @pi-decl _ S x\ extract-conclusion-params TheType (T x) R.
-extract-conclusion-params TheType (app [global GR|Args]) R :- !,
+extract-conclusion-params TheType T R :- coq.dest-gref-app T GR Args, !,
   factory-alias->gref GR Factory,
   factory-nparams Factory NP,
   std.map Args (copy-pack-holes TheType TheType) NewArgs,
@@ -272,22 +273,23 @@ assert-good-coverage! MLSortedRev CNL :- std.do! [
 
 % [get-structure-coercion S1 S2 F] finds the coecion F from the structure S1 to S2
 pred get-structure-coercion i:structure, i:structure, o:term.
-get-structure-coercion S T (global F) :-
+get-structure-coercion S T R :-
   coq.coercion.db-for (grefclass S) (grefclass T) L,
-  if (L = [pr F _]) true (coq.error "No one step coercion from" S "to" T).
+  if (L = [pr F _]) true (coq.error "No one step coercion from" S "to" T),
+  coq.env.global F R.
 
 pred get-structure-sort-projection i:structure, o:term.
 get-structure-sort-projection (indt S) Proj :- !,
   coq.env.projections S L,
   if (L = [some P, _]) true (coq.error "No canonical sort projection for" S),
-  Proj = global (const P).
+  coq.env.global (const P) Proj.
 get-structure-sort-projection S _ :- coq.error "get-structure-sort-projection: not a structure" S.
 
 pred get-structure-class-projection i:structure, o:term.
 get-structure-class-projection (indt S) T :- !,
   coq.env.projections S L,
   if (L = [_, some P]) true (coq.error "No canonical class projection for" S),
-  T = global (const P).
+  coq.env.global (const P) T.
 get-structure-class-projection S _ :- coq.error "get-structure-class-projection: not a structure" S.
 
 pred get-constructor i:gref, o:gref.
@@ -351,7 +353,7 @@ structure-nparams Structure NParams :-
 pred factory? i:term, o:w-args factoryname.
 factory? S (triple F Params T) :-
   not (var S), !,
-  safe-dest-app S (global GR) Args, factory-alias->gref GR F, factory-nparams F NP, !,
+  coq.dest-gref-app S GR Args, factory-alias->gref GR F, factory-nparams F NP, !,
   std.split-at NP Args Params [T|_].
 
 % [find-max-classes Mixins Classes] states that Classes is a list of classes

HB/common/log.elpi

@@ -28,14 +28,22 @@ strategy.set CL S :-
   coq.strategy.set CL S,
   log.private.log-vernac (log.private.coq.vernac.strategy CL S).
 
+pred upoly->flags4const i:prop.
+upoly->flags4const P :- upoly none none, !, P.
+upoly->flags4const P :- @univpoly! => P.
+
+pred upoly->flags4indt i:prop.
+upoly->flags4indt P :- upoly none none, !, P.
+upoly->flags4indt P :- @univpoly-cumul! => P.
+
 pred env.add-const-noimplicits i:id, i:term, i:term, i:opaque?, o:constant.
 env.add-const-noimplicits Name Bo Ty Opaque C :- std.do! [
   if (not(ground_term Ty ; ground_term Bo))
     (coq.error "HB: cannot infer some information in" Name
                ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
     true,
   avoid-name-collision Name Name1,
-  coq.env.add-const Name1 Bo Ty Opaque C,
+  upoly->flags4const (coq.env.add-const Name1 Bo Ty Opaque C),
   env.add-location (const C),
   if (var Ty) (Ty? = none) (Ty? = some Ty),
   log.private.log-vernac (log.private.coq.vernac.definition Name1 Ty? Bo),
@@ -49,7 +57,7 @@ env.add-const Name Bo Ty Opaque C :- std.do! [
                ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
     true,
   avoid-name-collision Name Name1,
-  coq.env.add-const Name1 Bo Ty Opaque C,
+  upoly->flags4const (coq.env.add-const Name1 Bo Ty Opaque C),
   env.add-location (const C),
   if (var Ty) (Ty? = none) (Ty? = some Ty),
   log.private.log-vernac (log.private.coq.vernac.definition Name1 Ty? Bo),
@@ -61,7 +69,7 @@ env.add-const-noimplicits-failondup Name Bo Ty Opaque C :- std.do! [
     (coq.error "HB: cannot infer some information in" Name
                ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
     true,
-  coq.env.add-const Name Bo Ty Opaque C,
+  upoly->flags4const (coq.env.add-const Name Bo Ty Opaque C),
   env.add-location (const C),
   if (var Ty) (Ty? = none) (Ty? = some Ty),
   log.private.log-vernac (log.private.coq.vernac.definition Name Ty? Bo),
@@ -87,7 +95,7 @@ env.add-indt Decl I :- std.do! [
   if (not(coq.ground-indt-decl? Decl))
     (coq.error "HB: cannot infer some information in" {coq.indt-decl->string Decl})
     true,
-  coq.env.add-indt Decl I,
+  upoly->flags4indt (coq.env.add-indt Decl I),
   (coq.env.record? I P ; P = ff),
   log.private.log-vernac (log.private.coq.vernac.inductive Decl P),
   env.add-location (indt I),

HB/common/phant-abbreviation.elpi

@@ -24,7 +24,8 @@ add-abbreviation N (private.phant-term AL T1) C Abbrev :- std.do! [
   NC is "phant_" ^ N,
   std.assert-ok! (coq.elaborate-skeleton T1 TTy T) "add-abbreviation: T illtyped",
   log.coq.env.add-const-noimplicits NC T TTy @transparent! C,
-  private.build-abbreviation 0 (global (const C)) AL NParams AbbrevT,
+  coq.env.global (const C) HD,
+  private.build-abbreviation 0 HD AL NParams AbbrevT,
   @global! => log.coq.notation.add-abbreviation N NParams AbbrevT tt Abbrev,
 ].
 
@@ -39,7 +40,7 @@ pred of-gref i:bool, i:gref, i:list mixinname, o:phant-term.
 of-gref WithCopy GRF RealMixinArgs PhBody:- !, std.do! [
   std.assert! (gref-deps GRF MLwP) "mk-phant-term: unknown gref",
   std.assert! (coq.env.typeof GRF FTy) "mk-phant-term: F illtyped",
-  coq.mk-eta (-1) FTy (global GRF) EtaF,
+  coq.mk-eta (-1) FTy {coq.env.global GRF} EtaF,
   % toposort-mixins ML MLSorted,
   MLwP = MLwPSorted, % Assumes we give them already sorted in dep order.
   std.rev {list-w-params_list MLwPSorted} MLSortedRev,
@@ -139,13 +140,13 @@ phant-fun Arg Ty PhF (phant-term [Arg|ArgL] (fun N Ty F)) :-
 pred phant-fun-mixin i:name, i:term, i:(term -> phant-term), o:phant-term.
 phant-fun-mixin N Ty PF (private.phant-term [Status|AL] (fun N Ty F)) :- !, std.do! [
   @pi-decl N Ty t\ PF t = private.phant-term AL (F t),
-  coq.safe-dest-app Ty (global Mixin) _,
+  coq.dest-gref-app Ty Mixin _,
   if (this-mixin-is-real-arg Mixin) (Status = private.real N) (Status = private.implicit)
 ].
 
 pred fun-unify-mixin i:term, i:name, i:term, i:(term -> phant-term), o:phant-term.
 fun-unify-mixin T N Ty PF Out :- !, std.do! [
-  coq.safe-dest-app Ty (global M) _,
+  coq.dest-gref-app Ty M _,
   Msg is "fun-unify-mixin: No mixin-src on " ^ {coq.term->string T},
   std.assert! (mixin-src T M Msrc) Msg,
   (@pi-decl `m` Ty m\ fun-unify none m Msrc (PF m) (PFM m)),
@@ -158,7 +159,7 @@ fun-unify-mixin T N Ty PF Out :- !, std.do! [
 pred phant-fun-struct i:term, i:name, i:structure, i:list term, i:(term -> phant-term), o:phant-term.
 phant-fun-struct T Name S Params PF Out :- std.do! [
   get-structure-sort-projection S SortProj,
-  mk-app (global S) Params SParams,
+  mk-app {coq.env.global S} Params SParams,
   mk-app SortProj Params SortProjParams,
   % Msg = {{lib:hb.nomsg}},
   Msg = some {{lp:SParams}},
@@ -200,6 +201,7 @@ build-type-pattern GR Pat :- build-type-pattern.aux GR {coq.env.typeof GR} Pat.
 build-type-pattern.aux GR T {{ lp:Pat _ }} :- coq.unify-eq T (prod N S T') ok, !,
   @pi-decl N S x\ build-type-pattern.aux GR (T' x) Pat.
 build-type-pattern.aux GR T (global GR) :- coq.unify-eq T {{ Type }} ok, !.
+build-type-pattern.aux GR T (pglobal GR _) :- coq.unify-eq T {{ Type }} ok, !.
 build-type-pattern.aux _ _ _ :- coq.error "HB: wrong carrier type".
 
 
@@ -237,13 +239,13 @@ pred mk-phant-term.mixins i:term, i:term, i:classname, i:phant-term,
   i:list term, i:name, i:term, i:(term -> list (w-args mixinname)), o:phant-term.
 mk-phant-term.mixins Target Src CN PF Params N Ty MLwA Out :- std.do! [
   class-def (class CN SI _),
-  mk-app (global SI) Params SIParams,
+  mk-app {coq.env.global SI} Params SIParams,
   coq.name-suffix N "local" Nlocal,
   (@pi-decl Nlocal Ty t\ sigma SK KC ML ParamsT SKPT\ std.do! [
     std.map (MLwA t) triple_1 ML,
     std.append Params [t] ParamsT,
-    SKPT = app [global {get-constructor SI} | ParamsT],
-    ClassTy t = app [global CN | ParamsT],
+    SKPT = app [{coq.env.global {get-constructor SI}} | ParamsT],
+    ClassTy t = app [{coq.env.global CN} | ParamsT],
     (@pi-decl `s` SIParams s\ @pi-decl `c` (ClassTy t) c\ sigma PF2\ std.do![
        synthesis.under-mixins.then (MLwA t) (fun-unify-mixin Target)
           (mk-phant-term.mixins.aux t Params c CN PF) PF2,

HB/common/stdpp.elpi

@@ -245,3 +245,16 @@ coq.fold-map (primitive _ as C) A C A :- !.
 coq.fold-map (uvar M L as X) A W A1 :- var X, !, std.fold-map L A coq.fold-map L1 A1, coq.mk-app-uvar M L1 W.
 % when used in CHR rules
 coq.fold-map (uvar X L) A (uvar X L1) A1 :- std.fold-map L A coq.fold-map L1 A1.
+
+pred upoly o:option upoly-decl, o:option upoly-decl-cumul.
+
+pred coq.unupoly-argument i:argument, o:argument, o:prop.
+coq.unupoly-argument (upoly-indt-decl I (upoly-decl _ _ _ _ as P))       (indt-decl I) (upoly (some P) none).
+coq.unupoly-argument (upoly-indt-decl I (upoly-decl-cumul _ _ _ _ as P)) (indt-decl I) (upoly none (some P)).
+coq.unupoly-argument (upoly-const-decl N B T P) (const-decl N B T) (upoly (some P) none).
+coq.unupoly-argument X X (upoly none none).
+
+pred coq.dest-gref-app i:term, o:gref, o:list term.
+coq.dest-gref-app T GR Args :-
+  coq.safe-dest-app T HD Args,
+  (HD = global GR ; HD = pglobal GR _).

HB/common/synthesis.elpi

@@ -30,7 +30,7 @@ infer-all-gref-deps Ps T GR X :- std.do! [
   std.assert! (gref-deps GR MLwP) "BUG: gref-deps should never fail",
   list-w-params_list MLwP ML,
   coq.env.typeof GR Ty,
-  coq.mk-eta (-1) Ty (global GR) EtaF,
+  coq.mk-eta (-1) Ty {coq.env.global GR} EtaF,
   coq.subst-fun {std.append Ps [T]} EtaF FT,
   private.instantiate-all-these-mixin-args FT T ML Xraw,
   infer-holes-depending-on-params T Xraw X,
@@ -40,24 +40,29 @@ infer-all-gref-deps Ps T GR X :- std.do! [
 pred infer-holes-depending-on-params i:term, i:term, o:term.
 infer-holes-depending-on-params T (app [global GR|Args]) (app [global GR|Args1]) :- !,
   std.map Args (infer-holes-depending-on-pack T) Args1.
+infer-holes-depending-on-params T (app [pglobal GR UI|Args]) (app [pglobal GR UI|Args1]) :- !,
+  std.map Args (infer-holes-depending-on-pack T) Args1.
 infer-holes-depending-on-params _ X X.
 
 pred class-of-phant i:term, o:gref, o:gref, o:gref.
 class-of-phant (prod N T F) X Y Z :- @pi-decl N T x\ class-of-phant (F x) X Y Z.
 class-of-phant (global GR) Y Z X :- class-def (class X GR _), get-constructor X Y, get-constructor GR Z.
+class-of-phant (pglobal GR _) Y Z X :- class-def (class X GR _), get-constructor X Y, get-constructor GR Z.
 class-of-phant (app[global GR|_]) Y Z X :- class-def (class X GR _), get-constructor X Y, get-constructor GR Z.
+class-of-phant (app[pglobal GR _|_]) Y Z X :- class-def (class X GR _), get-constructor X Y, get-constructor GR Z.
 
 pred infer-holes-depending-on-pack i:term, i:term, o:term.
-infer-holes-depending-on-pack T (app [global GR | Args]) S :-
+infer-holes-depending-on-pack T (app [HD | Args]) S :- coq.env.global GR HD,
   ((coq.gref->id GR GRS, rex.match "phant.*" GRS /*TODO: phant-clone? GR N*/);
     pack? GR _),
+    %% XXX shouldn't we put a bang here?
   coq.env.typeof GR Ty, class-of-phant Ty KC SC C,
   factory-nparams C N,
   std.take N Args Params, !,
   std.do! [
     infer-all-args-let Params T KC ClassInstance ok,
     std.rev [ClassInstance,T|{std.rev Params}] NewArgs,
-    S = app[global SC| NewArgs ]
+    S = app[{coq.env.global SC}| NewArgs ]
   ].
 infer-holes-depending-on-pack _ X X.
 
@@ -69,7 +74,7 @@ infer-holes-depending-on-pack _ X X.
 pred infer-all-args-let i:list term, i:term, i:gref, o:term, o:diagnostic.
 infer-all-args-let Ps T GR X Diag :- std.do! [
   coq.env.typeof GR Ty,
-  coq.mk-eta (-1) Ty (global GR) EtaF,
+  coq.mk-eta (-1) Ty {coq.env.global GR} EtaF,
   coq.subst-fun {std.append Ps [T]} EtaF FT,
   private.instantiate-all-args-let FT T X Diag,
 ].
@@ -206,7 +211,7 @@ mixin-for_mixin-builder (mixin-for _ _ B) B.
 pred builder->term i:list term, i:term, i:factoryname, i:mixinname, o:term.
 builder->term Ps T Src Tgt B :- !, std.do! [
   from Src Tgt FGR,
-  F = global FGR,
+  coq.env.global FGR F,
   gref-deps Src MLwP,
   list-w-params_list MLwP ML,
   infer-all-these-mixin-args Ps T ML F B,
@@ -220,7 +225,7 @@ builder->term Ps T Src Tgt B :- !, std.do! [
 % thus instanciating an abstraction on mixin M_i with X_i
 pred instantiate-all-these-mixin-args i:term, i:term, i:list mixinname, o:term.
 instantiate-all-these-mixin-args (fun _ Tm F) T ML R :-
-  coq.safe-dest-app Tm (global TmGR) _,
+  coq.dest-gref-app Tm TmGR _,
   factory-alias->gref TmGR M,
   std.mem! ML M,
   !,
@@ -232,7 +237,7 @@ instantiate-all-these-mixin-args F _ _ F.
 
 pred instantiate-all-args-let i:term, i:term, o:term, o:diagnostic.
 instantiate-all-args-let (fun N Tm F) T (let N Tm X R) Diag :- !, std.do! [
-  coq.safe-dest-app Tm (global TmGR) _,
+  coq.dest-gref-app Tm TmGR _,
   factory-alias->gref TmGR M,
   if (mixin-for T M X)
      (@pi-def N Tm X m\ instantiate-all-args-let (F m) T (R m) Diag)
@@ -253,18 +258,18 @@ structure-instance->mixin-srcs T S MSLC :- std.do! [
   structure-nparams S NParams,
   coq.mk-n-holes NParams Holes,
   std.append Holes [ST] HolesST,
-  coq.mk-app (global (const SortProj)) HolesST SortHolesST,
+  coq.mk-app {coq.env.global (const SortProj)} HolesST SortHolesST,
   % find an instance in ST
   coq.unify-eq T SortHolesST ok,
   % we look for an instance which is concrete, we take the parts
   get-constructor S KS,
-  coq.mk-app (global KS) {std.append Holes [T, CT]} KSHolesC,
+  coq.mk-app {coq.env.global KS} {std.append Holes [T, CT]} KSHolesC,
   coq.unify-eq ST KSHolesC ok,
   % if the class instance is concrete, we take the parts
   get-constructor (indt Class) KC,
   std.length {list-w-params_list CMLwP} CMixinsN,
   coq.mk-n-holes CMixinsN MIL,
-  coq.mk-app (global KC) {std.append Holes [T | MIL]} CBody,
+  coq.mk-app {coq.env.global KC} {std.append Holes [T | MIL]} CBody,
   coq.unify-eq CT CBody ok,
   % we finally generare micin-src clauses for all mixins
   std.map MIL (structure-instance->mixin-srcs.aux T) MSLL,
@@ -276,7 +281,7 @@ structure-instance->mixin-srcs T S MSLC :- std.do! [
 structure-instance->mixin-srcs _ _ [].
 
 structure-instance->mixin-srcs.aux2 Params T Class (some P) M :-
-  coq.mk-app (global (const P)) {std.append Params [T,Class]} M.
+  coq.mk-app {coq.env.global (const P)} {std.append Params [T,Class]} M.
 structure-instance->mixin-srcs.aux T  F CL :-
   factory-instance->new-mixins [] F ML,
   std.map ML (m\c\ c = mixin-src T m F) CL.
@@ -287,7 +292,7 @@ structure-instance->mixin-srcs.aux T  F CL :-
 pred factory-instance->new-mixins i:list mixinname, i:term, o:list mixinname.
 factory-instance->new-mixins OldMixins X NewML :- std.do! [
   std.assert-ok! (coq.typecheck X XTy) "mixin-src: X illtyped",
-  if (not (coq.safe-dest-app XTy (global _) _))
+  if (not (coq.dest-gref-app XTy _ _))
      (coq.error "Term:\n" {coq.term->string X}
                 "\nhas type:\n" {coq.term->string XTy}
                 "\nwhich is not a record")

HB/common/utils.elpi

@@ -6,6 +6,11 @@
 
 shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
 
+pred with-upoly-argument i:argument, i:(argument -> prop).
+with-upoly-argument UArg P :-
+  coq.unupoly-argument UArg Arg Flags,
+  Flags => P Arg.
+
 % HACK: move to coq-elpi proper, remove when coq-elpi > 1.9.2
 type attmap attribute-type.
 
@@ -203,7 +208,7 @@ params->holes (w-params.cons _ _ F) [_|PS] :- pi x\ params->holes (F x) PS.
 
 pred fresh-type o:term.
 fresh-type Ty :-
-  Ty = {{Type}},
+  Ty = sort(typ U), coq.univ.new U,
   std.assert-ok! (coq.typecheck-ty Ty _) "impossible".
 
 %%%%%%%%%%%%%%%%%%%%%%