From bf926b3e9b2546bd6ff307323197673b258a7b82 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Tue, 3 Nov 2020 18:44:08 +0100
Subject: [PATCH 1/4] minimal porting, no test with polymorphism

---
 hb.elpi      | 159 ++++++++++++++++++++++++++-------------------------
 structures.v |  10 ++--
 2 files changed, 86 insertions(+), 83 deletions(-)

diff --git a/hb.elpi b/hb.elpi
index 3daff910..b2f869ed 100644
--- a/hb.elpi
+++ b/hb.elpi
@@ -122,12 +122,12 @@ argument->gref (str S) GR :- located->gref S {coq.locate-all S} GR.
 argument->gref X _ :- coq.error "Argument" X "is expected to be a string".
 
 pred argument->term i:argument, o:term.
-argument->term (str S) (global GR) :- !, argument->gref (str S) GR.
+argument->term (str S) T :- !, argument->gref (str S) GR, coq.env.global GR T.
 argument->term (trm T) T1 :- !, std.assert-ok! (coq.elaborate-skeleton T _ T1) "not well typed term".
 argument->term X _ :- coq.error "Argument" X " is expected to be a term or a string".
 
 pred argument->ty i:argument, o:term.
-argument->ty (str S) T1 :- !, argument->gref (str S) GR, std.assert-ok! (coq.elaborate-ty-skeleton (global GR) _ T1) "global reference is not a type".
+argument->ty (str S) T1 :- !, argument->gref (str S) GR, std.assert-ok! (coq.elaborate-ty-skeleton (global GR _) _ T1) "global reference is not a type".
 argument->ty (trm T) T1 :- !, std.assert-ok! (coq.elaborate-ty-skeleton T _ T1) "not well typed type".
 argument->ty X _ :- coq.error "Argument" X " is expected to be a type or a string".
 
@@ -165,14 +165,14 @@ argument->asset (const-decl Id (some Bo) (arity Ty)) (asset-alias Id Bo) :- !,
 argument->asset X _ :- coq.error "Unsupported asset:" X.
 
 pred builder->string i:builder, o:string.
-builder->string (builder _ _ _ B) S :- coq.term->string (global B) S.
+builder->string (builder _ _ _ B) S :- coq.term->string (global B _) S.
 
 pred nice-gref->string i:gref, o:string.
 nice-gref->string X Mod :-
   coq.gref->path X Path,
   std.rev Path [_,Mod|_], !.
 nice-gref->string X S :-
-  coq.term->string (global X) S.
+  coq.term->string (global X _) S.
 
 pred target-gref i:term, o:gref.
 target-gref T GR :- whd1 T T1, !, target-gref T1 GR.
@@ -366,13 +366,14 @@ 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) T :- coq.env.global X T.
 
 pred mixin-src_mixin i:prop, o:mixinname.
 mixin-src_mixin (mixin-src _ M _) M.
 
 pred mixin-src_src i:prop, o:term.
 mixin-src_src (mixin-src _ _ S) S.
+mixin-src_src (pi c\ mixin-src _ _ c :- F c) T :- F T. % this is a bit pulp...
 
 
 pred extract-builder i:prop, o:builder.
@@ -424,7 +425,7 @@ factory-provides.one Params T B M (triple M PL T) :- std.do! [
 pred extract-conclusion-params i:term, o:list term.
 extract-conclusion-params (prod _ S T) R :- !,
   @pi-decl _ S x\ extract-conclusion-params (T x) R.
-extract-conclusion-params (app [global GR|Args]) R :- !,
+extract-conclusion-params (app [global GR _|Args]) R :- !,
   factory-alias->gref GR Factory,
   factory-nparams Factory NP,
   std.take NP Args R.
@@ -533,26 +534,28 @@ findall-newjoins CurrentClass AllSuper TodoJoins :-
 
 % [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 (global S) (global T) (global F) :-
+get-structure-coercion (global S _) (global T _) FU :-
   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 FU.
 
 % TODO
 pred get-structure-sort-projection i:structure, o:term.
 get-structure-sort-projection T Proj :-
-  safe-dest-app T (global (indt S)) Params,
+  safe-dest-app T (global (indt S) _) Params,
   coq.CS.canonical-projections S L,
   if (L = [some P, _]) true (coq.error "No canonical sort projection for" S),
-  mk-app (global (const P)) Params Proj.
+  mk-app {coq.env.global (const P)} Params Proj.
 
 pred get-structure-class-projection i:structure, o:term.
-get-structure-class-projection (global (indt S)) (global (const P)) :-
+get-structure-class-projection (global (indt S) _) T :-
   coq.CS.canonical-projections S L,
-  if (L = [_, some P]) true (coq.error "No canonical class projection for" S).
+  if (L = [_, some P]) true (coq.error "No canonical class projection for" S),
+  coq.env.global (const P) T.
 
 pred get-constructor i:term, o:gref.
-get-constructor (global (indt R) as S) (indc K) :- !,
- if (coq.env.indt R _ _ _ _ [K] _) true (coq.error "Not a record" S).
+get-constructor (global (indt R) UI as S) (indc K) :- !,
+ if (coq.env.indt R UI _ _ _ _ [K] _) true (coq.error "Not a record" S).
 
 pred safe-head i:term, o:term.
 safe-head (prod N T Body) Hd :-
@@ -564,8 +567,8 @@ safe-head T Hd :- safe-dest-app T Hd _.
 
 %% finding for locally defined structures
 pred get-cs-structure i:cs-instance, o:term.
-get-cs-structure (cs-instance _ _ (global Inst)) Struct :- std.do! [
-  coq.env.typeof Inst InstTy,
+get-cs-structure (cs-instance _ _ (global Inst UI)) Struct :- std.do! [
+  coq.env.typeof Inst UI InstTy,
   safe-head InstTy Struct
 ].
 
@@ -598,7 +601,7 @@ get-canonical-mixins-of T S MSL :- std.do! [
   if (coq.unify-eq T SortHolesST ok) (
     % Hum, this unification problem is not super trivial. TODO replace by something simpler
     get-constructor S KS,
-    coq.mk-app (global KS) {std.append Holes [T, C]} KSHolesC,
+    coq.mk-app {coq.env.global KS} {std.append Holes [T, C]} KSHolesC,
     std.assert-ok! (coq.unify-eq ST KSHolesC) "HB: get-canonical-mixins-of: ST = _ _ C",
     C = app Stuff,
     std.drop {calc (NParams + 2)} Stuff MIL,
@@ -669,7 +672,7 @@ phant-fun-implicit N Ty PF (phant-term [implicit-arg|AL] (fun N Ty F)) :- !,
 
 pred phant-fun-unify-mixin i:term, i:name, i:term, i:(term -> phant-term), o:phant-term.
 phant-fun-unify-mixin T N Ty PF Out :- !, std.do! [
-  safe-dest-app Ty (global M) _,
+  safe-dest-app Ty (global M _) _,
   Msg is "phant-fun-unify-mixin: No mixin-src on " ^ {coq.term->string T},
   std.assert! (mixin-src T M Msrc) Msg,
   (@pi-decl `m` Ty m\ phant-fun-unify {{lib:hb.nomsg}} m Msrc (PF m) (PFM m)),
@@ -693,7 +696,7 @@ phant-fun-struct T Name SI PF Out :- std.do! [
 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,
   factory-requires Src MLwP,
   list-w-params_list MLwP ML,
   mterm->term (mterm Ps T ML F) B,
@@ -707,7 +710,7 @@ builder->term Ps T Src Tgt B :- !, std.do! [
 % thus instanciating an abstraction on mixin M_i with X_i
 pred instantiate-mixin i:term, i:mixinname, i:term, o:term.
 instantiate-mixin T M (fun _ Tm F) R :-
-  safe-dest-app Tm (global TmGR) _,
+  safe-dest-app Tm (global TmGR _) _,
   factory-alias->gref TmGR M, !,
   mixin-for T M X, !,
   R = F X.
@@ -732,12 +735,12 @@ mterm->term (mterm Ps T ML F) SFX :- std.do! [
 pred mgref->term i:list term, i:term, i:gref, o:term.
 mgref->term Ps T GR X :- factory-requires GR MLwP, !, std.do! [
   list-w-params_list MLwP ML,
-  mterm->term (mterm Ps T ML (global GR)) X
+  mterm->term (mterm Ps T ML {coq.env.global GR}) X
 ].
 mgref->term Ps T GR X :- !, std.do! [
   std.assert! (gr-deps GR MLwP) "BUG: gr-deps should never fail",
   list-w-params_list MLwP ML,
-  mterm->term (mterm Ps T ML (global GR)) X
+  mterm->term (mterm Ps T ML {coq.env.global GR}) X
 ].
 
 % [mixin-srcs T X MSL] states that MSL is a list of [mixin-src T m X]
@@ -746,7 +749,7 @@ mgref->term Ps T GR X :- !, std.do! [
 pred mixin-srcs i:term, i:term, o:list prop.
 mixin-srcs T X MSL :- std.do! [
   std.assert-ok! (coq.typecheck X XTy) "mixin-src: X illtyped",
-  if (not (safe-dest-app XTy (global _) _))
+  if (not (safe-dest-app XTy (global _ _) _))
      (coq.error "Term:\n" {coq.term->string X}
                 "\nhas type:\n" {coq.term->string XTy}
                 "\nwhich is not a record")
@@ -816,7 +819,7 @@ assert!-mixin-for T M B :-
 
 pred factory? i:term, o:w-args factoryname.
 factory? S (triple F Params T) :-
-  safe-dest-app S (global GR) Args, factory-alias->gref GR F, factory-nparams F NP, !,
+  safe-dest-app S (global GR _) Args, factory-alias->gref GR F, factory-nparams F NP, !,
   std.split-at NP Args Params [T|_].
 
 pred prod-src-is-factory i:term.
@@ -855,7 +858,7 @@ term-deps T ML :-
 
 % shorthand for gref.
 pred gr-deps i:gref, o:list-w-params mixinname.
-gr-deps GR ML :- term-deps (global GR) ML.
+gr-deps GR ML :- term-deps {coq.env.global GR} ML.
 
 % [find-max-classes Mixins Classes] states that Classes is a list of classes
 %   which contain all the mixins in Mixins.
@@ -919,14 +922,14 @@ mk-phant-abbrev N (phant-term AL T) C Abbrev :- std.do! [
   NC is "phant_" ^ N,
   std.assert-ok! (coq.typecheck T TTy) "mk-phant-abbrev: T illtyped",
   hb-add-const NC T TTy @transparent! C,
-  mk-phant-abbrev.term 0 (global (const C)) AL NParams AbbrevT,
+  mk-phant-abbrev.term 0 {coq.env.global (const C)} AL NParams AbbrevT,
   @global! => coq.notation.add-abbreviation N NParams AbbrevT tt Abbrev,
 ].
 
 % [acc-phant-abbrev Str GR PhGR Abbrev] makes a phantom abbreviation for F
 pred acc-phant-abbrev i:string, i:gref, o:gref, o:abbreviation.
 acc-phant-abbrev Str GR (const PhC) Abbrev :- !, std.do! [
-  mk-phant-term (global GR) PhGR,
+  mk-phant-term {coq.env.global GR} PhGR,
   mk-phant-abbrev Str PhGR PhC Abbrev
 ].
 
@@ -938,7 +941,7 @@ pred phant-mixin-real o:mixinname.
 pred phant-fun-mixin i:name, i:term, i:(term -> phant-term), o:phant-term.
 phant-fun-mixin N Ty PF (phant-term [Status|AL] (fun N Ty F)) :- !, std.do! [
   @pi-decl N Ty t\ PF t = phant-term AL (F t),
-  safe-dest-app Ty (global Mixin) _,
+  safe-dest-app Ty (global Mixin _) _,
   if (phant-mixin-real Mixin) (Status = real-arg N) (Status = implicit-arg)
 ].
 
@@ -980,8 +983,8 @@ mk-phant-term.mixins T CN PF Params N Ty MLwA Out :- std.do! [
   (@pi-decl Nlocal Ty t\ sigma SK KC ML\ std.do! [
     std.map (MLwA t) triple_1 ML,
     std.append Params [T] ParamsT,
-    SKPT = app [global {get-constructor SI} | ParamsT],
-    ClassTy = app [global CN | ParamsT],
+    SKPT = app [{coq.env.global {get-constructor SI}} | ParamsT],
+    ClassTy = app [{coq.env.global CN} | ParamsT],
     (@pi-decl `s` SIParams s\ @pi-decl `c` ClassTy c\ sigma PF2\ std.do![
        under-mixins.then (MLwA t) (phant-fun-unify-mixin T) (mk-phant-term.mixins.aux t Params c CN PF) PF2,
        phant-fun-unify NoMsg s {mk-app SKPT [c]} PF2 (PFU t s c)])
@@ -991,7 +994,7 @@ mk-phant-term.mixins T CN PF Params N Ty MLwA Out :- std.do! [
 ].
 
 mk-phant-term.mixins.aux T Params C CN PF X :- std.do![
-  get-constructor (global CN) KC,
+  get-constructor {coq.env.global CN} KC,
   mgref->term Params T KC KCM,
   phant-fun-unify {{lib:hb.nomsg}} KCM C PF X,
 ].
@@ -1097,7 +1100,7 @@ params->holes (w-params.cons _ _ F) [_|PS] :- pi x\ params->holes (F x) PS.
 pred declare-instances i:term, i:list class.
 declare-instances T [class Class Struct MLwP|Rest] :-
   params->holes MLwP Params,
-  get-constructor (global Class) KC,
+  get-constructor {coq.env.global Class} KC,
 
   if (not(local-cs? T Struct))
      true % we build it
@@ -1119,7 +1122,7 @@ declare-instances T [class Class Struct MLwP|Rest] :-
   if-verbose (coq.say "HB: declare canonical structure instance" Name),
 
   get-constructor Struct KS,
-  mk-app (global KS) {std.append Params [T, KCApp]} S,
+  mk-app {coq.env.global KS} {std.append Params [T, KCApp]} S,
   std.assert-ok! (coq.typecheck S STy) "declare-instances: S illtyped",
 
   hb-add-const Name S STy @transparent! CS, % Bug coq/coq#11155, could be a Let
@@ -1135,7 +1138,7 @@ type factory-by-phantabbrev abbreviation -> factory-abbrev.
 pred declare-factory-abbrev i:id, i:factory-abbrev.
 declare-factory-abbrev Name (factory-by-classname GR) :-
   % looks fishy (the parameters are not taken into account)
-  @global! => coq.notation.add-abbreviation Name 1 (fun _ _ t\ app[global GR,t]) tt _.
+  @global! => coq.notation.add-abbreviation Name 1 (fun _ _ t\ app[{coq.env.global GR},t]) tt _.
 declare-factory-abbrev Name (factory-by-phantabbrev Abbr) :-
   coq.notation.abbreviation-body Abbr Nargs AbbrTrm,
   @global! => coq.notation.add-abbreviation Name Nargs AbbrTrm tt _.
@@ -1180,7 +1183,7 @@ postulate-arity (parameter ID _ S A) Acc T T1 Ty :-
   if-verbose (coq.say "HB: postulating" ID),
   if (var S) (coq.fresh-type S) true,
   @local! => hb-add-const ID _ S @opaque! C,
-  Var = global (const C),
+  coq.env.global (const C) Var,
   postulate-arity (A Var) [Var|Acc] T T1 Ty.
 postulate-arity (arity Ty) ArgsRev X T Ty :-
   hd-beta X {std.rev ArgsRev} X1 Stack1,
@@ -1191,7 +1194,7 @@ postulate-arity (arity Ty) ArgsRev X T Ty :-
 % all its dependencies, previously postulated and associated
 % to the corresponding mixin using mixin-for
 pred postulate-mixin i:w-args mixinname, i:list prop, o:list prop.
-postulate-mixin (triple M Ps T) MSL [mixin-src T M (global (const C))|MSL] :- MSL => std.do! [
+postulate-mixin (triple M Ps T) MSL [(pi c\ mixin-src T M c :- coq.env.global (const C) c)|MSL] :- MSL => std.do! [
   Name is "mixin_" ^ {gref->modname M},
 
   if-verbose (coq.say "HB: postulate" Name "on" {coq.term->string T}),
@@ -1250,8 +1253,8 @@ clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
   w-params.nparams MLwP NParams,
   std.length {list-w-params_list MLwP} NMixins,
 
-  (pi L L1 Params Rest PoArgs\
-    copy (app [global (const Po)| L]) (app [global (const C) | L1]) :-
+  (pi L L1 Params Rest PoArgs u1 u2\
+    copy (app [global (const Po) u1 | L]) (app [global (const C) u2| L1]) :-
       std.split-at NParams L Params [_|Rest],
       std.drop NMixins Rest PoArgs,
       std.append Params [S|PoArgs] L1) =>
@@ -1328,13 +1331,13 @@ pred mk-coe-class-body
   i:list (w-args mixinname),
   o:term.
 mk-coe-class-body FC TC TMLwP Params T _ CoeBody :- std.do! [
-  mk-app (global FC) {std.append Params [T]} Class,
+  mk-app {coq.env.global FC} {std.append Params [T]} Class,
 
   list-w-params_list TMLwP TML,
   std.map TML (from FC) Builders,
-  std.map Builders (x\r\mk-app (global x) Params r) BuildersP,
+  std.map Builders (x\r\sigma t\ coq.env.global x t, mk-app t Params r) BuildersP,
 
-  mk-app (global {get-constructor (global TC)})
+  mk-app {coq.env.global {get-constructor {coq.env.global TC}}}
     {coq.mk-n-holes {factory-nparams TC}} KCHoles,
 
   (pi c\ sigma Mixes\
@@ -1362,7 +1365,7 @@ mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProj
   mk-app ClassProjection Params ClassP,
   mk-app Coercion        Params CoercionP,
 
-  mk-app (global {get-constructor StructureT})
+  mk-app {coq.env.global {get-constructor StructureT}}
     {coq.mk-n-holes {factory-nparams TC}} PackPH,
 
   SCoeBody = {{ fun s : lp:StructureP =>
@@ -1395,7 +1398,7 @@ declare-coercion SortProjection ClassProjection
   hb-add-const CName CoeBody Ty @transparent! C,
   @global! => coq.coercion.declare (coercion (const C) 1 FC (grefclass TC)),
 
-  Coercion = global (const C),
+  coq.env.global (const C) Coercion,
   w-params.then FMLwP mk-fun ignore
     (mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProjection)
     SCoeBody,
@@ -1441,7 +1444,7 @@ declare-join (class C3 S3 MLwP3) (pr (class C1 S1 _) (class C2 S2 _)) (join C1 C
 
   if-verbose (coq.say "HB: declare unification hint" Name),
   w-params.fold MLwP3 mk-fun (join-body N1 N2 S3
-    (global S2_Pack) S1_sort S3_to_S1 S2_class S3_to_S2) JoinBody,
+    {coq.env.global S2_Pack} S1_sort S3_to_S1 S2_class S3_to_S2) JoinBody,
   std.assert-ok! (coq.typecheck JoinBody Ty) "declare-join: JoinBody illtyped",
   hb-add-const Name JoinBody Ty @transparent! J,
   coq.CS.declare-instance (const J).
@@ -1484,8 +1487,9 @@ pred mk-record+sort-field i:name, i:term, i:(term -> record-decl), o:indt-decl.
 mk-record+sort-field _ T F (record "type" {{ Type }} "Pack" (field _ "sort" T F)).
 
 pred mk-class-field i:classname, i:list term, i:term, i:list (w-args mixinname), o:record-decl.
-mk-class-field ClassName Params T _ (field _ "class" (app [global ClassName|Args]) _\end-record) :-
-  std.append Params [T] Args.
+mk-class-field ClassName Params T _ (field _ "class" (app [C|Args]) _\end-record) :-
+  std.append Params [T] Args,
+  coq.env.global ClassName C.
 
 % Builds the axioms record and the factories from this class to each mixin
 % TODO params
@@ -1516,14 +1520,14 @@ declare-class+structure MLwP (indt ClassInd) Structure SortProjection ClassProje
   coq.env.add-indt StructureDeclaration StructureName,
 
   coq.CS.canonical-projections StructureName [some SortP, some ClassP],
-  Structure = global (indt StructureName),
-  SortProjection = global (const SortP),
-  ClassProjection = global (const ClassP),
+  coq.env.global (indt StructureName) Structure,
+  coq.env.global (const SortP) SortProjection,
+  coq.env.global (const ClassP) ClassProjection,
 ].
 
 % Declares "sort" as a coercion Structurename >-> Sortclass
 pred declare-sort-coercion i:term, i:term.
-declare-sort-coercion (global StructureName) (global Proj) :-
+declare-sort-coercion (global StructureName _) (global Proj _) :-
 
   if-verbose (coq.say "HB: declare sort coercion"),
 
@@ -1540,7 +1544,7 @@ if-class-already-exists-error N [class _ S ML1wP|CS] ML2 :-
 pred export-mixin-coercion i:classname, i:option constant.
 export-mixin-coercion _ none.
 export-mixin-coercion ClassName (some C) :-
-  coq.env.typeof (const C) CTy,
+  coq.env.typeof (const C) _ CTy,
   safe-dest-app {safe-head CTy} Mixin _,
   coq.term->gref Mixin MixinGR,
   if-verbose (coq.say "HB: export class to mixin coercion for mixin" {nice-gref->string MixinGR}),
@@ -1548,19 +1552,19 @@ export-mixin-coercion ClassName (some C) :-
     coq.coercion.declare (coercion (const C) _ ClassName (grefclass MixinGR)).
 
 pred mc-compat-structure i:string, i:modpath, i:list mixinname, i:int, i:classname, i:term, i:option gref.
-mc-compat-structure ModuleName Module NewMixins CNParams ClassName ClassProjection Axioms :- std.do! [
+mc-compat-structure ModuleName _ NewMixins CNParams ClassName ClassProjection Axioms :- std.do! [
   CompatModuleName is "MathCompCompat" ^ ModuleName,
   coq.env.begin-module CompatModuleName none, % to avoid collisions
   coq.env.begin-module ModuleName none,
 
   if (Axioms = some GR)
-    (@global! => coq.notation.add-abbreviation "axiom" 0 (global GR) ff _)
+    (@global! => coq.notation.add-abbreviation "axiom" 0 {coq.env.global GR} ff _)
     true,
 
   if (NewMixins = [NewMixin]) (std.do! [
     if-verbose (coq.say "mc-compat-structure: declaring notations 'axioms', 'mixin_of' and 'Mixin'"),
     MArgs is {factory-nparams NewMixin} + 1,
-    mk-eta MArgs {coq.env.typeof NewMixin} (global NewMixin) EtaNewMixin,
+    mk-eta MArgs {coq.env.typeof NewMixin _} {coq.env.global NewMixin} EtaNewMixin,
     @global! => coq.notation.add-abbreviation "axioms" MArgs EtaNewMixin ff _,
     @global! => coq.notation.add-abbreviation "mixin_of" MArgs EtaNewMixin ff _,
     std.assert! (factory-constructor NewMixin FK) "BUG: Factory constructor missing",
@@ -1583,16 +1587,15 @@ mc-compat-structure ModuleName Module NewMixins CNParams ClassName ClassProjecti
   coq.env.end-module _,
   coq.env.end-module MCCompat,
   coq.env.export-module MCCompat,
-  %coq.env.import-module Module,
 ].
 
 pred clone-phant-body i:factoryname, i:term, i:term, i:list term, i:term, i:list (w-args mixinname), o:phant-term.
-clone-phant-body ClassName SortProjection (global (indt I) as Structure) PL T _ PhF :- std.do! [
-  std.assert! (coq.env.indt I _ _ _ _ [PackC] _) "wtf",
-  mk-app (global (indc PackC)) {std.append PL [T]} PackPLT,
+clone-phant-body ClassName SortProjection (global (indt I) UI as Structure) PL T _ PhF :- std.do! [
+  std.assert! (coq.env.indt I UI _ _ _ _ [PackC] _) "wtf",
+  mk-app (global (indc PackC) UI) {std.append PL [T]} PackPLT,
   mk-app Structure PL SPL,
   (@pi-decl `cT` SPL cT\
-  mk-app (global ClassName) {std.append PL [T]} CPL,
+  mk-app {coq.env.global ClassName} {std.append PL [T]} CPL,
   @pi-decl `c` CPL c\
   (Ph cT c) =
     {phant-fun-unify {{lib:hb.nomsg}} T {mk-app {mk-app SortProjection PL} [cT]}
@@ -1607,13 +1610,13 @@ clone-phant-body ClassName SortProjection (global (indt I) as Structure) PL T _
 pred pack-body.mixins i:list term, i:term, i:gref, i:gref, o:term.
 pack-body.mixins PL T BuildC PackS Body :- !, std.do! [
   mgref->term PL T BuildC Class,
-  mk-app (global PackS) {std.append PL [T, Class]} Body
+  mk-app {coq.env.global PackS} {std.append PL [T, Class]} Body
 ].
 
 pred pack-body i:classname, i:list term, i:term, i:list (w-args mixinname), o:term.
 pack-body ClassName PL T MLwA F :- std.do! [
   class-def (class ClassName S _),
-  get-constructor (global ClassName) BuildC,
+  get-constructor {coq.env.global ClassName} BuildC,
   get-constructor S PackS,
   under-mixins.then MLwA mk-fun (pack-body.mixins PL T BuildC PackS) F
 ].
@@ -1753,23 +1756,23 @@ main-end-declare-builders :- std.do! [
 
 pred add-mixin i:term, i:factoryname, i:bool, i:mixinname, i:term, o:list prop.
 add-mixin T FGR MakeCanon MissinMixin Bo [MixinSrcCl, BuiderDeclCl] :-
-  MixinSrcCl = mixin-src T MixinName (global (const C)),
+  MixinSrcCl = (pi c\ mixin-src T MixinName c :- coq.env.global (const C) c),
   BuiderDeclCl = builder-decl (builder N FGR MixinName (const C)),
   new_int N, % timestamp
 
   std.assert-ok! (coq.typecheck Bo Ty) "declare-instances: mixin illtyped",
-  safe-dest-app Ty (global MixinNameAlias) _,
+  safe-dest-app Ty (global MixinNameAlias _) _,
   factory-alias->gref MixinNameAlias MixinName,
 
   std.assert! (MissinMixin = MixinName) "HB: anomaly: we built the wrong mixin",
 
   % If the mixin instance is alreaduy a constant there is no need to
   % alias it.
-  if (Bo = global (const C)) true
+  if (Bo = global (const C) _) true
     (Name is {nice-gref->string FGR} ^"_to_" ^ {nice-gref->string MixinName} ^ "__" ^ {std.any->string {new_int}},
      if-verbose (coq.say "HB: declare" Name),
      hb-add-const Name Bo Ty @transparent! C),
-  if (MakeCanon = tt, whd (global (const C)) [] (global (indc _)) _)
+  if (MakeCanon = tt, whd {coq.env.global (const C)} [] (global (indc _) _) _)
      (if-verbose (coq.say "HB: declare canonical mixin instance" C),
       coq.CS.declare-instance (const C))
      true.
@@ -1828,7 +1831,7 @@ main-declare-instance T F [] :-
 
 pred declare-old-located i:string, i:located.
 declare-old-located Id (loc-gref GR) :-
-  @global! => coq.notation.add-abbreviation Id 0 (global GR) ff _.
+  @global! => coq.notation.add-abbreviation Id 0 {coq.env.global GR} ff _.
 declare-old-located Id (loc-abbreviation Abbrev) :-
   coq.notation.abbreviation Abbrev [] T,
   % FIXME: this assumes the abbreviation has no arg
@@ -1877,13 +1880,13 @@ 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,
   @local! => hb-add-const Name _ Package @opaque! C,
-  TheFactory = global (const C),
+  coq.env.global (const C) TheFactory,
 ].
 
 % Only record fields can be exported as operations.
 pred define-factory-operations i:term, i:term, i:gref.
 define-factory-operations TheType TheFactory (indt I) :- !,
-  coq.env.indt I _ NParams _ _ _ _,
+  coq.env.indt I _ _ NParams _ _ _ _,
   NHoles is NParams - 1,
   coq.CS.canonical-projections I PL,
   std.forall PL (define-factory-operation TheType TheFactory NHoles).
@@ -1894,7 +1897,7 @@ define-factory-operation _ _ _ none.
 define-factory-operation TheType TheFactory NHoles (some P) :-
   coq.mk-n-holes NHoles Holes,
   std.append Holes [TheFactory] Holes_Factory,
-  T = app[global (const P), TheType|Holes_Factory],
+  T = app[{coq.env.global (const P)}, TheType|Holes_Factory],
   std.assert-ok! (coq.typecheck T _) "Illtyped applied factory operation",
   coq.gref->id (const P) Name,
   @local! => coq.notation.add-abbreviation Name 0 T ff _.
@@ -1912,7 +1915,7 @@ builders-postulate-factories (context-item IDT _ TySkel none t\ context-item IDF
      (std.assert-ok! (coq.unify-eq Ty {{Type}}) "The last context item before the factory must be a type variable"),
   if-verbose (coq.say "HB: postulating type" IDT),
   @local! => hb-add-const IDT _ Ty @opaque! C, % no body, local -> a variable
-  TheType = global (const C),
+  coq.env.global (const C) TheType,
 
   std.assert! (factory? (TF TheType) (triple GRF Params TheType))
     "the last argument must be a factory applied to the type variable",
@@ -1928,7 +1931,7 @@ builders-postulate-factories (context-item ID _ TSkel none Factories) :- std.do!
   std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "builders-postulate-factorie: illtyped context",
   if (var T) (coq.fresh-type T) true,
   @local! => hb-add-const ID _ T @opaque! P, % no body, local -> a variable
-  TheParam = global (const P),
+  coq.env.global (const P) TheParam,
   builders-postulate-factories (Factories TheParam),
 ].
 
@@ -1966,7 +1969,7 @@ process-asset-named-parameters (asset-parameter Name T Rest as R) D Module Param
   if (var T) (fresh-indexed-type Ty) (Ty = T),
   @local! => hb-add-const Name _ Ty @opaque! C, % no body, local -> a variable
 
-  TheType = global (const C),
+  coq.env.global (const C) TheType,
   % We postulate the dependencies
   process-asset-unnamed-parameters (Rest TheType) [] Module TheType D {std.rev Params}
 ].
@@ -1976,7 +1979,7 @@ process-asset-named-parameters (asset-parameter Name T Rest) D Module Params :-
   if-verbose (coq.say "HB: postulate " Name),
   if (var T) (coq.fresh-type T) true,
   @local! => hb-add-const Name _ T @opaque! C, % no body, local -> a variable
-  TheParam = global (const C),
+  coq.env.global (const C) TheParam,
   process-asset-named-parameters (Rest TheParam) D Module [pr TheParam T|Params],
 ].
 
@@ -2010,19 +2013,19 @@ declare-factory-alias Ty1Skel GRFSwP Module TheType TheParams :- std.do! [
   std.assert-ok! (coq.elaborate-ty-skeleton Ty1Skel _ Ty1) "Illtyped alias factory",
   hb-add-const "axioms_" Ty1 _ @transparent! C,
 
-  std.assert! (safe-dest-app Ty1 (global PhF) _Args) "Argument must be a factory",
+  std.assert! (safe-dest-app Ty1 (global PhF _) _Args) "Argument must be a factory",
   std.assert! (factory-alias->gref PhF F) "BUG: Factory alias declaration missing",
   std.assert! (factory-constructor F FK) "BUG: Factory constructor missing",
 
   Hyps => mgref->term TheParams TheType FK MFK,
   std.assert-ok! (coq.typecheck MFK MFKTy) "BUG: typecking of former factory constructor failed",
-  (pi Args\ copy (app [global F|Args]) (global (const C))) => copy MFKTy MFKTyC,
+  (pi Args u1 u2\ copy (app [global F u1|Args]) (global (const C) u2)) => copy MFKTy MFKTyC,
   hb-add-const "Axioms_" MFK MFKTyC @transparent! CK,
   GRK = const CK,
 
   coq.env.end-section,
 
-  mk-phant-term (global GRK) PhGRK0,
+  mk-phant-term {coq.env.global GRK} PhGRK0,
   if (mixin-first-class F _) (PhGRK = PhGRK0) (append-phant-unify PhGRK0 PhGRK),
   mk-phant-abbrev "Build" PhGRK BuildConst _,
 
@@ -2081,13 +2084,13 @@ declare-mixin-or-factory Sort1 Fields0 GRFSwP Module TheType D TheParams :- std.
   std.assert-ok! (coq.elaborate-indt-decl-skeleton RDeclSkel RDecl) "record declaration illtyped",
   coq.env.add-indt RDecl R,
   coq.env.end-section,
-  coq.env.indt R tt _ _ _ [K] _,
+  coq.env.indt R _ tt _ _ _ [K] _,
   GRK = indc K,
 
   % TODO: should this be in the Exports module?
   if-verbose (coq.say "HB: declare notation axioms"),
 
-  mk-phant-term (global GRK) PhGRK0,
+  mk-phant-term {coq.env.global GRK} PhGRK0,
 
   if-verbose (coq.say "HB: declare notation Axioms"),
 
diff --git a/structures.v b/structures.v
index 9fc8d1a6..76b797a9 100644
--- a/structures.v
+++ b/structures.v
@@ -163,8 +163,8 @@ Elpi Accumulate lp:{{
 
 pred pp-from i:prop.
 pp-from (from F M T) :-
-  coq.say "From" {coq.term->string (global F)} "to" {coq.term->string (global M)},
-  coq.say "  " {coq.term->string (global T)},
+  coq.say "From" {coq.term->string (global F _)} "to" {coq.term->string (global M _)},
+  coq.say "  " {coq.term->string (global T _)},
   coq.say "".
 
 pred pp-list-w-params i:list-w-params mixinname, i:term.
@@ -178,7 +178,7 @@ pp-list-w-params.list-triple L S :-
   coq.say {coq.term->string S} ":=",
   std.forall L pp-list-w-params.triple.
 pp-list-w-params.triple (triple M Params T) :-
-  coq.say "  " {coq.term->string (app [global M|{std.append Params [T]}])}.
+  coq.say "  " {coq.term->string (app [global M _|{std.append Params [T]}])}.
 
 pred pp-class i:prop.
 pp-class (class-def (class _ S MLwP)) :-
@@ -345,14 +345,14 @@ main [const-decl Name (some BodySkel) TyWPSkel] :- !, std.do! [
     postulate-arity TyWP [] Body SectionBody SectionTy
   ),
 
-  std.assert! (coq.safe-dest-app SectionTy (global FactoryAlias) Args) "The type of the instance is not a factory",
+  std.assert! (coq.safe-dest-app SectionTy (global FactoryAlias _) Args) "The type of the instance is not a factory",
   factory-alias->gref FactoryAlias Factory,
   std.assert! (factory-nparams Factory NParams) "Not a factory synthesized by HB",
   hack-section-discharging SectionBody SectionBodyHack,
   if (Name = "_")
      (TheFactory = SectionBodyHack)
      (hb-add-const Name SectionBodyHack _ @transparent! C,
-      TheFactory = (global (const C))),
+      coq.env.global (const C) TheFactory),
   std.appendR {coq.mk-n-holes NParams} [TheType|_] Args,
   with-attributes (main-declare-instance TheType TheFactory Clauses),
 

From 07b7a4940095a5616ee98a7cb1dd1e4fdfc19c1f Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 5 Nov 2020 17:02:51 +0100
Subject: [PATCH 2/4] clanup

---
 hb.elpi      | 148 ++++++++++++++++++++++++++-------------------------
 structures.v |   8 +--
 2 files changed, 80 insertions(+), 76 deletions(-)

diff --git a/hb.elpi b/hb.elpi
index b2f869ed..96a11e66 100644
--- a/hb.elpi
+++ b/hb.elpi
@@ -204,9 +204,6 @@ gref->modname GR ModName :-
   coq.gref->path GR Path,
   if (std.rev Path [_,ModName|_]) true (coq.error "No enclosing module for " GR).
 
-pred term->modname i:structure, o:id.
-term->modname T ModName :- gref->modname {term->gref T} ModName.
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % function to predicate generic constructions %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -375,6 +372,14 @@ pred mixin-src_src i:prop, o:term.
 mixin-src_src (mixin-src _ _ S) S.
 mixin-src_src (pi c\ mixin-src _ _ c :- F c) T :- F T. % this is a bit pulp...
 
+pred class_name i:class, o:classname.
+class_name (class N _ _) N.
+
+pred class-def_name i:prop, o:classname.
+class-def_name (class-def (class N _ _)) N.
+
+pred classname->def i:classname, o:class.
+classname->def CN (class CN S ML) :- class-def (class CN S ML), !.
 
 pred extract-builder i:prop, o:builder.
 extract-builder (builder-decl B) B.
@@ -466,9 +471,9 @@ toposort-proj.acc Proj ES Acc [A|In] Out :- std.do![
 ].
 
 % Classes can be topologically sorted according to the subclass relation
-pred toposort-classes.mk-class-edge i:prop, o:pair class class.
+pred toposort-classes.mk-class-edge i:prop, o:pair classname classname.
 toposort-classes.mk-class-edge (sub-class C1 C2) (pr C2 C1).
-pred toposort-classes i:list class, o:list class.
+pred toposort-classes i:list classname, o:list classname.
 toposort-classes In Out :- std.do! [
   std.findall (sub-class C1_ C2_) SubClasses,
   std.map SubClasses toposort-classes.mk-class-edge ES,
@@ -476,10 +481,11 @@ toposort-classes In Out :- std.do! [
 ].
 
 pred findall-classes o:list class.
-findall-classes CLSorted :- std.do! [
+findall-classes CLSortedDef :- std.do! [
   std.findall (class-def C_) All,
-  std.map All (x\r\ x = class-def r) CL,
-  toposort-classes CL CLSorted
+  std.map All class-def_name CL,
+  toposort-classes CL CLSorted,
+  std.map CLSorted classname->def CLSortedDef,
 ].
 
 pred findall-builders o:list builder.
@@ -534,55 +540,54 @@ findall-newjoins CurrentClass AllSuper TodoJoins :-
 
 % [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 (global S _) (global T _) FU :-
+get-structure-coercion S T FU :-
   coq.coercion.db-for (grefclass S) (grefclass T) L,
   if (L = [pr F _]) true (coq.error "No one step coercion from" S "to" T),
   coq.env.global F FU.
 
-% TODO
 pred get-structure-sort-projection i:structure, o:term.
-get-structure-sort-projection T Proj :-
-  safe-dest-app T (global (indt S) _) Params,
+get-structure-sort-projection (indt S) Proj :- !,
   coq.CS.canonical-projections S L,
   if (L = [some P, _]) true (coq.error "No canonical sort projection for" S),
-  mk-app {coq.env.global (const P)} Params Proj.
+  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 (global (indt S) _) T :-
+get-structure-class-projection (indt S) T :- !,
   coq.CS.canonical-projections S L,
   if (L = [_, some P]) true (coq.error "No canonical class projection for" S),
   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:term, o:gref.
-get-constructor (global (indt R) UI as S) (indc K) :- !,
- if (coq.env.indt R UI _ _ _ _ [K] _) true (coq.error "Not a record" S).
+pred get-constructor i:gref, o:gref.
+get-constructor (indt R) (indc K) :- !,
+ if (coq.env.indt R _ _ _ _ _ [K] _) true (coq.error "Not a record" R).
+get-constructor I _ :- coq.error "get-constructor: not an inductive" I.
 
-pred safe-head i:term, o:term.
-safe-head (prod N T Body) Hd :-
-  @pi-decl N T x\
-    safe-head (Body x) (Hd' x),
-    std.assert! (Hd' x = Hd) "safe-head: the head symbol is a bound variable".
-safe-head T Hd :- whd1 T T', safe-head T' Hd.
-safe-head T Hd :- safe-dest-app T Hd _.
+pred head-gref-under-prods i:term, o:gref.
+head-gref-under-prods (prod N T Body) Hd :-
+  @pi-decl N T x\ head-gref-under-prods (Body x) Hd.
+head-gref-under-prods T Hd :- whd1 T T', head-gref-under-prods T' Hd.
+head-gref-under-prods T Hd :- safe-dest-app T (global Hd _) _.
 
 %% finding for locally defined structures
-pred get-cs-structure i:cs-instance, o:term.
-get-cs-structure (cs-instance _ _ (global Inst UI)) Struct :- std.do! [
-  coq.env.typeof Inst UI InstTy,
-  safe-head InstTy Struct
+pred get-cs-structure i:cs-instance, o:structure.
+get-cs-structure (cs-instance _ _ Inst) Struct :- std.do! [
+  coq.env.typeof Inst _ InstTy,
+  head-gref-under-prods InstTy Struct
 ].
 
 pred has-cs-instance i:gref, i:cs-instance.
 has-cs-instance GTy (cs-instance _ (cs-gref GTy) _).
 
-pred get-local-structures i:term, o:list term.
+pred get-local-structures i:term, o:list structure.
 get-local-structures TyTrm StructL :- std.do! [
   std.filter {coq.CS.db} (has-cs-instance {term->gref TyTrm}) DBGTyL,
   std.map DBGTyL get-cs-structure RecL,
   std.filter RecL is-structure StructL
 ].
 
-pred local-cs? i:term, i:term.
+pred local-cs? i:term, i:structure.
 local-cs? TyTerm Struct :-
   get-local-structures TyTerm StructL,
   std.mem! StructL Struct.
@@ -679,16 +684,17 @@ phant-fun-unify-mixin T N Ty PF Out :- !, std.do! [
   phant-fun-implicit N Ty PFM Out
 ].
 
-% [phant-fun-struct T SI PF PSF] states that PSF is a phant-term
+% [phant-fun-struct T SI SIParams PF PSF] states that PSF is a phant-term
 % which postulate a structure [s : SI] such that [T = sort s]
 % and then outputs [PF s]
-pred phant-fun-struct i:term, i:name, i:term, i:(term -> phant-term), o:phant-term.
-phant-fun-struct T Name SI 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 SI Params PF Out :- std.do! [
   get-structure-sort-projection SI Sort,
+  mk-app {coq.env.global SI} Params SITerm,
   % Msg = {{lib:hb.nomsg}},
-  Msg = {{lib:hb.some (lib:hb.pair "is not canonically a"%string lp:SI)}},
-  (@pi-decl Name SI s\ phant-fun-unify Msg T {mk-app Sort [s]} (PF s) (UnifSI s)),
-  phant-fun-implicit Name SI UnifSI Out
+  Msg = {{lib:hb.some (lib:hb.pair "is not canonically a"%string lp:SITerm)}},
+  (@pi-decl Name SITerm s\ phant-fun-unify Msg T {mk-app Sort [s]} (PF s) (UnifSI s)),
+  phant-fun-implicit Name SITerm UnifSI Out
 ].
 
 % [builder->term Params T Src Tgt MF] provides a term which is
@@ -977,7 +983,7 @@ pred mk-phant-term.mixins 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 T CN PF Params N Ty MLwA Out :- std.do! [
   class-def (class CN SI _),
-  mk-app SI Params SIParams,
+  mk-app {coq.env.global SI} Params SIParams,
   NoMsg = {{lib:hb.nomsg}},
   coq.name-suffix N "local" Nlocal,
   (@pi-decl Nlocal Ty t\ sigma SK KC ML\ std.do! [
@@ -989,12 +995,12 @@ mk-phant-term.mixins T CN PF Params N Ty MLwA Out :- std.do! [
        under-mixins.then (MLwA t) (phant-fun-unify-mixin T) (mk-phant-term.mixins.aux t Params c CN PF) PF2,
        phant-fun-unify NoMsg s {mk-app SKPT [c]} PF2 (PFU t s c)])
   ]),
-  Out = {phant-fun-struct T `s` SIParams s\
+  Out = {phant-fun-struct T `s` SI Params s\
           {phant-fun-implicit `c` ClassTy (PFU T s)}}
 ].
 
 mk-phant-term.mixins.aux T Params C CN PF X :- std.do![
-  get-constructor {coq.env.global CN} KC,
+  get-constructor CN KC,
   mgref->term Params T KC KCM,
   phant-fun-unify {{lib:hb.nomsg}} KCM C PF X,
 ].
@@ -1100,24 +1106,24 @@ params->holes (w-params.cons _ _ F) [_|PS] :- pi x\ params->holes (F x) PS.
 pred declare-instances i:term, i:list class.
 declare-instances T [class Class Struct MLwP|Rest] :-
   params->holes MLwP Params,
-  get-constructor {coq.env.global Class} KC,
+  get-constructor Class KC,
 
   if (not(local-cs? T Struct))
      true % we build it
      (if-verbose (coq.say "HB: skipping alreay existing"
-                    {coq.term->string Struct} "instance on"
+                    {nice-gref->string Struct} "instance on"
                     {coq.term->string T}),
       fail),
 
   if (mgref->term Params T KC KCApp)
-     (if-verbose (coq.say "HB: we can build a" {coq.term->string Struct} "on"
+     (if-verbose (coq.say "HB: we can build a" {nice-gref->string Struct} "on"
         {coq.term->string T}))
      fail,
 
   !,
   term->gref T TGR,
   coq.gref->id TGR TID,
-  Name is TID ^ "_is_a_" ^ {term->modname Struct},
+  Name is TID ^ "_is_a_" ^ {gref->modname Struct},
 
   if-verbose (coq.say "HB: declare canonical structure instance" Name),
 
@@ -1261,10 +1267,10 @@ clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
 
   clean-op-ty Ops S T1 T2.
 
-pred operation-body-and-ty i:list prop, i:constant, i:term, i:term, i:term,
+pred operation-body-and-ty i:list prop, i:constant, i:structure, i:term, i:term,
   i:list term, i:term, i:w-args A, o:pair term term.
 operation-body-and-ty EXI Poperation Struct Psort Pclass Params _T (triple _ Params _) (pr Bo Ty) :- std.do! [
-  mk-app Struct Params StructType,
+  mk-app {coq.env.global Struct} Params StructType,
   mk-app Psort Params PsortP,
   mk-app Pclass Params PclassP,
   Bo = fun `s` StructType Body,
@@ -1285,7 +1291,7 @@ operation-body-and-ty EXI Poperation Struct Psort Pclass Params _T (triple _ Par
 % same operation out of the package structure (out of the class field of the
 % structure). We also provide all the other mixin dependencies (other misins)
 % of the package structure.
-pred export-1-operation i:mixinname, i:term, i:term, i:term, i:one-w-params mixinname, i:option constant, i:list prop, o:list prop.
+pred export-1-operation i:mixinname, i:structure, i:term, i:term, i:one-w-params mixinname, i:option constant, i:list prop, o:list prop.
 export-1-operation _ _ _ _ _ none EX EX :- !. % not a projection, no operation
 export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std.do! [
   coq.gref->id (const Poperation) Name,
@@ -1304,7 +1310,7 @@ export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std
 ].
 
 % Given a list of mixins, it exports all operations in there
-pred export-operations.aux i:term, i:term, i:term, i:one-w-params mixinname, i:list prop, o:list prop.
+pred export-operations.aux i:structure, i:term, i:term, i:one-w-params mixinname, i:list prop, o:list prop.
 export-operations.aux Struct ProjSort ProjClass MwP EX1 EX2 :- !, std.do! [
   w-params_1 MwP (indt M),
   coq.CS.canonical-projections M Poperations,
@@ -1315,7 +1321,7 @@ pred mixin-not-already-declared i:one-w-params mixinname.
 mixin-not-already-declared MwP :-
   w-params_1 MwP M, not(mixin-first-class M _), M = indt _.
 
-pred export-operations i:term, i:term, i:term, i:list-w-params mixinname, i:list prop, o:list prop, o:list mixinname.
+pred export-operations i:structure, i:term, i:term, i:list-w-params mixinname, i:list prop, o:list prop, o:list mixinname.
 export-operations Structure ProjSort ProjClass MLwP EX1 EX2 MLToExport :- std.do! [
   distribute-w-params MLwP LMwP,
   std.filter LMwP mixin-not-already-declared LMwPToExport,
@@ -1337,7 +1343,7 @@ mk-coe-class-body FC TC TMLwP Params T _ CoeBody :- std.do! [
   std.map TML (from FC) Builders,
   std.map Builders (x\r\sigma t\ coq.env.global x t, mk-app t Params r) BuildersP,
 
-  mk-app {coq.env.global {get-constructor {coq.env.global TC}}}
+  mk-app {coq.env.global {get-constructor TC}}
     {coq.mk-n-holes {factory-nparams TC}} KCHoles,
 
   (pi c\ sigma Mixes\
@@ -1360,10 +1366,10 @@ pred mk-coe-structure-body
 mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProjection
     Params _T _ SCoeBody :- std.do! [
 
-  mk-app StructureF      Params StructureP,
-  mk-app SortProjection  Params SortP,
-  mk-app ClassProjection Params ClassP,
-  mk-app Coercion        Params CoercionP,
+  mk-app {coq.env.global StructureF} Params StructureP,
+  mk-app             SortProjection  Params SortP,
+  mk-app             ClassProjection Params ClassP,
+  mk-app             Coercion        Params CoercionP,
 
   mk-app {coq.env.global {get-constructor StructureT}}
     {coq.mk-n-holes {factory-nparams TC}} PackPH,
@@ -1377,12 +1383,12 @@ mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProj
 % from C1 to C2 given P1 P2 the two projections from the structure of C1
 pred declare-coercion i:term, i:term, i:class, i:class.
 declare-coercion SortProjection ClassProjection
-    (class FC StructureF FMLwP as FCDef) (class TC StructureT TMLwP as TCDef) :- std.do! [
+    (class FC StructureF FMLwP) (class TC StructureT TMLwP) :- std.do! [
 
-  acc current (clause _ _ (sub-class FCDef TCDef)),
+  acc current (clause _ _ (sub-class FC TC)),
 
-  term->modname StructureF ModNameF,
-  term->modname StructureT ModNameT,
+  gref->modname StructureF ModNameF,
+  gref->modname StructureT ModNameT,
   CName is ModNameF ^ "_class_to_" ^ ModNameT ^ "_class",
   SName is ModNameF ^ "_to_" ^ ModNameT,
 
@@ -1408,15 +1414,15 @@ declare-coercion SortProjection ClassProjection
   if-verbose (coq.say "HB: declare unification hint" SName),
 
   hb-add-const SName SCoeBody STy @transparent! SC,
-  @global! => coq.coercion.declare (coercion (const SC) 0 {term->gref StructureF} (grefclass {term->gref StructureT})),
+  @global! => coq.coercion.declare (coercion (const SC) 0 StructureF (grefclass StructureT)),
   coq.CS.declare-instance (const SC), % TODO: API in Elpi, take a @constant instead of gref
 ].
 
-pred join-body i:int, i:int, i:term, i:term, i:term, i:term, i:term, i:term,
+pred join-body i:int, i:int, i:structure, i:term, i:term, i:term, i:term, i:term,
   i:list term, i:name, i:term, i:(term -> A), o:term.
 join-body N1 N2 S3 S2_Pack S1_sort S3_to_S1 S2_class S3_to_S2
   P N _Ty _F (fun N S3P Pack) :- !,
-  mk-app S3 P S3P, !,
+  mk-app {coq.env.global S3} P S3P, !,
   coq.mk-n-holes N2 Holes2, !,
   coq.mk-n-holes N1 Holes1, !,
   @pi-decl N S3P s\
@@ -1430,8 +1436,8 @@ join-body N1 N2 S3 S2_Pack S1_sort S3_to_S1 S2_class S3_to_S2
 
 pred declare-join i:class, i:pair class class, o:prop.
 declare-join (class C3 S3 MLwP3) (pr (class C1 S1 _) (class C2 S2 _)) (join C1 C2 C3) :-
-  Name is "join_" ^ {term->modname S3} ^
-    "_between_" ^ {term->modname S1} ^ "_and_" ^ {term->modname S2},
+  Name is "join_" ^ {gref->modname S3} ^
+    "_between_" ^ {gref->modname S1} ^ "_and_" ^ {gref->modname S2},
 
   get-structure-coercion S3 S2 S3_to_S2,
   get-structure-coercion S3 S1 S3_to_S1,
@@ -1493,8 +1499,8 @@ mk-class-field ClassName Params T _ (field _ "class" (app [C|Args]) _\end-record
 
 % Builds the axioms record and the factories from this class to each mixin
 % TODO params
-pred declare-class+structure i:list-w-params mixinname, o:factoryname, o:term, o:term, o:term, o:list prop.
-declare-class+structure MLwP (indt ClassInd) Structure SortProjection ClassProjection AllFactories :- std.do! [
+pred declare-class+structure i:list-w-params mixinname, o:factoryname, o:structure, o:term, o:term, o:list prop.
+declare-class+structure MLwP (indt ClassInd) (indt StructureInd) SortProjection ClassProjection AllFactories :- std.do! [
 
   if-verbose (coq.say "HB: declare axioms record"),
 
@@ -1517,17 +1523,16 @@ declare-class+structure MLwP (indt ClassInd) Structure SortProjection ClassProje
     (mk-class-field (indt ClassInd)) StructureDeclaration,
 
   std.assert-ok! (coq.typecheck-indt-decl StructureDeclaration) "declare-structure: illtyped",
-  coq.env.add-indt StructureDeclaration StructureName,
+  hb-add-indt StructureDeclaration StructureInd,
 
-  coq.CS.canonical-projections StructureName [some SortP, some ClassP],
-  coq.env.global (indt StructureName) Structure,
+  coq.CS.canonical-projections StructureInd [some SortP, some ClassP],
   coq.env.global (const SortP) SortProjection,
   coq.env.global (const ClassP) ClassProjection,
 ].
 
 % Declares "sort" as a coercion Structurename >-> Sortclass
-pred declare-sort-coercion i:term, i:term.
-declare-sort-coercion (global StructureName _) (global Proj _) :-
+pred declare-sort-coercion i:structure, i:term.
+declare-sort-coercion StructureName (global Proj _) :-
 
   if-verbose (coq.say "HB: declare sort coercion"),
 
@@ -1538,15 +1543,14 @@ if-class-already-exists-error _ [] _.
 if-class-already-exists-error N [class _ S ML1wP|CS] ML2 :-
   list-w-params_list ML1wP ML1,
   if (list-eq-set ML1 ML2)
-     (coq.error "Structure" {coq.term->string S} "contains the same mixins of" N)
+     (coq.error "Structure" {nice-gref->string S} "contains the same mixins of" N)
      (if-class-already-exists-error N CS ML2).
 
 pred export-mixin-coercion i:classname, i:option constant.
 export-mixin-coercion _ none.
 export-mixin-coercion ClassName (some C) :-
   coq.env.typeof (const C) _ CTy,
-  safe-dest-app {safe-head CTy} Mixin _,
-  coq.term->gref Mixin MixinGR,
+  head-gref-under-prods CTy MixinGR,
   if-verbose (coq.say "HB: export class to mixin coercion for mixin" {nice-gref->string MixinGR}),
   @global! =>
     coq.coercion.declare (coercion (const C) _ ClassName (grefclass MixinGR)).
diff --git a/structures.v b/structures.v
index 76b797a9..1fc23a0e 100644
--- a/structures.v
+++ b/structures.v
@@ -43,7 +43,7 @@ Elpi Db hb.db lp:{{
 typeabbrev mixinname gref.
 typeabbrev classname gref.
 typeabbrev factoryname gref.
-typeabbrev structure term.
+typeabbrev structure gref.
 
 kind triple type -> type -> type -> type.
 type triple A -> B -> C -> triple A B C.
@@ -95,7 +95,7 @@ pred factory-nparams o:factoryname, o:int.
 pred class-def o:class.
 
 % is-structure
-pred is-structure o:term.
+pred is-structure o:gref.
 
 % [phant-abbrev Cst AbbrevCst Abbrev]
 % Stores phantom abbreviation Abbrev associated with Cst
@@ -109,7 +109,7 @@ pred phant-abbrev o:gref, o:gref, o:abbreviation.
 pred factory-builder-nparams o:constant, o:int.
 
 % [sub-class C1 C2] C1 is a sub-class of C2.
-pred sub-class o:class, o:class.
+pred sub-class o:classname, o:classname.
 
 %%%%%% Memory of exported mixins %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Operations (named mixin fields) need to be exported exactly once,
@@ -182,7 +182,7 @@ pp-list-w-params.triple (triple M Params T) :-
 
 pred pp-class i:prop.
 pp-class (class-def (class _ S MLwP)) :-
-  pp-list-w-params MLwP S.
+  pp-list-w-params MLwP {coq.env.global S}.
 
 pred pp-mixin-src i:prop.
 pp-mixin-src (mixin-src T M C) :-

From 54c90235527aece0e7bc77dafb1d23341d65e443 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 5 Nov 2020 17:04:24 +0100
Subject: [PATCH 3/4] ready to trun univpoly on

---
 hb.elpi | 82 ++++++++++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 72 insertions(+), 10 deletions(-)

diff --git a/hb.elpi b/hb.elpi
index 96a11e66..119d14e4 100644
--- a/hb.elpi
+++ b/hb.elpi
@@ -342,6 +342,41 @@ distribute-w-params (w-params.cons N T F) L :-
 distribute-w-params (w-params.nil N T F) L :-
   pi x\ std.map (F x) (bind-nil N T x) L.
 
+pred list-w-params.fold i:list-w-params A, i:B, o:B.
+list-w-params.fold (w-params.cons N T F) S0 S2 :-
+  fold T S0 S1,
+  @pi-decl N T x\ list-w-params.fold (F x) S1 S2.
+list-w-params.fold (w-params.nil N T F) S0 S2 :-
+  fold T S0 S1,
+  @pi-decl N T x\ std.fold (F x) S1 w-args.fold S2.
+
+pred w-args.fold i:w-args A, i:B, o:B.
+w-args.fold (triple _ L T) S0 S2 :-
+  std.fold L S0 fold S1,
+  fold T S1 S2.
+
+pred univs-of-list-w-params i:list-w-params A, o:coq.univ.set.
+univs-of-list-w-params W S :-
+  (pi u s0 s1\ fold (sort (typ u)) s0 s1 :- !, coq.univ.set.add u s0 s1) =>
+  list-w-params.fold W {coq.univ.set.empty} S.
+
+pred list-w-params.copy i:list-w-params A, o:list-w-params A.
+list-w-params.copy (w-params.cons N T F) (w-params.cons N T1 F1) :-
+  copy T T1,
+  @pi-decl N T x\ list-w-params.copy (F x) (F1 x).
+list-w-params.copy (w-params.nil N T F) (w-params.nil N T1 F1) :-
+  copy T T1,
+  @pi-decl N T x\ std.map (F x) w-args.copy (F1 x).
+
+pred w-args.copy i:w-args A, o:w-args A.
+w-args.copy (triple A L T) (triple A L1 T1) :-
+  std.map L copy L1, copy T T1.
+
+pred list-w-params.bind-univs i:list-w-params A, o:univ-closed (list-w-params A).
+list-w-params.bind-univs W R :-
+  univs-of-list-w-params W S,
+  coq.bind-universes {coq.univ.set.elements S} list-w-params.copy W R.
+
 % Specific to one-w-params
 pred w-params_1 i:one-w-params A, o:A.
 w-params_1 X Y :- w-params.then X ignore ignore (p\ t\ triple_1) Y.
@@ -349,10 +384,15 @@ w-params_1 X Y :- w-params.then X ignore ignore (p\ t\ triple_1) Y.
 % no implicit arguments
 pred hb-add-const i:id, i:term, i:term, i:opaque?, o:constant.
 hb-add-const Name Bo Ty Opaque C :- std.do! [
-  coq.env.add-const Name Bo Ty Opaque C,
+    coq.env.add-const Name Bo Ty Opaque C,
   coq.arguments.set-implicit (const C) [[]]
 ].
 
+pred hb-add-indt i:indt-decl, o:inductive.
+hb-add-indt D I :- std.do! [
+    coq.env.add-indt D I
+].
+
 %%%%%%%%% HB database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %Specialize coq.elpi.accumulate to "hiearchy.db"
@@ -1149,6 +1189,27 @@ declare-factory-abbrev Name (factory-by-phantabbrev Abbr) :-
   coq.notation.abbreviation-body Abbr Nargs AbbrTrm,
   @global! => coq.notation.add-abbreviation Name Nargs AbbrTrm tt _.
 
+% [mk-clause-with-univs Data Hyps MkHead Clause]
+%   Clause = pi u1 .. un\ Head :- coq.univ.new "" u1, ..., coq.univ.new "" un
+% where mkHead D Head
+% and Data = univ-binder u1\ ... univ-data D
+pred mk-clause-with-univs i:univ-closed A, i:list prop, i:(A -> prop -> prop), o:prop.
+mk-clause-with-univs (univ-binder F) Todo MkClauseHd (pi u\ Clause u) :-
+  pi u\ mk-clause-with-univs (F u) [coq.univ.new "" u|Todo] MkClauseHd (Clause u).
+mk-clause-with-univs (univ-data D) TodoRev MkClauseHd (Head :- Todo) :-
+  std.rev TodoRev Todo,
+  MkClauseHd D Head.
+
+pred mk-factory-requires-clause i:gref, i:list-w-params mixinname, o:prop.
+mk-factory-requires-clause GR MLwP Clause :-
+  list-w-params.bind-univs MLwP MLwPuc,
+  mk-clause-with-univs MLwPuc [] (x\r\ r = factory-requires GR x) Clause.
+
+pred mk-class-def-clause i:class, o:prop.
+mk-class-def-clause (class C S MLwP) Clause :-
+  list-w-params.bind-univs MLwP MLwPuc,
+  mk-clause-with-univs MLwPuc [] (x\r\ r = class-def (class C S x)) Clause.
+
 % [mk-factory-requires-clause-and-abbrev Str GR FL CL FactAbbrev]
 % computes the list of mixins ML provided by FL,
 % creates a clause in CL stating that GR requires ML (factory-requires ..), and
@@ -1157,7 +1218,7 @@ declare-factory-abbrev Name (factory-by-phantabbrev Abbr) :-
 pred mk-factory-requires-clause-and-abbrev i:string, i:gref, i:list-w-params factoryname, o:list prop, o:factory-abbrev.
 mk-factory-requires-clause-and-abbrev Str GR GRFS [FactoryRequires|Aliases] FactAbbrev :- !, std.do! [
   factories-provide GRFS ML,
-  FactoryRequires = factory-requires GR ML,
+  mk-factory-requires-clause GR ML FactoryRequires,
   if (factory-alias->gref GR _)
      (Aliases = [],
       FactAbbrev = factory-by-classname GR)
@@ -1508,7 +1569,7 @@ declare-class+structure MLwP (indt ClassInd) (indt StructureInd) SortProjection
     synthesize-fields.body ClassDeclaration,
 
   std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped",
-  coq.env.add-indt ClassDeclaration ClassInd,
+  hb-add-indt ClassDeclaration ClassInd,
   coq.CS.canonical-projections ClassInd Projs,
   % TODO: put this code in a named clause
   w-params.nparams MLwP NParams,
@@ -1593,11 +1654,11 @@ mc-compat-structure ModuleName _ NewMixins CNParams ClassName ClassProjection Ax
   coq.env.export-module MCCompat,
 ].
 
-pred clone-phant-body i:factoryname, i:term, i:term, i:list term, i:term, i:list (w-args mixinname), o:phant-term.
-clone-phant-body ClassName SortProjection (global (indt I) UI as Structure) PL T _ PhF :- std.do! [
+pred clone-phant-body i:factoryname, i:term, i:structure, i:list term, i:term, i:list (w-args mixinname), o:phant-term.
+clone-phant-body ClassName SortProjection (indt I) PL T _ PhF :- std.do! [
   std.assert! (coq.env.indt I UI _ _ _ _ [PackC] _) "wtf",
   mk-app (global (indc PackC) UI) {std.append PL [T]} PackPLT,
-  mk-app Structure PL SPL,
+  mk-app (global (indt I) UI) PL SPL,
   (@pi-decl `cT` SPL cT\
   mk-app {coq.env.global ClassName} {std.append PL [T]} CPL,
   @pi-decl `c` CPL c\
@@ -1620,7 +1681,7 @@ pack-body.mixins PL T BuildC PackS Body :- !, std.do! [
 pred pack-body i:classname, i:list term, i:term, i:list (w-args mixinname), o:term.
 pack-body ClassName PL T MLwA F :- std.do! [
   class-def (class ClassName S _),
-  get-constructor {coq.env.global ClassName} BuildC,
+  get-constructor ClassName BuildC,
   get-constructor S PackS,
   under-mixins.then MLwA mk-fun (pack-body.mixins PL T BuildC PackS) F
 ].
@@ -1656,7 +1717,7 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [
     ClassName Structure SortProjection ClassProjection Factories,
 
   w-params.map MLwP (_\_\_\ mk-nil) NilwP,
-  ClassRequires = factory-requires (ClassName) NilwP,
+  mk-factory-requires-clause (ClassName) NilwP ClassRequires,
   ClassAlias = (factory-alias->gref ClassName ClassName),
   CurrentClass = (class ClassName Structure MLwP),
 
@@ -1692,10 +1753,11 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [
 
   if-verbose (coq.say "HB: accumulating various props"),
   std.map MLToExport (m\r\ r = mixin-first-class m ClassName) MixinFirstClass,
+  mk-class-def-clause CurrentClass ClassDef,
   std.flatten [
       MixinFirstClass, EX, Factories,
       [ClassRequires], [ClassAlias], [is-structure Structure],
-      NewJoins, [class-def CurrentClass]
+      NewJoins, [ClassDef]
     ]
     NewClauses,
   std.forall NewClauses (c\ acc current (clause _ _ c)),
@@ -2086,7 +2148,7 @@ declare-mixin-or-factory Sort1 Fields0 GRFSwP Module TheType D TheParams :- std.
   Kname = "Axioms_",
   RDeclSkel = record "axioms_" Sort1 Kname Fields1,
   std.assert-ok! (coq.elaborate-indt-decl-skeleton RDeclSkel RDecl) "record declaration illtyped",
-  coq.env.add-indt RDecl R,
+  hb-add-indt RDecl R,
   coq.env.end-section,
   coq.env.indt R _ tt _ _ _ [K] _,
   GRK = indc K,

From a05c116b71379a136f91ef059c914cf5c0d43fb1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 5 Nov 2020 17:04:55 +0100
Subject: [PATCH 4/4] [DO NOT MERGE] turn univpoly on, it kind of works

---
 hb.elpi | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/hb.elpi b/hb.elpi
index 119d14e4..241bcacd 100644
--- a/hb.elpi
+++ b/hb.elpi
@@ -384,12 +384,14 @@ w-params_1 X Y :- w-params.then X ignore ignore (p\ t\ triple_1) Y.
 % no implicit arguments
 pred hb-add-const i:id, i:term, i:term, i:opaque?, o:constant.
 hb-add-const Name Bo Ty Opaque C :- std.do! [
+  @univpoly! =>
     coq.env.add-const Name Bo Ty Opaque C,
   coq.arguments.set-implicit (const C) [[]]
 ].
 
 pred hb-add-indt i:indt-decl, o:inductive.
 hb-add-indt D I :- std.do! [
+  @univpoly! =>
     coq.env.add-indt D I
 ].
 
@@ -1360,6 +1362,7 @@ export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std
   w-params.then MwP mk-fun-prod ignore (operation-body-and-ty EXI Poperation Struct Psort Pclass) (pr Body BodyTy),
 
   if-verbose (coq.say "HB: export operation" Name),
+  std.assert-ok! (coq.typecheck Body BodyTy) "export-1-operation: illtyped operation",
   hb-add-const Name Body BodyTy @transparent! C,
 
   w-params.nparams MwP NP,