Merge pull request #181 from math-comp/no_section_discharge_for_factory_aliases

No section discharge for alias factories and builder mixins

Author: gares

HB/common/stdpp.elpi

@@ -138,7 +138,7 @@ coq.gref.list->set L S :-
   std.fold L {coq.gref.set.empty} coq.gref.set.add S.
 
 % [coq.abstract-indt-decl Section I AbsI] abstracts I over the Section variables
-% which becomes parameter nodes if the indt-decl type
+% which becomes parameter nodes of the indt-decl type
 pred coq.abstract-indt-decl i:list constant, i:indt-decl, o:indt-decl.
 coq.abstract-indt-decl [] X X1 :- copy-indt-decl X X1.
 coq.abstract-indt-decl [C|CS] X (parameter ID explicit Ty1 X1) :-
@@ -149,6 +149,19 @@ coq.abstract-indt-decl [C|CS] X (parameter ID explicit Ty1 X1) :-
     (copy (global (const C)) x :- !) =>
     coq.abstract-indt-decl CS X (X1 x).
 
+% [coq.abstract-const-decl Section I AbsI] abstracts I over the Section variables
+% which becomes fun nodes
+pred coq.abstract-const-decl i:list constant, i:pair term term, o:pair term term.
+coq.abstract-const-decl [] (pr X Y) (pr X1 Y1) :- copy X X1, copy Y Y1.
+coq.abstract-const-decl [C|CS] X (pr (fun Name Ty1 X1) (prod Name Ty1 X2)) :-
+  coq.gref->string (const C) ID,
+  coq.id->name ID Name,
+  coq.env.typeof (const C) Ty,
+  copy Ty Ty1,
+  @pi-parameter ID Ty x\
+    (copy (global (const C)) x :- !) =>
+    coq.abstract-const-decl CS X (pr (X1 x) (X2 x)).
+
 % [coq.copy-clauses-for-unfold CS CL] generates clauses for the copy predicate
 % to unfold all constants in CS
 pred coq.copy-clauses-for-unfold i:list constant, o:list prop.

HB/common/synthesis.elpi

@@ -31,7 +31,7 @@ pred infer-all-mixin-args i:list term, i:term, i:gref, o:term.
 infer-all-mixin-args Ps T GR X :- !, std.do! [
   std.assert! (gref-deps GR MLwP) "BUG: gref-deps should never fail",
   list-w-params_list MLwP ML,
-  infer-mixin-args Ps T ML (global GR) X
+  infer-mixin-args Ps T ML (global GR) X,
 ].
 
 % [assert!-infer-mixin TheType M Out] infers one mixin M on TheType and
@@ -109,7 +109,7 @@ namespace private {
 % the databases [mixin-src] and [from]
 pred mixin-for i:term, i:mixinname, o:term.
 mixin-for T M MICompressed :- mixin-src T M Tm, !, std.do! [
-  if-verbose (coq.say "HB: Trying to infer mixin for" M),
+  %if-verbose (coq.say "HB: Trying to infer mixin for" M),
   std.assert-ok! (coq.typecheck Tm Ty) "mixin-for: Tm illtyped",
 
   factory? Ty (triple Factory Params _),
@@ -119,7 +119,7 @@ mixin-for T M MICompressed :- mixin-src T M Tm, !, std.do! [
       coq.subst-fun [Tm] B MI
   ),
 
-  if-verbose (coq.say "HB: Trying to compress mixin for" {coq.term->string MI}),
+  %if-verbose (coq.say "HB: Trying to compress mixin for" {coq.term->string MI}),
   compress-coercion-paths MI MICompressed,
 ].
 

HB/factory.elpi

@@ -157,22 +157,28 @@ process-asset-unnamed-parameters (asset-record _ Sort _ Fields) GRFS Module TheT
 
 pred declare-factory-alias i:term, i:list-w-params factoryname, i:id, i:term, i:list term.
 declare-factory-alias Ty1Skel GRFSwP Module TheType TheParams :- std.do! [
-
   % TODO maybe context.declare should just take GRFSwP and postulate
   % the parameters and the type
-  context.declare TheType TheParams GRFSwP Hyps _,
+  context.declare TheType TheParams GRFSwP MixinSrcClauses SectionCanonicalInstance,
+
+  if-verbose (coq.say "HB: declare constant axioms_"),
 
   std.assert-ok! (coq.elaborate-ty-skeleton Ty1Skel _ Ty1) "Illtyped alias factory",
-  log.coq.env.add-const-noimplicits "axioms_" Ty1 _ @transparent! C,
+
+  abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-const-decl (pr Ty1 _) (pr Ty1Closed _) Section,
+  log.coq.env.add-const-noimplicits "axioms_" Ty1Closed _ @transparent! C,
 
   std.assert! (safe-dest-app Ty1 (global PhF) _Args) "Argument must be a factory",
   std.assert! (factory-alias->gref PhF F) "BUG: Factory alias declaration missing",
   std.assert! (factory-constructor F FK) "BUG: Factory constructor missing",
 
-  Hyps => synthesis.infer-all-mixin-args TheParams TheType FK MFK,
+  MixinSrcClauses => synthesis.infer-all-mixin-args TheParams TheType FK MFK,
   std.assert-ok! (coq.typecheck MFK MFKTy) "BUG: typecking of former factory constructor failed",
-  (pi Args\ copy (app [global F|Args]) (global (const C))) => copy MFKTy MFKTyC,
-  log.coq.env.add-const-noimplicits "Axioms_" MFK MFKTyC @transparent! CK,
+  (pi Args\ copy (app[global F|Args]) (app[global (const C)|Section])) => copy MFKTy MFKTyC,
+
+  abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-const-decl (pr MFK MFKTyC) (pr MFKClosed MFKTyCClosed) _,
+  log.coq.env.add-const-noimplicits "Axioms_" MFKClosed MFKTyCClosed @transparent! CK,
+
   GRK = const CK,
 
   log.coq.env.end-section-name Module,
@@ -224,16 +230,16 @@ build-deps-for-projections R MLwP CL :- std.do! [
 % variables that aoccur. We don't want that for mixin/factories, so we implement
 % our own discharging. Note that definitions (like canonical instance) have
 % to be abstracted too.
-pred abstract-indt-decl-over-section i:list term, i:term, i:list prop, i:list constant, i:indt-decl, o:indt-decl.
-abstract-indt-decl-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance RDecl RDeclClosed :-
+pred abstract-over-section i:list term, i:term, i:list prop, i:list constant, i:(list constant -> A -> A -> prop), i:A, o:A, o:list term.
+abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance F X X1 Section :-
   % compute section variables to be used for discharging
   std.map MixinSrcClauses mixin-src_src Mixins,
   std.append TheParams [TheType|{std.rev Mixins}] Section,
   std.map Section (x\r\ x = global (const r)) SectionVars,
   % We discharge by hand the record declaration so that we can be sure all
   % parameters and mixins are abstracted (even if unused).
   coq.copy-clauses-for-unfold SectionCanonicalInstance CopyUnfold,
-  CopyUnfold => coq.abstract-indt-decl SectionVars RDecl RDeclClosed.
+  CopyUnfold => F SectionVars X X1.
 
 pred declare-mixin-or-factory i:term, i:record-decl, i:list-w-params factoryname, i:id, i:term, i:asset, i:list term.
 declare-mixin-or-factory Sort1 Fields GRFSwP Module TheType D TheParams :- std.do! [
@@ -245,7 +251,7 @@ declare-mixin-or-factory Sort1 Fields GRFSwP Module TheType D TheParams :- std.d
   RDeclSkel = record "axioms_" Sort1 Kname Fields,
   std.assert-ok! (coq.elaborate-indt-decl-skeleton RDeclSkel RDecl) "record declaration illtyped",
 
-  abstract-indt-decl-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance RDecl RDeclClosed,
+  abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _,
 
   log.coq.env.add-indt RDeclClosed R,
   log.coq.env.end-section-name Module, % We need to anyway declare the record inside the section

HB/instance.elpi

@@ -89,7 +89,9 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
   coq.gref->path TGR TPath,
   std.rev TPath [TMod|_],
   coq.gref->id TGR TID,
-  Name is TMod ^ "_" ^ TID ^ "_canonical_" ^ {gref->modname Struct},
+  if (TMod = TID)
+     (Name is TID ^ "_canonical_" ^ {gref->modname Struct})
+     (Name is TMod ^ "_" ^ TID ^ "_canonical_" ^ {gref->modname Struct}),
 
   if-verbose (coq.say "HB: declare canonical structure instance" Name),
 

examples/demo1/hierarchy_5.v

@@ -223,4 +223,7 @@ Proof. by rewrite -addrA subrr addr0. Qed.
 
 End Theory.
 
-HB.graph "hierarchy_5.dot".
+HB.graph "hierarchy_5.dot".
+
+(* we check the alias factory is abstracted over the whole section *)
+HB.check (SemiRing_of_AddComoid.axioms_ : forall A, forall m : AddMonoid_of_TYPE.axioms_ A, AddComoid_of_AddMonoid.axioms_ A m -> Type).

tests/compress_coe.v

@@ -34,4 +34,4 @@ HB.instance Definition prodD (D D' : D.type) :=
   hasD.Build (D * D')%type (d, d).
 
 Set Printing Coercions.
-Print prod_prod_canonical_D.
+Print prod_canonical_D.

tests/compress_coe.v.out

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