Merge pull request #1 from ecranceMERCE/update

update files + nix + header < 80char

.nix/config.nix

@@ -0,0 +1,102 @@
+{
+  ## DO NOT CHANGE THIS
+  format = "1.0.0";
+  ## unless you made an automated or manual update
+  ## to another supported format.
+
+  ## The attribute to build from the local sources,
+  ## either using nixpkgs data or the overlays located in `.nix/coq-overlays`
+  ## Will determine the default main-job of the bundles defined below
+  attribute = "trocq";
+
+  ## If you want to select a different attribute (to build from the local sources as well)
+  ## when calling `nix-shell` and `nix-build` without the `--argstr job` argument
+  # shell-attribute = "{{nix_name}}";
+
+  ## Maybe the shortname of the library is different from
+  ## the name of the nixpkgs attribute, if so, set it here:
+  # pname = "{{shortname}}";
+
+  ## Lists the dependencies, phrased in terms of nix attributes.
+  ## No need to list Coq, it is already included.
+  ## These dependencies will systematically be added to the currently
+  ## known dependencies, if any more than Coq.
+  ## /!\ Remove this field as soon as the package is available on nixpkgs.
+  ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then.
+  # buildInputs = [ ];
+
+  ## Indicate the relative location of your _CoqProject
+  ## If not specified, it defaults to "_CoqProject"
+  # coqproject = "_CoqProject";
+
+  ## select an entry to build in the following `bundles` set
+  ## defaults to "default"
+  default-bundle = "default";
+
+  ## write one `bundles.name` attribute set per
+  ## alternative configuration
+  ## When generating GitHub Action CI, one workflow file
+  ## will be created per bundle
+  bundles.default = {
+
+    ## You can override Coq and other Coq coqPackages
+    ## through the following attribute
+    coqPackages.coq.override.version = "8.17";
+    coqPackages.coq-elpi.override.version = "ecranceMERCE:strat";
+
+    ## In some cases, light overrides are not available/enough
+    ## in which case you can use either
+    # coqPackages.<coq-pkg>.overrideAttrs = o: <overrides>;
+    ## or a "long" overlay to put in `.nix/coq-overlays
+    ## you may use `nix-shell --run fetchOverlay <coq-pkg>`
+    ## to automatically retrieve the one from nixpkgs
+    ## if it exists and is correctly named/located
+
+    ## You can override Coq and other coqPackages
+    ## through the following attribute
+    ## If <ocaml-pkg> does not support light overrides,
+    ## you may use `overrideAttrs` or long overlays
+    ## located in `.nix/ocaml-overlays`
+    ## (there is no automation for this one)
+    #  ocamlPackages.<ocaml-pkg>.override.version = "x.xx";
+
+    ## You can also override packages from the nixpkgs toplevel
+    # <nix-pkg>.override.overrideAttrs = o: <overrides>;
+    ## Or put an overlay in `.nix/overlays`
+
+    ## you may mark a package as a main CI job (one to take deps and
+    ## rev deps from) as follows
+    # coqPackages.<main-pkg>.main-job = true;
+    ## by default the current package and its shell attributes are main jobs
+
+    ## you may mark a package as a CI job as follows
+    #  coqPackages.<another-pkg>.job = "test";
+    ## It can then built through
+    ## nix-build --argstr bundle "default" --arg job "test";
+    ## in the absence of such a directive, the job "another-pkg" will
+    ## is still available, but will be automatically included in the CI
+    ## via the command genNixActions only if it is a dependency or a
+    ## reverse dependency of a job flagged as "main-job" (see above).
+
+  };
+
+  ## Cachix caches to use in CI
+  ## Below we list some standard ones
+  cachix.coq = {};
+  cachix.math-comp = {};
+  cachix.coq-community = {};
+
+  ## If you have write access to one of these caches you can
+  ## provide the auth token or signing key through a secret
+  ## variable on GitHub. Then, you should give the variable
+  ## name here. For instance, coq-community projects can use
+  ## the following line instead of the one above:
+  # cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN";
+
+  ## Or if you have a signing key for a given Cachix cache:
+  # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY"
+
+  ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY
+  ## are the names of secret variables. They are set in
+  ## GitHub's web interface.
+}

.nix/coq-nix-toolbox.nix

@@ -0,0 +1 @@
+"f72eef6033e0abc9fa06f94fe718d8aa9c0d031a"

.nix/coq-overlays/HoTT/default.nix

@@ -0,0 +1,46 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+mkCoqDerivation {
+  pname = "HoTT";
+  repo = "Coq-HoTT";
+  owner = "HoTT";
+  inherit version;
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { case = range "8.14" "8.17"; out = coq.coq-version; }
+  ] null;
+  releaseRev = v: "V${v}";
+  release."8.14".sha256 = "sha256-7kXk2pmYsTNodHA+Qts3BoMsewvzmCbYvxw9Sgwyvq0=";
+  release."8.15".sha256 = "sha256-JfeiRZVnrjn3SQ87y6dj9DWNwCzrkK3HBogeZARUn9g=";
+  release."8.16".sha256 = "sha256-xcEbz4ZQ+U7mb0SEJopaczfoRc2GSgF2BGzUSWI0/HY=";
+  release."8.17".sha256 = "sha256-GjTUpzL9UzJm4C2ilCaYEufLG3hcj7rJPc5Op+OMal8=";
+
+  # versions of HoTT for Coq 8.17 and onwards will use dune
+  # opam-name = if lib.versions.isLe "8.17" coq.coq-version then "coq-hott" else null;
+  opam-name = "coq-hott";
+  useDune = lib.versions.isGe "8.17" coq.coq-version;
+
+  patchPhase = ''
+    patchShebangs etc
+  '';
+
+  meta = {
+    homepage = "https://homotopytypetheory.org/";
+    description = "The Homotopy Type Theory library";
+    longDescription = ''
+      Homotopy Type Theory is an interpretation of Martin-Löf’s intensional
+      type theory into abstract homotopy theory. Propositional equality is
+      interpreted as homotopy and type isomorphism as homotopy equivalence.
+      Logical constructions in type theory then correspond to
+      homotopy-invariant constructions on spaces, while theorems and even
+      proofs in the logical system inherit a homotopical meaning. As the
+      natural logic of homotopy, type theory is also related to higher
+      category theory as it is used e.g. in the notion of a higher topos.
+
+      The HoTT library is a development of homotopy-theoretic ideas in the Coq
+      proof assistant. It draws many ideas from Vladimir Voevodsky's
+      Foundations library (which has since been incorporated into the Unimath
+      library) and also cross-pollinates with the HoTT-Agda library.
+    '';
+    maintainers = with lib.maintainers; [ alizter siddharthist ];
+  };
+}

.nix/coq-overlays/coq-elpi/default.nix

@@ -0,0 +1,64 @@
+{ lib, mkCoqDerivation, which, coq, version ? null }:
+
+with builtins; with lib; let
+  elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [
+    { case = "8.11"; out = { version = "1.11.4"; };}
+    { case = "8.12"; out = { version = "1.12.0"; };}
+    { case = "8.13"; out = { version = "1.13.7"; };}
+    { case = "8.14"; out = { version = "1.13.7"; };}
+    { case = "8.15"; out = { version = "1.15.0"; };}
+    { case = "8.16"; out = { version = "1.16.5"; };}
+  ] {} );
+in mkCoqDerivation {
+  pname = "elpi";
+  repo  = "coq-elpi";
+  owner = "LPCIC";
+  inherit version;
+  defaultVersion = lib.switch coq.coq-version [
+    { case = "8.16"; out = "1.15.1"; }
+    { case = "8.15"; out = "1.14.0"; }
+    { case = "8.14"; out = "1.11.2"; }
+    { case = "8.13"; out = "1.11.1"; }
+    { case = "8.12"; out = "1.8.3_8.12"; }
+    { case = "8.11"; out = "1.6.3_8.11"; }
+  ] null;
+  release."1.15.1".sha256     = "sha256-NT2RlcIsFB9AvBhMxil4ZZIgx+KusMqDflj2HgQxsZg=";
+  release."1.14.0".sha256     = "sha256:1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp";
+  release."1.13.0".sha256     = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n";
+  release."1.12.1".sha256     = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY=";
+  release."1.11.2".sha256     = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4";
+  release."1.11.1".sha256     = "10j076vc2hdcbm15m6s7b6xdzibgfcbzlkgjnlkr2vv9k13qf8kc";
+  release."1.10.1".sha256     = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk";
+  release."1.9.7".sha256      = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1";
+  release."1.9.5".sha256      = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6";
+  release."1.9.4".sha256      = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq";
+  release."1.9.3".sha256      = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z";
+  release."1.9.2".sha256      = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07";
+  release."1.8.3_8.12".sha256  = "15z2l4zy0qpw0ws7bvsmpmyv543aqghrfnl48nlwzn9q0v89p557";
+  release."1.8.3_8.12".version = "1.8.3";
+  release."1.8.2_8.12".sha256  = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y";
+  release."1.8.2_8.12".version = "1.8.2";
+  release."1.8.1".sha256      = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r";
+  release."1.8.0".sha256      = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1";
+  release."1.7.0".sha256      = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8";
+  release."1.6.3_8.11".sha256 = "1j340cr2bv95clzzkkfmsjkklham1mj84cmiyprzwv20q89zr1hp";
+  release."1.6.3_8.11".version = "1.6.3";
+  release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn";
+  release."1.6.2_8.11".version = "1.6.2";
+  release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53";
+  release."1.6.1_8.11".version = "1.6.1";
+  release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq";
+  release."1.6.0_8.11".version = "1.6.0";
+  release."1.6.0".sha256      = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
+  releaseRev = v: "v${v}";
+
+  mlPlugin = true;
+  propagatedBuildInputs = [ elpi ];
+  buildPhase = "make build";
+
+  meta = {
+    description = "Coq plugin embedding ELPI.";
+    maintainers = [ maintainers.cohencyril ];
+    license = licenses.lgpl21Plus;
+  };
+}

.nix/coq-overlays/trocq/default.nix

@@ -0,0 +1,60 @@
+## File initially generated by createOverlay
+## and then supposedly modified manually.
+## Some hints for manual modifications are in the file,
+## but the full doc is on nixos / nix packages website:
+## https://nixos.org/manual/nixpkgs/stable/#sec-language-coq
+
+{ lib, mkCoqDerivation, which, coq, HoTT, coq-elpi
+  ## declare extra dependencies here, to be used in propagateBuildInputs e.g.
+  # , mathcomp, coq-elpi
+  , version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "trocq";
+  ## you can configure the domain, owner and repository, the default are:
+  # repo = "coq_modular_param";
+  # owner = "coq-community";
+  # domain = "github.com";
+
+  inherit version;
+## The `defaultVersion` attribute is important for nixpkgs but can be kept unchanged
+## for local usage since it will be ignored locally if
+## - this derivation corresponds to the main attribute,
+## - or its version is overridden (by a branch, PR, url or path) in `.nix/config.nix`.
+  defaultVersion = with versions; switch coq.coq-version [
+    ## Example of possible dependencies
+    # { case = range "8.13" "8.14"; out = "1.2.0"; }
+    ## other predicates are `isLe v`, `isLt v`, `isGe v`, `isGt v`, `isEq v` etc
+  ] null;
+
+  ## Declare existing releases
+  ## leave sha256 empty at first and then copy paste
+  ## the resulting sha given by the error message
+  # release."1.1.1".sha256 = "";
+  ## if the tag is not exactly the version number you can amend like this
+  # release."1.1.1".rev = "v1.1.1";
+  ## if a consistent scheme gives the tag from the release number, you can do like this:
+  # releaseRev = v: "v${v}";
+
+  ## Add dependencies in here. In particular you can add
+  ## - arbitrary nix packages (you need to require them at the beginning of the file)
+  ## - Coq packages (require them at the beginning of the file)
+  ## - OCaml packages (use `coq.ocamlPackages.xxx`, no need to require them at the beginning of the file)
+  propagatedBuildInputs = [ HoTT coq-elpi ]; ## e.g. `= [ mathcomp coq-elpi ]`
+
+  ## Does the package contain OCaml code?
+  mlPlugin = true;
+
+  ## Give some meta data
+  ## This is needed for submitting the package to nixpkgs but not required for local use.
+  meta = {
+    ## Describe your package in one sentence
+    # description = "";
+    ## Kindly ask one of these people if they want to be an official maintainer.
+    ## (You might also consider adding yourself to the list of maintainers)
+    # maintainers = with maintainers; [ cohencyril siraben vbgl Zimmi48 ];
+    ## Pick a license from
+    ## https://github.com/NixOS/nixpkgs/blob/master/lib/licenses.nix
+    # license = licenses.mit;
+  };
+}

_CoqProject

@@ -12,7 +12,11 @@ theories/Param_arrow.v
 theories/Database.v
 theories/Param.v
 theories/Trocq.v
+theories/Vernac.v
 theories/Param_paths.v
+theories/Param_sigma.v
+theories/Param_prod.v
+theories/Param_option.v
 
 examples/Example.v
 examples/int_to_Zp.v

default.nix

@@ -0,0 +1,12 @@
+{ config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false,
+  update-nixpkgs ? false, ci-matrix ? false,
+  override ? {}, ocaml-override ? {}, global-override ? {},
+  bundle ? null, job ? null, inNixShell ? null, src ? ./.,
+}@args:
+let auto = fetchGit {
+  url = "https://github.com/coq-community/coq-nix-toolbox.git";
+  ref = "master";
+  rev = import .nix/coq-nix-toolbox.nix;
+};
+in
+import auto ({inherit src;} // args)

elpi/annot.elpi

@@ -1,19 +1,18 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                            %                                Trocq                                %
-%  _______                   %                       Copyright (C) 2023 MERCE                      %
-% |__   __|                  %                (Mitsubishi Electric R&D Centre Europe)              %
-%    | |_ __ ___   ___ __ _  %                   Cyril Cohen <[email protected]>                %
-%    | | '__/ _ \ / __/ _` | %                   Enzo Crance <[email protected]>                %
-%    | | | | (_) | (_| (_| | %               Assia Mahboubi <[email protected]>              %
-%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%                        | | %            This file is distributed under the terms of the          %
-%                        |_| %              GNU Lesser General Public License Version 3            %
-%                            %             (see LICENSE file for the text of the license)          %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-% --------------------------------------------------------------------------------------------------
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                            %                     Trocq                      %
+%  _______                   %            Copyright (C) 2023 MERCE            %
+% |__   __|                  %     (Mitsubishi Electric R&D Centre Europe)    %
+%    | |_ __ ___   ___ __ _  %        Cyril Cohen <[email protected]>      %
+%    | | '__/ _ \ / __/ _` | %        Enzo Crance <[email protected]>      %
+%    | | | | (_) | (_| (_| | %    Assia Mahboubi <[email protected]>    %
+%    |_|_|  \___/ \___\__, | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%                        | | %   This file is distributed under the terms of  %
+%                        |_| %   GNU Lesser General Public License Version 3  %
+%                            % (see LICENSE file for the text of the license) %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% -----------------------------------------------------------------------------
 % annotated type theory
-% --------------------------------------------------------------------------------------------------
+% -----------------------------------------------------------------------------
 
 % this allows to easily make sure an application is beta-reduced
 :before "subst-fun:fail"
@@ -23,7 +22,7 @@ coq.subst-fun Args F FArgs :- !, coq.mk-app F Args FArgs.
 % NB: the output type is term because the annotations are encoded directly in Coq
 % see PType in Param.v
 pred term->annot-term i:term, o:term.
-term->annot-term (sort (typ U)) (app [pglobal (const PType) UI, M, N]) :- param.db.ptype PType, !,
+term->annot-term (sort (typ U)) (app [pglobal (const PType) UI, M, N]) :- trocq.db.ptype PType, !,
   coq.univ-instance UI [{coq.univ.variable U}],
   cstr.univ-link _ M N.
 term->annot-term (fun N T F) (fun N T' F') :- !,
@@ -57,7 +56,7 @@ typecheck T ATy :-
 pred sub-type i:term, i:term.
 % SubUniv
 sub-type (app [pglobal (const PType) _, M1, N1]) (app [pglobal (const PType) _, M2, N2]) :-
-  param.db.ptype PType, !,
+  trocq.db.ptype PType, !,
   cstr.univ-link C1 M1 N1,
   cstr.univ-link C2 M2 N2,
   cstr.geq C1 C2.
@@ -79,7 +78,7 @@ sub-type X _ :- coq.error "annot.sub-type:" X.
 % syntactic term equality, taking care of adding annotation equalities in the constraint graph
 pred eq i:term, i:term.
 eq (app [pglobal (const PType) UI, M1, N1]) (app [pglobal (const PType) UI, M2, N2]) :-
-  param.db.ptype PType, !,
+  trocq.db.ptype PType, !,
   cstr.univ-link C1 M1 N1,
   cstr.univ-link C2 M2 N2,
   cstr.eq C1 C2.
@@ -109,7 +108,7 @@ classes T Cs' Out :-
   ).
 
 pred all-classes i:term, o:list param-class.
-all-classes (app [pglobal (const PType) _, M, N]) [C] :- param.db.ptype PType, !,
+all-classes (app [pglobal (const PType) _, M, N]) [C] :- trocq.db.ptype PType, !,
   cstr.univ-link C M N.
 all-classes X Cs :- (X = prod _ T F ; X = fun _ T F), !,
   pi x\ std.append {all-classes T} {all-classes (F x)} Cs.
@@ -119,7 +118,7 @@ all-classes X [] :- (name X ; X = global _ ; X = pglobal _ _), !.
 all-classes X _ :- coq.error "all-classes:" X.
 
 pred out-class i:term, o:option param-class.
-out-class (app [pglobal (const PType) _, M, N]) (some C) :- param.db.ptype PType, !,
+out-class (app [pglobal (const PType) _, M, N]) (some C) :- trocq.db.ptype PType, !,
   cstr.univ-link C M N.
 out-class (prod _ _ F) Out :- !, pi x\ out-class (F x) Out.
 out-class (fun _ _ _) none :- !.