Merge pull request #70 from math-comp/coq-elpi-1.4

port to coq-elpi 1.4

Author: CohenCyril

.travis.yml

@@ -7,37 +7,18 @@ branches:
 env:
   global:
   - CONTRIB_NAME=hb
-  - ELPI_810=coq-elpi.1.3.0
-  - ELPI_811=coq-elpi.1.3.1
+  - ELPI_811=coq-elpi.1.4.0
   - ELPI_DEV=https://github.com/LPCIC/coq-elpi.git#coq-master
 
 jobs:
   include:
-  - language: nix
-    env:
-    - COQ=8.10
-    script:
-    - nix-build --argstr coq-version "${COQ}"
 
   - language: nix
     env:
     - COQ=8.11
     script:
     - nix-build --argstr coq-version "${COQ}"
 
-  - dist: bionic
-    language: minimal
-    services:
-    - docker
-    env:
-    - COQ=8.10 ELPI="install ${ELPI_810}" CMD="make && make install"
-    install:
-    - ./.travis/docker-install.sh
-    script:
-    - ./.travis/docker-test.sh
-    after_script:
-    - docker stop COQ
-
   - dist: bionic
     language: minimal
     services:

coq-hierarchy-builder.opam

@@ -11,8 +11,8 @@ 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"      {>= "8.11.0" & < "8.12.0~" }
+  "coq-elpi" {>= "1.4.0" & < "1.5.0~"}
   ]
 synopsis: "Hierarchy Builder"
 description: """

default.nix

@@ -1,41 +1,36 @@
 {withEmacs ? false,
  nixpkgs ?  (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/82b54d490663b6d87b7b34b9cfc0985df8b49c7d.tar.gz";
-  sha256 = "12gpsif48g5b4ys45x36g4vdf0srgal4c96351m7gd2jsgvdllyf";
+  url = "https://github.com/CohenCyril/nixpkgs/archive/8d04d29adb547353ed9fb5c5c4aa6d540e198366.tar.gz";
+  sha256 = "1v4l37xkadpnkydpycnk9hrjgh6yc792k66yi7f6203zzr0phzx8";
 }),
- coq-version ? "8.10",
+ 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;
-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

@@ -30,6 +30,8 @@
      see phant-abbrev, used to talk about the non canonical name of Foo
 */
 
+shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta }.
+
 %%%%%%%%% Elpi Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % This code could be moved in Elpi's standard library
 
@@ -81,7 +83,7 @@ add-abbrev N NParams AbbrevT Global OnlyParse Abbrev :-
 % runs P in a context where Coq #[attributes] are parsed
 pred with-attributes i:prop.
 with-attributes P :-
-  attributes A, parse-attributes A [att "verbose" bool] Opts, !,
+  attributes A, coq.parse-attributes A [att "verbose" bool] Opts, !,
   Opts => P.
 
 pred if-verbose i:prop.
@@ -125,14 +127,16 @@ name-of-asset-decl (asset-record X _ _ _) X.
 name-of-asset-decl (asset-alias X _) X.
 
 pred argument->asset i:argument, o:asset-decl.
-argument->asset (indt-decl (parameter Name Ty I)) (asset-parameter "T" Ty A) :- % TODO, take the name
+argument->asset (indt-decl (parameter ID _ Ty I)) (asset-parameter ID Ty A) :-
+  coq.string->name ID Name,
   @pi-decl Name Ty a\
     argument->asset (indt-decl (I a)) (A a).
 argument->asset (indt-decl (record Rid Ty Kid F)) (asset-record Rid Ty Kid F) :- !.
-argument->asset (const-decl Id (some (fun _ _ Bo)) (some (prod Name Src Ty))) (asset-parameter "T" Src A) :- !,
+argument->asset (const-decl Id (some (fun _ _ Bo)) (parameter ID _ Src Ty)) (asset-parameter ID Src A) :- !,
+  coq.id->name ID Name,
   @pi-decl Name Src a\
-    argument->asset (const-decl Id (some (Bo a)) (some (Ty a))) (A a).
-argument->asset (const-decl Id (some Bo) (some Ty)) (asset-alias Id Bo) :- !,
+    argument->asset (const-decl Id (some (Bo a)) (Ty a)) (A a).
+argument->asset (const-decl Id (some Bo) (arity Ty)) (asset-alias Id Bo) :- !,
   std.assert! (var Ty) "Factories aliases should not be given a type".
 argument->asset X _ :- coq.error "Unsupported asset:" X.
 
@@ -341,8 +345,9 @@ local-cs? TyTerm Struct :-
 pred get-canonical-mixins-of i:term, i:structure, o:list prop.
 get-canonical-mixins-of T S MSL :- std.do! [
   get-structure-sort-projection S Sort,
-  coq.unify-eq T (app [Sort, ST]),
-  coq.unify-eq ST (app [_, _, C]),
+  std.assert-ok! (coq.unify-eq T (app [Sort, ST])) "HB: get-canonical-mixins-of: T = sort ST",
+  % Hum, this unification problem is not super trivial. TODO replace by something simpler
+  std.assert-ok! (coq.unify-eq ST (app [_, _, C])) "HB: get-canonical-mixins-of: ST = _ _ C",
   C = app [_, _ | MIL],
   std.map MIL (mixin-srcs T) MSLL,
   std.flatten MSLL MSL
@@ -966,7 +971,7 @@ declare-class ML (indt ClassName) Factories :- std.do! [
 
   (@pi-decl `T` {{Type}} t\ synthesize-fields t ML (RDecl t)),
   ClassDeclaration =
-    (parameter `T` {{ Type }} t\
+    (parameter "T" explicit {{ Type }} t\
       record "axioms" {{ Type }} "Class" (RDecl t)),
   std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped",
   coq.env.add-indt ClassDeclaration ClassName,
@@ -1085,8 +1090,7 @@ main-begin-declare Module TName GRFS Decl :- std.do! [
 
   if-verbose (coq.say "HB: postulate type" TName),
 
-  coq.univ.new [] U,
-  Ty = sort (typ U),
+  coq.fresh-type Ty,
   coq.env.add-const TName _ Ty tt tt T, % no body, local -> a variable
   main-declare-context (global (const T)) GRFS _,
   acc current (clause _ _ (current-decl Decl))
@@ -1149,11 +1153,11 @@ declare-old-constant (some C) :-
 declare-old-constant _ :- true.
 
 pred main-begin-declare-builders i:context-decl.
-main-begin-declare-builders (context-item _ _ none _\ context-item IDF _ (some _) _\ context-end) :-
+main-begin-declare-builders (context-item _ _ _ none _\ context-item IDF _ _ (some _) _\ context-end) :-
     coq.error "factories cannot be given a body:" IDF.
-main-begin-declare-builders (context-item _ _ none _\ context-item ID1 _ none _\ context-item ID2 _ _ _) :-
+main-begin-declare-builders (context-item _ _ _ none _\ context-item ID1 _ _ none _\ context-item ID2 _ _ _ _) :-
   coq.error "only one factory is supported, got at least two" ID1 "and" ID2.
-main-begin-declare-builders (context-item IDT T none t\ context-item IDF (F t) none _\ context-end) :- std.do! [
+main-begin-declare-builders (context-item IDT _ T none t\ context-item IDF _ (F t) none _\ context-end) :- std.do! [
   Name is "Builders_" ^ {term_to_string {new_int}}, % TODO
   std.assert! (pi t\ F t = app[global GRA, t|_]) "a factory must be a name applied to the type variable",
   factory-alias->gref GRA GRF,
@@ -1164,8 +1168,7 @@ main-begin-declare-builders (context-item IDT T none t\ context-item IDF (F t) n
     coq.env.end-module _]) (true),
   coq.env.begin-section Name,
   std.assert! (T = sort (typ _)) "The first context item must be a type variable",
-  coq.univ.new [] U,
-  Ty = sort (typ U),
+  coq.fresh-type Ty,
   coq.env.add-const IDT _ Ty tt tt C, % no body, local -> a variable
   TheType = global (const C),
   builders-postulate-factories IDF GRA GRF TheType [],
@@ -1223,8 +1226,7 @@ main-declare-asset (asset-parameter Name T Rest as R) D :- std.do! [
   if-verbose (coq.say "HB: postulate type" Name),
 
   std.assert! (T = sort (typ _)) "The first record parameter must be a type",
-  coq.univ.new [] U,
-  Ty = sort (typ U),
+  coq.fresh-type Ty,
   coq.env.add-const Name _ Ty tt tt C, % no body, local -> a variable
   TheType = global (const C),
   collect-asset-parameters (Rest TheType) [] Module TheType D