Merge pull request #362 from math-comp/speedup-insertion

Speedup `compress` clause insertion

Author: CohenCyril

HB/common/synthesis.elpi

@@ -191,10 +191,16 @@ mixin-for T M MICompressed :- mixin-src T M Tm, !, std.do! [
   compress-coercion-paths MI MICompressed,
 ].
 
+pred compress-copy o:term, o:term.
+compress-copy X Y :- compress X Y, !.
+compress-copy (app L) (app L1) :- !, std.map L compress-copy L1.
+compress-copy X X.
+
+
 pred compress-coercion-paths i:term, o:term.
 compress-coercion-paths MI MICompressed :-
   if (get-option "compress_coercions" tt)
-     (compress MI MICompressed)
+     (compress-copy MI MICompressed)
      (MI = MICompressed).
 
 pred mixin-for_mixin-builder i:prop, o:term.

HB/structure.elpi

@@ -398,7 +398,7 @@ declare-coercion SortProjection ClassProjection
   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 _ (before "compress:begin") c)),
+  std.forall AllCompressionClauses (c\ log.coq.env.accumulate current "hb.db" (clause _ _ c)),
 ].
 
 

structures.v

@@ -232,9 +232,6 @@ pred docstring o:loc, o:string.
 % terms, since this is what you get when you apply coercions)
 :index (4)
 pred compress o:term, o:term.
-:name "compress:begin"
-compress (app L) (app L1) :- !, std.map L compress L1.
-compress X X.
 
 }}.
 

tests/compress_coe.v.out

@@ -1,4 +1,4 @@
-Datatypes_prod__canonical__compress_coe_D = 
+Datatypes_prod__canonical__compress_coe_D =
 fun D D' : D.type =>
 {|
   D.sort := D.sort D * D.sort D';

tests/hnf.v.out

@@ -1,12 +1,12 @@
-Datatypes_nat__canonical__hnf_S = 
+Datatypes_nat__canonical__hnf_S =
 {| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |}
      : S.type
-HB_unnamed_mixin_12 = 
+HB_unnamed_mixin_12 =
 {| M.x := f.y nat HB_unnamed_factory_10 + 1 |}
      : M.axioms_ nat
-Datatypes_bool__canonical__hnf_S = 
+Datatypes_bool__canonical__hnf_S =
 {| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_16 |} |}
      : S.type
-HB_unnamed_mixin_16 = 
+HB_unnamed_mixin_16 =
 Builders_6.HB_unnamed_factory_8 bool HB_unnamed_factory_13
      : M.axioms_ bool

tests/infer.v

@@ -17,7 +17,7 @@ HB.mixin Record barm (A : Type) (P : foo.type) (B: Type) (T : Type) := {
 HB.structure Definition bar A P B := { T of barm A P B T }.
 
 #[skip="8.1[0-5].*"] HB.check (bar.type_ bool nat bool).
-#[skip="8.16.*", fail] HB.check (bar.type_ bool nat bool).
+#[skip="8.1[67].*", fail] HB.check (bar.type_ bool nat bool).
 Print bar.phant_type.
 Print bar.type.
 Check bar.type bool nat bool.