Merge pull request #73 from math-comp/instance-def

syntax HB.instance Definition := ...

Author: gares

Changelog.md

@@ -1,5 +1,11 @@
 # Changelog
 
+## Unreleased
+
+- `HB.instance` can be applied directly to a definition as in
+  `HB.instance Definition foo := Bar.Build T ...`
+- port to coq-elpi version 1.4
+
 ## [0.9.0] - 2020-03-11
 
 First public release for Coq 8.10 and 8.11.

README.md

@@ -54,10 +54,8 @@ We proceed by showing that `Z` is an example of both structures, and use
 the lemma just proved on a statement about `Z`.
 
 ```coq
-Definition Z_CoMoid := AddComoid_of_Type.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l.
-HB.instance Z Z_CoMoid.
-Definition Z_AbGrp := AbelianGrp_of_AddComoid.Build Z Z.opp Z.add_opp_diag_l.
-HB.instance Z Z_AbGrp.
+HB.instance Definition Z_CoMoid := AddComoid_of_Type.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l.
+HB.instance Definition Z_AbGrp := AbelianGrp_of_AddComoid.Build Z Z.opp Z.add_opp_diag_l.
 
 Lemma example2 (x : Z) : x + (- x) = - 0.
 Proof. by rewrite example. Qed.

hb.elpi

@@ -1273,7 +1273,7 @@ declare-factory-alias Ty1 GRFS Module TheType :- std.do! [
 
   mk-phant-mixins (global GRK) PhGRK0,
   if (mixin-first-class F _) (PhGRK = PhGRK0) (append-phant-unify PhGRK0 PhGRK),
-  mk-phant-abbrev "Build" PhGRK _ _,
+  mk-phant-abbrev "Build" PhGRK BuildConst _,
 
   std.map Hyps mixin-src_mixin ML,
   main-factory-requires "axioms" (const C) ML Props SN,
@@ -1285,6 +1285,7 @@ declare-factory-alias Ty1 GRFS Module TheType :- std.do! [
   % std.map {gr-deps GRK} (_\ r\ r = maximal) Implicits,
   % coq.arguments.set-implicit GRK [[maximal|Implicits]] tt,
   acc current (clause _ _ (factory-constructor (const C) GRK)),
+  acc current (clause _ _ (factory-builder-nparams BuildConst 0)),
   coq.env.end-module Exports,
   coq.env.end-module _Module,
 
@@ -1319,7 +1320,7 @@ declare-mixin-or-factory Sort1 Fields0 GRFS Module TheType D :- std.do! [
   if-verbose (coq.say "HB: declare notation Axioms"),
 
   if (D = asset-mixin) (PhGRK = PhGRK0) (append-phant-unify PhGRK0 PhGRK),
-  mk-phant-abbrev "Build" PhGRK _ _,
+  mk-phant-abbrev "Build" PhGRK BuildConst _,
 
   std.map Hyps mixin-src_mixin ML,
   if (D = asset-mixin)
@@ -1333,6 +1334,7 @@ declare-mixin-or-factory Sort1 Fields0 GRFS Module TheType D :- std.do! [
   std.map {gr-deps GRK} (_\ r\ r = maximal) Implicits,
   coq.arguments.set-implicit GRK [[maximal|Implicits]] tt,
   acc current (clause _ _ (factory-constructor (indt R) GRK)),
+  acc current (clause _ _ (factory-builder-nparams BuildConst 0)),
   coq.env.end-module Exports,
   coq.env.end-module _Module,
 

readme.v

@@ -30,10 +30,8 @@ Notation "- x" := (opp x).
 Lemma example (G : AbelianGrp.type) (x : G) : x + (- x) = - 0.
 Proof. by rewrite addrC addNr -[LHS](addNr zero) addrC add0r. Qed.
 
-Definition Z_CoMoid := AddComoid_of_Type.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l.
-HB.instance Z Z_CoMoid.
-Definition Z_AbGrp := AbelianGrp_of_AddComoid.Build Z Z.opp Z.add_opp_diag_l.
-HB.instance Z Z_AbGrp.
+HB.instance Definition Z_CoMoid := AddComoid_of_Type.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l.
+HB.instance Definition Z_AbGrp := AbelianGrp_of_AddComoid.Build Z Z.opp Z.add_opp_diag_l.
 
 Lemma example2 (x : Z) : x + (- x) = - 0.
 Proof. by rewrite example. Qed.

structures.v

@@ -79,6 +79,10 @@ pred mixin-src o:term, o:mixinname, o:term.
 %      Notation   Abbrev t1 := (AbbrevSt t1 _ idfun).
 pred phant-abbrev o:gref, o:gref, o:abbreviation.
 
+% [factory-builder-nparams Build N] states that when the user writes
+% 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.
 pred sub-class o:class, o:class.
 
@@ -251,6 +255,8 @@ Elpi Export HB.structure.
     …
     Definition fN : FactoryN T := FactoryN.Build T …
     HB.instance T f1 … fN.
+
+    HB.instance Definition N := Factory.Build T …
     >>
 
 *)
@@ -259,9 +265,18 @@ Elpi Command HB.instance.
 Elpi Accumulate File "hb.elpi".
 Elpi Accumulate Db hb.db.
 Elpi Accumulate lp:{{
+main [const-decl Name (some Body) TyWP] :- !, std.do! [
+  coq.arity->term TyWP Ty,
+  std.assert-ok! (coq.typecheck Body Ty) "Definition illtyped",
+  std.assert! (coq.safe-dest-app Body (global (const Builder)) Args) "Not an application of a builder, use a section if you have parameters",
+  std.assert! (factory-builder-nparams Builder NParams) "Not a factory builder synthesized by HB",
+  coq.env.add-const Name Body Ty ff ff C,
+  std.appendR {coq.mk-n-holes NParams} [T|_] Args,
+  with-attributes (main-declare-canonical-instances T [global (const C)]),
+].
 main [S|FIS] :- std.map [S|FIS] argument->term [T|FIL], !,
   with-attributes (main-declare-canonical-instances T FIL).
-main _ :- coq.error "Usage: HB.instance <CarrierTerm> <FactoryInstanceTerm>*".
+main _ :- coq.error "Usage: HB.instance <CarrierTerm> <FactoryInstanceTerm>*\nUsage: HB.instance Definition <Name> := <Builder> T ...".
 
 }}.
 Elpi Typecheck.