diff options
135 files changed, 1750 insertions, 1238 deletions
diff --git a/azure-pipelines.yml b/azure-pipelines.yml index f2cec1eb19..c93920a884 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -43,7 +43,7 @@ jobs: vmImage: 'macOS-10.13' variables: - MACOSX_DEPLOYMENT_TARGET: '10.12' + MACOSX_DEPLOYMENT_TARGET: '10.11' steps: - checkout: self diff --git a/default.nix b/default.nix index 1e2cb3625d..d5c6cdb8ad 100644 --- a/default.nix +++ b/default.nix @@ -74,7 +74,7 @@ stdenv.mkDerivation rec { else with builtins; filterSource (path: _: - !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci"]) ./.; + !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci" "nix"]) ./.; preConfigure = '' patchShebangs dev/tools/ diff --git a/dev/ci/nix/bignums.nix b/dev/ci/nix/bignums.nix index 1d931c858e..d813ddd8d7 100644 --- a/dev/ci/nix/bignums.nix +++ b/dev/ci/nix/bignums.nix @@ -1,5 +1,5 @@ { ocamlPackages }: { - buildInputs = with ocamlPackages; [ ocaml findlib camlp5 ]; + buildInputs = [ ocamlPackages.ocaml ]; } diff --git a/dev/ci/nix/unicoq/unicoq-num.patch b/dev/ci/nix/unicoq/unicoq-num.patch index 6d96d94dfc..6d2f6470b1 100644 --- a/dev/ci/nix/unicoq/unicoq-num.patch +++ b/dev/ci/nix/unicoq/unicoq-num.patch @@ -4,19 +4,6 @@ Date: Thu Nov 29 08:59:22 2018 +0000 Make explicit dependency to num -diff --git a/Make b/Make -index 550dc6a..8aa1309 100644 ---- a/Make -+++ b/Make -@@ -9,7 +9,7 @@ src/logger.ml - src/munify.mli - src/munify.ml - src/unitactics.mlg --src/unicoq.mllib -+src/unicoq.mlpack - theories/Unicoq.v - test-suite/munifytest.v - test-suite/microtests.v diff --git a/Makefile.local b/Makefile.local new file mode 100644 index 0000000..88be365 @@ -24,21 +11,3 @@ index 0000000..88be365 +++ b/Makefile.local @@ -0,0 +1 @@ +CAMLPKGS += -package num -diff --git a/src/unicoq.mllib b/src/unicoq.mllib -deleted file mode 100644 -index 2b84e2d..0000000 ---- a/src/unicoq.mllib -+++ /dev/null -@@ -1,3 +0,0 @@ --Logger --Munify --Unitactics -diff --git a/src/unicoq.mlpack b/src/unicoq.mlpack -new file mode 100644 -index 0000000..2b84e2d ---- /dev/null -+++ b/src/unicoq.mlpack -@@ -0,0 +1,3 @@ -+Logger -+Munify -+Unitactics diff --git a/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh new file mode 100644 index 0000000000..dc39ea5ef0 --- /dev/null +++ b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh @@ -0,0 +1,7 @@ +if [ "$CI_PULL_REQUEST" = "8893" ] || [ "$CI_BRANCH" = "master+moving-evars-of-term-on-econstr" ]; then + + equations_CI_BRANCH=master+fix-evars_of_term-pr8893 + equations_CI_REF=master+fix-evars_of_term-pr8893 + equations_CI_GITURL=https://github.com/herbelin/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh new file mode 100644 index 0000000000..4032b1c6b5 --- /dev/null +++ b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10125" ] || [ "$CI_BRANCH" = "run_tactic_gen" ]; then + + paramcoq_CI_REF=run_tactic_gen + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq + +fi diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh new file mode 100644 index 0000000000..bc8aa33565 --- /dev/null +++ b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then + + unicoq_CI_REF=detype-anonymous + unicoq_CI_GITURL=https://github.com/maximedenes/unicoq + +fi diff --git a/dev/include_printers b/dev/include_printers index 90088e40bf..d077075eeb 100644 --- a/dev/include_printers +++ b/dev/include_printers @@ -11,6 +11,7 @@ #install_printer (* universes *) ppuniverses;; #install_printer (* univ level *) ppuni_level;; #install_printer (* univ context *) ppuniverse_context;; +#install_printer (* univ context *) ppaucontext;; #install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; #install_printer (* univ set *) ppuniverse_set;; diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index f4786d9431..8dfe1e7833 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/8471ab76242987b11afd4486b82888e1588f8307.tar.gz"; - sha256 = "06pp6b6x78jlinxifnphkbp79dx58jr990fkm4qziq0ay5klpxd7"; + url = "https://github.com/NixOS/nixpkgs/archive/bc9df0f66110039e495b6debe3a6cda4a1bb0fed.tar.gz"; + sha256 = "0y2w259j0vqiwjhjvlbsaqnp1nl2zwz6sbwwhkrqn7k7fmhmxnq1"; }) diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index a6ecec7e33..82f2e79549 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -62,6 +62,7 @@ install_printer Top_printers.ppuni_level install_printer Top_printers.ppuniverse_set install_printer Top_printers.ppuniverse_instance install_printer Top_printers.ppuniverse_context +install_printer Top_printers.ppaucontext install_printer Top_printers.ppuniverse_context_set install_printer Top_printers.ppuniverse_subst install_printer Top_printers.ppuniverse_opt_subst diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 816316487c..2859b56cbe 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -27,7 +27,6 @@ open Clenv let _ = Detyping.print_evar_arguments := true let _ = Detyping.print_universes := true let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false -let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found) (* std_ppcmds *) let pp x = Pp.pp_with !Topfmt.std_ft x @@ -236,6 +235,15 @@ let ppnamedcontextval e = let sigma = Evd.from_env env in pp (pr_named_context env sigma (named_context_of_val e)) +let ppaucontext auctx = + let nas = AUContext.names auctx in + let prlev l = match Level.var_index l with + | Some n -> Name.print nas.(n) + | None -> prlev l + in + pp (pr_universe_context prlev (AUContext.repr auctx)) + + let ppenv e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]") diff --git a/dev/top_printers.mli b/dev/top_printers.mli index cb32d2294c..2aa1808322 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -137,6 +137,7 @@ val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *) val ppuniverse_set : Univ.LSet.t -> unit val ppuniverse_instance : Univ.Instance.t -> unit val ppuniverse_context : Univ.UContext.t -> unit +val ppaucontext : Univ.AUContext.t -> unit val ppuniverse_context_set : Univ.ContextSet.t -> unit val ppuniverse_subst : Univ.universe_subst -> unit val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit diff --git a/doc/changelog/03-notations/10061-print-custom-grammar.rst b/doc/changelog/03-notations/10061-print-custom-grammar.rst deleted file mode 100644 index 8786c7ce6b..0000000000 --- a/doc/changelog/03-notations/10061-print-custom-grammar.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar` - (`#10061 <https://github.com/coq/coq/pull/10061>`_, - fixes `#9681 <http://github.com/coq/coq/pull/9681>`_, - by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin). diff --git a/doc/changelog/04-tactics/09996-hint-mode.rst b/doc/changelog/04-tactics/09996-hint-mode.rst deleted file mode 100644 index 06e9059b45..0000000000 --- a/doc/changelog/04-tactics/09996-hint-mode.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Modes are now taken into account by :tacn:`typeclasses eauto` for - local hypotheses - (`#9996 <https://github.com/coq/coq/pull/9996>`_, - fixes `#5752 <https://github.com/coq/coq/issues/5752>`_, - by Maxime Dénès, review by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/10059-change-no-check.rst b/doc/changelog/04-tactics/10059-change-no-check.rst deleted file mode 100644 index 987b2a8ccd..0000000000 --- a/doc/changelog/04-tactics/10059-change-no-check.rst +++ /dev/null @@ -1,7 +0,0 @@ -- New variant :tacn:`change_no_check` of :tacn:`change`, usable as a - documented replacement of :tacn:`convert_concl_no_check` - (`#10012 <https://github.com/coq/coq/pull/10012>`_, - `#10017 <https://github.com/coq/coq/pull/10017>`_, - `#10053 <https://github.com/coq/coq/pull/10053>`_, and - `#10059 <https://github.com/coq/coq/pull/10059>`_, - by Hugo Herbelin and Paolo G. Giarrusso). diff --git a/doc/changelog/06-ssreflect/09995-notations.rst b/doc/changelog/06-ssreflect/09995-notations.rst deleted file mode 100644 index 3dfc45242d..0000000000 --- a/doc/changelog/06-ssreflect/09995-notations.rst +++ /dev/null @@ -1,8 +0,0 @@ -- `inE` now expands `y \in r x` when `r` is a `simpl_rel`. - New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion - class, simplified `predType` interface: `pred_class` and `mkPredType` - deprecated, `{pred T}` and `PredType` should be used instead. - `if c return t then ...` now expects `c` to be a variable bound in `t`. - New `nonPropType` interface matching types that do _not_ have sort `Prop`. - New `relpre R f` definition for the preimage of a relation R under f - (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier). diff --git a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst new file mode 100644 index 0000000000..78874cadb1 --- /dev/null +++ b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst @@ -0,0 +1,6 @@ +- Deprecated flag `Refine Instance Mode` has been removed. + (`#09530 <https://github.com/coq/coq/pull/09530>`_, fixes + `#3632 <https://github.com/coq/coq/issues/3632>`_, `#3890 + <https://github.com/coq/coq/issues/3890>`_ and `#4638 + <https://github.com/coq/coq/issues/4638>`_ + by Maxime Dénès, review by Gaëtan Gilbert). diff --git a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst b/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst deleted file mode 100644 index 732c088f45..0000000000 --- a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull` - (`#9984 <https://github.com/coq/coq/pull/9984>`_, - by Jean-Christophe Léchenet and Oliver Nash). diff --git a/doc/changelog/12-misc/09964-changes.rst b/doc/changelog/12-misc/09964-changes.rst deleted file mode 100644 index dd873cfdd5..0000000000 --- a/doc/changelog/12-misc/09964-changes.rst +++ /dev/null @@ -1,14 +0,0 @@ -- Changelog has been moved from a specific file `CHANGES.md` to the - reference manual; former Credits chapter of the reference manual has - been split in two parts: a History chapter which was enriched with - additional historical information about Coq versions 1 to 5, and a - Changes chapter which was enriched with the content formerly in - `CHANGES.md` and `COMPATIBILITY` - (`#9133 <https://github.com/coq/coq/pull/9133>`_, - `#9668 <https://github.com/coq/coq/pull/9668>`_, - `#9939 <https://github.com/coq/coq/pull/9939>`_, - `#9964 <https://github.com/coq/coq/pull/9964>`_, - and `#10085 <https://github.com/coq/coq/pull/10085>`_, - by Théo Zimmermann, - with help and ideas from Emilio Jesús Gallego Arias, Gaëtan - Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi). diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 881f7a310d..b20669c7f1 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -60,8 +60,11 @@ The signatures of most objects can be written using a succinct DSL for Coq notat ``{*, …}``, ``{+, …}`` an optional or mandatory repeatable block, with repetitions separated by commas -``%|``, ``%{``, … - an escaped character (rendered without the leading ``%``) +``{| … | … | … }`` + an alternative, indicating than one of multiple constructs can be used + +``%{``, ``%}``, ``%|`` + an escaped character (rendered without the leading ``%``). In most cases, escaping is not necessary. In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``. But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``. (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.) .. FIXME document the new subscript support @@ -148,7 +151,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica Example:: .. prodn:: term += let: @pattern := @term in @term - .. prodn:: occ_switch ::= { {? + %| - } {* @num } } + .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } } ``.. table::`` :black_nib: A Coq table, i.e. a setting that is a set of values. Example:: diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 78803a927f..2093765608 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -60,8 +60,11 @@ The signatures of most objects can be written using a succinct DSL for Coq notat ``{*, …}``, ``{+, …}`` an optional or mandatory repeatable block, with repetitions separated by commas -``%|``, ``%{``, … - an escaped character (rendered without the leading ``%``) +``{| … | … | … }`` + an alternative, indicating than one of multiple constructs can be used + +``%{``, ``%}``, ``%|`` + an escaped character (rendered without the leading ``%``). In most cases, escaping is not necessary. In particular, the following expressions are all parsed as plain text, and do not need escaping: ``{ xyz }``, ``x |- y``. But the following escapes *are* needed: ``{| a b %| c | d }``, ``all: %{``. (We use ``%`` instead of the usual ``\`` because you'd have to type ``\`` twice in your reStructuredText file.) .. FIXME document the new subscript support diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty index 75eac1f724..3548b8754c 100644 --- a/doc/sphinx/_static/coqnotations.sty +++ b/doc/sphinx/_static/coqnotations.sty @@ -18,6 +18,9 @@ \newlength{\nscriptsize} \setlength{\nscriptsize}{0.8em} +\newlength{\nboxsep} +\setlength{\nboxsep}{2pt} + \newcommand*{\scriptsmallsquarebox}[1]{% % Force width \makebox[\nscriptsize]{% @@ -31,7 +34,8 @@ \newcommand*{\nsup}[1]{^{\nscript{0.15}{#1}}} \newcommand*{\nsub}[1]{_{\nscript{0.35}{#1}}} \newcommand*{\nnotation}[1]{#1} -\newcommand*{\nrepeat}[1]{\text{\adjustbox{cfbox=nbordercolor 0.5pt 2pt,bgcolor=nbgcolor}{#1\hspace{.5\nscriptsize}}}} +\newcommand*{\nbox}[1]{\adjustbox{cfbox=nbordercolor 0.5pt \nboxsep,bgcolor=nbgcolor}{#1}} +\newcommand*{\nrepeat}[1]{\text{\nbox{#1\hspace{.5\nscriptsize}}}} \newcommand*{\nwrapper}[1]{\ensuremath{\displaystyle#1}} % https://tex.stackexchange.com/questions/310877/ \newcommand*{\nhole}[1]{\textit{\color{nholecolor}#1}} @@ -42,9 +46,32 @@ } % </magic> +% https://tex.stackexchange.com/questions/490262/ +\def\naltsep{} +\newsavebox{\nsavedalt} +\newlength{\naltvruleht} +\newlength{\naltvruledp} +\def\naltvrule{\smash{\vrule height\naltvruleht depth\naltvruledp}} +\newcommand{\nalternative}[2]{% + % First measure the contents of the box without the bar + \bgroup% + \def\naltsep{}% + \savebox{\nsavedalt}{#1}% + \setlength{\naltvruleht}{\ht\nsavedalt}% + \setlength{\naltvruledp}{\dp\nsavedalt}% + \addtolength{\naltvruleht}{#2}% + \addtolength{\naltvruledp}{#2}% + % Then redraw it with the bar + \def\naltsep{\naltvrule}% + #1\egroup} + \newcssclass{notation-sup}{\nsup{#1}} \newcssclass{notation-sub}{\nsub{#1}} \newcssclass{notation}{\nnotation{#1}} \newcssclass{repeat}{\nrepeat{#1}} \newcssclass{repeat-wrapper}{\nwrapper{#1}} \newcssclass{hole}{\nhole{#1}} +\newcssclass{alternative}{\nalternative{\nbox{#1}}{0pt}} +\newcssclass{alternative-block}{#1} +\newcssclass{repeated-alternative}{\nalternative{#1}{\nboxsep}} +\newcssclass{alternative-separator}{\quad\naltsep{}\quad} diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index dcb47d1786..8322ab0137 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -45,15 +45,46 @@ width: 2.2em; } -.notation .repeat { +.notation .repeat, .notation .alternative { background: #EAEAEA; border: 1px solid #AAA; display: inline-block; - padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */ - padding-left: 0.2em; + padding: 0 0.2em 0 0.3em; margin: 0.25em 0; } +.notation .repeated-alternative { + display: inline-table; +} + +.notation .alternative { + display: inline-table; + padding: 0 0.2em; +} + +.notation .alternative-block { + display: table-cell; + padding: 0 0.5em; +} + +.notation .alternative-separator { + border-left: 1px solid black; /* Display a thin bar */ + display: table-cell; + width: 0; +} + +.alternative-block:first-child { + padding-left: 0; +} + +.alternative-block:last-child { + padding-right: 0; +} + +.notation .repeat { + padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */ +} + .notation .repeat-wrapper { display: inline-block; position: relative; diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index e93b01f14d..8a895eb515 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -99,7 +99,7 @@ Extraction Options Setting the target language ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Extraction Language ( OCaml | Haskell | Scheme ) +.. cmd:: Extraction Language {| OCaml | Haskell | Scheme } :name: Extraction Language The ability to fix target language is the first and more important diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index b474c51f17..847abb33fc 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -170,12 +170,12 @@ compatibility constraints. Adding new relations and morphisms ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident +.. cmd:: Add Parametric Relation @binders : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident This command declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`, :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`. - The :token:`ident` gives a unique name to the morphism and it is used + The final :token:`ident` gives a unique name to the morphism and it is used by the command to generate fresh names for automatically provided lemmas used internally. @@ -219,15 +219,16 @@ replace terms with related ones only in contexts that are syntactic compositions of parametric morphism instances declared with the following command. -.. cmd:: Add Parametric Morphism (x1 : T1) ... (xk : Tk) : (f t1 ... tn) with signature sig as @ident +.. cmd:: Add Parametric Morphism @binders : (@ident {+ @term__1}) with signature @term__2 as @ident - This command declares ``f`` as a parametric morphism of signature ``sig``. The - identifier :token:`ident` gives a unique name to the morphism and it is used as - the base name of the typeclass instance definition and as the name of - the lemma that proves the well-definedness of the morphism. The - parameters of the morphism as well as the signature may refer to the - context of variables. The command asks the user to prove interactively - that ``f`` respects the relations identified from the signature. + This command declares a parametric morphism :n:`@ident {+ @term__1}` of + signature :n:`@term__2`. The final identifier :token:`ident` gives a unique + name to the morphism and it is used as the base name of the typeclass + instance definition and as the name of the lemma that proves the + well-definedness of the morphism. The parameters of the morphism as well as + the signature may refer to the context of variables. The command asks the + user to prove interactively that the function denoted by the first + :token:`ident` respects the relations identified from the signature. .. example:: @@ -577,7 +578,7 @@ Deprecated syntax and backward incompatibilities Notice that the syntax is not completely backward compatible since the identifier was not required. -.. cmd:: Add Morphism f : @ident +.. cmd:: Add Morphism @ident : @ident :name: Add Morphism This command is restricted to the declaration of morphisms @@ -809,7 +810,7 @@ Usage ~~~~~ -.. tacn:: rewrite_strat @s [in @ident] +.. tacn:: rewrite_strat @s {? in @ident } :name: rewrite_strat Rewrite using the strategy s in hypothesis ident or the conclusion. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index b410833d25..22ddcae584 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -283,7 +283,7 @@ optional identifier is used when multiple functions have unsolved obligations (e.g. when defining mutually recursive blocks). The optional tactic is replaced by the default one if not specified. -.. cmd:: {? Local|Global} Obligation Tactic := @tactic +.. cmd:: {? {| Local | Global } } Obligation Tactic := @tactic :name: Obligation Tactic Sets the default obligation solving tactic applied to all obligations diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 77a6ee79cc..65934efaa6 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -311,24 +311,24 @@ Summary of the commands This command has no effect when used on a typeclass. -.. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } +.. cmd:: Instance @ident {? @binders} : @term__0 {+ @term} {? | @num} := { {*; @field_def} } This command is used to declare a typeclass instance named - :token:`ident` of the class :token:`class` with parameters ``t1`` to ``tn`` and - fields ``b1`` to ``bi``, where each field must be a declared field of - the class. Missing fields must be filled in interactive proof mode. + :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and + fields defined by :token:`field_def`, where each field must be a declared field of + the class. An arbitrary context of :token:`binders` can be put after the name of the instance and before the colon to declare a parameterized instance. An optional priority can be declared, 0 being the highest priority as for - :tacn:`auto` hints. If the priority is not specified, it defaults to the number + :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number of non-dependent binders of the instance. - .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term + .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @term__0 {+ @term} {? | @num } := @term This syntax is used for declaration of singleton class instances or - for directly giving an explicit term of type :n:`forall @binders, @class - @term__1 … @term__n`. One need not even mention the unique field name for + for directly giving an explicit term of type :n:`forall @binders, @term__0 + {+ @term}`. One need not even mention the unique field name for singleton classes. .. cmdv:: Global Instance @@ -356,11 +356,11 @@ Summary of the commands Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a few other commands related to typeclasses. -.. cmd:: Existing Instance {+ @ident} [| priority] +.. cmd:: Existing Instance {+ @ident} {? | @num} This command adds an arbitrary list of constants whose type ends with an applied typeclass to the instance database with an optional - priority. It can be used for redeclaring instances at the end of + priority :token:`num`. It can be used for redeclaring instances at the end of sections, or declaring structure projections as instances. This is equivalent to ``Hint Resolve ident : typeclass_instances``, except it registers instances for :cmd:`Print Instances`. @@ -408,7 +408,7 @@ few other commands related to typeclasses. + When considering local hypotheses, we use the union of all the modes declared in the given databases. - .. cmdv:: typeclasses eauto @num + .. tacv:: typeclasses eauto @num .. warning:: The semantics for the limit :n:`@num` @@ -417,7 +417,7 @@ few other commands related to typeclasses. counted, which might result in larger limits being necessary when searching with ``typeclasses eauto`` than with :tacn:`auto`. - .. cmdv:: typeclasses eauto with {+ @ident} + .. tacv:: typeclasses eauto with {+ @ident} This variant runs resolution with the given hint databases. It treats typeclass subgoals the same as other subgoals (no shelving of @@ -563,23 +563,10 @@ Settings of goals. Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this option to 0 turns that option off. -.. flag:: Refine Instance Mode - - .. deprecated:: 8.10 - - This flag allows to switch the behavior of instance declarations made through - the Instance command. - - + When it is off (the default), they fail with an error instead. - - + When it is on, instances that have unsolved holes in - their proof-term silently open the proof mode with the remaining - obligations to prove. - Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Typeclasses eauto := {? debug} {? (dfs) | (bfs) } @num +.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @num :name: Typeclasses eauto This command allows more global customization of the typeclass diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 574b943a78..cc2c43e7dd 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -355,6 +355,11 @@ Other changes in 8.10+beta1 that will do it automatically, using the output of ``coqc`` (`#8638 <https://github.com/coq/coq/pull/8638>`_, by Jason Gross). + - Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar` + (`#10061 <https://github.com/coq/coq/pull/10061>`_, + fixes `#9681 <http://github.com/coq/coq/pull/9681>`_, + by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin). + - The `quote plugin <https://coq.inria.fr/distrib/V8.9.0/refman/proof-engine/detailed-tactic-examples.html#quote>`_ was removed. If some users are interested in maintaining this plugin @@ -400,7 +405,32 @@ Other changes in 8.10+beta1 closes `#7632 <https://github.com/coq/coq/issues/7632>`_, by Théo Zimmermann). - - SSReflect clear discipline made consistent across the entire proof language. + - Modes are now taken into account by :tacn:`typeclasses eauto` for + local hypotheses + (`#9996 <https://github.com/coq/coq/pull/9996>`_, + fixes `#5752 <https://github.com/coq/coq/issues/5752>`_, + by Maxime Dénès, review by Pierre-Marie Pédrot). + + - New variant :tacn:`change_no_check` of :tacn:`change`, usable as a + documented replacement of :tacn:`convert_concl_no_check` + (`#10012 <https://github.com/coq/coq/pull/10012>`_, + `#10017 <https://github.com/coq/coq/pull/10017>`_, + `#10053 <https://github.com/coq/coq/pull/10053>`_, and + `#10059 <https://github.com/coq/coq/pull/10059>`_, + by Hugo Herbelin and Paolo G. Giarrusso). + + - The simplified value returned by :tacn:`field_simplify` is not + always a fraction anymore. When the denominator is :g:`1`, it + returns :g:`x` while previously it was returning :g:`x/1`. This + change could break codes that were post-processing application of + :tacn:`field_simplify` to get rid of these :g:`x/1` + (`#9854 <https://github.com/coq/coq/pull/9854>`_, + by Laurent Théry, + with help from Michael Soegtrop, Maxime Dénès, and Vincent Laporte). + +- SSReflect: + + - Clear discipline made consistent across the entire proof language. Whenever a clear switch `{x..}` comes immediately before an existing proof context entry (used as a view, as a rewrite rule or as name for a new context entry) then such entry is cleared too. @@ -414,6 +444,15 @@ Other changes in 8.10+beta1 (`#9341 <https://github.com/coq/coq/pull/9341>`_, by Enrico Tassi). + - `inE` now expands `y \in r x` when `r` is a `simpl_rel`. + New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion + class, simplified `predType` interface: `pred_class` and `mkPredType` + deprecated, `{pred T}` and `PredType` should be used instead. + `if c return t then ...` now expects `c` to be a variable bound in `t`. + New `nonPropType` interface matching types that do _not_ have sort `Prop`. + New `relpre R f` definition for the preimage of a relation R under f + (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier). + - Vernacular commands: - Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`. @@ -447,10 +486,9 @@ Other changes in 8.10+beta1 - :cmd:`Declare Instance` now requires an instance name. - The flag :flag:`Refine Instance Mode` has been turned off by default, - meaning that :cmd:`Instance` no longer opens a proof when a body is - provided. The flag has been deprecated and will be removed in the next - version. + The flag `Refine Instance Mode` has been turned off by default, meaning that + :cmd:`Instance` no longer opens a proof when a body is provided. The flag + has been deprecated and will be removed in the next version. (`#9270 <https://github.com/coq/coq/pull/9270>`_, and `#9825 <https://github.com/coq/coq/pull/9825>`_, @@ -459,7 +497,7 @@ Other changes in 8.10+beta1 - Command :cmd:`Instance`, when no body is provided, now always opens a proof. This is a breaking change, as instance of :n:`Instance @ident__1 : @ident__2.` where :n:`@ident__2` is a trivial class will - have to be changed into :n:`Instance @ident__1 : @ident__2 := {}.` + have to be changed into :n:`Instance @ident__1 : @ident__2 := %{%}.` or :n:`Instance @ident__1 : @ident__2. Proof. Qed.` (`#9274 <https://github.com/coq/coq/pull/9274>`_, by Maxime Dénès). @@ -535,10 +573,28 @@ Other changes in 8.10+beta1 `fset` database (`#9725 <https://github.com/coq/coq/pull/9725>`_, by Frédéric Besson). + - Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull` + (`#9984 <https://github.com/coq/coq/pull/9984>`_, + by Jean-Christophe Léchenet and Oliver Nash). + - Some error messages that show problems with a pair of non-matching values will now highlight the differences (`#8669 <https://github.com/coq/coq/pull/8669>`_, by Jim Fehrle). +- Changelog has been moved from a specific file `CHANGES.md` to the + reference manual; former Credits chapter of the reference manual has + been split in two parts: a History chapter which was enriched with + additional historical information about Coq versions 1 to 5, and a + Changes chapter which was enriched with the content formerly in + `CHANGES.md` and `COMPATIBILITY` + (`#9133 <https://github.com/coq/coq/pull/9133>`_, + `#9668 <https://github.com/coq/coq/pull/9668>`_, + `#9939 <https://github.com/coq/coq/pull/9939>`_, + `#9964 <https://github.com/coq/coq/pull/9964>`_, + and `#10085 <https://github.com/coq/coq/pull/10085>`_, + by Théo Zimmermann, + with help and ideas from Emilio Jesús Gallego Arias, Gaëtan + Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi). Version 8.9 ----------- @@ -3883,7 +3939,7 @@ Vernacular commands Equality Schemes", this replaces deprecated option "Equality Scheme"). - Made support for automatic generation of case analysis schemes available to user (governed by option "Set Case Analysis Schemes"). -- New command :n:`{? Global } Generalizable [All|No] [Variable|Variables] {* @ident}` to +- New command :n:`{? Global } Generalizable {| All | No } {| Variable | Variables } {* @ident}` to declare which identifiers are generalizable in `` `{} `` and `` `() `` binders. - New command "Print Opaque Dependencies" to display opaque constants in addition to all variables, parameters or axioms a theorem or diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index ba766c8c3d..5e214f6f7f 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -85,7 +85,7 @@ To build an object of type :token:`ident`, one should provide the constructor .. productionlist:: record_term : {| [`field_def` ; … ; `field_def`] |} - field_def : name [binders] := `record_term` + field_def : `ident` [`binders`] := `term` Alternatively, the following syntax allows creating objects by using named fields, as shown in this grammar. The fields do not have to be in any particular order, nor do they have @@ -831,16 +831,16 @@ Sections create local contexts which can be shared across multiple definitions. Links :token:`type` to each :token:`ident`. - .. cmdv:: Variable {+ ( {+ @ident } : @type ) } + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } Declare one or more variables with various types. - .. cmdv:: Variables {+ ( {+ @ident } : @type) } - Hypothesis {+ ( {+ @ident } : @type) } - Hypotheses {+ ( {+ @ident } : @type) } + .. cmdv:: Variables {+ ( {+ @ident } : @type) } + Hypothesis {+ ( {+ @ident } : @type) } + Hypotheses {+ ( {+ @ident } : @type) } :name: Variables; Hypothesis; Hypotheses - These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. + These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. .. cmd:: Let @ident := @term @@ -931,7 +931,7 @@ In the syntax of module application, the ! prefix indicates that any :token:`module_binding`. The output module type is verified against each :token:`module_type`. -.. cmdv:: Module [ Import | Export ] +.. cmdv:: Module {| Import | Export } Behaves like :cmd:`Module`, but automatically imports or exports the module. @@ -1648,7 +1648,7 @@ Declaring Implicit Arguments -.. cmd:: Arguments @qualid {* [ @ident ] | { @ident } | @ident } +.. cmd:: Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } :name: Arguments (implicits) This command is used to set implicit arguments *a posteriori*, @@ -1665,20 +1665,20 @@ Declaring Implicit Arguments This command clears implicit arguments. -.. cmdv:: Global Arguments @qualid {* [ @ident ] | { @ident } | @ident } +.. cmdv:: Global Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } This command is used to recompute the implicit arguments of :token:`qualid` after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -.. cmdv:: Local Arguments @qualid {* [ @ident ] | { @ident } | @ident } +.. cmdv:: Local Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } When in a module, tell not to activate the implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | { @ident } | @ident } } +.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @ident ] | { @ident } | @ident } } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of @@ -2167,7 +2167,7 @@ that specify which variables should be generalizable. Disable implicit generalization entirely. This is the default behavior. -.. cmd:: Generalizable (Variable | Variables) {+ @ident } +.. cmd:: Generalizable {| Variable | Variables } {+ @ident } Allow generalization of the given identifiers only. Calling this command multiple times adds to the allowed identifiers. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 5a1af9f9fa..8acbcbec8f 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -616,34 +616,34 @@ has type :token:`type`. Adds several parameters with specification :token:`type`. - .. cmdv:: Parameter {+ ( {+ @ident } : @type ) } + .. cmdv:: Parameter {+ ( {+ @ident } : @type ) } Adds blocks of parameters with different specifications. - .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) } + .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) } :name: Local Parameter Such parameters are never made accessible through their unqualified name by :cmd:`Import` and its variants. You have to explicitly give their fully qualified name to refer to them. - .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) } - {? Local } Axiom {+ ( {+ @ident } : @type ) } - {? Local } Axioms {+ ( {+ @ident } : @type ) } - {? Local } Conjecture {+ ( {+ @ident } : @type ) } - {? Local } Conjectures {+ ( {+ @ident } : @type ) } + .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) } + {? Local } Axiom {+ ( {+ @ident } : @type ) } + {? Local } Axioms {+ ( {+ @ident } : @type ) } + {? Local } Conjecture {+ ( {+ @ident } : @type ) } + {? Local } Conjectures {+ ( {+ @ident } : @type ) } :name: Parameters; Axiom; Axioms; Conjecture; Conjectures - These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. + These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. - .. cmdv:: Variable {+ ( {+ @ident } : @type ) } - Variables {+ ( {+ @ident } : @type ) } - Hypothesis {+ ( {+ @ident } : @type ) } - Hypotheses {+ ( {+ @ident } : @type ) } + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } + Variables {+ ( {+ @ident } : @type ) } + Hypothesis {+ ( {+ @ident } : @type ) } + Hypotheses {+ ( {+ @ident } : @type ) } :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section) Outside of any section, these variants are synonyms of - :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. + :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. For their meaning inside a section, see :cmd:`Variable` in :ref:`section-mechanism`. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index a7eb7c2319..bbd7e0ba3d 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -360,7 +360,7 @@ Detecting progress We can check if a tactic made progress with: -.. tacn:: progress expr +.. tacn:: progress @expr :name: progress :n:`@expr` is evaluated to v which must be a tactic value. The tactic value ``v`` @@ -555,7 +555,7 @@ Identity The constant :n:`idtac` is the identity tactic: it leaves any goal unchanged but it appears in the proof script. -.. tacn:: idtac {* message_token} +.. tacn:: idtac {* @message_token} :name: idtac This prints the given tokens. Strings and integers are printed @@ -684,7 +684,7 @@ Timing a tactic that evaluates to a term Tactic expressions that produce terms can be timed with the experimental tactic -.. tacn:: time_constr expr +.. tacn:: time_constr @expr :name: time_constr which evaluates :n:`@expr ()` and displays the time the tactic expression @@ -880,7 +880,7 @@ We can perform pattern matching on goals using the following expression: .. we should provide the full grammar here -.. tacn:: match goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end +.. tacn:: match goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end :name: match goal If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is @@ -918,7 +918,7 @@ We can perform pattern matching on goals using the following expression: first), but it possible to reverse this order (oldest first) with the :n:`match reverse goal with` variant. - .. tacv:: multimatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end + .. tacv:: multimatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end Using :n:`multimatch` instead of :n:`match` will allow subsequent tactics to backtrack into a right-hand side tactic which has backtracking points @@ -929,7 +929,7 @@ We can perform pattern matching on goals using the following expression: The syntax :n:`match [reverse] goal …` is, in fact, a shorthand for :n:`once multimatch [reverse] goal …`. - .. tacv:: lazymatch goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end + .. tacv:: lazymatch goal with {+| {+, @context_hyp} |- @cpattern => @expr } | _ => @expr end Using lazymatch instead of match will perform the same pattern matching procedure but will commit to the first matching branch with the first @@ -1135,33 +1135,33 @@ Defining |Ltac| functions Basically, |Ltac| toplevel definitions are made as follows: -.. cmd:: Ltac @ident {* @ident} := @expr +.. cmd:: {? Local} Ltac @ident {* @ident} := @expr + :name: Ltac This defines a new |Ltac| function that can be used in any tactic script or new |Ltac| toplevel definition. + If preceded by the keyword ``Local``, the tactic definition will not be + exported outside the current module. + .. note:: The preceding definition can equivalently be written: :n:`Ltac @ident := fun {+ @ident} => @expr` - Recursive and mutual recursive function definitions are also possible - with the syntax: - .. cmdv:: Ltac @ident {* @ident} {* with @ident {* @ident}} := @expr - It is also possible to *redefine* an existing user-defined tactic using the syntax: + This syntax allows recursive and mutual recursive function definitions. .. cmdv:: Ltac @qualid {* @ident} ::= @expr + This syntax *redefines* an existing user-defined tactic. + A previous definition of qualid must exist in the environment. The new definition will always be used instead of the old one and it goes across module boundaries. - If preceded by the keyword Local the tactic definition will not be - exported outside the current module. - Printing |Ltac| tactics ~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 6e33862b39..aa603fc966 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -668,7 +668,7 @@ A scope is a name given to a grammar entry used to produce some Ltac2 expression at parsing time. Scopes are described using a form of S-expression. .. prodn:: - ltac2_scope ::= @string %| @integer %| @lident ({+, @ltac2_scope}) + ltac2_scope ::= {| @string | @integer | @lident ({+, @ltac2_scope}) } A few scopes contain antiquotation features. For sake of uniformity, all antiquotations are introduced by the syntax :n:`$@lident`. @@ -751,7 +751,7 @@ Notations The Ltac2 parser can be extended by syntactic notations. -.. cmd:: Ltac2 Notation {+ @lident (@ltac2_scope) %| @string } {? : @integer} := @ltac2_term +.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @integer} := @ltac2_term :name: Ltac2 Notation A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded @@ -823,9 +823,9 @@ Ltac2 features a toplevel loop that can be used to evaluate expressions. Debug ----- -.. opt:: Ltac2 Backtrace +.. flag:: Ltac2 Backtrace - When this option is set, toplevel failures will be printed with a backtrace. + When this flag is set, toplevel failures will be printed with a backtrace. Compatibility layer with Ltac1 ------------------------------ @@ -966,7 +966,7 @@ errors produced by the typechecker. In Ltac expressions +++++++++++++++++++ -.. exn:: Unbound ( value | constructor ) X +.. exn:: Unbound {| value | constructor } X * if `X` is meant to be a term from the current stactic environment, replace the problematic use by `'X`. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 16b158c397..4a2f9c0db3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -322,7 +322,7 @@ Navigation in the proof tree .. index:: { } -.. cmd:: %{ %| %} +.. cmd:: {| %{ | %} } The command ``{`` (without a terminating period) focuses on the first goal, much like :cmd:`Focus` does, however, the subproof can only be @@ -430,7 +430,7 @@ not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further nesting levels provided they are delimited by these. Bullets are made of repeated ``-``, ``+`` or ``*`` symbols: -.. prodn:: bullet ::= {+ - } %| {+ + } %| {+ * } +.. prodn:: bullet ::= {| {+ - } | {+ + } | {+ * } } Note again that when a focused goal is proved a message is displayed together with a suggestion about the right bullet or ``}`` to unfocus it @@ -492,7 +492,7 @@ The following example script illustrates all these features: Set Bullet Behavior ``````````````````` -.. opt:: Bullet Behavior %( "None" %| "Strict Subproofs" %) +.. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } :name: Bullet Behavior This option controls the bullet behavior and can take two possible values: @@ -544,9 +544,9 @@ Requesting information ``<Your Tactic Text here>``. - .. deprecated:: 8.10 + .. deprecated:: 8.10 - Please use a text editor. + Please use a text editor. .. cmdv:: Show Proof :name: Show Proof @@ -680,7 +680,7 @@ This image shows an error message with diff highlighting in CoqIDE: How to enable diffs ``````````````````` -.. opt:: Diffs %( "on" %| "off" %| "removed" %) +.. opt:: Diffs {| "on" | "off" | "removed" } :name: Diffs The “on” setting highlights added tokens in green, while the “removed” setting diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 4e40df6f94..75e019592f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -617,7 +617,7 @@ Abbreviations selected occurrences of a term. .. prodn:: - occ_switch ::= { {? + %| - } {* @num } } + occ_switch ::= { {? {| + | - } } {* @num } } where: @@ -2273,7 +2273,7 @@ to the others. Iteration ~~~~~~~~~ -.. tacn:: do {? @num } ( @tactic | [ {+| @tactic } ] ) +.. tacn:: do {? @num } {| @tactic | [ {+| @tactic } ] } :name: do (ssreflect) This tactical offers an accurate control on the repetition of tactics. @@ -2300,7 +2300,7 @@ tactic should be repeated on the current subgoal. There are four kinds of multipliers: .. prodn:: - mult ::= @num ! %| ! %| @num ? %| ? + mult ::= {| @num ! | ! | @num ? | ? } Their meaning is: @@ -2571,7 +2571,7 @@ destruction of existential assumptions like in the tactic: An alternative use of the ``have`` tactic is to provide the explicit proof term for the intermediate lemma, using tactics of the form: -.. tacv:: have {? @ident } := term +.. tacv:: have {? @ident } := @term This tactic creates a new assumption of type the type of :token:`term`. If the @@ -5444,7 +5444,7 @@ equivalences are indeed taken into account, otherwise only single |SSR| searching tool -------------------- -.. cmd:: Search {? @pattern } {* {? - } %( @string %| @pattern %) {? % @ident} } {? in {+ {? - } @qualid } } +.. cmd:: Search {? @pattern } {* {? - } {| @string | @pattern } {? % @ident} } {? in {+ {? - } @qualid } } :name: Search (ssreflect) This is the |SSR| extension of the Search command. :token:`qualid` is the @@ -5686,7 +5686,7 @@ respectively. local cofix definition -.. tacn:: set @ident {? : @term } := {? @occ_switch } %( @term %| ( @c_pattern) %) +.. tacn:: set @ident {? : @term } := {? @occ_switch } {| @term | ( @c_pattern) } abbreviation (see :ref:`abbreviations_ssr`) @@ -5714,26 +5714,26 @@ introduction see :ref:`introduction_ssr` localization see :ref:`localization_ssr` -.. prodn:: tactic += do {? @mult } %( @tactic %| [ {+| @tactic } ] %) +.. prodn:: tactic += do {? @mult } {| @tactic | [ {+| @tactic } ] } iteration see :ref:`iteration_ssr` -.. prodn:: tactic += @tactic ; %( first %| last %) {? @num } %( @tactic %| [ {+| @tactic } ] %) +.. prodn:: tactic += @tactic ; {| first | last } {? @num } {| @tactic | [ {+| @tactic } ] } selector see :ref:`selectors_ssr` -.. prodn:: tactic += @tactic ; %( first %| last %) {? @num } +.. prodn:: tactic += @tactic ; {| first | last } {? @num } rotation see :ref:`selectors_ssr` -.. prodn:: tactic += by %( @tactic %| [ {*| @tactic } ] %) +.. prodn:: tactic += by {| @tactic | [ {*| @tactic } ] } closing see :ref:`terminators_ssr` Commands ~~~~~~~~ -.. cmd:: Hint View for %( move %| apply %) / @ident {? | @num } +.. cmd:: Hint View for {| move | apply } / @ident {? | @num } view hint declaration (see :ref:`declaring_new_hints_ssr`) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index c728b925ac..4e47621938 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1749,7 +1749,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``, and ``in`` clauses. -.. tacn:: case term +.. tacn:: case @term :name: case The tactic :n:`case` is a more basic tactic to perform case analysis without @@ -1982,7 +1982,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) :n:`induction @ident; induction @ident` (or :n:`induction @ident ; destruct @ident` depending on the exact needs). -.. tacv:: double induction num1 num2 +.. tacv:: double induction @num__1 @num__2 This tactic is deprecated and should be replaced by :n:`induction num1; induction num3` where :n:`num3` is the result @@ -2271,11 +2271,11 @@ and an explanation of the underlying technique. :undocumented: .. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern} - injection @num as {+ simple_intropattern} - injection as {+ simple_intropattern} - einjection @term {? with @bindings_list} as {+ simple_intropattern} - einjection @num as {+ simple_intropattern} - einjection as {+ simple_intropattern} + injection @num as {+ @simple_intropattern} + injection as {+ @simple_intropattern} + einjection @term {? with @bindings_list} as {+ @simple_intropattern} + einjection @num as {+ @simple_intropattern} + einjection as {+ @simple_intropattern} These variants apply :n:`intros {+ @simple_intropattern}` after the call to :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in @@ -2637,7 +2637,7 @@ and an explanation of the underlying technique. is correct at some time of the interactive development of a proof, use the command ``Guarded`` (see Section :ref:`requestinginformation`). -.. tacv:: fix @ident @num with {+ (ident {+ @binder} [{struct @ident}] : @type)} +.. tacv:: fix @ident @num with {+ (@ident {+ @binder} [{struct @ident}] : @type)} This starts a proof by mutual induction. The statements to be simultaneously proved are respectively :g:`forall binder ... binder, type`. @@ -3777,8 +3777,8 @@ The general command to add a hint to some databases :n:`{+ @ident}` is discrimination network to relax or constrain it in the case of discriminated databases. - .. cmdv:: Hint Variables %( Transparent %| Opaque %) : @ident - Hint Constants %( Transparent %| Opaque %) : @ident + .. cmdv:: Hint Variables {| Transparent | Opaque } : @ident + Hint Constants {| Transparent | Opaque } : @ident :name: Hint Variables; Hint Constants This sets the transparency flag used during unification of @@ -3850,7 +3850,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is semantics of :n:`Hint Cut @regexp` is to set the cut expression to :n:`c | regexp`, the initial cut expression being `emp`. - .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident + .. cmdv:: Hint Mode @qualid {* {| + | ! | - } } : @ident :name: Hint Mode This sets an optional mode of use of the identifier :n:`@qualid`. When @@ -4016,7 +4016,7 @@ We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior option which accepts three flags allowing for a fine-grained handling of non-imported hints. -.. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %) +.. opt:: Loose Hint Behavior {| "Lax" | "Warn" | "Strict" } :name: Loose Hint Behavior This option accepts three values, which control the behavior of hints w.r.t. @@ -4048,7 +4048,7 @@ Setting implicit automation tactics .. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`. - .. cmdv:: Proof with tactic using {+ @ident} + .. cmdv:: Proof with @tactic using {+ @ident} Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` @@ -4400,6 +4400,11 @@ Equality This tactic applies to a goal that has the form :g:`t=u` and transforms it into the two subgoals :n:`t=@term` and :n:`@term=u`. + .. tacv:: etransitivity + + This tactic behaves like :tacn:`transitivity`, using a fresh evar instead of + a concrete :token:`term`. + Equality and inductive sets --------------------------- diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index e207a072cc..26dc4e02cf 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -91,13 +91,13 @@ and tables: Flags, options and tables are identified by a series of identifiers, each with an initial capital letter. -.. cmd:: {? Local | Global | Export } Set @flag +.. cmd:: {? {| Local | Global | Export } } Set @flag :name: Set Sets :token:`flag` on. Scoping qualifiers are described :ref:`here <set_unset_scope_qualifiers>`. -.. cmd:: {? Local | Global | Export } Unset @flag +.. cmd:: {? {| Local | Global | Export } } Unset @flag :name: Unset Sets :token:`flag` off. Scoping qualifiers are @@ -108,13 +108,13 @@ capital letter. Prints the current value of :token:`flag`. -.. cmd:: {? Local | Global | Export } Set @option ( @num | @string ) +.. cmd:: {? {| Local | Global | Export } } Set @option {| @num | @string } :name: Set @option Sets :token:`option` to the specified value. Scoping qualifiers are described :ref:`here <set_unset_scope_qualifiers>`. -.. cmd:: {? Local | Global | Export } Unset @option +.. cmd:: {? {| Local | Global | Export } } Unset @option :name: Unset @option Sets :token:`option` to its default value. Scoping qualifiers are @@ -129,17 +129,17 @@ capital letter. Prints the current value of all flags and options, and the names of all tables. -.. cmd:: Add @table ( @string | @qualid ) +.. cmd:: Add @table {| @string | @qualid } :name: Add @table Adds the specified value to :token:`table`. -.. cmd:: Remove @table ( @string | @qualid ) +.. cmd:: Remove @table {| @string | @qualid } :name: Remove @table Removes the specified value from :token:`table`. -.. cmd:: Test @table for ( @string | @qualid ) +.. cmd:: Test @table for {| @string | @qualid } :name: Test @table for Reports whether :token:`table` contains the specified value. @@ -162,7 +162,7 @@ capital letter. Scope qualifiers for :cmd:`Set` and :cmd:`Unset` ````````````````````````````````````````````````` -:n:`{? Local | Global | Export }` +:n:`{? {| Local | Global | Export } }` Flag and option settings can be global in scope or local to nested scopes created by :cmd:`Module` and :cmd:`Section` commands. There are four alternatives: @@ -277,7 +277,7 @@ Requests to the environment :token:`term_pattern` (holes of the pattern are either denoted by `_` or by :n:`?@ident` when non linear patterns are expected). - .. cmdv:: Search { + [-]@term_pattern_string } + .. cmdv:: Search {+ {? -}@term_pattern_string} where :n:`@term_pattern_string` is a term_pattern, a string, or a string followed @@ -289,17 +289,17 @@ Requests to the environment prefixed by `-`, the search excludes the objects that mention that term_pattern or that string. - .. cmdv:: Search @term_pattern_string … @term_pattern_string inside {+ @qualid } + .. cmdv:: Search {+ {? -}@term_pattern_string} inside {+ @qualid } This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. - .. cmdv:: Search @term_pattern_string … @term_pattern_string outside {+ @qualid } + .. cmdv:: Search {+ {? -}@term_pattern_string} outside {+ @qualid } This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence. - .. cmdv:: @selector: Search [-]@term_pattern_string … [-]@term_pattern_string + .. cmdv:: @selector: Search {+ {? -}@term_pattern_string} This specifies the goal on which to search hypothesis (see Section :ref:`invocation-of-tactics`). @@ -353,7 +353,7 @@ Requests to the environment This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. - .. cmdv:: SearchHead term outside {+ @qualid } + .. cmdv:: SearchHead @term outside {+ @qualid } This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence. @@ -443,7 +443,7 @@ Requests to the environment SearchRewrite (_ + _ + _). - .. cmdv:: SearchRewrite term inside {+ @qualid } + .. cmdv:: SearchRewrite @term inside {+ @qualid } This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence. @@ -622,7 +622,7 @@ file is a particular case of module called *library file*. but if a further module, say `A`, contains a command :cmd:`Require Export` `B`, then the command :cmd:`Require Import` `A` also imports the module `B.` - .. cmdv:: Require [Import | Export] {+ @qualid } + .. cmdv:: Require {| Import | Export } {+ @qualid } This loads the modules named by the :token:`qualid` sequence and their recursive @@ -988,7 +988,7 @@ Controlling display This option controls the normal displaying. -.. opt:: Warnings "{+, {? %( - %| + %) } @ident }" +.. opt:: Warnings "{+, {? {| - | + } } @ident }" :name: Warnings This option configures the display of warnings. It is experimental, and diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 418922e9b3..3a12ee288a 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -336,29 +336,32 @@ Generation of induction principles with ``Functional`` ``Scheme`` Generation of inversion principles with ``Derive`` ``Inversion`` ----------------------------------------------------------------- -.. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort +.. cmd:: Derive Inversion @ident with @ident Sort @sort + Derive Inversion @ident with (forall @binders, @ident @term) Sort @sort This command generates an inversion principle for the - :tacn:`inversion ... using ...` tactic. Let :g:`I` be an inductive - predicate and :g:`x` the variables occurring in t. This command - generates and stocks the inversion lemma for the sort :g:`sort` - corresponding to the instance :g:`∀ (x:T), I t` with the name - :n:`@ident` in the global environment. When applied, it is - equivalent to having inverted the instance with the tactic - :g:`inversion`. - + :tacn:`inversion ... using ...` tactic. The first :token:`ident` is the name + of the generated principle. The second :token:`ident` should be an inductive + predicate, and :token:`binders` the variables occurring in the term + :token:`term`. This command generates the inversion lemma for the sort + :token:`sort` corresponding to the instance :n:`forall @binders, @ident @term`. + When applied, it is equivalent to having inverted the instance with the + tactic :g:`inversion`. -.. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort @sort +.. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort + Derive Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic inversion replaced by the tactic `inversion_clear`. -.. cmdv:: Derive Dependent Inversion @ident with forall (x:T), I t Sort @sort +.. cmdv:: Derive Dependent Inversion @ident with @ident Sort @sort + Derive Dependent Inversion @ident with (forall @binders, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion`. -.. cmdv:: Derive Dependent Inversion_clear @ident with forall(x:T), I t Sort @sort +.. cmdv:: Derive Dependent Inversion_clear @ident with @ident Sort @sort + Derive Dependent Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion_clear`. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index edec13f681..cda228a7da 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -327,22 +327,29 @@ symbols. Reserving notations ~~~~~~~~~~~~~~~~~~~ -A given notation may be used in different contexts. Coq expects all -uses of the notation to be defined at the same precedence and with the -same associativity. To avoid giving the precedence and associativity -every time, it is possible to declare a parsing rule in advance -without giving its interpretation. Here is an example from the initial -state of Coq. +.. cmd:: Reserved Notation @string {? (@modifiers) } -.. coqtop:: in + A given notation may be used in different contexts. Coq expects all + uses of the notation to be defined at the same precedence and with the + same associativity. To avoid giving the precedence and associativity + every time, this command declares a parsing rule (:token:`string`) in advance + without giving its interpretation. Here is an example from the initial + state of Coq. + + .. coqtop:: in + + Reserved Notation "x = y" (at level 70, no associativity). + + Reserving a notation is also useful for simultaneously defining an + inductive type or a recursive constant and a notation for it. - Reserved Notation "x = y" (at level 70, no associativity). + .. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence + their precedence and associativity cannot be changed. -Reserving a notation is also useful for simultaneously defining an -inductive type or a recursive constant and a notation for it. + .. cmdv:: Reserved Infix "@symbol" {* @modifiers} -.. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence - their precedence and associativity cannot be changed. + This command declares an infix parsing rule without giving its + interpretation. Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 0ade9fdbf5..4bdfac7c42 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -39,14 +39,29 @@ from sphinx.ext import mathbase from . import coqdoc from .repl import ansicolors from .repl.coqtop import CoqTop, CoqTopError +from .notations.parsing import ParseError from .notations.sphinx import sphinxify from .notations.plain import stringify_with_ellipses -def parse_notation(notation, source, line, rawtext=None): +PARSE_ERROR = """Parse error in notation! +Offending notation: {} +Error message: {}""" + +def notation_to_sphinx(notation, source, line, rawtext=None): """Parse notation and wrap it in an inline node""" - node = nodes.inline(rawtext or notation, '', *sphinxify(notation), classes=['notation']) - node.source, node.line = source, line - return node + try: + node = nodes.inline(rawtext or notation, '', *sphinxify(notation), classes=['notation']) + node.source, node.line = source, line + return node + except ParseError as e: + raise ExtensionError(PARSE_ERROR.format(notation, e.msg)) from e + +def notation_to_string(notation): + """Parse notation and format it as a string with ellipses.""" + try: + return stringify_with_ellipses(notation) + except ParseError as e: + raise ExtensionError(PARSE_ERROR.format(notation, e.msg)) from e def highlight_using_coqdoc(sentence): """Lex sentence using coqdoc, and yield inline nodes for each token""" @@ -136,7 +151,7 @@ class CoqObject(ObjectDescription): self._render_signature(signature, signode) name = self._names.get(signature) if name is None: - name = self._name_from_signature(signature) + name = self._name_from_signature(signature) # pylint: disable=assignment-from-none # remove trailing ‘.’ found in commands, but not ‘...’ (ellipsis) if name is not None and name.endswith(".") and not name.endswith("..."): name = name[:-1] @@ -241,7 +256,7 @@ class NotationObject(DocumentableObject): """ def _render_signature(self, signature, signode): position = self.state_machine.get_source_and_line(self.lineno) - tacn_node = parse_notation(signature, *position) + tacn_node = notation_to_sphinx(signature, *position) signode += addnodes.desc_name(signature, '', tacn_node) class GallinaObject(PlainObject): @@ -346,7 +361,7 @@ class OptionObject(NotationObject): annotation = "Option" def _name_from_signature(self, signature): - return stringify_with_ellipses(signature) + return notation_to_string(signature) class FlagObject(NotationObject): @@ -365,7 +380,7 @@ class FlagObject(NotationObject): annotation = "Flag" def _name_from_signature(self, signature): - return stringify_with_ellipses(signature) + return notation_to_string(signature) class TableObject(NotationObject): @@ -383,7 +398,7 @@ class TableObject(NotationObject): annotation = "Table" def _name_from_signature(self, signature): - return stringify_with_ellipses(signature) + return notation_to_string(signature) class ProductionObject(CoqObject): r"""A grammar production. @@ -403,7 +418,7 @@ class ProductionObject(CoqObject): Example:: .. prodn:: term += let: @pattern := @term in @term - .. prodn:: occ_switch ::= { {? + %| - } {* @num } } + .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } } """ subdomain = "prodn" @@ -432,7 +447,7 @@ class ProductionObject(CoqObject): lhs_node = nodes.literal(lhs_op, lhs_op) position = self.state_machine.get_source_and_line(self.lineno) - rhs_node = parse_notation(rhs, *position) + rhs_node = notation_to_sphinx(rhs, *position) signode += addnodes.desc_name(signature, '', lhs_node, rhs_node) return ('token', lhs) if op == '::=' else None @@ -475,7 +490,7 @@ class ExceptionObject(NotationObject): # Generate names automatically def _name_from_signature(self, signature): - return stringify_with_ellipses(signature) + return notation_to_string(signature) class WarningObject(NotationObject): """An warning raised by a Coq command or tactic.. @@ -497,7 +512,7 @@ class WarningObject(NotationObject): # Generate names automatically def _name_from_signature(self, signature): - return stringify_with_ellipses(signature) + return notation_to_string(signature) def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]): #pylint: disable=unused-argument, dangerous-default-value @@ -516,7 +531,7 @@ def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]): """ notation = utils.unescape(text, 1) position = inliner.reporter.get_source_and_line(lineno) - return [nodes.literal(rawtext, '', parse_notation(notation, *position, rawtext=rawtext))], [] + return [nodes.literal(rawtext, '', notation_to_sphinx(notation, *position, rawtext=rawtext))], [] def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]): #pylint: disable=dangerous-default-value diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g index a889ebda7b..01c656eb23 100644 --- a/doc/tools/coqrst/notations/TacticNotations.g +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -13,21 +13,38 @@ grammar TacticNotations; // needs rendering (in particular whitespace (kept in output) vs. WHITESPACE // (discarded)). +// The distinction between nopipeblock and block is needed because we only want +// to require escaping within alternative blocks, so that e.g. `first [ x | y ]` +// can be written without escaping the `|`. + top: blocks EOF; blocks: block ((whitespace)? block)*; -block: atomic | meta | hole | repeat | curlies; -repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE; + +block: pipe | nopipeblock; +nopipeblock: atomic | escaped | hole | alternative | repeat | curlies; + +alternative: LALT (WHITESPACE)? altblocks (WHITESPACE)? RBRACE; +altblocks: altblock ((WHITESPACE)? altsep (WHITESPACE)? altblock)+; +altblock: nopipeblock ((whitespace)? nopipeblock)*; + +repeat: LGROUP (ATOM | PIPE)? WHITESPACE blocks (WHITESPACE)? RBRACE; curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE; + +pipe: PIPE; +altsep: PIPE; whitespace: WHITESPACE; -meta: METACHAR; +escaped: ESCAPED; atomic: ATOM (SUB)?; hole: ID (SUB)?; -LGROUP: '{' [+*?]; + +LALT: '{|'; +LGROUP: '{+' | '{*' | '{?'; LBRACE: '{'; RBRACE: '}'; -METACHAR: '%' [|(){}]; -ATOM: '@' | '_' | ~[@_{} ]+; +ESCAPED: '%{' | '%}' | '%|'; +PIPE: '|'; +ATOM: '@' | '_' | ~[@_{}| ]+; ID: '@' ('_'? [a-zA-Z0-9])+; SUB: '_' '_' [a-zA-Z0-9]+; WHITESPACE: ' '+; diff --git a/doc/tools/coqrst/notations/TacticNotations.tokens b/doc/tools/coqrst/notations/TacticNotations.tokens index 88b38f97a6..2670e20aa6 100644 --- a/doc/tools/coqrst/notations/TacticNotations.tokens +++ b/doc/tools/coqrst/notations/TacticNotations.tokens @@ -1,10 +1,14 @@ -LGROUP=1 -LBRACE=2 -RBRACE=3 -METACHAR=4 -ATOM=5 -ID=6 -SUB=7 -WHITESPACE=8 -'{'=2 -'}'=3 +LALT=1 +LGROUP=2 +LBRACE=3 +RBRACE=4 +ESCAPED=5 +PIPE=6 +ATOM=7 +ID=8 +SUB=9 +WHITESPACE=10 +'{|'=1 +'{'=3 +'}'=4 +'|'=6 diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py index 27293e7e09..e3a115e32a 100644 --- a/doc/tools/coqrst/notations/TacticNotationsLexer.py +++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py @@ -1,4 +1,4 @@ -# Generated from TacticNotations.g by ANTLR 4.7 +# Generated from TacticNotations.g by ANTLR 4.7.2 from antlr4 import * from io import StringIO from typing.io import TextIO @@ -7,28 +7,34 @@ import sys def serializedATN(): with StringIO() as buf: - buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\n") - buf.write(":\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") - buf.write("\4\b\t\b\4\t\t\t\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3") - buf.write("\5\3\6\3\6\6\6 \n\6\r\6\16\6!\5\6$\n\6\3\7\3\7\5\7(\n") - buf.write("\7\3\7\6\7+\n\7\r\7\16\7,\3\b\3\b\3\b\6\b\62\n\b\r\b\16") - buf.write("\b\63\3\t\6\t\67\n\t\r\t\16\t8\2\2\n\3\3\5\4\7\5\t\6\13") - buf.write("\7\r\b\17\t\21\n\3\2\7\4\2,-AA\4\2*+}\177\4\2BBaa\7\2") - buf.write("\"\"BBaa}}\177\177\5\2\62;C\\c|\2?\2\3\3\2\2\2\2\5\3\2") - buf.write("\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2") - buf.write("\2\17\3\2\2\2\2\21\3\2\2\2\3\23\3\2\2\2\5\26\3\2\2\2\7") - buf.write("\30\3\2\2\2\t\32\3\2\2\2\13#\3\2\2\2\r%\3\2\2\2\17.\3") - buf.write("\2\2\2\21\66\3\2\2\2\23\24\7}\2\2\24\25\t\2\2\2\25\4\3") - buf.write("\2\2\2\26\27\7}\2\2\27\6\3\2\2\2\30\31\7\177\2\2\31\b") - buf.write("\3\2\2\2\32\33\7\'\2\2\33\34\t\3\2\2\34\n\3\2\2\2\35$") - buf.write("\t\4\2\2\36 \n\5\2\2\37\36\3\2\2\2 !\3\2\2\2!\37\3\2\2") - buf.write("\2!\"\3\2\2\2\"$\3\2\2\2#\35\3\2\2\2#\37\3\2\2\2$\f\3") - buf.write("\2\2\2%*\7B\2\2&(\7a\2\2\'&\3\2\2\2\'(\3\2\2\2()\3\2\2") - buf.write("\2)+\t\6\2\2*\'\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2") - buf.write("-\16\3\2\2\2./\7a\2\2/\61\7a\2\2\60\62\t\6\2\2\61\60\3") - buf.write("\2\2\2\62\63\3\2\2\2\63\61\3\2\2\2\63\64\3\2\2\2\64\20") - buf.write("\3\2\2\2\65\67\7\"\2\2\66\65\3\2\2\2\678\3\2\2\28\66\3") - buf.write("\2\2\289\3\2\2\29\22\3\2\2\2\t\2!#\',\638\2") + buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\f") + buf.write("M\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") + buf.write("\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t\13\3\2\3\2\3\2\3\3\3\3") + buf.write("\3\3\3\3\3\3\3\3\5\3!\n\3\3\4\3\4\3\5\3\5\3\6\3\6\3\6") + buf.write("\3\6\3\6\3\6\5\6-\n\6\3\7\3\7\3\b\3\b\6\b\63\n\b\r\b\16") + buf.write("\b\64\5\b\67\n\b\3\t\3\t\5\t;\n\t\3\t\6\t>\n\t\r\t\16") + buf.write("\t?\3\n\3\n\3\n\6\nE\n\n\r\n\16\nF\3\13\6\13J\n\13\r\13") + buf.write("\16\13K\2\2\f\3\3\5\4\7\5\t\6\13\7\r\b\17\t\21\n\23\13") + buf.write("\25\f\3\2\5\4\2BBaa\6\2\"\"BBaa}\177\5\2\62;C\\c|\2V\2") + buf.write("\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3") + buf.write("\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\2\21\3\2\2\2\2\23\3\2") + buf.write("\2\2\2\25\3\2\2\2\3\27\3\2\2\2\5 \3\2\2\2\7\"\3\2\2\2") + buf.write("\t$\3\2\2\2\13,\3\2\2\2\r.\3\2\2\2\17\66\3\2\2\2\218\3") + buf.write("\2\2\2\23A\3\2\2\2\25I\3\2\2\2\27\30\7}\2\2\30\31\7~\2") + buf.write("\2\31\4\3\2\2\2\32\33\7}\2\2\33!\7-\2\2\34\35\7}\2\2\35") + buf.write("!\7,\2\2\36\37\7}\2\2\37!\7A\2\2 \32\3\2\2\2 \34\3\2\2") + buf.write("\2 \36\3\2\2\2!\6\3\2\2\2\"#\7}\2\2#\b\3\2\2\2$%\7\177") + buf.write("\2\2%\n\3\2\2\2&\'\7\'\2\2\'-\7}\2\2()\7\'\2\2)-\7\177") + buf.write("\2\2*+\7\'\2\2+-\7~\2\2,&\3\2\2\2,(\3\2\2\2,*\3\2\2\2") + buf.write("-\f\3\2\2\2./\7~\2\2/\16\3\2\2\2\60\67\t\2\2\2\61\63\n") + buf.write("\3\2\2\62\61\3\2\2\2\63\64\3\2\2\2\64\62\3\2\2\2\64\65") + buf.write("\3\2\2\2\65\67\3\2\2\2\66\60\3\2\2\2\66\62\3\2\2\2\67") + buf.write("\20\3\2\2\28=\7B\2\29;\7a\2\2:9\3\2\2\2:;\3\2\2\2;<\3") + buf.write("\2\2\2<>\t\4\2\2=:\3\2\2\2>?\3\2\2\2?=\3\2\2\2?@\3\2\2") + buf.write("\2@\22\3\2\2\2AB\7a\2\2BD\7a\2\2CE\t\4\2\2DC\3\2\2\2E") + buf.write("F\3\2\2\2FD\3\2\2\2FG\3\2\2\2G\24\3\2\2\2HJ\7\"\2\2IH") + buf.write("\3\2\2\2JK\3\2\2\2KI\3\2\2\2KL\3\2\2\2L\26\3\2\2\2\13") + buf.write("\2 ,\64\66:?FK\2") return buf.getvalue() @@ -38,34 +44,36 @@ class TacticNotationsLexer(Lexer): decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ] - LGROUP = 1 - LBRACE = 2 - RBRACE = 3 - METACHAR = 4 - ATOM = 5 - ID = 6 - SUB = 7 - WHITESPACE = 8 + LALT = 1 + LGROUP = 2 + LBRACE = 3 + RBRACE = 4 + ESCAPED = 5 + PIPE = 6 + ATOM = 7 + ID = 8 + SUB = 9 + WHITESPACE = 10 channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ] modeNames = [ "DEFAULT_MODE" ] literalNames = [ "<INVALID>", - "'{'", "'}'" ] + "'{|'", "'{'", "'}'", "'|'" ] symbolicNames = [ "<INVALID>", - "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", "SUB", - "WHITESPACE" ] + "LALT", "LGROUP", "LBRACE", "RBRACE", "ESCAPED", "PIPE", "ATOM", + "ID", "SUB", "WHITESPACE" ] - ruleNames = [ "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", - "SUB", "WHITESPACE" ] + ruleNames = [ "LALT", "LGROUP", "LBRACE", "RBRACE", "ESCAPED", "PIPE", + "ATOM", "ID", "SUB", "WHITESPACE" ] grammarFileName = "TacticNotations.g" def __init__(self, input=None, output:TextIO = sys.stdout): super().__init__(input, output) - self.checkVersion("4.7") + self.checkVersion("4.7.2") self._interp = LexerATNSimulator(self, self.atn, self.decisionsToDFA, PredictionContextCache()) self._actions = None self._predicates = None diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens index 88b38f97a6..2670e20aa6 100644 --- a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens +++ b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens @@ -1,10 +1,14 @@ -LGROUP=1 -LBRACE=2 -RBRACE=3 -METACHAR=4 -ATOM=5 -ID=6 -SUB=7 -WHITESPACE=8 -'{'=2 -'}'=3 +LALT=1 +LGROUP=2 +LBRACE=3 +RBRACE=4 +ESCAPED=5 +PIPE=6 +ATOM=7 +ID=8 +SUB=9 +WHITESPACE=10 +'{|'=1 +'{'=3 +'}'=4 +'|'=6 diff --git a/doc/tools/coqrst/notations/TacticNotationsParser.py b/doc/tools/coqrst/notations/TacticNotationsParser.py index 645f078979..4a2a73672a 100644 --- a/doc/tools/coqrst/notations/TacticNotationsParser.py +++ b/doc/tools/coqrst/notations/TacticNotationsParser.py @@ -1,4 +1,4 @@ -# Generated from TacticNotations.g by ANTLR 4.7 +# Generated from TacticNotations.g by ANTLR 4.7.2 # encoding: utf-8 from antlr4 import * from io import StringIO @@ -7,31 +7,47 @@ import sys def serializedATN(): with StringIO() as buf: - buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\n") - buf.write("J\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b") - buf.write("\t\b\4\t\t\t\4\n\t\n\3\2\3\2\3\2\3\3\3\3\5\3\32\n\3\3") - buf.write("\3\7\3\35\n\3\f\3\16\3 \13\3\3\4\3\4\3\4\3\4\3\4\5\4\'") - buf.write("\n\4\3\5\3\5\5\5+\n\5\3\5\3\5\3\5\5\5\60\n\5\3\5\3\5\3") - buf.write("\6\3\6\5\6\66\n\6\3\6\3\6\5\6:\n\6\3\6\3\6\3\7\3\7\3\b") - buf.write("\3\b\3\t\3\t\5\tD\n\t\3\n\3\n\5\nH\n\n\3\n\2\2\13\2\4") - buf.write("\6\b\n\f\16\20\22\2\2\2L\2\24\3\2\2\2\4\27\3\2\2\2\6&") - buf.write("\3\2\2\2\b(\3\2\2\2\n\63\3\2\2\2\f=\3\2\2\2\16?\3\2\2") - buf.write("\2\20A\3\2\2\2\22E\3\2\2\2\24\25\5\4\3\2\25\26\7\2\2\3") - buf.write("\26\3\3\2\2\2\27\36\5\6\4\2\30\32\5\f\7\2\31\30\3\2\2") - buf.write("\2\31\32\3\2\2\2\32\33\3\2\2\2\33\35\5\6\4\2\34\31\3\2") - buf.write("\2\2\35 \3\2\2\2\36\34\3\2\2\2\36\37\3\2\2\2\37\5\3\2") - buf.write("\2\2 \36\3\2\2\2!\'\5\20\t\2\"\'\5\16\b\2#\'\5\22\n\2") - buf.write("$\'\5\b\5\2%\'\5\n\6\2&!\3\2\2\2&\"\3\2\2\2&#\3\2\2\2") - buf.write("&$\3\2\2\2&%\3\2\2\2\'\7\3\2\2\2(*\7\3\2\2)+\7\7\2\2*") - buf.write(")\3\2\2\2*+\3\2\2\2+,\3\2\2\2,-\7\n\2\2-/\5\4\3\2.\60") - buf.write("\7\n\2\2/.\3\2\2\2/\60\3\2\2\2\60\61\3\2\2\2\61\62\7\5") - buf.write("\2\2\62\t\3\2\2\2\63\65\7\4\2\2\64\66\5\f\7\2\65\64\3") - buf.write("\2\2\2\65\66\3\2\2\2\66\67\3\2\2\2\679\5\4\3\28:\5\f\7") - buf.write("\298\3\2\2\29:\3\2\2\2:;\3\2\2\2;<\7\5\2\2<\13\3\2\2\2") - buf.write("=>\7\n\2\2>\r\3\2\2\2?@\7\6\2\2@\17\3\2\2\2AC\7\7\2\2") - buf.write("BD\7\t\2\2CB\3\2\2\2CD\3\2\2\2D\21\3\2\2\2EG\7\b\2\2F") - buf.write("H\7\t\2\2GF\3\2\2\2GH\3\2\2\2H\23\3\2\2\2\13\31\36&*/") - buf.write("\659CG") + buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\f") + buf.write("\u0081\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") + buf.write("\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t\13\4\f\t\f\4\r\t\r\4\16") + buf.write("\t\16\4\17\t\17\4\20\t\20\3\2\3\2\3\2\3\3\3\3\5\3&\n\3") + buf.write("\3\3\7\3)\n\3\f\3\16\3,\13\3\3\4\3\4\5\4\60\n\4\3\5\3") + buf.write("\5\3\5\3\5\3\5\3\5\5\58\n\5\3\6\3\6\5\6<\n\6\3\6\3\6\5") + buf.write("\6@\n\6\3\6\3\6\3\7\3\7\5\7F\n\7\3\7\3\7\5\7J\n\7\3\7") + buf.write("\3\7\6\7N\n\7\r\7\16\7O\3\b\3\b\5\bT\n\b\3\b\7\bW\n\b") + buf.write("\f\b\16\bZ\13\b\3\t\3\t\5\t^\n\t\3\t\3\t\3\t\5\tc\n\t") + buf.write("\3\t\3\t\3\n\3\n\5\ni\n\n\3\n\3\n\5\nm\n\n\3\n\3\n\3\13") + buf.write("\3\13\3\f\3\f\3\r\3\r\3\16\3\16\3\17\3\17\5\17{\n\17\3") + buf.write("\20\3\20\5\20\177\n\20\3\20\2\2\21\2\4\6\b\n\f\16\20\22") + buf.write("\24\26\30\32\34\36\2\3\3\2\b\t\2\u0086\2 \3\2\2\2\4#\3") + buf.write("\2\2\2\6/\3\2\2\2\b\67\3\2\2\2\n9\3\2\2\2\fC\3\2\2\2\16") + buf.write("Q\3\2\2\2\20[\3\2\2\2\22f\3\2\2\2\24p\3\2\2\2\26r\3\2") + buf.write("\2\2\30t\3\2\2\2\32v\3\2\2\2\34x\3\2\2\2\36|\3\2\2\2 ") + buf.write("!\5\4\3\2!\"\7\2\2\3\"\3\3\2\2\2#*\5\6\4\2$&\5\30\r\2") + buf.write("%$\3\2\2\2%&\3\2\2\2&\'\3\2\2\2\')\5\6\4\2(%\3\2\2\2)") + buf.write(",\3\2\2\2*(\3\2\2\2*+\3\2\2\2+\5\3\2\2\2,*\3\2\2\2-\60") + buf.write("\5\24\13\2.\60\5\b\5\2/-\3\2\2\2/.\3\2\2\2\60\7\3\2\2") + buf.write("\2\618\5\34\17\2\628\5\32\16\2\638\5\36\20\2\648\5\n\6") + buf.write("\2\658\5\20\t\2\668\5\22\n\2\67\61\3\2\2\2\67\62\3\2\2") + buf.write("\2\67\63\3\2\2\2\67\64\3\2\2\2\67\65\3\2\2\2\67\66\3\2") + buf.write("\2\28\t\3\2\2\29;\7\3\2\2:<\7\f\2\2;:\3\2\2\2;<\3\2\2") + buf.write("\2<=\3\2\2\2=?\5\f\7\2>@\7\f\2\2?>\3\2\2\2?@\3\2\2\2@") + buf.write("A\3\2\2\2AB\7\6\2\2B\13\3\2\2\2CM\5\16\b\2DF\7\f\2\2E") + buf.write("D\3\2\2\2EF\3\2\2\2FG\3\2\2\2GI\5\26\f\2HJ\7\f\2\2IH\3") + buf.write("\2\2\2IJ\3\2\2\2JK\3\2\2\2KL\5\16\b\2LN\3\2\2\2ME\3\2") + buf.write("\2\2NO\3\2\2\2OM\3\2\2\2OP\3\2\2\2P\r\3\2\2\2QX\5\b\5") + buf.write("\2RT\5\30\r\2SR\3\2\2\2ST\3\2\2\2TU\3\2\2\2UW\5\b\5\2") + buf.write("VS\3\2\2\2WZ\3\2\2\2XV\3\2\2\2XY\3\2\2\2Y\17\3\2\2\2Z") + buf.write("X\3\2\2\2[]\7\4\2\2\\^\t\2\2\2]\\\3\2\2\2]^\3\2\2\2^_") + buf.write("\3\2\2\2_`\7\f\2\2`b\5\4\3\2ac\7\f\2\2ba\3\2\2\2bc\3\2") + buf.write("\2\2cd\3\2\2\2de\7\6\2\2e\21\3\2\2\2fh\7\5\2\2gi\5\30") + buf.write("\r\2hg\3\2\2\2hi\3\2\2\2ij\3\2\2\2jl\5\4\3\2km\5\30\r") + buf.write("\2lk\3\2\2\2lm\3\2\2\2mn\3\2\2\2no\7\6\2\2o\23\3\2\2\2") + buf.write("pq\7\b\2\2q\25\3\2\2\2rs\7\b\2\2s\27\3\2\2\2tu\7\f\2\2") + buf.write("u\31\3\2\2\2vw\7\7\2\2w\33\3\2\2\2xz\7\t\2\2y{\7\13\2") + buf.write("\2zy\3\2\2\2z{\3\2\2\2{\35\3\2\2\2|~\7\n\2\2}\177\7\13") + buf.write("\2\2~}\3\2\2\2~\177\3\2\2\2\177\37\3\2\2\2\23%*/\67;?") + buf.write("EIOSX]bhlz~") return buf.getvalue() @@ -45,37 +61,47 @@ class TacticNotationsParser ( Parser ): sharedContextCache = PredictionContextCache() - literalNames = [ "<INVALID>", "<INVALID>", "'{'", "'}'" ] + literalNames = [ "<INVALID>", "'{|'", "<INVALID>", "'{'", "'}'", "<INVALID>", + "'|'" ] - symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "METACHAR", - "ATOM", "ID", "SUB", "WHITESPACE" ] + symbolicNames = [ "<INVALID>", "LALT", "LGROUP", "LBRACE", "RBRACE", + "ESCAPED", "PIPE", "ATOM", "ID", "SUB", "WHITESPACE" ] RULE_top = 0 RULE_blocks = 1 RULE_block = 2 - RULE_repeat = 3 - RULE_curlies = 4 - RULE_whitespace = 5 - RULE_meta = 6 - RULE_atomic = 7 - RULE_hole = 8 - - ruleNames = [ "top", "blocks", "block", "repeat", "curlies", "whitespace", - "meta", "atomic", "hole" ] + RULE_nopipeblock = 3 + RULE_alternative = 4 + RULE_altblocks = 5 + RULE_altblock = 6 + RULE_repeat = 7 + RULE_curlies = 8 + RULE_pipe = 9 + RULE_altsep = 10 + RULE_whitespace = 11 + RULE_escaped = 12 + RULE_atomic = 13 + RULE_hole = 14 + + ruleNames = [ "top", "blocks", "block", "nopipeblock", "alternative", + "altblocks", "altblock", "repeat", "curlies", "pipe", + "altsep", "whitespace", "escaped", "atomic", "hole" ] EOF = Token.EOF - LGROUP=1 - LBRACE=2 - RBRACE=3 - METACHAR=4 - ATOM=5 - ID=6 - SUB=7 - WHITESPACE=8 + LALT=1 + LGROUP=2 + LBRACE=3 + RBRACE=4 + ESCAPED=5 + PIPE=6 + ATOM=7 + ID=8 + SUB=9 + WHITESPACE=10 def __init__(self, input:TokenStream, output:TextIO = sys.stdout): super().__init__(input, output) - self.checkVersion("4.7") + self.checkVersion("4.7.2") self._interp = ParserATNSimulator(self, self.atn, self.decisionsToDFA, self.sharedContextCache) self._predicates = None @@ -112,9 +138,9 @@ class TacticNotationsParser ( Parser ): self.enterRule(localctx, 0, self.RULE_top) try: self.enterOuterAlt(localctx, 1) - self.state = 18 + self.state = 30 self.blocks() - self.state = 19 + self.state = 31 self.match(TacticNotationsParser.EOF) except RecognitionException as re: localctx.exception = re @@ -163,24 +189,24 @@ class TacticNotationsParser ( Parser ): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 21 + self.state = 33 self.block() - self.state = 28 + self.state = 40 self._errHandler.sync(self) _alt = self._interp.adaptivePredict(self._input,1,self._ctx) while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: if _alt==1: - self.state = 23 + self.state = 35 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 22 + self.state = 34 self.whitespace() - self.state = 25 + self.state = 37 self.block() - self.state = 30 + self.state = 42 self._errHandler.sync(self) _alt = self._interp.adaptivePredict(self._input,1,self._ctx) @@ -198,18 +224,77 @@ class TacticNotationsParser ( Parser ): super().__init__(parent, invokingState) self.parser = parser + def pipe(self): + return self.getTypedRuleContext(TacticNotationsParser.PipeContext,0) + + + def nopipeblock(self): + return self.getTypedRuleContext(TacticNotationsParser.NopipeblockContext,0) + + + def getRuleIndex(self): + return TacticNotationsParser.RULE_block + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitBlock" ): + return visitor.visitBlock(self) + else: + return visitor.visitChildren(self) + + + + + def block(self): + + localctx = TacticNotationsParser.BlockContext(self, self._ctx, self.state) + self.enterRule(localctx, 4, self.RULE_block) + try: + self.state = 45 + self._errHandler.sync(self) + token = self._input.LA(1) + if token in [TacticNotationsParser.PIPE]: + self.enterOuterAlt(localctx, 1) + self.state = 43 + self.pipe() + pass + elif token in [TacticNotationsParser.LALT, TacticNotationsParser.LGROUP, TacticNotationsParser.LBRACE, TacticNotationsParser.ESCAPED, TacticNotationsParser.ATOM, TacticNotationsParser.ID]: + self.enterOuterAlt(localctx, 2) + self.state = 44 + self.nopipeblock() + pass + else: + raise NoViableAltException(self) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class NopipeblockContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + def atomic(self): return self.getTypedRuleContext(TacticNotationsParser.AtomicContext,0) - def meta(self): - return self.getTypedRuleContext(TacticNotationsParser.MetaContext,0) + def escaped(self): + return self.getTypedRuleContext(TacticNotationsParser.EscapedContext,0) def hole(self): return self.getTypedRuleContext(TacticNotationsParser.HoleContext,0) + def alternative(self): + return self.getTypedRuleContext(TacticNotationsParser.AlternativeContext,0) + + def repeat(self): return self.getTypedRuleContext(TacticNotationsParser.RepeatContext,0) @@ -219,48 +304,53 @@ class TacticNotationsParser ( Parser ): def getRuleIndex(self): - return TacticNotationsParser.RULE_block + return TacticNotationsParser.RULE_nopipeblock def accept(self, visitor:ParseTreeVisitor): - if hasattr( visitor, "visitBlock" ): - return visitor.visitBlock(self) + if hasattr( visitor, "visitNopipeblock" ): + return visitor.visitNopipeblock(self) else: return visitor.visitChildren(self) - def block(self): + def nopipeblock(self): - localctx = TacticNotationsParser.BlockContext(self, self._ctx, self.state) - self.enterRule(localctx, 4, self.RULE_block) + localctx = TacticNotationsParser.NopipeblockContext(self, self._ctx, self.state) + self.enterRule(localctx, 6, self.RULE_nopipeblock) try: - self.state = 36 + self.state = 53 self._errHandler.sync(self) token = self._input.LA(1) if token in [TacticNotationsParser.ATOM]: self.enterOuterAlt(localctx, 1) - self.state = 31 + self.state = 47 self.atomic() pass - elif token in [TacticNotationsParser.METACHAR]: + elif token in [TacticNotationsParser.ESCAPED]: self.enterOuterAlt(localctx, 2) - self.state = 32 - self.meta() + self.state = 48 + self.escaped() pass elif token in [TacticNotationsParser.ID]: self.enterOuterAlt(localctx, 3) - self.state = 33 + self.state = 49 self.hole() pass - elif token in [TacticNotationsParser.LGROUP]: + elif token in [TacticNotationsParser.LALT]: self.enterOuterAlt(localctx, 4) - self.state = 34 + self.state = 50 + self.alternative() + pass + elif token in [TacticNotationsParser.LGROUP]: + self.enterOuterAlt(localctx, 5) + self.state = 51 self.repeat() pass elif token in [TacticNotationsParser.LBRACE]: - self.enterOuterAlt(localctx, 5) - self.state = 35 + self.enterOuterAlt(localctx, 6) + self.state = 52 self.curlies() pass else: @@ -274,6 +364,232 @@ class TacticNotationsParser ( Parser ): self.exitRule() return localctx + class AlternativeContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def LALT(self): + return self.getToken(TacticNotationsParser.LALT, 0) + + def altblocks(self): + return self.getTypedRuleContext(TacticNotationsParser.AltblocksContext,0) + + + def RBRACE(self): + return self.getToken(TacticNotationsParser.RBRACE, 0) + + def WHITESPACE(self, i:int=None): + if i is None: + return self.getTokens(TacticNotationsParser.WHITESPACE) + else: + return self.getToken(TacticNotationsParser.WHITESPACE, i) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_alternative + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitAlternative" ): + return visitor.visitAlternative(self) + else: + return visitor.visitChildren(self) + + + + + def alternative(self): + + localctx = TacticNotationsParser.AlternativeContext(self, self._ctx, self.state) + self.enterRule(localctx, 8, self.RULE_alternative) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 55 + self.match(TacticNotationsParser.LALT) + self.state = 57 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.WHITESPACE: + self.state = 56 + self.match(TacticNotationsParser.WHITESPACE) + + + self.state = 59 + self.altblocks() + self.state = 61 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.WHITESPACE: + self.state = 60 + self.match(TacticNotationsParser.WHITESPACE) + + + self.state = 63 + self.match(TacticNotationsParser.RBRACE) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class AltblocksContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def altblock(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(TacticNotationsParser.AltblockContext) + else: + return self.getTypedRuleContext(TacticNotationsParser.AltblockContext,i) + + + def altsep(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(TacticNotationsParser.AltsepContext) + else: + return self.getTypedRuleContext(TacticNotationsParser.AltsepContext,i) + + + def WHITESPACE(self, i:int=None): + if i is None: + return self.getTokens(TacticNotationsParser.WHITESPACE) + else: + return self.getToken(TacticNotationsParser.WHITESPACE, i) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_altblocks + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitAltblocks" ): + return visitor.visitAltblocks(self) + else: + return visitor.visitChildren(self) + + + + + def altblocks(self): + + localctx = TacticNotationsParser.AltblocksContext(self, self._ctx, self.state) + self.enterRule(localctx, 10, self.RULE_altblocks) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 65 + self.altblock() + self.state = 75 + self._errHandler.sync(self) + _alt = 1 + while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: + if _alt == 1: + self.state = 67 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.WHITESPACE: + self.state = 66 + self.match(TacticNotationsParser.WHITESPACE) + + + self.state = 69 + self.altsep() + self.state = 71 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.WHITESPACE: + self.state = 70 + self.match(TacticNotationsParser.WHITESPACE) + + + self.state = 73 + self.altblock() + + else: + raise NoViableAltException(self) + self.state = 77 + self._errHandler.sync(self) + _alt = self._interp.adaptivePredict(self._input,8,self._ctx) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class AltblockContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def nopipeblock(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(TacticNotationsParser.NopipeblockContext) + else: + return self.getTypedRuleContext(TacticNotationsParser.NopipeblockContext,i) + + + def whitespace(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(TacticNotationsParser.WhitespaceContext) + else: + return self.getTypedRuleContext(TacticNotationsParser.WhitespaceContext,i) + + + def getRuleIndex(self): + return TacticNotationsParser.RULE_altblock + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitAltblock" ): + return visitor.visitAltblock(self) + else: + return visitor.visitChildren(self) + + + + + def altblock(self): + + localctx = TacticNotationsParser.AltblockContext(self, self._ctx, self.state) + self.enterRule(localctx, 12, self.RULE_altblock) + self._la = 0 # Token type + try: + self.enterOuterAlt(localctx, 1) + self.state = 79 + self.nopipeblock() + self.state = 86 + self._errHandler.sync(self) + _alt = self._interp.adaptivePredict(self._input,10,self._ctx) + while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: + if _alt==1: + self.state = 81 + self._errHandler.sync(self) + _la = self._input.LA(1) + if _la==TacticNotationsParser.WHITESPACE: + self.state = 80 + self.whitespace() + + + self.state = 83 + self.nopipeblock() + self.state = 88 + self._errHandler.sync(self) + _alt = self._interp.adaptivePredict(self._input,10,self._ctx) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + class RepeatContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -299,6 +615,9 @@ class TacticNotationsParser ( Parser ): def ATOM(self): return self.getToken(TacticNotationsParser.ATOM, 0) + def PIPE(self): + return self.getToken(TacticNotationsParser.PIPE, 0) + def getRuleIndex(self): return TacticNotationsParser.RULE_repeat @@ -314,33 +633,38 @@ class TacticNotationsParser ( Parser ): def repeat(self): localctx = TacticNotationsParser.RepeatContext(self, self._ctx, self.state) - self.enterRule(localctx, 6, self.RULE_repeat) + self.enterRule(localctx, 14, self.RULE_repeat) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 38 + self.state = 89 self.match(TacticNotationsParser.LGROUP) - self.state = 40 + self.state = 91 self._errHandler.sync(self) _la = self._input.LA(1) - if _la==TacticNotationsParser.ATOM: - self.state = 39 - self.match(TacticNotationsParser.ATOM) + if _la==TacticNotationsParser.PIPE or _la==TacticNotationsParser.ATOM: + self.state = 90 + _la = self._input.LA(1) + if not(_la==TacticNotationsParser.PIPE or _la==TacticNotationsParser.ATOM): + self._errHandler.recoverInline(self) + else: + self._errHandler.reportMatch(self) + self.consume() - self.state = 42 + self.state = 93 self.match(TacticNotationsParser.WHITESPACE) - self.state = 43 + self.state = 94 self.blocks() - self.state = 45 + self.state = 96 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 44 + self.state = 95 self.match(TacticNotationsParser.WHITESPACE) - self.state = 47 + self.state = 98 self.match(TacticNotationsParser.RBRACE) except RecognitionException as re: localctx.exception = re @@ -388,31 +712,31 @@ class TacticNotationsParser ( Parser ): def curlies(self): localctx = TacticNotationsParser.CurliesContext(self, self._ctx, self.state) - self.enterRule(localctx, 8, self.RULE_curlies) + self.enterRule(localctx, 16, self.RULE_curlies) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 49 + self.state = 100 self.match(TacticNotationsParser.LBRACE) - self.state = 51 + self.state = 102 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 50 + self.state = 101 self.whitespace() - self.state = 53 + self.state = 104 self.blocks() - self.state = 55 + self.state = 106 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 54 + self.state = 105 self.whitespace() - self.state = 57 + self.state = 108 self.match(TacticNotationsParser.RBRACE) except RecognitionException as re: localctx.exception = re @@ -422,6 +746,80 @@ class TacticNotationsParser ( Parser ): self.exitRule() return localctx + class PipeContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def PIPE(self): + return self.getToken(TacticNotationsParser.PIPE, 0) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_pipe + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitPipe" ): + return visitor.visitPipe(self) + else: + return visitor.visitChildren(self) + + + + + def pipe(self): + + localctx = TacticNotationsParser.PipeContext(self, self._ctx, self.state) + self.enterRule(localctx, 18, self.RULE_pipe) + try: + self.enterOuterAlt(localctx, 1) + self.state = 110 + self.match(TacticNotationsParser.PIPE) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + + class AltsepContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def PIPE(self): + return self.getToken(TacticNotationsParser.PIPE, 0) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_altsep + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitAltsep" ): + return visitor.visitAltsep(self) + else: + return visitor.visitChildren(self) + + + + + def altsep(self): + + localctx = TacticNotationsParser.AltsepContext(self, self._ctx, self.state) + self.enterRule(localctx, 20, self.RULE_altsep) + try: + self.enterOuterAlt(localctx, 1) + self.state = 112 + self.match(TacticNotationsParser.PIPE) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + class WhitespaceContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -446,10 +844,10 @@ class TacticNotationsParser ( Parser ): def whitespace(self): localctx = TacticNotationsParser.WhitespaceContext(self, self._ctx, self.state) - self.enterRule(localctx, 10, self.RULE_whitespace) + self.enterRule(localctx, 22, self.RULE_whitespace) try: self.enterOuterAlt(localctx, 1) - self.state = 59 + self.state = 114 self.match(TacticNotationsParser.WHITESPACE) except RecognitionException as re: localctx.exception = re @@ -459,35 +857,35 @@ class TacticNotationsParser ( Parser ): self.exitRule() return localctx - class MetaContext(ParserRuleContext): + class EscapedContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): super().__init__(parent, invokingState) self.parser = parser - def METACHAR(self): - return self.getToken(TacticNotationsParser.METACHAR, 0) + def ESCAPED(self): + return self.getToken(TacticNotationsParser.ESCAPED, 0) def getRuleIndex(self): - return TacticNotationsParser.RULE_meta + return TacticNotationsParser.RULE_escaped def accept(self, visitor:ParseTreeVisitor): - if hasattr( visitor, "visitMeta" ): - return visitor.visitMeta(self) + if hasattr( visitor, "visitEscaped" ): + return visitor.visitEscaped(self) else: return visitor.visitChildren(self) - def meta(self): + def escaped(self): - localctx = TacticNotationsParser.MetaContext(self, self._ctx, self.state) - self.enterRule(localctx, 12, self.RULE_meta) + localctx = TacticNotationsParser.EscapedContext(self, self._ctx, self.state) + self.enterRule(localctx, 24, self.RULE_escaped) try: self.enterOuterAlt(localctx, 1) - self.state = 61 - self.match(TacticNotationsParser.METACHAR) + self.state = 116 + self.match(TacticNotationsParser.ESCAPED) except RecognitionException as re: localctx.exception = re self._errHandler.reportError(self, re) @@ -523,17 +921,17 @@ class TacticNotationsParser ( Parser ): def atomic(self): localctx = TacticNotationsParser.AtomicContext(self, self._ctx, self.state) - self.enterRule(localctx, 14, self.RULE_atomic) + self.enterRule(localctx, 26, self.RULE_atomic) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 63 + self.state = 118 self.match(TacticNotationsParser.ATOM) - self.state = 65 + self.state = 120 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.SUB: - self.state = 64 + self.state = 119 self.match(TacticNotationsParser.SUB) @@ -572,17 +970,17 @@ class TacticNotationsParser ( Parser ): def hole(self): localctx = TacticNotationsParser.HoleContext(self, self._ctx, self.state) - self.enterRule(localctx, 16, self.RULE_hole) + self.enterRule(localctx, 28, self.RULE_hole) self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 67 + self.state = 122 self.match(TacticNotationsParser.ID) - self.state = 69 + self.state = 124 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.SUB: - self.state = 68 + self.state = 123 self.match(TacticNotationsParser.SUB) diff --git a/doc/tools/coqrst/notations/TacticNotationsVisitor.py b/doc/tools/coqrst/notations/TacticNotationsVisitor.py index c0bcc4af37..aba696c89f 100644 --- a/doc/tools/coqrst/notations/TacticNotationsVisitor.py +++ b/doc/tools/coqrst/notations/TacticNotationsVisitor.py @@ -1,4 +1,4 @@ -# Generated from TacticNotations.g by ANTLR 4.7 +# Generated from TacticNotations.g by ANTLR 4.7.2 from antlr4 import * if __name__ is not None and "." in __name__: from .TacticNotationsParser import TacticNotationsParser @@ -24,6 +24,26 @@ class TacticNotationsVisitor(ParseTreeVisitor): return self.visitChildren(ctx) + # Visit a parse tree produced by TacticNotationsParser#nopipeblock. + def visitNopipeblock(self, ctx:TacticNotationsParser.NopipeblockContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#alternative. + def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#altblocks. + def visitAltblocks(self, ctx:TacticNotationsParser.AltblocksContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#altblock. + def visitAltblock(self, ctx:TacticNotationsParser.AltblockContext): + return self.visitChildren(ctx) + + # Visit a parse tree produced by TacticNotationsParser#repeat. def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): return self.visitChildren(ctx) @@ -34,13 +54,23 @@ class TacticNotationsVisitor(ParseTreeVisitor): return self.visitChildren(ctx) + # Visit a parse tree produced by TacticNotationsParser#pipe. + def visitPipe(self, ctx:TacticNotationsParser.PipeContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by TacticNotationsParser#altsep. + def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext): + return self.visitChildren(ctx) + + # Visit a parse tree produced by TacticNotationsParser#whitespace. def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): return self.visitChildren(ctx) - # Visit a parse tree produced by TacticNotationsParser#meta. - def visitMeta(self, ctx:TacticNotationsParser.MetaContext): + # Visit a parse tree produced by TacticNotationsParser#escaped. + def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext): return self.visitChildren(ctx) diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py index 87a41cf9f3..d2b5d86b37 100644 --- a/doc/tools/coqrst/notations/html.py +++ b/doc/tools/coqrst/notations/html.py @@ -13,12 +13,24 @@ Uses the dominate package. """ from dominate import tags +from dominate.utils import text from .parsing import parse from .TacticNotationsParser import TacticNotationsParser from .TacticNotationsVisitor import TacticNotationsVisitor class TacticNotationsToHTMLVisitor(TacticNotationsVisitor): + def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext): + with tags.span(_class='alternative'): + self.visitChildren(ctx) + + def visitAltblock(self, ctx:TacticNotationsParser.AltblockContext): + with tags.span(_class='alternative-block'): + self.visitChildren(ctx) + + def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext): + tags.span('\u200b', _class="alternative-separator") + def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): with tags.span(_class="repeat-wrapper"): with tags.span(_class="repeat"): @@ -39,21 +51,20 @@ class TacticNotationsToHTMLVisitor(TacticNotationsVisitor): def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext): tags.span(ctx.ATOM().getText()) + def visitPipe(self, ctx:TacticNotationsParser.PipeContext): + text("|") + def visitHole(self, ctx:TacticNotationsParser.HoleContext): tags.span(ctx.ID().getText()[1:], _class="hole") sub = ctx.SUB() if sub: tags.sub(sub.getText()[1:]) - def visitMeta(self, ctx:TacticNotationsParser.MetaContext): - txt = ctx.METACHAR().getText()[1:] - if (txt == "{") or (txt == "}"): - tags.span(txt) - else: - tags.span(txt, _class="meta") + def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext): + tags.span(ctx.ESCAPED().getText()[1:]) def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): - tags.span(" ") # TODO: no need for a <span> here + text(" ") def htmlize(notation): """Translate notation to a dominate HTML tree""" diff --git a/doc/tools/coqrst/notations/parsing.py b/doc/tools/coqrst/notations/parsing.py index 506240d907..2312e09090 100644 --- a/doc/tools/coqrst/notations/parsing.py +++ b/doc/tools/coqrst/notations/parsing.py @@ -11,10 +11,22 @@ from .TacticNotationsLexer import TacticNotationsLexer from .TacticNotationsParser import TacticNotationsParser from antlr4 import CommonTokenStream, InputStream +from antlr4.error.ErrorListener import ErrorListener SUBSTITUTIONS = [#("@bindings_list", "{+ (@id := @val) }"), ("@qualid_or_string", "@id|@string")] +class ParseError(Exception): + def __init__(self, msg): + super().__init__() + self.msg = msg + +class ExceptionRaisingErrorListener(ErrorListener): + def syntaxError(self, recognizer, offendingSymbol, line, column, msg, e): + raise ParseError("{}:{}: {}".format(line, column, msg)) + +ERROR_LISTENER = ExceptionRaisingErrorListener() + def substitute(notation): """Perform common substitutions in the notation string. @@ -27,11 +39,13 @@ def substitute(notation): return notation def parse(notation): - """Parse a notation string. + """Parse a notation string, optionally reporting errors to `error_listener`. :return: An ANTLR AST. Use one of the supplied visitors (or write your own) to turn it into useful output. """ substituted = substitute(notation) lexer = TacticNotationsLexer(InputStream(substituted)) - return TacticNotationsParser(CommonTokenStream(lexer)).top() + parser = TacticNotationsParser(CommonTokenStream(lexer)) + parser.addErrorListener(ERROR_LISTENER) + return parser.top() diff --git a/doc/tools/coqrst/notations/plain.py b/doc/tools/coqrst/notations/plain.py index f6e82fc68e..2180c8e6a5 100644 --- a/doc/tools/coqrst/notations/plain.py +++ b/doc/tools/coqrst/notations/plain.py @@ -22,8 +22,16 @@ class TacticNotationsToDotsVisitor(TacticNotationsVisitor): def __init__(self): self.buffer = StringIO() + def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext): + self.buffer.write("[") + self.visitChildren(ctx) + self.buffer.write("]") + + def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext): + self.buffer.write("|") + def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): - separator = ctx.ATOM() + separator = ctx.ATOM() or ctx.PIPE() self.visitChildren(ctx) if ctx.LGROUP().getText()[1] == "+": spacer = (separator.getText() + " " if separator else "") @@ -38,11 +46,14 @@ class TacticNotationsToDotsVisitor(TacticNotationsVisitor): def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext): self.buffer.write(ctx.ATOM().getText()) + def visitPipe(self, ctx:TacticNotationsParser.PipeContext): + self.buffer.write("|") + def visitHole(self, ctx:TacticNotationsParser.HoleContext): self.buffer.write("‘{}’".format(ctx.ID().getText()[1:])) - def visitMeta(self, ctx:TacticNotationsParser.MetaContext): - self.buffer.write(ctx.METACHAR().getText()[1:]) + def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext): + self.buffer.write(ctx.ESCAPED().getText()[1:]) def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): self.buffer.write(" ") diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index e05b834184..4ed09e04a9 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -20,8 +20,6 @@ from .TacticNotationsVisitor import TacticNotationsVisitor from docutils import nodes from sphinx import addnodes -import sys - class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): def defaultResult(self): return [] @@ -31,16 +29,36 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): aggregate.extend(nextResult) return aggregate + def visitAlternative(self, ctx:TacticNotationsParser.AlternativeContext): + return [nodes.inline('', '', *self.visitChildren(ctx), classes=['alternative'])] + + def visitAltblock(self, ctx:TacticNotationsParser.AltblockContext): + return [nodes.inline('', '', *self.visitChildren(ctx), classes=['alternative-block'])] + + def visitAltsep(self, ctx:TacticNotationsParser.AltsepContext): + return [nodes.inline('|', '\u200b', classes=['alternative-separator'])] + + @staticmethod + def is_alternative(node): + return isinstance(node, nodes.inline) and node['classes'] == ['alternative'] + def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext): # Uses inline nodes instead of subscript and superscript to ensure that # we get the right customization hooks at the LaTeX level wrapper = nodes.inline('', '', classes=['repeat-wrapper']) - wrapper += nodes.inline('', '', *self.visitChildren(ctx), classes=["repeat"]) + + children = self.visitChildren(ctx) + if len(children) == 1 and self.is_alternative(children[0]): + # Use a custom style if an alternative is nested in a repeat. + # (We could detect this in CSS, but it's much harder in LaTeX.) + + children[0]['classes'] = ['repeated-alternative'] + wrapper += nodes.inline('', '', *children, classes=["repeat"]) repeat_marker = ctx.LGROUP().getText()[1] wrapper += nodes.inline(repeat_marker, repeat_marker, classes=['notation-sup']) - separator = ctx.ATOM() + separator = ctx.ATOM() or ctx.PIPE() if separator: sep = separator.getText() wrapper += nodes.inline(sep, sep, classes=['notation-sub']) @@ -65,6 +83,9 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): return [node] + def visitPipe(self, ctx:TacticNotationsParser.PipeContext): + return [nodes.Text("|")] + def visitHole(self, ctx:TacticNotationsParser.HoleContext): hole = ctx.ID().getText() token_name = hole[1:] @@ -75,23 +96,18 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): sub_index = sub.getText()[2:] node += nodes.subscript(sub_index, sub_index) - return [addnodes.pending_xref(token_name, node, reftype='token', refdomain='std', reftarget=token_name)] + return [addnodes.pending_xref(token_name, node, reftype='token', + refdomain='std', reftarget=token_name)] - def visitMeta(self, ctx:TacticNotationsParser.MetaContext): - meta = ctx.METACHAR().getText() - metachar = meta[1:] # remove escape char - token_name = metachar - if (metachar == "{") or (metachar == "}"): - classes=[] - else: - classes=["meta"] - return [nodes.inline(metachar, token_name, classes=classes)] + def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext): + escaped = ctx.ESCAPED().getText() + return [nodes.inline(escaped, escaped[1:])] def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): return [nodes.Text(" ")] def sphinxify(notation): - """Translate notation into a Sphinx document tree""" + """Translate a notation into a Sphinx document tree.""" vs = TacticNotationsToSphinxVisitor() return vs.visit(parse(notation)) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index be0318fbde..0a5bba39b9 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -656,26 +656,26 @@ let clear_hyps2_in_evi env sigma hyps t concl ids = (* spiwack: a few functions to gather evars on which goals depend. *) let queue_set q is_dependent set = Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set -let queue_term q is_dependent c = - queue_set q is_dependent (evars_of_term (EConstr.Unsafe.to_constr c)) +let queue_term evm q is_dependent c = + queue_set q is_dependent (evars_of_term evm c) let process_dependent_evar q acc evm is_dependent e = let evi = Evd.find evm e in (* Queues evars appearing in the types of the goal (conclusion, then hypotheses), they are all dependent. *) - queue_term q true evi.evar_concl; + queue_term evm q true evi.evar_concl; List.iter begin fun decl -> let open NamedDecl in - queue_term q true (NamedDecl.get_type decl); + queue_term evm q true (NamedDecl.get_type decl); match decl with | LocalAssum _ -> () - | LocalDef (_,b,_) -> queue_term q true b + | LocalDef (_,b,_) -> queue_term evm q true b end (EConstr.named_context_of_val evi.evar_hyps); match evi.evar_body with | Evar_empty -> if is_dependent then Evar.Map.add e None acc else acc | Evar_defined b -> - let subevars = evars_of_term (EConstr.Unsafe.to_constr b) in + let subevars = evars_of_term evm b in (* evars appearing in the definition of an evar [e] are marked as dependent when [e] is dependent itself: if [e] is a non-dependent goal, then, unless they are reach from another @@ -795,7 +795,7 @@ let filtered_undefined_evars_of_evar_info ?cache sigma evi = in let accu = match evi.evar_body with | Evar_empty -> Evar.Set.empty - | Evar_defined b -> evars_of_term (EConstr.Unsafe.to_constr b) + | Evar_defined b -> evars_of_term sigma b in let accu = Evar.Set.union (undefined_evars_of_term sigma evi.evar_concl) accu in let ctxt = EConstr.Unsafe.to_named_context (evar_filtered_context evi) in diff --git a/engine/evd.ml b/engine/evd.ml index d37b49e2dc..15b4c31851 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -222,7 +222,7 @@ let map_evar_body f = function let map_evar_info f evi = {evi with evar_body = map_evar_body f evi.evar_body; - evar_hyps = map_named_val f evi.evar_hyps; + evar_hyps = map_named_val (fun d -> NamedDecl.map_constr f d) evi.evar_hyps; evar_concl = f evi.evar_concl; evar_candidates = Option.map (List.map f) evi.evar_candidates } @@ -823,33 +823,6 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) = | Evar (evk2,_) -> fst (evar_source evk2 evd) | _ -> None -(** The following functions return the set of evars immediately - contained in the object *) - -(* excluding defined evars *) - -let evars_of_term c = - let rec evrec acc c = - match kind c with - | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) - | _ -> Constr.fold evrec acc c - in - evrec Evar.Set.empty c - -let evars_of_named_context nc = - Context.Named.fold_outside - (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr))) - nc - ~init:Evar.Set.empty - -let evars_of_filtered_evar_info evi = - Evar.Set.union (evars_of_term evi.evar_concl) - (Evar.Set.union - (match evi.evar_body with - | Evar_empty -> Evar.Set.empty - | Evar_defined b -> evars_of_term b) - (evars_of_named_context (evar_filtered_context evi))) - (**********************************************************) (* Sort variables *) @@ -1404,3 +1377,30 @@ module MiniEConstr = struct let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d end + +(** The following functions return the set of evars immediately + contained in the object *) + +(* excluding defined evars *) + +let evars_of_term evd c = + let rec evrec acc c = + match MiniEConstr.kind evd c with + | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) + | _ -> Constr.fold evrec acc c + in + evrec Evar.Set.empty c + +let evars_of_named_context evd nc = + Context.Named.fold_outside + (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term evd constr))) + nc + ~init:Evar.Set.empty + +let evars_of_filtered_evar_info evd evi = + Evar.Set.union (evars_of_term evd evi.evar_concl) + (Evar.Set.union + (match evi.evar_body with + | Evar_empty -> Evar.Set.empty + | Evar_defined b -> evars_of_term evd b) + (evars_of_named_context evd (evar_filtered_context evi))) diff --git a/engine/evd.mli b/engine/evd.mli index 29235050b0..587a1de044 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -491,16 +491,15 @@ val extract_changed_conv_pbs : evar_map -> val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option -(** The following functions return the set of evars immediately - contained in the object; need the term to be evar-normal otherwise - defined evars are returned too. *) +(** The following functions return the set of undefined evars + contained in the object. *) -val evars_of_term : constr -> Evar.Set.t +val evars_of_term : evar_map -> econstr -> Evar.Set.t (** including evars in instances of evars *) -val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t +val evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t -val evars_of_filtered_evar_info : evar_info -> Evar.Set.t +val evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t (** Metas *) val meta_list : evar_map -> (metavariable * clbinding) list diff --git a/engine/proofview.ml b/engine/proofview.ml index ecea637947..5c5a02d3fa 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -46,7 +46,7 @@ let compact el ({ solution } as pv) = let apply_subst_einfo _ ei = Evd.({ ei with evar_concl = nf ei.evar_concl; - evar_hyps = Environ.map_named_val nf0 ei.evar_hyps; + evar_hyps = Environ.map_named_val (fun d -> map_constr nf0 d) ei.evar_hyps; evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in @@ -641,7 +641,7 @@ let shelve_goals l = [sigma]. *) let depends_on sigma src tgt = let evi = Evd.find sigma tgt in - Evar.Set.mem src (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi)) + Evar.Set.mem src (Evd.evars_of_filtered_evar_info sigma (Evarutil.nf_evar_info sigma evi)) let unifiable_delayed g l = CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) l @@ -1251,9 +1251,9 @@ module V82 = struct let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in { Evd.it = goals ; sigma=solution; } - let top_evars initial = + let top_evars initial { solution=sigma; } = let evars_of_initial (c,_) = - Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c)) + Evar.Set.elements (Evd.evars_of_term sigma c) in CList.flatten (CList.map evars_of_initial initial) diff --git a/engine/proofview.mli b/engine/proofview.mli index 92f8b86df5..b7ff3ac432 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -595,7 +595,7 @@ module V82 : sig val top_goals : entry -> proofview -> Evar.t list Evd.sigma (* returns the existential variable used to start the proof *) - val top_evars : entry -> Evar.t list + val top_evars : entry -> proofview -> Evar.t list (* Caution: this function loses quite a bit of information. It should be avoided as much as possible. It should work as diff --git a/engine/termops.ml b/engine/termops.ml index 8a6bd17948..fcacb53ac4 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -187,7 +187,7 @@ let compute_evar_dependency_graph sigma = in match evar_body evi with | Evar_empty -> acc - | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term (EConstr.Unsafe.to_constr c)) acc + | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term sigma c) acc in Evd.fold fold sigma EvMap.empty diff --git a/interp/declare.ml b/interp/declare.ml index 76b4bab2ce..7ee7ecb5e8 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -36,9 +36,8 @@ type internal_flag = (** Declaration of constants and parameters *) type constant_obj = { - cst_decl : global_declaration option; - (** [None] when the declaration is a side-effect and has already been defined - in the global environment. *) + cst_decl : Cooking.recipe option; + (** Non-empty only when rebuilding a constant after a section *) cst_kind : logical_kind; cst_locl : bool; } @@ -65,21 +64,21 @@ let open_constant i ((sp,kn), obj) = let exists_name id = variable_exists id || Global.exists_objlabel (Label.of_id id) -let check_exists sp = - let id = basename sp in +let check_exists id = if exists_name id then alreadydeclared (Id.print id ++ str " already exists") let cache_constant ((sp,kn), obj) = + (* Invariant: the constant must exist in the logical environment, except when + redefining it when exiting a section. See [discharge_constant]. *) let id = basename sp in let kn' = match obj.cst_decl with | None -> if Global.exists_objlabel (Label.of_id (basename sp)) then Constant.make1 kn - else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".") - | Some decl -> - let () = check_exists sp in - Global.add_constant ~in_section:(Lib.sections_are_opened ()) id decl + else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(basename sp) ++ str".") + | Some r -> + Global.add_recipe ~in_section:(Lib.sections_are_opened ()) id r in assert (Constant.equal kn' (Constant.make1 kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); @@ -93,7 +92,9 @@ let discharge_constant ((sp, kn), obj) = let modlist = replacement_context () in let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in let abstract = (named_of_variable_context hyps, subst, uctx) in - let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in + let new_decl = { from; info = { Opaqueproof.modlist; abstract } } in + (* This is a hack: when leaving a section, we lose the constant definition, so + we have to store it in the libobject to be able to retrieve it after. *) Some { obj with cst_decl = Some new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) @@ -121,27 +122,22 @@ let update_tables c = declare_constant_implicits c; Notation.declare_ref_arguments_scope Evd.empty (ConstRef c) -let register_side_effect (c, role) = +let register_constant kn kind local = let o = inConstant { cst_decl = None; - cst_kind = IsProof Theorem; - cst_locl = false; + cst_kind = kind; + cst_locl = local; } in - let id = Label.to_id (Constant.label c) in - ignore(add_leaf id o); - update_tables c; + let id = Label.to_id (Constant.label kn) in + let _ = add_leaf id o in + update_tables kn + +let register_side_effect (c, role) = + let () = register_constant c (IsProof Theorem) false in match role with | Subproof -> () | Schema (ind, kind) -> !declare_scheme kind [|ind,c|] -let declare_constant_common id cst = - let o = inConstant cst in - let _, kn as oname = add_leaf id o in - pull_to_head oname; - let c = Global.constant_of_delta_kn kn in - update_tables c; - c - let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body = @@ -153,7 +149,8 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types const_entry_feedback = None; const_entry_inline_code = inline} -let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = +let define_constant ?role ?(export_seff=false) id cd = + (* Logically define the constant and its subproofs, no libobject tampering *) let is_poly de = match de.const_entry_universes with | Monomorphic_entry _ -> false | Polymorphic_entry _ -> true @@ -165,20 +162,27 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e export_seff || not de.const_entry_opaque || is_poly de -> - (* This globally defines the side-effects in the environment. We mark - exported constants as being side-effect not to redeclare them at - caching time. *) + (* This globally defines the side-effects in the environment. *) let de, export = Global.export_private_constants ~in_section de in export, ConstantEntry (PureEntry, DefinitionEntry de) | _ -> [], ConstantEntry (EffectEntry, cd) in + let kn, eff = Global.add_constant ?role ~in_section id decl in + kn, eff, export + +let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = + let () = check_exists id in + let kn, _eff, export = define_constant ~export_seff id cd in + (* Register the libobjects attached to the constants and its subproofs *) let () = List.iter register_side_effect export in - let cst = { - cst_decl = Some decl; - cst_kind = kind; - cst_locl = local; - } in - declare_constant_common id cst + let () = register_constant kn kind local in + kn + +let declare_private_constant ~role ?(internal=UserIndividualRequest) ?(local = false) id (cd, kind) = + let kn, eff, export = define_constant ~role id cd in + let () = assert (List.is_empty export) in + let () = register_constant kn kind local in + kn, eff let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) @@ -297,7 +301,7 @@ let open_inductive i ((sp,kn),mie) = let cache_inductive ((sp,kn),mie) = let names = inductive_names sp kn mie in - List.iter check_exists (List.map fst names); + List.iter check_exists (List.map (fun p -> basename (fst p)) names); let id = basename sp in let kn' = Global.add_mind id mie in assert (MutInd.equal kn' (MutInd.make1 kn)); diff --git a/interp/declare.mli b/interp/declare.mli index 8f1e73c88c..2ffde31fc0 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -55,6 +55,9 @@ val definition_entry : ?fix_exn:Future.fix_exn -> val declare_constant : ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t +val declare_private_constant : + role:side_effect_role -> ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> Constant.t * Safe_typing.private_constants + val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> ?local:bool -> Id.t -> ?types:constr -> diff --git a/interp/impargs.ml b/interp/impargs.ml index 90fb5a2036..806fe93297 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -497,9 +497,9 @@ type implicit_interactive_request = type implicit_discharge_request = | ImplLocal - | ImplConstant of Constant.t * implicits_flags + | ImplConstant of implicits_flags | ImplMutualInductive of MutInd.t * implicits_flags - | ImplInteractive of GlobRef.t * implicits_flags * + | ImplInteractive of implicits_flags * implicit_interactive_request let implicits_table = Summary.ref GlobRef.Map.empty ~name:"implicits" @@ -552,39 +552,24 @@ let add_section_impls vars extra_impls (cond,impls) = let discharge_implicits (_,(req,l)) = match req with | ImplLocal -> None - | ImplInteractive (ref,flags,exp) -> - (try - let vars = variable_section_segment_of_reference ref in - let extra_impls = impls_of_context vars in - let l' = [ref, List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in - Some (ImplInteractive (ref,flags,exp),l') - with Not_found -> (* ref not defined in this section *) Some (req,l)) - | ImplConstant (con,flags) -> - (try - let vars = variable_section_segment_of_reference (ConstRef con) in - let extra_impls = impls_of_context vars in - let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in - let l' = [ConstRef con,newimpls] in - Some (ImplConstant (con,flags),l') - with Not_found -> (* con not defined in this section *) Some (req,l)) - | ImplMutualInductive (kn,flags) -> - (try - let l' = List.map (fun (gr, l) -> - let vars = variable_section_segment_of_reference gr in - let extra_impls = impls_of_context vars in - (gr, - List.map (add_section_impls vars extra_impls) l)) l - in - Some (ImplMutualInductive (kn,flags),l') - with Not_found -> (* ref not defined in this section *) Some (req,l)) + | ImplMutualInductive _ | ImplInteractive _ | ImplConstant _ -> + let l' = + try + List.map (fun (gr, l) -> + let vars = variable_section_segment_of_reference gr in + let extra_impls = impls_of_context vars in + let newimpls = List.map (add_section_impls vars extra_impls) l in + (gr, newimpls)) l + with Not_found -> l in + Some (req,l') let rebuild_implicits (req,l) = match req with | ImplLocal -> assert false - | ImplConstant (con,flags) -> - let oldimpls = snd (List.hd l) in - let newimpls = compute_constant_implicits flags con in - req, [ConstRef con, List.map2 merge_impls oldimpls newimpls] + | ImplConstant flags -> + let ref,oldimpls = List.hd l in + let newimpls = compute_global_implicits flags ref in + req, [ref, List.map2 merge_impls oldimpls newimpls] | ImplMutualInductive (kn,flags) -> let newimpls = compute_all_mib_implicits flags kn in let rec aux olds news = @@ -595,15 +580,14 @@ let rebuild_implicits (req,l) = | _, _ -> assert false in req, aux l newimpls - | ImplInteractive (ref,flags,o) -> + | ImplInteractive (flags,o) -> + let ref,oldimpls = List.hd l in (if isVarRef ref && is_in_section ref then ImplLocal else req), match o with | ImplAuto -> - let oldimpls = snd (List.hd l) in let newimpls = compute_global_implicits flags ref in [ref,List.map2 merge_impls oldimpls newimpls] | ImplManual userimplsize -> - let oldimpls = snd (List.hd l) in if flags.auto then let newimpls = List.hd (compute_global_implicits flags ref) in let p = List.length (snd newimpls) - userimplsize in @@ -638,7 +622,7 @@ let declare_implicits_gen req flags ref = let declare_implicits local ref = let flags = { !implicit_args with auto = true } in let req = - if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in + if is_local local ref then ImplLocal else ImplInteractive(flags,ImplAuto) in declare_implicits_gen req flags ref let declare_var_implicits id = @@ -647,7 +631,7 @@ let declare_var_implicits id = let declare_constant_implicits con = let flags = !implicit_args in - declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con) + declare_implicits_gen (ImplConstant flags) flags (ConstRef con) let declare_mib_implicits kn = let flags = !implicit_args in @@ -697,7 +681,7 @@ let declare_manual_implicits local ref ?enriching l = let l = [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] in let req = if is_local local ref then ImplLocal - else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) + else ImplInteractive(flags,ImplManual (List.length autoimpls)) in add_anonymous_leaf (inImplicits (req,[ref,l])) let maybe_declare_manual_implicits local ref ?enriching l = @@ -756,7 +740,7 @@ let set_implicits local ref l = compute_implicit_statuses autoimpls imps)) l in let req = if is_local local ref then ImplLocal - else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) + else ImplInteractive(flags,ImplManual (List.length autoimpls)) in add_anonymous_leaf (inImplicits (req,[ref,l'])) let extract_impargs_data impls = diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index dffccf02fc..6277d874dd 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -281,7 +281,7 @@ let implicits_of_glob_constr ?(with_products=true) l = | _ -> () in [] | GLambda (na, bk, t, b) -> abs na bk b - | GLetIn (na, b, t, c) -> aux i b + | GLetIn (na, b, t, c) -> aux i c | GRec (fix_kind, nas, args, tys, bds) -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 1b348ae777..4b45608ae5 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -97,7 +97,8 @@ if (sp - num_args < coq_stack_threshold) { \ several architectures. */ -#if defined(__GNUC__) && !defined(DEBUG) +#if defined(__GNUC__) && !defined(DEBUG) && !defined(__INTEL_COMPILER) \ + && !defined(__llvm__) #ifdef __mips__ #define PC_REG asm("$16") #define SP_REG asm("$17") @@ -126,7 +127,7 @@ if (sp - num_args < coq_stack_threshold) { \ #define SP_REG asm("%edi") #define ACCU_REG #endif -#if defined(PPC) || defined(_POWER) || defined(_IBMR2) +#if defined(__ppc__) || defined(__ppc64__) #define PC_REG asm("26") #define SP_REG asm("27") #define ACCU_REG asm("28") @@ -141,8 +142,9 @@ if (sp - num_args < coq_stack_threshold) { \ #define SP_REG asm("a4") #define ACCU_REG asm("d7") #endif -#if defined(__arm__) && !defined(__thumb2__) -#define PC_REG asm("r9") +/* OCaml PR#4953: these specific registers not available in Thumb mode */ +#if defined(__arm__) && !defined(__thumb__) +#define PC_REG asm("r6") #define SP_REG asm("r8") #define ACCU_REG asm("r7") #endif @@ -152,6 +154,17 @@ if (sp - num_args < coq_stack_threshold) { \ #define ACCU_REG asm("38") #define JUMPTBL_BASE_REG asm("39") #endif +#ifdef __x86_64__ +#define PC_REG asm("%r15") +#define SP_REG asm("%r14") +#define ACCU_REG asm("%r13") +#endif +#ifdef __aarch64__ +#define PC_REG asm("%x19") +#define SP_REG asm("%x20") +#define ACCU_REG asm("%x21") +#define JUMPTBL_BASE_REG asm("%x22") +#endif #endif #define CheckInt1() do{ \ diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 412637c4b6..95f88c0306 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -389,7 +389,7 @@ type clos_infos = { i_flags : reds; i_cache : infos_cache } -type clos_tab = fconstr constant_def KeyTable.t +type clos_tab = (fconstr, Empty.t) constant_def KeyTable.t let info_flags info = info.i_flags let info_env info = info.i_cache.i_env diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index b1b69dded8..1a790eaed6 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -215,7 +215,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (** Conversion auxiliary functions to do step by step normalisation *) (** [unfold_reference] unfolds references in a [fconstr] *) -val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr constant_def +val unfold_reference : clos_infos -> clos_tab -> table_key -> (fconstr, Util.Empty.t) constant_def (*********************************************************************** i This is for lazy debug *) diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 6a9550342c..bdaf5fe422 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -20,7 +20,7 @@ val compile : fail_on_error:bool -> (** init, fun, fv *) val compile_constant_body : fail_on_error:bool -> - env -> universes -> Constr.t Mod_subst.substituted constant_def -> + env -> universes -> (Constr.t Mod_subst.substituted, 'opaque) constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 9b974c4ecc..9b6e37251f 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -152,11 +152,11 @@ let abstract_constant_body c (hyps, subst) = let c = Vars.subst_vars subst c in it_mkLambda_or_LetIn c hyps -type recipe = { from : constant_body; info : Opaqueproof.cooking_info } +type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info } type inline = bool -type result = { - cook_body : constr Mod_subst.substituted constant_def; +type 'opaque result = { + cook_body : (constr Mod_subst.substituted, 'opaque) constant_def; cook_type : types; cook_universes : universes; cook_private_univs : Univ.ContextSet.t option; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index b0f143c47d..b022e2ac09 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -13,12 +13,12 @@ open Declarations (** {6 Cooking the constants. } *) -type recipe = { from : constant_body; info : Opaqueproof.cooking_info } +type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info } type inline = bool -type result = { - cook_body : constr Mod_subst.substituted constant_def; +type 'opaque result = { + cook_body : (constr Mod_subst.substituted, 'opaque) constant_def; cook_type : types; cook_universes : universes; cook_private_univs : Univ.ContextSet.t option; @@ -27,7 +27,7 @@ type result = { cook_context : Constr.named_context option; } -val cook_constant : hcons:bool -> recipe -> result +val cook_constant : hcons:bool -> recipe -> Opaqueproof.opaque result val cook_constr : Opaqueproof.cooking_info -> constr -> constr (** {6 Utility functions used in module [Discharge]. } *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 5551742c02..36ee952099 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -47,10 +47,10 @@ type inline = int option transparent body, or an opaque one *) (* Global declarations (i.e. constants) can be either: *) -type 'a constant_def = +type ('a, 'opaque) constant_def = | Undef of inline (** a global assumption *) | Def of 'a (** or a transparent global definition *) - | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) + | OpaqueDef of 'opaque (** or an opaque global definition *) | Primitive of CPrimitives.t (** or a primitive operation *) type universes = @@ -87,9 +87,9 @@ type typing_flags = { (* some contraints are in constant_constraints, some other may be in * the OpaqueDef *) -type constant_body = { +type 'opaque constant_body = { const_hyps : Constr.named_context; (** New: younger hyp at top *) - const_body : Constr.t Mod_subst.substituted constant_def; + const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def; const_type : types; const_relevance : Sorts.relevance; const_body_code : Cemitcodes.to_patch_substituted option; @@ -246,7 +246,7 @@ type module_alg_expr = (** A component of a module structure *) type structure_field_body = - | SFBconst of constant_body + | SFBconst of Opaqueproof.opaque constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body | SFBmodtype of module_type_body diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 54a853fc81..fb02c6a029 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -26,21 +26,21 @@ val map_decl_arity : ('a -> 'c) -> ('b -> 'd) -> (** {6 Constants} *) -val subst_const_body : substitution -> constant_body -> constant_body +val subst_const_body : substitution -> Opaqueproof.opaque constant_body -> Opaqueproof.opaque constant_body (** Is there a actual body in const_body ? *) -val constant_has_body : constant_body -> bool +val constant_has_body : 'a constant_body -> bool -val constant_polymorphic_context : constant_body -> AUContext.t +val constant_polymorphic_context : 'a constant_body -> AUContext.t (** Is the constant polymorphic? *) -val constant_is_polymorphic : constant_body -> bool +val constant_is_polymorphic : 'a constant_body -> bool (** Return the universe context, in case the definition is polymorphic, otherwise the context is empty. *) -val is_opaque : constant_body -> bool +val is_opaque : 'a constant_body -> bool (** {6 Inductive types} *) @@ -83,7 +83,7 @@ val safe_flags : Conv_oracle.oracle -> typing_flags of the structure, but simply hash-cons all inner constr and other known elements *) -val hcons_const_body : constant_body -> constant_body +val hcons_const_body : 'a constant_body -> 'a constant_body val hcons_mind : mutual_inductive_body -> mutual_inductive_body val hcons_module_body : module_body -> module_body val hcons_module_type : module_type_body -> module_type_body diff --git a/kernel/entries.ml b/kernel/entries.ml index a3d32267a7..adb3f6bd29 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -108,21 +108,7 @@ type module_entry = | MExpr of module_params_entry * module_struct_entry * module_struct_entry option - -type seff_env = - [ `Nothing - (* The proof term and its universes. - Same as the constant_body's but not in an ephemeron *) - | `Opaque of Constr.t * Univ.ContextSet.t ] - (** Not used by the kernel. *) type side_effect_role = | Subproof | Schema of inductive * string - -type side_eff = { - seff_constant : Constant.t; - seff_body : Declarations.constant_body; - seff_env : seff_env; - seff_role : side_effect_role; -} diff --git a/kernel/environ.ml b/kernel/environ.ml index 97c9f8654a..05f342a82a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -46,7 +46,7 @@ type link_info = | LinkedInteractive of string | NotLinked -type constant_key = constant_body * (link_info ref * key) +type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref @@ -187,7 +187,7 @@ let match_named_context_val c = match c.env_named_ctx with let map_named_val f ctxt = let open Context.Named.Declaration in let fold accu d = - let d' = map_constr f d in + let d' = f d in let accu = if d == d' then accu else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu diff --git a/kernel/environ.mli b/kernel/environ.mli index 8c6bc105c7..f6cd41861e 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -42,7 +42,7 @@ type link_info = type key = int CEphemeron.key option ref -type constant_key = constant_body * (link_info ref * key) +type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref @@ -134,9 +134,9 @@ val ids_of_named_context_val : named_context_val -> Id.Set.t (** [map_named_val f ctxt] apply [f] to the body and the type of each declarations. - *** /!\ *** [f t] should be convertible with t *) + *** /!\ *** [f t] should be convertible with t, and preserve the name *) val map_named_val : - (constr -> constr) -> named_context_val -> named_context_val + (named_declaration -> named_declaration) -> named_context_val -> named_context_val val push_named : Constr.named_declaration -> env -> env val push_named_context : Constr.named_context -> env -> env @@ -174,19 +174,19 @@ val reset_with_named_context : named_context_val -> env -> env val pop_rel_context : int -> env -> env (** Useful for printing *) -val fold_constants : (Constant.t -> constant_body -> 'a -> 'a) -> env -> 'a -> 'a +val fold_constants : (Constant.t -> Opaqueproof.opaque constant_body -> 'a -> 'a) -> env -> 'a -> 'a (** {5 Global constants } {6 Add entries to global environment } *) -val add_constant : Constant.t -> constant_body -> env -> env -val add_constant_key : Constant.t -> constant_body -> link_info -> +val add_constant : Constant.t -> Opaqueproof.opaque constant_body -> env -> env +val add_constant_key : Constant.t -> Opaqueproof.opaque constant_body -> link_info -> env -> env val lookup_constant_key : Constant.t -> env -> constant_key (** Looks up in the context of global constant names raises [Not_found] if the required path is not found *) -val lookup_constant : Constant.t -> env -> constant_body +val lookup_constant : Constant.t -> env -> Opaqueproof.opaque constant_body val evaluable_constant : Constant.t -> env -> bool (** New-style polymorphism *) @@ -219,7 +219,7 @@ val constant_context : env -> Constant.t -> Univ.AUContext.t it lives in. For monomorphic constant, the latter is empty, and for polymorphic constants, the term contains De Bruijn universe variables that need to be instantiated. *) -val body_of_constant_body : env -> constant_body -> (Constr.constr * Univ.AUContext.t) option +val body_of_constant_body : env -> Opaqueproof.opaque constant_body -> (Constr.constr * Univ.AUContext.t) option (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant diff --git a/kernel/modops.ml b/kernel/modops.ml index 4f992d3972..4fdd7ab334 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -608,11 +608,7 @@ let clean_bounded_mod_expr sign = (** {6 Stm machinery } *) let join_constant_body except otab cb = match cb.const_body with - | OpaqueDef o -> - (match Opaqueproof.uuid_opaque otab o with - | Some uuid when not(Future.UUIDSet.mem uuid except) -> - Opaqueproof.join_opaque otab o - | _ -> ()) + | OpaqueDef o -> Opaqueproof.join_opaque ~except otab o | _ -> () let join_structure except otab s = diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 96efa7faa5..b5c03b6ca3 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -65,7 +65,7 @@ val empty_updates : code_location_updates val register_native_file : string -> unit val compile_constant_field : env -> string -> Constant.t -> - global list -> constant_body -> global list + global list -> 'a constant_body -> global list val compile_mind_field : ModPath.t -> Label.t -> global list -> mutual_inductive_body -> global list diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 303cb06c55..18c1bcc0f8 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -77,29 +77,23 @@ let subst_opaque sub = function | Indirect (s,dp,i) -> Indirect (sub::s,dp,i) | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.") -let iter_direct_opaque f = function - | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") - | Direct (d,cu) -> - Direct (d,Future.chain cu (fun (c, u) -> f c; c, u)) - let discharge_direct_opaque ~cook_constr ci = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") | Direct (d,cu) -> Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u)) -let join_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> ignore(Future.join cu) +let join except cu = match except with +| None -> ignore (Future.join cu) +| Some except -> + if Future.UUIDSet.mem (Future.uuid cu) except then () + else ignore (Future.join cu) + +let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function + | Direct (_,cu) -> join except cu | Indirect (_,dp,i) -> if DirPath.equal dp odp then let fp = snd (Int.Map.find i prfs) in - ignore(Future.join fp) - -let uuid_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> Some (Future.uuid cu) - | Indirect (_,dp,i) -> - if DirPath.equal dp odp - then Some (Future.uuid (snd (Int.Map.find i prfs))) - else None + join except fp let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> @@ -128,16 +122,6 @@ let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function then Some(Future.chain (snd (Int.Map.find i prfs)) snd) else !get_univ dp i -let get_proof { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> Future.chain cu fst - | Indirect (l,dp,i) -> - let pt = - if DirPath.equal dp odp - then Future.chain (snd (Int.Map.find i prfs)) fst - else !get_opaque dp i in - Future.chain pt (fun c -> - force_constr (List.fold_right subst_substituted l (from_val c))) - module FMap = Future.UUIDMap let a_constr = Future.from_val (mkRel 1) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 5ea6da649b..4e8956af06 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -39,12 +39,10 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab indirect opaque accessor configured below. *) val force_proof : opaquetab -> opaque -> constr val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t -val get_proof : opaquetab -> opaque -> constr Future.computation val get_constraints : opaquetab -> opaque -> Univ.ContextSet.t Future.computation option val subst_opaque : substitution -> opaque -> opaque -val iter_direct_opaque : (constr -> unit) -> opaque -> opaque type work_list = (Univ.Instance.t * Id.t array) Cmap.t * (Univ.Instance.t * Id.t array) Mindmap.t @@ -60,8 +58,7 @@ type cooking_info = { val discharge_direct_opaque : cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque -val uuid_opaque : opaquetab -> opaque -> Future.UUID.t option -val join_opaque : opaquetab -> opaque -> unit +val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit val dump : opaquetab -> Constr.t Future.computation array * diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 673f025c75..a5d8a480ee 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -228,19 +228,11 @@ let check_engagement env expected_impredicative_set = (** {6 Stm machinery } *) -let get_opaque_body env cbo = - match cbo.const_body with - | Undef _ -> assert false - | Primitive _ -> assert false - | Def _ -> `Nothing - | OpaqueDef opaque -> - `Opaque - (Opaqueproof.force_proof (Environ.opaque_tables env) opaque, - Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) - type side_effect = { from_env : Declarations.structure_body CEphemeron.key; - eff : Entries.side_eff list; + seff_constant : Constant.t; + seff_body : (Constr.t * Univ.ContextSet.t) Declarations.constant_body; + seff_role : Entries.side_effect_role; } module SideEffects : @@ -254,11 +246,9 @@ end = struct module SeffOrd = struct -open Entries type t = side_effect let compare e1 e2 = - let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in - List.compare cmp e1.eff e2.eff + Constant.CanOrd.compare e1.seff_constant e2.seff_constant end module SeffSet = Set.Make(SeffOrd) @@ -279,41 +269,40 @@ end type private_constants = SideEffects.t let side_effects_of_private_constants l = - let ans = List.rev (SideEffects.repr l) in - List.map_append (fun { eff; _ } -> eff) ans + List.rev (SideEffects.repr l) -let empty_private_constants = SideEffects.empty -let add_private mb eff effs = - let from_env = CEphemeron.create mb in - SideEffects.add { eff; from_env } effs -let concat_private = SideEffects.concat +(* Only used to push in an Environ.env. *) +let lift_constant c = + let body = match c.const_body with + | OpaqueDef _ -> Undef None + | Def _ | Undef _ | Primitive _ as body -> body + in + { c with const_body = body } -let make_eff env cst r = - let open Entries in - let cbo = Environ.lookup_constant cst env.env in - { - seff_constant = cst; - seff_body = cbo; - seff_env = get_opaque_body env.env cbo; - seff_role = r; - } +let map_constant f c = + let body = match c.const_body with + | OpaqueDef o -> OpaqueDef (f o) + | Def _ | Undef _ | Primitive _ as body -> body + in + { c with const_body = body } -let private_con_of_con env c = - let open Entries in - let eff = [make_eff env c Subproof] in - add_private env.revstruct eff empty_private_constants +let push_private_constants env eff = + let eff = side_effects_of_private_constants eff in + let add_if_undefined env eff = + try ignore(Environ.lookup_constant eff.seff_constant env); env + with Not_found -> Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env + in + List.fold_left add_if_undefined env eff -let private_con_of_scheme ~kind env cl = - let open Entries in - let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in - add_private env.revstruct eff empty_private_constants +let empty_private_constants = SideEffects.empty +let concat_private = SideEffects.concat let universes_of_private eff = - let open Entries in let fold acc eff = - let acc = match eff.seff_env with - | `Nothing -> acc - | `Opaque (_, ctx) -> ctx :: acc + let acc = match eff.seff_body.const_body with + | Def _ -> acc + | OpaqueDef (_, ctx) -> ctx :: acc + | Primitive _ | Undef _ -> assert false in match eff.seff_body.const_universes with | Monomorphic ctx -> ctx :: acc @@ -558,7 +547,6 @@ type 'a effect_entry = type global_declaration = | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration - | GlobalRecipe of Cooking.recipe type exported_private_constant = Constant.t * Entries.side_effect_role @@ -588,32 +576,27 @@ let add_constant_aux ~in_section senv (kn, cb) = let mk_pure_proof c = (c, Univ.ContextSet.empty), SideEffects.empty let inline_side_effects env body side_eff = - let open Entries in let open Constr in (** First step: remove the constants that are still in the environment *) - let filter { eff = se; from_env = mb } = - let map e = (e.seff_constant, e.seff_body, e.seff_env) in - let cbl = List.map map se in - let not_exists (c,_,_) = - try ignore(Environ.lookup_constant c env); false - with Not_found -> true in - let cbl = List.filter not_exists cbl in - (cbl, mb) + let filter e = + let cb = (e.seff_constant, e.seff_body) in + try ignore (Environ.lookup_constant e.seff_constant env); None + with Not_found -> Some (cb, e.from_env) in (* CAVEAT: we assure that most recent effects come first *) - let side_eff = List.map filter (SideEffects.repr side_eff) in - let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in - let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in + let side_eff = List.map_filter filter (SideEffects.repr side_eff) in + let sigs = List.rev_map (fun (_, mb) -> mb) side_eff in + let side_eff = List.fold_left (fun accu (cb, _) -> cb :: accu) [] side_eff in let side_eff = List.rev side_eff in (** Most recent side-effects first in side_eff *) if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs) else (** Second step: compute the lifts and substitutions to apply *) let cname c r = Context.make_annot (Name (Label.to_id (Constant.label c))) r in - let fold (subst, var, ctx, args) (c, cb, b) = - let (b, opaque) = match cb.const_body, b with - | Def b, _ -> (Mod_subst.force_constr b, false) - | OpaqueDef _, `Opaque (b,_) -> (b, true) + let fold (subst, var, ctx, args) (c, cb) = + let (b, opaque) = match cb.const_body with + | Def b -> (Mod_subst.force_constr b, false) + | OpaqueDef (b, _) -> (b, true) | _ -> assert false in match cb.const_universes with @@ -675,24 +658,22 @@ let inline_private_constants_in_definition_entry env ce = let inline_private_constants_in_constr env body side_eff = pi1 (inline_side_effects env body side_eff) -let rec is_nth_suffix n l suf = - if Int.equal n 0 then l == suf - else match l with - | [] -> false - | _ :: l -> is_nth_suffix (pred n) l suf +let is_suffix l suf = match l with +| [] -> false +| _ :: l -> l == suf (* Given the list of signatures of side effects, checks if they match. * I.e. if they are ordered descendants of the current revstruct. Returns the number of effects that can be trusted. *) let check_signatures curmb sl = - let is_direct_ancestor accu (mb, how_many) = + let is_direct_ancestor accu mb = match accu with | None -> None | Some (n, curmb) -> try let mb = CEphemeron.get mb in - if is_nth_suffix how_many mb curmb - then Some (n + how_many, mb) + if is_suffix mb curmb + then Some (n + 1, mb) else None with CEphemeron.InvalidKey -> None in let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in @@ -701,7 +682,8 @@ let check_signatures curmb sl = | Some (n, _) -> n -let constant_entry_of_side_effect cb u = +let constant_entry_of_side_effect eff = + let cb = eff.seff_body in let open Entries in let univs = match cb.const_universes with @@ -711,9 +693,9 @@ let constant_entry_of_side_effect cb u = Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx) in let pt = - match cb.const_body, u with - | OpaqueDef _, `Opaque (b, c) -> b, c - | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty + match cb.const_body with + | OpaqueDef (b, c) -> b, c + | Def b -> Mod_subst.force_constr b, Univ.ContextSet.empty | _ -> assert false in DefinitionEntry { const_entry_body = Future.from_val (pt, ()); @@ -724,21 +706,7 @@ let constant_entry_of_side_effect cb u = const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } -let turn_direct orig = - let open Entries in - let cb = orig.seff_body in - if Declareops.is_opaque cb then - let p = match orig.seff_env with - | `Opaque (b, c) -> (b, c) - | _ -> assert false - in - let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in - let cb = { cb with const_body } in - { orig with seff_body = cb } - else orig - let export_eff eff = - let open Entries in (eff.seff_constant, eff.seff_body, eff.seff_role) let export_side_effects mb env c = @@ -751,60 +719,62 @@ let export_side_effects mb env c = let not_exists e = try ignore(Environ.lookup_constant e.seff_constant env); false with Not_found -> true in - let aux (acc,sl) { eff = se; from_env = mb } = - let cbl = List.filter not_exists se in - if List.is_empty cbl then acc, sl - else cbl :: acc, (mb,List.length cbl) :: sl in + let aux (acc,sl) e = + if not (not_exists e) then acc, sl + else e :: acc, e.from_env :: sl in let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in let trusted = check_signatures mb signatures in let push_seff env eff = let { seff_constant = kn; seff_body = cb ; _ } = eff in - let env = Environ.add_constant kn cb env in + let env = Environ.add_constant kn (lift_constant cb) env in match cb.const_universes with | Polymorphic _ -> env | Monomorphic ctx -> - let ctx = match eff.seff_env with - | `Nothing -> ctx - | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx + let ctx = match eff.seff_body.const_body with + | Def _ -> ctx + | OpaqueDef (_, ctx') -> Univ.ContextSet.union ctx' ctx + | Undef _ | Primitive _ -> assert false in Environ.push_context_set ~strict:true ctx env in let rec translate_seff sl seff acc env = match seff with | [] -> List.rev acc, ce - | cbs :: rest -> + | eff :: rest -> if Int.equal sl 0 then - let env, cbs = - List.fold_left (fun (env,cbs) eff -> - let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in - let ce = constant_entry_of_side_effect ocb u in + let env, cb = + let kn = eff.seff_constant in + let ce = constant_entry_of_side_effect eff in let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in - let eff = { eff with - seff_body = cb; - seff_env = `Nothing; - } in - (push_seff env eff, export_eff eff :: cbs)) - (env,[]) cbs in - translate_seff 0 rest (cbs @ acc) env + let cb = map_constant Future.force cb in + let eff = { eff with seff_body = cb } in + (push_seff env eff, export_eff eff) + in + translate_seff 0 rest (cb :: acc) env else - let cbs_len = List.length cbs in - let cbs = List.map turn_direct cbs in - let env = List.fold_left push_seff env cbs in - let ecbs = List.map export_eff cbs in - translate_seff (sl - cbs_len) rest (ecbs @ acc) env + let env = push_seff env eff in + let ecb = export_eff eff in + translate_seff (sl - 1) rest (ecb :: acc) env in translate_seff trusted seff [] env let export_private_constants ~in_section ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in - let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in + let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create (Future.from_val p)) cb) in + let bodies = List.map map exported in let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in (ce, exported), senv -let add_constant ~in_section l decl senv = +let add_recipe ~in_section l r senv = + let kn = Constant.make2 senv.modpath l in + let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in + let cb = if in_section then cb else Declareops.hcons_const_body cb in + let senv = add_constant_aux ~in_section senv (kn, cb) in + kn, senv + +let add_constant ?role ~in_section l decl senv = let kn = Constant.make2 senv.modpath l in - let senv = let cb = match decl with | ConstantEntry (EffectEntry, ce) -> @@ -816,9 +786,9 @@ let add_constant ~in_section l decl senv = Term_typing.translate_constant (Term_typing.SideEffects handle) senv.env kn ce | ConstantEntry (PureEntry, ce) -> Term_typing.translate_constant Term_typing.Pure senv.env kn ce - | GlobalRecipe r -> - let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in - if in_section then cb else Declareops.hcons_const_body cb in + in + let senv = + let cb = map_constant Opaqueproof.create cb in add_constant_aux ~in_section senv (kn, cb) in let senv = match decl with @@ -827,7 +797,20 @@ let add_constant ~in_section l decl senv = add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv | _ -> senv in - kn, senv + let eff = match role with + | None -> empty_private_constants + | Some role -> + let cb = map_constant Future.force cb in + let from_env = CEphemeron.create senv.revstruct in + let eff = { + from_env = from_env; + seff_constant = kn; + seff_body = cb; + seff_role = role; + } in + SideEffects.add eff empty_private_constants + in + (kn, eff), senv (** Insertion of inductive types *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 46c97c1fb8..36ca3d8c47 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -43,25 +43,20 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment type private_constants -val side_effects_of_private_constants : - private_constants -> Entries.side_eff list -(** Return the list of individual side-effects in the order of their - creation. *) - val empty_private_constants : private_constants val concat_private : private_constants -> private_constants -> private_constants (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in [e1] must be more recent than those of [e2]. *) -val private_con_of_con : safe_environment -> Constant.t -> private_constants -val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constants - val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output val inline_private_constants_in_constr : Environ.env -> Constr.constr -> private_constants -> Constr.constr val inline_private_constants_in_definition_entry : Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry +val push_private_constants : Environ.env -> private_constants -> Environ.env +(** Push the constants in the environment if not already there. *) + val universes_of_private : private_constants -> Univ.ContextSet.t list val is_curmod_library : safe_environment -> bool @@ -93,7 +88,6 @@ type 'a effect_entry = type global_declaration = | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration - | GlobalRecipe of Cooking.recipe type exported_private_constant = Constant.t * Entries.side_effect_role @@ -105,8 +99,11 @@ val export_private_constants : in_section:bool -> (** returns the main constant plus a list of auxiliary constants (empty unless one requires the side effects to be exported) *) val add_constant : - in_section:bool -> Label.t -> global_declaration -> - Constant.t safe_transformer + ?role:Entries.side_effect_role -> in_section:bool -> Label.t -> global_declaration -> + (Constant.t * private_constants) safe_transformer + +val add_recipe : + in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer (** Adding an inductive type *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 1857ea3329..24845ce459 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -31,7 +31,7 @@ open Mod_subst an inductive type. It can also be useful to allow reorderings in inductive types *) type namedobject = - | Constant of constant_body + | Constant of Opaqueproof.opaque constant_body | IndType of inductive * mutual_inductive_body | IndConstr of constructor * mutual_inductive_body diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index faa4411e92..74c6189a65 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -154,7 +154,7 @@ the polymorphic case let c = Constr.hcons j.uj_val in feedback_completion_typecheck feedback_id; c, uctx) in - let def = OpaqueDef (Opaqueproof.create proofterm) in + let def = OpaqueDef proofterm in { Cooking.cook_body = def; cook_type = tyj.utj_val; @@ -207,7 +207,7 @@ the polymorphic case in let def = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in let def = - if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty))) + if opaque then OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) else Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; @@ -232,7 +232,7 @@ let record_aux env s_ty s_bo = (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" v -let build_constant_declaration _kn env result = +let build_constant_declaration env result = let open Cooking in let typ = result.cook_type in let check declared inferred = @@ -271,11 +271,8 @@ let build_constant_declaration _kn env result = | Undef _ | Primitive _ -> Id.Set.empty | Def cs -> global_vars_set env (Mod_subst.force_constr cs) | OpaqueDef lc -> - let vars = - global_vars_set env - (Opaqueproof.force_proof (opaque_tables env) lc) in - (* we force so that cst are added to the env immediately after *) - ignore(Opaqueproof.force_constraints (opaque_tables env) lc); + let (lc, _) = Future.force lc in + let vars = global_vars_set env lc in if !Flags.record_aux_file then record_aux env ids_typ vars; vars in @@ -296,11 +293,15 @@ let build_constant_declaration _kn env result = check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) - OpaqueDef (Opaqueproof.iter_direct_opaque (fun c -> - let ids_typ = global_vars_set env typ in - let ids_def = global_vars_set env c in - let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in - check declared inferred) lc) in + let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in + let kont c = + let ids_typ = global_vars_set env typ in + let ids_def = global_vars_set env c in + let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in + check declared inferred + in + OpaqueDef (iter kont lc) + in let univs = result.cook_universes in let tps = let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in @@ -318,8 +319,8 @@ let build_constant_declaration _kn env result = (*s Global and local constant declaration. *) -let translate_constant mb env kn ce = - build_constant_declaration kn env +let translate_constant mb env _kn ce = + build_constant_declaration env (infer_declaration ~trust:mb env ce) let translate_local_assum env t = @@ -327,8 +328,21 @@ let translate_local_assum env t = let t = Typeops.assumption_of_judgment env j in j.uj_val, t -let translate_recipe ~hcons env kn r = - build_constant_declaration kn env (Cooking.cook_constant ~hcons r) +let translate_recipe ~hcons env _kn r = + let open Cooking in + let result = Cooking.cook_constant ~hcons r in + let univs = result.cook_universes in + let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in + let tps = Option.map Cemitcodes.from_val res in + { const_hyps = Option.get result.cook_context; + const_body = result.cook_body; + const_type = result.cook_type; + const_body_code = tps; + const_universes = univs; + const_private_poly_univs = result.cook_private_univs; + const_relevance = result.cook_relevance; + const_inline_code = result.cook_inline; + const_typing_flags = Environ.typing_flags env } let translate_local_def env _id centry = let open Cooking in @@ -351,8 +365,7 @@ let translate_local_def env _id centry = | Def _ -> () | OpaqueDef lc -> let ids_typ = global_vars_set env typ in - let ids_def = global_vars_set env - (Opaqueproof.force_proof (opaque_tables env) lc) in + let ids_def = global_vars_set env (fst (Future.force lc)) in record_aux env ids_typ ids_def end; let () = match decl.cook_universes with @@ -362,8 +375,7 @@ let translate_local_def env _id centry = let c = match decl.cook_body with | Def c -> Mod_subst.force_constr c | OpaqueDef o -> - let p = Opaqueproof.force_proof (Environ.opaque_tables env) o in - let cst = Opaqueproof.force_constraints (Environ.opaque_tables env) o in + let (p, cst) = Future.force o in (** Let definitions are ensured to have no extra constraints coming from the body by virtue of the typing of [Entries.section_def_entry]. *) let () = assert (Univ.ContextSet.is_empty cst) in diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 1fa5eca2e3..592a97e132 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -33,14 +33,14 @@ val translate_local_assum : env -> types -> types * Sorts.relevance val translate_constant : 'a trust -> env -> Constant.t -> 'a constant_entry -> - constant_body + Opaqueproof.proofterm constant_body -val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> constant_body +val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body (** Internal functions, mentioned here for debug purpose only *) val infer_declaration : trust:'a trust -> env -> - 'a constant_entry -> Cooking.result + 'a constant_entry -> Opaqueproof.proofterm Cooking.result val build_constant_declaration : - Constant.t -> env -> Cooking.result -> constant_body + env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body diff --git a/library/global.ml b/library/global.ml index 06e06a8cf2..58e2380440 100644 --- a/library/global.ml +++ b/library/global.ml @@ -94,7 +94,8 @@ let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) -let add_constant ~in_section id d = globalize (Safe_typing.add_constant ~in_section (i2l id) d) +let add_constant ?role ~in_section id d = globalize (Safe_typing.add_constant ?role ~in_section (i2l id) d) +let add_recipe ~in_section id d = globalize (Safe_typing.add_recipe ~in_section (i2l id) d) let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) diff --git a/library/global.mli b/library/global.mli index a60de48897..984d8c666c 100644 --- a/library/global.mli +++ b/library/global.mli @@ -46,7 +46,8 @@ val export_private_constants : in_section:bool -> unit Entries.definition_entry * Safe_typing.exported_private_constant list val add_constant : - in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t + ?role:Entries.side_effect_role -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * Safe_typing.private_constants +val add_recipe : in_section:bool -> Id.t -> Cooking.recipe -> Constant.t val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t @@ -84,7 +85,7 @@ val add_module_parameter : (** {6 Queries in the global environment } *) val lookup_named : variable -> Constr.named_declaration -val lookup_constant : Constant.t -> Declarations.constant_body +val lookup_constant : Constant.t -> Opaqueproof.opaque Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body val lookup_pinductive : Constr.pinductive -> @@ -105,7 +106,7 @@ val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option polymorphic constants, the term contains De Bruijn universe variables that need to be instantiated. *) -val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option +val body_of_constant_body : Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *) (** {6 Compiled libraries } *) diff --git a/library/lib.ml b/library/lib.ml index a046360822..4be288ed20 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -211,9 +211,6 @@ let split_lib_at_opening sp = let add_entry sp node = lib_state := { !lib_state with lib_stk = (sp,node) :: !lib_state.lib_stk } -let pull_to_head oname = - lib_state := { !lib_state with lib_stk = (oname,List.assoc oname !lib_state.lib_stk) :: List.remove_assoc oname !lib_state.lib_stk } - let anonymous_id = let n = ref 0 in fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n)) diff --git a/library/lib.mli b/library/lib.mli index 30569197bc..5da76961a6 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -57,7 +57,6 @@ val segment_of_objects : val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit -val pull_to_head : Libobject.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 4425e41652..4769c2dc53 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -102,6 +102,7 @@ let start_deriving f suchthat lemma = let terminator = Proof_global.make_terminator terminator in let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in - fst @@ Proof_global.with_current_proof begin fun _ p -> - Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p + Proof_global.simple_with_current_proof begin fun _ p -> + let p,_,() = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in + p end pstate diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index d27c79cb62..bf98f8cd70 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -16,9 +16,9 @@ open Environ open Evd open Miniml -val extract_constant : env -> Constant.t -> constant_body -> ml_decl +val extract_constant : env -> Constant.t -> Opaqueproof.opaque constant_body -> ml_decl -val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec +val extract_constant_spec : env -> Constant.t -> 'a constant_body -> ml_spec (** For extracting "module ... with ..." declaration *) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 399a77c596..4e229a94b6 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -109,7 +109,7 @@ let labels_of_ref r = (*s Constants tables. *) -let typedefs = ref (Cmap_env.empty : (constant_body * ml_type) Cmap_env.t) +let typedefs = ref (Cmap_env.empty : (Opaqueproof.opaque constant_body * ml_type) Cmap_env.t) let init_typedefs () = typedefs := Cmap_env.empty let add_typedef kn cb t = typedefs := Cmap_env.add kn (cb,t) !typedefs @@ -120,7 +120,7 @@ let lookup_typedef kn cb = with Not_found -> None let cst_types = - ref (Cmap_env.empty : (constant_body * ml_schema) Cmap_env.t) + ref (Cmap_env.empty : (Opaqueproof.opaque constant_body * ml_schema) Cmap_env.t) let init_cst_types () = cst_types := Cmap_env.empty let add_cst_type kn cb s = cst_types := Cmap_env.add kn (cb,s) !cst_types let lookup_cst_type kn cb = diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index acc1bfee8a..7e53964642 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -72,11 +72,11 @@ val labels_of_ref : GlobRef.t -> ModPath.t * Label.t list [mutual_inductive_body] as checksum. In both case, we should ideally also check the env *) -val add_typedef : Constant.t -> constant_body -> ml_type -> unit -val lookup_typedef : Constant.t -> constant_body -> ml_type option +val add_typedef : Constant.t -> Opaqueproof.opaque constant_body -> ml_type -> unit +val lookup_typedef : Constant.t -> Opaqueproof.opaque constant_body -> ml_type option -val add_cst_type : Constant.t -> constant_body -> ml_schema -> unit -val lookup_cst_type : Constant.t -> constant_body -> ml_schema option +val add_cst_type : Constant.t -> Opaqueproof.opaque constant_body -> ml_schema -> unit +val lookup_cst_type : Constant.t -> Opaqueproof.opaque constant_body -> ml_schema option val add_ind : MutInd.t -> mutual_inductive_body -> ml_ind -> unit val lookup_ind : MutInd.t -> mutual_inductive_body -> ml_ind option diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 469551809c..12b12bc7b0 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -278,7 +278,7 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF } | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) - => { VtUnknown, VtNow } + => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater } -> { add_morphism_infer atts m n } diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index a68efa4713..963b7189f9 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1800,7 +1800,7 @@ let anew_instance ~pstate atts binders instance fields = let program_mode = atts.program in new_instance ~pstate ~program_mode atts.polymorphic binders instance (Some (true, CAst.make @@ CRecord (fields))) - ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info + ~global:atts.global ~generalize:false Hints.empty_hint_info let declare_instance_refl ~pstate atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 075ebf006a..0a5c85f4ab 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -290,7 +290,7 @@ let finalize_view s0 ?(simple_types=true) p = Goal.enter_one ~__LOC__ begin fun g -> let env = Goal.env g in let sigma = Goal.sigma g in - let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in + let evars_of_p = Evd.evars_of_term sigma p in let filter x _ = Evar.Set.mem x evars_of_p in let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in let p = Reductionops.nf_evar sigma p in @@ -307,7 +307,7 @@ Goal.enter_one ~__LOC__ begin fun g -> let und0 = (* Unassigned evars in the initial goal *) let sigma0 = Tacmach.project s0 in let g0info = Evd.find sigma0 (Tacmach.sig_it s0) in - let g0 = Evd.evars_of_filtered_evar_info g0info in + let g0 = Evd.evars_of_filtered_evar_info sigma0 g0info in List.filter (fun k -> Evar.Set.mem k g0) (List.map fst (Evar.Map.bindings (Evd.undefined_map sigma0))) in let rigid = rigid_of und0 in diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 4e0866a0c5..adbcfb8f3b 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -529,8 +529,8 @@ exception FoundUnif of (evar_map * UState.t * tpattern) (* Note: we don't update env as we descend into the term, as the primitive *) (* unification procedure always rejects subterms with bound variables. *) -let dont_impact_evars_in cl = - let evs_in_cl = Evd.evars_of_term cl in +let dont_impact_evars_in sigma0 cl = + let evs_in_cl = Evd.evars_of_term sigma0 cl in fun sigma -> Evar.Set.for_all (fun k -> try let _ = Evd.find_undefined sigma k in true with Not_found -> false) evs_in_cl @@ -544,7 +544,7 @@ let dont_impact_evars_in cl = (* - w_unify expands let-in (zeta conversion) eagerly, whereas we want to *) (* match a head let rigidly. *) let match_upats_FO upats env sigma0 ise orig_c = - let dont_impact_evars = dont_impact_evars_in orig_c in + let dont_impact_evars = dont_impact_evars_in sigma0 (EConstr.of_constr orig_c) in let rec loop c = let f, a = splay_app ise c in let i0 = ref (-1) in let fpats = @@ -586,7 +586,7 @@ let match_upats_FO upats env sigma0 ise orig_c = let match_upats_HO ~on_instance upats env sigma0 ise c = - let dont_impact_evars = dont_impact_evars_in c in + let dont_impact_evars = dont_impact_evars_in sigma0 (EConstr.of_constr c) in let it_did_match = ref false in let failed_because_of_TC = ref false in let rec aux upats env sigma0 ise c = diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index c9f18d89be..5ea9b79336 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -145,7 +145,7 @@ let mkSTACK = function type cbv_infos = { env : Environ.env; - tab : cbv_value Declarations.constant_def KeyTable.t; + tab : (cbv_value, Empty.t) Declarations.constant_def KeyTable.t; reds : RedFlags.reds; sigma : Evd.evar_map } diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 062e3ca8b2..82726eccf0 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -708,9 +708,6 @@ type binder_kind = BProd | BLambda | BLetIn (**********************************************************************) (* Main detyping function *) -let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable.")) -let set_detype_anonymous f = detype_anonymous := f - let detype_level sigma l = let l = hack_qualid_of_univ_level sigma l in GType (UNamed l) @@ -732,11 +729,13 @@ and detype_r d flags avoid env sigma t = match EConstr.kind sigma (collapse_appl sigma t) with | Rel n -> (try match lookup_name_of_rel n (fst env) with - | Name id -> GVar id - | Anonymous -> GVar (!detype_anonymous n) + | Name id -> GVar id + | Anonymous -> + let s = "_ANONYMOUS_REL_"^(string_of_int n) in + GVar (Id.of_string s) with Not_found -> - let s = "_UNBOUND_REL_"^(string_of_int n) - in GVar (Id.of_string s)) + let s = "_UNBOUND_REL_"^(string_of_int n) + in GVar (Id.of_string s)) | Meta n -> (* Meta in constr are not user-parsable and are mapped to Evar *) if n = Constr_matching.special_meta then diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 1a8e97efb8..00b0578a52 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -68,9 +68,6 @@ val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> clo val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option -(* XXX: This is a hack and should go away *) -val set_detype_anonymous : (?loc:Loc.t -> int -> Id.t) -> unit - val force_wildcard : unit -> bool val synthetize_type : unit -> bool diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 4f36354f79..52e15f466f 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -98,7 +98,7 @@ let solve ?with_end_tac gi info_lvl tac pr = else tac in let env = Global.env () in - let (p,(status,info)) = Proof.run_tactic env tac pr in + let (p,(status,info),()) = Proof.run_tactic env tac pr in let env = Global.env () in let sigma = Evd.from_env env in let () = @@ -161,7 +161,7 @@ let refine_by_tactic ~name ~poly env sigma ty tac = let prev_future_goals = save_future_goals sigma in (* Start a proof *) let prf = Proof.start ~name ~poly sigma [env, ty] in - let (prf, _) = + let (prf, _, ()) = try Proof.run_tactic env tac prf with Logic_monad.TacticFailure e as src -> (* Catch the inner error of the monad tactic *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 778d98b2cd..09e4e898fe 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -372,7 +372,7 @@ let run_tactic env tac pr = let sp = pr.proofview in let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in let tac = - tac >>= fun () -> + tac >>= fun result -> Proofview.tclEVARMAP >>= fun sigma -> (* Already solved goals are not to be counted as shelved. Nor are they to be marked as unresolvable. *) @@ -383,10 +383,10 @@ let run_tactic env tac pr = CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up."); let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in Proofview.Unsafe.tclEVARS sigma >>= fun () -> - Proofview.tclUNIT retrieved + Proofview.tclUNIT (result,retrieved) in let { name; poly } = pr in - let (retrieved,proofview,(status,to_shelve,give_up),info_trace) = + let ((result,retrieved),proofview,(status,to_shelve,give_up),info_trace) = Proofview.apply ~name ~poly env tac sp in let sigma = Proofview.return proofview in @@ -400,7 +400,7 @@ let run_tactic env tac pr = in let given_up = pr.given_up@give_up in let proofview = Proofview.Unsafe.reset_future_goals proofview in - { pr with proofview ; shelf ; given_up },(status,info_trace) + { pr with proofview ; shelf ; given_up },(status,info_trace),result (*** Commands ***) @@ -425,7 +425,7 @@ module V82 = struct { Evd.it=List.hd gls ; sigma=sigma; } let top_evars p = - Proofview.V82.top_evars p.entry + Proofview.V82.top_evars p.entry p.proofview let grab_evars p = if not (is_done p) then diff --git a/proofs/proof.mli b/proofs/proof.mli index 1f4748141a..248b9d921e 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -172,7 +172,7 @@ val no_focused_goal : t -> bool used. In which case it is [false]. *) val run_tactic : Environ.env - -> unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) + -> 'a Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) * 'a val maximal_unfocus : 'a focus_kind -> t -> t diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 08b98d702a..40ae4acc88 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -345,6 +345,6 @@ let update_global_env (pf : t) = with_current_proof (fun _ p -> Proof.in_proof p (fun sigma -> let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in - let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in + let (p,(status,info),()) = Proof.run_tactic (Global.env ()) tac p in (p, ()))) pf in res diff --git a/proofs/refine.ml b/proofs/refine.ml index 06e6b89df1..4a9404aa96 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -44,17 +44,6 @@ let typecheck_evar ev env sigma = let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in sigma -(* Get the side-effect's constant declarations to update the monad's - * environmnent *) -let add_if_undefined env eff = - let open Entries in - try ignore(Environ.lookup_constant eff.seff_constant env); env - with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env - -(* Add the side effects to the monad's environment, if not already done. *) -let add_side_effects env eff = - List.fold_left add_if_undefined env eff - let generic_refine ~typecheck f gl = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in @@ -71,8 +60,7 @@ let generic_refine ~typecheck f gl = let evs = Evd.save_future_goals sigma in (* Redo the effects in sigma in the monad's env *) let privates_csts = Evd.eval_side_effects sigma in - let sideff = Safe_typing.side_effects_of_private_constants privates_csts in - let env = add_side_effects env sideff in + let env = Safe_typing.push_private_constants env privates_csts in (* Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 2b32838964..04f10e7399 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -41,8 +41,8 @@ let simple_goal sigma g gs = let open Evd in let open Evarutil in let evi = Evd.find sigma g in - Set.is_empty (evars_of_term (EConstr.Unsafe.to_constr evi.evar_concl)) && - Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) && + Set.is_empty (evars_of_term sigma evi.evar_concl) && + Set.is_empty (evars_of_filtered_evar_info sigma (nf_evar_info sigma evi)) && not (List.exists (Proofview.depends_on sigma g) gs) let is_focused_goal_simple ~doc id = diff --git a/stm/stm.ml b/stm/stm.ml index 3eb6d03529..6f7cefb582 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -364,7 +364,6 @@ module VCS : sig val set_parsing_state : id -> Vernacstate.Parser.state -> unit val get_parsing_state : id -> Vernacstate.Parser.state option val get_proof_mode : id -> Pvernac.proof_mode option - val set_proof_mode : id -> Pvernac.proof_mode option -> unit (* cuts from start -> stop, raising Expired if some nodes are not there *) val slice : block_start:id -> block_stop:id -> vcs @@ -572,6 +571,7 @@ end = struct (* {{{ *) (match Vernacprop.under_control x with | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i + | VernacInstance (_,(({CAst.v=Name i},_),_,_),_,_) -> Id.to_string i | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind @@ -611,7 +611,6 @@ end = struct (* {{{ *) info.state <- new_state let get_proof_mode id = (get_info id).proof_mode - let set_proof_mode id pm = (get_info id).proof_mode <- pm let reached id = let info = get_info id in @@ -2085,8 +2084,8 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_fail ~st fail (fun () -> (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> - ignore(TaskQueue.with_n_workers nworkers (fun queue -> - PG_compat.with_current_proof (fun _ p -> + TaskQueue.with_n_workers nworkers (fun queue -> + PG_compat.simple_with_current_proof (fun _ p -> let Proof.{goals} = Proof.data p in let open TacTask in let res = CList.map_i (fun i g -> @@ -2131,7 +2130,8 @@ end = struct (* {{{ *) if solve then Tacticals.New.tclSOLVE [] else tclUNIT () end) in - Proof.run_tactic (Global.env()) assign_tac p)))) ()) + let p,_,() = Proof.run_tactic (Global.env()) assign_tac p in + p))) ()) end (* }}} *) @@ -3049,53 +3049,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) VCS.set_parsing_state id parsing_state) new_ids; `Ok - (* Unknown: we execute it, check for open goals and propagate sideeff *) - | VtUnknown, VtNow -> - let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in - if not (get_allow_nested_proofs ()) && in_proof then - "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on." - |> Pp.str - |> (fun s -> (UserError (None, s), Exninfo.null)) - |> State.exn_on ~valid:Stateid.dummy newtip - |> Exninfo.iraise - else - let id = VCS.new_node ~id:newtip proof_mode () in - let head_id = VCS.get_branch_pos head in - let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *) - let step () = - VCS.checkout VCS.Branch.master; - let mid = VCS.get_branch_pos VCS.Branch.master in - let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in - let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_vernac_interp id st x); - (* Vernac x may or may not start a proof *) - if not in_proof && PG_compat.there_are_pending_proofs () then - begin - let bname = VCS.mk_branch_name x in - let opacity_of_produced_term = function - (* This AST is ambiguous, hence we check it dynamically *) - | VernacInstance (_,_ , None, _) -> GuaranteesOpacity - | _ -> Doesn'tGuaranteeOpacity in - VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[])); - VCS.set_proof_mode id (Some (Vernacentries.get_default_proof_mode ())); - VCS.branch bname (`Proof (VCS.proof_nesting () + 1)); - end else begin - begin match (VCS.get_branch head).VCS.kind with - | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - | `Proof _ -> - VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - (* We hope it can be replayed, but we can't really know *) - ignore(VCS.propagate_sideff ~action:(ReplayCommand x)); - end; - VCS.checkout_shallowest_proof_branch (); - end in - State.define ~doc ~safe_id:head_id ~cache:true step id; - Backtrack.record (); `Ok - - | VtUnknown, VtLater -> - anomaly(str"classifier: VtUnknown must imply VtNow.") - | VtProofMode pm, VtNow -> let proof_mode = Pvernac.lookup_proof_mode pm in let id = VCS.new_node ~id:newtip proof_mode () in @@ -3105,7 +3058,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VtProofMode _, VtLater -> anomaly(str"classifier: VtProofMode must imply VtNow.") - end in let pr_rc rc = match rc with | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"]) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 4a4c5c94e9..7cecd801e4 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -21,7 +21,6 @@ let string_of_parallel = function | `No -> "" let string_of_vernac_type = function - | VtUnknown -> "Unknown" | VtStartProof _ -> "StartProof" | VtSideff _ -> "Sideff" | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)" @@ -61,7 +60,7 @@ let options_affecting_stm_scheduling = ] let classify_vernac e = - let static_classifier ~poly e = match e with + let static_classifier ~atts e = match e with (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) @@ -97,15 +96,18 @@ let classify_vernac e = VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater | VernacDefinition (_,({v=i},_),ProveBody _) -> - let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof(guarantee, idents_of_name i), VtLater + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof(guarantee, idents_of_name i), VtLater | VernacStartTheoremProof (_,l) -> - let ids = List.map (fun (({v=i}, _), _) -> i) l in - let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof (guarantee,ids), VtLater + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let ids = List.map (fun (({v=i}, _), _) -> i) l in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (guarantee,ids), VtLater | VernacFixpoint (discharge,l) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = - if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = @@ -115,8 +117,9 @@ let classify_vernac e = then VtStartProof (guarantee,ids), VtLater else VtSideff ids, VtLater | VernacCoFixpoint (discharge,l) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = - if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = @@ -185,8 +188,12 @@ let classify_vernac e = | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow | VernacProofMode pm -> VtProofMode pm, VtNow - (* These are ambiguous *) - | VernacInstance _ -> VtUnknown, VtNow + | VernacInstance (_,((name,_),_,_),None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (guarantee, idents_of_name name.CAst.v), VtLater + | VernacInstance (_,((name,_),_,_),_,_) -> + VtSideff (idents_of_name name.CAst.v), VtLater (* Stm will install a new classifier to handle these *) | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ @@ -201,9 +208,8 @@ let classify_vernac e = with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in let rec static_control_classifier v = v |> CAst.with_val (function - | VernacExpr (f, e) -> - let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in - static_classifier ~poly e + | VernacExpr (atts, e) -> + static_classifier ~atts e | VernacTimeout (_,e) -> static_control_classifier e | VernacTime (_,e) | VernacRedirect (_, e) -> static_control_classifier e @@ -214,6 +220,6 @@ let classify_vernac e = | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtLater - | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater)) + | (VtStartProof _ | VtProofMode _), _ -> VtQuery, VtLater)) in static_control_classifier e diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 7a61deba0c..6dd9a976f9 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -158,9 +158,9 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = (* do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in (* ppedrot: seems legit to have abstracted subproofs as local*) - Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl + Declare.declare_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:true id decl in - let cst = Impargs.with_implicit_protection cst () in + let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Entries.const_entry_universes with | Entries.Monomorphic_entry _ -> EInstance.empty | Entries.Polymorphic_entry (_, ctx) -> @@ -174,7 +174,6 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let lem = mkConstU (cst, inst) in let evd = Evd.set_universe_context evd ectx in let open Safe_typing in - let eff = private_con_of_con (Global.safe_env ()) cst in let effs = concat_private eff Entries.(snd (Future.force const.const_entry_body)) in let solve = diff --git a/tactics/equality.ml b/tactics/equality.ml index f049f8c568..45a4799ea1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -417,7 +417,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d find_elim hdcncl lft2rgt dep cls (Some t) >>= fun elim -> general_elim_clause with_evars frzevars tac cls c t l (match lft2rgt with None -> false | Some b -> b) - {elimindex = None; elimbody = (elim,NoBindings); elimrename = None} + {elimindex = None; elimbody = (elim,NoBindings) } end let adjust_rewriting_direction args lft2rgt = diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 16829482e5..b9485b8823 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -116,8 +116,7 @@ let compute_name internal id = | InternalTacticRequest -> Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name -let define internal id c poly univs = - let fd = declare_constant ~internal in +let define internal role id c poly univs = let id = compute_name internal id in let ctx = UState.minimize univs in let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in @@ -133,12 +132,12 @@ let define internal id c poly univs = const_entry_inline_code = false; const_entry_feedback = None; } in - let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in + let kn, eff = declare_private_constant ~role ~internal id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in let () = match internal with | InternalTacticRequest -> () | _-> definition_message id in - kn + kn, eff let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = let (c, ctx), eff = f mode ind in @@ -146,10 +145,10 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in + let role = Entries.Schema (ind, kind) in + let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in declare_scheme kind [|ind,const|]; - const, Safe_typing.concat_private - (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff + const, Safe_typing.concat_private neff eff let define_individual_scheme kind mode names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with @@ -163,15 +162,15 @@ let define_mutual_scheme_base kind suff f mode names mind = let ids = Array.init (Array.length mib.mind_packets) (fun i -> try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in - let consts = Array.map2 (fun id cl -> - define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in + let fold i effs id cl = + let role = Entries.Schema ((mind, i), kind)in + let cst, neff = define mode role id cl (Declareops.inductive_is_polymorphic mib) ctx in + (Safe_typing.concat_private neff effs, cst) + in + let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; - consts, - Safe_typing.concat_private - (Safe_typing.private_con_of_scheme - ~kind (Global.safe_env()) (Array.to_list schemes)) - eff + consts, eff let define_mutual_scheme kind mode names mind = match Hashtbl.find scheme_object_table kind with diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 4aa4d13e1e..6efa1ece9c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -204,10 +204,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = (str"Computed inversion goal was not closed in initial signature."); *) let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in - let pf = - fst (Proof.run_tactic env ( - tclTHEN intro (onLastHypId inv_op)) pf) - in + let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in let pfterm = List.hd (Proof.partial_proof pf) in let global_named_context = Global.named_context_val () in let ownSign = ref begin diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 806c955591..9dafa8bad9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -614,7 +614,7 @@ let cofix id = mutual_cofix id [] 0 type tactic_reduction = Reductionops.reduction_function type e_tactic_reduction = Reductionops.e_reduction_function -let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma = +let e_pf_change_decl (redfun : bool -> e_reduction_function) where env sigma decl = let open Context.Named.Declaration in match decl with | LocalAssum (id,ty) -> @@ -713,28 +713,61 @@ let e_change_in_hyp ~check ~reorder redfun (id,where) = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let hyp = Tacmach.New.pf_get_hyp id gl in - let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in + let (sigma, c) = e_pf_change_decl redfun where (Proofview.Goal.env gl) sigma hyp in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (convert_hyp ~check ~reorder c) end +type hyp_conversion = +| AnyHypConv (** Arbitrary conversion *) +| StableHypConv (** Does not introduce new dependencies on variables *) +| LocalHypConv (** Same as above plus no dependence on the named environment *) + let e_change_in_hyps ~check ~reorder f args = Proofview.Goal.enter begin fun gl -> - let fold (env, sigma) arg = - let (redfun, id, where) = f arg in - let hyp = - try lookup_named id env - with Not_found -> - raise (RefinerError (env, sigma, NoSuchHyp id)) + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let (env, sigma) = match reorder with + | LocalHypConv -> + (* If the reduction function is known not to depend on the named + context, then we can perform it in parallel. *) + let fold accu arg = + let (id, redfun) = f arg in + let old = try Id.Map.find id accu with Not_found -> [] in + Id.Map.add id (redfun :: old) accu + in + let reds = List.fold_left fold Id.Map.empty args in + let evdref = ref sigma in + let map d = + let id = NamedDecl.get_id d in + match Id.Map.find id reds with + | reds -> + let d = EConstr.of_named_decl d in + let fold redfun (sigma, d) = redfun env sigma d in + let (sigma, d) = List.fold_right fold reds (sigma, d) in + let () = evdref := sigma in + EConstr.Unsafe.to_named_decl d + | exception Not_found -> d in - let (sigma, d) = e_pf_change_decl redfun where hyp env sigma in - let sign = Logic.convert_hyp ~check ~reorder env sigma d in + let sign = Environ.map_named_val map (Environ.named_context_val env) in let env = reset_with_named_context sign env in - (env, sigma) + (env, !evdref) + | StableHypConv | AnyHypConv -> + let reorder = reorder == AnyHypConv in + let fold (env, sigma) arg = + let (id, redfun) = f arg in + let hyp = + try lookup_named id env + with Not_found -> + raise (RefinerError (env, sigma, NoSuchHyp id)) + in + let (sigma, d) = redfun env sigma hyp in + let sign = Logic.convert_hyp ~check ~reorder env sigma d in + let env = reset_with_named_context sign env in + (env, sigma) + in + List.fold_left fold (env, sigma) args in - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let (env, sigma) = List.fold_left fold (env, sigma) args in let ty = Proofview.Goal.concl gl in Proofview.Unsafe.tclEVARS sigma <*> @@ -851,10 +884,12 @@ let change ~check chg c cls = let f (id, occs, where) = let occl = bind_change_occurrences occs chg in let redfun deep env sigma t = change_on_subterm ~check Reduction.CONV deep c occl env sigma t in - (redfun, id, where) + let redfun env sigma d = e_pf_change_decl redfun where env sigma d in + (id, redfun) in + let reorder = if check then AnyHypConv else StableHypConv in (* Don't check, we do it already in [change_on_subterm] *) - e_change_in_hyps ~check:false ~reorder:check f hyps + e_change_in_hyps ~check:false ~reorder f hyps end let change_concl t = @@ -881,6 +916,22 @@ let pattern_option l = e_reduct_option ~check:false (pattern_occs l,DEFAULTcast) (* The main reduction function *) +let is_local_flag env flags = + if flags.rDelta then false + else + let check = function + | EvalVarRef _ -> false + | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (ConstRef c)) + in + List.for_all check flags.rConst + +let is_local_unfold env flags = + let check (_, c) = match c with + | EvalVarRef _ -> false + | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (ConstRef c)) + in + List.for_all check flags + let reduce redexp cl = let trace env sigma = let open Printer in @@ -889,23 +940,33 @@ let reduce redexp cl = in Proofview.Trace.name_tactic trace begin Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in let nbcl = (if cl.concl_occs = NoOccurrences then 0 else 1) + List.length hyps in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in - let reorder = match redexp with Fold _ | Pattern _ -> true | _ -> false in + let reorder = match redexp with + | Fold _ | Pattern _ -> AnyHypConv + | Simpl (flags, _) | Cbv flags | Cbn flags | Lazy flags -> + if is_local_flag env flags then LocalHypConv else StableHypConv + | Unfold flags -> + if is_local_unfold env flags then LocalHypConv else StableHypConv + | Red _ | Hnf | CbvVm _ | CbvNative _ -> StableHypConv + | ExtraRedExpr _ -> StableHypConv (* Should we be that lenient ?*) + in begin match cl.concl_occs with | NoOccurrences -> Proofview.tclUNIT () | occs -> let redexp = bind_red_expr_occurrences occs nbcl redexp in - let redfun = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in + let redfun = Redexpr.reduction_of_red_expr env redexp in e_change_in_concl ~check (revert_cast redfun) end <*> let f (id, occs, where) = let redexp = bind_red_expr_occurrences occs nbcl redexp in - let (redfun, _) = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in + let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in let redfun _ env sigma c = redfun env sigma c in - (redfun, id, where) + let redfun env sigma d = e_pf_change_decl redfun where env sigma d in + (id, redfun) in e_change_in_hyps ~check ~reorder f hyps end @@ -1302,14 +1363,11 @@ let do_replace id = function [Ti] and the first one (resp last one) being [G] whose hypothesis [id] is replaced by P using the proof given by [tac] *) -let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) - targetid id sigma0 clenv tac = +let clenv_refine_in with_evars targetid id sigma0 clenv tac = let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in let clenv = - if with_classes then { clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd } - else clenv in let new_hyp_typ = clenv_type clenv in if not with_evars then check_unresolved_evars_of_metas sigma0 clenv; @@ -1321,11 +1379,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd)) - (if sidecond_first then - Tacticals.New.tclTHENFIRST - (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac - else - Tacticals.New.tclTHENLAST + (Tacticals.New.tclTHENLAST (assert_after_then_gen with_clear naming new_hyp_typ tac) exact_tac) (********************************************) @@ -1360,22 +1414,25 @@ let rec contract_letin_in_lam_header sigma c = | LetIn (x,b,t,c) -> contract_letin_in_lam_header sigma (subst1 b c) | _ -> c -let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ()) - rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let elim = contract_letin_in_lam_header sigma elim in - let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in - let indmv = - (match EConstr.kind sigma (nth_arg sigma i elimclause.templval.rebus) with - | Meta mv -> mv - | _ -> user_err ~hdr:"elimination_clause" - (str "The type of elimination clause is not well-formed.")) +let elimination_in_clause_scheme env sigma with_evars ~flags + id hypmv elimclause = + let hyp = mkVar id in + let hyp_typ = Retyping.get_type_of env sigma hyp in + let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in + let elimclause'' = + (* The evarmap of elimclause is assumed to be an extension of hypclause, so + we do not need to merge the universes coming from hypclause. *) + try clenv_fchain ~with_univs:false ~flags hypmv elimclause hypclause + with PretypeError (env,evd,NoOccurrenceFound (op,_)) -> + (* Set the hypothesis name in the message *) + raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id))) in - let elimclause' = clenv_fchain ~flags indmv elimclause indclause in - Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags - end + let new_hyp_typ = clenv_type elimclause'' in + if EConstr.eq_constr sigma hyp_typ new_hyp_typ then + user_err ~hdr:"general_rewrite_in" + (str "Nothing to rewrite in " ++ Id.print id ++ str"."); + clenv_refine_in with_evars id id sigma elimclause'' + (fun id -> Proofview.tclUNIT ()) (* * Elimination tactic with bindings and using an arbitrary @@ -1387,11 +1444,10 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags type eliminator = { elimindex : int option; (* None = find it automatically *) - elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *) elimbody : EConstr.constr with_bindings } -let general_elim_clause_gen elimtac indclause elim = +let general_elim_clause with_evars flags where indclause elim = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -1399,7 +1455,27 @@ let general_elim_clause_gen elimtac indclause elim = let elimt = Retyping.get_type_of env sigma elimc in let i = match elim.elimindex with None -> index_of_ind_arg sigma elimt | Some i -> i in - elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause + let elimc = contract_letin_in_lam_header sigma elimc in + let elimclause = make_clenv_binding env sigma (elimc, elimt) lbindelimc in + let indmv = + (match EConstr.kind sigma (nth_arg sigma i elimclause.templval.rebus) with + | Meta mv -> mv + | _ -> user_err ~hdr:"elimination_clause" + (str "The type of elimination clause is not well-formed.")) + in + match where with + | None -> + let elimclause = clenv_fchain ~flags indmv elimclause indclause in + Clenvtac.res_pf elimclause ~with_evars ~with_classes:true ~flags + | Some id -> + let hypmv = + match List.remove Int.equal indmv (clenv_independent elimclause) with + | [a] -> a + | _ -> user_err ~hdr:"elimination_clause" + (str "The type of elimination clause is not well-formed.") + in + let elimclause = clenv_fchain ~flags indmv elimclause indclause in + elimination_in_clause_scheme env sigma with_evars ~flags id hypmv elimclause end let general_elim with_evars clear_flag (c, lbindc) elim = @@ -1408,12 +1484,12 @@ let general_elim with_evars clear_flag (c, lbindc) elim = let sigma = Tacmach.New.project gl in let ct = Retyping.get_type_of env sigma c in let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in - let elimtac = elimination_clause_scheme with_evars in let indclause = make_clenv_binding env sigma (c, t) lbindc in let sigma = meta_merge sigma (clear_metas indclause.evd) in + let flags = elim_flags () in Proofview.Unsafe.tclEVARS sigma <*> Tacticals.New.tclTHEN - (general_elim_clause_gen elimtac indclause elim) + (general_elim_clause with_evars flags None indclause elim) (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c) end @@ -1436,8 +1512,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = let elim = EConstr.of_constr elim in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (general_elim with_evars clear_flag (c,lbindc) - {elimindex = None; elimbody = (elim,NoBindings); - elimrename = Some (false, constructors_nrealdecls env (fst mind))}) + {elimindex = None; elimbody = (elim,NoBindings); }) end let general_case_analysis with_evars clear_flag (c,lbindc as cx) = @@ -1468,8 +1543,7 @@ let find_eliminator c gl = let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in if is_nonrec ind then raise IsNonrec; let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in - evd, {elimindex = None; elimbody = (c,NoBindings); - elimrename = Some (true, constructors_nrealdecls (Global.env()) ind)} + evd, { elimindex = None; elimbody = (c,NoBindings) } let default_elim with_evars clear_flag (c,_ as cx) = Proofview.tclORELSE @@ -1489,7 +1563,7 @@ let default_elim with_evars clear_flag (c,_ as cx) = let elim_in_context with_evars clear_flag c = function | Some elim -> general_elim with_evars clear_flag c - {elimindex = Some (-1); elimbody = elim; elimrename = None} + { elimindex = Some (-1); elimbody = elim } | None -> default_elim with_evars clear_flag c let elim with_evars clear_flag (c,lbindc as cx) elim = @@ -1515,48 +1589,6 @@ let simplest_elim c = default_elim false None (c,NoBindings) (e.g. it could replace id:A->B->C by id:C, knowing A/\B) *) -let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause = - (* The evarmap of elimclause is assumed to be an extension of hypclause, so - we do not need to merge the universes coming from hypclause. *) - try clenv_fchain ~with_univs:false ~flags mv elimclause hypclause - with PretypeError (env,evd,NoOccurrenceFound (op,_)) -> - (* Set the hypothesis name in the message *) - raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id))) - -let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) - id rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let elim = contract_letin_in_lam_header sigma elim in - let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in - let indmv = destMeta sigma (nth_arg sigma i elimclause.templval.rebus) in - let hypmv = - match List.remove Int.equal indmv (clenv_independent elimclause) with - | [a] -> a - | _ -> user_err ~hdr:"elimination_clause" - (str "The type of elimination clause is not well-formed.") - in - let elimclause' = clenv_fchain ~flags indmv elimclause indclause in - let hyp = mkVar id in - let hyp_typ = Retyping.get_type_of env sigma hyp in - let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in - let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in - let new_hyp_typ = clenv_type elimclause'' in - if EConstr.eq_constr sigma hyp_typ new_hyp_typ then - user_err ~hdr:"general_rewrite_in" - (str "Nothing to rewrite in " ++ Id.print id ++ str"."); - clenv_refine_in with_evars id id sigma elimclause'' - (fun id -> Proofview.tclUNIT ()) - end - -let general_elim_clause with_evars flags id c e = - let elim = match id with - | None -> elimination_clause_scheme with_evars ~with_classes:true ~flags - | Some id -> elimination_in_clause_scheme with_evars ~flags id - in - general_elim_clause_gen elim c e - (* Apply a tactic below the products of the conclusion of a lemma *) type conjunction_status = @@ -1828,7 +1860,7 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = in aux (make_clenv_binding env sigma (d,thm) lbind) -let apply_in_once ?(respect_opaque = false) sidecond_first with_delta +let apply_in_once ?(respect_opaque = false) with_delta with_destruct with_evars naming id (clear_flag,{ CAst.loc; v= d,lbind}) tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> @@ -1849,7 +1881,7 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in try let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in - clenv_refine_in ~sidecond_first with_evars targetid id sigma clause + clenv_refine_in with_evars targetid id sigma clause (fun id -> Tacticals.New.tclTHENLIST [ apply_clear_request clear_flag false c; @@ -1866,14 +1898,14 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta aux [] with_destruct d end -let apply_in_delayed_once ?(respect_opaque = false) sidecond_first with_delta +let apply_in_delayed_once ?(respect_opaque = false) with_delta with_destruct with_evars naming id (clear_flag,{CAst.loc;v=f}) tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let (sigma, c) = f env sigma in Tacticals.New.tclWITHHOLES with_evars - (apply_in_once ~respect_opaque sidecond_first with_delta with_destruct with_evars + (apply_in_once ~respect_opaque with_delta with_destruct with_evars naming id (clear_flag,CAst.(make ?loc c)) tac) sigma end @@ -2493,7 +2525,7 @@ and intro_pattern_action ?loc with_evars b style pat thin destopt tac id = clear [id] in let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings)) in - apply_in_delayed_once false true true with_evars naming id (None,CAst.make ?loc:loc' f) + apply_in_delayed_once true true with_evars naming id (None,CAst.make ?loc:loc' f) (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []]) and prepare_intros ?loc with_evars dft destopt = function @@ -2561,10 +2593,10 @@ let assert_as first hd ipat t = (* apply in as *) -let general_apply_in ?(respect_opaque=false) sidecond_first with_delta +let general_apply_in ?(respect_opaque=false) with_delta with_destruct with_evars id lemmas ipat = let tac (naming,lemma) tac id = - apply_in_delayed_once ~respect_opaque sidecond_first with_delta + apply_in_delayed_once ~respect_opaque with_delta with_destruct with_evars naming id lemma tac in Proofview.Goal.enter begin fun gl -> let destopt = @@ -2593,10 +2625,10 @@ let general_apply_in ?(respect_opaque=false) sidecond_first with_delta let apply_in simple with_evars id lemmas ipat = let lemmas = List.map (fun (k,{CAst.loc;v=l}) -> k, CAst.make ?loc (fun _ sigma -> (sigma,l))) lemmas in - general_apply_in false simple simple with_evars id lemmas ipat + general_apply_in simple simple with_evars id lemmas ipat let apply_delayed_in simple with_evars id lemmas ipat = - general_apply_in ~respect_opaque:true false simple simple with_evars id lemmas ipat + general_apply_in ~respect_opaque:true simple simple with_evars id lemmas ipat (*****************************) (* Tactics abstracting terms *) @@ -4183,7 +4215,7 @@ let find_induction_type isrec elim hyp0 gl = let scheme = compute_elim_sig sigma ~elimc elimt in if Option.is_empty scheme.indarg then error "Cannot find induction type"; let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in - let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in + let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in scheme, ElimUsing (elim,indsign) in match scheme.indref with @@ -4210,10 +4242,7 @@ let get_eliminator elim dep s gl = | ElimOver (isrec,id) -> let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in let _, (l, s) = compute_elim_signature elims id in - let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d))) - (List.rev s.branches) - in - evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l + evd, isrec, ({ elimindex = None; elimbody = elimc }, elimt), l (* Instantiate all meta variables of elimclause using lid, some elts of lid are parameters (first ones), the other are @@ -4257,7 +4286,7 @@ let recolle_clenv i params args elimclause gl = let induction_tac with_evars params indvars elim = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in - let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in + let ({ elimindex=i;elimbody=(elimc,lbindelimc) },elimt) = elim in let i = match i with None -> index_of_ind_arg sigma elimt | Some i -> i in (* elimclause contains this: (elimc ?i ?j ?k...?l) *) let elimc = contract_letin_in_lam_header sigma elimc in @@ -4362,7 +4391,7 @@ let induction_without_atomization isrec with_evars elim names lid = (* FIXME: Tester ca avec un principe dependant et non-dependant *) induction_tac with_evars params realindvars elim; ] in - let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in + let elim = ElimUsing (({ elimindex = Some (-1); elimbody = Option.get scheme.elimc }, scheme.elimt), indsign) in apply_induction_in_context with_evars None [] elim indvars names induct_tac end diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 9eb8196280..32c64bacf6 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -282,7 +282,6 @@ val compute_elim_sig : evar_map -> ?elimc:constr with_bindings -> types -> elim_ (** elim principle with the index of its inductive arg *) type eliminator = { elimindex : int option; (** None = find it automatically *) - elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *) elimbody : constr with_bindings } diff --git a/test-suite/bugs/closed/bug_10026.v b/test-suite/bugs/closed/bug_10026.v new file mode 100644 index 0000000000..0d3142d0f2 --- /dev/null +++ b/test-suite/bugs/closed/bug_10026.v @@ -0,0 +1,3 @@ +Require Import Coq.Lists.List. +Set Debug RAKAM. +Check fun _ => fold_right (fun A B => prod A B) unit _. diff --git a/test-suite/bugs/closed/bug_10189.v b/test-suite/bugs/closed/bug_10189.v new file mode 100644 index 0000000000..d603bff386 --- /dev/null +++ b/test-suite/bugs/closed/bug_10189.v @@ -0,0 +1,9 @@ +Definition foo : forall (x := unit) {y : nat}, nat := fun y => y. +Check foo (y := 3). (*We fail to get implicits in the type past a let-in*) +Definition foo' : forall (x : Set) {y : nat}, nat := fun _ y => y. +Check foo' unit (y := 3). (* It works with a function binder *) + +Definition bar := let f {x} : nat -> nat := fun y => x in f (x := 3). +(* Adding bar : nat -> nat gives implicits-in-term warning *) +Fail Check bar (x := 3). +(* The implicits from the type of the local definition leak to the outer term *) diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/closed/bug_3754.v index 18820b1a4c..7031cbf132 100644 --- a/test-suite/bugs/opened/bug_3754.v +++ b/test-suite/bugs/closed/bug_3754.v @@ -281,5 +281,7 @@ Defined. (factor2 fact)). rewrite <- ap_p_pp; rewrite_moveL_Mp_p. Set Debug Tactic Unification. - Fail rewrite (concat_Ap ff2). + rewrite (concat_Ap ff2). Abort. + +End Factorization. diff --git a/test-suite/bugs/closed/bug_3890.v b/test-suite/bugs/closed/bug_3890.v new file mode 100644 index 0000000000..e1823ac54c --- /dev/null +++ b/test-suite/bugs/closed/bug_3890.v @@ -0,0 +1,12 @@ +Set Nested Proofs Allowed. + +Class Foo. +Class Bar := b : Type. + +Instance foo : Foo. + +Instance bar : Bar. +exact Type. +Defined. + +Defined. diff --git a/test-suite/bugs/closed/bug_4429.v b/test-suite/bugs/closed/bug_4429.v deleted file mode 100644 index bf0e570ab8..0000000000 --- a/test-suite/bugs/closed/bug_4429.v +++ /dev/null @@ -1,31 +0,0 @@ -Require Import Arith.Compare_dec. -Require Import Unicode.Utf8. - -Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A := - match n with - | O => x - | S n' => f (my_nat_iter n' f x) - end. - -Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat := - match mn with - | (0, 0) => 0 - | (0, S n') => S n' - | (S m', 0) => S m' - | (S m', S n') => - match le_gt_dec (S m') (S n') with - | left _ => f (S m', S n' - S m') - | right _ => f (S m' - S n', S n') - end - end. - -Axiom max_correct_l : ∀ m n : nat, m <= max m n. -Axiom max_correct_r : ∀ m n : nat, n <= max m n. - -Hint Resolve max_correct_l max_correct_r : arith. - -Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')). -Proof. - intros. - Timeout 3 eauto with arith. -Qed. diff --git a/test-suite/bugs/closed/bug_4580.v b/test-suite/bugs/closed/bug_4580.v index a8a446cc9b..3f40569d61 100644 --- a/test-suite/bugs/closed/bug_4580.v +++ b/test-suite/bugs/closed/bug_4580.v @@ -2,6 +2,5 @@ Require Import Program. Class Foo (A : Type) := foo : A. -Unset Refine Instance Mode. Program Instance f1 : Foo nat := S _. Next Obligation. exact 0. Defined. diff --git a/test-suite/bugs/closed/bug_4638.v b/test-suite/bugs/closed/bug_4638.v new file mode 100644 index 0000000000..951fe5302b --- /dev/null +++ b/test-suite/bugs/closed/bug_4638.v @@ -0,0 +1,12 @@ +Set Nested Proofs Allowed. + +Class Foo. + +Goal True. + +Instance foo: Foo. +Qed. + +trivial. + +Qed. diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v deleted file mode 100644 index 9d83743b2a..0000000000 --- a/test-suite/bugs/opened/bug_3890.v +++ /dev/null @@ -1,22 +0,0 @@ -Set Nested Proofs Allowed. - -Class Foo. -Class Bar := b : Type. - -Set Refine Instance Mode. -Instance foo : Foo := _. -Unset Refine Instance Mode. -(* 1 subgoals, subgoal 1 (ID 4) - - ============================ - Foo *) - -Instance bar : Bar. -exact Type. -Defined. -(* bar is defined *) - -About foo. -(* foo not a defined object. *) - -Fail Defined. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 3888cafed3..736d05fefc 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -198,9 +198,7 @@ Module UniqueInstances. for it. *) Set Typeclasses Unique Instances. Class Eq (A : Type) : Set. - Set Refine Instance Mode. - Instance eqa : Eq nat := _. constructor. Qed. - Unset Refine Instance Mode. + Instance eqa : Eq nat. Qed. Instance eqb : Eq nat := {}. Class Foo (A : Type) (e : Eq A) : Set. Instance fooa : Foo _ eqa := {}. diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v index 05d63d9a47..49e0af9b2c 100644 --- a/theories/Compat/Coq89.v +++ b/theories/Compat/Coq89.v @@ -14,4 +14,3 @@ Local Set Warnings "-deprecated". Require Export Coq.Compat.Coq810. Unset Private Polymorphic Universes. -Set Refine Instance Mode. diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v index d8d222730e..1701bf4365 100644 --- a/user-contrib/Ltac2/Constr.v +++ b/user-contrib/Ltac2/Constr.v @@ -38,6 +38,7 @@ Ltac2 Type kind := [ | Fix (int array, int, ident option array, constr array, constr array) | CoFix (int, ident option array, constr array, constr array) | Proj (projection, constr) +| Uint63 (uint63) ]. Ltac2 @ external kind : constr -> kind := "ltac2" "constr_kind". diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index 16e7d7a6f9..dc1690bdfb 100644 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -14,6 +14,7 @@ Ltac2 Type int. Ltac2 Type string. Ltac2 Type char. Ltac2 Type ident. +Ltac2 Type uint63. (** Constr-specific built-in types *) Ltac2 Type meta. diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index d7e7b91ee6..da8600109e 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -424,8 +424,8 @@ let () = define1 "constr_kind" constr begin fun c -> Value.of_ext Value.val_projection p; Value.of_constr c; |] - | Int _ -> - assert false + | Int n -> + v_blk 17 [|Value.of_uint63 n|] end end @@ -503,6 +503,9 @@ let () = define1 "constr_make" valexpr begin fun knd -> let p = Value.to_ext Value.val_projection p in let c = Value.to_constr c in EConstr.mkProj (p, c) + | (17, [|n|]) -> + let n = Value.to_uint63 n in + EConstr.mkInt n | _ -> assert false in return (Value.of_constr c) diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 9fd01426de..254c2e5086 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -740,7 +740,6 @@ let register_redefinition ?(local = false) qid e = Lib.add_anonymous_leaf (inTac2Redefinition def) let perform_eval ~pstate e = - let open Proofview.Notations in let env = Global.env () in let (e, ty) = Tac2intern.intern ~strict:false e in let v = Tac2interp.interp Tac2interp.empty_environment e in @@ -761,12 +760,8 @@ let perform_eval ~pstate e = | Goal_select.SelectAll -> v | Goal_select.SelectAlreadyFocused -> assert false (* TODO **) in - (* HACK: the API doesn't allow to return a value *) - let ans = ref None in - let tac = (v >>= fun r -> ans := Some r; Proofview.tclUNIT ()) in - let (proof, _) = Proof.run_tactic (Global.env ()) tac proof in + let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in let sigma = Proof.in_proof proof (fun sigma -> sigma) in - let ans = match !ans with None -> assert false | Some r -> r in let name = int_name () in Feedback.msg_notice (str "- : " ++ pr_glbtype name (snd ty) ++ spc () ++ str "=" ++ spc () ++ diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml index e3127ab9df..1043d25a75 100644 --- a/user-contrib/Ltac2/tac2ffi.ml +++ b/user-contrib/Ltac2/tac2ffi.ml @@ -30,6 +30,8 @@ type valexpr = (** Open constructors *) | ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr (** Arbitrary data *) +| ValUint63 of Uint63.t + (** Primitive integers *) and closure = MLTactic : (valexpr, 'v) arity0 * 'v -> closure @@ -47,21 +49,21 @@ type t = valexpr let is_int = function | ValInt _ -> true -| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> false +| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> false let tag v = match v with | ValBlk (n, _) -> n -| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> +| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> CErrors.anomaly (Pp.str "Unexpected value shape") let field v n = match v with | ValBlk (_, v) -> v.(n) -| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> +| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> CErrors.anomaly (Pp.str "Unexpected value shape") let set_field v n w = match v with | ValBlk (_, v) -> v.(n) <- w -| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> +| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> CErrors.anomaly (Pp.str "Unexpected value shape") let make_block tag v = ValBlk (tag, v) @@ -192,7 +194,7 @@ let of_closure cls = ValCls cls let to_closure = function | ValCls cls -> cls -| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ -> assert false +| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ | ValUint63 _ -> assert false let closure = { r_of = of_closure; @@ -318,6 +320,17 @@ let open_ = { r_id = false; } +let of_uint63 n = ValUint63 n +let to_uint63 = function +| ValUint63 n -> n +| _ -> assert false + +let uint63 = { + r_of = of_uint63; + r_to = to_uint63; + r_id = false; +} + let of_constant c = of_ext val_constant c let to_constant c = to_ext val_constant c let constant = repr_ext val_constant diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli index bfc93d99e6..f8581061a0 100644 --- a/user-contrib/Ltac2/tac2ffi.mli +++ b/user-contrib/Ltac2/tac2ffi.mli @@ -28,6 +28,8 @@ type valexpr = (** Open constructors *) | ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr (** Arbitrary data *) +| ValUint63 of Uint63.t + (** Primitive integers *) type 'a arity @@ -143,6 +145,10 @@ val of_open : KerName.t * valexpr array -> valexpr val to_open : valexpr -> KerName.t * valexpr array val open_ : (KerName.t * valexpr array) repr +val of_uint63 : Uint63.t -> valexpr +val to_uint63 : valexpr -> Uint63.t +val uint63 : Uint63.t repr + type ('a, 'b) fun1 val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic diff --git a/vernac/classes.ml b/vernac/classes.ml index 9f233a2551..5a7f60584a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -31,16 +31,6 @@ module NamedDecl = Context.Named.Declaration open Decl_kinds open Entries -let refine_instance = ref false - -let () = Goptions.(declare_bool_option { - optdepr = true; - optname = "definition of instances by refining"; - optkey = ["Refine";"Instance";"Mode"]; - optread = (fun () -> !refine_instance); - optwrite = (fun b -> refine_instance := b) -}) - let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) @@ -328,6 +318,7 @@ let instance_hook k info global imps ?hook cst = (match hook with Some h -> h cst | None -> ()) let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = + (* XXX: Duplication of the declare_constant path *) let kind = IsDefinition Instance in let sigma = let levels = Univ.LSet.union (CVars.universes_of_constr termtype) @@ -349,14 +340,9 @@ let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst in let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma = Evd.minimize_universes sigma in - Pretyping.check_evars env (Evd.from_env env) sigma termtype; - let univs = Evd.check_univ_decl ~poly sigma decl in - let termtype = to_constr sigma termtype in + let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (ParameterEntry - (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) - in + (ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); instance_hook k pri global imps (ConstRef cst) @@ -374,6 +360,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po let obls, constr, typ = match term with | Some t -> + let termtype = EConstr.of_constr termtype in let obls, _, constr, typ = Obligations.eterm_obligations env id sigma 0 t termtype in obls, Some constr, typ @@ -400,7 +387,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po if not (Option.is_empty term) then let init_refine = Tacticals.New.tclTHENLIST [ - Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term))); + Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term)); Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls); Tactics.New.reduce_after_refine; ] @@ -418,7 +405,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po | None -> pstate) ()) -let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = +let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = let props = match props with | Some (true, { CAst.v = CRecord fs }) -> @@ -497,12 +484,12 @@ let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program (* Check that the type is free of evars now. *) Pretyping.check_evars env (Evd.from_env env) sigma termtype; let termtype = to_constr sigma termtype in - let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in let pstate = if not (Evd.has_undefined sigma) && not (Option.is_empty props) then - (declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype; + let term = to_constr sigma (Option.get term) in + (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype; None) - else if program_mode || refine || Option.is_empty props then + else if program_mode || Option.is_empty props then declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in id, pstate @@ -549,7 +536,7 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl = sigma, cl, u, c', ctx', ctx, imps, args, decl -let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mode +let new_instance ~pstate ?(global=false) ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in @@ -565,7 +552,7 @@ let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mo Namegen.next_global_ident_away i (Termops.vars_of_env env) in let env' = push_rel_context ctx env in - do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode + do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) pri = diff --git a/vernac/classes.mli b/vernac/classes.mli index e7f90ff306..57bb9ce312 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -48,7 +48,6 @@ val declare_instance_constant : val new_instance : pstate:Proof_global.t option -> ?global:bool (** Not global by default. *) -> - ?refine:bool (** Allow refinement *) -> program_mode:bool -> Decl_kinds.polymorphic -> local_binder_expr list -> diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 3406b6276f..27e31f486d 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -173,6 +173,11 @@ let do_assumptions ~pstate ~program_mode kind nl l = uvars, (coe,t,imps)) Univ.LSet.empty l in + (* XXX: Using `DeclareDef.prepare_parameter` here directly is not + possible as we indeed declare several parameters; however, + restrict_universe_context should be called in a centralized place + IMO, thus I think we should adapt `prepare_parameter` to handle + this case too. *) let sigma = Evd.restrict_universe_context sigma uvars in let uctx = Evd.check_univ_decl ~poly:(pi2 kind) sigma udecl in let ubinders = Evd.universe_binders sigma in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 12df3215ad..d2c986fe5c 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -88,11 +88,12 @@ let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ct let (c,ctx), sideff = Future.force ce.const_entry_body in assert(Safe_typing.empty_private_constants = sideff); assert(Univ.ContextSet.is_empty ctx); + Obligations.check_evars env evd; + let c = EConstr.of_constr c in let typ = match ce.const_entry_type with - | Some t -> t - | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c)) + | Some t -> EConstr.of_constr t + | None -> Retyping.get_type_of env evd c in - Obligations.check_evars env evd; let obls, _, c, cty = Obligations.eterm_obligations env ident evd 0 c typ in diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 20a2db7ca2..69e2a209eb 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -230,12 +230,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = in (* XXX: Capturing sigma here... bad bad *) let hook = Lemmas.mk_hook (hook sigma) in - (* XXX: Grounding non-ground terms here... bad bad *) - let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in - let fullctyp = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in Obligations.check_evars env sigma; let evars, _, evars_def, evars_typ = - Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp + Obligations.eterm_obligations env recname sigma 0 def typ in let ctx = Evd.evar_universe_context sigma in ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl @@ -246,7 +243,7 @@ let out_def = function | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.") let collect_evars_of_term evd c ty = - let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in + let evars = Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty) in Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) @@ -262,17 +259,13 @@ let do_program_recursive local poly fixkind fixl ntns = let evd = nf_evar_map_undefined evd in let collect_evars id def typ imps = (* Generalize by the recursive prototypes *) - let def = - EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) - and typ = - (* Worrying... *) - EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) - in + let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in + let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = Obligations.eterm_obligations env id evm - (List.length rec_sign) def typ - in (id, def, typ, imps, evars) + (List.length rec_sign) def typ in + (id, def, typ, imps, evars) in let (fixnames,fixrs,fixdefs,fixtypes) = fix in let fiximps = List.map pi2 info in diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 1c7cc5e636..317cf487cc 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -75,13 +75,7 @@ let adjust_guardness_conditions const = function List.interval 0 (List.length ((lam_assum c)))) lemma_guard (Array.to_list fixdefs) in *) - let fold env eff = - try - let _ = Environ.lookup_constant eff.seff_constant env in - env - with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env - in - let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in + let env = Safe_typing.push_private_constants env eff in let indexes = search_guard env possible_indexes fixdecls in @@ -395,10 +389,10 @@ let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms s maybe_declare_manual_implicits false ref imps; call_hook ?hook ctx [] strength ref) thms_data in let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in - let pstate, _ = Proof_global.with_current_proof (fun _ p -> + let pstate = Proof_global.simple_with_current_proof (fun _ p -> match init_tac with - | None -> p,(true,[]) - | Some tac -> Proof.run_tactic Global.(env ()) tac p) pstate in + | None -> p + | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in pstate let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms = diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1b1c618dc7..f768278dd7 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -39,7 +39,7 @@ let check_evars env evm = type oblinfo = { ev_name: int * Id.t; - ev_hyps: Constr.named_context; + ev_hyps: EConstr.named_context; ev_status: bool * Evar_kinds.obligation_definition_status; ev_chop: int option; ev_src: Evar_kinds.t Loc.located; @@ -50,11 +50,11 @@ type oblinfo = (** Substitute evar references in t using de Bruijn indices, where n binders were passed through. *) -let subst_evar_constr evs n idf t = +let subst_evar_constr evm evs n idf t = let seen = ref Int.Set.empty in let transparent = ref Id.Set.empty in let evar_info id = List.assoc_f Evar.equal id evs in - let rec substrec (depth, fixrels) c = match Constr.kind c with + let rec substrec (depth, fixrels) c = match EConstr.kind evm c with | Evar (k, args) -> let { ev_name = (id, idstr) ; ev_hyps = hyps ; ev_chop = chop } = @@ -84,18 +84,18 @@ let subst_evar_constr evs n idf t = in aux hyps args [] in if List.exists - (fun x -> match Constr.kind x with + (fun x -> match EConstr.kind evm x with | Rel n -> Int.List.mem n fixrels | _ -> false) args then transparent := Id.Set.add idstr !transparent; - mkApp (idf idstr, Array.of_list args) + EConstr.mkApp (idf idstr, Array.of_list args) | Fix _ -> - Constr.map_with_binders succfix substrec (depth, 1 :: fixrels) c - | _ -> Constr.map_with_binders succfix substrec (depth, fixrels) c + EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c + | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c in let t' = substrec (0, []) t in - t', !seen, !transparent + EConstr.to_constr evm t', !seen, !transparent (** Substitute variable references in t using de Bruijn indices, @@ -112,18 +112,18 @@ let subst_vars acc n t = to a product : forall H1 : t1, ..., forall Hn : tn, concl. Changes evars and hypothesis references to variable references. *) -let etype_of_evar evs hyps concl = +let etype_of_evar evm evs hyps concl = let open Context.Named.Declaration in let rec aux acc n = function decl :: tl -> - let t', s, trans = subst_evar_constr evs n mkVar (NamedDecl.get_type decl) in + let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar (NamedDecl.get_type decl) in let t'' = subst_vars acc 0 t' in let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in let s' = Int.Set.union s s' in let trans' = Id.Set.union trans trans' in (match decl with | LocalDef (id,c,_) -> - let c', s'', trans'' = subst_evar_constr evs n mkVar c in + let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in let c' = subst_vars acc 0 c' in mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest, Int.Set.union s'' s', @@ -131,7 +131,7 @@ let etype_of_evar evs hyps concl = | LocalAssum (id,_) -> mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') | [] -> - let t', s, trans = subst_evar_constr evs n mkVar concl in + let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in subst_vars acc 0 t', s, trans in aux [] 0 (List.rev hyps) @@ -151,7 +151,7 @@ let evar_dependencies evm oev = let one_step deps = Evar.Set.fold (fun ev s -> let evi = Evd.find evm ev in - let deps' = evars_of_filtered_evar_info evi in + let deps' = evars_of_filtered_evar_info evm evi in if Evar.Set.mem oev deps' then invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev) else Evar.Set.union deps' s) @@ -209,9 +209,7 @@ let eterm_obligations env name evm fs ?status t ty = (fun (id, (n, nstr), ev) l -> let hyps = Evd.evar_filtered_context ev in let hyps = trunc_named_context nc_len hyps in - let hyps = EConstr.Unsafe.to_named_context hyps in - let concl = EConstr.Unsafe.to_constr ev.evar_concl in - let evtyp, deps, transp = etype_of_evar l hyps concl in + let evtyp, deps, transp = etype_of_evar evm l hyps ev.evar_concl in let evtyp, hyps, chop = match chop_product fs evtyp with | Some t -> t, trunc_named_context fs hyps, fs @@ -237,9 +235,9 @@ let eterm_obligations env name evm fs ?status t ty = evn [] in let t', _, transparent = (* Substitute evar refs in the term by variables *) - subst_evar_constr evts 0 mkVar t + subst_evar_constr evm evts 0 EConstr.mkVar t in - let ty, _, _ = subst_evar_constr evts 0 mkVar ty in + let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in let evars = List.map (fun (ev, info) -> let { ev_name = (_, name); ev_status = force_status, status; @@ -252,7 +250,7 @@ let eterm_obligations env name evm fs ?status t ty = in name, typ, src, (force_status, status), deps, tac) evts in let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in - let evmap f c = pi1 (subst_evar_constr evts 0 f c) in + let evmap f c = pi1 (subst_evar_constr evm evts 0 f c) in Array.of_list (List.rev evars), (evnames, evmap), t', ty let hide_obligation () = diff --git a/vernac/obligations.mli b/vernac/obligations.mli index d25daeed9c..9214ddd4b9 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -26,14 +26,14 @@ val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar (* env, id, evars, number of function prototypes to try to clear from evars contexts, object and type *) val eterm_obligations : env -> Id.t -> evar_map -> int -> - ?status:Evar_kinds.obligation_definition_status -> constr -> types -> + ?status:Evar_kinds.obligation_definition_status -> EConstr.constr -> EConstr.types -> (Id.t * types * Evar_kinds.t Loc.located * (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array (* Existential key, obl. name, type as product, location of the original evar, associated tactic, status and dependencies as indexes into the array *) - * ((Evar.t * Id.t) list * ((Id.t -> constr) -> constr -> constr)) * + * ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * constr * types (* Translations from existential identifiers to obligation identifiers and for terms with existentials to closed terms, given a diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 118c126970..bf2efb2542 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -201,7 +201,7 @@ let set_emacs_print_strings () = let diff = "diff." in List.iter (fun b -> let (name, attrs) = b in - if diff = (String.sub name 0 (String.length diff)) then + if CString.is_sub diff name 0 then tag_map := CString.Map.add name { attrs with prefix = Some (Printf.sprintf "<%s>" name); suffix = Some (Printf.sprintf "</%s>" name) } diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index ef06e59316..730f5fd6da 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -36,7 +36,6 @@ type vernac_type = | VtProofMode of string (* To be removed *) | VtMeta - | VtUnknown and vernac_start = opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 4d89eaffd9..54e08d0e95 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -52,7 +52,6 @@ type vernac_type = | VtProofMode of string (* To be removed *) | VtMeta - | VtUnknown and vernac_start = opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = |