Pglobal (wip adapt to algebraic universes)

.nix/config.nix

@@ -2,7 +2,7 @@
   format = "1.0.0";
   attribute = "hierarchy-builder";
   no-rocq-yet = true;
-  default-bundle = "coq-8.20";
+  default-bundle = "coq-universes-clauses";
   bundles = let
     mcHBcommon = {
       mathcomp.override.version = "master";
@@ -29,23 +29,44 @@
       simple-io.override.version = "master";
       QuickChick.override.version = "master";
       # jasmin.override.version = "main";
-      jasmin.job = false;  # currently broken
+      jasmin.job = false; # currently broken
     };
   in {
-    "coq-master" = { rocqPackages = {
-      rocq-core.override.version = "master";
-      stdlib.override.version = "master";
-      rocq-elpi.override.version = "master";
-      rocq-elpi.override.elpi-version = "2.0.7";
-      bignums.override.version = "master";
-    }; coqPackages = mcHBcommon // {
-      coq.override.version = "master";
-      stdlib.override.version = "master";
-      coq-elpi.override.version = "master";
-      coq-elpi.override.elpi-version = "2.0.7";
-      bignums.override.version = "master";
-      coquelicot.job = false;
-    }; };
+    "coq-universes-clauses" = {
+      rocqPackages = {
+        rocq-core.override.version = "mattam82:universes-clauses";
+        stdlib.override.version = "master";
+        rocq-elpi.override.version = "CohenCyril:universes-clauses";
+        rocq-elpi.override.elpi-version = "2.0.7";
+        bignums.override.version = "master";
+      };
+      coqPackages = mcHBcommon // {
+        coq.override.version = "mattam82:universes-clauses";
+        stdlib.override.version = "master";
+        coq-elpi.override.version = "CohenCyril:universes-clauses";
+        coq-elpi.override.elpi-version = "2.0.7";
+        bignums.override.version = "master";
+        coquelicot.job = false;
+      };
+    };
+
+    "coq-master" = {
+      rocqPackages = {
+        rocq-core.override.version = "master";
+        stdlib.override.version = "master";
+        rocq-elpi.override.version = "master";
+        rocq-elpi.override.elpi-version = "2.0.7";
+        bignums.override.version = "master";
+      };
+      coqPackages = mcHBcommon // {
+        coq.override.version = "master";
+        stdlib.override.version = "master";
+        coq-elpi.override.version = "master";
+        coq-elpi.override.elpi-version = "2.0.7";
+        bignums.override.version = "master";
+        coquelicot.job = false;
+      };
+    };
 
     "coq-9.0".coqPackages = mcHBcommon // {
       coq.override.version = "9.0";
@@ -61,8 +82,8 @@
     };
 
   };
-  cachix.coq = {};
-  cachix.coq-community = {};
+  cachix.coq = { };
+  cachix.coq-community = { };
   cachix.math-comp.authToken = "CACHIX_AUTH_TOKEN";
 
 }

HB/about.elpi

@@ -38,7 +38,7 @@ main-located S (loc-abbreviation A) :- phant-abbrev GR PhB A, factory-constructo
 main-located S (loc-abbreviation A) :-
   coq.notation.abbreviation-body A NArgs _,
   coq.notation.abbreviation A {coq.mk-n-holes NArgs} T,
-  coq.safe-dest-app T (global GR) _, !,
+  coq.safe-dest-global-app T GR _, !,
   main-located S (loc-gref GR).
 
 main-located S (loc-gref GR) :- from Factory Mixin GR, !,
@@ -143,19 +143,19 @@ main-canonical-projection S Proj CanonicalProjectionValues :-
 
 pred pp-canonical-value i:cs-instance, o:coq.pp.
 pp-canonical-value (cs-instance _Proj (cs-gref GR) _Sol) Pp :-
-  coq.term->pp (global GR) V,
+  coq.term->pp {coq.env.global GR} V,
   Pp = box (hov 2) [ V , spc, {pp-loc-of GR} ].
 
 pred main-coercion i:string, i:list coercion.
 main-coercion S [coercion GR _ Src Tgt|_] :-
   % format
   if (class-def (class _ Src _) ; class-def (class Src _ _))
      (Source = str {gref->modname_short Src "."})
-     (coq.term->pp (global Src) Source),
+     (coq.term->pp {coq.env.global Src} Source),
   if2 (Tgt = grefclass TGR)
         (if (class-def (class _ TGR _) ; class-def (class TGR _ _))
           (Target = str {gref->modname_short TGR "."})
-          (coq.term->pp (global TGR) Target))
+          (coq.term->pp {coq.env.global TGR} Target))
       (Tgt = sortclass)
         (Target = str "Sortclass")
       (Target = str "Funclass"),
@@ -291,7 +291,7 @@ compute-arg-type.fields [OP|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :-
   (@pplevel! 200 => coq.term->pp TyArgsDepsRecord PPTy),
   @pi-parameter ID TyArgsDepsRecord op\
   (pi L L1 X\
-    copy (app[global(const OP)|L]) X :- std.drop ToDrop L L1, coq.mk-app op L1 X) =>
+    copy (app[{coq.env.global (const OP)}|L]) X :- std.drop ToDrop L L1, coq.mk-app op L1 X) =>
     compute-arg-type.fields Cs NDeps Args Xs FN.
 
 pred main-factory i:string, i:inductive.

HB/builders.elpi

@@ -90,7 +90,7 @@ declare-shadowed-constant (some C) :-
 
 pred declare-shadowed-located i:string, i:located.
 declare-shadowed-located Id (loc-gref GR) :-
-  @global! => log.coq.notation.add-abbreviation Id 0 (global GR) ff _.
+  @global! => log.coq.notation.add-abbreviation Id 0 {coq.env.global GR} ff _.
 declare-shadowed-located Id (loc-abbreviation Abbrev) :-
   coq.notation.abbreviation-body Abbrev NArgs T,
   @global! => log.coq.notation.add-abbreviation Id NArgs T ff _.
@@ -103,7 +103,7 @@ postulate-factory-abbrev TheType Params Name Falias TheFactory :- std.do! [
   Msg is "Unable to declare factory " ^ Name,
   std.assert-ok! (coq.typecheck-ty Package _) Msg,
   log.coq.env.add-section-variable-noimplicits Name Package C,
-  TheFactory = global (const C),
+  coq.env.global (const C) TheFactory,
 ].
 
 % Only record fields can be exported as operations.
@@ -121,14 +121,14 @@ define-factory-operation TheType Params TheFactory NHoles (some P) :-
   coq.mk-n-holes NHoles Holes,
   std.append Holes [TheFactory] Holes_Factory,
   std.append Params [TheType|Holes_Factory] Args,
-  T = app[global (const P)|Args],
+  T = app[{coq.env.global (const P)}|Args],
   std.assert-ok! (coq.typecheck T _) "Illtyped applied factory operation",
   coq.gref->id (const P) Name,
   @local! => log.coq.notation.add-abbreviation Name 0 T ff _.
 
 pred factory i:context-decl, o:string, o:gref.
 factory (context-item IDF _ T _ _\ context-end) IDF GR :- !,
-  coq.safe-dest-app T (global GR) _.
+  coq.safe-dest-global-app T GR _.
 factory (context-item _ _ _ _ R) IDF GR :- !, pi x\ factory (R x) IDF GR.
 factory _ _ _ :- !, coq.error "the last context item is not a factory".
 
@@ -146,4 +146,4 @@ postulate-factories ModName IDF CDecl :- std.do! [
   acc-clause current (current-mode (builder-from FKey TheFactory GRF ModName)),
 ].
 
-}
+}

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 _ _ GR) X :- coq.env.global GR X.
 
 pred mixin-src_mixin i:prop, o:mixinname.
 mixin-src_mixin (mixin-src _ M _) M.
@@ -59,7 +59,7 @@ 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 _ _ GR) B :- coq.env.global GR B.
 
 pred clause-to-export_clause i:prop, o:prop.
 clause-to-export_clause (clause-to-export _ C) C.
@@ -110,11 +110,13 @@ 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 :- !, std.do! [
+extract-conclusion-params TheType Tm R :-
+  coq.safe-dest-global-app Tm GR Args, !, std.do! [
   std.assert-ok! (factory-alias->gref GR Factory) "HB",
   factory-nparams Factory NP,
   std.map Args (copy-pack-holes TheType TheType) NewArgs,
-  std.take NP NewArgs R].
+  std.take NP NewArgs R
+  ].
 extract-conclusion-params TheType T R :- whd1 T T1, !, extract-conclusion-params TheType T1 R.
 
 
@@ -311,22 +313,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 Out :-
   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 Out.
 
 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.
@@ -350,18 +353,16 @@ has-cs-instance GTy (cs-instance _ (cs-gref GTy) _).
 
 
 pred mixin-src->has-mixin-instance i:prop, o:prop.
-mixin-src->has-mixin-instance  (mixin-src (global GR) M I) (has-mixin-instance (cs-gref GR) M IHd) :-
-  term->gref I IHd.
-
-mixin-src->has-mixin-instance (mixin-src (app [global GR|_] ) M I) (has-mixin-instance (cs-gref GR) M IHd) :-
-  term->gref I IHd.
-
 mixin-src->has-mixin-instance (mixin-src (prod _ _ _ ) M I) (has-mixin-instance cs-prod M IHd):-
   term->gref I IHd.
 
 mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd):-
   term->gref I IHd.
 
+mixin-src->has-mixin-instance  (mixin-src Src M I) (has-mixin-instance (cs-gref GR) M IHd) :- !,
+  coq.safe-dest-global-app Src GR _, !, term->gref I IHd.
+
+
 % this auxiliary function iterates over the list of arguments of an application,
 % and create the necessary unify condition for each arguments
 % and at the end returns the mixin-src clause with all the conditions
@@ -402,7 +403,7 @@ mixin-instance-type->mixin-src (prod N_ _ F) M I Cond (pi a \ C a) :-
 
 pred has-mixin-instance->mixin-src i:prop, o:prop.
 has-mixin-instance->mixin-src (has-mixin-instance _ M IHd) C :- std.do![
-  T = global IHd,
+  coq.env.global IHd T,
   coq.env.typeof IHd Ty,
   mixin-instance-type->mixin-src Ty M T [] C,
 ].
@@ -437,7 +438,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,
+  coq.safe-dest-global-app S GR Args,
   factory-alias->gref GR F ok,
   factory-nparams F NP, !,
   std.split-at NP Args Params [T|_].

HB/common/log.elpi

@@ -35,7 +35,7 @@ env.add-const-noimplicits 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,
+  @univpoly! => 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 +49,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,
+  @univpoly! => 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 +61,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,
+  @univpoly! => 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),
@@ -79,7 +79,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,
+  (@univpoly! => 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,7 @@ 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,
+  private.build-abbreviation 0 {coq.env.global (const C)} AL NParams AbbrevT,
   @global! => log.coq.notation.add-abbreviation N NParams AbbrevT tt Abbrev,
 ].
 
@@ -39,7 +39,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 +139,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.safe-dest-global-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.safe-dest-global-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 +158,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}},
@@ -199,7 +199,7 @@ pred build-type-pattern i:gref, o:term.
 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 G :- coq.unify-eq T {{ Type }} ok, !, coq.env.global GR G.
 build-type-pattern.aux _ _ _ :- coq.error "HB: wrong carrier type".
 
 
@@ -237,13 +237,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,
@@ -277,7 +277,7 @@ mk-phant-term.classes EtaF CNF PL Target Src MLwA PhF :- !, std.do! [
   std.map MLwA triple_1 ML,
   synthesis.under-mixins.then MLwA phant-fun-mixin (out\ sigma FPLTM\ std.do! [
     synthesis.infer-all-these-mixin-args PL Target ML EtaF FPLTM,
-    std.fold CNF (phant-term [] FPLTM) (mk-phant-term.class Target Src) out]) PhF
+    std.fold CNF (phant-term [] FPLTM) (mk-phant-term.class Target Src) out]) PhF,
 ].
 
 pred mk-phant-term-with-copy i:term, i:list classname,