Coq master 0.9.1

.travis.yml

@@ -3,6 +3,7 @@ version: ~> 1.0
 branches:
   only:
   - master
+  - coq-master
 
 env:
   global:

Changelog.md

@@ -1,5 +1,14 @@
 # Changelog
 
+## [0.9.1] - 2020-06-03
+
+- `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
+- Operations `op` from factory `f` are not bound to `f_op` anymore,
+  they are now bound to `op` and potentially masked operations
+  are accessible via `Super.op`.
+
 ## [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.

coq-hierarchy-builder.opam

@@ -11,8 +11,7 @@ dev-repo: "git+https://github.com/math-comp/hierarchy-builder"
 build: [ make ]
 install: [ make "install" "VFILES=structures.v" ]
 depends: [
-  "coq"      {>= "8.10.0" & < "8.12.0~" }
-  "coq-elpi" {>= "1.3.0" & < "1.4.0~"}
+  "coq-elpi"
   ]
 synopsis: "Hierarchy Builder"
 description: """

default.nix

@@ -1,44 +1,36 @@
 {withEmacs ? false,
  nixpkgs ?  (fetchTarball {
-  url = "https://github.com/CohenCyril/nixpkgs/archive/7f59c094a0e5c8659856e611075fe88d6177830f.tar.gz";
-  sha256 = "00cf4r8dqfx2hwlwaqb239h72m4s0wl97i98424xd4hki0vzifbi";
+  url = "https://github.com/CohenCyril/nixpkgs/archive/8d04d29adb547353ed9fb5c5c4aa6d540e198366.tar.gz";
+  sha256 = "1v4l37xkadpnkydpycnk9hrjgh6yc792k66yi7f6203zzr0phzx8";
 }),
  coq-version ? "8.11",
  print-env ? false
 }:
-with import nixpkgs {};
-let
-  pgEmacs = emacsWithPackages (epkgs:
-    with epkgs.melpaStablePackages; [proof-general]);
-  myCoqPackages = {
-    "8.10" = coqPackages_8_10;
-    "8.11" = coqPackages_8_11;
-    }."${coq-version}";
-  coq = myCoqPackages.coq;
-  coq-elpi = myCoqPackages.coq-elpi.overrideAttrs(o: {
-    name = "coq8.11-elpi-v1.4.0";
-    src = fetchTarball https://github.com/LPCIC/coq-elpi/archive/v1.4.0.tar.gz;
-  });
-in
-stdenv.mkDerivation {
+with import nixpkgs {
+  overlays = [ (super: self: {
+    coqPackages = { "8.11" = super.coqPackages_8_11;  }."${coq-version}".overrideScope' (self: super: {
+      ## Coq package override example:
+      # coq-elpi = super.coq-elpi.overrideAttrs (old: {
+      #   name = "coq8.11-elpi-v1.4.0";
+      #   src = fetchTarball https://github.com/LPCIC/coq-elpi/archive/v1.4.0.tar.gz;
+    });
+    coq = self.coqPackages.coq;
+  })];
+};
+let pgEmacs = emacsWithPackages (epkgs: with epkgs.melpaStablePackages; [proof-general]); in
+coqPackages.hierarchy-builder.overrideAttrs (old: {
   name = "coq${coq.coq-version}-hierarchy-builder-dev";
-
   src = ./.;
-
-  nativeBuildInputs = [ which ];
-  buildInputs = [ coq coq.ocaml coq.ocamlPackages.elpi coq-elpi ];
-
-  installPhase = ''make -f Makefile.coq VFILES=structures.v COQLIB=$out/lib/coq/${coq.coq-version}/ install'';
-
-  meta = {
-    description = "Coq plugin embedding ELPI.";
-    maintainers = [ stdenv.lib.maintainers.cohencyril ];
-    license = stdenv.lib.licenses.lgpl21;
-    inherit (coq.meta) platforms;
-    inherit (src.meta) homepage;
-  };
-
-  passthru = {
-    compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params;
-  };
+  buildInputs = old.buildInputs ++
+                (if lib.trivial.inNixShell then lib.optional withEmacs pgEmacs
+                 else []);
 }
+// (if lib.trivial.inNixShell then {
+  shellHook = ''
+    nixEnv (){
+      echo "Here is your work environement:"
+      for x in $buildInputs; do printf "  "; echo $x | cut -d "-" -f "2-"; done
+      echo "you can pass option '--argstr coq-version \"x.y\"' to nix-shell to change coq versions"
+    }
+  '' + lib.optionalString print-env "nixEnv";
+} else {}))

hb.elpi

@@ -585,7 +585,7 @@ mk-phant-implicit N Ty PF (phant-term [implicit-arg|AL] (fun N Ty F)) :- !,
 pred mk-phant-struct i:term, i:term, i:(term -> phant-term), o:phant-term.
 mk-phant-struct T SI PF (phant-term [implicit-arg, unify-arg|AL] UF) :-
   get-structure-sort-projection SI Sort,
-  pi s\ PF s = phant-term AL (F s),
+  (pi s\ PF s = phant-term AL (F s)),
   UF = {{fun (s : lp:SI) (u : lib:hb.unify lp:T (lp:Sort s)
     (lib:hb.some (lib:hb.pair "is not canonically a"%string lp:SI)))
       => lp:(F s)}}.
@@ -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.