diff options
75 files changed, 2450 insertions, 1947 deletions
diff --git a/.travis.yml b/.travis.yml index 83a4e7fdda..54e7754f21 100644 --- a/.travis.yml +++ b/.travis.yml @@ -183,6 +183,7 @@ matrix: - if: NOT (type = pull_request) os: osx + osx_image: xcode7.3 env: - TEST_TARGET="" - COMPILER="4.02.3" diff --git a/API/API.ml b/API/API.ml index 378c03ee4f..081ac2bb28 100644 --- a/API/API.ml +++ b/API/API.ml @@ -267,7 +267,9 @@ module Metasyntax = Metasyntax module Search = Search (* module Indschemes *) module Obligations = Obligations -module Command = Command +module ComDefinition = ComDefinition +module ComInductive = ComInductive +module ComFixpoint = ComFixpoint module Classes = Classes (* module Record *) (* module Assumptions *) diff --git a/API/API.mli b/API/API.mli index 8f46a58321..a69766901b 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4620,6 +4620,9 @@ end module Constrintern : sig + + open Evd + type ltac_sign = { ltac_vars : Names.Id.Set.t; ltac_bound : Names.Id.Set.t; @@ -4635,11 +4638,11 @@ sig | Variable type internalization_env = var_internalization_data Names.Id.Map.t - val interp_constr_evars : Environ.env -> Evd.evar_map ref -> - ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.constr + val interp_constr_evars : Environ.env -> evar_map -> + ?impls:internalization_env -> Constrexpr.constr_expr -> evar_map * EConstr.constr - val interp_type_evars : Environ.env -> Evd.evar_map ref -> - ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types + val interp_type_evars : Environ.env -> Evd.evar_map -> + ?impls:internalization_env -> Constrexpr.constr_expr -> evar_map * EConstr.types val empty_ltac_sign : ltac_sign val intern_gen : Pretyping.typing_constraint -> Environ.env -> @@ -4657,10 +4660,12 @@ sig val locate_reference : Libnames.qualid -> Globnames.global_reference val interp_type : Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Constr.types Evd.in_evar_universe_context + val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> - Environ.env -> Evd.evar_map ref -> Constrexpr.local_binder_expr list -> - internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits) + Environ.env -> Evd.evar_map -> Constrexpr.local_binder_expr list -> + evar_map * (internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits)) + val compute_internalization_data : Environ.env -> var_internalization_type -> Constr.types -> Impargs.manual_explicitation list -> var_internalization_data val empty_internalization_env : internalization_env @@ -6045,21 +6050,53 @@ sig val show_term : Names.Id.t option -> Pp.t end -module Command : +module ComDefinition : +sig + val do_definition : + program_mode:bool -> + Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option -> + Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> + Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit +end + +module ComFixpoint : sig + open Names open Constrexpr - open Vernacexpr type structured_fixpoint_expr = { fix_name : Id.t; - fix_univs : universe_decl_expr option; + fix_univs : Vernacexpr.universe_decl_expr option; fix_annot : Id.t Loc.located option; fix_binders : local_binder_expr list; fix_body : constr_expr option; fix_type : constr_expr } + type recursive_preentry = Names.Id.t list * Constr.t option list * Constr.types list + + val interp_fixpoint : + cofix:bool -> + structured_fixpoint_expr list -> Vernacexpr.decl_notation list -> + recursive_preentry * Univdecls.universe_decl * UState.t * + (EConstr.rel_context * Impargs.manual_implicits * int option) list + + val extract_fixpoint_components : bool -> + (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> + structured_fixpoint_expr list * Vernacexpr.decl_notation list + + val do_fixpoint : + Decl_kinds.locality -> Decl_kinds.polymorphic -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit + +end + +module ComInductive : +sig + open Names + open Constrexpr + open Vernacexpr + type structured_one_inductive_expr = { ind_name : Id.t; ind_univs : universe_decl_expr option; @@ -6070,30 +6107,12 @@ sig type structured_inductive_expr = local_binder_expr list * structured_one_inductive_expr list - type recursive_preentry = Names.Id.t list * Constr.t option list * Constr.types list - type one_inductive_impls val do_mutual_inductive : (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> Decl_kinds.private_flag -> Declarations.recursivity_kind -> unit - val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option -> - Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> - Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit - - val do_fixpoint : - Decl_kinds.locality -> Decl_kinds.polymorphic -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit - - val extract_fixpoint_components : bool -> - (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - structured_fixpoint_expr list * Vernacexpr.decl_notation list - - val interp_fixpoint : - structured_fixpoint_expr list -> Vernacexpr.decl_notation list -> - recursive_preentry * Univdecls.universe_decl * UState.t * - (EConstr.rel_context * Impargs.manual_implicits * int option) list - val extract_mutual_inductive_declaration_components : (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> structured_inductive_expr * Libnames.qualid list * Vernacexpr.decl_notation list @@ -6117,6 +6136,7 @@ sig ?abstract:bool -> ?global:bool -> ?refine:bool -> + program_mode:bool -> Decl_kinds.polymorphic -> Constrexpr.local_binder_expr list -> Vernacexpr.typeclass_constraint -> @@ -42,6 +42,8 @@ Vernacular Commands - The deprecated Coercion Local, Open Local Scope, Notation Local syntax was removed. Use Local as a prefix instead. +- For the Extraction Language command, "OCaml" is spelled correctly. + The older "Ocaml" is still accepted, but deprecated. Universes @@ -55,6 +57,14 @@ Checker - The checker now accepts filenames in addition to logical paths. +Changes from 8.7.0 to 8.7.1 +=========================== + +Compatibility with OCaml 4.06.0. + +Many bug fixes, documentation improvements, and user message improvements (for +details see the 8.7.1 milestone at https://github.com/coq/coq/milestone/10?closed=1). + Changes from 8.7+beta2 to 8.7.0 =============================== diff --git a/Makefile.build b/Makefile.build index 940943c41f..cbc1cbaab0 100644 --- a/Makefile.build +++ b/Makefile.build @@ -147,8 +147,14 @@ endif # For creating the missing .d, make will recursively build things like # coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d). +VDFILE := .vfiles +MLDFILE := .mlfiles +PLUGMLDFILE := plugins/.mlfiles +MLLIBDFILE := .mllibfiles +PLUGMLLIBDFILE := plugins/.mllibfiles + DEPENDENCIES := \ - $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(MLPACKFILES) $(CFILES) $(VFILES)) + $(addsuffix .d, $(MLDFILE) $(MLLIBDFILE) $(PLUGMLDFILE) $(PLUGMLLIBDFILE) $(CFILES) $(VDFILE)) -include $(DEPENDENCIES) @@ -189,7 +195,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) COQOPTS=$(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile -LOCALINCLUDES=$(if $(filter plugins/%,$<),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS))) +LOCALINCLUDES=$(if $(filter plugins/%,$@),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS))) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) @@ -197,7 +203,7 @@ OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS) -DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$<),, -I ide -I ide/utils) +DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$@),, -I ide -I ide/utils) # On MacOS, the binaries are signed, except our private ones ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin) @@ -301,7 +307,7 @@ kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h -e '/^}/q' $< $(TOTARGET) kernel/copcodes.ml: kernel/byterun/coq_instruct.h - sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' $< | \ + tr -d "\r" < $< | sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' | \ awk -f kernel/make-opcodes $(TOTARGET) %.o: %.c @@ -671,21 +677,24 @@ plugins/%.cmx: plugins/%.ml # Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12) OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack -%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) - $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" $(TOTARGET) +MAINMLFILES := $(filter-out checker/% plugins/%, $(MLFILES) $(MLIFILES)) +MAINMLLIBFILES := $(filter-out checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES)) + +$(MLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLFILES) $(D_DEPEND_AFTER_SRC) $(GENFILES) + $(SHOW)'OCAMLDEP MLFILES MLIFILES' + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(MAINMLFILES) $(TOTARGET) -%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) - $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" $(TOTARGET) +$(MLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLLIBFILES) $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP MLLIBFILES MLPACKFILES' + $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) $(MAINMLLIBFILES) $(TOTARGET) -%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) +$(PLUGMLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter plugins/%, $(MLFILES) $(MLIFILES)) $(D_DEPEND_AFTER_SRC) $(GENFILES) + $(SHOW)'OCAMLDEP plugins/MLFILES plugins/MLIFILES' + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(filter plugins/%, $(MLFILES) $(MLIFILES)) $(TOTARGET) -%.mlpack.d: $(D_DEPEND_BEFORE_SRC) %.mlpack $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) +$(PLUGMLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter plugins/%, $(MLLIBFILES) $(MLPACKFILES)) $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP plugins/MLLIBFILES plugins/MLPACKFILES' + $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) $(filter plugins/%, $(MLLIBFILES) $(MLPACKFILES)) $(TOTARGET) ########################################################################### # Compilation of .v files @@ -757,9 +766,9 @@ endif # Dependencies of .v files -%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) "$<" $(TOTARGET) +$(VDFILE).d: $(D_DEPEND_BEFORE_SRC) $(VFILES) $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) + $(SHOW)'COQDEP VFILES' + $(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) $(VFILES) $(TOTARGET) ########################################################################### diff --git a/Makefile.checker b/Makefile.checker index b14f705bed..7e0f588759 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -26,6 +26,12 @@ CHKLIBS:= -I config -I lib -I checker # The rules +CHECKMLDFILE := checker/.mlfiles +CHECKMLLIBFILE := checker/.mllibfiles + +CHECKERDEPS := $(addsuffix .d, $(CHECKMLDFILE) $(CHECKMLLIBFILE)) +-include $(CHECKERDEPS) + ifeq ($(BEST),opt) $(CHICKEN): checker/check.cmxa checker/main.ml $(SHOW)'OCAMLOPT -o $@' @@ -49,17 +55,13 @@ checker/check.cmxa: checker/check.mllib | md5chk $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) -checker/%.ml.d: checker/%.ml - $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) "$<" $(TOTARGET) - -checker/%.mli.d: checker/%.mli - $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) "$<" $(TOTARGET) +$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES)) + $(SHOW)'OCAMLDEP checker/MLFILES checker/MLIFILES' + $(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(filter checker/%, $(MLFILES) $(MLIFILES)) $(TOTARGET) -checker/%.mllib.d: checker/%.mllib | $(OCAMLLIBDEP) - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) "$<" $(TOTARGET) +$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) | $(OCAMLLIBDEP) + $(SHOW)'OCAMLLIBDEP checker/MLLIBFILES checker/MLPACKFILES' + $(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) $(TOTARGET) checker/%.cmi: checker/%.mli $(SHOW)'OCAMLC $<' @@ -75,8 +77,9 @@ checker/%.cmx: checker/%.ml md5chk: $(SHOW)'MD5SUM cic.mli' - $(HIDE)if grep -q `$(MD5SUM) checker/cic.mli` checker/values.ml; \ - then true; else echo "Error: outdated checker/values.ml"; false; fi + $(HIDE)v=`tr -d "\r" < checker/cic.mli | $(MD5SUM) | sed -n -e 's/ .*//' -e '/^/p'`; \ + if grep -q "$$v" checker/values.ml; \ + then true; else echo "Error: outdated checker/values.ml: $$v" >&2; false; fi .PHONY: md5chk diff --git a/dev/base_include b/dev/base_include index 1da5e3ed18..d7059fe74f 100644 --- a/dev/base_include +++ b/dev/base_include @@ -170,7 +170,7 @@ open Eqschemes open ExplainErr open Class -open Command +open ComDefinition open Indschemes open Ind_tables open Auto_ind_decl diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index f91b301b8c..665d541761 100644 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -345,7 +345,7 @@ IF "%COQREGTESTING%" == "Y" ( SET "EXTRAPACKAGES= " IF NOT "%APPVEYOR%" == "True" ( - SET EXTRAPACKAGES="-P wget,curl,git,gcc-core,gcc-g++,automake1.5" + SET EXTRAPACKAGES=-P wget,curl,git,gcc-core,gcc-g++,automake1.5 ) IF "%RUNSETUP%"=="Y" ( diff --git a/dev/ci/user-overlays/06217-coqdep-at-once.sh b/dev/ci/user-overlays/06217-coqdep-at-once.sh new file mode 100644 index 0000000000..68e1901f7f --- /dev/null +++ b/dev/ci/user-overlays/06217-coqdep-at-once.sh @@ -0,0 +1,3 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6217" ] || [ "$TRAVIS_BRANCH" = "coqdep-at-once" ]; then + UniMath_CI_GITURL=https://github.com/SkySkimmer/UniMath.git +fi diff --git a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh b/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh new file mode 100644 index 0000000000..c0dcf79e1d --- /dev/null +++ b/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6392" ] || [ "$TRAVIS_BRANCH" = "econstr+fix_class" ]; then + Equations_CI_BRANCH=econstr+fix_class + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git +fi diff --git a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh new file mode 100644 index 0000000000..8aea7dee3a --- /dev/null +++ b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6413" ] || [ "$TRAVIS_BRANCH" = "interp+less_impstyle_p2" ]; then + Equations_CI_BRANCH=interp+less_impstyle_p2 + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index c69be4f4de..01aa6b599b 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -46,6 +46,11 @@ We changed the type of the following functions: - `Global.body_of_constant`: same as above. +- `Constrinterp.*` generally, many functions that used to take an + `evar_map ref` have been now switched to functions that will work in + a functional way. The old style of passing `evar_map`s as references + is not supported anymore. + We have changed the representation of the following types: - `Lib.object_prefix` is now a record instead of a nested tuple. diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex index 7ad895f9d8..376ef031db 100644 --- a/doc/refman/Cases.tex +++ b/doc/refman/Cases.tex @@ -280,6 +280,18 @@ Fail Check end). \end{coq_example} +The option {\tt Set Asymmetric Patterns} \optindex{Asymmetric Patterns} +(off by default) removes parameters from constructors in patterns: +\begin{coq_example} + Set Asymmetric Patterns. + Check (fun l:List nat => + match l with + | nil => nil + | cons _ l' => l' + end) + Unset Asymmetric Patterns. +\end{coq_example} + \paragraph{Implicit arguments in patterns} By default, implicit arguments are omitted in patterns. So we write: diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index cab6739998..6e76d04e77 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -526,14 +526,14 @@ potentially more expensive proof-search (i.e. more useless backtracking). \subsection{\tt Set Typeclass Resolution After Apply} -\optindex{Typeclasses Resolution After Apply} +\optindex{Typeclass Resolution After Apply} \emph{Deprecated since 8.6} This option (off by default in Coq 8.6 and 8.5) controls the resolution of typeclass subgoals generated by the {\tt apply} tactic. \subsection{\tt Set Typeclass Resolution For Conversion} -\optindex{Typeclasses Resolution For Conversion} +\optindex{Typeclass Resolution For Conversion} This option (on by default) controls the use of typeclass resolution when a unification problem cannot be solved during diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 79060e6062..cff7be3e96 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -1,4 +1,4 @@ -\achapter{Extraction of programs in Objective Caml and Haskell} +\achapter{Extraction of programs in OCaml and Haskell} %HEVEA\cutname{extraction.html} \label{Extraction} \aauthor{Jean-Christophe Filliâtre and Pierre Letouzey} @@ -95,12 +95,12 @@ one monolithic file or one file per \Coq\ library. \begin{description} \item {\tt Extraction TestCompile} \qualid$_1$ \dots\ \qualid$_n$. ~\par All the globals (or modules) \qualid$_1$ \dots\ \qualid$_n$ and all - their dependencies are extracted to a temporary Ocaml file, just as in + their dependencies are extracted to a temporary {\ocaml} file, just as in {\tt Extraction "{\em file}"}. Then this temporary file and its - signature are compiled with the same Ocaml compiler used to built - \Coq. This command succeeds only if the extraction and the Ocaml + signature are compiled with the same {\ocaml} compiler used to built + \Coq. This command succeeds only if the extraction and the {\ocaml} compilation succeed (and it fails if the current target language - of the extraction is not Ocaml). + of the extraction is not {\ocaml}). \end{description} \asection{Extraction options} @@ -109,26 +109,26 @@ one monolithic file or one file per \Coq\ library. \comindex{Extraction Language} The ability to fix target language is the first and more important -of the extraction options. Default is Ocaml. +of the extraction options. Default is {\ocaml}. \begin{description} -\item {\tt Extraction Language Ocaml}. +\item {\tt Extraction Language OCaml}. \item {\tt Extraction Language Haskell}. \item {\tt Extraction Language Scheme}. \end{description} \asubsection{Inlining and optimizations} -Since Objective Caml is a strict language, the extracted code has to +Since {\ocaml} is a strict language, the extracted code has to be optimized in order to be efficient (for instance, when using induction principles we do not want to compute all the recursive calls but only the needed ones). So the extraction mechanism provides an automatic optimization routine that will be called each time the user -want to generate Ocaml programs. The optimizations can be split in two +want to generate {\ocaml} programs. The optimizations can be split in two groups: the type-preserving ones -- essentially constant inlining and reductions -- and the non type-preserving ones -- some function abstractions of dummy types are removed when it is deemed safe in order to have more elegant types. Therefore some constants may not appear in the -resulting monolithic Ocaml program. In the case of modular extraction, +resulting monolithic {\ocaml} program. In the case of modular extraction, even if some inlining is done, the inlined constant are nevertheless printed, to ensure session-independent programs. @@ -367,15 +367,15 @@ As for {\tt Extract Inductive}, this command should be used with care: \item Extracting an inductive type to a pre-existing ML inductive type is quite sound. But extracting to a general type (by providing an ad-hoc pattern-matching) will often \emph{not} be fully rigorously -correct. For instance, when extracting {\tt nat} to Ocaml's {\tt +correct. For instance, when extracting {\tt nat} to {\ocaml}'s {\tt int}, it is theoretically possible to build {\tt nat} values that are -larger than Ocaml's {\tt max\_int}. It is the user's responsibility to +larger than {\ocaml}'s {\tt max\_int}. It is the user's responsibility to be sure that no overflow or other bad events occur in practice. \item Translating an inductive type to an ML type does \emph{not} magically improve the asymptotic complexity of functions, even if the ML type is an efficient representation. For instance, when extracting -{\tt nat} to Ocaml's {\tt int}, the function {\tt mult} stays +{\tt nat} to {\ocaml}'s {\tt int}, the function {\tt mult} stays quadratic. It might be interesting to associate this translation with some specific {\tt Extract Constant} when primitive counterparts exist. \end{itemize} @@ -402,7 +402,7 @@ Extract Inductive prod => "(*)" [ "(,)" ]. \end{coq_example} \noindent As an example of translation to a non-inductive datatype, let's turn -{\tt nat} into Ocaml's {\tt int} (see caveat above): +{\tt nat} into {\ocaml}'s {\tt int} (see caveat above): \begin{coq_example} Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))". @@ -417,7 +417,7 @@ directly depends from the names of the \Coq\ files. It may happen that these filenames are in conflict with already existing files, either in the standard library of the target language or in other code that is meant to be linked with the extracted code. -For instance the module {\tt List} exists both in \Coq\ and in Ocaml. +For instance the module {\tt List} exists both in \Coq\ and in {\ocaml}. It is possible to instruct the extraction not to use particular filenames. \begin{description} @@ -430,7 +430,7 @@ It is possible to instruct the extraction not to use particular filenames. Allow the extraction to use any filename. \end{description} -\noindent For Ocaml, a typical use of these commands is +\noindent For {\ocaml}, a typical use of these commands is {\tt Extraction Blacklist String List}. \asection{Differences between \Coq\ and ML type systems} @@ -438,7 +438,7 @@ It is possible to instruct the extraction not to use particular filenames. Due to differences between \Coq\ and ML type systems, some extracted programs are not directly typable in ML. -We now solve this problem (at least in Ocaml) by adding +We now solve this problem (at least in {\ocaml}) by adding when needed some unsafe casting {\tt Obj.magic}, which give a generic type {\tt 'a} to any term. @@ -455,7 +455,7 @@ Definition dp := fun (A B:Set)(x:A)(y:B)(f:forall C:Set, C->C) => (f A x, f B y). \end{verbatim} -In Ocaml, for instance, the direct extracted term would be +In {\ocaml}, for instance, the direct extracted term would be \begin{verbatim} let dp x y f = Pair((f () x),(f () y)) \end{verbatim} @@ -480,13 +480,13 @@ Inductive anything : Type := dummy : forall A:Set, A -> anything. \end{verbatim} which corresponds to the definition of an ML dynamic type. -In Ocaml, we must cast any argument of the constructor dummy. +In {\ocaml}, we must cast any argument of the constructor dummy. \end{itemize} \noindent Even with those unsafe castings, you should never get error like ``segmentation fault''. In fact even if your program may seem -ill-typed to the Ocaml type-checker, it can't go wrong: it comes +ill-typed to the {\ocaml} type-checker, it can't go wrong: it comes from a Coq well-typed terms, so for example inductives will always have the correct number of arguments, etc. diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex index 8025fbe29f..82765da6ed 100644 --- a/doc/refman/Omega.tex +++ b/doc/refman/Omega.tex @@ -149,6 +149,32 @@ intro; omega. % Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+. +\section{Options} + +\begin{quote} + \optindex{Stable Omega} + {\tt Unset Stable Omega} +\end{quote} +This deprecated option (on by default) is for compatibility with Coq +pre 8.5. It resets internal name counters to make executions of +{\tt omega} independent. + +\begin{quote} + \optindex{Omega UseLocalDefs} + {\tt Unset Omega UseLocalDefs} +\end{quote} +This option (on by default) allows {\tt omega} to use the bodies of +local variables. + +\begin{quote} + \optindex{Omega System} + {\tt Set Omega System} + \optindex{Omega Action} + {\tt Set Omega Action} +\end{quote} +These two options (off by default) activate the printing of debug +information. + \asection{Technical data} \label{technical} diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index e56c8fa7fe..b4e270e6c3 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -403,10 +403,14 @@ Fail Check B.T. \end{Warnings} \subsection{\tt Print Module {\ident} -\comindex{Print Module}} +\comindex{Print Module} \optindex{Short Module Printing}} Prints the module type and (optionally) the body of the module {\ident}. +For this command and {\tt Print Module Type}, the option {\tt Short + Module Printing} (off by default) disables the printing of the types of fields, +leaving only their names. + \subsection{\tt Print Module Type {\ident} \comindex{Print Module Type}} diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 8f659ded35..1d3311edc2 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -395,6 +395,8 @@ Proof. \end{ErrMsgs} +\subsection[\tt Set Bullet Behavior.]{\tt Set Bullet Behavior.\optindex{Bullet Behavior}} + The bullet behavior can be controlled by the following commands. \begin{quote} diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 956f308512..30724759d2 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -127,8 +127,10 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}. \optindex{Boolean Equality Schemes} \optindex{Elimination Schemes} \optindex{Nonrecursive Elimination Schemes} +\optindex{Record Elimination Schemes} \optindex{Case Analysis Schemes} \optindex{Decidable Equality Schemes} +\optindex{Rewriting Schemes} \label{set-nonrecursive-elimination-schemes} } @@ -142,6 +144,7 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic declaration of the induction principles. It can be activated with the command {\tt Set Nonrecursive Elimination Schemes}. It can be deactivated again with {\tt Unset Nonrecursive Elimination Schemes}. +{\tt Record Elimination Schemes} is a deprecated alias of {\tt Nonrecursive Elimination Schemes}. In addition, the {\tt Case Analysis Schemes} flag governs the generation of case analysis lemmas for inductive types, i.e. corresponding to the @@ -156,6 +159,9 @@ However you have to be careful with this option since \Coq~ may now reject well-defined inductive types because it cannot compute a Boolean equality for them. +The {\tt Rewriting Schemes} flag governs generation of equality +related schemes such as congruence. + \subsection{\tt Combined Scheme} \label{CombinedScheme} \comindex{Combined Scheme} diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex index be199e0b24..31dabcdd4e 100644 --- a/doc/refman/RefMan-ssr.tex +++ b/doc/refman/RefMan-ssr.tex @@ -3096,10 +3096,10 @@ the tactic \ssrC{rewrite (=~ multi1)} is equivalent to \end{lstlisting} except that the constants \ssrC{eqba, eqab, mult1_rev} have not been created. -Rewriting with multirules -is useful to implement simplification or transformation -procedures, to be applied on terms of small to medium size. For -instance the library \ssrL{ssrnat} provides two implementations for +Rewriting with multirules is useful to implement simplification or +transformation procedures, to be applied on terms of small to medium +size. For instance, the library \ssrL{ssrnat} --- available in the +external math-comp library --- provides two implementations for arithmetic operations on natural numbers: an elementary one and a tail recursive version, less inefficient but also less convenient for reasoning purposes. The library also provides one lemma per such diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 675c2bf174..66a5f107a5 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3334,6 +3334,14 @@ evaluating purely computational expressions (i.e. with little dead code). \end{Variants} +\Rem The following option makes {\tt cbv} (and its derivative {\tt + compute}) print information about the constants it encounters and +the unfolding decisions it makes. +\begin{quote} + \optindex{Debug Cbv} + {\tt Set Debug Cbv} +\end{quote} + % Obsolete? Anyway not very important message %\begin{ErrMsgs} %\item \errindex{Delta must be specified before} @@ -3507,6 +3515,13 @@ of {\tt cbn} while doing reductions in unification, type inference and tactic applications. It can result in expensive unifications, as refolding currently uses a potentially exponential heuristic. +\begin{quote} + \optindex{Debug RAKAM} + {\tt Set Debug RAKAM} +\end{quote} +This option makes {\tt cbn} print various debugging information. +{\tt RAKAM} is the Refolding Algebraic Krivine Abstract Machine. + \subsection{\tt unfold \qualid} \tacindex{unfold} \label{unfold} @@ -3703,6 +3718,9 @@ hints of the database named {\tt core}. This variant is very useful for getting a better understanding of automation, or to know what lemmas/assumptions were used. +\item {\tt debug auto} Behaves like {\tt auto} but shows the tactics + it tries to solve the goal, including failing paths. + \item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} \ident$_1$ {\ldots} \ident$_n$} @@ -3723,6 +3741,8 @@ hints of the database named {\tt core}. \item {\tt info\_trivial} +\item {\tt debug trivial} + \item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} \ident$_1$ {\ldots} \ident$_n$} @@ -3732,6 +3752,19 @@ hints of the database named {\tt core}. \Rem {\tt auto} either solves completely the goal or else leaves it intact. \texttt{auto} and \texttt{trivial} never fail. +\Rem The following options enable printing of informative or debug +information for the {\tt auto} and {\tt trivial} tactics: +\begin{quote} + \optindex{Info Auto} + {\tt Set Info Auto} + \optindex{Debug Auto} + {\tt Set Debug Auto} + \optindex{Info Trivial} + {\tt Set Info Trivial} + \optindex{Debug Trivial} + {\tt Set Debug Trivial} +\end{quote} + \SeeAlso Section~\ref{Hints-databases} \subsection{\tt eauto} @@ -3768,6 +3801,14 @@ Note that {\tt ex\_intro} should be declared as a hint. \end{Variants} +\Rem {\tt eauto} obeys the following options: +\begin{quote} + \optindex{Info Eauto} + {\tt Set Info Eauto} + \optindex{Debug Eauto} + {\tt Set Debug Eauto} +\end{quote} + \SeeAlso Section~\ref{Hints-databases} \subsection{\tt autounfold with \ident$_1$ \mbox{\dots} \ident$_n$} @@ -4710,6 +4751,13 @@ congruence. described above. \end{ErrMsgs} +\noindent {\bf Remark: } {\tt congruence} can be made to print debug +information by setting the following option: + +\begin{quote} +\optindex{Congruence Verbose} +{\tt Set Congruence Verbose} +\end{quote} \section{Checking properties of terms} diff --git a/engine/eConstr.ml b/engine/eConstr.ml index d303038c5d..a65b3941ef 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -150,6 +150,8 @@ type rel_declaration = (constr, types) Context.Rel.Declaration.pt type named_context = (constr, types) Context.Named.pt type rel_context = (constr, types) Context.Rel.pt +type 'a puniverses = 'a * EInstance.t + let in_punivs a = (a, EInstance.empty) let mkProp = of_kind (Sort (ESorts.make Sorts.prop)) @@ -768,6 +770,20 @@ let rec isArity sigma c = | Sort _ -> true | _ -> false +type arity = rel_context * ESorts.t + +let destArity sigma = + let open Context.Rel.Declaration in + let rec prodec_rec l c = + match kind sigma c with + | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) c + | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c + | Cast (c,_,_) -> prodec_rec l c + | Sort s -> l,s + | _ -> anomaly ~label:"destArity" (Pp.str "not an arity.") + in + prodec_rec [] + let mkProd_or_LetIn decl c = let open Context.Rel.Declaration in match decl with @@ -815,6 +831,15 @@ let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e) let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e) let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e) +let map_rel_context_in_env f env sign = + let rec aux env acc = function + | d::sign -> + aux (push_rel d env) (Context.Rel.Declaration.map_constr (f env) d :: acc) sign + | [] -> + acc + in + aux env [] (List.rev sign) + let fresh_global ?loc ?rigid ?names env sigma reference = let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in evd, of_constr t diff --git a/engine/eConstr.mli b/engine/eConstr.mli index f54c422adc..30de748a19 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -56,6 +56,8 @@ sig val is_empty : t -> bool end +type 'a puniverses = 'a * EInstance.t + (** {5 Destructors} *) val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term @@ -144,7 +146,11 @@ val isFix : Evd.evar_map -> t -> bool val isCoFix : Evd.evar_map -> t -> bool val isCase : Evd.evar_map -> t -> bool val isProj : Evd.evar_map -> t -> bool + +type arity = rel_context * ESorts.t +val destArity : Evd.evar_map -> types -> arity val isArity : Evd.evar_map -> t -> bool + val isVarId : Evd.evar_map -> Id.t -> t -> bool val isRelN : Evd.evar_map -> int -> t -> bool @@ -260,6 +266,9 @@ val lookup_rel : int -> env -> rel_declaration val lookup_named : variable -> env -> named_declaration val lookup_named_val : variable -> named_context_val -> named_declaration +val map_rel_context_in_env : + (env -> constr -> constr) -> env -> rel_context -> rel_context + (* XXX Missing Sigma proxy *) val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> diff --git a/ide/coq-ssreflect.lang b/ide/coq-ssreflect.lang index 7cfc167018..bd9cb4bfa2 100644 --- a/ide/coq-ssreflect.lang +++ b/ide/coq-ssreflect.lang @@ -228,7 +228,7 @@ <keyword>Implicit\%{space}+Arguments</keyword> <keyword>(Import)|(Include)</keyword> <keyword>Require(\%{space}+((Import)|(Export)))?</keyword> - <keyword>(Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))?</keyword> + <keyword>(Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(OCaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))?</keyword> <keyword>Extract\%{space}+(Inlined\%{space}+)?(Constant)|(Inductive)</keyword> <include> <context sub-pattern="1" style-ref="vernac-keyword"/> diff --git a/ide/coq.lang b/ide/coq.lang index 484264ece3..e9eab48de7 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -188,7 +188,7 @@ <keyword>(\%{locality}|(Reserved|Tactic)\%{space})?Notation</keyword> <keyword>\%{locality}Infix</keyword> <keyword>Declare\%{space}ML\%{space}Module</keyword> - <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)</keyword> + <keyword>Extraction\%{space}Language\%{space}(OCaml|Haskell|Scheme|JSON)</keyword> </context> <context id="hint-command" style-ref="vernac-keyword"> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 74ae321202..61b33aa415 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2098,39 +2098,36 @@ let interp_open_constr env sigma c = (* Not all evars expected to be resolved and computation of implicit args *) -let interp_constr_evars_gen_impls env evdref +let interp_constr_evars_gen_impls env sigma ?(impls=empty_internalization_env) expected_type c = let c = intern_gen expected_type ~impls env c in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in - let evd, c = understand_tcc env !evdref ~expected_type c in - evdref := evd; - c, imps + let sigma, c = understand_tcc env sigma ~expected_type c in + sigma, (c, imps) -let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c = - interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c +let interp_constr_evars_impls env sigma ?(impls=empty_internalization_env) c = + interp_constr_evars_gen_impls env sigma ~impls WithoutTypeConstraint c let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ = interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c -let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c = - interp_constr_evars_gen_impls env evdref ~impls IsType c +let interp_type_evars_impls env sigma ?(impls=empty_internalization_env) c = + interp_constr_evars_gen_impls env sigma ~impls IsType c (* Not all evars expected to be resolved, with side-effect on evars *) -let interp_constr_evars_gen env evdref ?(impls=empty_internalization_env) expected_type c = +let interp_constr_evars_gen env sigma ?(impls=empty_internalization_env) expected_type c = let c = intern_gen expected_type ~impls env c in - let evd, c = understand_tcc env !evdref ~expected_type c in - evdref := evd; - c + understand_tcc env sigma ~expected_type c let interp_constr_evars env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c -let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen env evdref ~impls (OfType (EConstr.of_constr typ)) c +let interp_casted_constr_evars env sigma ?(impls=empty_internalization_env) c typ = + interp_constr_evars_gen env sigma ~impls (OfType typ) c -let interp_type_evars env evdref ?(impls=empty_internalization_env) c = - interp_constr_evars_gen env evdref IsType ~impls c +let interp_type_evars env sigma ?(impls=empty_internalization_env) c = + interp_constr_evars_gen env sigma IsType ~impls c (* Miscellaneous *) @@ -2185,17 +2182,16 @@ let intern_context global_level env impl_env binders = with InternalizationError (loc,e) -> user_err ?loc ~hdr:"internalize" (explain_internalization_error e) -let interp_glob_context_evars env evdref k bl = +let interp_glob_context_evars env sigma k bl = let open EConstr in - let (env, par, _, impls) = + let env, sigma, par, _, impls = List.fold_left - (fun (env,params,n,impls) (na, k, b, t) -> + (fun (env,sigma,params,n,impls) (na, k, b, t) -> let t' = if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t else t in - let (evd,t) = understand_tcc env !evdref ~expected_type:IsType t' in - evdref := evd; + let sigma, t = understand_tcc env sigma ~expected_type:IsType t' in match b with None -> let d = LocalAssum (na,t) in @@ -2205,16 +2201,15 @@ let interp_glob_context_evars env evdref k bl = (ExplByPos (n, na), (true, true, true)) :: impls else impls in - (push_rel d env, d::params, succ n, impls) + (push_rel d env, sigma, d::params, succ n, impls) | Some b -> - let (evd,c) = understand_tcc env !evdref ~expected_type:(OfType t) b in - evdref := evd; + let sigma, c = understand_tcc env sigma ~expected_type:(OfType t) b in let d = LocalDef (na, c, t) in - (push_rel d env, d::params, n, impls)) - (env,[],k+1,[]) (List.rev bl) - in (env, par), impls + (push_rel d env, sigma, d::params, n, impls)) + (env,sigma,[],k+1,[]) (List.rev bl) + in sigma, ((env, par), impls) -let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params = +let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params = let int_env,bl = intern_context global_level env impl_env params in - let x = interp_glob_context_evars env evdref shift bl in - int_env, x + let sigma, x = interp_glob_context_evars env sigma shift bl in + sigma, (int_env, x) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 46f96d20b4..632b423b05 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -112,28 +112,28 @@ val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.co (** Accepting unresolved evars *) -val interp_constr_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> EConstr.constr +val interp_constr_evars : env -> evar_map -> + ?impls:internalization_env -> constr_expr -> evar_map * EConstr.constr -val interp_casted_constr_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> types -> EConstr.constr +val interp_casted_constr_evars : env -> evar_map -> + ?impls:internalization_env -> constr_expr -> EConstr.types -> evar_map * EConstr.constr -val interp_type_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> EConstr.types +val interp_type_evars : env -> evar_map -> + ?impls:internalization_env -> constr_expr -> evar_map * EConstr.types (** Accepting unresolved evars and giving back the manual implicit arguments *) -val interp_constr_evars_impls : env -> evar_map ref -> +val interp_constr_evars_impls : env -> evar_map -> ?impls:internalization_env -> constr_expr -> - EConstr.constr * Impargs.manual_implicits + evar_map * (EConstr.constr * Impargs.manual_implicits) -val interp_casted_constr_evars_impls : env -> evar_map ref -> +val interp_casted_constr_evars_impls : env -> evar_map -> ?impls:internalization_env -> constr_expr -> EConstr.types -> - EConstr.constr * Impargs.manual_implicits + evar_map * (EConstr.constr * Impargs.manual_implicits) -val interp_type_evars_impls : env -> evar_map ref -> +val interp_type_evars_impls : env -> evar_map -> ?impls:internalization_env -> constr_expr -> - EConstr.types * Impargs.manual_implicits + evar_map * (EConstr.types * Impargs.manual_implicits) (** Interprets constr patterns *) @@ -158,8 +158,8 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConst val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> - env -> evar_map ref -> local_binder_expr list -> - internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits) + env -> evar_map -> local_binder_expr list -> + evar_map * (internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits)) (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) (* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) diff --git a/lib/cList.ml b/lib/cList.ml index ca69628af7..0ef7c3d8ba 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -96,6 +96,8 @@ sig val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a + val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list + val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list @@ -446,6 +448,12 @@ let rec fold_left3 f accu l1 l2 l3 = | (a1::l1, a2::l2, a3::l3) -> fold_left3 f (f accu a1 a2 a3) l1 l2 l3 | (_, _, _) -> invalid_arg "List.fold_left3" +let rec fold_left4 f accu l1 l2 l3 l4 = + match (l1, l2, l3, l4) with + ([], [], [], []) -> accu + | (a1::l1, a2::l2, a3::l3, a4::l4) -> fold_left4 f (f accu a1 a2 a3 a4) l1 l2 l3 l4 + | (_,_, _, _) -> invalid_arg "List.fold_left4" + (* [fold_right_and_left f [a1;...;an] hd = f (f (... (f (f hd an @@ -765,12 +773,13 @@ let share_tails l1 l2 = in shr_rev [] (List.rev l1, List.rev l2) +(* Poor man's monadic map *) let rec fold_left_map f e = function - | [] -> (e,[]) - | h::t -> - let e',h' = f e h in - let e'',t' = fold_left_map f e' t in - e'',h'::t' + | [] -> (e,[]) + | h::t -> + let e',h' = f e h in + let e'',t' = fold_left_map f e' t in + e'',h'::t' let fold_map = fold_left_map @@ -790,12 +799,26 @@ let fold_right_map f l e = let fold_map' = fold_right_map +let on_snd f (x,y) = (x,f y) + let fold_left2_map f e l l' = - List.fold_left2 (fun (e,l) x x' -> let (e,y) = f e x x' in (e,y::l)) (e,[]) l l' + on_snd List.rev @@ + List.fold_left2 (fun (e,l) x x' -> + let (e,y) = f e x x' in + (e, y::l) + ) (e, []) l l' let fold_right2_map f l l' e = List.fold_right2 (fun x x' (l,e) -> let (y,e) = f x x' e in (y::l,e)) l l' ([],e) +let fold_left3_map f e l l' l'' = + on_snd List.rev @@ + fold_left3 (fun (e,l) x x' x'' -> let (e,y) = f e x x' x'' in (e,y::l)) (e,[]) l l' l'' + +let fold_left4_map f e l1 l2 l3 l4 = + on_snd List.rev @@ + fold_left4 (fun (e,l) x1 x2 x3 x4 -> let (e,y) = f e x1 x2 x3 x4 in (e,y::l)) (e,[]) l1 l2 l3 l4 + let map_assoc f = List.map (fun (x,a) -> (x,f a)) let rec assoc_f f a = function diff --git a/lib/cList.mli b/lib/cList.mli index 8cb07da79c..f87db04cf4 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -211,7 +211,14 @@ sig val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a (** Same with two lists, folding on the right *) + val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list + (** Same with three lists, folding on the left *) + + val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list + (** Same with four lists, folding on the left *) + val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list + (* [@@ocaml.deprecated "Same as [fold_left_map]"] *) (** @deprecated Same as [fold_left_map] *) val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index fb65a8639a..c8c4c2dad9 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -38,9 +38,8 @@ let start_deriving f suchthat lemma = let f_type = EConstr.Unsafe.to_constr f_type in let ef = EConstr.Unsafe.to_constr ef in let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in - let evdref = ref sigma in - let suchthat = Constrintern.interp_type_evars env' evdref suchthat in - TCons ( env' , !evdref , suchthat , (fun sigma _ -> + let sigma, suchthat = Constrintern.interp_type_evars env' sigma suchthat in + TCons ( env' , sigma , suchthat , (fun sigma _ -> TNil sigma)))))) in diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 23452febdc..24c70bccfb 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -42,14 +42,20 @@ ARGUMENT EXTEND int_or_id END let pr_language = function - | Ocaml -> str "Ocaml" + | Ocaml -> str "OCaml" | Haskell -> str "Haskell" | Scheme -> str "Scheme" | JSON -> str "JSON" +let warn_deprecated_ocaml_spelling = + CWarnings.create ~name:"deprecated-ocaml-spelling" ~category:"deprecated" + (fun () -> + strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\".")) + VERNAC ARGUMENT EXTEND language PRINTED BY pr_language -| [ "Ocaml" ] -> [ Ocaml ] +| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ] +| [ "OCaml" ] -> [ Ocaml ] | [ "Haskell" ] -> [ Haskell ] | [ "Scheme" ] -> [ Scheme ] | [ "JSON" ] -> [ JSON ] diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 938bec25b9..b81010c7bd 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -40,17 +40,17 @@ let _= in declare_int_option gdopt -let congruence_depth=ref 100 let _= + let congruence_depth=ref 100 in let gdopt= - { optdepr=false; + { optdepr=true; (* noop *) optname="Congruence Depth"; optkey=["Congruence";"Depth"]; optread=(fun ()->Some !congruence_depth); optwrite= (function - None->congruence_depth:=0 + None->congruence_depth:=0 | Some i->congruence_depth:=(max i 0))} in declare_int_option gdopt diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index fa43536304..889c064b24 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1497,7 +1497,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) Decl_kinds.Finite with | UserError(s,msg) as e -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 9e22ad3063..071599d9c5 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -158,8 +158,8 @@ let build_newrecursive (fun (env,impls) (((_,recname),_),bl,arityc,_) -> let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in - let evdref = ref (Evd.from_env env0) in - let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in + let evd = Evd.from_env env0 in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in let open Context.Named.Declaration in (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) @@ -406,7 +406,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp match fixpoint_exprl with | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - Command.do_definition + ComDefinition.do_definition + ~program_mode:false fname (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); @@ -426,7 +427,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> @@ -616,8 +617,8 @@ and rebuild_nal aux bk bl' nal typ = let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = - let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in + let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in + let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 9e2774ff32..9fcb35f89e 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -889,11 +889,11 @@ let merge_inductive (ind1: inductive) (ind2: inductive) } in *) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) - let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,pl,impls = Command.interp_mutual_inductive indl [] + let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in + let mie,pl,impls = ComInductive.interp_mutual_inductive indl [] false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) - ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) + ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls) (* Find infos on identifier id. *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 766adfc63a..363ad5dfc9 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1427,7 +1427,7 @@ let com_terminate nb_args ctx hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = - let evmap, env = Pfedit.get_current_context () in + let evd, env = Pfedit.get_current_context () in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; @@ -1479,13 +1479,13 @@ let (com_eqn : int -> Id.t -> | ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in - let evmap, env = Pfedit.get_current_context () in - let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in + let evd, env = Pfedit.get_current_context () in + let evd = Evd.from_ctx (Evd.evar_universe_context evd) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in (Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign:(Environ.named_context_val env) - evmap + evd (EConstr.of_constr equation_lemma_type) (Lemmas.mk_hook (fun _ _ -> ())); ignore (by @@ -1528,14 +1528,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let open Constr in let open CVars in let env = Global.env() in - let evd = ref (Evd.from_env env) in - let function_type = interp_type_evars env evd type_of_f in + let evd = Evd.from_env env in + let evd, function_type = interp_type_evars env evd type_of_f in let function_type = EConstr.Unsafe.to_constr function_type in let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) - let ty = interp_type_evars env evd ~impls:rec_impls eq in + let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in let ty = EConstr.Unsafe.to_constr ty in - let evm, nf = Evarutil.nf_evars_and_universes !evd in + let evd, nf = Evarutil.nf_evars_and_universes evd in let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in let function_type = nf function_type in let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in @@ -1560,16 +1560,16 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in + let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res in (* Refresh the global universes, now including those of _F *) - let evm = Evd.from_env (Global.env ()) in + let evd = Evd.from_env (Global.env ()) in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in let relation, evuctx = - interp_constr env_with_pre_rec_args evm r + interp_constr env_with_pre_rec_args evd r in - let evm = Evd.from_ctx evuctx in + let evd = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) @@ -1599,7 +1599,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num and functional_ref = destConst (constr_of_global functional_ref) and eq_ref = destConst (constr_of_global eq_ref) in generate_induction_principle f_ref tcc_lemma_constr - functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation); + functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evd (EConstr.of_constr res)) (EConstr.of_constr relation); Flags.if_verbose msgnl (h 1 (Ppconstr.pr_id function_name ++ spc () ++ str"is defined" )++ fnl () ++ @@ -1618,5 +1618,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num term_id using_lemmas (List.length res_vars) - evm (Lemmas.mk_hook hook)) + evd (Lemmas.mk_hook hook)) () diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 97f43eaa8f..1615465281 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -289,7 +289,7 @@ let rec find_in_stack what acc = function | { name } as x :: rest when String.equal name what -> Some(acc, x, rest) | { name } as x :: rest -> find_in_stack what (x :: acc) rest -let exit_tactic start_time c = +let exit_tactic ~count_call start_time c = let diff = time () -. start_time in match Local.(!stack) with | [] | [_] -> @@ -304,7 +304,7 @@ let exit_tactic start_time c = let node = { node with total = node.total +. diff; local = node.local +. diff; - ncalls = node.ncalls + 1; + ncalls = node.ncalls + (if count_call then 1 else 0); max_total = max node.max_total diff; } in (* updating the stack *) @@ -341,7 +341,7 @@ let tclFINALLY tac (finally : unit Proofview.tactic) = (fun v -> finally <*> Proofview.tclUNIT v) (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn) -let do_profile s call_trace tac = +let do_profile s call_trace ?(count_call=true) tac = let open Proofview.Notations in Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> if !is_profiling then @@ -359,7 +359,7 @@ let do_profile s call_trace tac = tac (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> (match call_trace with - | (_, c) :: _ -> exit_tactic start_time c + | (_, c) :: _ -> exit_tactic ~count_call start_time c | [] -> ())))) | None -> tac diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli index 07990c7502..adedf7ee91 100644 --- a/plugins/ltac/profile_ltac.mli +++ b/plugins/ltac/profile_ltac.mli @@ -9,9 +9,39 @@ (** Ltac profiling primitives *) +(* Note(JasonGross): Ltac semantics are a bit insane. There isn't + really a good notion of how many times a tactic has been "called", + because tactics can be partially evaluated, and it's unclear + whether the number of "calls" should be the number of times the + body is fetched and unfolded, or the number of times the code is + executed to a value, etc. The logic in [Tacinterp.eval_tactic] + gives a decent approximation, which I believe roughly corresponds + to the number of times that the engine runs the tactic value which + results from evaluating the tactic expression bound to the name + we're considering. However, this is a poor approximation of the + time spent in the tactic; we want to consider time spent evaluating + a tactic expression to a tactic value to be time spent in the + expression, not just time spent in the caller of the expression. + So we need to wrap some nodes in additional profiling calls which + don't count towards to total call count. Whether or not a call + "counts" is indicated by the [count_call] boolean argument. + + Unfortunately, at present, we can get very strange call graphs when + a named tactic expression never runs as a tactic value: if we have + [Ltac t0 := t.] and [Ltac t1 := t0.], then [t1] is considered to + run 0(!) times. It evaluates to [t] during tactic expression + evaluation, and although the call trace records the fact that it + was called by [t0] which was called by [t1], the tactic running + phase never sees this. Thus we get one call tree (from expression + evaluation) that has [t1] calls [t0] calls [t], and another call + tree which says that the caller of [t1] calls [t] directly; the + expression evaluation time goes in the first tree, and the call + count and tactic running time goes in the second tree. Alas, I + suspect that fixing this requires a redesign of how the profiler + hooks into the tactic engine. *) val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> - 'b Proofview.tactic -> 'b Proofview.tactic + ?count_call:bool -> 'b Proofview.tactic -> 'b Proofview.tactic val set_profiling : bool -> unit diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2e14243d8a..a698b05dd7 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1781,7 +1781,9 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = - new_instance (Flags.is_universe_polymorphism ()) + let program_mode = Flags.is_program_mode () in + let poly = Flags.is_universe_polymorphism () in + new_instance ~program_mode poly binders instance (Some (true, CAst.make @@ CRecord (fields))) ~global ~generalize:false ~refine:false Hints.empty_hint_info @@ -2012,9 +2014,10 @@ let add_morphism glob binders m s n = [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - ignore(new_instance ~global:glob poly binders instance - (Some (true, CAst.make @@ CRecord [])) - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) + let program_mode = Flags.is_program_mode () in + ignore(new_instance ~program_mode ~global:glob poly binders instance + (Some (true, CAst.make @@ CRecord [])) + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index ded902a8fb..ccded44179 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1158,10 +1158,14 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Proofview.V82.tactic begin tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) end - | TacAbstract (tac,ido) -> + | TacAbstract (t,ido) -> + let call = LtacMLCall tac in + push_trace(None,call) ist >>= fun trace -> + Profile_ltac.do_profile "eval_tactic:TacAbstract" trace + (catch_error_tac trace begin Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT - (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac) - end + (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t) + end end) | TacThen (t1,t) -> Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t) | TacDispatch tl -> @@ -1272,7 +1276,8 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = let extra = TacStore.set extra f_trace trace in let ist = { lfun = Id.Map.empty; extra = extra; } in let appl = GlbAppl[r,[]] in - val_interp ~appl ist (Tacenv.interp_ltac r) + Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false + (val_interp ~appl ist (Tacenv.interp_ltac r)) and interp_tacarg ist arg : Val.t Ftactic.t = match arg with @@ -1338,7 +1343,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = let ist = { lfun = newlfun; extra = TacStore.set ist.extra f_trace []; } in - catch_error_tac trace (val_interp ist body) >>= fun v -> + Profile_ltac.do_profile "interp_app" trace ~count_call:false + (catch_error_tac trace (val_interp ist body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) end begin fun (e, info) -> diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index bd9633afbd..6032ed2af8 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -143,14 +143,14 @@ let newssrcongrtac arg ist gl = (** Coq rewrite compatibility flag *) -let ssr_strict_match = ref false let _ = - Goptions.declare_bool_option + let ssr_strict_match = ref false in + Goptions.declare_bool_option { Goptions.optname = "strict redex matching"; Goptions.optkey = ["Match"; "Strict"]; Goptions.optread = (fun () -> !ssr_strict_match); - Goptions.optdepr = false; + Goptions.optdepr = true; (* noop *) Goptions.optwrite = (fun b -> ssr_strict_match := b) } (** Rewrite rules *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index b49da57a4b..bbb3a1bb2b 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -442,19 +442,20 @@ let add_class cl = let instance_constructor (cl,u) args = let lenpars = List.count is_local_assum (snd cl.cl_context) in + let open EConstr in let pars = fst (List.chop lenpars args) in match cl.cl_impl with | IndRef ind -> let ind = ind, u in - (Some (applistc (mkConstructUi (ind, 1)) args), - applistc (mkIndU ind) pars) + (Some (applist (mkConstructUi (ind, 1), args)), + applist (mkIndU ind, pars)) | ConstRef cst -> let cst = cst, u in let term = match args with | [] -> None | _ -> Some (List.last args) in - (term, applistc (mkConstU cst) pars) + (term, applist (mkConstU cst, pars)) | _ -> assert false let typeclasses () = Refmap.fold (fun _ l c -> l :: c) !classes [] diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 618826f3d0..8ee061330a 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -83,8 +83,8 @@ val is_instance : global_reference -> bool (** Returns the term and type for the given instance of the parameters and fields of the type class. *) -val instance_constructor : typeclass Univ.puniverses -> constr list -> - constr option * types +val instance_constructor : typeclass EConstr.puniverses -> EConstr.t list -> + EConstr.t option * EConstr.t (** Filter which evars to consider for resolution. *) type evar_filter = Evar.t -> Evar_kinds.t -> bool diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 1ae3577edb..01065868d4 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -249,11 +249,11 @@ let add_inversion_lemma name env sigma t sort dep inv_op = let add_inversion_lemma_exn na com comsort bool tac = let env = Global.env () in - let evd = ref (Evd.from_env env) in - let c = Constrintern.interp_type_evars env evd com in - let evd, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env !evd comsort in + let sigma = Evd.from_env env in + let sigma, c = Constrintern.interp_type_evars env sigma com in + let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in try - add_inversion_lemma na env evd c sort bool tac + add_inversion_lemma na env sigma c sort bool tac with | UserError (Some "Case analysis",s) -> (* Reference to Indrec *) user_err ~hdr:"Inv needs Nodep Prop Set" s diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired index 729de2f366..7900c034da 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired @@ -1,7 +1,6 @@ Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' -COQDEP Fast.v -COQDEP Slow.v +COQDEP VFILES Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' Makefile:69: warning: undefined variable '*' diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired index b25bc3683c..7ab0bc75d9 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired @@ -1,7 +1,6 @@ Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' -COQDEP Fast.v -COQDEP Slow.v +COQDEP VFILES Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' Makefile:69: warning: undefined variable '*' diff --git a/test-suite/output-modulo-time/ltacprof.out b/test-suite/output-modulo-time/ltacprof.out index cc04c2c9bd..5553e1b38d 100644 --- a/test-suite/output-modulo-time/ltacprof.out +++ b/test-suite/output-modulo-time/ltacprof.out @@ -1,12 +1,15 @@ -total time: 1.528s +total time: 1.032s - tactic local total calls max + tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─sleep' -------------------------------- 100.0% 100.0% 1 1.528s +─sleep' -------------------------------- 100.0% 100.0% 1 1.032s +─sleep --------------------------------- 0.0% 0.0% 0 0.000s ─constructor --------------------------- 0.0% 0.0% 1 0.000s - tactic local total calls max + tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─sleep' -------------------------------- 100.0% 100.0% 1 1.528s +─sleep' -------------------------------- 100.0% 100.0% 1 1.032s +─sleep --------------------------------- 0.0% 0.0% 0 0.000s +└sleep' -------------------------------- 0.0% 0.0% 0 0.000s ─constructor --------------------------- 0.0% 0.0% 1 0.000s diff --git a/test-suite/output-modulo-time/ltacprof_abstract.out b/test-suite/output-modulo-time/ltacprof_abstract.out new file mode 100644 index 0000000000..c60c5abddf --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_abstract.out @@ -0,0 +1,14 @@ +total time: 0.964s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─sleep' -------------------------------- 100.0% 100.0% 1 0.964s +─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.964s +─constructor --------------------------- 0.0% 0.0% 1 0.000s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.964s + ├─sleep' ------------------------------ 100.0% 100.0% 1 0.964s + └─constructor ------------------------- 0.0% 0.0% 1 0.000s + diff --git a/test-suite/output-modulo-time/ltacprof_abstract.v b/test-suite/output-modulo-time/ltacprof_abstract.v new file mode 100644 index 0000000000..10a76309e3 --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_abstract.v @@ -0,0 +1,8 @@ +(* -*- coq-prog-args: ("-profile-ltac-cutoff" "0.0") -*- *) +Ltac sleep' := do 100 (do 100 (do 100 idtac)). +Ltac sleep := sleep'. + +Theorem x : True. +Proof. + idtac. idtac. abstract (sleep; constructor). +Defined. diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.out b/test-suite/output-modulo-time/ltacprof_cutoff.out index 0cd5777ccf..d91a38bb54 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.out +++ b/test-suite/output-modulo-time/ltacprof_cutoff.out @@ -1,31 +1,37 @@ -total time: 1.584s +total time: 1.632s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s -─sleep --------------------------------- 100.0% 100.0% 3 0.572s -─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s +─sleep --------------------------------- 100.0% 100.0% 3 0.584s +─foo2 ---------------------------------- 0.0% 100.0% 1 1.632s +─foo1 ---------------------------------- 0.0% 64.2% 1 1.048s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s -└foo1 ---------------------------------- 0.0% 63.9% 1 1.012s +─foo2 ---------------------------------- 0.0% 100.0% 1 1.632s +└foo1 ---------------------------------- 0.0% 64.2% 1 1.048s -total time: 1.584s +total time: 0.520s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─foo2 ---------------------------------- 0.0% 100.0% 1 0.520s +─sleep --------------------------------- 99.2% 99.2% 52 0.016s +─foo1 ---------------------------------- 0.0% 97.7% 1 0.508s +─foo0 ---------------------------------- 0.8% 96.2% 1 0.500s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─foo2 ---------------------------------- 0.0% 100.0% 1 0.520s +└foo1 ---------------------------------- 0.0% 97.7% 1 0.508s +└foo0 ---------------------------------- 0.8% 96.2% 1 0.500s +└sleep --------------------------------- 95.4% 95.4% 50 0.016s + +total time: 0.000s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─sleep --------------------------------- 100.0% 100.0% 3 0.572s -─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s -─foo1 ---------------------------------- 0.0% 63.9% 1 1.012s -─foo0 ---------------------------------- 0.0% 31.3% 1 0.496s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─foo2 ---------------------------------- 0.0% 100.0% 1 1.584s - ├─foo1 -------------------------------- 0.0% 63.9% 1 1.012s - │ ├─sleep ----------------------------- 32.6% 32.6% 1 0.516s - │ └─foo0 ------------------------------ 0.0% 31.3% 1 0.496s - │ └sleep ----------------------------- 31.3% 31.3% 1 0.496s - └─sleep ------------------------------- 36.1% 36.1% 1 0.572s diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v index 3dad6271af..ae5d51bae8 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.v +++ b/test-suite/output-modulo-time/ltacprof_cutoff.v @@ -1,12 +1,28 @@ (* -*- coq-prog-args: ("-profile-ltac") -*- *) Require Coq.ZArith.BinInt. -Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). +Module WithIdTac. + Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). -Ltac foo0 := idtac; sleep. -Ltac foo1 := sleep; foo0. -Ltac foo2 := sleep; foo1. -Goal True. - foo2. - Show Ltac Profile CutOff 47. - constructor. -Qed. + Ltac foo0 := idtac; sleep. + Ltac foo1 := sleep; foo0. + Ltac foo2 := sleep; foo1. + Goal True. + foo2. + Show Ltac Profile CutOff 47. + constructor. + Qed. +End WithIdTac. + +Module TestEval. + Ltac sleep := let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac. + + Ltac foo0 := idtac; do 50 (idtac; sleep). + Ltac foo1 := sleep; foo0. + Ltac foo2 := sleep; foo1. + Goal True. + Reset Ltac Profile. + foo2. + Show Ltac Profile CutOff 47. + constructor. + Qed. +End TestEval. diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out new file mode 100644 index 0000000000..91ceb1b583 --- /dev/null +++ b/test-suite/output/bug5778.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +In nested Ltac calls to "c", "abs" and "abstract b ltac:(())", last call +failed. +The term "I" has type "True" which should be Set, Prop or Type. diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v new file mode 100644 index 0000000000..0dcd76aeff --- /dev/null +++ b/test-suite/output/bug5778.v @@ -0,0 +1,7 @@ +Ltac a _ := pose (I : I). +Ltac b _ := a (). +Ltac abs _ := abstract b (). +Ltac c _ := abs (). +Goal True. + Fail c (). +Abort. diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 0ee2232502..83726bfdc5 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -635,6 +635,6 @@ Recursive Extraction Everything. Require Import ZArith. -Extraction Language Ocaml. +Extraction Language OCaml. Recursive Extraction Z_modulo_2 Zdiv_eucl_exist. Extraction TestCompile Z_modulo_2 Zdiv_eucl_exist. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 2b56c63a0c..33a2f8593e 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -227,8 +227,9 @@ COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop) # We here define a bunch of variables about the files being part of the # Coq project in order to ease the writing of build target and build rules +VDFILE := .coqdeps + ALLSRCFILES := \ - $(VFILES) \ $(ML4FILES) \ $(MLFILES) \ $(MLPACKFILES) \ @@ -308,7 +309,7 @@ else DO_NATDYNLINK = endif -ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) +ALLDFILES = $(addsuffix .d,$(ALLSRCFILES) $(VDFILE)) # Compilation targets ######################################################### @@ -713,9 +714,9 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack $(SHOW)'COQDEP $<' $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) -$(addsuffix .d,$(VFILES)): %.v.d: %.v - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c "$<" $(redir_if_ok) +$(VDFILE).d: $(VFILES) + $(SHOW)'COQDEP VFILES' + $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c $(VFILES) $(redir_if_ok) # Misc ######################################################################## diff --git a/vernac/classes.ml b/vernac/classes.ml index 3e47f881c1..c2e9a5ab44 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -8,10 +8,7 @@ (*i*) open Names -open Term -open Constr -open Vars -open Environ +open EConstr open Nametab open CErrors open Util @@ -70,7 +67,7 @@ let existing_instance glob g info = let c = global g in let info = Option.default Hints.empty_hint_info info in let instance, _ = Global.type_of_global_in_context (Global.env ()) c in - let _, r = decompose_prod_assum instance in + let _, r = Term.decompose_prod_assum instance in match class_of_constr Evd.empty (EConstr.of_constr r) with | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob (*FIXME*) (Flags.use_polymorphic_flag ()) c) @@ -83,19 +80,20 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m (* Declare everything in the parameters as implicit, and the class instance as well *) -let type_ctx_instance evars env ctx inst subst = - let rec aux (subst, instctx) l = function +let type_ctx_instance env sigma ctx inst subst = + let open Vars in + let rec aux (sigma, subst, instctx) l = function decl :: ctx -> let t' = substl subst (RelDecl.get_type decl) in - let c', l = + let (sigma, c'), l = match decl with - | LocalAssum _ -> EConstr.Unsafe.to_constr (interp_casted_constr_evars env evars (List.hd l) t'), List.tl l - | LocalDef (_,b,_) -> substl subst b, l + | LocalAssum _ -> interp_casted_constr_evars env sigma (List.hd l) t', List.tl l + | LocalDef (_,b,_) -> (sigma, substl subst b), l in let d = RelDecl.get_name decl, Some c', t' in - aux (c' :: subst, d :: instctx) l ctx - | [] -> subst - in aux (subst, []) inst (List.rev ctx) + aux (sigma, c' :: subst, d :: instctx) l ctx + | [] -> sigma, subst + in aux (sigma, subst, []) inst (List.rev ctx) let id_of_class cl = match cl.cl_impl with @@ -112,32 +110,31 @@ let instance_hook k info global imps ?hook cst = Typeclasses.declare_instance (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant k info global imps ?hook id decl poly evm term termtype = +let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = let kind = IsDefinition Instance in - let evm = + let sigma = let env = Global.env () in let levels = Univ.LSet.union (Univops.universes_of_constr env termtype) (Univops.universes_of_constr env term) in - Evd.restrict_universe_context evm levels + Evd.restrict_universe_context sigma levels in - let uctx = Evd.check_univ_decl ~poly evm decl in + let uctx = Evd.check_univ_decl ~poly sigma decl in let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in Declare.definition_message id; - Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders evm); + Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma); instance_hook k info global imps ?hook (ConstRef kn); id let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) - poly ctx (instid, bk, cl) props ?(generalize=true) + ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in let ((loc, instid), pl) = instid in - let evd, decl = Univdecls.interp_univ_decl_opt env pl in - let evars = ref evd in + let sigma, decl = Univdecls.interp_univ_decl_opt env pl in let tclass, ids = match bk with | Decl_kinds.Implicit -> @@ -155,26 +152,26 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) else tclass in - let k, u, cty, ctx', ctx, len, imps, subst = - let impls, ((env', ctx), imps) = interp_context_evars env evars ctx in - let ctx = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) ctx in - let c', imps' = interp_type_evars_impls ~impls env' evars tclass in - let c' = EConstr.Unsafe.to_constr c' in + let sigma, k, u, cty, ctx', ctx, len, imps, subst = + let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in + let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in let len = List.length ctx in let imps = imps @ Impargs.lift_implicits len imps' in - let ctx', c = decompose_prod_assum c' in + let ctx', c = decompose_prod_assum sigma c' in let ctx'' = ctx' @ ctx in - let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in - let u = EConstr.EInstance.kind !evars u in - let cl = Typeclasses.typeclass_univ_instance (k, u) in - let _, args = + let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in + let u_s = EInstance.kind sigma u in + let cl = Typeclasses.typeclass_univ_instance (k, u_s) in + let args = List.map of_constr args in + let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in + let _, args = List.fold_right (fun decl (args, args') -> match decl with | LocalAssum _ -> (List.tl args, List.hd args :: args') - | LocalDef (_,b,_) -> (args, substl args' b :: args')) - (snd cl.cl_context) (args, []) + | LocalDef (_,b,_) -> (args, Vars.substl args' b :: args')) + cl_context (args, []) in - cl, u, c', ctx', ctx, len, imps, args + sigma, cl, u, c', ctx', ctx, len, imps, args in let id = match instid with @@ -188,9 +185,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) Namegen.next_global_ident_away i (Termops.vars_of_env env) in let env' = push_rel_context ctx env in - evars := Evarutil.nf_evar_map !evars; - evars := resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env !evars; - let subst = List.map (fun c -> EConstr.Unsafe.to_constr (Evarutil.nf_evar !evars (EConstr.of_constr c))) subst in + let sigma = Evarutil.nf_evar_map sigma in + let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in if abstract then begin let subst = List.fold_left2 @@ -198,18 +194,16 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) [] subst (snd k.cl_context) in let (_, ty_constr) = instance_constructor (k,u) subst in - let nf, subst = Evarutil.e_nf_evars_and_universes evars in - let termtype = - let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - nf t - in - Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); - let univs = Evd.check_univ_decl ~poly !evars decl in + let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in + let sigma,_ = Evarutil.nf_evars_and_universes sigma in + Pretyping.check_evars env Evd.empty sigma termtype; + let univs = Evd.check_univ_decl ~poly sigma decl in + let termtype = to_constr sigma termtype in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in - Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders !evars); + Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); instance_hook k pri global imps ?hook (ConstRef cst); id end else ( @@ -221,16 +215,16 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) Some (Inl fs) | Some (_, t) -> Some (Inr t) | None -> - if Flags.is_program_mode () then Some (Inl []) + if program_mode then Some (Inl []) else None in - let subst = + let subst, sigma = match props with - | None -> if List.is_empty k.cl_props then Some (Inl subst) else None + | None -> + (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma | Some (Inr term) -> - let c = interp_casted_constr_evars env' evars term cty in - let c = EConstr.Unsafe.to_constr c in - Some (Inr (c, subst)) + let sigma, c = interp_casted_constr_evars env' sigma term cty in + Some (Inr (c, subst)), sigma | Some (Inl props) -> let get_id = function @@ -267,9 +261,10 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) | (n, _) :: _ -> unbound_method env' k.cl_impl (get_id n) | _ -> - Some (Inl (type_ctx_instance evars (push_rel_context ctx' env') - k.cl_props props subst)) - in + let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in + let sigma, res = type_ctx_instance (push_rel_context ctx' env') sigma kcl_props props subst in + Some (Inl res), sigma + in let term, termtype = match subst with | None -> let termtype = it_mkProd_or_LetIn cty ctx in @@ -281,34 +276,30 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) in let (app, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in + let term = it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in Some term, termtype | Some (Inr (def, subst)) -> let termtype = it_mkProd_or_LetIn cty ctx in - let term = Termops.it_mkLambda_or_LetIn def ctx in + let term = it_mkLambda_or_LetIn def ctx in Some term, termtype in - let _ = - evars := Evarutil.nf_evar_map !evars; - evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true - env !evars; - (* Try resolving fields that are typeclasses automatically. *) - evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false - env !evars - in - let _ = evars := Evarutil.nf_evar_map_undefined !evars in - let evm, nf = Evarutil.nf_evar_map_universes !evars in - let termtype = nf termtype in - let _ = (* Check that the type is free of evars now. *) - Pretyping.check_evars env Evd.empty evm (EConstr.of_constr termtype) - in - let term = Option.map nf term in - if not (Evd.has_undefined evm) && not (Option.is_empty term) then + let sigma = Evarutil.nf_evar_map sigma in + let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in + (* Try resolving fields that are typeclasses automatically. *) + let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in + let sigma = Evarutil.nf_evar_map_undefined sigma in + (* Beware of this step, it is required as to minimize universes. *) + let sigma, _nf = Evarutil.nf_evar_map_universes sigma in + (* Check that the type is free of evars now. *) + Pretyping.check_evars env Evd.empty sigma termtype; + let termtype = to_constr sigma termtype in + let term = Option.map (to_constr sigma) term in + if not (Evd.has_undefined sigma) && not (Option.is_empty term) then declare_instance_constant k pri global imps ?hook id decl - poly evm (Option.get term) termtype - else if Flags.is_program_mode () || refine || Option.is_empty term then begin + poly sigma (Option.get term) termtype + else if program_mode || refine || Option.is_empty term then begin let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in - if Flags.is_program_mode () then + if program_mode then let hook vis gr _ = let cst = match gr with ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false gr ~enriching:false [imps]; @@ -318,12 +309,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) match term with | Some t -> let obls, _, constr, typ = - Obligations.eterm_obligations env id evm 0 t termtype + Obligations.eterm_obligations env id sigma 0 t termtype in obls, Some constr, typ | None -> [||], None, termtype in let hook = Lemmas.mk_hook hook in - let ctx = Evd.evar_universe_context evm in + let ctx = Evd.evar_universe_context sigma in ignore (Obligations.add_definition id ?term:constr ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls); id @@ -334,16 +325,16 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) the pretyping after the proof has opened. As a consequence, we use the low-level primitives to code the refinement manually.*) - let gls = List.rev (Evd.future_goals evm) in - let evm = Evd.reset_future_goals evm in - Lemmas.start_proof id ~pl:decl kind evm (EConstr.of_constr termtype) + let gls = List.rev (Evd.future_goals sigma) in + let sigma = Evd.reset_future_goals sigma in + Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype) (Lemmas.mk_hook (fun _ -> instance_hook k pri global imps ?hook)); (* spiwack: I don't know what to do with the status here. *) if not (Option.is_empty term) then let init_refine = Tacticals.New.tclTHENLIST [ - Refine.refine ~typecheck:false (fun evm -> (evm,EConstr.of_constr (Option.get term))); + Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term))); Proofview.Unsafe.tclNEWGOALS gls; Tactics.New.reduce_after_refine; ] @@ -357,6 +348,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) else CErrors.user_err Pp.(str "Unsolved obligations remaining.")) let named_of_rel_context l = + let open Vars in let acc, ctx = List.fold_right (fun decl (subst, ctx) -> @@ -370,20 +362,20 @@ let named_of_rel_context l = let context poly l = let env = Global.env() in - let evars = ref (Evd.from_env env) in - let _, ((env', fullctx), impls) = interp_context_evars env evars l in - let fullctx = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) fullctx in - let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in - let fullctx = Context.Rel.map subst fullctx in - let ce t = Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr t) in + let sigma = Evd.from_env env in + let sigma, (_, ((env', fullctx), impls)) = interp_context_evars env sigma l in + (* Note, we must use the normalized evar from now on! *) + let sigma,_ = Evarutil.nf_evars_and_universes sigma in + let ce t = Pretyping.check_evars env Evd.empty sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in let ctx = try named_of_rel_context fullctx with e when CErrors.noncritical e -> user_err Pp.(str "Anonymous variables not allowed in contexts.") in - let uctx = ref (Evd.universe_context_set !evars) in + let uctx = ref (Evd.universe_context_set sigma) in let fn status (id, b, t) = + let b, t = Option.map (to_constr sigma) b, to_constr sigma t in if Lib.is_modtype () && not (Lib.sections_are_opened ()) then (* Declare the universe context once *) let univs = if poly @@ -399,7 +391,7 @@ let context poly l = (DefinitionEntry entry, IsAssumption Logical) in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in - match class_of_constr !evars (EConstr.of_constr t) with + match class_of_constr sigma (of_constr t) with | Some (rels, ((tc,_), args) as _cl) -> add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*) poly (ConstRef cst)); @@ -419,7 +411,7 @@ let context poly l = in let nstatus = match b with | None -> - pi3 (Command.declare_assumption false decl (t, univs) Universes.empty_binders [] impl + pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl Vernacexpr.NoInline (Loc.tag id)) | Some b -> let decl = (Discharge, poly, Definition) in diff --git a/vernac/classes.mli b/vernac/classes.mli index c0f03227c4..d47c6a6f81 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -41,6 +41,7 @@ val new_instance : ?abstract:bool -> (** Not abstract by default. *) ?global:bool -> (** Not global by default. *) ?refine:bool -> (** Allow refinement *) + program_mode:bool -> Decl_kinds.polymorphic -> local_binder_expr list -> Vernacexpr.typeclass_constraint -> diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml new file mode 100644 index 0000000000..5d7adb24a5 --- /dev/null +++ b/vernac/comAssumption.ml @@ -0,0 +1,182 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open CErrors +open Util +open Vars +open Environ +open Declare +open Names +open Globnames +open Constrexpr_ops +open Constrintern +open Impargs +open Decl_kinds +open Pretyping +open Vernacexpr +open Entries + +(* 2| Variable/Hypothesis/Parameter/Axiom declarations *) + +let axiom_into_instance = ref false + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "automatically declare axioms whose type is a typeclass as instances"; + optkey = ["Typeclasses";"Axioms";"Are";"Instances"]; + optread = (fun _ -> !axiom_into_instance); + optwrite = (:=) axiom_into_instance; } + +let should_axiom_into_instance = function + | Discharge -> + (* The typeclass behaviour of Variable and Context doesn't depend + on section status *) + true + | Global | Local -> !axiom_into_instance + +let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) = +match local with +| Discharge when Lib.sections_are_opened () -> + let ctx = match ctx with + | Monomorphic_const_entry ctx -> ctx + | Polymorphic_const_entry ctx -> Univ.ContextSet.of_context ctx + in + let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in + let _ = declare_variable ident decl in + let () = assumption_message ident in + let () = + if not !Flags.quiet && Proof_global.there_are_pending_proofs () then + Feedback.msg_info (str"Variable" ++ spc () ++ Id.print ident ++ + strbrk " is not visible from current goals") + in + let r = VarRef ident in + let () = Typeclasses.declare_instance None true r in + let () = if is_coe then Class.try_add_new_coercion r ~local:true false in + (r,Univ.Instance.empty,true) + +| Global | Local | Discharge -> + let do_instance = should_axiom_into_instance local in + let local = DeclareDef.get_locality ident ~kind:"axiom" local in + let inl = match nl with + | NoInline -> None + | DefaultInline -> Some (Flags.get_inline_level()) + | InlineAt i -> Some i + in + let decl = (ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in + let kn = declare_constant ident ~local decl in + let gr = ConstRef kn in + let () = maybe_declare_manual_implicits false gr imps in + let () = Declare.declare_univ_binders gr pl in + let () = assumption_message ident in + let () = if do_instance then Typeclasses.declare_instance None false gr in + let () = if is_coe then Class.try_add_new_coercion gr ~local p in + let inst = match ctx with + | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx + | Monomorphic_const_entry _ -> Univ.Instance.empty + in + (gr,inst,Lib.is_modtype_strict ()) + +let interp_assumption sigma env impls bl c = + let c = mkCProdN ?loc:(local_binders_loc bl) bl c in + let sigma, (ty, impls) = interp_type_evars_impls env sigma ~impls c in + let ty = EConstr.Unsafe.to_constr ty in + sigma, (ty, impls) + +(* When monomorphic the universe constraints are declared with the first declaration only. *) +let next_uctx = + let empty_uctx = Monomorphic_const_entry Univ.ContextSet.empty in + function + | Polymorphic_const_entry _ as uctx -> uctx + | Monomorphic_const_entry _ -> empty_uctx + +let declare_assumptions idl is_coe k (c,uctx) pl imps nl = + let refs, status, _ = + List.fold_left (fun (refs,status,uctx) id -> + let ref',u',status' = + declare_assumption is_coe k (c,uctx) pl imps false nl id in + (ref',u')::refs, status' && status, next_uctx uctx) + ([],true,uctx) idl + in + List.rev refs, status + + +let maybe_error_many_udecls = function + | ((loc,id), Some _) -> + user_err ?loc ~hdr:"many_universe_declarations" + Pp.(str "When declaring multiple axioms in one command, " ++ + str "only the first is allowed a universe binder " ++ + str "(which will be shared by the whole block).") + | (_, None) -> () + +let process_assumptions_udecls kind l = + let udecl, first_id = match l with + | (coe, ((id, udecl)::rest, c))::rest' -> + List.iter maybe_error_many_udecls rest; + List.iter (fun (coe, (idl, c)) -> List.iter maybe_error_many_udecls idl) rest'; + udecl, id + | (_, ([], _))::_ | [] -> assert false + in + let () = match kind, udecl with + | (Discharge, _, _), Some _ when Lib.sections_are_opened () -> + let loc = fst first_id in + let msg = Pp.str "Section variables cannot be polymorphic." in + user_err ?loc msg + | _ -> () + in + udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l + +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 l = + if pi2 kind (* poly *) then + (* Separate declarations so that A B : Type puts A and B in different levels. *) + List.fold_right (fun (is_coe,(idl,c)) acc -> + List.fold_right (fun id acc -> + (is_coe, ([id], c)) :: acc) idl acc) + l [] + else l + in + (* We intepret all declarations in the same evar_map, i.e. as a telescope. *) + let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) -> + let sigma,(t,imps) = interp_assumption sigma env ienv [] c in + let env = + push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in + let ienv = List.fold_right (fun (_,id) ienv -> + let impls = compute_internalization_data env Variable t imps in + Id.Map.add id impls ienv) idl ienv in + ((sigma,env,ienv),((is_coe,idl),t,imps))) + (sigma,env,empty_internalization_env) l + in + let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in + (* The universe constraints come from the whole telescope. *) + let sigma = Evd.nf_constraints sigma in + let nf_evar c = EConstr.to_constr sigma (EConstr.of_constr c) in + let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> + let t = nf_evar t in + let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in + uvars, (coe,t,imps)) + Univ.LSet.empty l + in + let sigma = Evd.restrict_universe_context sigma uvars in + let uctx = Evd.check_univ_decl ~poly:(pi2 kind) sigma udecl in + let ubinders = Evd.universe_binders sigma in + pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) -> + let t = replace_vars subst t in + let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in + let subst' = List.map2 + (fun (_,id) (c,u) -> (id, Universes.constr_of_global_univ (c,u))) + idl refs + in + subst'@subst, status' && status, next_uctx uctx) + ([], true, uctx) l) diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli new file mode 100644 index 0000000000..2fa156abd8 --- /dev/null +++ b/vernac/comAssumption.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Constr +open Entries +open Globnames +open Vernacexpr +open Constrexpr +open Decl_kinds + +(** {6 Parameters/Assumptions} *) + +val do_assumptions : locality * polymorphic * assumption_object_kind -> + Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool + +(************************************************************************) +(** Internal API *) +(************************************************************************) + +(** Exported for Classes *) + +(** returns [false] if the assumption is neither local to a section, + nor in a module type and meant to be instantiated. *) +val declare_assumption : coercion_flag -> assumption_kind -> + types in_constant_universes_entry -> + Universes.universe_binders -> Impargs.manual_implicits -> + bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> + global_reference * Univ.Instance.t * bool diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml new file mode 100644 index 0000000000..883121479f --- /dev/null +++ b/vernac/comDefinition.ml @@ -0,0 +1,131 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Util +open Constr +open Environ +open Entries +open Termops +open Redexpr +open Declare +open Constrintern +open Pretyping + +open Context.Rel.Declaration + +(* Commands of the interface: Constant definitions *) + +let rec under_binders env sigma f n c = + if Int.equal n 0 then f env sigma (EConstr.of_constr c) else + match Constr.kind c with + | Lambda (x,t,c) -> + mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c) + | LetIn (x,b,t,c) -> + mkLetIn (x,b,t,under_binders (push_rel (LocalDef (x,b,t)) env) sigma f (n-1) c) + | _ -> assert false + +let red_constant_entry n ce sigma = function + | None -> ce + | Some red -> + let proof_out = ce.const_entry_body in + let env = Global.env () in + let (redfun, _) = reduction_of_red_expr env red in + let redfun env sigma c = + let (_, c) = redfun env sigma c in + EConstr.Unsafe.to_constr c + in + { ce with const_entry_body = Future.chain proof_out + (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) } + +let warn_implicits_in_term = + CWarnings.create ~name:"implicits-in-term" ~category:"implicits" + (fun () -> + strbrk "Implicit arguments declaration relies on type." ++ spc () ++ + strbrk "The term declares more implicits than the type here.") + +let interp_definition pl bl poly red_option c ctypopt = + let env = Global.env() in + let evd, decl = Univdecls.interp_univ_decl_opt env pl in + let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in + let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in + let nb_args = Context.Rel.nhyps ctx in + let evd,imps,ce = + match ctypopt with + None -> + let evd, subst = Evd.nf_univ_variables evd in + let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in + let env_bl = push_rel_context ctx env in + let evd, (c, imps2) = interp_constr_evars_impls ~impls env_bl evd c in + let c = EConstr.Unsafe.to_constr c in + let evd,nf = Evarutil.nf_evars_and_universes evd in + let body = nf (it_mkLambda_or_LetIn c ctx) in + let vars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in + let evd = Evd.restrict_universe_context evd vars in + let uctx = Evd.check_univ_decl ~poly evd decl in + evd, imps1@(Impargs.lift_implicits nb_args imps2), + definition_entry ~univs:uctx body + | Some ctyp -> + let evd, (ty, impsty) = interp_type_evars_impls ~impls env_bl evd ctyp in + let evd, subst = Evd.nf_univ_variables evd in + let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in + let env_bl = push_rel_context ctx env in + let evd, (c, imps2) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in + let c = EConstr.Unsafe.to_constr c in + let evd, nf = Evarutil.nf_evars_and_universes evd in + let body = nf (it_mkLambda_or_LetIn c ctx) in + let ty = EConstr.Unsafe.to_constr ty in + let typ = nf (Term.it_mkProd_or_LetIn ty ctx) in + let beq b1 b2 = if b1 then b2 else not b2 in + let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in + (* Check that all implicit arguments inferable from the term + are inferable from the type *) + let chk (key,va) = + impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *) + in + if not (try List.for_all chk imps2 with Not_found -> false) + then warn_implicits_in_term (); + let bodyvars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in + let tyvars = EConstr.universes_of_constr env evd (EConstr.of_constr ty) in + let vars = Univ.LSet.union bodyvars tyvars in + let evd = Evd.restrict_universe_context evd vars in + let uctx = Evd.check_univ_decl ~poly evd decl in + evd, imps1@(Impargs.lift_implicits nb_args impsty), + definition_entry ~types:typ ~univs:uctx body + in + (red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps) + +let check_definition (ce, evd, _, imps) = + check_evars_are_solved (Global.env ()) evd Evd.empty; + ce + +let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = + let (ce, evd, univdecl, imps as def) = + interp_definition univdecl bl (pi2 k) red_option c ctypopt + in + if program_mode then + let env = Global.env () in + let (c,ctx), sideff = Future.force ce.const_entry_body in + assert(Safe_typing.empty_private_constants = sideff); + assert(Univ.ContextSet.is_empty ctx); + let typ = match ce.const_entry_type with + | Some t -> t + | None -> EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr c)) + in + Obligations.check_evars env evd; + let obls, _, c, cty = + Obligations.eterm_obligations env ident evd 0 c typ + in + let ctx = Evd.evar_universe_context evd in + let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in + ignore(Obligations.add_definition + ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls) + else let ce = check_definition def in + ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps + (Lemmas.mk_hook + (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli new file mode 100644 index 0000000000..4a65c1e915 --- /dev/null +++ b/vernac/comDefinition.mli @@ -0,0 +1,30 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Entries +open Decl_kinds +open Redexpr +open Constrexpr + +(** {6 Definitions/Let} *) + +val do_definition : program_mode:bool -> + Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> + local_binder_expr list -> red_expr option -> constr_expr -> + constr_expr option -> unit Lemmas.declaration_hook -> unit + +(************************************************************************) +(** Internal API *) +(************************************************************************) + +(** Not used anywhere. *) +val interp_definition : + Vernacexpr.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 diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml new file mode 100644 index 0000000000..d648e293aa --- /dev/null +++ b/vernac/comFixpoint.ml @@ -0,0 +1,356 @@ +open Pp +open CErrors +open Util +open Constr +open Vars +open Termops +open Declare +open Names +open Constrexpr +open Constrexpr_ops +open Constrintern +open Decl_kinds +open Pretyping +open Evarutil +open Evarconv +open Misctypes +open Vernacexpr + +module RelDecl = Context.Rel.Declaration + +(* 3c| Fixpoints and co-fixpoints *) + +(* An (unoptimized) function that maps preorders to partial orders... + + Input: a list of associations (x,[y1;...;yn]), all yi distincts + and different of x, meaning x<=y1, ..., x<=yn + + Output: a list of associations (x,Inr [y1;...;yn]), collecting all + distincts yi greater than x, _or_, (x, Inl y) meaning that + x is in the same class as y (in which case, x occurs + nowhere else in the association map) + + partial_order : ('a * 'a list) list -> ('a * ('a,'a list) union) list +*) + +let rec partial_order cmp = function + | [] -> [] + | (x,xge)::rest -> + let rec browse res xge' = function + | [] -> + let res = List.map (function + | (z, Inr zge) when List.mem_f cmp x zge -> + (z, Inr (List.union cmp zge xge')) + | r -> r) res in + (x,Inr xge')::res + | y::xge -> + let rec link y = + try match List.assoc_f cmp y res with + | Inl z -> link z + | Inr yge -> + if List.mem_f cmp x yge then + let res = List.remove_assoc_f cmp y res in + let res = List.map (function + | (z, Inl t) -> + if cmp t y then (z, Inl x) else (z, Inl t) + | (z, Inr zge) -> + if List.mem_f cmp y zge then + (z, Inr (List.add_set cmp x (List.remove cmp y zge))) + else + (z, Inr zge)) res in + browse ((y,Inl x)::res) xge' (List.union cmp xge (List.remove cmp x yge)) + else + browse res (List.add_set cmp y (List.union cmp xge' yge)) xge + with Not_found -> browse res (List.add_set cmp y xge') xge + in link y + in browse (partial_order cmp rest) [] xge + +let non_full_mutual_message x xge y yge isfix rest = + let reason = + if Id.List.mem x yge then + Id.print y ++ str " depends on " ++ Id.print x ++ strbrk " but not conversely" + else if Id.List.mem y xge then + Id.print x ++ str " depends on " ++ Id.print y ++ strbrk " but not conversely" + else + Id.print y ++ str " and " ++ Id.print x ++ strbrk " are not mutually dependent" in + let e = if List.is_empty rest then reason else strbrk "e.g., " ++ reason in + let k = if isfix then "fixpoint" else "cofixpoint" in + let w = + if isfix + then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl() + else mt () in + strbrk "Not a fully mutually defined " ++ str k ++ fnl () ++ + str "(" ++ e ++ str ")." ++ fnl () ++ w + +let warn_non_full_mutual = + CWarnings.create ~name:"non-full-mutual" ~category:"fixpoints" + (fun (x,xge,y,yge,isfix,rest) -> + non_full_mutual_message x xge y yge isfix rest) + +let check_mutuality env evd isfix fixl = + let names = List.map fst fixl in + let preorder = + List.map (fun (id,def) -> + (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' (EConstr.of_constr def)) names)) + fixl in + let po = partial_order Id.equal preorder in + match List.filter (function (_,Inr _) -> true | _ -> false) po with + | (x,Inr xge)::(y,Inr yge)::rest -> + warn_non_full_mutual (x,xge,y,yge,isfix,rest) + | _ -> () + +type structured_fixpoint_expr = { + fix_name : Id.t; + fix_univs : universe_decl_expr option; + fix_annot : Id.t Loc.located option; + fix_binders : local_binder_expr list; + fix_body : constr_expr option; + fix_type : constr_expr +} + +let interp_fix_context ~cofix env sigma fix = + let before, after = if not cofix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in + let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars env sigma before in + let sigma, (impl_env', ((env'', ctx'), imps')) = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after in + let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in + sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) + +let interp_fix_ccl sigma impls (env,_) fix = + interp_type_evars_impls ~impls env sigma fix.fix_type + +let interp_fix_body env_rec sigma impls (_,ctx) fix ccl = + let open EConstr in + Option.cata (fun body -> + let env = push_rel_context ctx env_rec in + let sigma, body = interp_casted_constr_evars env sigma ~impls body ccl in + sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.fix_body + +let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx + +let prepare_recursive_declaration fixnames fixtypes fixdefs = + let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in + let names = List.map (fun id -> Name id) fixnames in + (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) + +(* Jump over let-bindings. *) + +let compute_possible_guardness_evidences (ctx,_,recindex) = + (* A recursive index is characterized by the number of lambdas to + skip before finding the relevant inductive argument *) + match recindex with + | Some i -> [i] + | None -> + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual + fixpoints ?) *) + List.interval 0 (Context.Rel.nhyps ctx - 1) + +type recursive_preentry = + Id.t list * constr option list * types list + +(* Wellfounded definition *) + +let contrib_name = "Program" +let subtac_dir = [contrib_name] +let tactics_module = subtac_dir @ ["Tactics"] + +let init_constant dir s sigma = + Evarutil.new_global sigma (Coqlib.coq_reference "Command" dir s) + +let fix_proto = init_constant tactics_module "fix_proto" + +let interp_recursive ~program_mode ~cofix fixl notations = + let open Context.Named.Declaration in + let open EConstr in + let env = Global.env() in + let fixnames = List.map (fun fix -> fix.fix_name) fixl in + + (* Interp arities allowing for unresolved types *) + let all_universes = + List.fold_right (fun sfe acc -> + match sfe.fix_univs , acc with + | None , acc -> acc + | x , None -> x + | Some ls , Some us -> + let lsu = ls.univdecl_instance and usu = us.univdecl_instance in + if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) 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, (fixctxs, fiximppairs, fixannots) = + on_snd List.split3 @@ + List.fold_left_map (fun sigma -> interp_fix_context env sigma ~cofix) sigma fixl in + let fixctximpenvs, fixctximps = List.split fiximppairs in + let sigma, (fixccls,fixcclimps) = + on_snd List.split @@ + List.fold_left3_map interp_fix_ccl sigma fixctximpenvs fixctxs fixl in + let fixtypes = List.map2 build_fix_type fixctxs fixccls in + let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in + let fiximps = List.map3 + (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps)) + fixctximps fixcclimps fixctxs in + let sigma, rec_sign = + List.fold_left2 + (fun (sigma, env') id t -> + if program_mode then + let sigma, sort = Typing.type_of ~refresh:true env sigma t in + let sigma, fixprot = + try + let sigma, h_term = fix_proto sigma in + let app = mkApp (h_term, [|sort; t|]) in + let _evd = ref sigma in + let res = Typing.e_solve_evars env _evd app in + !_evd, res + with e when CErrors.noncritical e -> sigma, t + in + sigma, LocalAssum (id,fixprot) :: env' + else sigma, LocalAssum (id,t) :: env') + (sigma,[]) fixnames fixtypes + in + let env_rec = push_named_context rec_sign env in + + (* Get interpretation metadatas *) + let fixtypes = List.map EConstr.Unsafe.to_constr fixtypes in + let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in + + (* Interp bodies with rollback because temp use of notations/implicit *) + let sigma, fixdefs = + Metasyntax.with_syntax_protection (fun () -> + List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations; + List.fold_left4_map + (fun sigma fixctximpenv -> interp_fix_body env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls)) + sigma fixctximpenvs fixctxs fixl fixccls) + () in + + (* Instantiate evars and check all are resolved *) + let sigma = solve_unif_constraints_with_heuristics env_rec sigma in + let sigma, nf = nf_evars_and_universes sigma in + let fixdefs = List.map (fun c -> Option.map EConstr.Unsafe.to_constr c) fixdefs in + let fixdefs = List.map (Option.map nf) fixdefs in + let fixtypes = List.map nf fixtypes in + let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in + + (* Build the fix declaration block *) + (env,rec_sign,decl,sigma), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots + +let check_recursive isfix env evd (fixnames,fixdefs,_) = + check_evars_are_solved env evd Evd.empty; + if List.for_all Option.has_some fixdefs then begin + let fixdefs = List.map Option.get fixdefs in + check_mutuality env evd isfix (List.combine fixnames fixdefs) + end + +let interp_fixpoint ~cofix l ntns = + let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l ntns in + check_recursive true env evd fix; + (fix,pl,Evd.evar_universe_context evd,info) + +let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = + if List.exists Option.is_empty fixdefs then + (* Some bodies to define by proof *) + let thms = + List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps)))) + fixnames fixtypes fiximps in + let init_tac = + Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) + fixdefs) in + let evd = Evd.from_ctx ctx in + Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint) + evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) + else begin + (* We shortcut the proof process *) + let fixdefs = List.map Option.get fixdefs in + let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in + let env = Global.env() in + let indexes = search_guard env indexes fixdecls in + let fiximps = List.map (fun (n,r,p) -> r) fiximps in + let vars = Univops.universes_of_constr env (mkFix ((indexes,0),fixdecls)) in + let fixdecls = + List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in + let evd = Evd.from_ctx ctx in + let evd = Evd.restrict_universe_context evd vars in + let ctx = Evd.check_univ_decl ~poly evd pl in + let pl = Evd.universe_binders evd in + let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in + ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) + fixnames fixdecls fixtypes fiximps); + (* Declare the recursive definitions *) + fixpoint_message (Some indexes) fixnames; + end; + (* Declare notations *) + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns + +let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns = + if List.exists Option.is_empty fixdefs then + (* Some bodies to define by proof *) + let thms = + List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps)))) + fixnames fixtypes fiximps in + let init_tac = + Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) + fixdefs) in + let evd = Evd.from_ctx ctx in + Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) + evd pl (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) + else begin + (* We shortcut the proof process *) + let fixdefs = List.map Option.get fixdefs in + let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in + let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in + let env = Global.env () in + let vars = Univops.universes_of_constr env (List.hd fixdecls) in + let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in + let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in + let evd = Evd.from_ctx ctx in + let evd = Evd.restrict_universe_context evd vars in + let ctx = Evd.check_univ_decl ~poly evd pl in + let pl = Evd.universe_binders evd in + ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) + fixnames fixdecls fixtypes fiximps); + (* Declare the recursive definitions *) + cofixpoint_message fixnames + end; + (* Declare notations *) + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns + +let extract_decreasing_argument limit = function + | (na,CStructRec) -> na + | (na,_) when not limit -> na + | _ -> user_err Pp.(str + "Only structural decreasing is supported for a non-Program Fixpoint") + +let extract_fixpoint_components limit l = + let fixl, ntnl = List.split l in + let fixl = List.map (fun (((_,id),pl),ann,bl,typ,def) -> + let ann = extract_decreasing_argument limit ann in + {fix_name = id; fix_annot = ann; fix_univs = pl; + fix_binders = bl; fix_body = def; fix_type = typ}) fixl in + fixl, List.flatten ntnl + +let extract_cofixpoint_components l = + let fixl, ntnl = List.split l in + List.map (fun (((_,id),pl),bl,typ,def) -> + {fix_name = id; fix_annot = None; fix_univs = pl; + fix_binders = bl; fix_body = def; fix_type = typ}) fixl, + List.flatten ntnl + +let check_safe () = + let open Declarations in + let flags = Environ.typing_flags (Global.env ()) in + flags.check_universes && flags.check_guarded + +let do_fixpoint local poly l = + let fixl, ntns = extract_fixpoint_components true l in + let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in + let possible_indexes = + List.map compute_possible_guardness_evidences info in + declare_fixpoint local poly fix possible_indexes ntns; + if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () + +let do_cofixpoint local poly l = + let fixl,ntns = extract_cofixpoint_components l in + let cofix = interp_fixpoint ~cofix:true fixl ntns in + declare_cofixpoint local poly cofix ntns; + if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli new file mode 100644 index 0000000000..2c84bd84d5 --- /dev/null +++ b/vernac/comFixpoint.mli @@ -0,0 +1,93 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Constr +open Decl_kinds +open Constrexpr +open Vernacexpr + +(** {6 Fixpoints and cofixpoints} *) + +(** Entry points for the vernacular commands Fixpoint and CoFixpoint *) + +val do_fixpoint : + (* When [false], assume guarded. *) + locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit + +val do_cofixpoint : + (* When [false], assume guarded. *) + locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit + +(************************************************************************) +(** Internal API *) +(************************************************************************) + +type structured_fixpoint_expr = { + fix_name : Id.t; + fix_univs : Vernacexpr.universe_decl_expr option; + fix_annot : Id.t Loc.located option; + fix_binders : local_binder_expr list; + fix_body : constr_expr option; + fix_type : constr_expr +} + +(** Typing global fixpoints and cofixpoint_expr *) + +(** Exported for Program *) +val interp_recursive : + (* Misc arguments *) + program_mode:bool -> cofix:bool -> + (* Notations of the fixpoint / should that be folded in the previous argument? *) + structured_fixpoint_expr list -> decl_notation list -> + + (* env / signature / univs / evar_map *) + (Environ.env * EConstr.named_context * Univdecls.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 *) + (EConstr.rel_context * Impargs.manual_explicitation list * int option) list + +(** Exported for Funind *) + +(** Extracting the semantical components out of the raw syntax of + (co)fixpoints declarations *) + +val extract_fixpoint_components : bool -> + (fixpoint_expr * decl_notation list) list -> + structured_fixpoint_expr list * decl_notation list + +val extract_cofixpoint_components : + (cofixpoint_expr * decl_notation list) list -> + structured_fixpoint_expr list * decl_notation list + +type recursive_preentry = + Id.t list * constr option list * types list + +val interp_fixpoint : + cofix:bool -> + structured_fixpoint_expr list -> decl_notation list -> + recursive_preentry * Univdecls.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 * + (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 * + (Context.Rel.t * Impargs.manual_implicits * int option) list -> + decl_notation list -> unit + +(** Very private function, do not use *) +val compute_possible_guardness_evidences : + ('a, 'b) Context.Rel.pt * 'c * int option -> int list diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml new file mode 100644 index 0000000000..f3f50f41dd --- /dev/null +++ b/vernac/comInductive.ml @@ -0,0 +1,456 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open CErrors +open Sorts +open Util +open Constr +open Termops +open Environ +open Declare +open Names +open Libnames +open Globnames +open Nameops +open Constrexpr +open Constrexpr_ops +open Constrintern +open Nametab +open Impargs +open Reductionops +open Indtypes +open Decl_kinds +open Pretyping +open Evarutil +open Indschemes +open Misctypes +open Context.Rel.Declaration +open Entries + +module RelDecl = Context.Rel.Declaration + +(* 3b| Mutual inductive definitions *) + +let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function + | CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c) + | CLetIn (na,b,t,c) -> CLetIn (na,b,t,complete_conclusion a cs c) + | CHole (k, _, _) -> + let (has_no_args,name,params) = a in + if not has_no_args then + user_err ?loc + (strbrk"Cannot infer the non constant arguments of the conclusion of " + ++ Id.print cs ++ str "."); + let args = List.map (fun id -> CAst.make ?loc @@ CRef(Ident(loc,id),None)) params in + CAppExpl ((None,Ident(loc,name),None),List.rev args) + | c -> c + ) + +let push_types env idl tl = + List.fold_left2 (fun env id t -> Environ.push_rel (LocalAssum (Name id,t)) env) + env idl tl + +type structured_one_inductive_expr = { + ind_name : Id.t; + ind_univs : Vernacexpr.universe_decl_expr option; + ind_arity : constr_expr; + ind_lc : (Id.t * constr_expr) list +} + +type structured_inductive_expr = + local_binder_expr list * structured_one_inductive_expr list + +let minductive_message warn = function + | [] -> user_err Pp.(str "No inductive definition.") + | [x] -> (Id.print x ++ str " is defined" ++ + if warn then str " as a non-primitive record" else mt()) + | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ + spc () ++ str "are defined") + +let check_all_names_different indl = + let ind_names = List.map (fun ind -> ind.ind_name) indl in + let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in + let l = List.duplicates Id.equal ind_names in + let () = match l with + | [] -> () + | t :: _ -> raise (InductiveError (SameNamesTypes t)) + in + let l = List.duplicates Id.equal cstr_names in + let () = match l with + | [] -> () + | c :: _ -> raise (InductiveError (SameNamesConstructors (List.hd l))) + in + let l = List.intersect Id.equal ind_names cstr_names in + match l with + | [] -> () + | _ -> raise (InductiveError (SameNamesOverlap l)) + +let mk_mltype_data sigma env assums arity indname = + let is_ml_type = is_sort env sigma (EConstr.of_constr arity) in + (is_ml_type,indname,assums) + +let prepare_param = function + | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t + | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b + +(** Make the arity conclusion flexible to avoid generating an upper bound universe now, + only if the universe does not appear anywhere else. + This is really a hack to stay compatible with the semantics of template polymorphic + inductives which are recognized when a "Type" appears at the end of the conlusion in + the source syntax. *) + +let rec check_anonymous_type ind = + let open Glob_term in + match DAst.get ind with + | GSort (GType []) -> true + | GProd ( _, _, _, e) + | GLetIn (_, _, _, e) + | GLambda (_, _, _, e) + | GApp (e, _) + | GCast (e, _) -> check_anonymous_type e + | _ -> false + +let make_conclusion_flexible sigma ty poly = + if poly && Term.isArity ty then + let _, concl = Term.destArity ty in + match concl with + | Type u -> + (match Univ.universe_level u with + | Some u -> + Evd.make_flexible_variable sigma ~algebraic:true u + | None -> sigma) + | _ -> sigma + else sigma + +let is_impredicative env u = + u = Prop Null || (is_impredicative_set env && u = Prop Pos) + +let interp_ind_arity env sigma ind = + let c = intern_gen IsType env ind.ind_arity in + let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in + let sigma,t = understand_tcc env sigma ~expected_type:IsType c in + let pseudo_poly = check_anonymous_type c in + let () = if not (Reductionops.is_arity env sigma t) then + user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity") + in + let t = EConstr.Unsafe.to_constr t in + sigma, (t, pseudo_poly, impls) + +let interp_cstrs env sigma impls mldata arity ind = + let cnames,ctyps = List.split ind.ind_lc in + (* Complete conclusions of constructor types if given in ML-style syntax *) + let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in + (* Interpret the constructor types *) + let sigma, (ctyps'', cimpls) = + on_snd List.split @@ + List.fold_left_map (fun sigma l -> + on_snd (on_fst EConstr.Unsafe.to_constr) @@ + interp_type_evars_impls env sigma ~impls l) sigma ctyps' in + sigma, (cnames, ctyps'', cimpls) + +let sign_level env evd sign = + fst (List.fold_right + (fun d (lev,env) -> + match d with + | LocalDef _ -> lev, push_rel d env + | LocalAssum _ -> + let s = destSort (Reduction.whd_all env + (EConstr.Unsafe.to_constr (nf_evar evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d)))))) + in + let u = univ_of_sort s in + (Univ.sup u lev, push_rel d env)) + sign (Univ.type0m_univ,env)) + +let sup_list min = List.fold_left Univ.sup min + +let extract_level env evd min tys = + let sorts = List.map (fun ty -> + let ctx, concl = Reduction.dest_prod_assum env ty in + sign_level env evd (LocalAssum (Anonymous, concl) :: ctx)) tys + in sup_list min sorts + +let is_flexible_sort evd u = + match Univ.Universe.level u with + | Some l -> Evd.is_flexible_level evd l + | None -> false + +let inductive_levels env evd poly arities inds = + let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in + let levels = List.map (fun (x,(ctx,a)) -> + if a = Prop Null then None + else Some (univ_of_sort a)) destarities + in + let cstrs_levels, min_levels, sizes = + CList.split3 + (List.map2 (fun (_,tys,_) (arity,(ctx,du)) -> + let len = List.length tys in + let minlev = Sorts.univ_of_sort du in + let minlev = + if len > 1 && not (is_impredicative env du) then + Univ.sup minlev Univ.type0_univ + else minlev + in + let minlev = + (** Indices contribute. *) + if Indtypes.is_indices_matter () && List.length ctx > 0 then ( + let ilev = sign_level env evd ctx in + Univ.sup ilev minlev) + else minlev + in + let clev = extract_level env evd minlev tys in + (clev, minlev, len)) inds destarities) + in + (* Take the transitive closure of the system of constructors *) + (* level constraints and remove the recursive dependencies *) + let levels' = Universes.solve_constraints_system (Array.of_list levels) + (Array.of_list cstrs_levels) (Array.of_list min_levels) + in + let evd, arities = + CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len -> + if is_impredicative env du then + (** Any product is allowed here. *) + evd, arity :: arities + else (** If in a predicative sort, or asked to infer the type, + we take the max of: + - indices (if in indices-matter mode) + - constructors + - Type(1) if there is more than 1 constructor + *) + (** Constructors contribute. *) + let evd = + if Sorts.is_set du then + if not (Evd.check_leq evd cu Univ.type0_univ) then + raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType) + else evd + else evd + (* Evd.set_leq_sort env evd (Type cu) du *) + in + let evd = + if len >= 2 && Univ.is_type0m_univ cu then + (** "Polymorphic" type constraint and more than one constructor, + should not land in Prop. Add constraint only if it would + land in Prop directly (no informative arguments as well). *) + Evd.set_leq_sort env evd (Prop Pos) du + else evd + in + let duu = Sorts.univ_of_sort du in + let evd = + if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then + if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then + Evd.set_eq_sort env evd (Prop Null) du + else evd + else Evd.set_eq_sort env evd (Type cu) du + in + (evd, arity :: arities)) + (evd,[]) (Array.to_list levels') destarities sizes + in evd, List.rev arities + +let check_named (loc, na) = match na with +| Name _ -> () +| Anonymous -> + let msg = str "Parameters must be named." in + user_err ?loc msg + + +let check_param = function +| CLocalDef (na, _, _) -> check_named na +| CLocalAssum (nas, Default _, _) -> List.iter check_named nas +| CLocalAssum (nas, Generalized _, _) -> () +| CLocalPattern (loc,_) -> + Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.") + +let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = + check_all_names_different indl; + 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, (impls, ((env_params, ctx_params), userimpls)) = + interp_context_evars env0 sigma paramsl + in + let ctx_params = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx_params in + let indnames = List.map (fun ind -> ind.ind_name) indl in + + (* Names of parameters as arguments of the inductive type (defs removed) *) + let assums = List.filter is_local_assum ctx_params in + let params = List.map (RelDecl.get_name %> Name.get_id) assums in + + (* Interpret the arities *) + let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in + + let fullarities = List.map (fun (c, _, _) -> Term.it_mkProd_or_LetIn c ctx_params) arities in + let env_ar = push_types env0 indnames fullarities in + let env_ar_params = push_rel_context ctx_params env_ar in + + (* Compute interpretation metadatas *) + let indimpls = List.map (fun (_, _, impls) -> userimpls @ + lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in + let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in + let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in + let ntn_impls = compute_internalization_env env0 (Inductive (params,true)) indnames fullarities indimpls in + let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in + + let sigma, constructors = + Metasyntax.with_syntax_protection (fun () -> + (* Temporary declaration of notations and scopes *) + List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations; + (* Interpret the constructor types *) + List.fold_left3_map (fun sigma -> interp_cstrs env_ar_params sigma impls) sigma mldatas arities indl) + () in + + (* Try further to solve evars, and instantiate them *) + let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in + (* Compute renewed arities *) + let sigma, nf = nf_evars_and_universes sigma in + let arities = List.map nf arities in + let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in + let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in + let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in + let sigma, nf' = nf_evars_and_universes sigma in + let nf x = nf' (nf x) in + let arities = List.map nf' arities in + let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in + let ctx_params = Context.Rel.map nf ctx_params in + let uctx = Evd.check_univ_decl ~poly sigma decl in + List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities; + Context.Rel.iter (fun c -> check_evars env0 Evd.empty sigma (EConstr.of_constr c)) ctx_params; + List.iter (fun (_,ctyps,_) -> + List.iter (fun c -> check_evars env_ar_params Evd.empty sigma (EConstr.of_constr c)) ctyps) + constructors; + + (* Build the inductive entries *) + let entries = List.map4 (fun ind arity template (cnames,ctypes,cimpls) -> { + mind_entry_typename = ind.ind_name; + mind_entry_arity = arity; + mind_entry_template = template; + mind_entry_consnames = cnames; + mind_entry_lc = ctypes + }) indl arities aritypoly constructors in + let impls = + let len = Context.Rel.nhyps ctx_params in + List.map2 (fun indimpls (_,_,cimpls) -> + indimpls, List.map (fun impls -> + userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors + in + let univs = + match uctx with + | Polymorphic_const_entry uctx -> + if cum then + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) + else Polymorphic_ind_entry uctx + | Monomorphic_const_entry uctx -> + Monomorphic_ind_entry uctx + in + (* Build the mutual inductive entry *) + let mind_ent = + { mind_entry_params = List.map prepare_param ctx_params; + mind_entry_record = None; + mind_entry_finite = finite; + mind_entry_inds = entries; + mind_entry_private = if prv then Some false else None; + mind_entry_universes = univs; + } + in + (if poly && cum then + Inductiveops.infer_inductive_subtyping env_ar sigma mind_ent + else mind_ent), Evd.universe_binders sigma, impls + +(* Very syntactical equality *) +let eq_local_binders bl1 bl2 = + List.equal local_binder_eq bl1 bl2 + +let extract_coercions indl = + let mkqid (_,((_,id),_)) = qualid_of_ident id in + let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in + List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl)) + +let extract_params indl = + let paramsl = List.map (fun (_,params,_,_) -> params) indl in + match paramsl with + | [] -> anomaly (Pp.str "empty list of inductive types.") + | params::paramsl -> + if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str + "Parameters should be syntactically the same for each inductive type."); + params + +let extract_inductive indl = + List.map (fun (((_,indname),pl),_,ar,lc) -> { + ind_name = indname; ind_univs = pl; + ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar; + ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc + }) indl + +let extract_mutual_inductive_declaration_components indl = + let indl,ntnl = List.split indl in + let params = extract_params indl in + let coes = extract_coercions indl in + let indl = extract_inductive indl in + (params,indl), coes, List.flatten ntnl + +let is_recursive mie = + let rec is_recursive_constructor lift typ = + match Constr.kind typ with + | Prod (_,arg,rest) -> + not (EConstr.Vars.noccurn Evd.empty (** FIXME *) lift (EConstr.of_constr arg)) || + is_recursive_constructor (lift+1) rest + | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest + | _ -> false + in + match mie.mind_entry_inds with + | [ind] -> + let nparams = List.length mie.mind_entry_params in + List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc + | _ -> false + +let declare_mutual_inductive_with_eliminations mie pl impls = + (* spiwack: raises an error if the structure is supposed to be non-recursive, + but isn't *) + begin match mie.mind_entry_finite with + | BiFinite when is_recursive mie -> + if Option.has_some mie.mind_entry_record then + user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") + else + user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")) + | _ -> () + end; + let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in + let (_, kn), prim = declare_mind mie in + let mind = Global.mind_of_delta_kn kn in + List.iteri (fun i (indimpls, constrimpls) -> + let ind = (mind,i) in + let gr = IndRef ind in + maybe_declare_manual_implicits false gr indimpls; + Declare.declare_univ_binders gr pl; + List.iteri + (fun j impls -> + maybe_declare_manual_implicits false + (ConstructRef (ind, succ j)) impls) + constrimpls) + impls; + let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in + Flags.if_verbose Feedback.msg_info (minductive_message warn_prim names); + if mie.mind_entry_private == None + then declare_default_schemes mind; + mind + +type one_inductive_impls = + Impargs.manual_explicitation list (* for inds *)* + Impargs.manual_explicitation list list (* for constrs *) + +let do_mutual_inductive indl cum poly prv finite = + let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in + (* Interpret the types *) + let mie,pl,impls = interp_mutual_inductive indl ntns cum poly prv finite in + (* Declare the mutual inductive block with its associated schemes *) + ignore (declare_mutual_inductive_with_eliminations mie pl impls); + (* Declare the possible notations of inductive types *) + List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; + (* Declare the coercions *) + List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes; + (* If positivity is assumed declares itself as unsafe. *) + if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli new file mode 100644 index 0000000000..82ea131e1c --- /dev/null +++ b/vernac/comInductive.mli @@ -0,0 +1,65 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Entries +open Libnames +open Vernacexpr +open Constrexpr +open Decl_kinds + +(** {6 Inductive and coinductive types} *) + +(** Entry points for the vernacular commands Inductive and CoInductive *) + +val do_mutual_inductive : + (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> + polymorphic -> private_flag -> Declarations.recursivity_kind -> unit + +(************************************************************************) +(** Internal API *) +(************************************************************************) + +(** Exported for Record and Funind *) + +(** Registering a mutual inductive definition together with its + associated schemes *) + +type one_inductive_impls = + Impargs.manual_implicits (** for inds *)* + Impargs.manual_implicits list (** for constrs *) + +val declare_mutual_inductive_with_eliminations : + mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list -> + MutInd.t + +(** Exported for Funind *) + +(** Extracting the semantical components out of the raw syntax of mutual + inductive declarations *) + +type structured_one_inductive_expr = { + ind_name : Id.t; + ind_univs : Vernacexpr.universe_decl_expr option; + ind_arity : constr_expr; + ind_lc : (Id.t * constr_expr) list +} + +type structured_inductive_expr = + local_binder_expr list * structured_one_inductive_expr list + +val extract_mutual_inductive_declaration_components : + (one_inductive_expr * decl_notation list) list -> + structured_inductive_expr * (*coercions:*) qualid list * decl_notation list + +(** Typing mutual inductive definitions *) + +val interp_mutual_inductive : + structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> + polymorphic -> private_flag -> Declarations.recursivity_kind -> + mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml new file mode 100644 index 0000000000..a9a91e3043 --- /dev/null +++ b/vernac/comProgramFixpoint.ml @@ -0,0 +1,342 @@ +open Pp +open CErrors +open Util +open Constr +open Entries +open Vars +open Declare +open Names +open Libnames +open Globnames +open Nameops +open Constrexpr +open Constrexpr_ops +open Constrintern +open Decl_kinds +open Evarutil +open Context.Rel.Declaration +open ComFixpoint + +module RelDecl = Context.Rel.Declaration + +(* Wellfounded definition *) + +open Coqlib + +let contrib_name = "Program" +let subtac_dir = [contrib_name] +let fixsub_module = subtac_dir @ ["Wf"] +(* let tactics_module = subtac_dir @ ["Tactics"] *) + +let init_reference dir s () = Coqlib.coq_reference "Command" dir s +let init_constant dir s sigma = + Evarutil.new_global sigma (Coqlib.coq_reference "Command" dir s) + +let make_ref l s = init_reference l s +(* let fix_proto = init_constant tactics_module "fix_proto" *) +let fix_sub_ref = make_ref fixsub_module "Fix_sub" +let measure_on_R_ref = make_ref fixsub_module "MR" +let well_founded = init_constant ["Init"; "Wf"] "well_founded" +let mkSubset sigma name typ prop = + let open EConstr in + let sigma, app_h = Evarutil.new_global sigma (delayed_force build_sigma).typ in + sigma, mkApp (app_h, [| typ; mkLambda (name, typ, prop) |]) + +let sigT = Lazy.from_fun build_sigma_type + +let make_qref s = Qualid (Loc.tag @@ qualid_of_string s) +let lt_ref = make_qref "Init.Peano.lt" + +let rec telescope sigma l = + let open EConstr in + let open Vars in + match l with + | [] -> assert false + | [LocalAssum (n, t)] -> + sigma, t, [LocalDef (n, mkRel 1, t)], mkRel 1 + | LocalAssum (n, t) :: tl -> + let sigma, ty, tys, (k, constr) = + List.fold_left + (fun (sigma, ty, tys, (k, constr)) decl -> + let t = RelDecl.get_type decl in + let pred = mkLambda (RelDecl.get_name decl, t, ty) in + let sigma, ty = Evarutil.new_global sigma (Lazy.force sigT).typ in + let sigma, intro = Evarutil.new_global sigma (Lazy.force sigT).intro in + let sigty = mkApp (ty, [|t; pred|]) in + let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in + (sigma, sigty, pred :: tys, (succ k, intro))) + (sigma, t, [], (2, mkRel 1)) tl + in + let sigma, last, subst = List.fold_right2 + (fun pred decl (sigma, prev, subst) -> + let t = RelDecl.get_type decl in + let sigma, p1 = Evarutil.new_global sigma (Lazy.force sigT).proj1 in + let sigma, p2 = Evarutil.new_global sigma (Lazy.force sigT).proj2 in + let proj1 = applist (p1, [t; pred; prev]) in + let proj2 = applist (p2, [t; pred; prev]) in + (sigma, lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst)) + (List.rev tys) tl (sigma, mkRel 1, []) + in sigma, ty, (LocalDef (n, last, t) :: subst), constr + + | LocalDef (n, b, t) :: tl -> + let sigma, ty, subst, term = telescope sigma tl in + sigma, ty, (LocalDef (n, b, t) :: subst), lift 1 term + +let nf_evar_context sigma ctx = + List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx + +let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = + let open EConstr in + let open Vars in + 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, (_, ((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 + let sigma, top_arity = interp_type_evars top_env sigma arityc in + let full_arity = it_mkProd_or_LetIn top_arity binders_rel in + let sigma, argtyp, letbinders, make = telescope sigma binders_rel in + let argname = Id.of_string "recarg" in + let arg = LocalAssum (Name argname, argtyp) in + let binders = letbinders @ [arg] in + let binders_env = push_rel_context binders_rel env in + let sigma, (rel, _) = interp_constr_evars_impls env sigma r in + let relty = Typing.unsafe_type_of env sigma rel in + let relargty = + let error () = + user_err ?loc:(constr_loc r) + ~hdr:"Command.build_wellfounded" + (Printer.pr_econstr_env env sigma rel ++ str " is not an homogeneous binary relation.") + in + try + let ctx, ar = Reductionops.splay_prod_n env sigma 2 relty in + match ctx, EConstr.kind sigma ar with + | [LocalAssum (_,t); LocalAssum (_,u)], Sort s + when Sorts.is_prop (ESorts.kind sigma s) && Reductionops.is_conv env sigma t u -> t + | _, _ -> error () + with e when CErrors.noncritical e -> error () + in + let sigma, measure = interp_casted_constr_evars binders_env sigma measure relargty in + let sigma, wf_rel, wf_rel_fun, measure_fn = + let measure_body, measure = + it_mkLambda_or_LetIn measure letbinders, + it_mkLambda_or_LetIn measure binders + in + let sigma, comb = Evarutil.new_global sigma (delayed_force measure_on_R_ref) in + let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in + let wf_rel_fun x y = + mkApp (rel, [| subst1 x measure_body; + subst1 y measure_body |]) + in sigma, wf_rel, wf_rel_fun, measure + in + let sigma, wf_term = well_founded sigma in + let wf_proof = mkApp (wf_term, [| argtyp ; wf_rel |]) in + let argid' = Id.of_string (Id.to_string argname ^ "'") in + let wfarg sigma len = + let sigma, ss_term = mkSubset sigma (Name argid') argtyp (wf_rel_fun (mkRel 1) (mkRel (len + 1))) in + sigma, LocalAssum (Name argid', ss_term) + in + let sigma, intern_bl = + let sigma, wfa = wfarg sigma 1 in + sigma, wfa :: [arg] + in + let _intern_env = push_rel_context intern_bl env in + let sigma, proj = Evarutil.new_global sigma (delayed_force build_sigma).Coqlib.proj1 in + let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in + let projection = (* in wfarg :: arg :: before *) + mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |]) + in + let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in + let intern_arity = substl [projection] top_arity_let in + (* substitute the projection of wfarg for something, + now intern_arity is in wfarg :: arg *) + let sigma, wfa = wfarg sigma 1 in + let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfa] in + let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in + let sigma, curry_fun = + let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in + let sigma, intro = Evarutil.new_global sigma (delayed_force build_sigma).Coqlib.intro in + let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in + let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in + let rcurry = mkApp (rel, [| measure; lift len measure |]) in + let lam = LocalAssum (Name (Id.of_string "recproof"), rcurry) in + let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in + let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in + sigma, LocalDef (Name recname, body, ty) + in + let fun_bl = intern_fun_binder :: [arg] in + let lift_lets = lift_rel_context 1 letbinders in + let sigma, intern_body = + let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in + let (r, l, impls, scopes) = + Constrintern.compute_internalization_data env + Constrintern.Recursive (EConstr.Unsafe.to_constr full_arity) impls + in + let newimpls = Id.Map.singleton recname + (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))], + scopes @ [None]) in + interp_casted_constr_evars (push_rel_context ctx env) sigma + ~impls:newimpls body (lift 1 top_arity) + in + let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in + let prop = mkLambda (Name argname, argtyp, top_arity_let) in + (* XXX: Previous code did parallel evdref update, so possible old + weak ordering semantics may bite here. *) + let sigma, def = + let sigma, h_a_term = Evarutil.new_global sigma (delayed_force fix_sub_ref) in + let sigma, h_e_term = Evarutil.new_evar env sigma + ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in + sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |]) + in + let _evd = ref sigma in + let def = Typing.e_solve_evars env _evd def in + let sigma = !_evd in + let sigma = Evarutil.nf_evar_map sigma in + let def = mkApp (def, [|intern_body_lam|]) in + let binders_rel = nf_evar_context sigma binders_rel in + let binders = nf_evar_context sigma binders in + let top_arity = Evarutil.nf_evar sigma top_arity in + let hook, recname, typ = + if List.length binders_rel > 1 then + let name = add_suffix recname "_func" in + (* XXX: Mutating the evar_map in the hook! *) + (* XXX: Likely the sigma is out of date when the hook is called .... *) + let hook sigma l gr _ = + let sigma, h_body = Evarutil.new_global sigma gr in + let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in + let ty = it_mkProd_or_LetIn top_arity binders_rel in + let ty = EConstr.Unsafe.to_constr ty in + let univs = Evd.check_univ_decl ~poly sigma decl in + (*FIXME poly? *) + let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in + (** FIXME: include locality *) + let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in + let gr = ConstRef c in + let () = Universes.register_universe_binders gr (Evd.universe_binders sigma) in + if Impargs.is_implicit_args () || not (List.is_empty impls) then + Impargs.declare_manual_implicits false gr [impls] + in + let typ = it_mkProd_or_LetIn top_arity binders in + hook, name, typ + else + let typ = it_mkProd_or_LetIn top_arity binders_rel in + let hook sigma l gr _ = + if Impargs.is_implicit_args () || not (List.is_empty impls) then + Impargs.declare_manual_implicits false gr [impls] + in hook, recname, typ + in + (* XXX: Capturing sigma here... bad bad *) + let hook = Lemmas.mk_hook (hook sigma) in + let fullcoqc = EConstr.to_constr sigma def in + let fullctyp = EConstr.to_constr sigma typ in + Obligations.check_evars env sigma; + let evars, _, evars_def, evars_typ = + Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp + in + let ctx = Evd.evar_universe_context sigma in + ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl + evars_typ ctx evars ~hook) + +let out_def = function + | Some def -> def + | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.") + +let collect_evars_of_term evd c ty = + let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in + Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) + evars (Evd.from_ctx (Evd.evar_universe_context evd)) + +let do_program_recursive local poly fixkind fixl ntns = + let cofix = fixkind = Obligations.IsCoFixpoint in + let (env, rec_sign, pl, evd), fix, info = + interp_recursive ~cofix ~program_mode:true fixl ntns + in + (* Program-specific code *) + (* Get the interesting evars, those that were not instanciated *) + let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in + (* Solve remaining evars *) + let evd = nf_evar_map_undefined evd in + let collect_evars id def typ imps = + (* Generalize by the recursive prototypes *) + let def = + EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign) + and typ = + EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign) + in + let evm = collect_evars_of_term evd def typ in + let evars, _, def, typ = + Obligations.eterm_obligations env id evm + (List.length rec_sign) def typ + in (id, def, typ, imps, evars) + in + let (fixnames,fixdefs,fixtypes) = fix in + let fiximps = List.map pi2 info in + let fixdefs = List.map out_def fixdefs in + let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in + let () = if not cofix then begin + let possible_indexes = List.map ComFixpoint.compute_possible_guardness_evidences info in + let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), + Array.of_list fixtypes, + Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) + in + let indexes = + Pretyping.search_guard (Global.env ()) possible_indexes fixdecls in + List.iteri (fun i _ -> + Inductive.check_fix env + ((indexes,i),fixdecls)) + fixl + end in + let ctx = Evd.evar_universe_context evd in + let kind = match fixkind with + | Obligations.IsFixpoint _ -> (local, poly, Fixpoint) + | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint) + in + Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind + +let do_program_fixpoint local poly l = + let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in + match g, l with + | [(n, CWfRec r)], [((((_,id),pl),_,bl,typ,def),ntn)] -> + let recarg = + match n with + | Some n -> mkIdentC (snd n) + | None -> + user_err ~hdr:"do_program_fixpoint" + (str "Recursive argument required for well-founded fixpoints") + in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn + + | [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] -> + build_wellfounded (id, pl, n, bl, typ, out_def def) poly + (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn + + | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g -> + let fixl,ntns = extract_fixpoint_components true l in + let fixkind = Obligations.IsFixpoint g in + do_program_recursive local poly fixkind fixl ntns + + | _, _ -> + user_err ~hdr:"do_program_fixpoint" + (str "Well-founded fixpoints not allowed in mutually recursive blocks") + +let extract_cofixpoint_components l = + let fixl, ntnl = List.split l in + List.map (fun (((_,id),pl),bl,typ,def) -> + {fix_name = id; fix_annot = None; fix_univs = pl; + fix_binders = bl; fix_body = def; fix_type = typ}) fixl, + List.flatten ntnl + +let check_safe () = + let open Declarations in + let flags = Environ.typing_flags (Global.env ()) in + flags.check_universes && flags.check_guarded + +let do_fixpoint local poly l = + do_program_fixpoint local poly l; + if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () + +let do_cofixpoint local poly l = + let fixl,ntns = extract_cofixpoint_components l in + do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns; + if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli new file mode 100644 index 0000000000..943cb8efe6 --- /dev/null +++ b/vernac/comProgramFixpoint.mli @@ -0,0 +1,12 @@ +open Decl_kinds +open Vernacexpr + +(** Special Fixpoint handling when command is activated. *) + +val do_fixpoint : + (* When [false], assume guarded. *) + locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit + +val do_cofixpoint : + (* When [false], assume guarded. *) + locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit diff --git a/vernac/command.ml b/vernac/command.ml deleted file mode 100644 index 23be2c3082..0000000000 --- a/vernac/command.ml +++ /dev/null @@ -1,1364 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Pp -open CErrors -open Sorts -open Util -open Constr -open Vars -open Termops -open Environ -open Redexpr -open Declare -open Names -open Libnames -open Globnames -open Nameops -open Constrexpr -open Constrexpr_ops -open Constrintern -open Nametab -open Impargs -open Reductionops -open Indtypes -open Decl_kinds -open Pretyping -open Evarutil -open Evarconv -open Indschemes -open Misctypes -open Vernacexpr -open Context.Rel.Declaration -open Entries - -module RelDecl = Context.Rel.Declaration - -let do_universe poly l = Declare.do_universe poly l -let do_constraint poly l = Declare.do_constraint poly l - -let rec under_binders env sigma f n c = - if Int.equal n 0 then f env sigma (EConstr.of_constr c) else - match Constr.kind c with - | Lambda (x,t,c) -> - mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c) - | LetIn (x,b,t,c) -> - mkLetIn (x,b,t,under_binders (push_rel (LocalDef (x,b,t)) env) sigma f (n-1) c) - | _ -> assert false - -let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function - | CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c) - | CLetIn (na,b,t,c) -> CLetIn (na,b,t,complete_conclusion a cs c) - | CHole (k, _, _) -> - let (has_no_args,name,params) = a in - if not has_no_args then - user_err ?loc - (strbrk"Cannot infer the non constant arguments of the conclusion of " - ++ Id.print cs ++ str "."); - let args = List.map (fun id -> CAst.make ?loc @@ CRef(Ident(loc,id),None)) params in - CAppExpl ((None,Ident(loc,name),None),List.rev args) - | c -> c - ) - -(* Commands of the interface *) - -(* 1| Constant definitions *) - -let red_constant_entry n ce sigma = function - | None -> ce - | Some red -> - let proof_out = ce.const_entry_body in - let env = Global.env () in - let (redfun, _) = reduction_of_red_expr env red in - let redfun env sigma c = - let (_, c) = redfun env sigma c in - EConstr.Unsafe.to_constr c - in - { ce with const_entry_body = Future.chain proof_out - (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) } - -let warn_implicits_in_term = - CWarnings.create ~name:"implicits-in-term" ~category:"implicits" - (fun () -> - strbrk "Implicit arguments declaration relies on type." ++ spc () ++ - strbrk "The term declares more implicits than the type here.") - -let interp_definition pl bl poly red_option c ctypopt = - let env = Global.env() in - let evd, decl = Univdecls.interp_univ_decl_opt env pl in - let evdref = ref evd in - let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in - let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in - let nb_args = Context.Rel.nhyps ctx in - let imps,ce = - match ctypopt with - None -> - let subst = evd_comb0 Evd.nf_univ_variables evdref in - let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in - let env_bl = push_rel_context ctx env in - let c, imps2 = interp_constr_evars_impls ~impls env_bl evdref c in - let c = EConstr.Unsafe.to_constr c in - let nf,subst = Evarutil.e_nf_evars_and_universes evdref in - let body = nf (it_mkLambda_or_LetIn c ctx) in - let vars = EConstr.universes_of_constr env !evdref (EConstr.of_constr body) in - let () = evdref := Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl ~poly !evdref decl in - imps1@(Impargs.lift_implicits nb_args imps2), - definition_entry ~univs:uctx body - | Some ctyp -> - let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in - let subst = evd_comb0 Evd.nf_univ_variables evdref in - let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in - let env_bl = push_rel_context ctx env in - let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in - let c = EConstr.Unsafe.to_constr c in - let nf, subst = Evarutil.e_nf_evars_and_universes evdref in - let body = nf (it_mkLambda_or_LetIn c ctx) in - let ty = EConstr.Unsafe.to_constr ty in - let typ = nf (Term.it_mkProd_or_LetIn ty ctx) in - let beq b1 b2 = if b1 then b2 else not b2 in - let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in - (* Check that all implicit arguments inferable from the term - are inferable from the type *) - let chk (key,va) = - impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *) - in - if not (try List.for_all chk imps2 with Not_found -> false) - then warn_implicits_in_term (); - let bodyvars = EConstr.universes_of_constr env !evdref (EConstr.of_constr body) in - let tyvars = EConstr.universes_of_constr env !evdref (EConstr.of_constr ty) in - let vars = Univ.LSet.union bodyvars tyvars in - let () = evdref := Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl ~poly !evdref decl in - imps1@(Impargs.lift_implicits nb_args impsty), - definition_entry ~types:typ ~univs:uctx body - in - (red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, imps) - -let check_definition (ce, evd, _, imps) = - check_evars_are_solved (Global.env ()) evd Evd.empty; - ce - -let do_definition ident k univdecl bl red_option c ctypopt hook = - let (ce, evd, univdecl, imps as def) = - interp_definition univdecl bl (pi2 k) red_option c ctypopt - in - if Flags.is_program_mode () then - let env = Global.env () in - let (c,ctx), sideff = Future.force ce.const_entry_body in - assert(Safe_typing.empty_private_constants = sideff); - assert(Univ.ContextSet.is_empty ctx); - let typ = match ce.const_entry_type with - | Some t -> t - | None -> EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr c)) - in - Obligations.check_evars env evd; - let obls, _, c, cty = - Obligations.eterm_obligations env ident evd 0 c typ - in - let ctx = Evd.evar_universe_context evd in - let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in - ignore(Obligations.add_definition - ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls) - else let ce = check_definition def in - ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps - (Lemmas.mk_hook - (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) - -(* 2| Variable/Hypothesis/Parameter/Axiom declarations *) - -let axiom_into_instance = ref false - -let _ = - let open Goptions in - declare_bool_option - { optdepr = false; - optname = "automatically declare axioms whose type is a typeclass as instances"; - optkey = ["Typeclasses";"Axioms";"Are";"Instances"]; - optread = (fun _ -> !axiom_into_instance); - optwrite = (:=) axiom_into_instance; } - -let should_axiom_into_instance = function - | Discharge -> - (* The typeclass behaviour of Variable and Context doesn't depend - on section status *) - true - | Global | Local -> !axiom_into_instance - -let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) = -match local with -| Discharge when Lib.sections_are_opened () -> - let ctx = match ctx with - | Monomorphic_const_entry ctx -> ctx - | Polymorphic_const_entry ctx -> Univ.ContextSet.of_context ctx - in - let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in - let _ = declare_variable ident decl in - let () = assumption_message ident in - let () = - if not !Flags.quiet && Proof_global.there_are_pending_proofs () then - Feedback.msg_info (str"Variable" ++ spc () ++ Id.print ident ++ - strbrk " is not visible from current goals") - in - let r = VarRef ident in - let () = Typeclasses.declare_instance None true r in - let () = if is_coe then Class.try_add_new_coercion r ~local:true false in - (r,Univ.Instance.empty,true) - -| Global | Local | Discharge -> - let do_instance = should_axiom_into_instance local in - let local = DeclareDef.get_locality ident ~kind:"axiom" local in - let inl = match nl with - | NoInline -> None - | DefaultInline -> Some (Flags.get_inline_level()) - | InlineAt i -> Some i - in - let decl = (ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in - let kn = declare_constant ident ~local decl in - let gr = ConstRef kn in - let () = maybe_declare_manual_implicits false gr imps in - let () = Declare.declare_univ_binders gr pl in - let () = assumption_message ident in - let () = if do_instance then Typeclasses.declare_instance None false gr in - let () = if is_coe then Class.try_add_new_coercion gr ~local p in - let inst = match ctx with - | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx - | Monomorphic_const_entry _ -> Univ.Instance.empty - in - (gr,inst,Lib.is_modtype_strict ()) - -let interp_assumption evdref env impls bl c = - let c = mkCProdN ?loc:(local_binders_loc bl) bl c in - let ty, impls = interp_type_evars_impls env evdref ~impls c in - let ty = EConstr.Unsafe.to_constr ty in - (ty, impls) - -(* When monomorphic the universe constraints are declared with the first declaration only. *) -let next_uctx = - let empty_uctx = Monomorphic_const_entry Univ.ContextSet.empty in - function - | Polymorphic_const_entry _ as uctx -> uctx - | Monomorphic_const_entry _ -> empty_uctx - -let declare_assumptions idl is_coe k (c,uctx) pl imps nl = - let refs, status, _ = - List.fold_left (fun (refs,status,uctx) id -> - let ref',u',status' = - declare_assumption is_coe k (c,uctx) pl imps false nl id in - (ref',u')::refs, status' && status, next_uctx uctx) - ([],true,uctx) idl - in - List.rev refs, status - - -let maybe_error_many_udecls = function - | ((loc,id), Some _) -> - user_err ?loc ~hdr:"many_universe_declarations" - Pp.(str "When declaring multiple axioms in one command, " ++ - str "only the first is allowed a universe binder " ++ - str "(which will be shared by the whole block).") - | (_, None) -> () - -let process_assumptions_udecls kind l = - let udecl, first_id = match l with - | (coe, ((id, udecl)::rest, c))::rest' -> - List.iter maybe_error_many_udecls rest; - List.iter (fun (coe, (idl, c)) -> List.iter maybe_error_many_udecls idl) rest'; - udecl, id - | (_, ([], _))::_ | [] -> assert false - in - let () = match kind, udecl with - | (Discharge, _, _), Some _ when Lib.sections_are_opened () -> - let loc = fst first_id in - let msg = Pp.str "Section variables cannot be polymorphic." in - user_err ?loc msg - | _ -> () - in - udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l - -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 evdref, udecl = - let evd, udecl = Univdecls.interp_univ_decl_opt env udecl in - ref evd, udecl - in - let l = - if pi2 kind (* poly *) then - (* Separate declarations so that A B : Type puts A and B in different levels. *) - List.fold_right (fun (is_coe,(idl,c)) acc -> - List.fold_right (fun id acc -> - (is_coe, ([id], c)) :: acc) idl acc) - l [] - else l - in - (* We intepret all declarations in the same evar_map, i.e. as a telescope. *) - let _,l = List.fold_left_map (fun (env,ienv) (is_coe,(idl,c)) -> - let t,imps = interp_assumption evdref env ienv [] c in - let env = - push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in - let ienv = List.fold_right (fun (_,id) ienv -> - let impls = compute_internalization_data env Variable t imps in - Id.Map.add id impls ienv) idl ienv in - ((env,ienv),((is_coe,idl),t,imps))) - (env,empty_internalization_env) l - in - let evd = solve_remaining_evars all_and_fail_flags env !evdref Evd.empty in - (* The universe constraints come from the whole telescope. *) - let evd = Evd.nf_constraints evd in - let nf_evar c = EConstr.to_constr evd (EConstr.of_constr c) in - let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> - let t = nf_evar t in - let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in - uvars, (coe,t,imps)) - Univ.LSet.empty l - in - let evd = Evd.restrict_universe_context evd uvars in - let uctx = Evd.check_univ_decl ~poly:(pi2 kind) evd udecl in - let ubinders = Evd.universe_binders evd in - pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) -> - let t = replace_vars subst t in - let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in - let subst' = List.map2 - (fun (_,id) (c,u) -> (id, Universes.constr_of_global_univ (c,u))) - idl refs - in - subst'@subst, status' && status, next_uctx uctx) - ([], true, uctx) l) - -(* 3a| Elimination schemes for mutual inductive definitions *) - -(* 3b| Mutual inductive definitions *) - -let push_types env idl tl = - List.fold_left2 (fun env id t -> Environ.push_rel (LocalAssum (Name id,t)) env) - env idl tl - -type structured_one_inductive_expr = { - ind_name : Id.t; - ind_univs : Vernacexpr.universe_decl_expr option; - ind_arity : constr_expr; - ind_lc : (Id.t * constr_expr) list -} - -type structured_inductive_expr = - local_binder_expr list * structured_one_inductive_expr list - -let minductive_message warn = function - | [] -> user_err Pp.(str "No inductive definition.") - | [x] -> (Id.print x ++ str " is defined" ++ - if warn then str " as a non-primitive record" else mt()) - | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ - spc () ++ str "are defined") - -let check_all_names_different indl = - let ind_names = List.map (fun ind -> ind.ind_name) indl in - let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in - let l = List.duplicates Id.equal ind_names in - let () = match l with - | [] -> () - | t :: _ -> raise (InductiveError (SameNamesTypes t)) - in - let l = List.duplicates Id.equal cstr_names in - let () = match l with - | [] -> () - | c :: _ -> raise (InductiveError (SameNamesConstructors (List.hd l))) - in - let l = List.intersect Id.equal ind_names cstr_names in - match l with - | [] -> () - | _ -> raise (InductiveError (SameNamesOverlap l)) - -let mk_mltype_data evdref env assums arity indname = - let is_ml_type = is_sort env !evdref (EConstr.of_constr arity) in - (is_ml_type,indname,assums) - -let prepare_param = function - | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t - | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b - -(** Make the arity conclusion flexible to avoid generating an upper bound universe now, - only if the universe does not appear anywhere else. - This is really a hack to stay compatible with the semantics of template polymorphic - inductives which are recognized when a "Type" appears at the end of the conlusion in - the source syntax. *) - -let rec check_anonymous_type ind = - let open Glob_term in - match DAst.get ind with - | GSort (GType []) -> true - | GProd ( _, _, _, e) - | GLetIn (_, _, _, e) - | GLambda (_, _, _, e) - | GApp (e, _) - | GCast (e, _) -> check_anonymous_type e - | _ -> false - -let make_conclusion_flexible evdref ty poly = - if poly && Term.isArity ty then - let _, concl = Term.destArity ty in - match concl with - | Type u -> - (match Univ.universe_level u with - | Some u -> - evdref := Evd.make_flexible_variable !evdref ~algebraic:true u - | None -> ()) - | _ -> () - else () - -let is_impredicative env u = - u = Prop Null || (is_impredicative_set env && u = Prop Pos) - -let interp_ind_arity env evdref ind = - let c = intern_gen IsType env ind.ind_arity in - let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in - let (evd,t) = understand_tcc env !evdref ~expected_type:IsType c in - evdref := evd; - let pseudo_poly = check_anonymous_type c in - let () = if not (Reductionops.is_arity env !evdref t) then - user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity") - in - let t = EConstr.Unsafe.to_constr t in - t, pseudo_poly, impls - -let interp_cstrs evdref env impls mldata arity ind = - let cnames,ctyps = List.split ind.ind_lc in - (* Complete conclusions of constructor types if given in ML-style syntax *) - let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in - (* Interpret the constructor types *) - let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls %> on_fst EConstr.Unsafe.to_constr) ctyps') in - (cnames, ctyps'', cimpls) - -let sign_level env evd sign = - fst (List.fold_right - (fun d (lev,env) -> - match d with - | LocalDef _ -> lev, push_rel d env - | LocalAssum _ -> - let s = destSort (Reduction.whd_all env - (EConstr.Unsafe.to_constr (nf_evar evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d)))))) - in - let u = univ_of_sort s in - (Univ.sup u lev, push_rel d env)) - sign (Univ.type0m_univ,env)) - -let sup_list min = List.fold_left Univ.sup min - -let extract_level env evd min tys = - let sorts = List.map (fun ty -> - let ctx, concl = Reduction.dest_prod_assum env ty in - sign_level env evd (LocalAssum (Anonymous, concl) :: ctx)) tys - in sup_list min sorts - -let is_flexible_sort evd u = - match Univ.Universe.level u with - | Some l -> Evd.is_flexible_level evd l - | None -> false - -let inductive_levels env evdref poly arities inds = - let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in - let levels = List.map (fun (x,(ctx,a)) -> - if a = Prop Null then None - else Some (univ_of_sort a)) destarities - in - let cstrs_levels, min_levels, sizes = - CList.split3 - (List.map2 (fun (_,tys,_) (arity,(ctx,du)) -> - let len = List.length tys in - let minlev = Sorts.univ_of_sort du in - let minlev = - if len > 1 && not (is_impredicative env du) then - Univ.sup minlev Univ.type0_univ - else minlev - in - let minlev = - (** Indices contribute. *) - if Indtypes.is_indices_matter () && List.length ctx > 0 then ( - let ilev = sign_level env !evdref ctx in - Univ.sup ilev minlev) - else minlev - in - let clev = extract_level env !evdref minlev tys in - (clev, minlev, len)) inds destarities) - in - (* Take the transitive closure of the system of constructors *) - (* level constraints and remove the recursive dependencies *) - let levels' = Universes.solve_constraints_system (Array.of_list levels) - (Array.of_list cstrs_levels) (Array.of_list min_levels) - in - let evd, arities = - CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len -> - if is_impredicative env du then - (** Any product is allowed here. *) - evd, arity :: arities - else (** If in a predicative sort, or asked to infer the type, - we take the max of: - - indices (if in indices-matter mode) - - constructors - - Type(1) if there is more than 1 constructor - *) - (** Constructors contribute. *) - let evd = - if Sorts.is_set du then - if not (Evd.check_leq evd cu Univ.type0_univ) then - raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType) - else evd - else evd - (* Evd.set_leq_sort env evd (Type cu) du *) - in - let evd = - if len >= 2 && Univ.is_type0m_univ cu then - (** "Polymorphic" type constraint and more than one constructor, - should not land in Prop. Add constraint only if it would - land in Prop directly (no informative arguments as well). *) - Evd.set_leq_sort env evd (Prop Pos) du - else evd - in - let duu = Sorts.univ_of_sort du in - let evd = - if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then - if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then - Evd.set_eq_sort env evd (Prop Null) du - else evd - else Evd.set_eq_sort env evd (Type cu) du - in - (evd, arity :: arities)) - (!evdref,[]) (Array.to_list levels') destarities sizes - in evdref := evd; List.rev arities - -let check_named (loc, na) = match na with -| Name _ -> () -| Anonymous -> - let msg = str "Parameters must be named." in - user_err ?loc msg - - -let check_param = function -| CLocalDef (na, _, _) -> check_named na -| CLocalAssum (nas, Default _, _) -> List.iter check_named nas -| CLocalAssum (nas, Generalized _, _) -> () -| CLocalPattern (loc,_) -> - Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.") - -let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = - check_all_names_different indl; - List.iter check_param paramsl; - let env0 = Global.env() in - let pl = (List.hd indl).ind_univs in - let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in - let evdref = ref evd in - let impls, ((env_params, ctx_params), userimpls) = - interp_context_evars env0 evdref paramsl - in - let ctx_params = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx_params in - let indnames = List.map (fun ind -> ind.ind_name) indl in - - (* Names of parameters as arguments of the inductive type (defs removed) *) - let assums = List.filter is_local_assum ctx_params in - let params = List.map (RelDecl.get_name %> Name.get_id) assums in - - (* Interpret the arities *) - let arities = List.map (interp_ind_arity env_params evdref) indl in - - let fullarities = List.map (fun (c, _, _) -> Term.it_mkProd_or_LetIn c ctx_params) arities in - let env_ar = push_types env0 indnames fullarities in - let env_ar_params = push_rel_context ctx_params env_ar in - - (* Compute interpretation metadatas *) - let indimpls = List.map (fun (_, _, impls) -> userimpls @ - lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in - let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in - let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in - let ntn_impls = compute_internalization_env env0 (Inductive (params,true)) indnames fullarities indimpls in - let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in - - let constructors = - Metasyntax.with_syntax_protection (fun () -> - (* Temporary declaration of notations and scopes *) - List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations; - (* Interpret the constructor types *) - List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl) - () in - - (* Try further to solve evars, and instantiate them *) - let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref Evd.empty in - evdref := sigma; - (* Compute renewed arities *) - let nf,_ = e_nf_evars_and_universes evdref in - let arities = List.map nf arities in - let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in - let _ = List.iter2 (fun ty poly -> make_conclusion_flexible evdref ty poly) arities aritypoly in - let arities = inductive_levels env_ar_params evdref poly arities constructors in - let nf',_ = e_nf_evars_and_universes evdref in - let nf x = nf' (nf x) in - let arities = List.map nf' arities in - let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in - let ctx_params = Context.Rel.map nf ctx_params in - let evd = !evdref in - let uctx = Evd.check_univ_decl ~poly evd decl in - List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities; - Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params; - List.iter (fun (_,ctyps,_) -> - List.iter (fun c -> check_evars env_ar_params Evd.empty evd (EConstr.of_constr c)) ctyps) - constructors; - - (* Build the inductive entries *) - let entries = List.map4 (fun ind arity template (cnames,ctypes,cimpls) -> { - mind_entry_typename = ind.ind_name; - mind_entry_arity = arity; - mind_entry_template = template; - mind_entry_consnames = cnames; - mind_entry_lc = ctypes - }) indl arities aritypoly constructors in - let impls = - let len = Context.Rel.nhyps ctx_params in - List.map2 (fun indimpls (_,_,cimpls) -> - indimpls, List.map (fun impls -> - userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors - in - let univs = - match uctx with - | Polymorphic_const_entry uctx -> - if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) - else Polymorphic_ind_entry uctx - | Monomorphic_const_entry uctx -> - Monomorphic_ind_entry uctx - in - (* Build the mutual inductive entry *) - let mind_ent = - { mind_entry_params = List.map prepare_param ctx_params; - mind_entry_record = None; - mind_entry_finite = finite; - mind_entry_inds = entries; - mind_entry_private = if prv then Some false else None; - mind_entry_universes = univs; - } - in - (if poly && cum then - Inductiveops.infer_inductive_subtyping env_ar evd mind_ent - else mind_ent), Evd.universe_binders evd, impls - -(* Very syntactical equality *) -let eq_local_binders bl1 bl2 = - List.equal local_binder_eq bl1 bl2 - -let extract_coercions indl = - let mkqid (_,((_,id),_)) = qualid_of_ident id in - let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in - List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl)) - -let extract_params indl = - let paramsl = List.map (fun (_,params,_,_) -> params) indl in - match paramsl with - | [] -> anomaly (Pp.str "empty list of inductive types.") - | params::paramsl -> - if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str - "Parameters should be syntactically the same for each inductive type."); - params - -let extract_inductive indl = - List.map (fun (((_,indname),pl),_,ar,lc) -> { - ind_name = indname; ind_univs = pl; - ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar; - ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc - }) indl - -let extract_mutual_inductive_declaration_components indl = - let indl,ntnl = List.split indl in - let params = extract_params indl in - let coes = extract_coercions indl in - let indl = extract_inductive indl in - (params,indl), coes, List.flatten ntnl - -let is_recursive mie = - let rec is_recursive_constructor lift typ = - match Constr.kind typ with - | Prod (_,arg,rest) -> - not (EConstr.Vars.noccurn Evd.empty (** FIXME *) lift (EConstr.of_constr arg)) || - is_recursive_constructor (lift+1) rest - | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest - | _ -> false - in - match mie.mind_entry_inds with - | [ind] -> - let nparams = List.length mie.mind_entry_params in - List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc - | _ -> false - -let declare_mutual_inductive_with_eliminations mie pl impls = - (* spiwack: raises an error if the structure is supposed to be non-recursive, - but isn't *) - begin match mie.mind_entry_finite with - | BiFinite when is_recursive mie -> - if Option.has_some mie.mind_entry_record then - user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") - else - user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")) - | _ -> () - end; - let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in - let (_, kn), prim = declare_mind mie in - let mind = Global.mind_of_delta_kn kn in - List.iteri (fun i (indimpls, constrimpls) -> - let ind = (mind,i) in - let gr = IndRef ind in - maybe_declare_manual_implicits false gr indimpls; - Declare.declare_univ_binders gr pl; - List.iteri - (fun j impls -> - maybe_declare_manual_implicits false - (ConstructRef (ind, succ j)) impls) - constrimpls) - impls; - let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in - Flags.if_verbose Feedback.msg_info (minductive_message warn_prim names); - if mie.mind_entry_private == None - then declare_default_schemes mind; - mind - -type one_inductive_impls = - Impargs.manual_explicitation list (* for inds *)* - Impargs.manual_explicitation list list (* for constrs *) - -let do_mutual_inductive indl cum poly prv finite = - let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in - (* Interpret the types *) - let mie,pl,impls = interp_mutual_inductive indl ntns cum poly prv finite in - (* Declare the mutual inductive block with its associated schemes *) - ignore (declare_mutual_inductive_with_eliminations mie pl impls); - (* Declare the possible notations of inductive types *) - List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; - (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes; - (* If positivity is assumed declares itself as unsafe. *) - if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () - -(* 3c| Fixpoints and co-fixpoints *) - -(* An (unoptimized) function that maps preorders to partial orders... - - Input: a list of associations (x,[y1;...;yn]), all yi distincts - and different of x, meaning x<=y1, ..., x<=yn - - Output: a list of associations (x,Inr [y1;...;yn]), collecting all - distincts yi greater than x, _or_, (x, Inl y) meaning that - x is in the same class as y (in which case, x occurs - nowhere else in the association map) - - partial_order : ('a * 'a list) list -> ('a * ('a,'a list) union) list -*) - -let rec partial_order cmp = function - | [] -> [] - | (x,xge)::rest -> - let rec browse res xge' = function - | [] -> - let res = List.map (function - | (z, Inr zge) when List.mem_f cmp x zge -> - (z, Inr (List.union cmp zge xge')) - | r -> r) res in - (x,Inr xge')::res - | y::xge -> - let rec link y = - try match List.assoc_f cmp y res with - | Inl z -> link z - | Inr yge -> - if List.mem_f cmp x yge then - let res = List.remove_assoc_f cmp y res in - let res = List.map (function - | (z, Inl t) -> - if cmp t y then (z, Inl x) else (z, Inl t) - | (z, Inr zge) -> - if List.mem_f cmp y zge then - (z, Inr (List.add_set cmp x (List.remove cmp y zge))) - else - (z, Inr zge)) res in - browse ((y,Inl x)::res) xge' (List.union cmp xge (List.remove cmp x yge)) - else - browse res (List.add_set cmp y (List.union cmp xge' yge)) xge - with Not_found -> browse res (List.add_set cmp y xge') xge - in link y - in browse (partial_order cmp rest) [] xge - -let non_full_mutual_message x xge y yge isfix rest = - let reason = - if Id.List.mem x yge then - Id.print y ++ str " depends on " ++ Id.print x ++ strbrk " but not conversely" - else if Id.List.mem y xge then - Id.print x ++ str " depends on " ++ Id.print y ++ strbrk " but not conversely" - else - Id.print y ++ str " and " ++ Id.print x ++ strbrk " are not mutually dependent" in - let e = if List.is_empty rest then reason else strbrk "e.g., " ++ reason in - let k = if isfix then "fixpoint" else "cofixpoint" in - let w = - if isfix - then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl() - else mt () in - strbrk "Not a fully mutually defined " ++ str k ++ fnl () ++ - str "(" ++ e ++ str ")." ++ fnl () ++ w - -let warn_non_full_mutual = - CWarnings.create ~name:"non-full-mutual" ~category:"fixpoints" - (fun (x,xge,y,yge,isfix,rest) -> - non_full_mutual_message x xge y yge isfix rest) - -let check_mutuality env evd isfix fixl = - let names = List.map fst fixl in - let preorder = - List.map (fun (id,def) -> - (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' (EConstr.of_constr def)) names)) - fixl in - let po = partial_order Id.equal preorder in - match List.filter (function (_,Inr _) -> true | _ -> false) po with - | (x,Inr xge)::(y,Inr yge)::rest -> - warn_non_full_mutual (x,xge,y,yge,isfix,rest) - | _ -> () - -type structured_fixpoint_expr = { - fix_name : Id.t; - fix_univs : universe_decl_expr option; - fix_annot : Id.t Loc.located option; - fix_binders : local_binder_expr list; - fix_body : constr_expr option; - fix_type : constr_expr -} - -let interp_fix_context env evdref isfix fix = - let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in - let impl_env, ((env', ctx), imps) = interp_context_evars env evdref before in - let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' evdref after in - let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in - ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) - -let interp_fix_ccl evdref impls (env,_) fix = - let (c, impl) = interp_type_evars_impls ~impls env evdref fix.fix_type in - (c, impl) - -let interp_fix_body env_rec evdref impls (_,ctx) fix ccl = - let open EConstr in - Option.map (fun body -> - let env = push_rel_context ctx env_rec in - let body = interp_casted_constr_evars env evdref ~impls body ccl in - it_mkLambda_or_LetIn body ctx) fix.fix_body - -let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx - -let prepare_recursive_declaration fixnames fixtypes fixdefs = - let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in - let names = List.map (fun id -> Name id) fixnames in - (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) - -(* Jump over let-bindings. *) - -let compute_possible_guardness_evidences (ctx,_,recindex) = - (* A recursive index is characterized by the number of lambdas to - skip before finding the relevant inductive argument *) - match recindex with - | Some i -> [i] - | None -> - (* If recursive argument was not given by user, we try all args. - An earlier approach was to look only for inductive arguments, - but doing it properly involves delta-reduction, and it finally - doesn't seem to worth the effort (except for huge mutual - fixpoints ?) *) - List.interval 0 (Context.Rel.nhyps ctx - 1) - -type recursive_preentry = - Id.t list * constr option list * types list - -(* Wellfounded definition *) - -open Coqlib - -let contrib_name = "Program" -let subtac_dir = [contrib_name] -let fixsub_module = subtac_dir @ ["Wf"] -let tactics_module = subtac_dir @ ["Tactics"] - -let init_reference dir s () = Coqlib.coq_reference "Command" dir s -let init_constant dir s evdref = - let (sigma, c) = Evarutil.new_global !evdref (Coqlib.coq_reference "Command" dir s) - in evdref := sigma; c - -let make_ref l s = init_reference l s -let fix_proto = init_constant tactics_module "fix_proto" -let fix_sub_ref = make_ref fixsub_module "Fix_sub" -let measure_on_R_ref = make_ref fixsub_module "MR" -let well_founded = init_constant ["Init"; "Wf"] "well_founded" -let mkSubset evdref name typ prop = - let open EConstr in - mkApp (Evarutil.e_new_global evdref (delayed_force build_sigma).typ, - [| typ; mkLambda (name, typ, prop) |]) -let sigT = Lazy.from_fun build_sigma_type - -let make_qref s = Qualid (Loc.tag @@ qualid_of_string s) -let lt_ref = make_qref "Init.Peano.lt" - -let rec telescope evdref l = - let open EConstr in - let open Vars in - match l with - | [] -> assert false - | [LocalAssum (n, t)] -> t, [LocalDef (n, mkRel 1, t)], mkRel 1 - | LocalAssum (n, t) :: tl -> - let ty, tys, (k, constr) = - List.fold_left - (fun (ty, tys, (k, constr)) decl -> - let t = RelDecl.get_type decl in - let pred = mkLambda (RelDecl.get_name decl, t, ty) in - let ty = Evarutil.e_new_global evdref (Lazy.force sigT).typ in - let intro = Evarutil.e_new_global evdref (Lazy.force sigT).intro in - let sigty = mkApp (ty, [|t; pred|]) in - let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in - (sigty, pred :: tys, (succ k, intro))) - (t, [], (2, mkRel 1)) tl - in - let (last, subst) = List.fold_right2 - (fun pred decl (prev, subst) -> - let t = RelDecl.get_type decl in - let p1 = Evarutil.e_new_global evdref (Lazy.force sigT).proj1 in - let p2 = Evarutil.e_new_global evdref (Lazy.force sigT).proj2 in - let proj1 = applist (p1, [t; pred; prev]) in - let proj2 = applist (p2, [t; pred; prev]) in - (lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst)) - (List.rev tys) tl (mkRel 1, []) - in ty, (LocalDef (n, last, t) :: subst), constr - - | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope evdref tl in - ty, (LocalDef (n, b, t) :: subst), lift 1 term - -let nf_evar_context sigma ctx = - List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx - -let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = - let open EConstr in - let open Vars in - 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 evd, decl = Univdecls.interp_univ_decl_opt env pl in - let evdref = ref evd in - let _, ((env', binders_rel), impls) = interp_context_evars env evdref bl in - let len = List.length binders_rel in - let top_env = push_rel_context binders_rel env in - let top_arity = interp_type_evars top_env evdref arityc in - let full_arity = it_mkProd_or_LetIn top_arity binders_rel in - let argtyp, letbinders, make = telescope evdref binders_rel in - let argname = Id.of_string "recarg" in - let arg = LocalAssum (Name argname, argtyp) in - let binders = letbinders @ [arg] in - let binders_env = push_rel_context binders_rel env in - let rel, _ = interp_constr_evars_impls env evdref r in - let relty = Typing.unsafe_type_of env !evdref rel in - let relargty = - let error () = - user_err ?loc:(constr_loc r) - ~hdr:"Command.build_wellfounded" - (Printer.pr_econstr_env env !evdref rel ++ str " is not an homogeneous binary relation.") - in - try - let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in - match ctx, EConstr.kind !evdref ar with - | [LocalAssum (_,t); LocalAssum (_,u)], Sort s - when Sorts.is_prop (ESorts.kind !evdref s) && Reductionops.is_conv env !evdref t u -> t - | _, _ -> error () - with e when CErrors.noncritical e -> error () - in - let relargty = EConstr.Unsafe.to_constr relargty in - let measure = interp_casted_constr_evars binders_env evdref measure relargty in - let wf_rel, wf_rel_fun, measure_fn = - let measure_body, measure = - it_mkLambda_or_LetIn measure letbinders, - it_mkLambda_or_LetIn measure binders - in - let comb = Evarutil.e_new_global evdref (delayed_force measure_on_R_ref) in - let relargty = EConstr.of_constr relargty in - let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in - let wf_rel_fun x y = - mkApp (rel, [| subst1 x measure_body; - subst1 y measure_body |]) - in wf_rel, wf_rel_fun, measure - in - let wf_proof = mkApp (well_founded evdref, [| argtyp ; wf_rel |]) in - let argid' = Id.of_string (Id.to_string argname ^ "'") in - let wfarg len = LocalAssum (Name argid', - mkSubset evdref (Name argid') argtyp - (wf_rel_fun (mkRel 1) (mkRel (len + 1)))) - in - let intern_bl = wfarg 1 :: [arg] in - let _intern_env = push_rel_context intern_bl env in - let proj = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.proj1 in - let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in - let projection = (* in wfarg :: arg :: before *) - mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |]) - in - let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in - let intern_arity = substl [projection] top_arity_let in - (* substitute the projection of wfarg for something, - now intern_arity is in wfarg :: arg *) - let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in - let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in - let curry_fun = - let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in - let intro = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.intro in - let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in - let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in - let rcurry = mkApp (rel, [| measure; lift len measure |]) in - let lam = LocalAssum (Name (Id.of_string "recproof"), rcurry) in - let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in - let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in - LocalDef (Name recname, body, ty) - in - let fun_bl = intern_fun_binder :: [arg] in - let lift_lets = lift_rel_context 1 letbinders in - let intern_body = - let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in - let (r, l, impls, scopes) = - Constrintern.compute_internalization_data env - Constrintern.Recursive (EConstr.Unsafe.to_constr full_arity) impls - in - let newimpls = Id.Map.singleton recname - (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))], - scopes @ [None]) in - interp_casted_constr_evars (push_rel_context ctx env) evdref - ~impls:newimpls body (EConstr.Unsafe.to_constr (lift 1 top_arity)) - in - let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in - let prop = mkLambda (Name argname, argtyp, top_arity_let) in - let def = - mkApp (Evarutil.e_new_global evdref (delayed_force fix_sub_ref), - [| argtyp ; wf_rel ; - Evarutil.e_new_evar env evdref - ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof; - prop |]) - in - let def = Typing.e_solve_evars env evdref def in - let _ = evdref := Evarutil.nf_evar_map !evdref in - let def = mkApp (def, [|intern_body_lam|]) in - let binders_rel = nf_evar_context !evdref binders_rel in - let binders = nf_evar_context !evdref binders in - let top_arity = Evarutil.nf_evar !evdref top_arity in - let hook, recname, typ = - if List.length binders_rel > 1 then - let name = add_suffix recname "_func" in - let hook l gr _ = - let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in - let ty = it_mkProd_or_LetIn top_arity binders_rel in - let ty = EConstr.Unsafe.to_constr ty in - let univs = Evd.check_univ_decl ~poly !evdref decl in - (*FIXME poly? *) - let ce = definition_entry ~types:ty ~univs (EConstr.to_constr !evdref body) in - (** FIXME: include locality *) - let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in - let gr = ConstRef c in - let () = Universes.register_universe_binders gr (Evd.universe_binders !evdref) in - if Impargs.is_implicit_args () || not (List.is_empty impls) then - Impargs.declare_manual_implicits false gr [impls] - in - let typ = it_mkProd_or_LetIn top_arity binders in - hook, name, typ - else - let typ = it_mkProd_or_LetIn top_arity binders_rel in - let hook l gr _ = - if Impargs.is_implicit_args () || not (List.is_empty impls) then - Impargs.declare_manual_implicits false gr [impls] - in hook, recname, typ - in - let hook = Lemmas.mk_hook hook in - let fullcoqc = EConstr.to_constr !evdref def in - let fullctyp = EConstr.to_constr !evdref typ in - Obligations.check_evars env !evdref; - let evars, _, evars_def, evars_typ = - Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp - in - let ctx = Evd.evar_universe_context !evdref in - ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl - evars_typ ctx evars ~hook) - -let interp_recursive isfix fixl notations = - let open Context.Named.Declaration in - let open EConstr in - let env = Global.env() in - let fixnames = List.map (fun fix -> fix.fix_name) fixl in - - (* Interp arities allowing for unresolved types *) - let all_universes = - List.fold_right (fun sfe acc -> - match sfe.fix_univs , acc with - | None , acc -> acc - | x , None -> x - | Some ls , Some us -> - let lsu = ls.univdecl_instance and usu = us.univdecl_instance in - if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) lsu usu) then - user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); - Some us) fixl None in - let evd, decl = Univdecls.interp_univ_decl_opt env all_universes in - let evdref = ref evd in - let fixctxs, fiximppairs, fixannots = - List.split3 (List.map (interp_fix_context env evdref isfix) fixl) in - let fixctximpenvs, fixctximps = List.split fiximppairs in - let fixccls,fixcclimps = List.split (List.map3 (interp_fix_ccl evdref) fixctximpenvs fixctxs fixl) in - let fixtypes = List.map2 build_fix_type fixctxs fixccls in - let fixtypes = List.map (fun c -> nf_evar !evdref c) fixtypes in - let fiximps = List.map3 - (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps)) - fixctximps fixcclimps fixctxs in - let rec_sign = - List.fold_left2 - (fun env' id t -> - if Flags.is_program_mode () then - let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in - let fixprot = - try - let app = mkApp (fix_proto evdref, [|sort; t|]) in - Typing.e_solve_evars env evdref app - with e when CErrors.noncritical e -> t - in - LocalAssum (id,fixprot) :: env' - else LocalAssum (id,t) :: env') - [] fixnames fixtypes - in - let env_rec = push_named_context rec_sign env in - - (* Get interpretation metadatas *) - let fixtypes = List.map EConstr.Unsafe.to_constr fixtypes in - let fixccls = List.map EConstr.Unsafe.to_constr fixccls in - let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in - - (* Interp bodies with rollback because temp use of notations/implicit *) - let fixdefs = - Metasyntax.with_syntax_protection (fun () -> - List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations; - List.map4 - (fun fixctximpenv -> interp_fix_body env_rec evdref (Id.Map.fold Id.Map.add fixctximpenv impls)) - fixctximpenvs fixctxs fixl fixccls) - () in - - (* Instantiate evars and check all are resolved *) - let evd = solve_unif_constraints_with_heuristics env_rec !evdref in - let evd, nf = nf_evars_and_universes evd in - let fixdefs = List.map (fun c -> Option.map EConstr.Unsafe.to_constr c) fixdefs in - let fixdefs = List.map (Option.map nf) fixdefs in - let fixtypes = List.map nf fixtypes in - let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in - - (* Build the fix declaration block *) - (env,rec_sign,decl,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots - -let check_recursive isfix env evd (fixnames,fixdefs,_) = - check_evars_are_solved env evd Evd.empty; - if List.for_all Option.has_some fixdefs then begin - let fixdefs = List.map Option.get fixdefs in - check_mutuality env evd isfix (List.combine fixnames fixdefs) - end - -let interp_fixpoint l ntns = - let (env,_,pl,evd),fix,info = interp_recursive true l ntns in - check_recursive true env evd fix; - (fix,pl,Evd.evar_universe_context evd,info) - -let interp_cofixpoint l ntns = - let (env,_,pl,evd),fix,info = interp_recursive false l ntns in - check_recursive false env evd fix; - (fix,pl,Evd.evar_universe_context evd,info) - -let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = - if List.exists Option.is_empty fixdefs then - (* Some bodies to define by proof *) - let thms = - List.map3 (fun id t (ctx,imps,_) -> (id,(t,(List.map RelDecl.get_name ctx,imps)))) - fixnames fixtypes fiximps in - let init_tac = - Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) - fixdefs) in - let evd = Evd.from_ctx ctx in - Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint) - evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) - else begin - (* We shortcut the proof process *) - let fixdefs = List.map Option.get fixdefs in - let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in - let env = Global.env() in - let indexes = search_guard env indexes fixdecls in - let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let vars = Univops.universes_of_constr env (mkFix ((indexes,0),fixdecls)) in - let fixdecls = - List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in - let evd = Evd.from_ctx ctx in - let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl ~poly evd pl in - let pl = Evd.universe_binders evd in - let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in - ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) - fixnames fixdecls fixtypes fiximps); - (* Declare the recursive definitions *) - fixpoint_message (Some indexes) fixnames; - end; - (* Declare notations *) - List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns - -let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns = - if List.exists Option.is_empty fixdefs then - (* Some bodies to define by proof *) - let thms = - List.map3 (fun id t (ctx,imps,_) -> (id,(t,(List.map RelDecl.get_name ctx,imps)))) - fixnames fixtypes fiximps in - let init_tac = - Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) - fixdefs) in - let evd = Evd.from_ctx ctx in - Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) - evd pl (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) - else begin - (* We shortcut the proof process *) - let fixdefs = List.map Option.get fixdefs in - let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in - let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let env = Global.env () in - let vars = Univops.universes_of_constr env (List.hd fixdecls) in - let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in - let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in - let evd = Evd.from_ctx ctx in - let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl ~poly evd pl in - let pl = Evd.universe_binders evd in - ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) - fixnames fixdecls fixtypes fiximps); - (* Declare the recursive definitions *) - cofixpoint_message fixnames - end; - (* Declare notations *) - List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns - -let extract_decreasing_argument limit = function - | (na,CStructRec) -> na - | (na,_) when not limit -> na - | _ -> user_err Pp.(str - "Only structural decreasing is supported for a non-Program Fixpoint") - -let extract_fixpoint_components limit l = - let fixl, ntnl = List.split l in - let fixl = List.map (fun (((_,id),pl),ann,bl,typ,def) -> - let ann = extract_decreasing_argument limit ann in - {fix_name = id; fix_annot = ann; fix_univs = pl; - fix_binders = bl; fix_body = def; fix_type = typ}) fixl in - fixl, List.flatten ntnl - -let extract_cofixpoint_components l = - let fixl, ntnl = List.split l in - List.map (fun (((_,id),pl),bl,typ,def) -> - {fix_name = id; fix_annot = None; fix_univs = pl; - fix_binders = bl; fix_body = def; fix_type = typ}) fixl, - List.flatten ntnl - -let out_def = function - | Some def -> def - | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.") - -let collect_evars_of_term evd c ty = - let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in - Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) - evars (Evd.from_ctx (Evd.evar_universe_context evd)) - -let do_program_recursive local poly fixkind fixl ntns = - let isfix = fixkind != Obligations.IsCoFixpoint in - let (env, rec_sign, pl, evd), fix, info = - interp_recursive isfix fixl ntns - in - (* Program-specific code *) - (* Get the interesting evars, those that were not instanciated *) - let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in - (* Solve remaining evars *) - let evd = nf_evar_map_undefined evd in - let collect_evars id def typ imps = - (* Generalize by the recursive prototypes *) - let def = - EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign) - and typ = - EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign) - in - let evm = collect_evars_of_term evd def typ in - let evars, _, def, typ = - Obligations.eterm_obligations env id evm - (List.length rec_sign) def typ - in (id, def, typ, imps, evars) - in - let (fixnames,fixdefs,fixtypes) = fix in - let fiximps = List.map pi2 info in - let fixdefs = List.map out_def fixdefs in - let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in - let () = if isfix then begin - let possible_indexes = List.map compute_possible_guardness_evidences info in - let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), - Array.of_list fixtypes, - Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) - in - let indexes = - Pretyping.search_guard (Global.env ()) possible_indexes fixdecls in - List.iteri (fun i _ -> - Inductive.check_fix env - ((indexes,i),fixdecls)) - fixl - end in - let ctx = Evd.evar_universe_context evd in - let kind = match fixkind with - | Obligations.IsFixpoint _ -> (local, poly, Fixpoint) - | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint) - in - Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind - -let do_program_fixpoint local poly l = - let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in - match g, l with - | [(n, CWfRec r)], [((((_,id),pl),_,bl,typ,def),ntn)] -> - let recarg = - match n with - | Some n -> mkIdentC (snd n) - | None -> - user_err ~hdr:"do_program_fixpoint" - (str "Recursive argument required for well-founded fixpoints") - in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn - - | [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] -> - build_wellfounded (id, pl, n, bl, typ, out_def def) poly - (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn - - | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g -> - let fixl,ntns = extract_fixpoint_components true l in - let fixkind = Obligations.IsFixpoint g in - do_program_recursive local poly fixkind fixl ntns - - | _, _ -> - user_err ~hdr:"do_program_fixpoint" - (str "Well-founded fixpoints not allowed in mutually recursive blocks") - -let check_safe () = - let open Declarations in - let flags = Environ.typing_flags (Global.env ()) in - flags.check_universes && flags.check_guarded - -let do_fixpoint local poly l = - if Flags.is_program_mode () then do_program_fixpoint local poly l - else - let fixl, ntns = extract_fixpoint_components true l in - let (_, _, _, info as fix) = interp_fixpoint fixl ntns in - let possible_indexes = - List.map compute_possible_guardness_evidences info in - declare_fixpoint local poly fix possible_indexes ntns; - if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () - -let do_cofixpoint local poly l = - let fixl,ntns = extract_cofixpoint_components l in - if Flags.is_program_mode () then - do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns - else - let cofix = interp_cofixpoint fixl ntns in - declare_cofixpoint local poly cofix ntns; - if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/command.mli b/vernac/command.mli deleted file mode 100644 index c7342e6da9..0000000000 --- a/vernac/command.mli +++ /dev/null @@ -1,163 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Constr -open Entries -open Libnames -open Globnames -open Vernacexpr -open Constrexpr -open Decl_kinds -open Redexpr - -(** This file is about the interpretation of raw commands into typed - ones and top-level declaration of the main Gallina objects *) - -val do_universe : polymorphic -> Id.t Loc.located list -> unit -val do_constraint : polymorphic -> - (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> unit - -(** {6 Definitions/Let} *) - -val interp_definition : - Vernacexpr.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 - -val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> - local_binder_expr list -> red_expr option -> constr_expr -> - constr_expr option -> unit Lemmas.declaration_hook -> unit - -(** {6 Parameters/Assumptions} *) - -(* val interp_assumption : env -> evar_map ref -> *) -(* local_binder_expr list -> constr_expr -> *) -(* types Univ.in_universe_context_set * Impargs.manual_implicits *) - -(** returns [false] if the assumption is neither local to a section, - nor in a module type and meant to be instantiated. *) -val declare_assumption : coercion_flag -> assumption_kind -> - types in_constant_universes_entry -> - Universes.universe_binders -> Impargs.manual_implicits -> - bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> - global_reference * Univ.Instance.t * bool - -val do_assumptions : locality * polymorphic * assumption_object_kind -> - Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool - -(* val declare_assumptions : variable Loc.located list -> *) -(* coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> *) -(* Impargs.manual_implicits -> bool -> Vernacexpr.inline -> bool *) - -(** {6 Inductive and coinductive types} *) - -(** Extracting the semantical components out of the raw syntax of mutual - inductive declarations *) - -type structured_one_inductive_expr = { - ind_name : Id.t; - ind_univs : Vernacexpr.universe_decl_expr option; - ind_arity : constr_expr; - ind_lc : (Id.t * constr_expr) list -} - -type structured_inductive_expr = - local_binder_expr list * structured_one_inductive_expr list - -val extract_mutual_inductive_declaration_components : - (one_inductive_expr * decl_notation list) list -> - structured_inductive_expr * (*coercions:*) qualid list * decl_notation list - -(** Typing mutual inductive definitions *) - -type one_inductive_impls = - Impargs.manual_implicits (** for inds *)* - Impargs.manual_implicits list (** for constrs *) - -val interp_mutual_inductive : - structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Declarations.recursivity_kind -> - mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list - -(** Registering a mutual inductive definition together with its - associated schemes *) - -val declare_mutual_inductive_with_eliminations : - mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list -> - MutInd.t - -(** Entry points for the vernacular commands Inductive and CoInductive *) - -val do_mutual_inductive : - (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Declarations.recursivity_kind -> unit - -(** {6 Fixpoints and cofixpoints} *) - -type structured_fixpoint_expr = { - fix_name : Id.t; - fix_univs : Vernacexpr.universe_decl_expr option; - fix_annot : Id.t Loc.located option; - fix_binders : local_binder_expr list; - fix_body : constr_expr option; - fix_type : constr_expr -} - -(** Extracting the semantical components out of the raw syntax of - (co)fixpoints declarations *) - -val extract_fixpoint_components : bool -> - (fixpoint_expr * decl_notation list) list -> - structured_fixpoint_expr list * decl_notation list - -val extract_cofixpoint_components : - (cofixpoint_expr * decl_notation list) list -> - structured_fixpoint_expr list * decl_notation list - -(** Typing global fixpoints and cofixpoint_expr *) - -type recursive_preentry = - Id.t list * constr option list * types list - -val interp_fixpoint : - structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * Univdecls.universe_decl * UState.t * - (EConstr.rel_context * Impargs.manual_implicits * int option) list - -val interp_cofixpoint : - structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * Univdecls.universe_decl * UState.t * - (EConstr.rel_context * Impargs.manual_implicits * int option) list - -(** Registering fixpoints and cofixpoints in the environment *) - -val declare_fixpoint : - locality -> polymorphic -> - recursive_preentry * Univdecls.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 * - (Context.Rel.t * Impargs.manual_implicits * int option) list -> - decl_notation list -> unit - -(** Entry points for the vernacular commands Fixpoint and CoFixpoint *) - -val do_fixpoint : - (* When [false], assume guarded. *) - locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit - -val do_cofixpoint : - (* When [false], assume guarded. *) - locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit - -(** Utils *) - -val check_mutuality : Environ.env -> Evd.evar_map -> bool -> (Id.t * types) list -> unit diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 200c2260ed..27a680b9b6 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -13,12 +13,10 @@ open CErrors open Util open Pp open Names -open Term open Constr open Declarations open Declareops open Entries -open Environ open Nameops open Globnames open Decls @@ -88,28 +86,28 @@ let adjust_guardness_conditions const = function (mkFix ((indexes,0),fixdecls), ctx), eff | _ -> (body, ctx), eff) } -let find_mutually_recursive_statements thms = +let find_mutually_recursive_statements sigma thms = let n = List.length thms in let inds = List.map (fun (id,(t,impls)) -> - let (hyps,ccl) = decompose_prod_assum t in + let (hyps,ccl) = EConstr.decompose_prod_assum sigma t in let x = (id,(t,impls)) in - let whnf_hyp_hds = map_rel_context_in_env - (fun env c -> EConstr.Unsafe.to_constr (fst (whd_all_stack env Evd.empty (EConstr.of_constr c)))) + let whnf_hyp_hds = EConstr.map_rel_context_in_env + (fun env c -> fst (Reductionops.whd_all_stack env sigma c)) (Global.env()) hyps in let ind_hyps = List.flatten (List.map_i (fun i decl -> let t = RelDecl.get_type decl in - match Constr.kind t with + match EConstr.kind sigma t with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in mind.mind_finite <> Decl_kinds.CoFinite -> [ind,x,i] | _ -> - []) 0 (List.rev (List.filter RelDecl.is_local_assum whnf_hyp_hds))) in + []) 0 (List.rev (List.filter Context.Rel.Declaration.is_local_assum whnf_hyp_hds))) in let ind_ccl = - let cclenv = push_rel_context hyps (Global.env()) in - let whnf_ccl,_ = whd_all_stack cclenv Evd.empty (EConstr.of_constr ccl) in - match Constr.kind (EConstr.Unsafe.to_constr whnf_ccl) with + let cclenv = EConstr.push_rel_context hyps (Global.env()) in + let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in + match EConstr.kind sigma whnf_ccl with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite -> @@ -163,14 +161,14 @@ let find_mutually_recursive_statements thms = in (finite,guard,None), ordered_inds -let look_for_possibly_mutual_statements = function +let look_for_possibly_mutual_statements sigma = function | [id,(t,impls)] -> (* One non recursively proved theorem *) None,[id,(t,impls)],None | _::_ as thms -> (* More than one statement and/or an explicit decreasing mark: *) (* we look for a common inductive hyp or a common coinductive conclusion *) - let recguard,ordered_inds = find_mutually_recursive_statements thms in + let recguard,ordered_inds = find_mutually_recursive_statements sigma thms in let thms = List.map pi2 ordered_inds in Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds) | [] -> anomaly (Pp.str "Empty list of theorems.") @@ -377,7 +375,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_ let rec_tac_initializer finite guard thms snl = if finite then - match List.map (fun (id,(t,_)) -> (id,EConstr.of_constr t)) thms with + match List.map (fun (id,(t,_)) -> (id,t)) thms with | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else @@ -385,11 +383,11 @@ let rec_tac_initializer finite guard thms snl = let nl = match snl with | None -> List.map succ (List.map List.last guard) | Some nl -> nl - in match List.map2 (fun (id,(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with + in match List.map2 (fun (id,(t,_)) n -> (id,n, t)) thms nl with | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false -let start_proof_with_initialization kind ctx decl recguard thms snl hook = +let start_proof_with_initialization kind sigma decl recguard thms snl hook = let intro_tac (_, (_, (ids, _))) = Tacticals.New.tclMAP (function | Name id -> Tactics.intro_mustbe_force id @@ -424,16 +422,15 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook = if List.is_empty other_thms then [] else (* there are several theorems defined mutually *) let body,opaq = retrieve_first_recthm ctx ref in - let subst = Evd.evar_universe_context_subst ctx in - let norm c = Universes.subst_opt_univs_constr subst c in - let body = Option.map norm body in + let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in + let body = Option.map EConstr.of_constr body in let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in List.map_i (save_remaining_recthms kind norm uctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; call_hook (fun exn -> exn) hook strength ref) thms_data in - start_proof_univs id ~pl:decl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard + start_proof_univs id ~pl:decl kind sigma t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in @@ -442,22 +439,24 @@ let start_proof_com ?inference_hook kind thms hook = match decl with | None -> Evd.from_env env0, Univdecls.default_univ_decl | Some decl -> - Univdecls.interp_univ_decl_opt env0 (snd decl) in - let evdref = ref evd in - let thms = List.map (fun (sopt,(bl,t)) -> - let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in - let t', imps' = interp_type_evars_impls ~impls env evdref t in + Univdecls.interp_univ_decl_opt env0 (snd decl) in + let evd, thms = List.fold_left_map (fun evd (sopt,(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 let flags = all_and_fail_flags in let flags = { flags with use_hook = inference_hook } in - evdref := solve_remaining_evars flags env !evdref Evd.empty; + let evd = solve_remaining_evars flags env evd Evd.empty in let ids = List.map RelDecl.get_name ctx in - (compute_proof_name (pi1 kind) sopt, - (EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.it_mkProd_or_LetIn t' ctx)), - (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps')))) - thms in - let recguard,thms,snl = look_for_possibly_mutual_statements thms in - let evd, nf = Evarutil.nf_evars_and_universes !evdref in - let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in + (* XXX: The nf_evar is critical !! *) + evd, (compute_proof_name (pi1 kind) sopt, + (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), + (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps')))) + evd thms in + let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in + let evd, _nf = Evarutil.nf_evars_and_universes evd in + (* XXX: This nf_evar is critical too!! We are normalizing twice if + 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 if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then @@ -470,7 +469,6 @@ let start_proof_com ?inference_hook kind thms hook = in start_proof_with_initialization kind evd decl recguard thms snl hook - (* Saving a proof *) let keep_admitted_vars = ref true diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index a4854b4a6b..ca92e856bc 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Constr open Decl_kinds type 'a declaration_hook @@ -37,11 +36,11 @@ val start_proof_com : goal_kind -> Vernacexpr.proof_expr list -> unit declaration_hook -> unit -val start_proof_with_initialization : +val start_proof_with_initialization : goal_kind -> Evd.evar_map -> Univdecls.universe_decl -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> (Id.t (* name of thm *) * - (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list + (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit val universe_proof_terminator : diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 181068089e..58e4b00fc7 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1185,7 +1185,6 @@ let init_program () = Coqlib.check_required_library ["Coq";"Init";"Specif"]; Coqlib.check_required_library ["Coq";"Program";"Tactics"] - let set_program_mode c = if c then if !Flags.program_mode then () diff --git a/vernac/record.ml b/vernac/record.ml index 1cdc538b5b..114b55cb40 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -60,23 +60,25 @@ let _ = optread = (fun () -> !typeclasses_unique); optwrite = (fun b -> typeclasses_unique := b); } -let interp_fields_evars env evars impls_env nots l = +let interp_fields_evars env sigma impls_env nots l = List.fold_left2 - (fun (env, uimpls, params, impls) no ((loc, i), b, t) -> - let t', impl = interp_type_evars_impls env evars ~impls t in - let b' = Option.map (fun x -> fst (interp_casted_constr_evars_impls env evars ~impls x t')) b in + (fun (env, sigma, uimpls, params, impls) no ((loc, i), b, t) -> + let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in + let sigma, b' = + Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@ + interp_casted_constr_evars_impls env sigma ~impls x t') (sigma,None) b in let impls = match i with | Anonymous -> impls - | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method (EConstr.to_constr !evars t') impl) impls + | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method (EConstr.to_constr sigma t') impl) impls in let d = match b' with | None -> LocalAssum (i,t') | Some b' -> LocalDef (i,b',t') in List.iter (Metasyntax.set_notation_for_interpretation env impls) no; - (EConstr.push_rel d env, impl :: uimpls, d::params, impls)) - (env, [], [], impls_env) nots l + (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls)) + (env, sigma, [], [], impls_env) nots l let compute_constructor_level evars env l = List.fold_right (fun d (env, univ) -> @@ -97,10 +99,9 @@ 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 evd, decl = Univdecls.interp_univ_decl_opt env0 pl in - let evars = ref evd in - let _ = - let error bk (loc, name) = + let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in + let _ = + let error bk (loc, name) = match bk, name with | Default _, Anonymous -> user_err ?loc ~hdr:"record" (str "Record parameters must be named") @@ -112,63 +113,65 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = | CLocalPattern (loc,(_,_)) -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps in - let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in - let typ, sort, template = match t with + let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in + let sigma, typ, sort, template = match t with | Some t -> let env = EConstr.push_rel_context newps env0 in let poly = match t with | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in - let s = interp_type_evars env evars ~impls:empty_internalization_env t in - let sred = Reductionops.whd_all env !evars s in - (match EConstr.kind !evars sred with + let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in + let sred = Reductionops.whd_all env sigma s in + (match EConstr.kind sigma sred with | Sort s' -> - let s' = EConstr.ESorts.kind !evars s' in + let s' = EConstr.ESorts.kind sigma s' in (if poly then - match Evd.is_sort_variable !evars s' with - | Some l -> evars := Evd.make_flexible_variable !evars ~algebraic:true l; - s, s', true - | None -> s, s', false - else s, s', false) + match Evd.is_sort_variable sigma s' with + | Some l -> + let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in + sigma, s, s', true + | None -> + sigma, s, s', false + else sigma, s, s', false) | _ -> user_err ?loc:(constr_loc t) (str"Sort expected.")) | None -> let uvarkind = Evd.univ_flexible_alg in - let s = Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars in - EConstr.mkSort s, s, true + let sigma, s = Evd.new_sort_variable uvarkind sigma in + sigma, EConstr.mkSort s, s, true in let arity = EConstr.it_mkProd_or_LetIn typ newps in let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in let assums = List.filter is_local_assum newps in let params = List.map (RelDecl.get_name %> Name.get_id) assums in let ty = Inductive (params,(finite != BiFinite)) in - let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr !evars arity] [imps] in - let env2,impls,newfs,data = - interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs) + let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr sigma arity] [imps] in + let env2,sigma,impls,newfs,data = + interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) in - let evars = - Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars Evd.empty in - let typ, evars = - let _, univ = compute_constructor_level evars env_ar newfs in + let sigma = + Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma Evd.empty in + let sigma, typ = + let _, univ = compute_constructor_level sigma env_ar newfs in if not def && (Sorts.is_prop sort || (Sorts.is_set sort && is_impredicative_set env0)) then - typ, evars + sigma, typ else - let evars = Evd.set_leq_sort env_ar evars (Type univ) sort in + let sigma = Evd.set_leq_sort env_ar sigma (Type univ) sort in if Univ.is_small_univ univ && - Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars sort) then + Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then (* We can assume that the level in aritysort is not constrained and clear it, if it is flexible *) - EConstr.mkSort (Sorts.sort_of_univ univ), - Evd.set_eq_sort env_ar evars (Prop Pos) sort - else typ, evars + Evd.set_eq_sort env_ar sigma (Prop Pos) sort, + EConstr.mkSort (Sorts.sort_of_univ univ) + else sigma, typ in - let evars, nf = Evarutil.nf_evars_and_universes evars in - let newfs = List.map (EConstr.to_rel_decl evars) newfs in - let newps = List.map (EConstr.to_rel_decl evars) newps in - let typ = EConstr.to_constr evars typ in - let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in - let univs = Evd.check_univ_decl ~poly evars decl in - let ubinders = Evd.universe_binders evars in + let sigma, _ = Evarutil.nf_evars_and_universes sigma in + let newfs = List.map (EConstr.to_rel_decl sigma) newfs in + let newps = List.map (EConstr.to_rel_decl sigma) newps in + let typ = EConstr.to_constr sigma typ in + let ce t = Pretyping.check_evars env0 Evd.empty sigma (EConstr.of_constr t) in + let univs = Evd.check_univ_decl ~poly sigma decl in + let ubinders = Evd.universe_binders sigma in List.iter (iter_constr ce) (List.rev newps); List.iter (iter_constr ce) (List.rev newfs); ubinders, univs, typ, template, imps, newps, impls, newfs @@ -430,7 +433,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t | Monomorphic_const_entry _ -> mie in - let kn = Command.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in + let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 8673155e28..f001b572a5 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -11,7 +11,11 @@ Search Indschemes DeclareDef Obligations -Command +ComDefinition +ComAssumption +ComInductive +ComFixpoint +ComProgramFixpoint Classes Record Assumptions diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 161e0c5357..a581043ac1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -18,7 +18,6 @@ open Tacmach open Constrintern open Prettyp open Printer -open Command open Goptions open Libnames open Globnames @@ -479,6 +478,7 @@ let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def = | Discharge -> Dumpglob.dump_definition lid true "var" | Local | Global -> Dumpglob.dump_definition lid false "def" in + let program_mode = Flags.is_program_mode () in (match def with | ProveBody (bl,t) -> (* local binders, typ *) start_proof_and_print (local, atts.polymorphic, DefinitionBody kind) @@ -489,7 +489,7 @@ let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def = | Some r -> let sigma, env = Pfedit.get_current_context () in Some (snd (Hook.get f_interp_redexp env sigma r)) in - do_definition id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook) + ComDefinition.do_definition ~program_mode id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook) let vernac_start_proof ~atts kind l = let local = enforce_locality_exp atts.locality NoDischarge in @@ -520,7 +520,7 @@ let vernac_assumption ~atts discharge kind l nl = List.iter (fun (lid, _) -> if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl) l; - let status = do_assumptions kind nl l in + let status = ComAssumption.do_assumptions kind nl l in if not status then Feedback.feedback Feedback.AddedAxiom let should_treat_as_cumulative cum poly = @@ -592,18 +592,29 @@ let vernac_inductive ~atts cum lo finite indl = | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") in let indl = List.map unpack indl in - do_mutual_inductive indl is_cumulative atts.polymorphic lo finite + ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite let vernac_fixpoint ~atts discharge l = let local = enforce_locality_exp atts.locality discharge in if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; + (* XXX: Switch to the attribute system and match on ~atts *) + let do_fixpoint = if Flags.is_program_mode () then + ComProgramFixpoint.do_fixpoint + else + ComFixpoint.do_fixpoint + in do_fixpoint local atts.polymorphic l let vernac_cofixpoint ~atts discharge l = let local = enforce_locality_exp atts.locality discharge in if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; + let do_cofixpoint = if Flags.is_program_mode () then + ComProgramFixpoint.do_cofixpoint + else + ComFixpoint.do_cofixpoint + in do_cofixpoint local atts.polymorphic l let vernac_scheme l = @@ -627,14 +638,14 @@ let vernac_universe ~atts l = user_err ?loc:atts.loc ~hdr:"vernac_universe" (str"Polymorphic universes can only be declared inside sections, " ++ str "use Monomorphic Universe instead"); - do_universe atts.polymorphic l + Declare.do_universe atts.polymorphic l let vernac_constraint ~atts l = if atts.polymorphic && not (Lib.sections_are_opened ()) then user_err ?loc:atts.loc ~hdr:"vernac_constraint" (str"Polymorphic universe constraints can only be declared" ++ str " inside sections, use Monomorphic Constraint instead"); - do_constraint atts.polymorphic l + Declare.do_constraint atts.polymorphic l (**********************) (* Modules *) @@ -831,7 +842,8 @@ let vernac_identity_coercion ~atts id qids qidt = let vernac_instance ~atts abst sup inst props pri = let global = not (make_section_locality atts.locality) in Dumpglob.dump_constraint inst false "inst"; - ignore(Classes.new_instance ~abstract:abst ~global atts.polymorphic sup inst props pri) + let program_mode = Flags.is_program_mode () in + ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri) let vernac_context ~atts l = if not (Classes.context atts.polymorphic l) then Feedback.feedback Feedback.AddedAxiom |