HB compiles!

Author: CohenCyril

HB/common/phant-abbreviation.elpi

@@ -257,21 +257,17 @@ mk-phant-term.mixins Target Src CN PF Params N Ty MLwA Out :- std.do! [
 ].
 
 mk-phant-term.mixins.aux T Params C CN PF X :- std.do![
-  coq.say "entering mk-phant-term.mixins.aux" CN KC,
   get-constructor CN KC,
   synthesis.infer-all-gref-deps Params T KC KCM,
   fun-unify none KCM C PF X,
-  coq.say "exiting mk-phant-term.mixins.aux" CN X,
 ].
 
 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),
-  coq.say "Class Hit:" CN CMLwP,
   w-params.fold CMLwP fun-implicit
     (mk-phant-term.mixins Target Src CN PF) CPF,
-  coq.say "Class Folded!"
 ].
 
 pred mk-phant-term.classes
@@ -281,9 +277,7 @@ 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 Target ML EtaF FPLTM,
-    coq.say "MID-PHANT-TERM-CLASSES",
     std.fold CNF (phant-term [] FPLTM) (mk-phant-term.class Target Src) out]) PhF,
-    coq.say "FOLDED!"
 ].
 
 pred mk-phant-term-with-copy i:term, i:list classname,

HB/common/synthesis.elpi

@@ -17,12 +17,10 @@ namespace synthesis {
 % which are misxins in ML, abstracts the others
 pred infer-all-these-mixin-args i:list term, i:term, i:list mixinname, i:term, o:term.
 infer-all-these-mixin-args Ps T ML F SFX :- std.do! [
-  coq.say "SYNTH MIXINS = " Ps "," T "," ML "," F,
   std.assert-ok! (coq.typecheck F Ty) "try-infer-these-mixin-args: F illtyped",
   coq.mk-eta (-1) Ty F EtaF,
   coq.subst-fun {std.append Ps [T]} EtaF FT,
   private.instantiate-all-these-mixin-args FT T ML SFX,
-  coq.say "SYNTH MIXINS END"
 ].
 
 % [infer-all-gref-deps Ps T GR X] fills in all the arguments of GR

HB/factory.elpi

@@ -296,7 +296,6 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   if-verbose (coq.say {header} "declare notation Build"),
 
   GRDepsClauses => phant.of-gref ff GRK [] PhGRK,
-  coq.say "XXXXXXX",
   GRDepsClauses => phant.add-abbreviation "Build" PhGRK BuildConst BuildAbbrev,
 
   if-verbose (coq.say {header} "declare notation axioms"),

HB/instance.elpi

@@ -240,7 +240,6 @@ declare-instance Factory T F Clauses CFL CSL :-
     T F TheFactory FGR Clauses CFL CSL.
 declare-instance Factory T F Clauses CFL CSL :-
   declare-canonical-instances-from-factory Factory T F Clauses1 CFL CSL,
-  coq.say "DONE",
   if (get-option "export" tt)
      (coq.env.current-library File,
       std.map {std.append CFL CSL} (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2)

HB/structure.elpi

@@ -162,8 +162,6 @@ declare Module BSkel Sort :- std.do! [
 
   export.module {calc (Module ^ ".Exports")} Exports,
 
-  coq.say "Struct = " {coq.env.global Structure},
-
   if-verbose (coq.say {header} "exporting operations"),
     ClassAlias => Factories => GRDepsClauses =>
       private.export-operations Structure SortProjection ClassProjection MLwP [] EX MLToExport,

tests/compress_coe.v.out

@@ -1,4 +1,4 @@
-Datatypes_prod__canonical__compress_coe_D =
+Datatypes_prod__canonical__compress_coe_D@{u} =
 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_8 |} |}
      : S.type
-HB_unnamed_mixin_8 =
+HB_unnamed_mixin_8@{} =
 {| M.x := f.y nat HB_unnamed_factory_6 + 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_12 |} |}
      : S.type
-HB_unnamed_mixin_12 =
+HB_unnamed_mixin_12@{} =
 Builders_1.HB_unnamed_factory_3 bool HB_unnamed_factory_9
      : M.axioms_ bool