Use only sub-class in compress_coercion

The compress predicate had a cubic number of entries in the size of
a hierarchy whereas sub-class is only quadratic.

Compilation of MathComp:
before: 22:57 (1.53 GB)
  HB.structure: 05:42
  HB.instance: 02:31
after: 20:36 (1.26 GB)
  HB.structure: 03:10
  HB.instance: 02:29

Author: proux01

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/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/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/structure.elpi

@@ -360,8 +360,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 +391,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,
-  acc-clauses current AllCompressionClauses,
+  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

structures.v

@@ -142,9 +142,10 @@ pred is-structure o:gref.
 % the [F.Build T] abbreviation the term behind it has N arguments before T
 pred factory-builder-nparams o:constant, o:int.
 
-% [sub-class C1 C2] C1 is a sub-class of C2, see also sub-class? which computes
-% it on the fly
-pred sub-class o:classname, o:classname.
+% [sub-class C1 C2 Coercion12 NparamsCoercion] C1 is a sub-class of C2,
+% see also sub-class? which computes it on the fly
+:index (2 2 1)
+pred sub-class o:classname, o:classname, o:constant, o:int.
 
 % [gref-deps GR MLwP] is a (pre computed) list of dependencies of a know global
 % constant. The list is topologically sorted
@@ -226,13 +227,6 @@ pred decl-location o:gref, o:loc.
 % [docstring Loc Doc] links a location in the source text and some doc
 pred docstring o:loc, o:string.
 
-%% database for #[compress_coercions] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% coercions chains compression rules (we only care about non applicative
-% terms, since this is what you get when you apply coercions)
-:index (4)
-pred compress o:term, o:term.
-
 }}.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)