diff options
117 files changed, 1151 insertions, 1112 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 782efb5be..9e87d2ca7 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -307,6 +307,11 @@ /test-suite/coqwc/ @silene # Secondary maintainer @gares +/tools/TimeFileMaker.py @JasonGross +/tools/make-both-single-timing-files.py @JasonGross +/tools/make-both-time-files.py @JasonGross +/tools/make-one-time-file.py @JasonGross + ########## Toplevel ########## /toplevel/ @ejgallego diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 05d2c635a..a6eed661e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -342,6 +342,9 @@ ci-mtac2: ci-pidetop: <<: *ci-template +ci-quickchick: + <<: *ci-template-flambda + ci-sf: <<: *ci-template @@ -138,40 +138,6 @@ Then, you may want to consider whether you want to restore the autosaves) #run. endif -# Check that every compiled file around has a known source file. -# This should help preventing weird compilation failures caused by leftover -# compiled files after deleting or moving some source files. - -EXISTINGVO:=$(call find, '*.vo') -KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) -ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) - -EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa') -KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \ - $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) -KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ - $(MLIFILES:.mli=.cmi) \ - $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma -ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS)) - -ifeq (,$(findstring clean,$(MAKECMDGOALS))) # Skip this for 'make clean' and alii -ifndef ACCEPT_ALIEN_VO -ifdef ALIENVO -$(error Leftover compiled Coq files without known sources: $(ALIENVO); \ -remove them first, for instance via 'make voclean' or 'make alienclean' \ -(or skip this check via 'make ACCEPT_ALIEN_VO=1')) -endif -endif - -ifndef ACCEPT_ALIEN_OBJ -ifdef ALIENOBJS -$(error Leftover compiled OCaml files without known sources: $(ALIENOBJS); \ -remove them first, for instance via 'make clean' or 'make alienclean' \ -(or skip this check via 'make ACCEPT_ALIEN_OBJ=1')) -endif -endif -endif - # Apart from clean and tags, everything will be done in a sub-call to make # on Makefile.build. This way, we avoid doing here the -include of .d : # since they trigger some compilations, we do not want them for a mere clean. @@ -187,7 +153,7 @@ endif MAKE_OPTS := --warn-undefined-variable --no-builtin-rules -submake: +submake: alienclean $(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS) noconfig: @@ -283,6 +249,22 @@ devdocclean: rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex rm -f $(OCAMLDOCDIR)/html/*.html +# Ensure that every compiled file around has a known source file. +# This should help preventing weird compilation failures caused by leftover +# compiled files after deleting or moving some source files. + +EXISTINGVO:=$(call find, '*.vo') +KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) +ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) + +EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa') +KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \ + $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) +KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ + $(MLIFILES:.mli=.cmi) \ + $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma +ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS)) + alienclean: rm -f $(ALIENOBJS) $(ALIENVO) diff --git a/Makefile.ci b/Makefile.ci index ce725d19d..7f63157fa 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -17,6 +17,7 @@ CI_TARGETS=ci-bignums \ ci-cpdt \ ci-cross-crypto \ ci-elpi \ + ci-ext-lib \ ci-equations \ ci-fcsl-pcm \ ci-fiat-crypto \ @@ -31,6 +32,7 @@ CI_TARGETS=ci-bignums \ ci-math-comp \ ci-mtac2 \ ci-pidetop \ + ci-quickchick \ ci-sf \ ci-tlc \ ci-unimath \ @@ -50,6 +52,8 @@ ci-math-classes: ci-bignums ci-corn: ci-math-classes +ci-quickchick: ci-ext-lib + ci-formal-topology: ci-corn # Generic rule, we use make to ease travis integration with mixed rules diff --git a/checker/cic.mli b/checker/cic.mli index c4b00d0dc..27e2a479f 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -241,7 +241,7 @@ type constant_body = { const_type : constr; const_body_code : to_patch_substituted; const_universes : constant_universes; - const_proj : projection_body option; + const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; } diff --git a/checker/environ.ml b/checker/environ.ml index bbd043c8e..809150cea 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -7,6 +7,7 @@ open Declarations type globals = { env_constants : constant_body Cmap_env.t; + env_projections : projection_body Cmap_env.t; env_inductives : mutual_inductive_body Mindmap_env.t; env_inductives_eq : KerName.t KNmap.t; env_modules : module_body MPmap.t; @@ -34,6 +35,7 @@ let empty_oracle = { let empty_env = { env_globals = { env_constants = Cmap_env.empty; + env_projections = Cmap_env.empty; env_inductives = Mindmap_env.empty; env_inductives_eq = KNmap.empty; env_modules = MPmap.empty; @@ -165,12 +167,10 @@ let evaluable_constant cst env = with Not_found | NotEvaluableConst _ -> false let is_projection cst env = - not (Option.is_empty (lookup_constant cst env).const_proj) + (lookup_constant cst env).const_proj let lookup_projection p env = - match (lookup_constant (Projection.constant p) env).const_proj with - | Some pb -> pb - | None -> anomaly ("lookup_projection: constant is not a projection.") + Cmap_env.find (Projection.constant p) env.env_globals.env_projections (* Mutual Inductives *) let scrape_mind env kn= @@ -194,6 +194,13 @@ let add_mind kn mib env = Printf.ksprintf anomaly ("Inductive %s is already defined.") (MutInd.to_string kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in + let new_projections = match mib.mind_record with + | None | Some None -> env.env_globals.env_projections + | Some (Some (id, kns, pbs)) -> + Array.fold_left2 (fun projs kn pb -> + Cmap_env.add kn pb projs) + env.env_globals.env_projections kns pbs + in let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in let new_inds_eq = if KerName.equal kn1 kn2 then env.env_globals.env_inductives_eq @@ -201,8 +208,9 @@ let add_mind kn mib env = KNmap.add kn1 kn2 env.env_globals.env_inductives_eq in let new_globals = { env.env_globals with - env_inductives = new_inds; - env_inductives_eq = new_inds_eq} in + env_inductives = new_inds; + env_projections = new_projections; + env_inductives_eq = new_inds_eq} in { env with env_globals = new_globals } diff --git a/checker/environ.mli b/checker/environ.mli index 81da83875..4a7597249 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -5,6 +5,7 @@ open Cic type globals = { env_constants : constant_body Cmap_env.t; + env_projections : projection_body Cmap_env.t; env_inductives : mutual_inductive_body Mindmap_env.t; env_inductives_eq : KerName.t KNmap.t; env_modules : module_body MPmap.t; diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 7685863ea..ca9581167 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -47,13 +47,8 @@ let check_constant_declaration env kn cb = let () = match body_of_constant cb with | Some bd -> - (match cb.const_proj with - | None -> let j = infer envty bd in - conv_leq envty j ty - | Some pb -> - let env' = add_constant kn cb env' in - let j = infer env' bd in - conv_leq envty j ty) + let j = infer envty bd in + conv_leq envty j ty | None -> () in let env = diff --git a/checker/values.ml b/checker/values.ml index 1ac8d7cef..f7ab95fe2 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -15,7 +15,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 c4fdf8a846aed45c27b5acb1add7d1c6 checker/cic.mli +MD5 92de14d7bf9134532e8a0cff5618bd50 checker/cic.mli *) @@ -240,7 +240,7 @@ let v_cb = v_tuple "constant_body" v_constr; Any; v_const_univs; - Opt v_projbody; + v_bool; v_bool; v_typing_flags|] diff --git a/clib/cMap.ml b/clib/cMap.ml index f6e52594b..54a8b2585 100644 --- a/clib/cMap.ml +++ b/clib/cMap.ml @@ -35,9 +35,9 @@ sig val fold_left : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b val smartmap : ('a -> 'a) -> 'a t -> 'a t - (** [@@ocaml.deprecated "Same as [Smart.map]"] *) + [@@ocaml.deprecated "Same as [Smart.map]"] val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t - (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *) + [@@ocaml.deprecated "Same as [Smart.mapi]"] val height : 'a t -> int module Smart : sig @@ -66,9 +66,9 @@ sig val fold_left : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b val smartmap : ('a -> 'a) -> 'a map -> 'a map - (** [@@ocaml.deprecated "Same as [Smart.map]"] *) + [@@ocaml.deprecated "Same as [Smart.map]"] val smartmapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map - (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *) + [@@ocaml.deprecated "Same as [Smart.mapi]"] val height : 'a map -> int module Smart : sig diff --git a/clib/cMap.mli b/clib/cMap.mli index b45effb95..127bf23ab 100644 --- a/clib/cMap.mli +++ b/clib/cMap.mli @@ -58,10 +58,10 @@ sig (** Folding keys in decreasing order. *) val smartmap : ('a -> 'a) -> 'a t -> 'a t - (** [@@ocaml.deprecated "Same as [Smart.map]"] *) + [@@ocaml.deprecated "Same as [Smart.map]"] val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t - (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *) + [@@ocaml.deprecated "Same as [Smart.mapi]"] val height : 'a t -> int (** An indication of the logarithmic size of a map *) diff --git a/configure.ml b/configure.ml index 45c3bb67a..933143e68 100644 --- a/configure.ml +++ b/configure.ml @@ -33,7 +33,7 @@ let cprintf s = cfprintf stdout s let ceprintf s = cfprintf stderr s let die msg = ceprintf "%s%s%s\nConfiguration script failed!" red msg reset; exit 1 -let warn s = cprintf ("%sWarning: " ^^ s ^^ "%s") yellow reset +let warn s = kfprintf (fun oc -> cfprintf oc "%s" reset) stdout ("%sWarning: " ^^ s) yellow let s2i = int_of_string let i2s = string_of_int diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 5c882ee85..87d837b38 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -170,3 +170,15 @@ ######################################################################## : "${pidetop_CI_BRANCH:=v8.9}" : "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}" + +######################################################################## +# ext-lib +######################################################################## +: "${ext_lib_CI_BRANCH:=master}" +: "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib.git}" + +######################################################################## +# quickchick +######################################################################## +: "${quickchick_CI_BRANCH:=master}" +: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick.git}" diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index f867fd189..5b5cbd11a 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -8,6 +8,7 @@ export NJOBS if [ -n "${GITLAB_CI}" ]; then + export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH" export COQBIN="$PWD/_install_ci/bin" export CI_BRANCH="$CI_COMMIT_REF_NAME" if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]] @@ -27,6 +28,7 @@ else CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" export CI_BRANCH fi + export OCAMLPATH="$PWD:$OCAMLPATH" export COQBIN="$PWD/bin" fi export PATH="$COQBIN:$PATH" diff --git a/dev/ci/ci-ext-lib.sh b/dev/ci/ci-ext-lib.sh new file mode 100755 index 000000000..cf212c2fb --- /dev/null +++ b/dev/ci/ci-ext-lib.sh @@ -0,0 +1,16 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" + +# This script could be included inside other ones +# Let's avoid to source ci-common twice in this case +if [ -z "${CI_BUILD_DIR}" ]; +then + . "${ci_dir}/ci-common.sh" +fi + +ext_lib_CI_DIR="${CI_BUILD_DIR}/ExtLib" + +git_checkout "${ext_lib_CI_BRANCH}" "${ext_lib_CI_GITURL}" "${ext_lib_CI_DIR}" + +( cd "${ext_lib_CI_DIR}" && make && make install) diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh index 2ac4d2167..32cba0808 100755 --- a/dev/ci/ci-pidetop.sh +++ b/dev/ci/ci-pidetop.sh @@ -12,13 +12,11 @@ git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}" # `-local`. We need to improve this divergence but if we use Dune this # "local" oddity goes away automatically so not bothering... if [ -d "$COQBIN/../lib/coq" ]; then - COQOCAMLLIB="$COQBIN/../lib/" COQLIB="$COQBIN/../lib/coq/" else - COQOCAMLLIB="$COQBIN/../" COQLIB="$COQBIN/../" fi -( cd "${pidetop_CI_DIR}" && OCAMLPATH="$COQOCAMLLIB" jbuilder build @install ) +( cd "${pidetop_CI_DIR}" && jbuilder build @install ) echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh new file mode 100755 index 000000000..fc39e2685 --- /dev/null +++ b/dev/ci/ci-quickchick.sh @@ -0,0 +1,18 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" + +# This script could be included inside other ones +# Let's avoid to source ci-common twice in this case +if [ -z "${CI_BUILD_DIR}" ]; +then + . "${ci_dir}/ci-common.sh" +fi + +quickchick_CI_DIR="${CI_BUILD_DIR}/Quickchick" + +install_ssreflect + +git_checkout "${quickchick_CI_BRANCH}" "${quickchick_CI_GITURL}" "${quickchick_CI_DIR}" + +( cd "${quickchick_CI_DIR}" && make && make install) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 346b7c7dd..4838dd734 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -41,6 +41,15 @@ Printer.ml API pr_subgoal and pr_goal was removed to simplify the code. It was earlierly used by PCoq. +Source code organization + +- We have eliminated / fused some redundant modules and relocated a + few interfaces files. The `intf` folder is gone, and now for example + `Constrexpr` is located in `interp/`, `Vernacexpr` in `vernac/` and + so on. Changes should be compatible, but in a few cases stricter + layering requirements may mean that functions have moved. In all + cases adapting is a matter of changing the module name. + Vernacular commands - The implementation of vernacular commands has been refactored so it diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 3036fac81..35a605ddd 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -32,7 +32,16 @@ Names (link targets) are auto-generated for most simple objects, though they can - Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. - Vernac variants, tactic notations, and tactic variants do not have a default name. -Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. +Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects):: + + .. cmdv:: Lemma @ident {? @binders} : @type + Remark @ident {? @binders} : @type + Fact @ident {? @binders} : @type + Corollary @ident {? @binders} : @type + Proposition @ident {? @binders} : @type + :name: Lemma; Remark; Fact; Corollary; Proposition + + These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`. Notations --------- diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index f90efa995..f1d2541eb 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -32,7 +32,16 @@ Names (link targets) are auto-generated for most simple objects, though they can - Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. - Vernac variants, tactic notations, and tactic variants do not have a default name. -Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. +Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms). Undocumented objects should have the `:undocumented:` flag instead, as shown above. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects):: + + .. cmdv:: Lemma @ident {? @binders} : @type + Remark @ident {? @binders} : @type + Fact @ident {? @binders} : @type + Corollary @ident {? @binders} : @type + Proposition @ident {? @binders} : @type + :name: Lemma; Remark; Fact; Corollary; Proposition + + These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`. Notations --------- diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 6af6e7897..afb49413d 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -200,6 +200,8 @@ The following abbreviations are allowed: The type annotation ``:A`` can be omitted when ``A`` can be synthesized by the system. +.. _coq-equality: + Equality ++++++++ diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 53b993edd..6ea1c162f 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -13,42 +13,37 @@ Extensions of |Gallina| Record types ---------------- -The ``Record`` construction is a macro allowing the definition of +The :cmd:`Record` construction is a macro allowing the definition of records as is done in many programming languages. Its syntax is -described in the grammar below. In fact, the ``Record`` macro is more general +described in the grammar below. In fact, the :cmd:`Record` macro is more general than the usual record types, since it allows also for “manifest” -expressions. In this sense, the ``Record`` construction allows defining +expressions. In this sense, the :cmd:`Record` construction allows defining “signatures”. .. _record_grammar: .. productionlist:: `sentence` - record : `record_keyword` ident [binders] [: sort] := [ident] { [`field` ; … ; `field`] }. + record : `record_keyword` `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. record_keyword : Record | Inductive | CoInductive - field : name [binders] : type [ where notation ] - : | name [binders] [: term] := term + field : `ident` [ `binders` ] : `type` [ where `notation` ] + : | `ident` [ `binders` ] [: `type` ] := `term` In the expression: -.. cmd:: Record @ident {* @param } {? : @sort} := {? @ident} { {*; @ident {* @binder } : @term } } +.. cmd:: Record @ident @binders {? : @sort} := {? @ident} { {*; @ident @binders : @type } } -the first identifier `ident` is the name of the defined record and `sort` is its +the first identifier :token:`ident` is the name of the defined record and :token:`sort` is its type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted, -the default name ``Build_``\ `ident`, where `ident` is the record name, is used. If `sort` is +the default name ``Build_``\ :token:`ident`, where :token:`ident` is the record name, is used. If :token:`sort` is omitted, the default sort is `\Type`. The identifiers inside the brackets are the names of -fields. For a given field `ident`, its type is :g:`forall binder …, term`. +fields. For a given field :token:`ident`, its type is :g:`forall binders, type`. Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the -order of the fields is important. Finally, each `param` is a parameter of the record. +order of the fields is important. Finally, :token:`binders` are parameters of the record. More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, we might have: - -.. coqtop:: in - - Record ident param : sort := { ident₁ : type₁ ; ident₂ := term₂ ; ident₃ : type₃ }. - -in which case the correctness of |type_3| may rely on the instance |term_2| of |ident_2| and |term_2| in turn -may depend on |ident_1|. +:n:`Record @ident @binders : @sort := { @ident₁ : @type₁ ; @ident₂ := @term₂ ; @ident₃ : @type₃ }`. +in which case the correctness of :n:`@type₃` may rely on the instance :n:`@term₂` of :n:`@ident₂` and :n:`@term₂` may in turn depend on :n:`@ident₁`. .. example:: @@ -69,11 +64,10 @@ depends on both ``top`` and ``bottom``. Let us now see the work done by the ``Record`` macro. First the macro generates a variant type definition with just one constructor: +:n:`Variant @ident {? @binders } : @sort := @ident₀ {? @binders }`. -.. cmd:: Variant @ident {* @params} : @sort := @ident {* (@ident : @term_1)} - -To build an object of type `ident`, one should provide the constructor -|ident_0| with the appropriate number of terms filling the fields of the record. +To build an object of type :n:`@ident`, one should provide the constructor +:n:`@ident₀` with the appropriate number of terms filling the fields of the record. .. example:: Let us define the rational :math:`1/2`: @@ -379,6 +373,7 @@ we have the following equivalence Notice that the printing uses the :g:`if` syntax because `sumbool` is declared as such (see :ref:`controlling-match-pp`). +.. _irrefutable-patterns: Irrefutable patterns: the destructuring let variants ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 76a016ff6..c26ae2a93 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -48,26 +48,26 @@ Blanks Comments Comments in Coq are enclosed between ``(*`` and ``*)``, and can be nested. - They can contain any character. However, string literals must be + They can contain any character. However, :token:`string` literals must be correctly closed. Comments are treated as blanks. Identifiers and access identifiers - Identifiers, written ident, are sequences of letters, digits, ``_`` and + Identifiers, written :token:`ident`, are sequences of letters, digits, ``_`` and ``'``, that do not start with a digit or ``'``. That is, they are recognized by the following lexical class: .. productionlist:: coq first_letter : a..z ∣ A..Z ∣ _ ∣ unicode-letter subsequent_letter : a..z ∣ A..Z ∣ 0..9 ∣ _ ∣ ' ∣ unicode-letter ∣ unicode-id-part - ident : `first_letter` [`subsequent_letter` … `subsequent_letter`] - access_ident : . `ident` + ident : `first_letter`[`subsequent_letter`…`subsequent_letter`] + access_ident : .`ident` - All characters are meaningful. In particular, identifiers are case- - sensitive. The entry ``unicode-letter`` non-exhaustively includes Latin, + All characters are meaningful. In particular, identifiers are case-sensitive. + The entry ``unicode-letter`` non-exhaustively includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical letter-like - symbols, hyphens, non-breaking space, … The entry ``unicode-id-part`` non- - exhaustively includes symbols for prime letters and subscripts. + symbols, hyphens, non-breaking space, … The entry ``unicode-id-part`` + non-exhaustively includes symbols for prime letters and subscripts. Access identifiers, written :token:`access_ident`, are identifiers prefixed by `.` (dot) without blank. They are used in the syntax of qualified @@ -79,8 +79,8 @@ Natural numbers and integers .. productionlist:: coq digit : 0..9 - num : `digit` … `digit` - integer : [-] `num` + num : `digit`…`digit` + integer : [-]`num` Strings Strings are delimited by ``"`` (double quote), and enclose a sequence of @@ -139,14 +139,14 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : | `term` <: `term` : | `term` :> : | `term` -> `term` - : | `term` arg … arg + : | `term` `arg` … `arg` : | @ `qualid` [`term` … `term`] : | `term` % `ident` : | match `match_item` , … , `match_item` [`return_type`] with : [[|] `equation` | … | `equation`] end : | `qualid` : | `sort` - : | num + : | `num` : | _ : | ( `term` ) arg : `term` @@ -155,6 +155,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. binder : `name` : | ( `name` … `name` : `term` ) : | ( `name` [: `term`] := `term` ) + : | ' `pattern` name : `ident` | _ qualid : `ident` | `qualid` `access_ident` sort : Prop | Set | Type @@ -162,7 +163,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : | `fix_body` with `fix_body` with … with `fix_body` for `ident` cofix_bodies : `cofix_body` : | `cofix_body` with `cofix_body` with … with `cofix_body` for `ident` - fix_body : `ident` `binders` [annotation] [: `term`] := `term` + fix_body : `ident` `binders` [`annotation`] [: `term`] := `term` cofix_body : `ident` [`binders`] [: `term`] := `term` annotation : { struct `ident` } match_item : `term` [as `name`] [in `qualid` [`pattern` … `pattern`]] @@ -176,7 +177,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : | `pattern` % `ident` : | `qualid` : | _ - : | num + : | `num` : | ( `or_pattern` , … , `or_pattern` ) or_pattern : `pattern` | … | `pattern` @@ -185,7 +186,7 @@ Types ----- Coq terms are typed. Coq types are recognized by the same syntactic -class as :token`term`. We denote by :token:`type` the semantic subclass +class as :token:`term`. We denote by :production:`type` the semantic subclass of types inside the syntactic class :token:`term`. .. _gallina-identifiers: @@ -197,8 +198,8 @@ Qualified identifiers and simple identifiers (definitions, lemmas, theorems, remarks or facts), *global variables* (parameters or axioms), *inductive types* or *constructors of inductive types*. *Simple identifiers* (or shortly :token:`ident`) are a syntactic subset -of qualified identifiers. Identifiers may also denote local *variables*, -what qualified identifiers do not. +of qualified identifiers. Identifiers may also denote *local variables*, +while qualified identifiers do not. Numerals -------- @@ -211,7 +212,7 @@ numbers (see :ref:`datatypes`). .. note:: - negative integers are not at the same level as :token:`num`, for this + Negative integers are not at the same level as :token:`num`, for this would make precedence unnatural. Sorts @@ -220,12 +221,12 @@ Sorts There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`. - :g:`Prop` is the universe of *logical propositions*. The logical propositions - themselves are typing the proofs. We denote propositions by *form*. + themselves are typing the proofs. We denote propositions by :production:`form`. This constitutes a semantic subclass of the syntactic class :token:`term`. - :g:`Set` is is the universe of *program types* or *specifications*. The specifications themselves are typing the programs. We denote - specifications by *specif*. This constitutes a semantic subclass of + specifications by :production:`specif`. This constitutes a semantic subclass of the syntactic class :token:`term`. - :g:`Type` is the type of :g:`Prop` and :g:`Set` @@ -241,18 +242,18 @@ Various constructions such as :g:`fun`, :g:`forall`, :g:`fix` and :g:`cofix` *bind* variables. A binding is represented by an identifier. If the binding variable is not used in the expression, the identifier can be replaced by the symbol :g:`_`. When the type of a bound variable cannot be synthesized by the -system, it can be specified with the notation ``(ident : type)``. There is also +system, it can be specified with the notation :n:`(@ident : @type)`. There is also a notation for a sequence of binding variables sharing the same type: -``(``:token:`ident`:math:`_1`…:token:`ident`:math:`_n` : :token:`type```)``. A +:n:`({+ @ident} : @type)`. A binder can also be any pattern prefixed by a quote, e.g. :g:`'(x,y)`. Some constructions allow the binding of a variable to value. This is called a “let-binder”. The entry :token:`binder` of the grammar accepts either an assumption binder as defined above or a let-binder. The notation in -the latter case is ``(ident := term)``. In a let-binder, only one +the latter case is :n:`(@ident := @term)`. In a let-binder, only one variable can be introduced at the same time. It is also possible to give the type of the variable as follows: -``(ident : term := term)``. +:n:`(@ident : @type := @term)`. Lists of :token:`binder` are allowed. In the case of :g:`fun` and :g:`forall`, it is intended that at least one binder of the list is an assumption otherwise @@ -263,7 +264,7 @@ the case of a single sequence of bindings sharing the same type (e.g.: Abstractions ------------ -The expression ``fun ident : type => term`` defines the +The expression :n:`fun @ident : @type => @term` defines the *abstraction* of the variable :token:`ident`, of type :token:`type`, over the term :token:`term`. It denotes a function of the variable :token:`ident` that evaluates to the expression :token:`term` (e.g. :g:`fun x : A => x` denotes the identity @@ -283,7 +284,7 @@ Section :ref:`let-in`). Products -------- -The expression :g:`forall ident : type, term` denotes the +The expression :n:`forall @ident : @type, @term` denotes the *product* of the variable :token:`ident` of type :token:`type`, over the term :token:`term`. As for abstractions, :g:`forall` is followed by a binder list, and products over several variables are equivalent to an iteration of one-variable @@ -314,17 +315,17 @@ The expression :token:`term`\ :math:`_0` :token:`term`\ :math:`_1` ... :token:`term`\ :math:`_1` ) … ) :token:`term`\ :math:`_n` : associativity is to the left. -The notation ``(ident := term)`` for arguments is used for making +The notation :n:`(@ident := @term)` for arguments is used for making explicit the value of implicit arguments (see Section :ref:`explicit-applications`). Type cast --------- -The expression ``term : type`` is a type cast expression. It enforces +The expression :n:`@term : @type` is a type cast expression. It enforces the type of :token:`term` to be :token:`type`. -``term <: type`` locally sets up the virtual machine for checking that +:n:`@term <: @type` locally sets up the virtual machine for checking that :token:`term` has type :token:`type`. Inferable subterms @@ -339,20 +340,18 @@ guess the missing piece of information. Let-in definitions ------------------ -``let`` :token:`ident` := :token:`term`:math:`_1` in :token:`term`:math:`_2` -denotes the local binding of :token:`term`:math:`_1` to the variable -:token:`ident` in :token:`term`:math:`_2`. There is a syntactic sugar for let-in -definition of functions: ``let`` :token:`ident` :token:`binder`:math:`_1` … -:token:`binder`:math:`_n` := :token:`term`:math:`_1` in :token:`term`:math:`_2` -stands for ``let`` :token:`ident` := ``fun`` :token:`binder`:math:`_1` … -:token:`binder`:math:`_n` => :token:`term`:math:`_1` in :token:`term`:math:`_2`. +:n:`let @ident := @term in @term’` +denotes the local binding of :token:`term` to the variable +:token:`ident` in :token:`term`’. There is a syntactic sugar for let-in +definition of functions: :n:`let @ident {+ @binder} := @term in @term’` +stands for :n:`let @ident := fun {+ @binder} => @term in @term’`. Definition by case analysis --------------------------- Objects of inductive types can be destructurated by a case-analysis construction called *pattern-matching* expression. A pattern-matching -expression is used to analyze the structure of an inductive objects and +expression is used to analyze the structure of an inductive object and to apply specific treatments accordingly. This paragraph describes the basic form of pattern-matching. See @@ -360,14 +359,14 @@ Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the des of the general form. The basic form of pattern-matching is characterized by a single :token:`match_item` expression, a :token:`mult_pattern` restricted to a single :token:`pattern` and :token:`pattern` restricted to the form -:token:`qualid` :token:`ident`. +:n:`@qualid {* @ident}`. -The expression match :token:`term`:math:`_0` :token:`return_type` with +The expression match ":token:`term`:math:`_0` :token:`return_type` with :token:`pattern`:math:`_1` => :token:`term`:math:`_1` :math:`|` … :math:`|` -:token:`pattern`:math:`_n` => :token:`term`:math:`_n` end, denotes a -:token:`pattern-matching` over the term :token:`term`:math:`_0` (expected to be +:token:`pattern`:math:`_n` => :token:`term`:math:`_n` end" denotes a +*pattern-matching* over the term :token:`term`:math:`_0` (expected to be of an inductive type :math:`I`). The terms :token:`term`:math:`_1`\ …\ -:token:`term`:math:`_n` are the :token:`branches` of the pattern-matching +:token:`term`:math:`_n` are the *branches* of the pattern-matching expression. Each of :token:`pattern`:math:`_i` has a form :token:`qualid` :token:`ident` where :token:`qualid` must denote a constructor. There should be exactly one branch for every constructor of :math:`I`. @@ -395,40 +394,39 @@ is dependent in the return type. For instance, in the following example: Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := match b as x return or (eq bool x true) (eq bool x false) with - | true => or_introl (eq bool true true) (eq bool true false) - (eq_refl bool true) - | false => or_intror (eq bool false true) (eq bool false false) - (eq_refl bool false) + | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true) + | false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false) end. -the branches have respective types or :g:`eq bool true true :g:`eq bool true -false` and or :g:`eq bool false true` :g:`eq bool false false` while the whole -pattern-matching expression has type or :g:`eq bool b true` :g:`eq bool b -false`, the identifier :g:`x` being used to represent the dependency. Remark -that when the term being matched is a variable, the as clause can be -omitted and the term being matched can serve itself as binding name in -the return type. For instance, the following alternative definition is -accepted and has the same meaning as the previous one. +the branches have respective types ":g:`or (eq bool true true) (eq bool true false)`" +and ":g:`or (eq bool false true) (eq bool false false)`" while the whole +pattern-matching expression has type ":g:`or (eq bool b true) (eq bool b false)`", +the identifier :g:`b` being used to represent the dependency. -.. coqtop:: in +.. note:: - Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := - match b return or (eq bool b true) (eq bool b false) with - | true => or_introl (eq bool true true) (eq bool true false) - (eq_refl bool true) - | false => or_intror (eq bool false true) (eq bool false false) - (eq_refl bool false) - end. + When the term being matched is a variable, the ``as`` clause can be + omitted and the term being matched can serve itself as binding name in + the return type. For instance, the following alternative definition is + accepted and has the same meaning as the previous one. + + .. coqtop:: in + + Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := + match b return or (eq bool b true) (eq bool b false) with + | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true) + | false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false) + end. The second subcase is only relevant for annotated inductive types such -as the equality predicate (see Section :ref:`Equality`), +as the equality predicate (see Section :ref:`coq-equality`), the order predicate on natural numbers or the type of lists of a given length (see Section :ref:`matching-dependent`). In this configuration, the type of each branch can depend on the type dependencies specific to the branch and the whole pattern-matching expression has a type determined by the specific dependencies in the type of the term being matched. This dependency of the return type in the annotations of the inductive type -is expressed using a “in I _ ... _ :token:`pattern`:math:`_1` ... +is expressed using a “:g:`in` :math:`I` :g:`_ … _` :token:`pattern`:math:`_1` … :token:`pattern`:math:`_n`” clause, where - :math:`I` is the inductive type of the term being matched; @@ -452,44 +450,43 @@ For instance, in the following example: | eq_refl _ => eq_refl A x end. -the type of the branch has type :g:`eq A x x` because the third argument of -g:`eq` is g:`x` in the type of the pattern :g:`refl_equal`. On the contrary, the +the type of the branch is :g:`eq A x x` because the third argument of +:g:`eq` is :g:`x` in the type of the pattern :g:`eq_refl`. On the contrary, the type of the whole pattern-matching expression has type :g:`eq A y x` because the third argument of eq is y in the type of H. This dependency of the case analysis -in the third argument of :g:`eq` is expressed by the identifier g:`z` in the +in the third argument of :g:`eq` is expressed by the identifier :g:`z` in the return type. Finally, the third subcase is a combination of the first and second subcase. In particular, it only applies to pattern-matching on terms in -a type with annotations. For this third subcase, both the clauses as and -in are available. +a type with annotations. For this third subcase, both the clauses ``as`` and +``in`` are available. There are specific notations for case analysis on types with one or two -constructors: “if … then … else …” and “let (…, ” (see -Sections :ref:`if-then-else` and :ref:`let-in`). +constructors: ``if … then … else …`` and ``let (…,…) := … in …`` (see +Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`). Recursive functions ------------------- -The expression “fix :token:`ident`:math:`_1` :token:`binder`:math:`_1` : -:token:`type`:math:`_1` ``:=`` :token:`term`:math:`_1` with … with +The expression “``fix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``:`` +:token:`type`:math:`_1` ``:=`` :token:`term`:math:`_1` ``with … with`` :token:`ident`:math:`_n` :token:`binder`:math:`_n` : :token:`type`:math:`_n` -``:=`` :token:`term`:math:`_n` for :token:`ident`:math:`_i`” denotes the -:math:`i`\ component of a block of functions defined by mutual well-founded +``:=`` :token:`term`:math:`_n` ``for`` :token:`ident`:math:`_i`” denotes the +:math:`i`-th component of a block of functions defined by mutual structural recursion. It is the local counterpart of the :cmd:`Fixpoint` command. When -:math:`n=1`, the “for :token:`ident`:math:`_i`” clause is omitted. +:math:`n=1`, the “``for`` :token:`ident`:math:`_i`” clause is omitted. -The expression “cofix :token:`ident`:math:`_1` :token:`binder`:math:`_1` : -:token:`type`:math:`_1` with … with :token:`ident`:math:`_n` :token:`binder`:math:`_n` -: :token:`type`:math:`_n` for :token:`ident`:math:`_i`” denotes the -:math:`i`\ component of a block of terms defined by a mutual guarded -co-recursion. It is the local counterpart of the ``CoFixpoint`` command. See -Section :ref:`CoFixpoint` for more details. When -:math:`n=1`, the “ for :token:`ident`:math:`_i`” clause is omitted. +The expression “``cofix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``:`` +:token:`type`:math:`_1` ``with … with`` :token:`ident`:math:`_n` :token:`binder`:math:`_n` +: :token:`type`:math:`_n` ``for`` :token:`ident`:math:`_i`” denotes the +:math:`i`-th component of a block of terms defined by a mutual guarded +co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When +:math:`n=1`, the “``for`` :token:`ident`:math:`_i`” clause is omitted. The association of a single fixpoint and a local definition have a special -syntax: “let fix f … := … in …” stands for “let f := fix f … := … in …”. The -same applies for co-fixpoints. +syntax: :n:`let fix @ident @binders := @term in` stands for +:n:`let @ident := fix @ident @binders := @term in`. The same applies for co-fixpoints. .. _vernacular: @@ -527,6 +524,9 @@ The Vernacular : | Proof . … Admitted . .. todo:: This use of … in this grammar is inconsistent + What about removing the proof part of this grammar from this chapter + and putting it somewhere where top-level tactics can be described as well? + See also #7583. This grammar describes *The Vernacular* which is the language of commands of Gallina. A sentence of the vernacular language, like in @@ -551,77 +551,74 @@ has type :token:`type`. .. _Axiom: -.. cmd:: Axiom @ident : @term +.. cmd:: Parameter @ident : @type - This command links :token:`term` to the name :token:`ident` as its specification in - the global context. The fact asserted by :token:`term` is thus assumed as a + This command links :token:`type` to the name :token:`ident` as its specification in + the global context. The fact asserted by :token:`type` is thus assumed as a postulate. -.. exn:: @ident already exists. - :name: @ident already exists. (Axiom) - -.. cmdv:: Parameter @ident : @term - :name: Parameter - - Is equivalent to ``Axiom`` :token:`ident` : :token:`term` - -.. cmdv:: Parameter {+ @ident } : @term - - Adds parameters with specification :token:`term` - -.. cmdv:: Parameter {+ ( {+ @ident } : @term ) } - - Adds blocks of parameters with different specifications. + .. exn:: @ident already exists. + :name: @ident already exists. (Axiom) + :undocumented: -.. cmdv:: Parameters {+ ( {+ @ident } : @term ) } + .. cmdv:: Parameter {+ @ident } : @type - Synonym of ``Parameter``. + Adds several parameters with specification :token:`type`. -.. cmdv:: Local Axiom @ident : @term + .. cmdv:: Parameter {+ ( {+ @ident } : @type ) } - Such axioms 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. + Adds blocks of parameters with different specifications. -.. cmdv:: Conjecture @ident : @term - :name: Conjecture + .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) } + :name: Local Parameter - Is equivalent to ``Axiom`` :token:`ident` : :token:`term`. + 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. -.. cmd:: Variable @ident : @term + .. 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 -This command links :token:`term` to the name :token:`ident` in the context of -the current section (see Section :ref:`section-mechanism` for a description of -the section mechanism). When the current section is closed, name :token:`ident` -will be unknown and every object using this variable will be explicitly -parametrized (the variable is *discharged*). Using the ``Variable`` command out -of any section is equivalent to using ``Local Parameter``. + These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. -.. exn:: @ident already exists. - :name: @ident already exists. (Variable) +.. cmd:: Variable @ident : @type -.. cmdv:: Variable {+ @ident } : @term + This command links :token:`type` to the name :token:`ident` in the context of + the current section (see Section :ref:`section-mechanism` for a description of + the section mechanism). When the current section is closed, name :token:`ident` + will be unknown and every object using this variable will be explicitly + parametrized (the variable is *discharged*). Using the :cmd:`Variable` command out + of any section is equivalent to using :cmd:`Local Parameter`. - Links :token:`term` to each :token:`ident`. + .. exn:: @ident already exists. + :name: @ident already exists. (Variable) + :undocumented: -.. cmdv:: Variable {+ ( {+ @ident } : @term) } + .. cmdv:: Variable {+ @ident } : @term - Adds blocks of variables with different specifications. + Links :token:`type` to each :token:`ident`. -.. cmdv:: Variables {+ ( {+ @ident } : @term) } - :name: Variables + .. cmdv:: Variable {+ ( {+ @ident } : @term ) } -.. cmdv:: Hypothesis {+ ( {+ @ident } : @term) } - :name: Hypothesis + Adds blocks of variables with different specifications. -.. cmdv:: Hypotheses {+ ( {+ @ident } : @term) } + .. cmdv:: Variables {+ ( {+ @ident } : @term) } + Hypothesis {+ ( {+ @ident } : @term) } + Hypotheses {+ ( {+ @ident } : @term) } + :name: Variables; Hypothesis; Hypotheses -Synonyms of ``Variable``. + These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @term) }`. -It is advised to use the keywords ``Axiom`` and ``Hypothesis`` for -logical postulates (i.e. when the assertion *term* is of sort ``Prop``), -and to use the keywords ``Parameter`` and ``Variable`` in other cases -(corresponding to the declaration of an abstract mathematical entity). +.. note:: + It is advised to use the commands :cmd:`Axiom`, :cmd:`Conjecture` and + :cmd:`Hypothesis` (and their plural forms) for logical postulates (i.e. when + the assertion :token:`type` is of sort :g:`Prop`), and to use the commands + :cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases + (corresponding to the declaration of an abstract mathematical entity). .. _gallina-definitions: @@ -649,63 +646,65 @@ Section :ref:`typing-rules`. This command binds :token:`term` to the name :token:`ident` in the environment, provided that :token:`term` is well-typed. -.. exn:: @ident already exists. - :name: @ident already exists. (Definition) - -.. cmdv:: Definition @ident : @term := @term - - It checks that the type of :token:`term`:math:`_2` is definitionally equal to - :token:`term`:math:`_1`, and registers :token:`ident` as being of type - :token:`term`:math:`_1`, and bound to value :token:`term`:math:`_2`. - + .. exn:: @ident already exists. + :name: @ident already exists. (Definition) + :undocumented: -.. cmdv:: Definition @ident {* @binder } : @term := @term + .. cmdv:: Definition @ident : @type := @term - This is equivalent to ``Definition`` :token:`ident` : :g:`forall` - :token:`binder`:math:`_1` … :token:`binder`:math:`_n`, :token:`term`:math:`_1` := - fun :token:`binder`:math:`_1` … - :token:`binder`:math:`_n` => :token:`term`:math:`_2`. + This variant checks that the type of :token:`term` is definitionally equal to + :token:`type`, and registers :token:`ident` as being of type + :token:`type`, and bound to value :token:`term`. -.. cmdv:: Local Definition @ident := @term + .. exn:: The term @term has type @type while it is expected to have type @type'. + :undocumented: - Such definitions 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:: Definition @ident @binders {? : @term } := @term -.. cmdv:: Example @ident := @term - :name: Example + This is equivalent to + :n:`Definition @ident : forall @binders, @term := fun @binders => @term`. -.. cmdv:: Example @ident : @term := @term + .. cmdv:: Local Definition @ident {? @binders } {? : @type } := @term + :name: Local Definition -.. cmdv:: Example @ident {* @binder } : @term := @term + Such definitions 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. -These are synonyms of the Definition forms. + .. cmdv:: {? Local } Example @ident {? @binders } {? : @type } := @term + :name: Example -.. exn:: The term @term has type @type while it is expected to have type @type. + This is equivalent to :cmd:`Definition`. -See also :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. +.. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. .. cmd:: Let @ident := @term -This command binds the value :token:`term` to the name :token:`ident` in the -environment of the current section. The name :token:`ident` disappears when the -current section is eventually closed, and, all persistent objects (such -as theorems) defined within the section and depending on :token:`ident` are -prefixed by the let-in definition ``let`` :token:`ident` ``:=`` :token:`term` -``in``. Using the ``Let`` command out of any section is equivalent to using -``Local Definition``. + This command binds the value :token:`term` to the name :token:`ident` in the + environment of the current section. The name :token:`ident` disappears when the + current section is eventually closed, and all persistent objects (such + as theorems) defined within the section and depending on :token:`ident` are + prefixed by the let-in definition :n:`let @ident := @term in`. + Using the :cmd:`Let` command out of any section is equivalent to using + :cmd:`Local Definition`. -.. exn:: @ident already exists. - :name: @ident already exists. (Let) + .. exn:: @ident already exists. + :name: @ident already exists. (Let) + :undocumented: -.. cmdv:: Let @ident : @term := @term + .. cmdv:: Let @ident {? @binders } {? : @type } := @term + :undocumented: -.. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body} + .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body} + :name: Let Fixpoint + :undocumented: -.. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body} + .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body} + :name: Let CoFixpoint + :undocumented: -See also Sections :ref:`section-mechanism`, commands :cmd:`Opaque`, -:cmd:`Transparent`, and tactic :tacn:`unfold`. +.. seealso:: Section :ref:`section-mechanism`, commands :cmd:`Opaque`, + :cmd:`Transparent`, and tactic :tacn:`unfold`. .. _gallina-inductive-definitions: @@ -719,63 +718,80 @@ explain also co-inductive types. Simple inductive types ~~~~~~~~~~~~~~~~~~~~~~ -The definition of a simple inductive type has the following form: +.. cmd:: Inductive @ident : {? @sort } := {? | } @ident : @type {* | @ident : @type } -.. cmd:: Inductive @ident : @sort := {? | } @ident : @type {* | @ident : @type } + This command defines a simple inductive type and its constructors. + The first :token:`ident` is the name of the inductively defined type + and :token:`sort` is the universe where it lives. The next :token:`ident`\s + are the names of its constructors and :token:`type` their respective types. + Depending on the universe where the inductive type :token:`ident` lives + (e.g. its type :token:`sort`), Coq provides a number of destructors. + Destructors are named :token:`ident`\ ``_ind``, :token:`ident`\ ``_rec`` + or :token:`ident`\ ``_rect`` which respectively correspond to elimination + principles on :g:`Prop`, :g:`Set` and :g:`Type`. + The type of the destructors expresses structural induction/recursion + principles over objects of type :token:`ident`. + The constant :token:`ident`\ ``_ind`` is always provided, + whereas :token:`ident`\ ``_rec`` and :token:`ident`\ ``_rect`` can be + impossible to derive (for example, when :token:`ident` is a proposition). -The name :token:`ident` is the name of the inductively defined type and -:token:`sort` is the universes where it lives. The :token:`ident` are the names -of its constructors and :token:`type` their respective types. The types of the -constructors have to satisfy a *positivity condition* (see Section -:ref:`positivity`) for :token:`ident`. This condition ensures the soundness of -the inductive definition. If this is the case, the :token:`ident` are added to -the environment with their respective types. Accordingly to the universe where -the inductive type lives (e.g. its type :token:`sort`), Coq provides a number of -destructors for :token:`ident`. Destructors are named ``ident_ind``, -``ident_rec`` or ``ident_rect`` which respectively correspond to -elimination principles on :g:`Prop`, :g:`Set` and :g:`Type`. The type of the -destructors expresses structural induction/recursion principles over objects of -:token:`ident`. We give below two examples of the use of the Inductive -definitions. + .. exn:: Non strictly positive occurrence of @ident in @type. -The set of natural numbers is defined as: + The types of the constructors have to satisfy a *positivity condition* + (see Section :ref:`positivity`). This condition ensures the soundness of + the inductive definition. -.. coqtop:: all + .. exn:: The conclusion of @type is not valid; it must be built from @ident. - Inductive nat : Set := - | O : nat - | S : nat -> nat. + The conclusion of the type of the constructors must be the inductive type + :token:`ident` being defined (or :token:`ident` applied to arguments in + the case of annotated inductive types — cf. next section). -The type nat is defined as the least :g:`Set` containing :g:`O` and closed by -the :g:`S` constructor. The names :g:`nat`, :g:`O` and :g:`S` are added to the -environment. + .. example:: + The set of natural numbers is defined as: -Now let us have a look at the elimination principles. They are three of them: -:g:`nat_ind`, :g:`nat_rec` and :g:`nat_rect`. The type of :g:`nat_ind` is: + .. coqtop:: all -.. coqtop:: all + Inductive nat : Set := + | O : nat + | S : nat -> nat. - Check nat_ind. + The type nat is defined as the least :g:`Set` containing :g:`O` and closed by + the :g:`S` constructor. The names :g:`nat`, :g:`O` and :g:`S` are added to the + environment. -This is the well known structural induction principle over natural -numbers, i.e. the second-order form of Peano’s induction principle. It -allows proving some universal property of natural numbers (:g:`forall -n:nat, P n`) by induction on :g:`n`. + Now let us have a look at the elimination principles. They are three of them: + :g:`nat_ind`, :g:`nat_rec` and :g:`nat_rect`. The type of :g:`nat_ind` is: -The types of :g:`nat_rec` and :g:`nat_rect` are similar, except that they pertain -to :g:`(P:nat->Set)` and :g:`(P:nat->Type)` respectively. They correspond to -primitive induction principles (allowing dependent types) respectively -over sorts ``Set`` and ``Type``. The constant ``ident_ind`` is always -provided, whereas ``ident_rec`` and ``ident_rect`` can be impossible -to derive (for example, when :token:`ident` is a proposition). + .. coqtop:: all -.. coqtop:: in + Check nat_ind. + + This is the well known structural induction principle over natural + numbers, i.e. the second-order form of Peano’s induction principle. It + allows proving some universal property of natural numbers (:g:`forall + n:nat, P n`) by induction on :g:`n`. + + The types of :g:`nat_rec` and :g:`nat_rect` are similar, except that they pertain + to :g:`(P:nat->Set)` and :g:`(P:nat->Type)` respectively. They correspond to + primitive induction principles (allowing dependent types) respectively + over sorts ``Set`` and ``Type``. + + .. cmdv:: Inductive @ident {? : @sort } := {? | } {*| @ident {? @binders } {? : @type } } + + Constructors :token:`ident`\s can come with :token:`binders` in which case, + the actual type of the constructor is :n:`forall @binders, @type`. + + In the case where inductive types have no annotations (next section + gives an example of such annotations), a constructor can be defined + by only giving the type of its arguments. + + .. example:: - Inductive nat : Set := O | S (_:nat). + .. coqtop:: in + + Inductive nat : Set := O | S (_:nat). -In the case where inductive types have no annotations (next section -gives an example of such annotations), a constructor can be defined -by only giving the type of its arguments. Simple annotated inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -784,203 +800,195 @@ In an annotated inductive types, the universe where the inductive type is defined is no longer a simple sort, but what is called an arity, which is a type whose conclusion is a sort. -As an example of annotated inductive types, let us define the -:g:`even` predicate: - -.. coqtop:: all +.. example:: - Inductive even : nat -> Prop := - | even_0 : even O - | even_SS : forall n:nat, even n -> even (S (S n)). + As an example of annotated inductive types, let us define the + :g:`even` predicate: -The type :g:`nat->Prop` means that even is a unary predicate (inductively -defined) over natural numbers. The type of its two constructors are the -defining clauses of the predicate even. The type of :g:`even_ind` is: + .. coqtop:: all -.. coqtop:: all + Inductive even : nat -> Prop := + | even_0 : even O + | even_SS : forall n:nat, even n -> even (S (S n)). - Check even_ind. + The type :g:`nat->Prop` means that even is a unary predicate (inductively + defined) over natural numbers. The type of its two constructors are the + defining clauses of the predicate even. The type of :g:`even_ind` is: -From a mathematical point of view it asserts that the natural numbers satisfying -the predicate even are exactly in the smallest set of naturals satisfying the -clauses :g:`even_0` or :g:`even_SS`. This is why, when we want to prove any -predicate :g:`P` over elements of :g:`even`, it is enough to prove it for :g:`O` -and to prove that if any natural number :g:`n` satisfies :g:`P` its double -successor :g:`(S (S n))` satisfies also :g:`P`. This is indeed analogous to the -structural induction principle we got for :g:`nat`. + .. coqtop:: all -.. exn:: Non strictly positive occurrence of @ident in @type. + Check even_ind. -.. exn:: The conclusion of @type is not valid; it must be built from @ident. + From a mathematical point of view it asserts that the natural numbers satisfying + the predicate even are exactly in the smallest set of naturals satisfying the + clauses :g:`even_0` or :g:`even_SS`. This is why, when we want to prove any + predicate :g:`P` over elements of :g:`even`, it is enough to prove it for :g:`O` + and to prove that if any natural number :g:`n` satisfies :g:`P` its double + successor :g:`(S (S n))` satisfies also :g:`P`. This is indeed analogous to the + structural induction principle we got for :g:`nat`. Parametrized inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In the previous example, each constructor introduces a different -instance of the predicate even. In some cases, all the constructors -introduces the same generic instance of the inductive definition, in -which case, instead of an annotation, we use a context of parameters -which are binders shared by all the constructors of the definition. +.. cmdv:: Inductive @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type} -The general scheme is: + In the previous example, each constructor introduces a different + instance of the predicate :g:`even`. In some cases, all the constructors + introduce the same generic instance of the inductive definition, in + which case, instead of an annotation, we use a context of parameters + which are :token:`binders` shared by all the constructors of the definition. -.. cmdv:: Inductive @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type} - -Parameters differ from inductive type annotations in the fact that the -conclusion of each type of constructor :g:`term` invoke the inductive type with -the same values of parameters as its specification. - -A typical example is the definition of polymorphic lists: - -.. coqtop:: in + Parameters differ from inductive type annotations in the fact that the + conclusion of each type of constructor invoke the inductive type with + the same values of parameters as its specification. - Inductive list (A:Set) : Set := - | nil : list A - | cons : A -> list A -> list A. + .. example:: -.. note:: + A typical example is the definition of polymorphic lists: - In the type of :g:`nil` and :g:`cons`, we write :g:`(list A)` and not - just :g:`list`. The constructors :g:`nil` and :g:`cons` will have respectively - types: + .. coqtop:: in - .. coqtop:: all + Inductive list (A:Set) : Set := + | nil : list A + | cons : A -> list A -> list A. - Check nil. - Check cons. + In the type of :g:`nil` and :g:`cons`, we write :g:`(list A)` and not + just :g:`list`. The constructors :g:`nil` and :g:`cons` will have respectively + types: - Types of destructors are also quantified with :g:`(A:Set)`. + .. coqtop:: all -Variants -++++++++ + Check nil. + Check cons. -.. coqtop:: in + Types of destructors are also quantified with :g:`(A:Set)`. - Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A). + Once again, it is possible to specify only the type of the arguments + of the constructors, and to omit the type of the conclusion: -This is an alternative definition of lists where we specify the -arguments of the constructors rather than their full type. + .. coqtop:: in -.. coqtop:: in + Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A). - Variant sum (A B:Set) : Set := left : A -> sum A B | right : B -> sum A B. +.. note:: + + It is possible in the type of a constructor, to + invoke recursively the inductive definition on an argument which is not + the parameter itself. -The ``Variant`` keyword is identical to the ``Inductive`` keyword, except -that it disallows recursive definition of types (in particular lists cannot -be defined with the Variant keyword). No induction scheme is generated for -this variant, unless :opt:`Nonrecursive Elimination Schemes` is set. + One can define : -.. exn:: The @num th argument of @ident must be @ident in @type. + .. coqtop:: all -New from Coq V8.1 -+++++++++++++++++ + Inductive list2 (A:Set) : Set := + | nil2 : list2 A + | cons2 : A -> list2 (A*A) -> list2 A. -The condition on parameters for inductive definitions has been relaxed -since Coq V8.1. It is now possible in the type of a constructor, to -invoke recursively the inductive definition on an argument which is not -the parameter itself. + that can also be written by specifying only the type of the arguments: -One can define : + .. coqtop:: all reset -.. coqtop:: all + Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)). - Inductive list2 (A:Set) : Set := - | nil2 : list2 A - | cons2 : A -> list2 (A*A) -> list2 A. + But the following definition will give an error: -that can also be written by specifying only the type of the arguments: + .. coqtop:: all -.. coqtop:: all reset + Fail Inductive listw (A:Set) : Set := + | nilw : listw (A*A) + | consw : A -> listw (A*A) -> listw (A*A). - Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)). + because the conclusion of the type of constructors should be :g:`listw A` + in both cases. -But the following definition will give an error: + + A parametrized inductive definition can be defined using annotations + instead of parameters but it will sometimes give a different (bigger) + sort for the inductive definition and will produce a less convenient + rule for case elimination. -.. coqtop:: all +.. seealso:: + Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. - Fail Inductive listw (A:Set) : Set := - | nilw : listw (A*A) - | consw : A -> listw (A*A) -> listw (A*A). +Variants +~~~~~~~~ -Because the conclusion of the type of constructors should be :g:`listw A` in -both cases. +.. cmd:: Variant @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type} -A parametrized inductive definition can be defined using annotations -instead of parameters but it will sometimes give a different (bigger) -sort for the inductive definition and will produce a less convenient -rule for case elimination. + The :cmd:`Variant` command is identical to the :cmd:`Inductive` command, except + that it disallows recursive definition of types (for instance, lists cannot + be defined using :cmd:`Variant`). No induction scheme is generated for + this variant, unless option :opt:`Nonrecursive Elimination Schemes` is on. -See also Section :ref:`inductive-definitions` and the :tacn:`induction` -tactic. + .. exn:: The @num th argument of @ident must be @ident in @type. + :undocumented: Mutually defined inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The definition of a block of mutually inductive types has the form: +.. cmdv:: Inductive @ident {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident {? : @type } } } -.. cmdv:: Inductive @ident : @term := {? | } @ident : @type {* | @ident : @type } {* with @ident : @term := {? | } @ident : @type {* | @ident : @type }} + This variant allows defining a block of mutually inductive types. + It has the same semantics as the above :cmd:`Inductive` definition for each + :token:`ident`. All :token:`ident` are simultaneously added to the environment. + Then well-typing of constructors can be checked. Each one of the :token:`ident` + can be used on its own. -It has the same semantics as the above ``Inductive`` definition for each -:token:`ident` All :token:`ident` are simultaneously added to the environment. -Then well-typing of constructors can be checked. Each one of the :token:`ident` -can be used on its own. + .. cmdv:: Inductive @ident @binders {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident @binders {? : @type } } } -It is also possible to parametrize these inductive definitions. However, -parameters correspond to a local context in which the whole set of -inductive declarations is done. For this reason, the parameters must be -strictly the same for each inductive types The extended syntax is: + In this variant, the inductive definitions are parametrized + with :token:`binders`. However, parameters correspond to a local context + in which the whole set of inductive declarations is done. For this + reason, the parameters must be strictly the same for each inductive types. -.. cmdv:: Inductive @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type } {* with @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type }} - -The typical example of a mutual inductive data type is the one for trees and -forests. We assume given two types :g:`A` and :g:`B` as variables. It can -be declared the following way. +.. example:: + The typical example of a mutual inductive data type is the one for trees and + forests. We assume given two types :g:`A` and :g:`B` as variables. It can + be declared the following way. -.. coqtop:: in + .. coqtop:: in - Variables A B : Set. + Variables A B : Set. - Inductive tree : Set := - node : A -> forest -> tree + Inductive tree : Set := node : A -> forest -> tree - with forest : Set := - | leaf : B -> forest - | cons : tree -> forest -> forest. + with forest : Set := + | leaf : B -> forest + | cons : tree -> forest -> forest. -This declaration generates automatically six induction principles. They are -respectively called :g:`tree_rec`, :g:`tree_ind`, :g:`tree_rect`, -:g:`forest_rec`, :g:`forest_ind`, :g:`forest_rect`. These ones are not the most -general ones but are just the induction principles corresponding to each -inductive part seen as a single inductive definition. + This declaration generates automatically six induction principles. They are + respectively called :g:`tree_rec`, :g:`tree_ind`, :g:`tree_rect`, + :g:`forest_rec`, :g:`forest_ind`, :g:`forest_rect`. These ones are not the most + general ones but are just the induction principles corresponding to each + inductive part seen as a single inductive definition. -To illustrate this point on our example, we give the types of :g:`tree_rec` -and :g:`forest_rec`. + To illustrate this point on our example, we give the types of :g:`tree_rec` + and :g:`forest_rec`. -.. coqtop:: all + .. coqtop:: all - Check tree_rec. + Check tree_rec. - Check forest_rec. + Check forest_rec. -Assume we want to parametrize our mutual inductive definitions with the -two type variables :g:`A` and :g:`B`, the declaration should be -done the following way: + Assume we want to parametrize our mutual inductive definitions with the + two type variables :g:`A` and :g:`B`, the declaration should be + done the following way: -.. coqtop:: in + .. coqtop:: in - Inductive tree (A B:Set) : Set := - node : A -> forest A B -> tree A B + Inductive tree (A B:Set) : Set := node : A -> forest A B -> tree A B - with forest (A B:Set) : Set := - | leaf : B -> forest A B - | cons : tree A B -> forest A B -> forest A B. + with forest (A B:Set) : Set := + | leaf : B -> forest A B + | cons : tree A B -> forest A B -> forest A B. -Assume we define an inductive definition inside a section. When the -section is closed, the variables declared in the section and occurring -free in the declaration are added as parameters to the inductive -definition. + Assume we define an inductive definition inside a section + (cf. :ref:`section-mechanism`). When the section is closed, the variables + declared in the section and occurring free in the declaration are added as + parameters to the inductive definition. -See also Section :ref:`section-mechanism`. +.. seealso:: + A generic command :cmd:`Scheme` is useful to build automatically various + mutual induction principles. .. _coinductive-types: @@ -995,41 +1003,47 @@ constructors. Infinite objects are introduced by a non-ending (but effective) process of construction, defined in terms of the constructors of the type. -An example of a co-inductive type is the type of infinite sequences of -natural numbers, usually called streams. It can be introduced in -Coq using the ``CoInductive`` command: +.. cmd:: CoInductive @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type} -.. coqtop:: all + This command introduces a co-inductive type. + The syntax of the command is the same as the command :cmd:`Inductive`. + No principle of induction is derived from the definition of a co-inductive + type, since such principles only make sense for inductive types. + For co-inductive types, the only elimination principle is case analysis. + +.. example:: + An example of a co-inductive type is the type of infinite sequences of + natural numbers, usually called streams. - CoInductive Stream : Set := - Seq : nat -> Stream -> Stream. + .. coqtop:: in -The syntax of this command is the same as the command :cmd:`Inductive`. Notice -that no principle of induction is derived from the definition of a co-inductive -type, since such principles only make sense for inductive ones. For co-inductive -ones, the only elimination principle is case analysis. For example, the usual -destructors on streams :g:`hd:Stream->nat` and :g:`tl:Str->Str` can be defined -as follows: + CoInductive Stream : Set := Seq : nat -> Stream -> Stream. -.. coqtop:: all + The usual destructors on streams :g:`hd:Stream->nat` and :g:`tl:Str->Str` + can be defined as follows: - Definition hd (x:Stream) := let (a,s) := x in a. - Definition tl (x:Stream) := let (a,s) := x in s. + .. coqtop:: in + + Definition hd (x:Stream) := let (a,s) := x in a. + Definition tl (x:Stream) := let (a,s) := x in s. Definition of co-inductive predicates and blocks of mutually -co-inductive definitions are also allowed. An example of a co-inductive -predicate is the extensional equality on streams: +co-inductive definitions are also allowed. + +.. example:: + An example of a co-inductive predicate is the extensional equality on + streams: -.. coqtop:: all + .. coqtop:: in - CoInductive EqSt : Stream -> Stream -> Prop := - eqst : forall s1 s2:Stream, - hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2. + CoInductive EqSt : Stream -> Stream -> Prop := + eqst : forall s1 s2:Stream, + hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2. -In order to prove the extensionally equality of two streams :g:`s1` and :g:`s2` -we have to construct an infinite proof of equality, that is, an infinite object -of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite objects in -Section :ref:`cofixpoint`. + In order to prove the extensional equality of two streams :g:`s1` and :g:`s2` + we have to construct an infinite proof of equality, that is, an infinite + object of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite + objects in Section :ref:`cofixpoint`. Definition of recursive functions --------------------------------- @@ -1043,197 +1057,178 @@ constructions. .. _Fixpoint: -.. cmd:: Fixpoint @ident @params {struct @ident} : @type := @term - -This command allows defining functions by pattern-matching over inductive objects -using a fixed point construction. The meaning of this declaration is to -define :token:`ident` a recursive function with arguments specified by the -binders in :token:`params` such that :token:`ident` applied to arguments corresponding -to these binders has type :token:`type`:math:`_0`, and is equivalent to the -expression :token:`term`:math:`_0`. The type of the :token:`ident` is consequently -:g:`forall` :token:`params`, :token:`type`:math:`_0` and the value is equivalent to -:g:`fun` :token:`params` :g:`=>` :token:`term`:math:`_0`. - -To be accepted, a ``Fixpoint`` definition has to satisfy some syntactical -constraints on a special argument called the decreasing argument. They -are needed to ensure that the Fixpoint definition always terminates. The -point of the {struct :token:`ident`} annotation is to let the user tell the -system which argument decreases along the recursive calls. For instance, -one can define the addition function as : - -.. coqtop:: all - - Fixpoint add (n m:nat) {struct n} : nat := - match n with - | O => m - | S p => S (add p m) - end. +.. cmd:: Fixpoint @ident @binders {? {struct @ident} } {? : @type } := @term -The ``{struct`` :token:`ident```}`` annotation may be left implicit, in this case the -system try successively arguments from left to right until it finds one that -satisfies the decreasing condition. + This command allows defining functions by pattern-matching over inductive + objects using a fixed point construction. The meaning of this declaration is + to define :token:`ident` a recursive function with arguments specified by + the :token:`binders` such that :token:`ident` applied to arguments + corresponding to these :token:`binders` has type :token:`type`, and is + equivalent to the expression :token:`term`. The type of :token:`ident` is + consequently :n:`forall @binders, @type` and its value is equivalent + to :n:`fun @binders => @term`. -.. note:: + To be accepted, a :cmd:`Fixpoint` definition has to satisfy some syntactical + constraints on a special argument called the decreasing argument. They + are needed to ensure that the :cmd:`Fixpoint` definition always terminates. + The point of the :n:`{struct @ident}` annotation is to let the user tell the + system which argument decreases along the recursive calls. - Some fixpoints may have several arguments that fit as decreasing - arguments, and this choice influences the reduction of the fixpoint. Hence an - explicit annotation must be used if the leftmost decreasing argument is not the - desired one. Writing explicit annotations can also speed up type-checking of - large mutual fixpoints. + The :n:`{struct @ident}` annotation may be left implicit, in this case the + system tries successively arguments from left to right until it finds one + that satisfies the decreasing condition. -The match operator matches a value (here :g:`n`) with the various -constructors of its (inductive) type. The remaining arguments give the -respective values to be returned, as functions of the parameters of the -corresponding constructor. Thus here when :g:`n` equals :g:`O` we return -:g:`m`, and when :g:`n` equals :g:`(S p)` we return :g:`(S (add p m))`. + .. note:: -The match operator is formally described in detail in Section -:ref:`match-construction`. -The system recognizes that in the inductive call :g:`(add p m)` the first -argument actually decreases because it is a *pattern variable* coming from -:g:`match n with`. + + Some fixpoints may have several arguments that fit as decreasing + arguments, and this choice influences the reduction of the fixpoint. + Hence an explicit annotation must be used if the leftmost decreasing + argument is not the desired one. Writing explicit annotations can also + speed up type-checking of large mutual fixpoints. -.. example:: + + In order to keep the strong normalization property, the fixed point + reduction will only be performed when the argument in position of the + decreasing argument (which type should be in an inductive definition) + starts with a constructor. - The following definition is not correct and generates an error message: - .. coqtop:: all + .. example:: + One can define the addition function as : - Fail Fixpoint wrongplus (n m:nat) {struct n} : nat := - match m with - | O => n - | S p => S (wrongplus n p) - end. + .. coqtop:: all - because the declared decreasing argument n actually does not decrease in - the recursive call. The function computing the addition over the second - argument should rather be written: + Fixpoint add (n m:nat) {struct n} : nat := + match n with + | O => m + | S p => S (add p m) + end. - .. coqtop:: all + The match operator matches a value (here :g:`n`) with the various + constructors of its (inductive) type. The remaining arguments give the + respective values to be returned, as functions of the parameters of the + corresponding constructor. Thus here when :g:`n` equals :g:`O` we return + :g:`m`, and when :g:`n` equals :g:`(S p)` we return :g:`(S (add p m))`. - Fixpoint plus (n m:nat) {struct m} : nat := - match m with - | O => n - | S p => S (plus n p) - end. + The match operator is formally described in + Section :ref:`match-construction`. + The system recognizes that in the inductive call :g:`(add p m)` the first + argument actually decreases because it is a *pattern variable* coming + from :g:`match n with`. -.. example:: + .. example:: - The ordinary match operation on natural numbers can be mimicked in the - following way. + The following definition is not correct and generates an error message: - .. coqtop:: all + .. coqtop:: all - Fixpoint nat_match - (C:Set) (f0:C) (fS:nat -> C -> C) (n:nat) {struct n} : C := - match n with - | O => f0 - | S p => fS p (nat_match C f0 fS p) - end. + Fail Fixpoint wrongplus (n m:nat) {struct n} : nat := + match m with + | O => n + | S p => S (wrongplus n p) + end. -.. example:: + because the declared decreasing argument :g:`n` does not actually + decrease in the recursive call. The function computing the addition over + the second argument should rather be written: - The recursive call may not only be on direct subterms of the recursive - variable n but also on a deeper subterm and we can directly write the - function mod2 which gives the remainder modulo 2 of a natural number. + .. coqtop:: all - .. coqtop:: all + Fixpoint plus (n m:nat) {struct m} : nat := + match m with + | O => n + | S p => S (plus n p) + end. - Fixpoint mod2 (n:nat) : nat := - match n with - | O => O - | S p => match p with - | O => S O - | S q => mod2 q - end - end. + .. example:: -In order to keep the strong normalization property, the fixed point -reduction will only be performed when the argument in position of the -decreasing argument (which type should be in an inductive definition) -starts with a constructor. + The recursive call may not only be on direct subterms of the recursive + variable :g:`n` but also on a deeper subterm and we can directly write + the function :g:`mod2` which gives the remainder modulo 2 of a natural + number. -The ``Fixpoint`` construction enjoys also the with extension to define functions -over mutually defined inductive types or more generally any mutually recursive -definitions. + .. coqtop:: all -.. cmdv:: Fixpoint @ident @params {struct @ident} : @type := @term {* with @ident {+ @params} : @type := @term} + Fixpoint mod2 (n:nat) : nat := + match n with + | O => O + | S p => match p with + | O => S O + | S q => mod2 q + end + end. -allows to define simultaneously fixpoints. -The size of trees and forests can be defined the following way: + .. cmdv:: Fixpoint @ident @binders {? {struct @ident} } {? : @type } := @term {* with @ident @binders {? : @type } := @term } + + This variant allows defining simultaneously several mutual fixpoints. + It is especially useful when defining functions over mutually defined + inductive types. -.. coqtop:: all + .. example:: + The size of trees and forests can be defined the following way: - Fixpoint tree_size (t:tree) : nat := - match t with - | node a f => S (forest_size f) - end - with forest_size (f:forest) : nat := - match f with - | leaf b => 1 - | cons t f' => (tree_size t + forest_size f') - end. + .. coqtop:: all -A generic command Scheme is useful to build automatically various mutual -induction principles. It is described in Section -:ref:`proofschemes-induction-principles`. + Fixpoint tree_size (t:tree) : nat := + match t with + | node a f => S (forest_size f) + end + with forest_size (f:forest) : nat := + match f with + | leaf b => 1 + | cons t f' => (tree_size t + forest_size f') + end. .. _cofixpoint: Definitions of recursive objects in co-inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: CoFixpoint @ident : @type := @term +.. cmd:: CoFixpoint @ident {? @binders } {? : @type } := @term -introduces a method for constructing an infinite object of a coinductive -type. For example, the stream containing all natural numbers can be -introduced applying the following method to the number :g:`O` (see -Section :ref:`coinductive-types` for the definition of :g:`Stream`, :g:`hd` and -:g:`tl`): + This command introduces a method for constructing an infinite object of a + coinductive type. For example, the stream containing all natural numbers can + be introduced applying the following method to the number :g:`O` (see + Section :ref:`coinductive-types` for the definition of :g:`Stream`, :g:`hd` + and :g:`tl`): -.. coqtop:: all - - CoFixpoint from (n:nat) : Stream := Seq n (from (S n)). - -Oppositely to recursive ones, there is no decreasing argument in a -co-recursive definition. To be admissible, a method of construction must -provide at least one extra constructor of the infinite object for each -iteration. A syntactical guard condition is imposed on co-recursive -definitions in order to ensure this: each recursive call in the -definition must be protected by at least one constructor, and only by -constructors. That is the case in the former definition, where the -single recursive call of :g:`from` is guarded by an application of -:g:`Seq`. On the contrary, the following recursive function does not -satisfy the guard condition: + .. coqtop:: all -.. coqtop:: all + CoFixpoint from (n:nat) : Stream := Seq n (from (S n)). - Fail CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream := - if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s). + Oppositely to recursive ones, there is no decreasing argument in a + co-recursive definition. To be admissible, a method of construction must + provide at least one extra constructor of the infinite object for each + iteration. A syntactical guard condition is imposed on co-recursive + definitions in order to ensure this: each recursive call in the + definition must be protected by at least one constructor, and only by + constructors. That is the case in the former definition, where the single + recursive call of :g:`from` is guarded by an application of :g:`Seq`. + On the contrary, the following recursive function does not satisfy the + guard condition: -The elimination of co-recursive definition is done lazily, i.e. the -definition is expanded only when it occurs at the head of an application -which is the argument of a case analysis expression. In any other -context, it is considered as a canonical expression which is completely -evaluated. We can test this using the command ``Eval``, which computes -the normal forms of a term: + .. coqtop:: all -.. coqtop:: all + Fail CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream := + if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s). - Eval compute in (from 0). - Eval compute in (hd (from 0)). - Eval compute in (tl (from 0)). + The elimination of co-recursive definition is done lazily, i.e. the + definition is expanded only when it occurs at the head of an application + which is the argument of a case analysis expression. In any other + context, it is considered as a canonical expression which is completely + evaluated. We can test this using the command :cmd:`Eval`, which computes + the normal forms of a term: -.. cmdv:: CoFixpoint @ident @params : @type := @term + .. coqtop:: all - As for most constructions, arguments of co-fixpoints expressions - can be introduced before the :g:`:=` sign. + Eval compute in (from 0). + Eval compute in (hd (from 0)). + Eval compute in (tl (from 0)). -.. cmdv:: CoFixpoint @ident : @type := @term {+ with @ident : @type := @term } + .. cmdv:: CoFixpoint @ident {? @binders } {? : @type } := @term {* with @ident {? @binders } : {? @type } := @term } - As in the :cmd:`Fixpoint` command, it is possible to introduce a block of - mutually dependent methods. + As in the :cmd:`Fixpoint` command, it is possible to introduce a block of + mutually dependent methods. .. _Assertions: @@ -1253,6 +1248,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: the theorem is bound to the name :token:`ident` in the environment. .. exn:: The term @term has type @type which should be Set, Prop or Type. + :undocumented: .. exn:: @ident already exists. :name: @ident already exists. (Theorem) @@ -1266,24 +1262,16 @@ Chapter :ref:`Tactics`. The basic assertion command is: This feature, called nested proofs, is disabled by default. To activate it, turn option :opt:`Nested Proofs Allowed` on. - The following commands are synonyms of :n:`Theorem @ident {? @binders } : type`: - .. cmdv:: Lemma @ident {? @binders } : @type - :name: Lemma - - .. cmdv:: Remark @ident {? @binders } : @type - :name: Remark - - .. cmdv:: Fact @ident {? @binders } : @type - :name: Fact - - .. cmdv:: Corollary @ident {? @binders } : @type - :name: Corollary + Remark @ident {? @binders } : @type + Fact @ident {? @binders } : @type + Corollary @ident {? @binders } : @type + Proposition @ident {? @binders } : @type + :name: Lemma; Remark; Fact; Corollary; Proposition - .. cmdv:: Proposition @ident {? @binders } : @type - :name: Proposition + These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`. -.. cmdv:: Theorem @ident : @type {* with @ident : @type} +.. cmdv:: Theorem @ident {? @binders } : @type {* with @ident {? @binders } : @type} This command is useful for theorems that are proved by simultaneous induction over a mutually inductive assumption, or that assert mutually dependent @@ -1305,7 +1293,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: The command can be used also with :cmd:`Lemma`, :cmd:`Remark`, etc. instead of :cmd:`Theorem`. -.. cmdv:: Definition @ident : @type +.. cmdv:: Definition @ident {? @binders } : @type This allows defining a term of type :token:`type` using the proof editing mode. It behaves as :cmd:`Theorem` but is intended to be used in conjunction with @@ -1316,22 +1304,22 @@ Chapter :ref:`Tactics`. The basic assertion command is: .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. -.. cmdv:: Let @ident : @type +.. cmdv:: Let @ident {? @binders } : @type - Like Definition :token:`ident` : :token:`type`. except that the definition is + Like :n:`Definition @ident {? @binders } : @type` except that the definition is turned into a let-in definition generalized over the declarations depending on it after closing the current section. -.. cmdv:: Fixpoint @ident @binders with +.. cmdv:: Fixpoint @ident @binders : @type {* with @ident @binders : @type} - This generalizes the syntax of Fixpoint so that one or more bodies + This generalizes the syntax of :cmd:`Fixpoint` so that one or more bodies can be defined interactively using the proof editing mode (when a body is omitted, its type is mandatory in the syntax). When the block - of proofs is completed, it is intended to be ended by Defined. + of proofs is completed, it is intended to be ended by :cmd:`Defined`. -.. cmdv:: CoFixpoint @ident with +.. cmdv:: CoFixpoint @ident {? @binders } : @type {* with @ident {? @binders } : @type} - This generalizes the syntax of CoFixpoint so that one or more bodies + This generalizes the syntax of :cmd:`CoFixpoint` so that one or more bodies can be defined interactively using the proof editing mode. A proof starts by the keyword :cmd:`Proof`. Then Coq enters the proof editing mode diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 2b128b98f..88c1e225f 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -178,7 +178,7 @@ Sequence A sequence is an expression of the following form: .. tacn:: @expr ; @expr - :name: ; + :name: ltac-seq The expression :n:`@expr__1` is evaluated to :n:`v__1`, which must be a tactic value. The tactic :n:`v__1` is applied to the current goal, diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 8d6e23764..ab3a485b2 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -118,7 +118,7 @@ class CoqObject(ObjectDescription): annotation = self.annotation + ' ' signode += addnodes.desc_annotation(annotation, annotation) self._render_signature(signature, signode) - return self.options.get("name") or self._name_from_signature(signature) + return self._names.get(signature) or self._name_from_signature(signature) def _record_name(self, name, target_id): """Record a name, mapping it to target_id @@ -176,8 +176,22 @@ class CoqObject(ObjectDescription): if report == "warning": raise self.warning(msg) + def _prepare_names(self): + sigs = self.get_signatures() + names = self.options.get("name") + if names is None: + self._names = {} + else: + names = [n.strip() for n in names.split(";")] + if len(names) != len(sigs): + ERR = ("Expected {} semicolon-separated names, got {}. " + + "Please provide one name per signature line.") + raise self.error(ERR.format(len(names), len(sigs))) + self._names = dict(zip(sigs, names)) + def run(self): self._warn_if_undocumented() + self._prepare_names() return super().run() class PlainObject(CoqObject): diff --git a/engine/uState.ml b/engine/uState.ml index 15cf4d4c1..643c621fd 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -305,8 +305,20 @@ let reference_of_level uctx = let pr_uctx_level uctx l = Libnames.pr_reference (reference_of_level uctx l) +type ('a, 'b) gen_universe_decl = { + univdecl_instance : 'a; (* Declared universes *) + univdecl_extensible_instance : bool; (* Can new universes be added *) + univdecl_constraints : 'b; (* Declared constraints *) + univdecl_extensible_constraints : bool (* Can new constraints be added *) } + type universe_decl = - (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl + (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl + +let default_univ_decl = + { univdecl_instance = []; + univdecl_extensible_instance = true; + univdecl_constraints = Univ.Constraint.empty; + univdecl_extensible_constraints = true } let error_unbound_universes left uctx = let open Univ in @@ -367,7 +379,6 @@ let check_implication uctx cstrs cstrs' = (str "Universe constraints are not implied by the ones declared.") let check_mono_univ_decl uctx decl = - let open Misctypes in let () = let names = decl.univdecl_instance in let extensible = decl.univdecl_extensible_instance in @@ -380,7 +391,6 @@ let check_mono_univ_decl uctx decl = uctx.uctx_local let check_univ_decl ~poly uctx decl = - let open Misctypes in let ctx = let names = decl.univdecl_instance in let extensible = decl.univdecl_extensible_instance in diff --git a/engine/uState.mli b/engine/uState.mli index d1678a155..e2f25642e 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -138,8 +138,16 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst (** Universe minimization *) val minimize : t -> t +type ('a, 'b) gen_universe_decl = { + univdecl_instance : 'a; (* Declared universes *) + univdecl_extensible_instance : bool; (* Can new universes be added *) + univdecl_constraints : 'b; (* Declared constraints *) + univdecl_extensible_constraints : bool (* Can new constraints be added *) } + type universe_decl = - (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl + (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl + +val default_univ_decl : universe_decl (** [check_univ_decl ctx decl] diff --git a/pretyping/constrexpr.ml b/interp/constrexpr.ml index 1443dfb51..ca6ea94f0 100644 --- a/pretyping/constrexpr.ml +++ b/interp/constrexpr.ml @@ -16,8 +16,7 @@ open Decl_kinds (** {6 Concrete syntax for terms } *) (** [constr_expr] is the abstract syntax tree produced by the parser *) - -type universe_decl_expr = (lident list, Glob_term.glob_constraint list) gen_universe_decl +type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl type ident_decl = lident * universe_decl_expr option type name_decl = lname * universe_decl_expr option diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 3eb5acfc5..1be1dd96c 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -600,3 +600,35 @@ let _ = Goptions.declare_bool_option { Goptions.optread = (fun () -> !asymmetric_patterns); Goptions.optwrite = (fun a -> asymmetric_patterns:=a); } + +(** Local universe and constraint declarations. *) + +let interp_univ_constraints env evd cstrs = + let interp (evd,cstrs) (u, d, u') = + let ul = Pretyping.interp_known_glob_level evd u in + let u'l = Pretyping.interp_known_glob_level evd u' in + let cstr = (ul,d,u'l) in + let cstrs' = Univ.Constraint.add cstr cstrs in + try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in + evd, cstrs' + with Univ.UniverseInconsistency e -> + CErrors.user_err ~hdr:"interp_constraint" + (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e) + in + List.fold_left interp (evd,Univ.Constraint.empty) cstrs + +let interp_univ_decl env decl = + let open UState in + let pl : lident list = decl.univdecl_instance in + let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in + let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in + let decl = { univdecl_instance = pl; + univdecl_extensible_instance = decl.univdecl_extensible_instance; + univdecl_constraints = cstrs; + univdecl_extensible_constraints = decl.univdecl_extensible_constraints } + in evd, decl + +let interp_univ_decl_opt env l = + match l with + | None -> Evd.from_env env, UState.default_univ_decl + | Some decl -> interp_univ_decl env decl diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 2df9e5a8c..b4f0886ac 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -116,3 +116,10 @@ val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a (** Placeholder for global option, should be moved to a parameter *) val asymmetric_patterns : bool ref + +(** Local universe and constraint declarations. *) +val interp_univ_decl : Environ.env -> universe_decl_expr -> + Evd.evar_map * UState.universe_decl + +val interp_univ_decl_opt : Environ.env -> universe_decl_expr option -> + Evd.evar_map * UState.universe_decl diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3a88284e4..848180743 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -820,11 +820,11 @@ let split_by_type ids subst = | NtnTypeConstr -> let terms,terms' = bind id scl terms terms' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.AsStrictPattern) -> + | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnBinderParsedAsConstr Extend.AsIdent -> + | NtnTypeBinder NtnBinderParsedAsConstr AsIdent -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') @@ -999,7 +999,7 @@ let intern_qualid qid intern env ntnvars us args = match intern_extended_global_of_qualid qid with | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args | SynDef sp -> - let (ids,c) = Syntax_def.search_syntactic_definition sp in + let (ids,c) = Syntax_def.search_syntactic_definition ?loc sp in let nids = List.length ids in if List.length args < nids then error_not_enough_arguments ?loc; let args1,args2 = List.chop nids args in @@ -1141,9 +1141,18 @@ let check_number_of_pattern loc n l = if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p))) let check_or_pat_variables loc ids idsl = - if List.exists (fun ids' -> not (List.eq_set (fun {loc;v=id} {v=id'} -> Id.equal id id') ids ids')) idsl then - user_err ?loc (str - "The components of this disjunctive pattern must bind the same variables.") + let eq_id {v=id} {v=id'} = Id.equal id id' in + (* Collect remaining patterns which do not have the same variables as the first pattern *) + let idsl = List.filter (fun ids' -> not (List.eq_set eq_id ids ids')) idsl in + match idsl with + | ids'::_ -> + (* Look for an [id] which is either in [ids] and not in [ids'] or in [ids'] and not in [ids] *) + let ids'' = List.subtract eq_id ids ids' in + let ids'' = if ids'' = [] then List.subtract eq_id ids' ids else ids'' in + user_err ?loc + (strbrk "The components of this disjunctive pattern must bind the same variables (" ++ + Id.print (List.hd ids'').v ++ strbrk " is not bound in all patterns).") + | [] -> () (** Use only when params were NOT asked to the user. @return if letin are included *) diff --git a/pretyping/genredexpr.ml b/interp/genredexpr.ml index 80697461a..80697461a 100644 --- a/pretyping/genredexpr.ml +++ b/interp/genredexpr.ml diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 289890544..b48db9ac5 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -17,12 +17,14 @@ open Glob_term open Constrexpr open Libnames open Typeclasses -open Typeclasses_errors open Pp open Libobject open Nameops open Context.Rel.Declaration +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *) +let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m)) + module RelDecl = Context.Rel.Declaration (*i*) @@ -238,7 +240,7 @@ let implicit_application env ?(allow_partial=true) f ty = let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in if not (Int.equal needlen applen) then - Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd + mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd end; let pars = List.rev (List.combine ci rd) in let args, avoid = combine_params avoid f par pars in diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 39d0174f9..e64c5c542 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -45,3 +45,7 @@ val implicit_application : Id.Set.t -> ?allow_partial:bool -> (Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t -> Constrexpr.constr_expr * Id.Set.t) -> constr_expr -> constr_expr * Id.Set.t + +(* Should be likely located elsewhere *) +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *) +val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Context.Rel.t -> 'a diff --git a/interp/interp.mllib b/interp/interp.mllib index 37a327a7d..3668455ae 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,3 +1,6 @@ +Constrexpr +Genredexpr +Redops Tactypes Stdarg Genintern @@ -7,7 +10,6 @@ Notation Syntax_def Smartlocate Constrexpr_ops -Ppextend Dumpglob Reserve Impargs diff --git a/interp/modintern.ml b/interp/modintern.ml index dc93d8dc4..fefd2ab6f 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -63,7 +63,7 @@ let transl_with_decl env = function | CWith_Module ({CAst.v=fqid},qid) -> WithMod (fqid,lookup_module qid), Univ.ContextSet.empty | CWith_Definition ({CAst.v=fqid},udecl,c) -> - let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in + let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in let c, ectx = interp_constr env sigma c in begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with | Entries.Polymorphic_const_entry ctx -> diff --git a/interp/notation.ml b/interp/notation.ml index 192c477be..05fcd0e7f 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -20,7 +20,6 @@ open Constrexpr open Notation_term open Glob_term open Glob_ops -open Ppextend open Context.Named.Declaration (*i*) @@ -56,9 +55,6 @@ type scope = { delimiters: delimiters option } -(* Uninterpreted notation map: notation -> level * DirPath.t *) -let notation_level_map = ref String.Map.empty - (* Scopes table: scope_name -> symbol_interpretation *) let scope_map = ref String.Map.empty @@ -75,44 +71,6 @@ let default_scope = "" (* empty name, not available from outside *) let init_scope_map () = scope_map := String.Map.add default_scope empty_scope !scope_map -(**********************************************************************) -(* Operations on scopes *) - -let parenRelation_eq t1 t2 = match t1, t2 with -| L, L | E, E | Any, Any -> true -| Prec l1, Prec l2 -> Int.equal l1 l2 -| _ -> false - -open Extend - -let production_level_eq l1 l2 = true (* (l1 = l2) *) - -let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with -| NextLevel, NextLevel -> true -| NumLevel n1, NumLevel n2 -> Int.equal n1 n2 -| (NextLevel | NumLevel _), _ -> false *) - -let constr_entry_key_eq eq v1 v2 = match v1, v2 with -| ETName, ETName -> true -| ETReference, ETReference -> true -| ETBigint, ETBigint -> true -| ETBinder b1, ETBinder b2 -> b1 == b2 -| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2 -| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2 -| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 -| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2' -| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false - -let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) = - let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in - let prod_eq (l1,pp1) (l2,pp2) = - if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2 - else production_level_eq l1 l2 in - Int.equal l1 l2 && List.equal tolerability_eq t1 t2 - && List.equal (constr_entry_key_eq prod_eq) u1 u2 - -let level_eq = level_eq_gen false - let declare_scope scope = try let _ = String.Map.find scope !scope_map in () with Not_found -> @@ -427,18 +385,6 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function (* Can we switch to [scope]? Yes if it has defined delimiters *) find_with_delimiters ntn_scope -(* Uninterpreted notation levels *) - -let declare_notation_level ?(onlyprint=false) ntn level = - if String.Map.mem ntn !notation_level_map then - anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level."); - notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map - -let level_of_notation ?(onlyprint=false) ntn = - let (level,onlyprint') = String.Map.find ntn !notation_level_map in - if onlyprint' && not onlyprint then raise Not_found; - level - (* The mapping between notations and their interpretation *) let warn_notation_overridden = @@ -1113,63 +1059,24 @@ let pr_visibility prglob = function | None -> pr_scope_stack prglob !scope_stack (**********************************************************************) -(* Mapping notations to concrete syntax *) - -type unparsing_rule = unparsing list * precedence -type extra_unparsing_rules = (string * string) list -(* Concrete syntax for symbolic-extension table *) -let notation_rules = - ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t) - -let declare_notation_rule ntn ~extra unpl gram = - notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules - -let find_notation_printing_rule ntn = - try pi1 (String.Map.find ntn !notation_rules) - with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".") -let find_notation_extra_printing_rules ntn = - try pi2 (String.Map.find ntn !notation_rules) - with Not_found -> [] -let find_notation_parsing_rules ntn = - try pi3 (String.Map.find ntn !notation_rules) - with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".") - -let get_defined_notations () = - String.Set.elements @@ String.Map.domain !notation_rules - -let add_notation_extra_printing_rule ntn k v = - try - notation_rules := - let p, pp, gr = String.Map.find ntn !notation_rules in - String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules - with Not_found -> - user_err ~hdr:"add_notation_extra_printing_rule" - (str "No such Notation.") - -(**********************************************************************) (* Synchronisation with reset *) let freeze _ = - (!scope_map, !notation_level_map, !scope_stack, !arguments_scope, - !delimiters_map, !notations_key_table, !notation_rules, - !scope_class_map) + (!scope_map, !scope_stack, !arguments_scope, + !delimiters_map, !notations_key_table, !scope_class_map) -let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) = +let unfreeze (scm,scs,asc,dlm,fkm,clsc) = scope_map := scm; - notation_level_map := nlm; scope_stack := scs; delimiters_map := dlm; arguments_scope := asc; notations_key_table := fkm; - notation_rules := pprules; scope_class_map := clsc let init () = init_scope_map (); - notation_level_map := String.Map.empty; delimiters_map := String.Map.empty; notations_key_table := KeyMap.empty; - notation_rules := String.Map.empty; scope_class_map := initial_scope_class_map let _ = diff --git a/interp/notation.mli b/interp/notation.mli index ccc67fe49..b177b7f1e 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -14,7 +14,6 @@ open Libnames open Constrexpr open Glob_term open Notation_term -open Ppextend (** Notations *) @@ -32,8 +31,6 @@ val declare_scope : scope_name -> unit val current_scopes : unit -> scopes -val level_eq : level -> level -> bool - (** Check where a scope is opened or not in a scope list, or in * the current opened scopes *) val scope_is_open_in_scopes : scope_name -> scopes -> bool @@ -135,11 +132,6 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list val availability_of_notation : scope_name option * notation -> local_scopes -> (scope_name option * delimiters option) option -(** {6 Declare and test the level of a (possibly uninterpreted) notation } *) - -val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit -val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *) - (** {6 Miscellaneous} *) val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> @@ -200,21 +192,6 @@ val locate_notation : (glob_constr -> Pp.t) -> notation -> val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t -(** {6 Printing rules for notations} *) - -(** Declare and look for the printing rule for symbolic notations *) -type unparsing_rule = unparsing list * precedence -type extra_unparsing_rules = (string * string) list -val declare_notation_rule : - notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit -val find_notation_printing_rule : notation -> unparsing_rule -val find_notation_extra_printing_rules : notation -> extra_unparsing_rules -val find_notation_parsing_rules : notation -> notation_grammar -val add_notation_extra_printing_rule : notation -> string -> string -> unit - -(** Returns notations with defined parsing/printing rules *) -val get_defined_notations : unit -> notation list - (** Rem: printing rules for primitive token are canonical *) val with_notation_protection : ('a -> 'b) -> 'a -> 'b diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index b0480aa70..f208b23fb 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -687,7 +687,7 @@ let is_onlybinding_meta id metas = let is_onlybinding_pattern_like_meta isvar id metas = try match Id.List.assoc id metas with | _,NtnTypeBinder (NtnBinderParsedAsConstr - (Extend.AsIdentOrPattern | Extend.AsStrictPattern)) -> true + (AsIdentOrPattern | AsStrictPattern)) -> true | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar) | _ -> false with Not_found -> false diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 1a46746cc..52a6354a0 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -62,6 +62,11 @@ type subscopes = tmp_scope_name option * scope_name list (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y, x carries the sequence of objects bound to the list x..y *) +type constr_as_binder_kind = + | AsIdent + | AsIdentOrPattern + | AsStrictPattern + type notation_binder_source = (* This accepts only pattern *) (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *) @@ -69,7 +74,7 @@ type notation_binder_source = (* This accepts only ident *) | NtnParsedAsIdent (* This accepts ident, or pattern, or both *) - | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind + | NtnBinderParsedAsConstr of constr_as_binder_kind type notation_var_instance_type = | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList @@ -91,33 +96,3 @@ type notation_interp_env = { ninterp_var_type : notation_var_internalization_type Id.Map.t; ninterp_rec_vars : Id.t Id.Map.t; } - -type grammar_constr_prod_item = - | GramConstrTerminal of Tok.t - | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option - | GramConstrListMark of int * bool * int - (* tells action rule to make a list of the n previous parsed items; - concat with last parsed list when true; additionally release - the p last items as if they were parsed autonomously *) - -(** Dealing with precedences *) - -type precedence = int -type parenRelation = L | E | Any | Prec of precedence -type tolerability = precedence * parenRelation - -type level = precedence * tolerability list * Extend.constr_entry_key list - -(** Grammar rules for a notation *) - -type one_notation_grammar = { - notgram_level : level; - notgram_assoc : Extend.gram_assoc option; - notgram_notation : Constrexpr.notation; - notgram_prods : grammar_constr_prod_item list list; -} - -type notation_grammar = { - notgram_onlyprinting : bool; - notgram_rules : one_notation_grammar list -} diff --git a/pretyping/redops.ml b/interp/redops.ml index 90c3bdfae..b9a74136e 100644 --- a/pretyping/redops.ml +++ b/interp/redops.ml @@ -42,3 +42,23 @@ let make_red_flag l = let all_flags = {rBeta = true; rMatch = true; rFix = true; rCofix = true; rZeta = true; rDelta = true; rConst = []} + +(** Mapping [red_expr_gen] *) + +let map_flags f flags = + { flags with rConst = List.map f flags.rConst } + +let map_occs f (occ,e) = (occ,f e) + +let map_red_expr_gen f g h = function + | Fold l -> Fold (List.map f l) + | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l) + | Simpl (flags,occs_o) -> + Simpl (map_flags g flags, Option.map (map_occs (Util.map_union g h)) occs_o) + | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l) + | Cbv flags -> Cbv (map_flags g flags) + | Lazy flags -> Lazy (map_flags g flags) + | CbvVm occs_o -> CbvVm (Option.map (map_occs (Util.map_union g h)) occs_o) + | CbvNative occs_o -> CbvNative (Option.map (map_occs (Util.map_union g h)) occs_o) + | Cbn flags -> Cbn (map_flags g flags) + | ExtraRedExpr _ | Red _ | Hnf as x -> x diff --git a/pretyping/redops.mli b/interp/redops.mli index 285931ecd..7254f29b2 100644 --- a/pretyping/redops.mli +++ b/interp/redops.mli @@ -13,3 +13,8 @@ open Genredexpr val make_red_flag : 'a red_atom list -> 'a glob_red_flag val all_flags : 'a glob_red_flag + +(** Mapping [red_expr_gen] *) + +val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) -> + ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 47faa5885..a4f20fd73 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -96,13 +96,13 @@ let warn_compatibility_notation = CWarnings.(create ~name:"compatibility-notation" ~category:"deprecated" ~default:Enabled pr_compat_warning) -let verbose_compat kn def = function +let verbose_compat ?loc kn def = function | Some v when Flags.version_strictly_greater v -> - warn_compatibility_notation (kn, def, v) + warn_compatibility_notation ?loc (kn, def, v) | _ -> () -let search_syntactic_definition kn = +let search_syntactic_definition ?loc kn = let pat,v = KNmap.find kn !syntax_table in let def = out_pat pat in - verbose_compat kn def v; + verbose_compat ?loc kn def v; def diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 1933b8a9a..c5b6655ff 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -18,4 +18,4 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr val declare_syntactic_definition : bool -> Id.t -> Flags.compat_version option -> syndef_interpretation -> unit -val search_syntactic_definition : KerName.t -> syndef_interpretation +val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 8389dd326..b722e4200 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -708,12 +708,10 @@ let rec lambda_of_constr env c = Lcofix(init, (names, ltypes, lbodies)) | Proj (p,c) -> - let kn = Projection.constant p in - let cb = lookup_constant kn env.global_env in - let pb = Option.get cb.const_proj in + let pb = lookup_projection p env.global_env in let n = pb.proj_arg in let lc = lambda_of_constr env c in - Lproj (n,kn,lc) + Lproj (n,Projection.constant p,lc) and lambda_of_app env f args = match Constr.kind f with diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 6f4541e95..5783453e6 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -156,7 +156,7 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : projection_body option; + cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; @@ -227,28 +227,10 @@ let cook_constant ~hcons env { from = cb; info } = hyps) hyps ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in - let projection pb = - let c' = abstract_constant_body (expmod pb.proj_body) hyps in - let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in - let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in - let ((mind, _), _), n' = - try - let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in - match kind c' with - | App (f,l) -> (destInd f, Array.length l) - | Ind ind -> ind, 0 - | _ -> assert false - with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0) - in - let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in - { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg; - proj_eta = etab, etat; - proj_type = ty'; proj_body = c' } - in { cook_body = body; cook_type = typ; - cook_proj = Option.map projection cb.const_proj; + cook_proj = cb.const_proj; cook_universes = univs; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7bd0ae566..0d907f3de 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,7 +21,7 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : projection_body option; + cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index b7427d20a..913c13173 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -87,7 +87,7 @@ type constant_body = { const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; - const_proj : projection_body option; + const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 832d478b3..75c0e5b4c 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -94,14 +94,13 @@ let subst_const_body sub cb = else let body' = subst_const_def sub cb.const_body in let type' = subst_const_type sub cb.const_type in - let proj' = Option.Smart.map (subst_const_proj sub) cb.const_proj in if body' == cb.const_body && type' == cb.const_type - && proj' == cb.const_proj then cb + then cb else { const_hyps = []; const_body = body'; const_type = type'; - const_proj = proj'; + const_proj = cb.const_proj; const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; diff --git a/kernel/environ.ml b/kernel/environ.ml index c3e7cec75..fb89576dd 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -52,6 +52,7 @@ type mind_key = mutual_inductive_body * link_info ref type globals = { env_constants : constant_key Cmap_env.t; + env_projections : projection_body Cmap_env.t; env_inductives : mind_key Mindmap_env.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t} @@ -108,6 +109,7 @@ let empty_rel_context_val = { let empty_env = { env_globals = { env_constants = Cmap_env.empty; + env_projections = Cmap_env.empty; env_inductives = Mindmap_env.empty; env_modules = MPmap.empty; env_modtypes = MPmap.empty}; @@ -485,14 +487,10 @@ let type_in_type_constant cst env = not (lookup_constant cst env).const_typing_flags.check_universes let lookup_projection cst env = - match (lookup_constant (Projection.constant cst) env).const_proj with - | Some pb -> pb - | None -> anomaly (Pp.str "lookup_projection: constant is not a projection.") + Cmap_env.find (Projection.constant cst) env.env_globals.env_projections let is_projection cst env = - match (lookup_constant cst env).const_proj with - | Some _ -> true - | None -> false + (lookup_constant cst env).const_proj (* Mutual Inductives *) let polymorphic_ind (mind,i) env = @@ -514,11 +512,18 @@ let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false else template_polymorphic_ind ind env -let add_mind_key kn mind_key env = +let add_mind_key kn (mind, _ as mind_key) env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in + let new_projections = match mind.mind_record with + | None | Some None -> env.env_globals.env_projections + | Some (Some (id, kns, pbs)) -> + Array.fold_left2 (fun projs kn pb -> + Cmap_env.add kn pb projs) + env.env_globals.env_projections kns pbs + in let new_globals = { env.env_globals with - env_inductives = new_inds } in + env_inductives = new_inds; env_projections = new_projections; } in { env with env_globals = new_globals } let add_mind kn mib env = diff --git a/kernel/environ.mli b/kernel/environ.mli index fc45ce0e3..8928b32f1 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -48,6 +48,7 @@ type mind_key = mutual_inductive_body * link_info ref type globals = { env_constants : constant_key Cmap_env.t; + env_projections : projection_body Cmap_env.t; env_inductives : mind_key Mindmap_env.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 9bed598bb..090acdf16 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -803,9 +803,7 @@ let rec subterm_specif renv stack t = (* We take the subterm specs of the constructor of the record *) let wf_args = (dest_subterms wf).(0) in (* We extract the tree of the projected argument *) - let kn = Projection.constant p in - let cb = lookup_constant kn renv.env in - let pb = Option.get cb.const_proj in + let pb = lookup_projection p renv.env in let n = pb.proj_arg in spec_of_tree (List.nth wf_args n) | Dead_code -> Dead_code diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 0cd0ad46c..036cd4847 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1859,7 +1859,7 @@ and compile_named env sigma univ auxdefs id = let compile_constant env sigma prefix ~interactive con cb = match cb.const_proj with - | None -> + | false -> let no_univs = match cb.const_universes with | Monomorphic_const _ -> true @@ -1903,7 +1903,8 @@ let compile_constant env sigma prefix ~interactive con cb = if interactive then LinkedInteractive prefix else Linked prefix end - | Some pb -> + | true -> + let pb = lookup_projection (Projection.make con false) env in let mind = pb.proj_ind in let ind = (mind,0) in let mib = lookup_mind mind env in @@ -2029,11 +2030,12 @@ let rec compile_deps env sigma prefix ~interactive init t = else let comp_stack, (mind_updates, const_updates) = match cb.const_proj, cb.const_body with - | None, Def t -> + | false, Def t -> compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t) - | Some pb, _ -> - let mind = pb.proj_ind in - compile_mind_deps env prefix ~interactive init mind + | true, _ -> + let pb = lookup_projection (Projection.make c false) env in + let mind = pb.proj_ind in + compile_mind_deps env prefix ~interactive init mind | _ -> init in let code, name = diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 7352c1882..db1109e75 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -250,7 +250,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Undef nl; cook_type = t; - cook_proj = None; + cook_proj = false; cook_universes = univs; cook_inline = false; cook_context = ctx; @@ -291,7 +291,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = None; + cook_proj = false; cook_universes = Monomorphic_const univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -343,7 +343,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = None; + cook_proj = false; cook_universes = univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -370,7 +370,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term)); cook_type = typ; - cook_proj = Some pb; + cook_proj = true; cook_universes = univs; cook_inline = false; cook_context = None; @@ -458,30 +458,8 @@ let build_constant_declaration kn env result = check declared inferred) lc) in let univs = result.cook_universes in let tps = - let res = - match result.cook_proj with - | None -> Cbytegen.compile_constant_body ~fail_on_error:false env univs def - | Some pb -> - (* The compilation of primitive projections is a bit tricky, because - they refer to themselves (the body of p looks like fun c => - Proj(p,c)). We break the cycle by building an ad-hoc compilation - environment. A cleaner solution would be that kernel projections are - simply Proj(i,c) with i an int and c a constr, but we would have to - get rid of the compatibility layer. *) - let cb = - { const_hyps = hyps; - const_body = def; - const_type = typ; - const_proj = result.cook_proj; - const_body_code = None; - const_universes = univs; - const_inline_code = result.cook_inline; - const_typing_flags = Environ.typing_flags env; - } - in - let env = add_constant kn cb env in - Cbytegen.compile_constant_body ~fail_on_error:false env univs def - in Option.map Cemitcodes.from_val res + let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in + Option.map Cemitcodes.from_val res in { const_hyps = hyps; const_body = def; diff --git a/kernel/typeops.ml b/kernel/typeops.ml index fd9cefb2c..325d5cecd 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -528,13 +528,3 @@ let judge_of_case env ci pj cj lfj = let lf, lft = dest_judgev lfj in make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) - -let type_of_projection_constant env (p,u) = - let cst = Projection.constant p in - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if Declareops.constant_is_polymorphic cb then - Vars.subst_instance_constr u pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 85b2cfffd..546f2d2b4 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -100,8 +100,6 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -val type_of_projection_constant : env -> Projection.t puniverses -> types - val type_of_constant_in : env -> pconstant -> types (** Check that hyps are included in env and fails with error otherwise *) diff --git a/library/heads.ml b/library/heads.ml index 198672a0a..3d5f6a6ff 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -129,7 +129,7 @@ let compute_head = function let cb = Environ.lookup_constant cst env in let is_Def = function Declarations.Def _ -> true | _ -> false in let body = - if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body + if not cb.Declarations.const_proj && is_Def cb.Declarations.const_body then Global.body_of_constant cst else None in (match body with diff --git a/library/misctypes.ml b/library/misctypes.ml index a3c887045..cfae07484 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -112,9 +112,3 @@ type multi = | UpTo of int | RepeatStar | RepeatPlus - -type ('a, 'b) gen_universe_decl = { - univdecl_instance : 'a; (* Declared universes *) - univdecl_extensible_instance : bool; (* Can new universes be added *) - univdecl_constraints : 'b; (* Declared constraints *) - univdecl_extensible_constraints : bool (* Can new constraints be added *) } diff --git a/parsing/extend.ml b/parsing/extend.ml index 734b859f6..f2af594ef 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -31,11 +31,6 @@ type production_level = | NextLevel | NumLevel of int -type constr_as_binder_kind = - | AsIdent - | AsIdentOrPattern - | AsStrictPattern - (** User-level types used to tell how to parse or interpret of the non-terminal *) type 'a constr_entry_key_gen = @@ -44,7 +39,7 @@ type 'a constr_entry_key_gen = | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) | ETConstr of 'a - | ETConstrAsBinder of constr_as_binder_kind * 'a + | ETConstrAsBinder of Notation_term.constr_as_binder_kind * 'a | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *) | ETOther of string * string diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml new file mode 100644 index 000000000..346350641 --- /dev/null +++ b/parsing/notation_gram.ml @@ -0,0 +1,42 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Extend + +(** Dealing with precedences *) + +type precedence = int +type parenRelation = L | E | Any | Prec of precedence +type tolerability = precedence * parenRelation + +type level = precedence * tolerability list * constr_entry_key list + +type grammar_constr_prod_item = + | GramConstrTerminal of Tok.t + | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option + | GramConstrListMark of int * bool * int + (* tells action rule to make a list of the n previous parsed items; + concat with last parsed list when true; additionally release + the p last items as if they were parsed autonomously *) + +(** Grammar rules for a notation *) + +type one_notation_grammar = { + notgram_level : level; + notgram_assoc : Extend.gram_assoc option; + notgram_notation : Constrexpr.notation; + notgram_prods : grammar_constr_prod_item list list; +} + +type notation_grammar = { + notgram_onlyprinting : bool; + notgram_rules : one_notation_grammar list +} diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml new file mode 100644 index 000000000..071e6db20 --- /dev/null +++ b/parsing/notgram_ops.ml @@ -0,0 +1,65 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open CErrors +open Util +open Extend +open Notation_gram + +(* Uninterpreted notation levels *) + +let notation_level_map = Summary.ref ~name:"notation_level_map" String.Map.empty + +let declare_notation_level ?(onlyprint=false) ntn level = + if String.Map.mem ntn !notation_level_map then + anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level."); + notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map + +let level_of_notation ?(onlyprint=false) ntn = + let (level,onlyprint') = String.Map.find ntn !notation_level_map in + if onlyprint' && not onlyprint then raise Not_found; + level + +(**********************************************************************) +(* Operations on scopes *) + +let parenRelation_eq t1 t2 = match t1, t2 with +| L, L | E, E | Any, Any -> true +| Prec l1, Prec l2 -> Int.equal l1 l2 +| _ -> false + +let production_level_eq l1 l2 = true (* (l1 = l2) *) + +let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with +| NextLevel, NextLevel -> true +| NumLevel n1, NumLevel n2 -> Int.equal n1 n2 +| (NextLevel | NumLevel _), _ -> false *) + +let constr_entry_key_eq eq v1 v2 = match v1, v2 with +| ETName, ETName -> true +| ETReference, ETReference -> true +| ETBigint, ETBigint -> true +| ETBinder b1, ETBinder b2 -> b1 == b2 +| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2 +| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2 +| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 +| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2' +| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false + +let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) = + let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in + let prod_eq (l1,pp1) (l2,pp2) = + if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2 + else production_level_eq l1 l2 in + Int.equal l1 l2 && List.equal tolerability_eq t1 t2 + && List.equal (constr_entry_key_eq prod_eq) u1 u2 + +let level_eq = level_eq_gen false diff --git a/pretyping/univdecls.mli b/parsing/notgram_ops.mli index 305d045b1..f427a607b 100644 --- a/pretyping/univdecls.mli +++ b/parsing/notgram_ops.mli @@ -8,14 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Local universe and constraint declarations. *) -type universe_decl = - (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl +(* Merge with metasyntax? *) +open Constrexpr +open Notation_gram -val default_univ_decl : universe_decl +val level_eq : level -> level -> bool -val interp_univ_decl : Environ.env -> Constrexpr.universe_decl_expr -> - Evd.evar_map * universe_decl +(** {6 Declare and test the level of a (possibly uninterpreted) notation } *) -val interp_univ_decl_opt : Environ.env -> Constrexpr.universe_decl_expr option -> - Evd.evar_map * universe_decl +val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit +val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *) diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index da4a0421b..2154f2f88 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,6 +1,9 @@ Tok CLexer Extend +Notation_gram +Ppextend +Notgram_ops Pcoq G_constr G_prim diff --git a/interp/ppextend.ml b/parsing/ppextend.ml index c75d9e12f..d2b50fa83 100644 --- a/interp/ppextend.ml +++ b/parsing/ppextend.ml @@ -8,8 +8,10 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Util open Pp -open Notation_term +open CErrors +open Notation_gram (*s Pretty-print. *) @@ -41,3 +43,34 @@ type unparsing = | UnpTerminal of string | UnpBox of ppbox * unparsing Loc.located list | UnpCut of ppcut + +type unparsing_rule = unparsing list * precedence +type extra_unparsing_rules = (string * string) list +(* Concrete syntax for symbolic-extension table *) +let notation_rules = + Summary.ref ~name:"notation-rules" (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t) + +let declare_notation_rule ntn ~extra unpl gram = + notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules + +let find_notation_printing_rule ntn = + try pi1 (String.Map.find ntn !notation_rules) + with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".") +let find_notation_extra_printing_rules ntn = + try pi2 (String.Map.find ntn !notation_rules) + with Not_found -> [] +let find_notation_parsing_rules ntn = + try pi3 (String.Map.find ntn !notation_rules) + with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".") + +let get_defined_notations () = + String.Set.elements @@ String.Map.domain !notation_rules + +let add_notation_extra_printing_rule ntn k v = + try + notation_rules := + let p, pp, gr = String.Map.find ntn !notation_rules in + String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules + with Not_found -> + user_err ~hdr:"add_notation_extra_printing_rule" + (str "No such Notation.") diff --git a/interp/ppextend.mli b/parsing/ppextend.mli index c81058e72..9f61e121a 100644 --- a/interp/ppextend.mli +++ b/parsing/ppextend.mli @@ -8,7 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Notation_term +open Constrexpr +open Notation_gram (** {6 Pretty-print. } *) @@ -26,6 +27,9 @@ val ppcmd_of_box : ppbox -> Pp.t -> Pp.t val ppcmd_of_cut : ppcut -> Pp.t +(** {6 Printing rules for notations} *) + +(** Declare and look for the printing rule for symbolic notations *) type unparsing = | UnpMetaVar of int * parenRelation | UnpBinderMetaVar of int * parenRelation @@ -34,3 +38,15 @@ type unparsing = | UnpTerminal of string | UnpBox of ppbox * unparsing Loc.located list | UnpCut of ppcut + +type unparsing_rule = unparsing list * precedence +type extra_unparsing_rules = (string * string) list + +val declare_notation_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit +val find_notation_printing_rule : notation -> unparsing_rule +val find_notation_extra_printing_rules : notation -> extra_unparsing_rules +val find_notation_parsing_rules : notation -> notation_grammar +val add_notation_extra_printing_rule : notation -> string -> string -> unit + +(** Returns notations with defined parsing/printing rules *) +val get_defined_notations : unit -> notation list diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index cdd698304..5aee70194 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1066,8 +1066,10 @@ let extract_constant env kn cb = | Undef _ -> warn_info (); mk_typ_ax () | Def c -> (match cb.const_proj with - | None -> mk_typ (get_body c) - | Some pb -> mk_typ (EConstr.of_constr pb.proj_body)) + | false -> mk_typ (get_body c) + | true -> + let pb = lookup_projection (Projection.make kn false) env in + mk_typ (EConstr.of_constr pb.proj_body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_typ (get_opaque env c) @@ -1077,8 +1079,10 @@ let extract_constant env kn cb = | Undef _ -> warn_info (); mk_ax () | Def c -> (match cb.const_proj with - | None -> mk_def (get_body c) - | Some pb -> mk_def (EConstr.of_constr pb.proj_body)) + | false -> mk_def (get_body c) + | true -> + let pb = lookup_projection (Projection.make kn false) env in + mk_def (EConstr.of_constr pb.proj_body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_def (get_opaque env c) diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 702b83034..4e7c8b754 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -251,7 +251,7 @@ END let pr_by_arg_tac _prc _prlc prtac opt_c = match opt_c with | None -> mt () - | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t) + | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t) ARGUMENT EXTEND by_arg_tac TYPED AS tactic_opt diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index e5a4f090e..ff697e3c7 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -66,7 +66,7 @@ val wit_by_arg_tac : Geninterp.Val.t option) Genarg.genarg_type val pr_by_arg_tac : - (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) -> + (int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) -> raw_tactic_expr option -> Pp.t val test_lpar_id_colon : unit Pcoq.Gram.entry diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 3dfe308a5..b29af6680 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -18,7 +18,7 @@ open Genarg open Geninterp open Stdarg open Libnames -open Notation_term +open Notation_gram open Misctypes open Locus open Decl_kinds diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 799a52cc8..5d2a99618 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -17,7 +17,7 @@ open Names open Misctypes open Environ open Constrexpr -open Notation_term +open Notation_gram open Tacexpr type 'a grammar_tactic_prod_item_expr = @@ -153,5 +153,5 @@ val pr_value : tolerability -> Val.t -> Pp.t val ltop : tolerability -val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) -> +val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) -> 'a Genprint.top_printer diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index a1d8b087e..50bf687b1 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -112,7 +112,7 @@ let subst_glob_constr_or_pattern subst (bvars,c,p) = (bvars,subst_glob_constr subst c,subst_pattern subst p) let subst_redexp subst = - Miscops.map_red_expr_gen + Redops.map_red_expr_gen (subst_glob_constr subst) (subst_evaluable subst) (subst_glob_constr_or_pattern subst) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 138b42e54..fbfbdb110 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -64,7 +64,7 @@ DECLARE PLUGIN "ssreflect_plugin" * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; -let tacltop = (5,Notation_term.E) +let tacltop = (5,Notation_gram.E) let pr_ssrtacarg _ _ prt = prt tacltop ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 2ac7c7e26..7cd3751ce 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -14,11 +14,11 @@ open Ltac_plugin val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type -val pr_ssrtacarg : 'a -> 'b -> (Notation_term.tolerability -> 'c) -> 'c +val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type -val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c -> 'd +val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 8e3c33ff7..b1ab2d2b7 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -629,6 +629,10 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = env evdref scl ar.template_level (ctx,ar.template_param_levels) in !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl)) +let type_of_projection_constant env (p,u) = + let pb = lookup_projection p env in + Vars.subst_instance_constr u pb.proj_type + let type_of_projection_knowing_arg env sigma p c ty = let c = EConstr.Unsafe.to_constr c in let IndType(pars,realargs) = @@ -637,7 +641,7 @@ let type_of_projection_knowing_arg env sigma p c ty = raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type") in let (_,u), pars = dest_ind_family pars in - substl (c :: List.rev pars) (Typeops.type_of_projection_constant env (p,u)) + substl (c :: List.rev pars) (type_of_projection_constant env (p,u)) (***********************************************) (* Guard condition *) diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 1b536bfda..1697e54ab 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -10,7 +10,6 @@ open Util open Misctypes -open Genredexpr (** Mapping [cast_type] *) @@ -42,26 +41,6 @@ let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with | IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2 | _ -> false -(** Mapping [red_expr_gen] *) - -let map_flags f flags = - { flags with rConst = List.map f flags.rConst } - -let map_occs f (occ,e) = (occ,f e) - -let map_red_expr_gen f g h = function - | Fold l -> Fold (List.map f l) - | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l) - | Simpl (flags,occs_o) -> - Simpl (map_flags g flags, Option.map (map_occs (map_union g h)) occs_o) - | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l) - | Cbv flags -> Cbv (map_flags g flags) - | Lazy flags -> Lazy (map_flags g flags) - | CbvVm occs_o -> CbvVm (Option.map (map_occs (map_union g h)) occs_o) - | CbvNative occs_o -> CbvNative (Option.map (map_occs (map_union g h)) occs_o) - | Cbn flags -> Cbn (map_flags g flags) - | ExtraRedExpr _ | Red _ | Hnf as x -> x - (** Mapping bindings *) let map_explicit_bindings f l = diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli index 1d4504541..6a84fb9eb 100644 --- a/pretyping/miscops.mli +++ b/pretyping/miscops.mli @@ -9,7 +9,6 @@ (************************************************************************) open Misctypes -open Genredexpr (** Mapping [cast_type] *) @@ -25,11 +24,6 @@ val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool val intro_pattern_naming_eq : intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool -(** Mapping [red_expr_gen] *) - -val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) -> - ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen - (** Mapping bindings *) val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index c48decdb0..3d9b5d3cf 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -16,13 +16,10 @@ Evarsolve Recordops Evarconv Typing -Constrexpr -Genredexpr Miscops Glob_term Ltac_pretype Glob_ops -Redops Pattern Patternops Constr_matching @@ -37,4 +34,3 @@ Indrec Cases Pretyping Unification -Univdecls diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 89c5d7e7b..a1ac53c73 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -12,7 +12,6 @@ open Names open EConstr open Environ -open Constrexpr (*i*) type contexts = Parameters | Properties @@ -20,7 +19,6 @@ type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr | UnboundMethod of GlobRef.t * Misctypes.lident (* Class name, method *) - | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *) exception TypeClassError of env * typeclass_error @@ -29,5 +27,3 @@ let typeclass_error env err = raise (TypeClassError (env, err)) let not_a_class env c = typeclass_error env (NotAClass c) let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id)) - -let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m)) diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 4aabc0aee..1003f2ae1 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -11,14 +11,12 @@ open Names open EConstr open Environ -open Constrexpr type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr | UnboundMethod of GlobRef.t * Misctypes.lident (** Class name, method *) - | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *) exception TypeClassError of env * typeclass_error @@ -26,5 +24,3 @@ val not_a_class : env -> constr -> 'a val unbound_method : env -> GlobRef.t -> Misctypes.lident -> 'a -val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a - diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml deleted file mode 100644 index 8864be576..000000000 --- a/pretyping/univdecls.ml +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open CErrors - -(** Local universes and constraints declarations *) -type universe_decl = - (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl - -let default_univ_decl = - let open Misctypes in - { univdecl_instance = []; - univdecl_extensible_instance = true; - univdecl_constraints = Univ.Constraint.empty; - univdecl_extensible_constraints = true } - -let interp_univ_constraints env evd cstrs = - let interp (evd,cstrs) (u, d, u') = - let ul = Pretyping.interp_known_glob_level evd u in - let u'l = Pretyping.interp_known_glob_level evd u' in - let cstr = (ul,d,u'l) in - let cstrs' = Univ.Constraint.add cstr cstrs in - try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in - evd, cstrs' - with Univ.UniverseInconsistency e -> - user_err ~hdr:"interp_constraint" - (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e) - in - List.fold_left interp (evd,Univ.Constraint.empty) cstrs - -let interp_univ_decl env decl = - let open Misctypes in - let pl : lident list = decl.univdecl_instance in - let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in - let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in - let decl = { univdecl_instance = pl; - univdecl_extensible_instance = decl.univdecl_extensible_instance; - univdecl_constraints = cstrs; - univdecl_extensible_constraints = decl.univdecl_extensible_constraints } - in evd, decl - -let interp_univ_decl_opt env l = - match l with - | None -> Evd.from_env env, default_univ_decl - | Some decl -> interp_univ_decl env decl diff --git a/printing/genprint.ml b/printing/genprint.ml index 1bb7838a4..fa53a8794 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -19,15 +19,15 @@ open Geninterp (* Printing generic values *) type 'a with_level = - { default_already_surrounded : Notation_term.tolerability; - default_ensure_surrounded : Notation_term.tolerability; + { default_already_surrounded : Notation_gram.tolerability; + default_ensure_surrounded : Notation_gram.tolerability; printer : 'a } type printer_result = | PrinterBasic of (unit -> Pp.t) -| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level +| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level -type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t type top_printer_result = | TopPrinterBasic of (unit -> Pp.t) diff --git a/printing/genprint.mli b/printing/genprint.mli index fd5dd7259..1a31025a9 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -13,15 +13,15 @@ open Genarg type 'a with_level = - { default_already_surrounded : Notation_term.tolerability; - default_ensure_surrounded : Notation_term.tolerability; + { default_already_surrounded : Notation_gram.tolerability; + default_ensure_surrounded : Notation_gram.tolerability; printer : 'a } type printer_result = | PrinterBasic of (unit -> Pp.t) -| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level +| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level -type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t type top_printer_result = | TopPrinterBasic of (unit -> Pp.t) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 2a5f38697..e877b3c63 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -19,7 +19,7 @@ open Constr open Libnames open Pputils open Ppextend -open Notation_term +open Notation_gram open Constrexpr open Constrexpr_ops open Decl_kinds @@ -88,8 +88,6 @@ let tag_var = tag Tag.variable | Numeral (_,b) -> if b then lposint else lnegint | String _ -> latom - open Notation - let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps = let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists in let pop r = let a = List.hd !r in r := List.tl !r; a in diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 127c4471c..05f48ec79 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -16,7 +16,7 @@ open Libnames open Constrexpr open Names open Misctypes -open Notation_term +open Notation_gram val prec_less : precedence -> tolerability -> bool diff --git a/printing/printer.mli b/printing/printer.mli index ac0e12979..7a8b963d2 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -36,7 +36,7 @@ val pr_constr : constr -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t -val pr_constr_n_env : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t +val pr_constr_n_env : env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t (** Same, but resilient to [Nametab] errors. Prints fully-qualified names when [shortest_qualid_of_global] has failed. Prints "??" @@ -57,7 +57,7 @@ val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t val pr_leconstr : EConstr.t -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] -val pr_econstr_n_env : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t +val pr_econstr_n_env : env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t val pr_etype_env : env -> evar_map -> EConstr.types -> Pp.t val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t @@ -87,7 +87,7 @@ val pr_type_env : env -> evar_map -> types -> Pp.t val pr_type : types -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] -val pr_closed_glob_n_env : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t +val pr_closed_glob_n_env : env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t val pr_closed_glob : closed_glob_constr -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 805635dfa..7b7973224 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -24,7 +24,7 @@ open Decl_kinds proof of mutually dependent theorems) *) val start_proof : - Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> + Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> ?init_tac:unit Proofview.tactic -> Proof_global.proof_terminator -> unit diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index d5cb5b09f..3abdd129e 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -97,7 +97,7 @@ type pstate = { proof : Proof.t; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; - universe_decl: Univdecls.universe_decl; + universe_decl: UState.universe_decl; } type t = pstate list @@ -238,13 +238,6 @@ let activate_proof_mode mode = let disactivate_current_proof_mode () = CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()) -let default_universe_decl = - let open Misctypes in - { univdecl_instance = []; - univdecl_extensible_instance = true; - univdecl_constraints = Univ.Constraint.empty; - univdecl_extensible_constraints = true } - (** [start_proof sigma id pl str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this @@ -253,7 +246,7 @@ let default_universe_decl = end of the proof to close the proof. The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -let start_proof sigma id ?(pl=default_universe_decl) str goals terminator = +let start_proof sigma id ?(pl=UState.default_univ_decl) str goals terminator = let initial_state = { pid = id; terminator = CEphemeron.create terminator; @@ -265,7 +258,7 @@ let start_proof sigma id ?(pl=default_universe_decl) str goals terminator = universe_decl = pl } in push initial_state pstates -let start_dependent_proof id ?(pl=default_universe_decl) str goals terminator = +let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator = let initial_state = { pid = id; terminator = CEphemeron.create terminator; diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index de4cec488..0141cacb9 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -71,14 +71,14 @@ val apply_terminator : proof_terminator -> proof_ending -> unit evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) val start_proof : - Evd.evar_map -> Names.Id.t -> ?pl:Univdecls.universe_decl -> + Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between initial goals. *) val start_dependent_proof : - Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> + Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> Proofview.telescope -> proof_terminator -> unit (** Update the proofs global environment after a side-effecting command @@ -130,7 +130,7 @@ val set_used_variables : val get_used_variables : unit -> Context.Named.t option (** Get the universe declaration associated to the current proof. *) -val get_universe_decl : unit -> Univdecls.universe_decl +val get_universe_decl : unit -> UState.universe_decl module V82 : sig val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list * diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index f9e7bbfac..03ebc3275 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -263,7 +263,7 @@ let subst_mps subst c = EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c)) let subst_red_expr subs = - Miscops.map_red_expr_gen + Redops.map_red_expr_gen (subst_mps subs) (Mod_subst.subst_evaluable_reference subs) (Patternops.subst_pattern subs) diff --git a/tactics/hints.ml b/tactics/hints.ml index e32807f4b..a86103d57 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -294,15 +294,15 @@ let strip_params env sigma c = | App (f, args) -> (match EConstr.kind sigma f with | Const (p,_) -> - let cb = lookup_constant p env in - (match cb.Declarations.const_proj with - | Some pb -> - let n = pb.Declarations.proj_npars in - if Array.length args > n then - mkApp (mkProj (Projection.make p false, args.(n)), - Array.sub args (n+1) (Array.length args - (n + 1))) - else c - | None -> c) + let p = Projection.make p false in + (match lookup_projection p env with + | pb -> + let n = pb.Declarations.proj_npars in + if Array.length args > n then + mkApp (mkProj (p, args.(n)), + Array.sub args (n+1) (Array.length args - (n + 1))) + else c + | exception Not_found -> c) | _ -> c) | _ -> c diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli index 2c748f9c9..7bce57789 100644 --- a/tactics/term_dnet.mli +++ b/tactics/term_dnet.mli @@ -26,7 +26,7 @@ open Mod_subst The results returned here are perfect, since post-filtering is done inside here. - See lib/dnet.mli for more details. + See tactics/dnet.mli for more details. *) (** Identifiers to store (right hand side of the association) *) diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py index 32c52c7a1..c6af2ff1f 100755 --- a/tools/make-both-single-timing-files.py +++ b/tools/make-both-single-timing-files.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +#!/usr/bin/env python2 import sys from TimeFileMaker import * diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py index f730a8d6b..643429679 100755 --- a/tools/make-both-time-files.py +++ b/tools/make-both-time-files.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +#!/usr/bin/env python2 import sys from TimeFileMaker import * diff --git a/tools/make-one-time-file.py b/tools/make-one-time-file.py index e66136df9..c9905249e 100755 --- a/tools/make-one-time-file.py +++ b/tools/make-one-time-file.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +#!/usr/bin/env python2 import sys from TimeFileMaker import * diff --git a/vernac/classes.ml b/vernac/classes.ml index c82208980..946a7bb32 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -77,8 +77,8 @@ let existing_instance glob g info = ~hdr:"declare_instance" (Pp.str "Constant does not build instances of a declared type class.") -let mismatched_params env n m = mismatched_ctx_inst env Parameters n m -let mismatched_props env n m = mismatched_ctx_inst env Properties n m +let mismatched_params env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Parameters n m +let mismatched_props env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Properties n m (* Declare everything in the parameters as implicit, and the class instance as well *) @@ -137,7 +137,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in let ({CAst.loc;v=instid}, pl) = instid in - let sigma, decl = Univdecls.interp_univ_decl_opt env pl in + let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in let tclass, ids = match bk with | Decl_kinds.Implicit -> diff --git a/vernac/classes.mli b/vernac/classes.mli index 631da8400..eea2a211d 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -32,7 +32,7 @@ val declare_instance_constant : Impargs.manual_explicitation list -> (** implicits *) ?hook:(GlobRef.t -> unit) -> Id.t -> (** name *) - Univdecls.universe_decl -> + UState.universe_decl -> bool -> (* polymorphic *) Evd.evar_map -> (* Universes *) Constr.t -> (** body *) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 492ae1d9b..a8ac52846 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -136,7 +136,7 @@ let do_assumptions kind nl l = let open Context.Named.Declaration in let env = Global.env () in let udecl, l = process_assumptions_udecls kind l in - let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in + let sigma, udecl = interp_univ_decl_opt env udecl in let l = if pi2 kind (* poly *) then (* Separate declarations so that A B : Type puts A and B in different levels. *) diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 2d4bd6779..f55c852c0 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -65,7 +65,7 @@ let interp_definition pl bl poly red_option c ctypopt = let open EConstr in let env = Global.env() in (* Explicitly bound universes and constraints *) - let evd, decl = Univdecls.interp_univ_decl_opt env pl in + let evd, decl = Constrexpr_ops.interp_univ_decl_opt env pl in (* Build the parameters *) let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in (* Build the type *) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 6f81c4575..7f1c902c0 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -29,4 +29,4 @@ val do_definition : program_mode:bool -> val interp_definition : universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * - Univdecls.universe_decl * Impargs.manual_implicits + UState.universe_decl * Impargs.manual_implicits diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index d996443d6..ea731b34c 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -173,11 +173,12 @@ let interp_recursive ~program_mode ~cofix fixl notations = | None , acc -> acc | x , None -> x | Some ls , Some us -> - let lsu = ls.univdecl_instance and usu = us.univdecl_instance in + let open UState in + let lsu = ls.univdecl_instance and usu = us.univdecl_instance in if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); Some us) fixl None in - let sigma, decl = Univdecls.interp_univ_decl_opt env all_universes in + let sigma, decl = interp_univ_decl_opt env all_universes in let sigma, (fixctxs, fiximppairs, fixannots) = on_snd List.split3 @@ List.fold_left_map (fun sigma -> interp_fix_context env sigma ~cofix) sigma fixl in diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 36c2993af..a6992a30b 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -49,7 +49,7 @@ val interp_recursive : structured_fixpoint_expr list -> decl_notation list -> (* env / signature / univs / evar_map *) - (Environ.env * EConstr.named_context * Univdecls.universe_decl * Evd.evar_map) * + (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (* names / defs / types *) (Id.t list * Constr.constr option list * Constr.types list) * (* ctx per mutual def / implicits / struct annotations *) @@ -74,19 +74,19 @@ type recursive_preentry = val interp_fixpoint : cofix:bool -> structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * Univdecls.universe_decl * UState.t * + recursive_preentry * UState.universe_decl * UState.t * (EConstr.rel_context * Impargs.manual_implicits * int option) list (** Registering fixpoints and cofixpoints in the environment *) (** [Not used so far] *) val declare_fixpoint : locality -> polymorphic -> - recursive_preentry * Univdecls.universe_decl * UState.t * + recursive_preentry * UState.universe_decl * UState.t * (Context.Rel.t * Impargs.manual_implicits * int option) list -> Proof_global.lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : locality -> polymorphic -> - recursive_preentry * Univdecls.universe_decl * UState.t * + recursive_preentry * UState.universe_decl * UState.t * (Context.Rel.t * Impargs.manual_implicits * int option) list -> decl_notation list -> unit diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 790e83dbe..101c14266 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -333,7 +333,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = List.iter check_param paramsl; let env0 = Global.env() in let pl = (List.hd indl).ind_univs in - let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in + let sigma, decl = interp_univ_decl_opt env0 pl in let sigma, (impls, ((env_params, ctx_params), userimpls)) = interp_context_evars env0 sigma paramsl in diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index f41e0fc44..a6d7fccf3 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -91,7 +91,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in Coqlib.check_required_library ["Coq";"Program";"Wf"]; let env = Global.env() in - let sigma, decl = Univdecls.interp_univ_decl_opt env pl in + let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars env sigma bl in let len = List.length binders_rel in let top_env = push_rel_context binders_rel env in diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 5f63d21c4..e7a308dda 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -8,14 +8,14 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open CErrors open Util -open Pcoq +open CErrors +open Names +open Libnames open Constrexpr -open Notation_term open Extend -open Libnames -open Names +open Notation_gram +open Pcoq (**********************************************************************) (* This determines (depending on the associativity of the current diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli index e15add10f..b0341e6a1 100644 --- a/vernac/egramcoq.mli +++ b/vernac/egramcoq.mli @@ -15,5 +15,5 @@ (** {5 Adding notations} *) -val extend_constr_grammar : Notation_term.one_notation_grammar -> unit +val extend_constr_grammar : Notation_gram.one_notation_grammar -> unit (** Add a term notation rule to the parsing system. *) diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index f68dcae26..504e7095b 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -66,6 +66,8 @@ let process_vernac_interp_error exn = match fst exn with wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te) | Typeclasses_errors.TypeClassError(env, te) -> wrap_vernac_error exn (Himsg.explain_typeclass_error env te) + | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) -> + wrap_vernac_error exn (Himsg.explain_mismatched_contexts e c l x) | InductiveError e -> wrap_vernac_error exn (Himsg.explain_inductive_error e) | Modops.ModuleTypingError e -> diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 index 6c7df8cfa..dd8149d0a 100644 --- a/vernac/g_vernac.ml4 +++ b/vernac/g_vernac.ml4 @@ -230,6 +230,7 @@ GEXTEND Gram ext = [ "+" -> true | -> false ]; "}" -> (l',ext) | ext = [ "}" -> true | "|}" -> false ] -> ([], ext) ] -> + let open UState in { univdecl_instance = l; univdecl_extensible_instance = ext; univdecl_constraints = fst cs; @@ -1147,8 +1148,8 @@ GEXTEND Gram [ [ "at"; n = level -> n ] ] ; constr_as_binder_kind: - [ [ "as"; IDENT "ident" -> AsIdent - | "as"; IDENT "pattern" -> AsIdentOrPattern - | "as"; IDENT "strict"; IDENT "pattern" -> AsStrictPattern ] ] + [ [ "as"; IDENT "ident" -> Notation_term.AsIdent + | "as"; IDENT "pattern" -> Notation_term.AsIdentOrPattern + | "as"; IDENT "strict"; IDENT "pattern" -> Notation_term.AsStrictPattern ] ] ; END diff --git a/vernac/himsg.ml b/vernac/himsg.ml index d4c5def6f..5d671ef52 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1033,7 +1033,6 @@ let explain_mismatched_contexts env c i j = let explain_typeclass_error env = function | NotAClass c -> explain_not_a_class env c | UnboundMethod (cid, id) -> explain_unbound_method env cid id - | MismatchedContextInstance (c,i,j) -> explain_mismatched_contexts env c i j (* Refiner errors *) diff --git a/vernac/himsg.mli b/vernac/himsg.mli index 0e20d18c6..1d3807502 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -25,6 +25,8 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t val explain_inductive_error : inductive_error -> Pp.t +val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Context.Rel.t -> Pp.t + val explain_typeclass_error : env -> typeclass_error -> Pp.t val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 3c7ede3c9..ce74f2344 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -436,7 +436,7 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook = let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in let decl = fst (List.hd thms) in - let evd, decl = Univdecls.interp_univ_decl_opt env0 (snd decl) in + let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) -> let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in @@ -456,7 +456,7 @@ let start_proof_com ?inference_hook kind thms hook = you look at the previous lines... *) let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in let () = - let open Misctypes in + let open UState in if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl) in diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 398f7d6d0..c9e4876ee 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -21,13 +21,13 @@ val call_hook : (** A hook start_proof calls on the type of the definition being started *) val set_start_hook : (EConstr.types -> unit) -> unit -val start_proof : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> +val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> unit declaration_hook -> unit -val start_proof_univs : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> +val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> unit declaration_hook) -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> @@ -39,7 +39,7 @@ val start_proof_com : unit declaration_hook -> unit val start_proof_with_initialization : - goal_kind -> Evd.evar_map -> Univdecls.universe_decl -> + goal_kind -> Evd.evar_map -> UState.universe_decl -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> (Id.t (* name of thm *) * (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index e038f54dd..2245e762f 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -15,6 +15,7 @@ open Names open Constrexpr open Constrexpr_ops open Notation_term +open Notation_gram open Notation_ops open Ppextend open Extend @@ -709,7 +710,7 @@ let error_parsing_incompatible_level ntn ntn' oldprec prec = pr_level ntn prec ++ str ".") type syntax_extension = { - synext_level : Notation_term.level; + synext_level : Notation_gram.level; synext_notation : notation; synext_notgram : notation_grammar; synext_unparsing : unparsing list; @@ -728,8 +729,8 @@ let check_and_extend_constr_grammar ntn rule = let ntn_for_grammar = rule.notgram_notation in if String.equal ntn ntn_for_grammar then raise Not_found; let prec = rule.notgram_level in - let oldprec = Notation.level_of_notation ntn_for_grammar in - if not (Notation.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; + let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in + if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; with Not_found -> Egramcoq.extend_constr_grammar rule @@ -738,16 +739,16 @@ let cache_one_syntax_extension se = let prec = se.synext_level in let onlyprint = se.synext_notgram.notgram_onlyprinting in try - let oldprec = Notation.level_of_notation ~onlyprint ntn in - if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; + let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in + if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; with Not_found -> if is_active_compat se.synext_compat then begin (* Reserve the notation level *) - Notation.declare_notation_level ntn prec ~onlyprint; + Notgram_ops.declare_notation_level ntn prec ~onlyprint; (* Declare the parsing rule *) if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules; (* Declare the notation rule *) - Notation.declare_notation_rule ntn + declare_notation_rule ntn ~extra:se.synext_extra (se.synext_unparsing, pi1 prec) se.synext_notgram end @@ -1061,7 +1062,7 @@ let find_precedence lev etyps symbols onlyprint = [],Option.get lev let check_curly_brackets_notation_exists () = - try let _ = Notation.level_of_notation "{ _ }" in () + try let _ = Notgram_ops.level_of_notation "{ _ }" in () with Not_found -> user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\ specially and require that the notation \"{ _ }\" is already reserved.") @@ -1274,10 +1275,10 @@ exception NoSyntaxRule let recover_notation_syntax ntn = try - let prec = Notation.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in - let pp_rule,_ = Notation.find_notation_printing_rule ntn in - let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in - let pa_rule = Notation.find_notation_parsing_rules ntn in + let prec = Notgram_ops.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in + let pp_rule,_ = find_notation_printing_rule ntn in + let pp_extra_rules = find_notation_extra_printing_rules ntn in + let pa_rule = find_notation_parsing_rules ntn in { synext_level = prec; synext_notation = ntn; synext_notgram = pa_rule; @@ -1444,7 +1445,7 @@ let add_notation_extra_printing_rule df k v = let notk = let _,_, symbs = analyze_notation_tokens ~onlyprint:true df in make_notation_key symbs in - Notation.add_notation_extra_printing_rule notk k v + add_notation_extra_printing_rule notk k v (* Infix notations *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 6ef8294df..1a3b1f39b 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -308,7 +308,7 @@ type program_info_aux = { prg_body: constr; prg_type: constr; prg_ctx: UState.t; - prg_univdecl: Univdecls.universe_decl; + prg_univdecl: UState.universe_decl; prg_obligations: obligations; prg_deps : Id.t list; prg_fixkind : fixpoint_kind option ; @@ -1099,7 +1099,7 @@ let show_term n = Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ Printer.pr_constr_env env sigma prg.prg_body) -let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl) +let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls = let sign = Decls.initialize_named_context_for_proof () in @@ -1119,7 +1119,7 @@ let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl) | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res | _ -> res) -let add_mutual_definitions l ctx ?(univdecl=Univdecls.default_univ_decl) ?tactic +let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind = let sign = Decls.initialize_named_context_for_proof () in diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 4b6165fb1..b1eaf51ac 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -54,7 +54,7 @@ val default_tactic : unit Proofview.tactic ref val add_definition : Names.Id.t -> ?term:constr -> types -> UState.t -> - ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *) + ?univdecl:UState.universe_decl -> (* Universe binders and constraints *) ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> @@ -72,7 +72,7 @@ val add_mutual_definitions : (Names.Id.t * constr * types * (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list -> UState.t -> - ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *) + ?univdecl:UState.universe_decl -> (* Universe binders and constraints *) ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(constr -> constr) -> diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 3655947a5..7aff758e9 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -55,7 +55,7 @@ open Pputils (if extensible then str"+" else mt()) let pr_universe_decl l = - let open Misctypes in + let open UState in match l with | None -> mt () | Some l -> @@ -102,7 +102,7 @@ open Pputils | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level" - let pr_constr_as_binder_kind = function + let pr_constr_as_binder_kind = let open Notation_term in function | AsIdent -> keyword "as ident" | AsIdentOrPattern -> keyword "as pattern" | AsStrictPattern -> keyword "as strict pattern" diff --git a/vernac/record.ml b/vernac/record.ml index 5ff118473..e6a3afe4e 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -102,7 +102,7 @@ let binders_of_decls = List.map binder_of_decl let typecheck_params_and_fields finite def id poly pl t ps nots fs = let env0 = Global.env () in - let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in + let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in let _ = let error bk {CAst.loc; v=name} = match bk, name with diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 4ff9d105b..74355e1a7 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -207,7 +207,7 @@ type proof_expr = type syntax_modifier = | SetItemLevel of string list * Extend.production_level - | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option + | SetItemLevelAsBinder of string list * Notation_term.constr_as_binder_kind * Extend.production_level option | SetLevel of int | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key |