Introducing FactoryName.sort

.gitignore

@@ -46,6 +46,7 @@ _minted-*
 *.aux
 *.log
 *.out
+!*.v.out
 *.synctex.gz
 *.toc
 *.vrb

.nix/config.nix

@@ -3,7 +3,7 @@
   attribute = "hierarchy-builder";
   default-bundle = "coq-8.13";
   bundles = let common = {
-      mathcomp.override.version = "hierarchy-builder";
+      mathcomp.override.version = "hierarchy-builder-local-pack-better";
       mathcomp.job = false;
       mathcomp-single.job = true;
   }; in {

.vscode/settings.json

@@ -41,7 +41,7 @@
         "**/_minted-*": true,
         "**/*.aux": true,
         "**/*.log": true,
-        "**/*.out": true,
+//      "**/*.out": true, // .v.out is used for expected test output
         "**/*.synctex.gz": true,
         "**/*.toc": true,
         "**/*.vrb": true,
@@ -89,7 +89,7 @@
         "**/_minted-*": true,
         "**/*.aux": true,
         "**/*.log": true,
-        "**/*.out": true,
+//      "**/*.out": true, // .v.out is used for expected test output
         "**/*.synctex.gz": true,
         "**/*.toc": true,
         "**/*.vrb": true,

HB/about.elpi

@@ -159,7 +159,7 @@ main-operation S MixinSource _ :-
   coq.say {coq.pp->string PpOriginMixin},
   coq.say.
 
-pred main-structure i:string, i:classname, i:structure, i:list-w-params mixinname.
+pred main-structure i:string, i:classname, i:structure, i:mixins.
 main-structure S Class Structure MLwP :-
   % fetch
   list-w-params_list MLwP ML,

HB/builders.elpi

@@ -9,20 +9,21 @@ begin CtxSkel :- std.do! [
   if-verbose (coq.say "HB: begin module for builders"),
   log.coq.env.begin-module Name none,
 
-  std.assert-ok! (builders.private.elaborate-context-skel->factory CtxSkel Ctx GRF) "Context illtyped",
+  builders.private.factory CtxSkel IDF GRF,
 
   % the Super module to access operations/axioms shadowed by the ones in the factory
   if (GRF = indt FRecord) (std.do! [
     if-verbose (coq.say "HB: begin module Super"),
     log.coq.env.begin-module "Super" none,
-    std.forall {coq.CS.canonical-projections FRecord} builders.private.declare-shadowed-constant,
+    std.forall {coq.CS.canonical-projections FRecord}
+      builders.private.declare-shadowed-constant,
     log.coq.env.end-module-name "Super" _,
     if-verbose (coq.say "HB: ended module Super")
   ]) (true),
 
   log.coq.env.begin-section Name,
   if-verbose (coq.say "HB: postulating factories"),
-  builders.private.postulate-factories Name Ctx,
+  builders.private.postulate-factories Name IDF CtxSkel,
 ].
 
 }
@@ -50,18 +51,26 @@ builders.end :- std.do! [
   gref->modname GR 1 "" M,
   Name is M ^ "_Exports",
   log.coq.env.begin-module Name none,
+
   std.forall Clauses (c\ log.coq.env.accumulate current "hb.db" (clause _ _ c)),
   std.forall ExportClausesFiltered (c\ log.coq.env.accumulate current "hb.db" (clause _ _ c)),
 
+  Clauses => ExportClausesFiltered => current-mode no-builder =>
+    instance.declare-factory-sort-factory GR,
+
   log.coq.env.end-module-name Name Exports,
   log.coq.env.end-module-name ModName _,
   export.module {calc (ModName ^ "." ^ Name)} Exports,
+
+
 ].
 
 /* ------------------------------------------------------------------------- */
 /* ----------------------------- private code ------------------------------ */
 /* ------------------------------------------------------------------------- */
 
+pred factory.cdecl->w-mixins i:context-decl, o:w-mixins context-decl.
+
 namespace builders.private {
 
 % [declare-1-builder (builder _ F M B) From MoreFrom] Given B of type FB, it
@@ -90,28 +99,6 @@ declare-shadowed-located Id (loc-abbreviation Abbrev) :-
   coq.notation.abbreviation-body Abbrev NArgs T,
   @global! => log.coq.notation.add-abbreviation Id NArgs T ff _.
 
-% Elaborating factory (F Params T) is hard, since we don't have (yet) all the structures
-% on T that makes the phat abbreviation (F Params T), which unfolds to (F_phant Params T _ idfun...)
-% actually typecheck. So we purge all idfun disabling the inference of canonical mixins
-% over T the factory depends on
-pred elaborate-context-skel->factory i:context-decl, o:context-decl, o:factoryname, o:diagnostic.
-elaborate-context-skel->factory
-  (context-item IDT IT TTySkel none t\ context-item IDF IF (TFSkel t) none _\ context-end)
-  (context-item IDT IT TTy none t\ context-item IDF IF (TFSkel t) none _\ context-end) GRF Diag
-:- !, std.do-ok! Diag [
-  coq.elaborate-ty-skeleton TTySkel _ TTy,
-  (d\ coq.id->name IDT NameT),
-  (d\ @pi-decl NameT TTy t\ purge-id (TFSkel t) (TFSkel1 t), coq.elaborate-ty-skeleton (TFSkel1 t) _ (TF1 t) d),
-  (d\ @pi-decl NameT TTy t\ std.assert! (factory? (TF1 t) (triple GRF _Params t)) "the last argument must be a factory applied to the type variable"),
-].
-elaborate-context-skel->factory (context-item ID I TSkel none C) (context-item ID I T none C1) GRF Diag :- !, std.do-ok! Diag [
-  coq.elaborate-ty-skeleton TSkel _ T,
-  (d\ coq.id->name ID Name),
-  (d\ @pi-decl Name T x\ elaborate-context-skel->factory (C x) (C1 x) GRF d),
-].
-elaborate-context-skel->factory (context-item ID _ _ (some _) _) _ _ _ :-
-  coq.error "context item cannot be given a body:" ID.
-
 pred postulate-factory-abbrev i:term, i:list term, i:id, i:factoryname, o:term.
 postulate-factory-abbrev TheType Params Name Falias TheFactory :- std.do! [
   factory-alias->gref Falias F,
@@ -143,40 +130,24 @@ define-factory-operation TheType Params TheFactory NHoles (some P) :-
   coq.gref->id (const P) Name,
   @local! => log.coq.notation.add-abbreviation Name 0 T ff _.
 
-pred fresh-type o:term.
-fresh-type Ty :-
-  Ty = {{Type}},
-  std.assert-ok! (coq.typecheck-ty Ty _) "impossible".
-
-pred postulate-factories i:id, i:context-decl.
-postulate-factories ModName (context-item IDT _ TySkel none t\ context-item IDF _ (TF t) none _\ context-end) :- !, std.do! [
-  % TODO we should allow T to be anything.
-  std.assert-ok! (coq.elaborate-ty-skeleton TySkel _ Ty) "builders-postulate-factory: illtyped context",
-  if (var Ty) (fresh-type Ty) true,
-  if-verbose (coq.say "HB: postulating type" IDT),
-  log.coq.env.add-section-variable-noimplicits IDT Ty C,
-  TheType = global (const C),
-
-  std.assert! (factory? (TF TheType) (triple GRF Params TheType))
-    "the last argument must be a factory applied to the type variable",
-  gref-deps GRF GRFMLwP, % TODO: remove, pass to context.declare the list-w-params-eta-expansion of GRF
-  context.declare TheType Params GRFMLwP _ _,
-  postulate-factory-abbrev TheType Params IDF GRF TheFactory,
-  define-factory-operations TheType Params TheFactory GRF,
+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) _.
+factory (context-item _ _ _ _ R) IDF GR :- !, pi x\ factory (R x) IDF GR.
+factory _ _ _ :- !, coq.error "the last context item is not a factory".
+
+pred postulate-factories i:id, i:string, i:context-decl.
+postulate-factories ModName IDF CDecl :- std.do! [
+  factory.cdecl->w-mixins CDecl (pr FLwP _),
+  context.declare.params-key FLwP _ _ FLwA,
+  std.assert! (FLwA = [triple GRF FParams FKey])
+    "HB: cannot declare builders for more than one factory at a time",
+  gref-deps GRF DepswP,
+  context.declare.mixins FKey FParams DepswP _ _,
+  postulate-factory-abbrev FKey FParams IDF GRF TheFactory,
+  define-factory-operations FKey FParams TheFactory GRF,
   log.coq.env.accumulate current "hb.db" (clause _ _
-    (current-mode (builder-from TheType TheFactory GRF ModName))),
-].
-
-postulate-factories ModName (context-item ID _ TSkel none Factories) :- std.do! [
-  if-verbose (coq.say "HB: postulating" ID),
-  std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "postulate-factories: illtyped context",
-  if (var T) (coq.fresh-type T) true,
-  log.coq.env.add-section-variable-noimplicits ID T P,
-  TheParam = global (const P),
-  postulate-factories ModName (Factories TheParam),
+    (current-mode (builder-from FKey TheFactory GRF ModName))),
 ].
 
-postulate-factories _ (context-item ID _ _ (some _) _) :-
-  coq.error "context item cannot be given a body:" ID.
-
-}
+}

HB/common/database.elpi

@@ -32,7 +32,7 @@ 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 classname->mixins i:classname, o:list-w-params mixinname.
+pred classname->mixins i:classname, o:mixins.
 classname->mixins CN MLwP :- class-def (class CN _ MLwP).
 
 pred module-to-export_module i:prop, o:modpath.
@@ -73,13 +73,19 @@ sub-class? (class C1 _ ML1P) (class C2 _ ML2P) :-
   std.forall ML2 (m2\ std.exists ML1 (m1\ m1 = m2)).
 
 % [factory-provides F MLwP] computes the mixins MLwP generated by F
-pred factory-provides i:factoryname, o:list-w-params mixinname.
+pred factory-provides i:factoryname, o:mixins.
 factory-provides FactoryAlias MLwP :- std.do! [
   factory-alias->gref FactoryAlias Factory,
   gref-deps Factory RMLwP,
   w-params.map RMLwP (factory-provides.base Factory) MLwP
 ].
 
+pred mixin->factories i:mixinname, o:list factoryname.
+mixin->factories M FL :- std.do! [
+  std.findall (from F_ M B_) AllF,
+  std.map AllF from_factory FL
+].
+
 pred factory-provides.base i:factoryname, i:list term, i: term,
   i:list (w-args mixinname), o:list (w-args mixinname).
 factory-provides.base Factory Params T _RMLwP MLwP :- std.do! [
@@ -111,7 +117,7 @@ extract-conclusion-params T R :- whd1 T T1, !, extract-conclusion-params T1 R.
 %  cons tp p\ nil t\ [pr f1 [p,t]]
 %    f1 p t = m1 t, m2 p t
 %  cons tp p\ nil t\ [pr m1 [t], pr m2 [p,t]]
-pred factories-provide i:list-w-params factoryname, o:list-w-params mixinname.
+pred factories-provide i:list-w-params factoryname, o:mixins.
 factories-provide FLwP MLwP :- std.do! [
   list-w-params.flatten-map FLwP factory-provides UnsortedMLwP,
   w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP,
@@ -296,6 +302,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, !,
   std.split-at NP Args Params [T|_].
 

HB/common/phant-abbreviation.elpi

@@ -28,26 +28,32 @@ add-abbreviation N (private.phant-term AL T1) C Abbrev :- std.do! [
   @global! => log.coq.notation.add-abbreviation N NParams AbbrevT tt Abbrev,
 ].
 
-% [of-gref GR RealMixinArgs PT] builds a phant-term taking all parameters,
+% [of-gref WithCopy GR RealMixinArgs PT]
+% builds a phant-term taking all parameters,
 % the type, then inferring automatically all structures covering the mixins
 % GR depends on. RealMixinArgs is a list of mixins one wants to explicitly
 % pass (instead of being inferred)
-pred of-gref i:gref, i:list mixinname, o:phant-term.
-of-gref GRF RealMixinArgs PhBody:- !, std.do! [
+% If WithCopy = tt, an extra argument is added after all the parameters
+% and before the source keu to replace the target key by a user chosen one.
+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,
   % toposort-mixins ML MLSorted,
   MLwP = MLwPSorted, % Assumes we give them already sorted in dep order.
   std.rev {list-w-params_list MLwPSorted} MLSortedRev,
-
-  std.map RealMixinArgs (m\r\ r = private.this-mixin-is-real-arg m) RMClauses,
-  std.filter MLSortedRev (m\not(std.mem! RealMixinArgs m)) MLSortedRevFiltered,
+  std.map RealMixinArgs (m\ r\ r = private.this-mixin-is-real-arg m) RMClauses,
+  std.filter MLSortedRev (m\ not(std.mem! RealMixinArgs m)) MLSortedRevFiltered,
   find-max-classes MLSortedRevFiltered CNL,
   assert-good-coverage! MLSortedRevFiltered CNL,
 
-  RMClauses => w-params.then MLwP fun-real fun-real
-    (private.mk-phant-term.classes EtaF CNL) PhBody,
+  RMClauses => if (WithCopy = ff)
+    (w-params.then MLwP fun-real fun-real
+      (ps\ t\ ml\ o\ private.mk-phant-term.classes EtaF CNL ps t t ml o) PhBody)
+    (w-params.fold MLwP fun-real
+      (private.mk-phant-term-with-copy EtaF CNL) PhBody
+  )
 ].
 
 % API à la carte: start with a term and wrap it up -------------------------
@@ -71,10 +77,10 @@ fun-unify OMsg X1 X2 (private.phant-term AL F) (private.phant-term [private.unif
 
 % [fun-implicit N T Ph Ph1] Adds an implicit argument name N of type T areound Ph
 pred fun-implicit i:name, i:term, i:(term -> phant-term), o:phant-term.
-fun-implicit N Ty (t\private.phant-term AL (F t))
+fun-implicit N Ty (t\ private.phant-term AL (F t))
                   (private.phant-term [private.implicit|AL] (fun N Ty F)).
 
-% [fun-infer-type N T Ph Ph1] Adds an argument N of type T such that one passes 
+% [fun-infer-type N T Ph Ph1] Adds an argument N of type T such that one passes
 % a value V of type {{ Type }} the corresponding canonical VC of type T is passed
 % for N , eg `fun T (phT : phant T) => Ph`
 pred fun-infer-type i:class, i:name, i:term, i:(term -> phant-term), o:phant-term.
@@ -198,34 +204,40 @@ build-abbreviation K F [unify|AL] K' FAbbrev :- !,
 %         unify, ..., unify]
 %   {{fun p_1 ... p_k T m_0 .. m_n =>
 %       fun q_1 .. q_l =>
-%         [find s_0 | T ~ s_0]
-%         [find c_0 | s_0 ~ SK q_1 .. q_l T c_0]
+%         [find t   | T ~ t]
+%         [find s_0 | t ~ s_0]
+%         [find c_0 | s_0 ~ SK q_1 .. q_l t c_0]
 %         [find m'_{i_0_0}, .., m'_{i_0_n0} | c_0 ~ CK m'_{i_0_0} .. m'_{i_0_n0}]
 %         fun of hb.unify m_{i_0_0} m'_{i_0_0} & ... & hb.unify m_{i_0_n0} m'_{i_0_n0} =>
 %       ...
 %       fun q'_1 .. q'_l' =>
-%         [find s_k | T ~ s_k]
-%         [find c_k | s_k ~ SK q'_1 .. q'_l' T c_k]
+%         [find t   | T ~ t]
+%         [find s_k | t ~ s_k]
+%         [find c_k | s_k ~ SK q'_1 .. q'_l' y c_k]
 %         [find m'_{i_k_0}, .., m'_{i_k_nk} | c_0 ~ CK m'_{i_k_0} .. m'_{i_k_nk}]
 %         fun of hb.unify m_{i_0_0} m'_{i_0_0} & ... & hb.unify m_{i_k_nk} m'_{i_k_nk} =>
 %       F p_1 ... p_k T m_i0_j0 .. m_il_jl}}
-pred mk-phant-term.mixins i:term, i:classname, i:phant-term,
+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 T CN PF Params N Ty MLwA Out :- std.do! [
+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,
   coq.name-suffix N "local" Nlocal,
-  (@pi-decl Nlocal Ty t\ sigma SK KC ML\ std.do! [
+  (@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,
+    std.append Params [t] ParamsT,
     SKPT = app [global {get-constructor SI} | ParamsT],
-    ClassTy = app [global CN | ParamsT],
-    (@pi-decl `s` SIParams s\ @pi-decl `c` ClassTy c\ sigma PF2\ std.do![
-       synthesis.under-mixins.then (MLwA t) (fun-unify-mixin T) (mk-phant-term.mixins.aux t Params c CN PF) PF2,
-       fun-unify none s {mk-app SKPT [c]} PF2 (PFU t s c)])
+    ClassTy t = app [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,
+       fun-unify none s {mk-app SKPT [c]} PF2 (PFU t s c),
+       ]),
+    Body t = {fun-unify none t Src
+               {phant-fun-struct t `s` SI Params s\
+                 {fun-implicit `c` (ClassTy t) (PFU t s)}}}
   ]),
-  Out = {phant-fun-struct T `s` SI Params s\
-          {fun-implicit `c` ClassTy (PFU T s)}}
+  fun-implicit Nlocal Ty Body Out
 ].
 
 mk-phant-term.mixins.aux T Params C CN PF X :- std.do![
@@ -234,20 +246,32 @@ mk-phant-term.mixins.aux T Params C CN PF X :- std.do![
   fun-unify none KCM C PF X,
 ].
 
-pred mk-phant-term.class i:term, i:classname, i:phant-term, o:phant-term.
-mk-phant-term.class T CN PF CPF :- !, std.do! [
+pred mk-phant-term.class
+  i:term, i:term, i:classname, i:phant-term, o:phant-term.
+mk-phant-term.class Target Src CN PF CPF :- !, std.do! [
   class-def (class CN _ CMLwP),
-  w-params.fold CMLwP fun-implicit (mk-phant-term.mixins T CN PF) CPF
+  w-params.fold CMLwP fun-implicit
+    (mk-phant-term.mixins Target Src CN PF) CPF,
 ].
 
-pred mk-phant-term.classes i:term, i:list classname, i:list term, i:term,
-                      i:list (w-args mixinname), o:phant-term.
-mk-phant-term.classes EtaF CNF PL T MLwA PhF :- !, std.do! [
+pred mk-phant-term.classes
+  i:term, i:list classname, i:list term, i:term, i:term,
+  i:list (w-args mixinname), o:phant-term.
+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 T ML EtaF FPLTM,
-    std.fold CNF (phant-term [] FPLTM) (mk-phant-term.class T) out]) PhF
+    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
 ].
 
+pred mk-phant-term-with-copy i:term, i:list classname,
+  i:list term, i:name, i:term,
+  i:(term -> list (w-args mixinname)), o:phant-term.
+mk-phant-term-with-copy EtaF CNF PL N Ty MLwA PhF :- !, std.do! [
+  (@pi-decl N Ty target\ @pi-decl N Ty src\ sigma Body\
+    mk-phant-term.classes EtaF CNF PL target src (MLwA target) Body,
+    fun-unify none target src Body (BodyUnif target src)),
+  fun-real N Ty (target\ {fun-real N Ty (BodyUnif target)}) PhF
+].
 
 }}

HB/common/stdpp.elpi

@@ -19,6 +19,9 @@ triple_3 (triple _ _ C) C.
 
 namespace std {
 
+pred nlist i:int, i:A, o: list A.
+nlist N X L :- std.map {std.iota N} (_\ y\ y = X) L.
+
 pred list-diff i:list A, i:list A, o:list A.
 list-diff X [] X.
 list-diff L [D|DS] R :-