Merge pull request #380 from proux01/perf_compress_coercion

A few performance improvements

HB/about.elpi

@@ -192,8 +192,10 @@ main-structure S Class Structure MLwP :-
     std.findall (exported-op m P O) OPS,
     std.map OPS (c\out\ sigma p\ c = exported-op m p out) r) OPLL,
   std.flatten OPLL Operations,
-  std.map {std.findall (sub-class Class C_)} (x\r\ x = sub-class Class r) SubClasses,
-  std.map {std.findall (sub-class C_ Class)} (x\r\ x = sub-class r Class) SuperClasses,
+  std.map {std.findall (sub-class Class CS_ CoeS_ NS_)}
+    (x\r\ x = sub-class Class r _ _) SubClasses,
+  std.map {std.findall (sub-class Cs_ Class Coes_ Ns_)}
+    (x\r\ x = sub-class r Class _ _) SuperClasses,
   % format
   PpOrigin = box (hov 4) [
     str "HB: ", str S, str " is a structure", spc,

HB/common/compat_acc_clauses_816.elpi

@@ -0,0 +1,2 @@
+pred acc-clauses i:scope, i:list prop.
+acc-clauses Scope CL :- std.forall CL (acc-clause Scope).

HB/common/compat_acc_clauses_all.elpi

@@ -0,0 +1,2 @@
+pred acc-clauses i:scope, i:list prop.
+acc-clauses Scope CL :- coq.elpi.accumulate-clauses Scope "hb.db" {std.map CL (c\r\ r = clause _ _ c)}.

HB/common/database.elpi

@@ -155,10 +155,10 @@ 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 classname classname.
-toposort-classes.mk-class-edge (sub-class C1 C2) (pr C2 C1).
+toposort-classes.mk-class-edge (sub-class C1 C2 _ _) (pr C2 C1).
 pred toposort-classes i:list classname, o:list classname.
 toposort-classes In Out :- std.do! [
-  std.findall (sub-class C1_ C2_) SubClasses,
+  std.findall (sub-class C1_ C2_ _ _) SubClasses,
   std.map SubClasses toposort-classes.mk-class-edge ES,
   std.toposort ES In Out,
 ].

HB/common/log.elpi

@@ -181,14 +181,6 @@ log.coq.CS.declare-instance C  :- std.do! [
   log.private.log-vernac (log.private.coq.vernac.canonical Name Local),
 ].
 
-% Since "accumulate" is a keyword we can't use it as a predicate name
-% in the namespace, so we just define it here with the full name
-pred log.coq.env.accumulate i:scope, i:string, i:clause.
-log.coq.env.accumulate S DB CL :- std.do! [
-  coq.elpi.accumulate S DB CL,
-  if-verbose (log.private.log-vernac (log.private.coq.vernac.comment CL)),
-].
-
 pred log.coq.check i:term, o:term, o:term, o:diagnostic.
 log.coq.check Skel Ty T D :- std.do! [
   coq.elaborate-skeleton Skel Ty T D,

HB/common/synthesis.elpi

@@ -191,8 +191,21 @@ mixin-for T M MICompressed :- mixin-src T M Tm, !, std.do! [
   compress-coercion-paths MI MICompressed,
 ].
 
+pred drop i:int, i:list A, o:list A.
+drop 0 L L :- !.
+drop N [_|XS] L :- !, N1 is N - 1, drop N1 XS L.
+
 pred compress-copy o:term, o:term.
-compress-copy X Y :- compress X Y, !.
+compress-copy (app [global (const C) | L]) R :-
+  sub-class C2 C3 C NparamsC,
+  drop NparamsC L [app [global (const C') | L']],
+  sub-class C1 C2 C' NparamsC',
+  drop NparamsC' L' L'',
+  sub-class C1 C3 C'' NparamsC'',
+  std.append {coq.mk-n-holes NparamsC''} L'' HL'',
+  CHL'' = app [global (const C'') | HL''],
+  coq.typecheck CHL'' _ ok, !,
+  compress-copy CHL'' R.
 compress-copy (app L) (app L1) :- !, std.map L compress-copy L1.
 compress-copy X X.
 

HB/common/utils.elpi

@@ -74,8 +74,11 @@ with-locality P :-
 pred acc-clause i:scope, i:prop.
 acc-clause Scope C :- coq.elpi.accumulate Scope "hb.db" (clause _ _ C).
 
+/* Uncomment and remove HB/common/compat_acc_clauses_*.elpi once requiring coq-elpi >= 1.18.0,
+   which implies Coq >= 8.17
 pred acc-clauses i:scope, i:list prop.
-acc-clauses Scope CL :- std.forall CL (acc-clause Scope).
+acc-clauses Scope CL :- coq.elpi.accumulate-clauses Scope "hb.db" {std.map CL (c\r\ r = clause _ _ c)}.
+*/
 
 pred save-docstring.
 save-docstring :-

HB/context.elpi

@@ -39,7 +39,7 @@ declare.mixins TheType TheParamsSection MLwPRaw MLwP MSL CL :-  std.do! [
   std.map TheParamsSection triple_2 TheParams,
   apply-w-params MLwPRaw TheParams TheType MLwAllArgsRaw,
   std.fold MLwAllArgsRaw (triple [] [] []) (private.postulate-mixin TheType) (triple CL MSL MLwPRev),
-  std.forall CL (cs\ acc-clause current (local-canonical cs)),
+  acc-clauses current {std.map CL (cs\r\ r = local-canonical cs)},
   std.rev MLwPRev MLwPSection,
   build-list-w-params TheParamsSection TheType MLwPSection MLwP,
   acc-clauses current MSL,

HB/structure.elpi

@@ -160,37 +160,14 @@ declare Module BSkel Sort :- std.do! [
 
   @global! => log.coq.notation.add-abbreviation "on" 1
     {{fun T => (lp:{{ ClassOfAbbrev_ {{_}} }} : (lp:AppClassHoles T)) }} tt
-    OnAbbrev,
-
-  log.coq.env.begin-module "EtaAndMixinExports" none,
-
-  if (get-option "primitive" tt) true (
-    if-verbose (coq.say {header} "eta expanded instances"),
-    NewClauses => std.do! [
-      w-params.fold MLwP mk-fun
-        (private.mk-hb-eta.on Structure SortProjection OnAbbrev) EtaInstanceBody,
-      w-params.fold MLwP (mk-parameter explicit)
-        (private.mk-hb-eta.arity Structure ClassName SortProjection)
-        EtaInstanceArity,
-      instance.declare-const "_" EtaInstanceBody EtaInstanceArity _
-    ]
-    ),
-
-  % std.flatten {std.map NewMixins mixin->factories} NewFactories,
-  % NewClauses => std.forall NewFactories instance.declare-factory-sort-factory,
-
-  log.coq.env.end-module-name "EtaAndMixinExports" EtaExports,
+    _OnAbbrev,
 
   log.coq.env.end-module-name Module ModulePath,
 
   if-verbose (coq.say {header} "end modules; export" Exports),
 
   export.module {calc (Module ^ ".Exports")} Exports,
 
-  if-verbose (coq.say {header} "export" EtaExports),
-
-  export.module {calc (Module ^ ".EtaAndMixinExports")} EtaExports,
-
   if-verbose (coq.say {header} "exporting operations"),
     ClassAlias => Factories => GRDepsClauses =>
       private.export-operations Structure SortProjection ClassProjection MLwP [] EX MLToExport,
@@ -360,8 +337,6 @@ pred declare-coercion i:term, i:term, i:class, i:class.
 declare-coercion SortProjection ClassProjection
     (class FC StructureF FMLwP) (class TC StructureT TMLwP) :- std.do! [
 
-  acc-clause current (sub-class FC TC),
-
   gref->modname StructureF 2 "_" ModNameF,
   gref->modname StructureT 2 "_" ModNameT,
   CName is ModNameF ^ "_class__to__" ^ ModNameT ^ "_class",
@@ -393,41 +368,10 @@ declare-coercion SortProjection ClassProjection
 
   log.coq.CS.declare-instance SC,
 
-  if-verbose (coq.say {header} "declare coercion path compression rules"),
-
-  findall-classes All,
-  CurrentTgtClass = (class TC StructureT TMLwP),
-  std.filter All (sub-class? CurrentTgtClass) AllTgtSuper,
-  std.map AllTgtSuper class_structure AllTgtSuperStructures,
-
-  mk-compression-clauses StructureF StructureT AllTgtSuperStructures AllCompressionClauses,
-  std.forall AllCompressionClauses (c\ log.coq.env.accumulate current "hb.db" (clause _ _ c)),
+  w-params.nparams FMLwP NparamsSC,
+  acc-clause current (sub-class FC TC SC NparamsSC)
 ].
 
-
-pred mk-compression-clauses i:gref, i:gref, i:list gref, o:list prop.
-mk-compression-clauses _ _ [] [].
-mk-compression-clauses StructureF StructureT [StructureE|Rest] Res :- std.do! [
-  std.assert! (coq.coercion.db-for (grefclass StructureF) (grefclass StructureT) [pr C1 Nparams1]) "wrong number of coercions",
-  std.assert! (coq.coercion.db-for (grefclass StructureT) (grefclass StructureE) [pr C2 Nparams2]) "wrong number of coercions",
-  std.assert! (coq.coercion.db-for (grefclass StructureF) (grefclass StructureE) [pr C3 Nparams3]) "wrong number of coercions",
-  coq.mk-app (global C1) {coq.mk-n-holes Nparams1} F,
-  coq.mk-app (global C2) {coq.mk-n-holes Nparams2} G,
-  coq.mk-app (global C3) {coq.mk-n-holes Nparams3} H,
-  RuleSkel = {{ fun x => lp:G (lp:F x) = lp:H x}},
-  std.assert-ok! (coq.elaborate-skeleton RuleSkel _ Rule) "coercion composition fails",
-  (((pi X L\ coq.fold-map X L X [X|L] :- var X, not(std.exists L (same_var X))) => coq.fold-map Rule [] Rule Holes,
-  mk-compression-clause Holes Rule Clause,
-  mk-compression-clauses StructureF StructureT Rest Clauses,
-  Res = [Clause|Clauses]) ; (Res = [])),
-].
-
-pred mk-compression-clause i:list term, i:term, o:prop.
-mk-compression-clause [] (fun _ _ x\ app[_,_,LHS x,RHS x]) (pi x\ C x) :-
-  pi x\ copy (LHS x) (L x), copy (RHS x) (R x), C x = (pi tmp\ compress (L x) (R x)).
-mk-compression-clause [UV|Rest] T (pi v\ R v) :-
-  pi v\ (pi U\ copy U v :- same_var U UV, !) => mk-compression-clause Rest T (R v).
-
 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
@@ -714,32 +658,4 @@ sigT->list-w-params {{ lib:@hb.sigT _ lp:{{ fun N Ty B }} }} L C :-
   @pi-decl N Ty t\
     product->triples (B t) (Rest t) C.
 
-pred mk-hb-eta.on i:structure, i:term, i:abbreviation,
-  i:list term, i:name, i:term, i:A, o:term.
-mk-hb-eta.on Structure SortProjection OnAbbrev
-    Params NT _T _ (fun NT Ty Body) :- !, std.do! [
-  coq.mk-app (global Structure) Params Ty,
-  @pi-decl NT Ty s\ sigma Tm\ std.do! [
-    coq.mk-app {{lib:@hb.eta}}
-      [_, {coq.mk-app SortProjection {std.append Params [s]}}]
-      Tm,
-    std.assert-ok! (coq.typecheck Tm _) "HB: eta illtyped",
-    coq.notation.abbreviation OnAbbrev [Tm] (Body s)
-  ]
-].
-
-pred mk-hb-eta.arity i:structure, i:classname, i:term, i:list term,
-  i:name, i:term, i:A, o:arity.
-mk-hb-eta.arity Structure ClassName SortProjection
-    Params NT _T _ Out :- !, std.do! [
-  coq.mk-app (global Structure) Params Ty,
-  (@pi-decl NT Ty s\ sigma Tm\ std.do! [
-    coq.mk-app {{lib:@hb.eta}}
-      [_, {coq.mk-app SortProjection {std.append Params [s]}}] Tm,
-    std.assert-ok! (coq.typecheck Tm _) "HB: eta illtyped",
-    coq.mk-app (global ClassName) {std.append Params [Tm]} (Concl s)
-  ]),
-  Out = parameter {coq.name->id NT} explicit Ty s\ arity (Concl s)
-].
-
 }}