diff options
-rw-r--r-- | .circleci/config.yml | 2 | ||||
-rw-r--r-- | .gitlab-ci.yml | 21 | ||||
-rw-r--r-- | default.nix | 80 | ||||
-rw-r--r-- | dev/ci/ci-common.sh | 2 | ||||
-rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 10 | ||||
-rw-r--r-- | dev/doc/changes.md | 83 | ||||
-rw-r--r-- | doc/sphinx/language/cic.rst | 231 | ||||
-rw-r--r-- | grammar/coqpp_ast.mli | 21 | ||||
-rw-r--r-- | grammar/coqpp_lex.mll | 4 | ||||
-rw-r--r-- | grammar/coqpp_main.ml | 237 | ||||
-rw-r--r-- | grammar/coqpp_parse.mly | 76 | ||||
-rw-r--r-- | grammar/tacextend.mlp | 9 | ||||
-rw-r--r-- | plugins/btauto/g_btauto.mlg (renamed from plugins/btauto/g_btauto.ml4) | 6 | ||||
-rw-r--r-- | plugins/cc/g_congruence.mlg (renamed from plugins/cc/g_congruence.ml4) | 14 | ||||
-rw-r--r-- | plugins/fourier/g_fourier.mlg (renamed from plugins/fourier/g_fourier.ml4) | 6 | ||||
-rw-r--r-- | plugins/ltac/coretactics.mlg (renamed from plugins/ltac/coretactics.ml4) | 184 | ||||
-rw-r--r-- | plugins/ltac/g_eqdecide.mlg (renamed from plugins/ltac/g_eqdecide.ml4) | 8 | ||||
-rw-r--r-- | plugins/ltac/tacentries.ml | 30 | ||||
-rw-r--r-- | plugins/ltac/tacentries.mli | 4 | ||||
-rw-r--r-- | plugins/micromega/g_micromega.mlg (renamed from plugins/micromega/g_micromega.ml4) | 38 | ||||
-rw-r--r-- | plugins/nsatz/g_nsatz.mlg (renamed from plugins/nsatz/g_nsatz.ml4) | 6 | ||||
-rw-r--r-- | plugins/omega/g_omega.mlg (renamed from plugins/omega/g_omega.ml4) | 9 | ||||
-rw-r--r-- | plugins/quote/g_quote.mlg (renamed from plugins/quote/g_quote.ml4) | 16 | ||||
-rw-r--r-- | plugins/romega/g_romega.mlg (renamed from plugins/romega/g_romega.ml4) | 12 | ||||
-rw-r--r-- | plugins/rtauto/g_rtauto.mlg (renamed from plugins/rtauto/g_rtauto.ml4) | 5 | ||||
-rw-r--r-- | pretyping/nativenorm.ml | 39 | ||||
-rw-r--r-- | pretyping/vnorm.ml | 37 | ||||
-rw-r--r-- | shell.nix | 4 | ||||
-rw-r--r-- | tools/CoqMakefile.in | 10 |
29 files changed, 736 insertions, 468 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 03aeed2eb..950674b34 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -11,7 +11,7 @@ defaults: - image: $CI_REGISTRY_IMAGE:$CACHEKEY environment: &envvars - CACHEKEY: "bionic_coq-V2018-06-13-V1" + CACHEKEY: "bionic_coq-V2018-07-02-V4" CI_REGISTRY_IMAGE: registry.gitlab.com/coq/coq version: 2 diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 4e159ebdc..773a89a46 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-06-13-V1" + CACHEKEY: "bionic_coq-V2018-07-02-V4" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -45,6 +45,9 @@ before_script: - opam list - opam config list +after_script: + - echo "The build completed normally (not a runner failure)." + ################ GITLAB CACHING ###################### # - use artifacts between jobs # ###################################################### @@ -233,6 +236,22 @@ windows32: variables: ARCH: "32" +pkg:nix: + image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git + stage: test + variables: + GIT_STRATEGY: none + dependencies: [] # We don't need to download build artifacts + before_script: [] # We don't want to use the shared 'before_script' + script: + - export TMPDIR=$PWD + - nix-build "$CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz" -K + artifacts: + name: "$CI_JOB_NAME.logs" + when: on_failure + paths: + - nix-build-coq.drv-0/*/test-suite/logs + warnings:base: <<: *warnings-template diff --git a/default.nix b/default.nix index a2645f4fc..1be274081 100644 --- a/default.nix +++ b/default.nix @@ -9,23 +9,27 @@ # nix-shell supports the --arg option (see Nix doc) that allows you for # instance to do this: -# $ nix-shell --arg ocamlPackages "(import <nixpkgs> {}).ocamlPackages_latest" --arg buildIde false +# $ nix-shell --arg ocamlPackages "(import <nixpkgs> {}).ocaml-ng.ocamlPackages_4_05" --arg buildIde false # You can also compile Coq and "install" it by running: # $ make clean # (only needed if you have left-over compilation files) # $ nix-build # at the root of the Coq repository. # nix-build also supports the --arg option, so you will be able to do: -# $ nix-build --arg doCheck false +# $ nix-build --arg doInstallCheck false # if you want to speed up things by not running the test-suite. # Once the build is finished, you will find, in the current directory, # a symlink to where Coq was installed. -{ pkgs ? (import <nixpkgs> {}) +{ pkgs ? + (import (fetchTarball { + url = "https://github.com/NixOS/nixpkgs/archive/060a98e9f4ad879492e48d63e887b0b6db26299e.tar.gz"; + sha256 = "1lzvp3md0hf6kp2bvc6dbzh40navlyd51qlns9wbkz6lqk3lgf6j"; + }) {}) , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06 , buildIde ? true , buildDoc ? true -, doCheck ? true +, doInstallCheck ? true }: with pkgs; @@ -36,64 +40,50 @@ stdenv.mkDerivation rec { name = "coq"; buildInputs = [ - - # Coq dependencies hostname - ] ++ (with ocamlPackages; [ - ocaml - findlib - camlp5_strict - num - - ]) ++ (if buildIde then [ - - # CoqIDE dependencies - ocamlPackages.lablgtk - - ] else []) ++ (if buildDoc then [ - + python2 time # coq-makefile timing tools + ] + ++ (with ocamlPackages; [ ocaml findlib camlp5_strict num ]) + ++ optional buildIde ocamlPackages.lablgtk + ++ optionals buildDoc [ # Sphinx doc dependencies pkgconfig (python3.withPackages (ps: [ ps.sphinx ps.sphinx_rtd_theme ps.pexpect ps.beautifulsoup4 ps.antlr4-python3-runtime ps.sphinxcontrib-bibtex ])) - antlr4 - - ] else []) ++ (if doCheck then - + antlr4 + ] + ++ optionals doInstallCheck ( # Test-suite dependencies # ncurses is required to build an OCaml REPL optional (!versionAtLeast ocaml.version "4.07") ncurses - ++ [ - python - rsync - which - ocamlPackages.ounit - - ] else []) ++ (if lib.inNixShell then [ - ocamlPackages.merlin - ocamlPackages.ocp-indent - ocamlPackages.ocp-index - - # Dependencies of the merging script - jq - curl - git - gnupg - - ] else []); + ++ [ ocamlPackages.ounit rsync which ] + ) + ++ optionals lib.inNixShell ( + [ jq curl git gnupg ] # Dependencies of the merging script + ++ (with ocamlPackages; [ merlin ocp-indent ocp-index ]) # Dev tools + ); src = if lib.inNixShell then null else with builtins; filterSource - (path: _: !elem (baseNameOf path) [".git" "result" "bin"]) ./.; + (path: _: + !elem (baseNameOf path) [".git" "result" "bin" "_build_ci"]) ./.; prefixKey = "-prefix "; - buildFlags = [ "world" ] ++ optional buildDoc "doc-html"; + buildFlags = [ "world" "byte" ] ++ optional buildDoc "doc-html"; + + installTargets = + [ "install" "install-byte" ] ++ optional buildDoc "install-doc-html"; + + inherit doInstallCheck; - installTargets = [ "install" ] ++ optional buildDoc "install-doc-html"; + preInstallCheck = '' + patchShebangs tools/ + patchShebangs test-suite/ + ''; - inherit doCheck; + installCheckTarget = [ "check" ]; } diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 85df249d3..a68cd0933 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -69,7 +69,7 @@ git_checkout() if [ ! -d .git ] ; then git clone "${_DEPTH[@]}" "${_URL}" . ; fi && \ echo "Checking out ${_DEST}" && \ git fetch "${_URL}" "${_BRANCH}" && \ - git checkout "${_COMMIT}" && \ + git -c advice.detachedHead=false checkout "${_COMMIT}" && \ echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" ) } diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 52f851917..a4ee6a379 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-06-13-V1" +# CACHEKEY: "bionic_coq-V2018-07-02-V4" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -6,10 +6,12 @@ LABEL maintainer="e@x80.org" ENV DEBIAN_FRONTEND="noninteractive" -RUN apt-get update -qq && apt-get install -y -qq m4 wget time gcc-multilib opam \ +RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ + m4 automake autoconf time wget rsync git gcc-multilib opam \ libgtk2.0-dev libgtksourceview2.0-dev \ - texlive-latex-extra texlive-fonts-recommended texlive-science \ - python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip + texlive-latex-extra texlive-fonts-recommended texlive-science tipa \ + python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex \ + python3-setuptools python3-wheel python3-pip RUN pip3 install antlr4-python3-runtime diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 4177513a1..6d5023405 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -95,19 +95,73 @@ Primitive number parsers ### Transitioning away from Camlp5 -In an effort to reduce dependency on Camlp5, the use of Camlp5 GEXTEND macro -is discouraged. Most plugin writers do not need this low-level interface, but -for those who do, the transition path is somewhat straightforward. To convert -a ml4 file containing only standard OCaml with GEXTEND statements, the following -should be enough: -- replace its "ml4" extension with "mlg" -- replace GEXTEND with GRAMMAR EXTEND -- wrap every occurrence of OCaml code into braces { } +In an effort to reduce dependency on camlp5, the use of several grammar macros +is discouraged. Coq is now shipped with its own preprocessor, called coqpp, +which serves the same purpose as camlp5. + +To perform the transition to coqpp macros, one first needs to change the +extension of a macro file from `.ml4` to `.mlg`. Not all camlp5 macros are +handled yet. + +Due to parsing constraints, the syntax of the macros is slightly different, but +updating the source code is mostly a matter of straightforward +search-and-replace. The main differences are summarized below. + +#### OCaml code + +Every piece of toplevel OCaml code needs to be wrapped into braces. For instance, code of the form ``` let myval = 0 +``` +should be turned into +``` +{ +let myval = 0 +} +``` + +#### TACTIC EXTEND + +Steps to perform: +- replace the brackets enclosing OCaml code in actions with braces +- if not there yet, add a leading `|̀ to the first rule + +For instance, code of the form: +``` +TACTIC EXTEND my_tac + [ "tac1" int_or_var(i) tactic(t) ] -> [ mytac1 ist i t ] +| [ "tac2" tactic(t) ] -> [ mytac2 t ] +END +``` +should be turned into +``` +TACTIC EXTEND my_tac +| [ "tac1" int_or_var(i) tactic(t) ] -> { mytac1 ist i t } +| [ "tac2" tactic(t) ] -> { mytac2 t } +END +``` + +#### VERNAC EXTEND + +Not handled yet. + +#### ARGUMENT EXTEND + +Not handled yet. + +#### GEXTEND +Most plugin writers do not need this low-level interface, but for the sake of +completeness we document it. + +Steps to perform are: +- replace GEXTEND with GRAMMAR EXTEND +- wrap every occurrence of OCaml code in actions into braces { } + +For instance, code of the form +``` GEXTEND Gram GLOBAL: my_entry; @@ -119,10 +173,6 @@ END ``` should be turned into ``` -{ -let myval = 0 -} - GRAMMAR EXTEND Gram GLOBAL: my_entry; @@ -133,9 +183,12 @@ my_entry: END ``` -Currently mlg files can only contain GRAMMAR EXTEND statements. They do not -support TACTIC, VERNAC nor ARGUMENT EXTEND. In case you have a file containing -both kinds at the same time, it is recommended splitting it in two. +Caveats: +- No `GLOBAL` entries mean that they are all local, while camlp5 special-cases + this as a shorthand for all global entries. Solution: always define a `GLOBAL` + section. +- No complex patterns allowed in token naming. Solution: match on it inside the + OCaml quotation. ## Changes between Coq 8.7 and Coq 8.8 diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index f6bab0267..b01a4ef0f 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -721,67 +721,68 @@ called the *context of parameters*. Furthermore, we must have that each :math:`T` in :math:`(t:T)∈Γ_I` can be written as: :math:`∀Γ_P,∀Γ_{\mathit{Arr}(t)}, S` where :math:`Γ_{\mathit{Arr}(t)}` is called the *Arity* of the inductive type t and :math:`S` is called the sort of the inductive type t (not to be confused with :math:`\Sort` which is the set of sorts). -** Examples** The declaration for parameterized lists is: - -.. math:: - \ind{1}{[\List:\Set→\Set]}{\left[\begin{array}{rcl} - \Nil & : & \forall A:\Set,\List~A \\ - \cons & : & \forall A:\Set, A→ \List~A→ \List~A - \end{array} - \right]} - -which corresponds to the result of the |Coq| declaration: .. example:: - .. coqtop:: in - - Inductive list (A:Set) : Set := - | nil : list A - | cons : A -> list A -> list A. + The declaration for parameterized lists is: -The declaration for a mutual inductive definition of tree and forest -is: + .. math:: + \ind{1}{[\List:\Set→\Set]}{\left[\begin{array}{rcl} + \Nil & : & \forall A:\Set,\List~A \\ + \cons & : & \forall A:\Set, A→ \List~A→ \List~A + \end{array} + \right]} -.. math:: - \ind{~}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} - {\left[\begin{array}{rcl} - \node &:& \forest → \tree\\ - \emptyf &:& \forest\\ - \consf &:& \tree → \forest → \forest\\ - \end{array}\right]} + which corresponds to the result of the |Coq| declaration: -which corresponds to the result of the |Coq| declaration: + .. coqtop:: in + + Inductive list (A:Set) : Set := + | nil : list A + | cons : A -> list A -> list A. .. example:: - .. coqtop:: in + The declaration for a mutual inductive definition of tree and forest + is: - Inductive tree : Set := - | node : forest -> tree - with forest : Set := - | emptyf : forest - | consf : tree -> forest -> forest. + .. math:: + \ind{~}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} + {\left[\begin{array}{rcl} + \node &:& \forest → \tree\\ + \emptyf &:& \forest\\ + \consf &:& \tree → \forest → \forest\\ + \end{array}\right]} -The declaration for a mutual inductive definition of even and odd is: + which corresponds to the result of the |Coq| declaration: -.. math:: - \ind{1}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ - \odd&:&\nat → \Prop \end{array}\right]} - {\left[\begin{array}{rcl} - \evenO &:& \even~0\\ - \evenS &:& \forall n, \odd~n -> \even~(\kw{S}~n)\\ - \oddS &:& \forall n, \even~n -> \odd~(\kw{S}~n) - \end{array}\right]} + .. coqtop:: in -which corresponds to the result of the |Coq| declaration: + Inductive tree : Set := + | node : forest -> tree + with forest : Set := + | emptyf : forest + | consf : tree -> forest -> forest. .. example:: - .. coqtop:: in + The declaration for a mutual inductive definition of even and odd is: + + .. math:: + \ind{1}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ + \odd&:&\nat → \Prop \end{array}\right]} + {\left[\begin{array}{rcl} + \evenO &:& \even~0\\ + \evenS &:& \forall n, \odd~n -> \even~(\kw{S}~n)\\ + \oddS &:& \forall n, \even~n -> \odd~(\kw{S}~n) + \end{array}\right]} + + which corresponds to the result of the |Coq| declaration: - Inductive even : nat -> prop := - | even_O : even 0 - | even_S : forall n, odd n -> even (S n) - with odd : nat -> prop := - | odd_S : forall n, even n -> odd (S n). + .. coqtop:: in + + Inductive even : nat -> prop := + | even_O : even 0 + | even_S : forall n, odd n -> even (S n) + with odd : nat -> prop := + | odd_S : forall n, even n -> odd (S n). @@ -838,8 +839,8 @@ rules, we need a few definitions: Arity of a given sort +++++++++++++++++++++ -A type :math:`T` is an *arity of sort s* if it converts to the sort s or to a -product :math:`∀ x:T,U` with :math:`U` an arity of sort s. +A type :math:`T` is an *arity of sort* :math:`s` if it converts to the sort :math:`s` or to a +product :math:`∀ x:T,U` with :math:`U` an arity of sort :math:`s`. .. example:: @@ -850,7 +851,7 @@ product :math:`∀ x:T,U` with :math:`U` an arity of sort s. Arity +++++ A type :math:`T` is an *arity* if there is a :math:`s∈ \Sort` such that :math:`T` is an arity of -sort s. +sort :math:`s`. .. example:: @@ -921,29 +922,29 @@ condition* for a constant :math:`X` in the following cases: For instance, if one considers the following variant of a tree type branching over the natural numbers: - .. coqtop:: in + .. coqtop:: in - Inductive nattree (A:Type) : Type := - | leaf : nattree A - | node : A -> (nat -> nattree A) -> nattree A. - End TreeExample. - - Then every instantiated constructor of ``nattree A`` satisfies the nested positivity - condition for ``nattree``: + Inductive nattree (A:Type) : Type := + | leaf : nattree A + | node : A -> (nat -> nattree A) -> nattree A. + End TreeExample. + + Then every instantiated constructor of ``nattree A`` satisfies the nested positivity + condition for ``nattree``: - + Type ``nattree A`` of constructor ``leaf`` satisfies the positivity condition for - ``nattree`` because ``nattree`` does not appear in any (real) arguments of the - type of that constructor (primarily because ``nattree`` does not have any (real) - arguments) ... (bullet 1) + + Type ``nattree A`` of constructor ``leaf`` satisfies the positivity condition for + ``nattree`` because ``nattree`` does not appear in any (real) arguments of the + type of that constructor (primarily because ``nattree`` does not have any (real) + arguments) ... (bullet 1) - + Type ``A → (nat → nattree A) → nattree A`` of constructor ``node`` satisfies the - positivity condition for ``nattree`` because: + + Type ``A → (nat → nattree A) → nattree A`` of constructor ``node`` satisfies the + positivity condition for ``nattree`` because: - - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 3) + - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 3) - - ``nattree`` occurs only strictly positively in ``nat → nattree A`` ... (bullet 3 + 2) + - ``nattree`` occurs only strictly positively in ``nat → nattree A`` ... (bullet 3 + 2) - - ``nattree`` satisfies the positivity condition for ``nattree A`` ... (bullet 1) + - ``nattree`` satisfies the positivity condition for ``nattree A`` ... (bullet 1) .. _Correctness-rules: @@ -978,35 +979,33 @@ provided that the following side conditions hold: One can remark that there is a constraint between the sort of the arity of the inductive type and the sort of the type of its constructors which will always be satisfied for the impredicative -sortProp but may fail to define inductive definition on sort Set and +sort :math:`\Prop` but may fail to define inductive definition on sort :math:`\Set` and generate constraints between universes for inductive definitions in the Type hierarchy. -**Examples**. It is well known that the existential quantifier can be encoded as an -inductive definition. The following declaration introduces the second- -order existential quantifier :math:`∃ X.P(X)`. - .. example:: + It is well known that the existential quantifier can be encoded as an + inductive definition. The following declaration introduces the second- + order existential quantifier :math:`∃ X.P(X)`. + .. coqtop:: in - + Inductive exProp (P:Prop->Prop) : Prop := | exP_intro : forall X:Prop, P X -> exProp P. -The same definition on Set is not allowed and fails: + The same definition on :math:`\Set` is not allowed and fails: -.. example:: .. coqtop:: all Fail Inductive exSet (P:Set->Prop) : Set := exS_intro : forall X:Set, P X -> exSet P. -It is possible to declare the same inductive definition in the -universe Type. The exType inductive definition has type -:math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT_intro}` -has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`. + It is possible to declare the same inductive definition in the + universe :math:`\Type`. The :g:`exType` inductive definition has type + :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT_intro}` + has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`. -.. example:: .. coqtop:: all Inductive exType (P:Type->Prop) : Type := @@ -1019,9 +1018,9 @@ has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`. Template polymorphism +++++++++++++++++++++ -Inductive types declared in Type are polymorphic over their arguments -in Type. If :math:`A` is an arity of some sort and s is a sort, we write :math:`A_{/s}` -for the arity obtained from :math:`A` by replacing its sort with s. +Inductive types declared in :math:`\Type` are polymorphic over their arguments +in :math:`\Type`. If :math:`A` is an arity of some sort and math:`s` is a sort, we write :math:`A_{/s}` +for the arity obtained from :math:`A` by replacing its sort with :math:`s`. Especially, if :math:`A` is well-typed in some global environment and local context, then :math:`A_{/s}` is typable by typability of all products in the Calculus of Inductive Constructions. The following typing rule is @@ -1382,7 +1381,7 @@ this type. [I:Prop|I→ s] A *singleton definition* has only one constructor and all the -arguments of this constructor have type Prop. In that case, there is a +arguments of this constructor have type :math:`\Prop`. In that case, there is a canonical way to interpret the informative extraction on an object in that type, such that the elimination on any sort :math:`s` is legal. Typical examples are the conjunction of non-informative propositions and the @@ -1421,45 +1420,45 @@ corresponding to the :math:`c:C` constructor. We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math:`c`. -**Example.** -The following term in concrete syntax:: +.. example:: + The following term in concrete syntax:: - match t as l return P' with - | nil _ => t1 - | cons _ hd tl => t2 - end + match t as l return P' with + | nil _ => t1 + | cons _ hd tl => t2 + end -can be represented in abstract syntax as + can be represented in abstract syntax as -.. math:: - \case(t,P,f 1 | f 2 ) + .. math:: + \case(t,P,f 1 | f 2 ) -where + where -.. math:: - \begin{eqnarray*} - P & = & \lambda~l~.~P^\prime\\ - f_1 & = & t_1\\ - f_2 & = & \lambda~(hd:\nat)~.~\lambda~(tl:\List~\nat)~.~t_2 - \end{eqnarray*} + .. math:: + \begin{eqnarray*} + P & = & \lambda~l~.~P^\prime\\ + f_1 & = & t_1\\ + f_2 & = & \lambda~(hd:\nat)~.~\lambda~(tl:\List~\nat)~.~t_2 + \end{eqnarray*} -According to the definition: + According to the definition: -.. math:: - \{(\kw{nil}~\nat)\}^P ≡ \{(\kw{nil}~\nat) : (\List~\nat)\}^P ≡ (P~(\kw{nil}~\nat)) + .. math:: + \{(\kw{nil}~\nat)\}^P ≡ \{(\kw{nil}~\nat) : (\List~\nat)\}^P ≡ (P~(\kw{nil}~\nat)) -.. math:: - - \begin{array}{rl} - \{(\kw{cons}~\nat)\}^P & ≡\{(\kw{cons}~\nat) : (\nat→\List~\nat→\List~\nat)\}^P \\ - & ≡∀ n:\nat, \{(\kw{cons}~\nat~n) : \List~\nat→\List~\nat)\}^P \\ - & ≡∀ n:\nat, ∀ l:\List~\nat, \{(\kw{cons}~\nat~n~l) : \List~\nat)\}^P \\ - & ≡∀ n:\nat, ∀ l:\List~\nat,(P~(\kw{cons}~\nat~n~l)). - \end{array} + .. math:: + + \begin{array}{rl} + \{(\kw{cons}~\nat)\}^P & ≡\{(\kw{cons}~\nat) : (\nat→\List~\nat→\List~\nat)\}^P \\ + & ≡∀ n:\nat, \{(\kw{cons}~\nat~n) : \List~\nat→\List~\nat)\}^P \\ + & ≡∀ n:\nat, ∀ l:\List~\nat, \{(\kw{cons}~\nat~n~l) : \List~\nat)\}^P \\ + & ≡∀ n:\nat, ∀ l:\List~\nat,(P~(\kw{cons}~\nat~n~l)). + \end{array} -Given some :math:`P` then :math:`\{(\kw{nil}~\nat)\}^P` represents the expected type of :math:`f_1` , -and :math:`\{(\kw{cons}~\nat)\}^P` represents the expected type of :math:`f_2`. + Given some :math:`P` then :math:`\{(\kw{nil}~\nat)\}^P` represents the expected type of :math:`f_1` , + and :math:`\{(\kw{cons}~\nat)\}^P` represents the expected type of :math:`f_2`. .. _Typing-rule: @@ -1819,7 +1818,7 @@ while it will type-check, if one uses instead the `coqtop` ``-impredicative-set`` option.. The major change in the theory concerns the rule for product formation -in the sort Set, which is extended to a domain in any sort: +in the sort :math:`\Set`, which is extended to a domain in any sort: .. inference:: ProdImp @@ -1832,11 +1831,11 @@ in the sort Set, which is extended to a domain in any sort: This extension has consequences on the inductive definitions which are allowed. In the impredicative system, one can build so-called *large inductive definitions* like the example of second-order existential -quantifier (exSet). +quantifier (:g:`exSet`). There should be restrictions on the eliminations which can be performed on such definitions. The eliminations rules in the -impredicative system for sort Set become: +impredicative system for sort :math:`\Set` become: diff --git a/grammar/coqpp_ast.mli b/grammar/coqpp_ast.mli index 245e530ae..39b4d2ab3 100644 --- a/grammar/coqpp_ast.mli +++ b/grammar/coqpp_ast.mli @@ -13,14 +13,22 @@ type loc = { type code = { code : string } +type user_symbol = +| Ulist1 of user_symbol +| Ulist1sep of user_symbol * string +| Ulist0 of user_symbol +| Ulist0sep of user_symbol * string +| Uopt of user_symbol +| Uentry of string +| Uentryl of string * int + type token_data = | TokNone | TokName of string -| TokNameSep of string * string type ext_token = | ExtTerminal of string -| ExtNonTerminal of string * token_data +| ExtNonTerminal of user_symbol * token_data type tactic_rule = { tac_toks : ext_token list; @@ -70,11 +78,18 @@ type grammar_ext = { gramext_entries : grammar_entry list; } +type tactic_ext = { + tacext_name : string; + tacext_level : int option; + tacext_rules : tactic_rule list; +} + type node = | Code of code | Comment of string +| DeclarePlugin of string | GramExt of grammar_ext | VernacExt -| TacticExt of string * tactic_rule list +| TacticExt of tactic_ext type t = node list diff --git a/grammar/coqpp_lex.mll b/grammar/coqpp_lex.mll index f35766b16..6c6562c20 100644 --- a/grammar/coqpp_lex.mll +++ b/grammar/coqpp_lex.mll @@ -83,6 +83,7 @@ let alphanum = ['_' 'a'-'z' 'A'-'Z' '0'-'9' '\''] let ident = letterlike alphanum* let qualid = ident ('.' ident)* let space = [' ' '\t' '\r'] +let number = [ '0'-'9' ] rule extend = parse | "(*" { start_comment (); comment lexbuf } @@ -92,6 +93,8 @@ rule extend = parse | "TACTIC" { TACTIC } | "EXTEND" { EXTEND } | "END" { END } +| "DECLARE" { DECLARE } +| "PLUGIN" { PLUGIN } (** Camlp5 specific keywords *) | "GLOBAL" { GLOBAL } | "FIRST" { FIRST } @@ -105,6 +108,7 @@ rule extend = parse (** Standard *) | ident { IDENT (Lexing.lexeme lexbuf) } | qualid { QUALID (Lexing.lexeme lexbuf) } +| number { INT (int_of_string (Lexing.lexeme lexbuf)) } | space { extend lexbuf } | '\"' { string lexbuf } | '\n' { newline lexbuf; extend lexbuf } diff --git a/grammar/coqpp_main.ml b/grammar/coqpp_main.ml index 23a5104e2..ef591bc99 100644 --- a/grammar/coqpp_main.ml +++ b/grammar/coqpp_main.ml @@ -55,6 +55,8 @@ let string_split s = in if len == 0 then [] else split 0 +let plugin_name = "__coq_plugin_name" + module GramExt : sig @@ -82,42 +84,42 @@ let get_local_entries ext = in uniquize StringSet.empty local -let print_local chan ext = +let print_local fmt ext = let locals = get_local_entries ext in match locals with | [] -> () | e :: locals -> - let mk_e chan e = fprintf chan "%s.Entry.create \"%s\"" ext.gramext_name e in - let () = fprintf chan "@[<hv 2>let %s =@ @[%a@]@]@ " e mk_e e in - let iter e = fprintf chan "@[<hv 2>and %s =@ @[%a@]@]@ " e mk_e e in + let mk_e fmt e = fprintf fmt "%s.Entry.create \"%s\"" ext.gramext_name e in + let () = fprintf fmt "@[<hv 2>let %s =@ @[%a@]@]@ " e mk_e e in + let iter e = fprintf fmt "@[<hv 2>and %s =@ @[%a@]@]@ " e mk_e e in let () = List.iter iter locals in - fprintf chan "in@ " + fprintf fmt "in@ " -let print_string chan s = fprintf chan "\"%s\"" s +let print_string fmt s = fprintf fmt "\"%s\"" s -let print_list chan pr l = - let rec prl chan = function +let print_list fmt pr l = + let rec prl fmt = function | [] -> () - | [x] -> fprintf chan "%a" pr x - | x :: l -> fprintf chan "%a;@ %a" pr x prl l + | [x] -> fprintf fmt "%a" pr x + | x :: l -> fprintf fmt "%a;@ %a" pr x prl l in - fprintf chan "@[<hv>[%a]@]" prl l + fprintf fmt "@[<hv>[%a]@]" prl l -let print_opt chan pr = function -| None -> fprintf chan "None" -| Some x -> fprintf chan "Some@ (%a)" pr x +let print_opt fmt pr = function +| None -> fprintf fmt "None" +| Some x -> fprintf fmt "Some@ (%a)" pr x -let print_position chan pos = match pos with -| First -> fprintf chan "Extend.First" -| Last -> fprintf chan "Extend.Last" -| Before s -> fprintf chan "Extend.Before@ \"%s\"" s -| After s -> fprintf chan "Extend.After@ \"%s\"" s -| Level s -> fprintf chan "Extend.Level@ \"%s\"" s +let print_position fmt pos = match pos with +| First -> fprintf fmt "Extend.First" +| Last -> fprintf fmt "Extend.Last" +| Before s -> fprintf fmt "Extend.Before@ \"%s\"" s +| After s -> fprintf fmt "Extend.After@ \"%s\"" s +| Level s -> fprintf fmt "Extend.Level@ \"%s\"" s -let print_assoc chan = function -| LeftA -> fprintf chan "Extend.LeftA" -| RightA -> fprintf chan "Extend.RightA" -| NonA -> fprintf chan "Extend.NonA" +let print_assoc fmt = function +| LeftA -> fprintf fmt "Extend.LeftA" +| RightA -> fprintf fmt "Extend.RightA" +| NonA -> fprintf fmt "Extend.NonA" type symb = | SymbToken of string * string option @@ -171,111 +173,166 @@ let rec parse_tokens = function and parse_token tkn = parse_tokens [tkn] -let print_fun chan (vars, body) = +let print_fun fmt (vars, body) = let vars = List.rev vars in let iter = function - | None -> fprintf chan "_@ " - | Some id -> fprintf chan "%s@ " id + | None -> fprintf fmt "_@ " + | Some id -> fprintf fmt "%s@ " id in - let () = fprintf chan "fun@ " in + let () = fprintf fmt "fun@ " in let () = List.iter iter vars in (** FIXME: use Coq locations in the macros *) - let () = fprintf chan "loc ->@ @[%s@]" body.code in + let () = fprintf fmt "loc ->@ @[%s@]" body.code in () (** Meta-program instead of calling Tok.of_pattern here because otherwise violates value restriction *) -let print_tok chan = function -| "", s -> fprintf chan "Tok.KEYWORD %a" print_string s -| "IDENT", s -> fprintf chan "Tok.IDENT %a" print_string s -| "PATTERNIDENT", s -> fprintf chan "Tok.PATTERNIDENT %a" print_string s -| "FIELD", s -> fprintf chan "Tok.FIELD %a" print_string s -| "INT", s -> fprintf chan "Tok.INT %a" print_string s -| "STRING", s -> fprintf chan "Tok.STRING %a" print_string s -| "LEFTQMARK", _ -> fprintf chan "Tok.LEFTQMARK" -| "BULLET", s -> fprintf chan "Tok.BULLET %a" print_string s -| "EOI", _ -> fprintf chan "Tok.EOI" +let print_tok fmt = function +| "", s -> fprintf fmt "Tok.KEYWORD %a" print_string s +| "IDENT", s -> fprintf fmt "Tok.IDENT %a" print_string s +| "PATTERNIDENT", s -> fprintf fmt "Tok.PATTERNIDENT %a" print_string s +| "FIELD", s -> fprintf fmt "Tok.FIELD %a" print_string s +| "INT", s -> fprintf fmt "Tok.INT %a" print_string s +| "STRING", s -> fprintf fmt "Tok.STRING %a" print_string s +| "LEFTQMARK", _ -> fprintf fmt "Tok.LEFTQMARK" +| "BULLET", s -> fprintf fmt "Tok.BULLET %a" print_string s +| "EOI", _ -> fprintf fmt "Tok.EOI" | _ -> failwith "Tok.of_pattern: not a constructor" -let rec print_prod chan p = +let rec print_prod fmt p = let (vars, tkns) = List.split p.gprod_symbs in let f = (vars, p.gprod_body) in let tkn = List.rev_map parse_tokens tkns in - fprintf chan "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun f + fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun f -and print_symbols chan = function -| [] -> fprintf chan "Extend.Stop" +and print_symbols fmt = function +| [] -> fprintf fmt "Extend.Stop" | tkn :: tkns -> - fprintf chan "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn + fprintf fmt "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn -and print_symbol chan tkn = match tkn with +and print_symbol fmt tkn = match tkn with | SymbToken (t, s) -> let s = match s with None -> "" | Some s -> s in - fprintf chan "(Extend.Atoken (%a))" print_tok (t, s) + fprintf fmt "(Extend.Atoken (%a))" print_tok (t, s) | SymbEntry (e, None) -> - fprintf chan "(Extend.Aentry %s)" e + fprintf fmt "(Extend.Aentry %s)" e | SymbEntry (e, Some l) -> - fprintf chan "(Extend.Aentryl (%s, %a))" e print_string l + fprintf fmt "(Extend.Aentryl (%s, %a))" e print_string l | SymbSelf -> - fprintf chan "Extend.Aself" + fprintf fmt "Extend.Aself" | SymbNext -> - fprintf chan "Extend.Anext" + fprintf fmt "Extend.Anext" | SymbList0 (s, None) -> - fprintf chan "(Extend.Alist0 %a)" print_symbol s + fprintf fmt "(Extend.Alist0 %a)" print_symbol s | SymbList0 (s, Some sep) -> - fprintf chan "(Extend.Alist0sep (%a, %a))" print_symbol s print_symbol sep + fprintf fmt "(Extend.Alist0sep (%a, %a))" print_symbol s print_symbol sep | SymbList1 (s, None) -> - fprintf chan "(Extend.Alist1 %a)" print_symbol s + fprintf fmt "(Extend.Alist1 %a)" print_symbol s | SymbList1 (s, Some sep) -> - fprintf chan "(Extend.Alist1sep (%a, %a))" print_symbol s print_symbol sep + fprintf fmt "(Extend.Alist1sep (%a, %a))" print_symbol s print_symbol sep | SymbOpt s -> - fprintf chan "(Extend.Aopt %a)" print_symbol s + fprintf fmt "(Extend.Aopt %a)" print_symbol s | SymbRules rules -> - let pr chan (r, body) = + let pr fmt (r, body) = let (vars, tkn) = List.split r in let tkn = List.rev tkn in - fprintf chan "Extend.Rules @[({ Extend.norec_rule = %a },@ (%a))@]" print_symbols tkn print_fun (vars, body) + fprintf fmt "Extend.Rules @[({ Extend.norec_rule = %a },@ (%a))@]" print_symbols tkn print_fun (vars, body) in - let pr chan rules = print_list chan pr rules in - fprintf chan "(Extend.Arules %a)" pr (List.rev rules) - -let print_rule chan r = - let pr_lvl chan lvl = print_opt chan print_string lvl in - let pr_asc chan asc = print_opt chan print_assoc asc in - let pr_prd chan prd = print_list chan print_prod prd in - fprintf chan "@[(%a,@ %a,@ %a)@]" pr_lvl r.grule_label pr_asc r.grule_assoc pr_prd (List.rev r.grule_prods) - -let print_entry chan gram e = - let print_position_opt chan pos = print_opt chan print_position pos in - let print_rules chan rules = print_list chan print_rule rules in - fprintf chan "let () =@ @[%s.safe_extend@ %s@ @[(%a, %a)@]@]@ in@ " + let pr fmt rules = print_list fmt pr rules in + fprintf fmt "(Extend.Arules %a)" pr (List.rev rules) + +let print_rule fmt r = + let pr_lvl fmt lvl = print_opt fmt print_string lvl in + let pr_asc fmt asc = print_opt fmt print_assoc asc in + let pr_prd fmt prd = print_list fmt print_prod prd in + fprintf fmt "@[(%a,@ %a,@ %a)@]" pr_lvl r.grule_label pr_asc r.grule_assoc pr_prd (List.rev r.grule_prods) + +let print_entry fmt gram e = + let print_position_opt fmt pos = print_opt fmt print_position pos in + let print_rules fmt rules = print_list fmt print_rule rules in + fprintf fmt "let () =@ @[%s.safe_extend@ %s@ @[(%a, %a)@]@]@ in@ " gram e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules -let print_ast chan ext = - let () = fprintf chan "let _ = @[" in - let () = fprintf chan "@[<v>%a@]" print_local ext in - let () = List.iter (fun e -> print_entry chan ext.gramext_name e) ext.gramext_entries in - let () = fprintf chan "()@]\n" in +let print_ast fmt ext = + let () = fprintf fmt "let _ = @[" in + let () = fprintf fmt "@[<v>%a@]" print_local ext in + let () = List.iter (fun e -> print_entry fmt ext.gramext_name e) ext.gramext_entries in + let () = fprintf fmt "()@]@\n" in () end -let pr_ast chan = function -| Code s -> fprintf chan "%s@\n" s.code -| Comment s -> fprintf chan "%s@\n" s -| GramExt gram -> fprintf chan "%a@\n" GramExt.print_ast gram -| VernacExt -> fprintf chan "VERNACEXT@\n" -| TacticExt (id, rules) -> - let pr_tok = function - | ExtTerminal s -> Printf.sprintf "%s" s - | ExtNonTerminal (s, _) -> Printf.sprintf "%s" s - in - let pr_tacrule r = - let toks = String.concat " " (List.map pr_tok r.tac_toks) in - Printf.sprintf "[%s] -> {%s}" toks r.tac_body.code +module TacticExt : +sig + +val print_ast : Format.formatter -> tactic_ext -> unit + +end = +struct + +let rec print_symbol fmt = function +| Ulist1 s -> + fprintf fmt "@[Extend.TUlist1 (%a)@]" print_symbol s +| Ulist1sep (s, sep) -> + fprintf fmt "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep +| Ulist0 s -> + fprintf fmt "@[Extend.TUlist0 (%a)@]" print_symbol s +| Ulist0sep (s, sep) -> + fprintf fmt "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep +| Uopt s -> + fprintf fmt "@[Extend.TUopt (%a)@]" print_symbol s +| Uentry e -> + fprintf fmt "@[Extend.TUentry (Genarg.get_arg_tag wit_%s)@]" e +| Uentryl (e, l) -> + assert (e = "tactic"); + fprintf fmt "@[Extend.TUentryl (Genarg.get_arg_tag wit_%s, %i)@]" e l + +let rec print_clause fmt = function +| [] -> fprintf fmt "@[TyNil@]" +| ExtTerminal s :: cl -> fprintf fmt "@[TyIdent (\"%s\", %a)@]" s print_clause cl +| ExtNonTerminal (g, TokNone) :: cl -> + fprintf fmt "@[TyAnonArg (%a, %a)@]" + print_symbol g print_clause cl +| ExtNonTerminal (g, TokName id) :: cl -> + fprintf fmt "@[TyArg (%a, \"%s\", %a)@]" + print_symbol g id print_clause cl + +let rec print_binders fmt = function +| [] -> fprintf fmt "ist@ " +| (ExtTerminal _ | ExtNonTerminal (_, TokNone)) :: rem -> print_binders fmt rem +| (ExtNonTerminal (_, TokName id)) :: rem -> + fprintf fmt "%s@ %a" id print_binders rem + +let print_rule fmt r = + fprintf fmt "@[TyML (%a, @[fun %a -> %s@])@]" + print_clause r.tac_toks print_binders r.tac_toks r.tac_body.code + +let rec print_rules fmt = function +| [] -> () +| [r] -> fprintf fmt "(%a)@\n" print_rule r +| r :: rem -> fprintf fmt "(%a);@\n%a" print_rule r print_rules rem + +let print_rules fmt rules = + fprintf fmt "Tacentries.([@[<v>%a@]])" print_rules rules + +let print_ast fmt ext = + let pr fmt () = + let level = match ext.tacext_level with None -> 0 | Some i -> i in + fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a" + plugin_name ext.tacext_name level print_rules ext.tacext_rules in - let rules = String.concat ", " (List.map pr_tacrule rules) in - fprintf chan "TACTICEXT (%s, [%s])@\n" id rules + let () = fprintf fmt "let () = @[%a@]\n" pr () in + () + +end + +let pr_ast fmt = function +| Code s -> fprintf fmt "%s@\n" s.code +| Comment s -> fprintf fmt "%s@\n" s +| DeclarePlugin name -> fprintf fmt "let %s = \"%s\"@\n" plugin_name name +| GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram +| VernacExt -> fprintf fmt "VERNACEXT@\n" +| TacticExt tac -> fprintf fmt "%a@\n" TacticExt.print_ast tac let () = let () = diff --git a/grammar/coqpp_parse.mly b/grammar/coqpp_parse.mly index aa22d2717..baafd633c 100644 --- a/grammar/coqpp_parse.mly +++ b/grammar/coqpp_parse.mly @@ -10,13 +10,59 @@ open Coqpp_ast +let starts s pat = + let len = String.length s in + let patlen = String.length pat in + if patlen <= len && String.sub s 0 patlen = pat then + Some (String.sub s patlen (len - patlen)) + else None + +let ends s pat = + let len = String.length s in + let patlen = String.length pat in + if patlen <= len && String.sub s (len - patlen) patlen = pat then + Some (String.sub s 0 (len - patlen)) + else None + +let between s pat1 pat2 = match starts s pat1 with +| None -> None +| Some s -> ends s pat2 + +let without_sep k sep r = + if sep <> "" then raise Parsing.Parse_error else k r + +let parse_user_entry s sep = + let table = [ + "ne_", "_list", without_sep (fun r -> Ulist1 r); + "ne_", "_list_sep", (fun sep r -> Ulist1sep (r, sep)); + "", "_list", without_sep (fun r -> Ulist0 r); + "", "_list_sep", (fun sep r -> Ulist0sep (r, sep)); + "", "_opt", without_sep (fun r -> Uopt r); + ] in + let rec parse s sep = function + | [] -> + let () = without_sep ignore sep () in + begin match starts s "tactic" with + | Some ("0"|"1"|"2"|"3"|"4"|"5") -> Uentryl ("tactic", int_of_string s) + | Some _ | None -> Uentry s + end + | (pat1, pat2, k) :: rem -> + match between s pat1 pat2 with + | None -> parse s sep rem + | Some s -> + let r = parse s "" table in + k sep r + in + parse s sep table + %} %token <Coqpp_ast.code> CODE %token <string> COMMENT %token <string> IDENT QUALID %token <string> STRING -%token VERNAC TACTIC GRAMMAR EXTEND END +%token <int> INT +%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN %token LBRACKET RBRACKET PIPE ARROW COMMA EQUAL %token LPAREN RPAREN COLON SEMICOLON %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA @@ -42,11 +88,16 @@ nodes: node: | CODE { Code $1 } | COMMENT { Comment $1 } +| declare_plugin { $1 } | grammar_extend { $1 } | vernac_extend { $1 } | tactic_extend { $1 } ; +declare_plugin: +| DECLARE PLUGIN STRING { DeclarePlugin $3 } +; + grammar_extend: | GRAMMAR EXTEND qualid_or_ident globals gram_entries END { GramExt { gramext_name = $3; gramext_globals = $4; gramext_entries = $5 } } @@ -57,7 +108,13 @@ vernac_extend: ; tactic_extend: -| TACTIC EXTEND IDENT tactic_rules END { TacticExt ($3, $4) } +| TACTIC EXTEND IDENT tactic_level tactic_rules END + { TacticExt { tacext_name = $3; tacext_level = $4; tacext_rules = $5 } } +; + +tactic_level: +| { None } +| LEVEL INT { Some $2 } ; tactic_rules: @@ -77,9 +134,18 @@ ext_tokens: ext_token: | STRING { ExtTerminal $1 } -| IDENT { ExtNonTerminal ($1, TokNone) } -| IDENT LPAREN IDENT RPAREN { ExtNonTerminal ($1, TokName $3) } -| IDENT LPAREN IDENT COMMA STRING RPAREN { ExtNonTerminal ($1, TokNameSep ($3, $5)) } +| IDENT { + let e = parse_user_entry $1 "" in + ExtNonTerminal (e, TokNone) + } +| IDENT LPAREN IDENT RPAREN { + let e = parse_user_entry $1 "" in + ExtNonTerminal (e, TokName $3) + } +| IDENT LPAREN IDENT COMMA STRING RPAREN { + let e = parse_user_entry $1 $5 in + ExtNonTerminal (e, TokName $3) +} ; qualid_or_ident: diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 525be6432..cea0bed59 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -15,11 +15,6 @@ open Argextend let plugin_name = <:expr< __coq_plugin_name >> -let mlexpr_of_ident id = - (** Workaround for badly-designed generic arguments lacking a closure *) - let id = "$" ^ id in - <:expr< Names.Id.of_string_soft $str:id$ >> - let rec mlexpr_of_symbol = function | Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >> | Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >> @@ -38,9 +33,9 @@ let rec mlexpr_of_clause = function | [] -> <:expr< TyNil >> | ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >> | ExtNonTerminal(g,None) :: cl -> - <:expr< TyAnonArg(Loc.tag($mlexpr_of_symbol g$), $mlexpr_of_clause cl$) >> + <:expr< TyAnonArg($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> | ExtNonTerminal(g,Some id) :: cl -> - <:expr< TyArg(Loc.tag($mlexpr_of_symbol g$, $mlexpr_of_ident id$), $mlexpr_of_clause cl$) >> + <:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_string id$, $mlexpr_of_clause cl$) >> let rec binders_of_clause e = function | [] -> <:expr< fun ist -> $e$ >> diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.mlg index 3ae0f45cb..312ef1e55 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.mlg @@ -8,11 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin +} + DECLARE PLUGIN "btauto_plugin" TACTIC EXTEND btauto -| [ "btauto" ] -> [ Refl_btauto.Btauto.tac ] +| [ "btauto" ] -> { Refl_btauto.Btauto.tac } END diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.mlg index fb013ac13..685059294 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.mlg @@ -8,22 +8,26 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open Cctac open Stdarg +} + DECLARE PLUGIN "cc_plugin" (* Tactic registration *) TACTIC EXTEND cc - [ "congruence" ] -> [ congruence_tac 1000 [] ] - |[ "congruence" integer(n) ] -> [ congruence_tac n [] ] - |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ] +| [ "congruence" ] -> { congruence_tac 1000 [] } +| [ "congruence" integer(n) ] -> { congruence_tac n [] } +| [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l } |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> - [ congruence_tac n l ] + { congruence_tac n l } END TACTIC EXTEND f_equal - [ "f_equal" ] -> [ f_equal ] +| [ "f_equal" ] -> { f_equal } END diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.mlg index 44560ac18..703e29f96 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.mlg @@ -8,11 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open FourierR +} + DECLARE PLUGIN "fourier_plugin" TACTIC EXTEND fourier - [ "fourierz" ] -> [ fourier () ] +| [ "fourierz" ] -> { fourier () } END diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.mlg index 61525cb49..6388906f5 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.mlg @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Util open Locus open Tactypes @@ -18,147 +20,153 @@ open Tacarg open Names open Logic +let wit_hyp = wit_var + +} + DECLARE PLUGIN "ltac_plugin" (** Basic tactics *) TACTIC EXTEND reflexivity - [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] +| [ "reflexivity" ] -> { Tactics.intros_reflexivity } END TACTIC EXTEND exact - [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ] +| [ "exact" casted_constr(c) ] -> { Tactics.exact_no_check c } END TACTIC EXTEND assumption - [ "assumption" ] -> [ Tactics.assumption ] +| [ "assumption" ] -> { Tactics.assumption } END TACTIC EXTEND etransitivity - [ "etransitivity" ] -> [ Tactics.intros_transitivity None ] +| [ "etransitivity" ] -> { Tactics.intros_transitivity None } END TACTIC EXTEND cut - [ "cut" constr(c) ] -> [ Tactics.cut c ] +| [ "cut" constr(c) ] -> { Tactics.cut c } END TACTIC EXTEND exact_no_check - [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ] +| [ "exact_no_check" constr(c) ] -> { Tactics.exact_no_check c } END TACTIC EXTEND vm_cast_no_check - [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ] +| [ "vm_cast_no_check" constr(c) ] -> { Tactics.vm_cast_no_check c } END TACTIC EXTEND native_cast_no_check - [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ] +| [ "native_cast_no_check" constr(c) ] -> { Tactics.native_cast_no_check c } END TACTIC EXTEND casetype - [ "casetype" constr(c) ] -> [ Tactics.case_type c ] +| [ "casetype" constr(c) ] -> { Tactics.case_type c } END TACTIC EXTEND elimtype - [ "elimtype" constr(c) ] -> [ Tactics.elim_type c ] +| [ "elimtype" constr(c) ] -> { Tactics.elim_type c } END TACTIC EXTEND lapply - [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ] +| [ "lapply" constr(c) ] -> { Tactics.cut_and_apply c } END TACTIC EXTEND transitivity - [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ] +| [ "transitivity" constr(c) ] -> { Tactics.intros_transitivity (Some c) } END (** Left *) TACTIC EXTEND left - [ "left" ] -> [ Tactics.left_with_bindings false NoBindings ] +| [ "left" ] -> { Tactics.left_with_bindings false NoBindings } END TACTIC EXTEND eleft - [ "eleft" ] -> [ Tactics.left_with_bindings true NoBindings ] +| [ "eleft" ] -> { Tactics.left_with_bindings true NoBindings } END TACTIC EXTEND left_with - [ "left" "with" bindings(bl) ] -> [ +| [ "left" "with" bindings(bl) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.left_with_bindings false bl) - ] + } END TACTIC EXTEND eleft_with - [ "eleft" "with" bindings(bl) ] -> [ +| [ "eleft" "with" bindings(bl) ] -> { Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.left_with_bindings true bl) - ] + } END (** Right *) TACTIC EXTEND right - [ "right" ] -> [ Tactics.right_with_bindings false NoBindings ] +| [ "right" ] -> { Tactics.right_with_bindings false NoBindings } END TACTIC EXTEND eright - [ "eright" ] -> [ Tactics.right_with_bindings true NoBindings ] +| [ "eright" ] -> { Tactics.right_with_bindings true NoBindings } END TACTIC EXTEND right_with - [ "right" "with" bindings(bl) ] -> [ +| [ "right" "with" bindings(bl) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.right_with_bindings false bl) - ] + } END TACTIC EXTEND eright_with - [ "eright" "with" bindings(bl) ] -> [ +| [ "eright" "with" bindings(bl) ] -> { Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.right_with_bindings true bl) - ] + } END (** Constructor *) TACTIC EXTEND constructor - [ "constructor" ] -> [ Tactics.any_constructor false None ] -| [ "constructor" int_or_var(i) ] -> [ +| [ "constructor" ] -> { Tactics.any_constructor false None } +| [ "constructor" int_or_var(i) ] -> { Tactics.constructor_tac false None i NoBindings - ] -| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [ + } +| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> { let tac bl = Tactics.constructor_tac false None i bl in Tacticals.New.tclDELAYEDWITHHOLES false bl tac - ] + } END TACTIC EXTEND econstructor - [ "econstructor" ] -> [ Tactics.any_constructor true None ] -| [ "econstructor" int_or_var(i) ] -> [ +| [ "econstructor" ] -> { Tactics.any_constructor true None } +| [ "econstructor" int_or_var(i) ] -> { Tactics.constructor_tac true None i NoBindings - ] -| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [ + } +| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> { let tac bl = Tactics.constructor_tac true None i bl in Tacticals.New.tclDELAYEDWITHHOLES true bl tac - ] + } END (** Specialize *) TACTIC EXTEND specialize - [ "specialize" constr_with_bindings(c) ] -> [ +| [ "specialize" constr_with_bindings(c) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None) - ] -| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [ + } +| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat)) - ] + } END TACTIC EXTEND symmetry - [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ] +| [ "symmetry" ] -> { Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} } END TACTIC EXTEND symmetry_in -| [ "symmetry" "in" in_clause(cl) ] -> [ Tactics.intros_symmetry cl ] +| [ "symmetry" "in" in_clause(cl) ] -> { Tactics.intros_symmetry cl } END (** Split *) +{ + let rec delayed_list = function | [] -> fun _ sigma -> (sigma, []) | x :: l -> @@ -167,147 +175,159 @@ let rec delayed_list = function let (sigma, l) = delayed_list l env sigma in (sigma, x :: l) +} + TACTIC EXTEND split - [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ] +| [ "split" ] -> { Tactics.split_with_bindings false [NoBindings] } END TACTIC EXTEND esplit - [ "esplit" ] -> [ Tactics.split_with_bindings true [NoBindings] ] +| [ "esplit" ] -> { Tactics.split_with_bindings true [NoBindings] } END TACTIC EXTEND split_with - [ "split" "with" bindings(bl) ] -> [ +| [ "split" "with" bindings(bl) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.split_with_bindings false [bl]) - ] + } END TACTIC EXTEND esplit_with - [ "esplit" "with" bindings(bl) ] -> [ +| [ "esplit" "with" bindings(bl) ] -> { Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.split_with_bindings true [bl]) - ] + } END TACTIC EXTEND exists - [ "exists" ] -> [ Tactics.split_with_bindings false [NoBindings] ] -| [ "exists" ne_bindings_list_sep(bll, ",") ] -> [ +| [ "exists" ] -> { Tactics.split_with_bindings false [NoBindings] } +| [ "exists" ne_bindings_list_sep(bll, ",") ] -> { Tacticals.New.tclDELAYEDWITHHOLES false (delayed_list bll) (fun bll -> Tactics.split_with_bindings false bll) - ] + } END TACTIC EXTEND eexists - [ "eexists" ] -> [ Tactics.split_with_bindings true [NoBindings] ] -| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> [ +| [ "eexists" ] -> { Tactics.split_with_bindings true [NoBindings] } +| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> { Tacticals.New.tclDELAYEDWITHHOLES true (delayed_list bll) (fun bll -> Tactics.split_with_bindings true bll) - ] + } END (** Intro *) TACTIC EXTEND intros_until - [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ] +| [ "intros" "until" quantified_hypothesis(h) ] -> { Tactics.intros_until h } END TACTIC EXTEND intro -| [ "intro" ] -> [ Tactics.intro_move None MoveLast ] -| [ "intro" ident(id) ] -> [ Tactics.intro_move (Some id) MoveLast ] -| [ "intro" ident(id) "at" "top" ] -> [ Tactics.intro_move (Some id) MoveFirst ] -| [ "intro" ident(id) "at" "bottom" ] -> [ Tactics.intro_move (Some id) MoveLast ] -| [ "intro" ident(id) "after" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveAfter h) ] -| [ "intro" ident(id) "before" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveBefore h) ] -| [ "intro" "at" "top" ] -> [ Tactics.intro_move None MoveFirst ] -| [ "intro" "at" "bottom" ] -> [ Tactics.intro_move None MoveLast ] -| [ "intro" "after" hyp(h) ] -> [ Tactics.intro_move None (MoveAfter h) ] -| [ "intro" "before" hyp(h) ] -> [ Tactics.intro_move None (MoveBefore h) ] +| [ "intro" ] -> { Tactics.intro_move None MoveLast } +| [ "intro" ident(id) ] -> { Tactics.intro_move (Some id) MoveLast } +| [ "intro" ident(id) "at" "top" ] -> { Tactics.intro_move (Some id) MoveFirst } +| [ "intro" ident(id) "at" "bottom" ] -> { Tactics.intro_move (Some id) MoveLast } +| [ "intro" ident(id) "after" hyp(h) ] -> { Tactics.intro_move (Some id) (MoveAfter h) } +| [ "intro" ident(id) "before" hyp(h) ] -> { Tactics.intro_move (Some id) (MoveBefore h) } +| [ "intro" "at" "top" ] -> { Tactics.intro_move None MoveFirst } +| [ "intro" "at" "bottom" ] -> { Tactics.intro_move None MoveLast } +| [ "intro" "after" hyp(h) ] -> { Tactics.intro_move None (MoveAfter h) } +| [ "intro" "before" hyp(h) ] -> { Tactics.intro_move None (MoveBefore h) } END (** Move *) TACTIC EXTEND move - [ "move" hyp(id) "at" "top" ] -> [ Tactics.move_hyp id MoveFirst ] -| [ "move" hyp(id) "at" "bottom" ] -> [ Tactics.move_hyp id MoveLast ] -| [ "move" hyp(id) "after" hyp(h) ] -> [ Tactics.move_hyp id (MoveAfter h) ] -| [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ] +| [ "move" hyp(id) "at" "top" ] -> { Tactics.move_hyp id MoveFirst } +| [ "move" hyp(id) "at" "bottom" ] -> { Tactics.move_hyp id MoveLast } +| [ "move" hyp(id) "after" hyp(h) ] -> { Tactics.move_hyp id (MoveAfter h) } +| [ "move" hyp(id) "before" hyp(h) ] -> { Tactics.move_hyp id (MoveBefore h) } END (** Rename *) TACTIC EXTEND rename -| [ "rename" ne_rename_list_sep(ids, ",") ] -> [ Tactics.rename_hyp ids ] +| [ "rename" ne_rename_list_sep(ids, ",") ] -> { Tactics.rename_hyp ids } END (** Revert *) TACTIC EXTEND revert - [ "revert" ne_hyp_list(hl) ] -> [ Tactics.revert hl ] +| [ "revert" ne_hyp_list(hl) ] -> { Tactics.revert hl } END (** Simple induction / destruct *) +{ + let simple_induct h = Tacticals.New.tclTHEN (Tactics.intros_until h) (Tacticals.New.onLastHyp Tactics.simplest_elim) +} + TACTIC EXTEND simple_induction - [ "simple" "induction" quantified_hypothesis(h) ] -> [ simple_induct h ] +| [ "simple" "induction" quantified_hypothesis(h) ] -> { simple_induct h } END +{ + let simple_destruct h = Tacticals.New.tclTHEN (Tactics.intros_until h) (Tacticals.New.onLastHyp Tactics.simplest_case) +} + TACTIC EXTEND simple_destruct - [ "simple" "destruct" quantified_hypothesis(h) ] -> [ simple_destruct h ] +| [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h } END (** Double induction *) TACTIC EXTEND double_induction - [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> - [ Elim.h_double_induction h1 h2 ] +| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> + { Elim.h_double_induction h1 h2 } END (* Admit *) TACTIC EXTEND admit - [ "admit" ] -> [ Proofview.give_up ] +|[ "admit" ] -> { Proofview.give_up } END (* Fix *) TACTIC EXTEND fix - [ "fix" ident(id) natural(n) ] -> [ Tactics.fix id n ] +| [ "fix" ident(id) natural(n) ] -> { Tactics.fix id n } END (* Cofix *) TACTIC EXTEND cofix - [ "cofix" ident(id) ] -> [ Tactics.cofix id ] +| [ "cofix" ident(id) ] -> { Tactics.cofix id } END (* Clear *) TACTIC EXTEND clear - [ "clear" hyp_list(ids) ] -> [ +| [ "clear" hyp_list(ids) ] -> { if List.is_empty ids then Tactics.keep [] else Tactics.clear ids - ] -| [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ] + } +| [ "clear" "-" ne_hyp_list(ids) ] -> { Tactics.keep ids } END (* Clearbody *) TACTIC EXTEND clearbody - [ "clearbody" ne_hyp_list(ids) ] -> [ Tactics.clear_body ids ] +| [ "clearbody" ne_hyp_list(ids) ] -> { Tactics.clear_body ids } END (* Generalize dependent *) TACTIC EXTEND generalize_dependent - [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ] +| [ "generalize" "dependent" constr(c) ] -> { Tactics.generalize_dep c } END (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) +{ + open Tacexpr let initial_atomic () = @@ -364,3 +384,5 @@ let initial_tacticals () = ] let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin" + +} diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.mlg index 2251a6620..e57afe3e3 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.mlg @@ -14,15 +14,19 @@ (* by Eduardo Gimenez *) (************************************************************************) +{ + open Eqdecide open Stdarg +} + DECLARE PLUGIN "ltac_plugin" TACTIC EXTEND decide_equality -| [ "decide" "equality" ] -> [ decideEqualityGoal ] +| [ "decide" "equality" ] -> { decideEqualityGoal } END TACTIC EXTEND compare -| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ] +| [ "compare" constr(c1) constr(c2) ] -> { compare c1 c2 } END diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 876e6f320..fac464a62 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -554,13 +554,18 @@ let () = ] in register_grammars_by_name "tactic" entries +let get_identifier id = + (** Workaround for badly-designed generic arguments lacking a closure *) + Names.Id.of_string_soft ("$" ^ id) + + type _ ty_sig = | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig | TyIdent : string * 'r ty_sig -> 'r ty_sig | TyArg : - (('a, 'b, 'c) Extend.ty_user_symbol * Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig | TyAnonArg : - ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml @@ -578,10 +583,11 @@ let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol fun sign -> match sign with | TyNil -> [] | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig' - | TyArg ((loc,(a,id)),sig') -> - TacNonTerm (loc,(untype_user_symbol a,Some id)) :: clause_of_sign sig' - | TyAnonArg ((loc,a),sig') -> - TacNonTerm (loc,(untype_user_symbol a,None)) :: clause_of_sign sig' + | TyArg (a, id, sig') -> + let id = get_identifier id in + TacNonTerm (None,(untype_user_symbol a,Some id)) :: clause_of_sign sig' + | TyAnonArg (a, sig') -> + TacNonTerm (None,(untype_user_symbol a,None)) :: clause_of_sign sig' let clause_of_ty_ml = function | TyML (t,_) -> clause_of_sign t @@ -604,7 +610,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i | _ :: _ -> assert false end | TyIdent (s, sig') -> eval_sign sig' tac - | TyArg ((_loc,(a,id)), sig') -> + | TyArg (a, _, sig') -> let f = eval_sign sig' in begin fun tac vals ist -> match vals with | [] -> assert false @@ -612,7 +618,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i let v' = Taccoerce.Value.cast (topwit (prj a)) v in f (tac v') vals ist end tac - | TyAnonArg ((_loc,a), sig') -> eval_sign sig' tac + | TyAnonArg (a, sig') -> eval_sign sig' tac let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function | TyML (t,tac) -> eval_sign t tac @@ -624,14 +630,14 @@ let is_constr_entry = function let rec only_constr : type a. a ty_sig -> bool = function | TyNil -> true | TyIdent(_,_) -> false -| TyArg((_,(u,_)),s) -> if is_constr_entry u then only_constr s else false -| TyAnonArg((_,u),s) -> if is_constr_entry u then only_constr s else false +| TyArg (u, _, s) -> if is_constr_entry u then only_constr s else false +| TyAnonArg (u, s) -> if is_constr_entry u then only_constr s else false let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function | TyNil -> [] | TyIdent (_,s) -> mk_sign_vars s -| TyArg((_,(_,name)),s) -> Name name :: mk_sign_vars s -| TyAnonArg((_,_),s) -> Anonymous :: mk_sign_vars s +| TyArg (_, name, s) -> Name (get_identifier name) :: mk_sign_vars s +| TyAnonArg (_, s) -> Anonymous :: mk_sign_vars s let dummy_id = Id.of_string "_" diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 2bfbbe2e1..9bba9ba71 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -72,9 +72,9 @@ type _ ty_sig = | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig | TyIdent : string * 'r ty_sig -> 'r ty_sig | TyArg : - (('a, 'b, 'c) Extend.ty_user_symbol * Names.Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig | TyAnonArg : - ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.mlg index 81140a46a..21f0414e9 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.mlg @@ -16,70 +16,74 @@ (* *) (************************************************************************) +{ + open Ltac_plugin open Stdarg open Tacarg +} + DECLARE PLUGIN "micromega_plugin" TACTIC EXTEND RED -| [ "myred" ] -> [ Tactics.red_in_concl ] +| [ "myred" ] -> { Tactics.red_in_concl } END TACTIC EXTEND PsatzZ -| [ "psatz_Z" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_Z i +| [ "psatz_Z" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Z i (Tacinterp.tactic_of_value ist t)) - ] -| [ "psatz_Z" tactic(t)] -> [ (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) ] + } +| [ "psatz_Z" tactic(t)] -> { (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) } END TACTIC EXTEND Lia -[ "xlia" tactic(t) ] -> [ (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) ] +| [ "xlia" tactic(t) ] -> { (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND Nia -[ "xnlia" tactic(t) ] -> [ (Coq_micromega.xnlia (Tacinterp.tactic_of_value ist t)) ] +| [ "xnlia" tactic(t) ] -> { (Coq_micromega.xnlia (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND NRA -[ "xnra" tactic(t) ] -> [ (Coq_micromega.nra (Tacinterp.tactic_of_value ist t))] +| [ "xnra" tactic(t) ] -> { (Coq_micromega.nra (Tacinterp.tactic_of_value ist t))} END TACTIC EXTEND NQA -[ "xnqa" tactic(t) ] -> [ (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))] +| [ "xnqa" tactic(t) ] -> { (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))} END TACTIC EXTEND Sos_Z -| [ "sos_Z" tactic(t) ] -> [ (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) ] +| [ "sos_Z" tactic(t) ] -> { (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND Sos_Q -| [ "sos_Q" tactic(t) ] -> [ (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) ] +| [ "sos_Q" tactic(t) ] -> { (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND Sos_R -| [ "sos_R" tactic(t) ] -> [ (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) ] +| [ "sos_R" tactic(t) ] -> { (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND LRA_Q -[ "lra_Q" tactic(t) ] -> [ (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) ] +| [ "lra_Q" tactic(t) ] -> { (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND LRA_R -[ "lra_R" tactic(t) ] -> [ (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) ] +| [ "lra_R" tactic(t) ] -> { (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND PsatzR -| [ "psatz_R" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) ] -| [ "psatz_R" tactic(t) ] -> [ (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) ] +| [ "psatz_R" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) } +| [ "psatz_R" tactic(t) ] -> { (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND PsatzQ -| [ "psatz_Q" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) ] -| [ "psatz_Q" tactic(t) ] -> [ (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) ] +| [ "psatz_Q" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) } +| [ "psatz_Q" tactic(t) ] -> { (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) } END diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.mlg index 4ac49adb9..16ff512e8 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.mlg @@ -8,11 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open Stdarg +} + DECLARE PLUGIN "nsatz_plugin" TACTIC EXTEND nsatz_compute -| [ "nsatz_compute" constr(lt) ] -> [ Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) ] +| [ "nsatz_compute" constr(lt) ] -> { Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) } END diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.mlg index 170b937c9..c3d063cff 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.mlg @@ -18,6 +18,8 @@ DECLARE PLUGIN "omega_plugin" +{ + open Ltac_plugin open Names open Coq_omega @@ -43,14 +45,15 @@ let omega_tactic l = (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs)) (omega_solver) +} TACTIC EXTEND omega -| [ "omega" ] -> [ omega_tactic [] ] +| [ "omega" ] -> { omega_tactic [] } END TACTIC EXTEND omega' | [ "omega" "with" ne_ident_list(l) ] -> - [ omega_tactic (List.map Names.Id.to_string l) ] -| [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ] + { omega_tactic (List.map Names.Id.to_string l) } +| [ "omega" "with" "*" ] -> { omega_tactic ["nat";"positive";"N";"Z"] } END diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.mlg index 09209dc22..749903c3a 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.mlg @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open Names open Tacexpr @@ -16,8 +18,12 @@ open Quote open Stdarg open Tacarg +} + DECLARE PLUGIN "quote_plugin" +{ + let cont = Id.of_string "cont" let x = Id.of_string "x" @@ -27,12 +33,14 @@ let make_cont (k : Val.t) (c : EConstr.t) = let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac)) +} + TACTIC EXTEND quote - [ "quote" ident(f) ] -> [ quote f [] ] -| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ] +| [ "quote" ident(f) ] -> { quote f [] } +| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> { quote f lc } | [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] -> - [ gen_quote (make_cont k) c f [] ] + { gen_quote (make_cont k) c f [] } | [ "quote" ident(f) "[" ne_ident_list(lc) "]" "in" constr(c) "using" tactic(k) ] -> - [ gen_quote (make_cont k) c f lc ] + { gen_quote (make_cont k) c f lc } END diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.mlg index 5b77d08de..c1ce30027 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.mlg @@ -9,6 +9,8 @@ DECLARE PLUGIN "romega_plugin" +{ + open Ltac_plugin open Names open Refl_omega @@ -39,13 +41,15 @@ let romega_tactic unsafe l = (Tactics.intros) (total_reflexive_omega_tactic unsafe)) +} + TACTIC EXTEND romega -| [ "romega" ] -> [ romega_tactic false [] ] -| [ "unsafe_romega" ] -> [ romega_tactic true [] ] +| [ "romega" ] -> { romega_tactic false [] } +| [ "unsafe_romega" ] -> { romega_tactic true [] } END TACTIC EXTEND romega' | [ "romega" "with" ne_ident_list(l) ] -> - [ romega_tactic false (List.map Names.Id.to_string l) ] -| [ "romega" "with" "*" ] -> [ romega_tactic false ["nat";"positive";"N";"Z"] ] + { romega_tactic false (List.map Names.Id.to_string l) } +| [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] } END diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.mlg index aa6757634..9c9fdcfa2 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.mlg @@ -8,12 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ open Ltac_plugin +} + DECLARE PLUGIN "rtauto_plugin" TACTIC EXTEND rtauto - [ "rtauto" ] -> [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ] +| [ "rtauto" ] -> { Proofview.V82.tactic (Refl_tauto.rtauto_tac) } END diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 16d003f67..21c202205 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -144,7 +144,7 @@ let construct_of_constr_const env tag typ = let construct_of_constr_block = construct_of_constr false -let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p = +let build_branches_type env sigma (mind,_ as _ind) mib mip u params p = let rtbl = mip.mind_reloc_tbl in (* [build_one_branch i cty] construit le type de la ieme branche (commence a 0) et les lambda correspondant aux realargs *) @@ -161,20 +161,17 @@ let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p = let codom = let ndecl = List.length decl in let papp = mkApp(lift ndecl p,crealargs) in - if dep then - let cstr = ith_constructor_of_inductive (fst ind) (i+1) in - let relargs = Array.init carity (fun i -> mkRel (carity-i)) in - let params = Array.map (lift ndecl) params in - let dep_cstr = mkApp(mkApp(mkConstructU (cstr,snd ind),params),relargs) in - mkApp(papp,[|dep_cstr|]) - else papp + let cstr = ith_constructor_of_inductive (fst ind) (i+1) in + let relargs = Array.init carity (fun i -> mkRel (carity-i)) in + let params = Array.map (lift ndecl) params in + let dep_cstr = mkApp(mkApp(mkConstructU (cstr,snd ind),params),relargs) in + mkApp(papp,[|dep_cstr|]) in decl, decl_with_letin, codom in Array.mapi build_one_branch mip.mind_nf_lc -let build_case_type dep p realargs c = - if dep then mkApp(mkApp(p, realargs), [|c|]) - else mkApp(p, realargs) +let build_case_type p realargs c = + mkApp(mkApp(p, realargs), [|c|]) (* normalisation of values *) @@ -317,9 +314,9 @@ and nf_atom_type env sigma atom = let pT = hnf_prod_applist_assum env nparamdecls (Inductiveops.type_of_inductive env ind) (Array.to_list params) in - let dep, p = nf_predicate env sigma ind mip params p pT in + let p = nf_predicate env sigma ind mip params p pT in (* Calcul du type des branches *) - let btypes = build_branches_type env sigma (fst ind) mib mip u params dep p in + let btypes = build_branches_type env sigma (fst ind) mib mip u params p in (* calcul des branches *) let bsw = branch_of_switch (nb_rel env) ans bs in let mkbranch i v = @@ -328,7 +325,7 @@ and nf_atom_type env sigma atom = Termops.it_mkLambda_or_LetIn_from_no_LetIn b decl_with_letin in let branchs = Array.mapi mkbranch bsw in - let tcase = build_case_type dep p realargs a in + let tcase = build_case_type p realargs a in let ci = ans.asw_ci in mkCase(ci, p, a, branchs), tcase | Afix(tt,ft,rp,s) -> @@ -375,18 +372,18 @@ and nf_atom_type env sigma atom = and nf_predicate env sigma ind mip params v pT = match kind (whd_allnolet env pT) with | LetIn (name,b,t,pT) -> - let dep,body = + let body = nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in - dep, mkLetIn (name,b,t,body) + mkLetIn (name,b,t,body) | Prod (name,dom,codom) -> begin match kind_of_value v with | Vfun f -> let k = nb_rel env in let vb = f (mk_rel_accu k) in - let dep,body = + let body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in - dep, mkLambda(name,dom,body) - | _ -> false, nf_type env sigma v + mkLambda(name,dom,body) + | _ -> nf_type env sigma v end | _ -> match kind_of_value v with @@ -399,8 +396,8 @@ and nf_predicate env sigma ind mip params v pT = let params = if Int.equal n 0 then params else Array.map (lift n) params in let dom = mkApp(mkIndU ind,Array.append params rargs) in let body = nf_type (push_rel (LocalAssum (name,dom)) env) sigma vb in - true, mkLambda(name,dom,body) - | _ -> false, nf_type env sigma v + mkLambda(name,dom,body) + | _ -> nf_type env sigma v and nf_evar env sigma evk ty args = let evi = try Evd.find sigma evk with Not_found -> assert false in diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index bd6062824..440076c16 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -103,7 +103,7 @@ let construct_of_constr_block = construct_of_constr false let type_of_ind env (ind, u) = type_of_inductive env (Inductive.lookup_mind_specif env ind, u) -let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p = +let build_branches_type env sigma (mind,_ as _ind) mib mip u params p = let rtbl = mip.mind_reloc_tbl in (* [build_one_branch i cty] construit le type de la ieme branche (commence a 0) et les lambda correspondant aux realargs *) @@ -120,20 +120,17 @@ let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p = let codom = let ndecl = List.length decl in let papp = mkApp(lift ndecl p,crealargs) in - if dep then - let cstr = ith_constructor_of_inductive ind (i+1) in - let relargs = Array.init carity (fun i -> mkRel (carity-i)) in - let params = Array.map (lift ndecl) params in - let dep_cstr = mkApp(mkApp(mkConstructU (cstr,u),params),relargs) in - mkApp(papp,[|dep_cstr|]) - else papp + let cstr = ith_constructor_of_inductive ind (i+1) in + let relargs = Array.init carity (fun i -> mkRel (carity-i)) in + let params = Array.map (lift ndecl) params in + let dep_cstr = mkApp(mkApp(mkConstructU (cstr,u),params),relargs) in + mkApp(papp,[|dep_cstr|]) in decl, decl_with_letin, codom in Array.mapi build_one_branch mip.mind_nf_lc -let build_case_type dep p realargs c = - if dep then mkApp(mkApp(p, realargs), [|c|]) - else mkApp(p, realargs) +let build_case_type p realargs c = + mkApp(mkApp(p, realargs), [|c|]) (* La fonction de normalisation *) @@ -266,9 +263,9 @@ and nf_stk ?from:(from=0) env sigma c t stk = let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in - let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in + let p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) - let btypes = build_branches_type env sigma ind mib mip u params dep p in + let btypes = build_branches_type env sigma ind mib mip u params p in (* calcul des branches *) let bsw = branch_of_switch (nb_rel env) sw in let mkbranch i (n,v) = @@ -277,7 +274,7 @@ and nf_stk ?from:(from=0) env sigma c t stk = Termops.it_mkLambda_or_LetIn_from_no_LetIn b decl_with_letin in let branchs = Array.mapi mkbranch bsw in - let tcase = build_case_type dep p realargs c in + let tcase = build_case_type p realargs c in let ci = sw.sw_annot.Cbytecodes.ci in nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk | Zproj p :: stk -> @@ -289,17 +286,17 @@ and nf_stk ?from:(from=0) env sigma c t stk = and nf_predicate env sigma ind mip params v pT = match kind (whd_allnolet env pT) with | LetIn (name,b,t,pT) -> - let dep,body = + let body = nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in - dep, mkLetIn (name,b,t,body) + mkLetIn (name,b,t,body) | Prod (name,dom,codom) -> begin match whd_val v with | Vfun f -> let k = nb_rel env in let vb = reduce_fun k f in - let dep,body = + let body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in - dep, mkLambda(name,dom,body) + mkLambda(name,dom,body) | _ -> assert false end | _ -> @@ -313,8 +310,8 @@ and nf_predicate env sigma ind mip params v pT = let params = if Int.equal n 0 then params else Array.map (lift n) params in let dom = mkApp(mkIndU ind,Array.append params rargs) in let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in - true, mkLambda(name,dom,body) - | _ -> false, nf_val env sigma v crazy_type + mkLambda(name,dom,body) + | _ -> nf_val env sigma v crazy_type and nf_args env sigma vargs ?from:(f=0) t = let t = ref t in diff --git a/shell.nix b/shell.nix new file mode 100644 index 000000000..45070b2ba --- /dev/null +++ b/shell.nix @@ -0,0 +1,4 @@ +# Some developers don't want a pinned nix-shell by default. +# If you want to use the pin nix-shell or a more sophisticated set of arguments: +# $ nix-shell default.nix +import ./default.nix { pkgs = import <nixpkgs> {}; } diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 8e60d3932..7aa2d0a5a 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -65,20 +65,20 @@ VERBOSE ?= # Time the Coq process (set to non empty), and how (see default value) TIMED?= TIMECMD?= -# Use /usr/bin/env time on linux, gtime on Mac OS +# Use command time on linux, gtime on Mac OS TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" ifneq (,$(TIMED)) -ifeq (0,$(shell /usr/bin/env time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) -STDTIME?=/usr/bin/env time -f $(TIMEFMT) +ifeq (0,$(shell command time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=command time -f $(TIMEFMT) else ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=gtime -f $(TIMEFMT) else -STDTIME?=time +STDTIME?=command time endif endif else -STDTIME?=/usr/bin/env time -f $(TIMEFMT) +STDTIME?=command time -f $(TIMEFMT) endif # Coq binaries |