diff options
112 files changed, 2150 insertions, 1449 deletions
diff --git a/.dir-locals.el b/.dir-locals.el deleted file mode 100644 index e32ce14a4..000000000 --- a/.dir-locals.el +++ /dev/null @@ -1,37 +0,0 @@ -;; EMACS CONFIGURATION FOR COQ DEVELOPPERS This configuration will be -;; executed for each opened file under coq root directory. -((nil - . ((eval - . (progn - ;; coq root directory (ending with slash) - (let ((coq-root-directory (when buffer-file-name - (locate-dominating-file - buffer-file-name - ".dir-locals.el"))) - (coq-project-find-file - (and (boundp 'coq-project-find-file) coq-project-find-file))) - ;; coq tags file and coq debugger executable - (set (make-local-variable 'tags-file-name) - (concat coq-root-directory "TAGS")) - (setq camldebug-command-name (concat coq-root-directory - "dev/ocamldebug-coq")) - - ;; Setting the compilation directory to coq root. This is - ;; mutually exclusive with the setting of default-directory - ;; below. Also setting the path for next error. - (unless coq-project-find-file - (set (make-local-variable 'compile-command) - (concat "make -C " coq-root-directory)) - (set (make-local-variable 'compilation-search-path) - (cons coq-root-directory nil))) - - ;; Set default directory to coq root ONLY IF variable - ;; coq-project-find-file is non nil. This should remain a - ;; user preference and not be set by default. This setting - ;; is redundant with compile-command above as M-x compile - ;; always CD's to default directory. To enable it add this - ;; to your emacs config: (setq coq-project-find-file t) - (when coq-project-find-file - (setq default-directory coq-root-directory)))) - )) - )) @@ -68,6 +68,11 @@ Universes module and library boundaries. Global universe names introduced in an inductive / constant / Let declaration get qualified with the name of the declaration. +- Universe cumulativity for inductive types is now specified as a + variance for each polymorphic universe. See the reference manual for + more information. +- Fix #5726: Notations that start with `Type` now support universe instances + with `@{u}`. Checker @@ -84,6 +89,18 @@ Documentation moved to the GitHub wiki section of this repository; the main entry page is https://github.com/coq/coq/wiki/The-Coq-FAQ. +Changes from 8.7.1 to 8.7.2 +=========================== + +Fixed a critical bug in the VM handling of universes (#6677). This bug +affected all releases since 8.5. + +Improved support for building with OCaml 4.06.0 and external num package. + +Many other bug fixes, documentation improvements, and user +message improvements (for details, see the 8.7.2 milestone at +https://github.com/coq/coq/milestone/11?closed=1). + Changes from 8.7.0 to 8.7.1 =========================== diff --git a/Makefile.build b/Makefile.build index 83e3c7ca9..39d177a13 100644 --- a/Makefile.build +++ b/Makefile.build @@ -406,17 +406,16 @@ $(COQTOPEXE): $(COQTOPBYTE) cp $< $@ endif -# Are "-cclib lcoqrun -dllib -lcoqrun" necessary? +# VMBYTEFLAGS will either contain -custom of the right -dllpath for the VM $(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLC) -linkall -linkpkg -I toplevel \ - -I kernel/byterun -dllpath $(abspath kernel/byterun) -cclib -lcoqrun -dllib -lcoqrun \ + -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \ $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \ $(LINKCMO) $(BYTEFLAGS) \ $(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@ -# coqc - +# For coqc COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo $(COQC): $(call bestobj, $(COQCCMO)) diff --git a/Makefile.ci b/Makefile.ci index 334827a93..80fbd7bbe 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -1,5 +1,4 @@ -CI_TARGETS=ci-all \ - ci-bignums \ +CI_TARGETS=ci-bignums \ ci-color \ ci-compcert \ ci-coq-dpdgraph \ @@ -23,7 +22,7 @@ CI_TARGETS=ci-all \ ci-unimath \ ci-vst -.PHONY: $(CI_TARGETS) +.PHONY: ci-all $(CI_TARGETS) ci-color: ci-bignums @@ -37,6 +36,8 @@ ci-formal-topology: ci-corn $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* +ci-all: $(CI_TARGETS) + # For emacs: # Local Variables: # mode: makefile diff --git a/checker/checker.ml b/checker/checker.ml index b8b4d5dc2..e8eff889c 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -18,7 +18,7 @@ let () = at_exit flush_all let chk_pp = Pp.pp_with Format.std_formatter let fatal_error info anomaly = - flush_all (); Feedback.msg_error info; flush_all (); + flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]%!@\n" Pp.pp_with info; flush_all (); exit (if anomaly then 129 else 1) let coq_root = Id.of_string "Coq" diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 4de597766..1807ae0ec 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -564,14 +564,23 @@ let check_subtyping cumi paramsctxt env inds = We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n] and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together with the cumulativity constraints [ cumul_cst ]. *) - let len = AUContext.size (ACumulativityInfo.univ_context cumi) in - let inst = Instance.of_array (Array.init len (fun i -> Level.var (i + len))) in + let uctx = ACumulativityInfo.univ_context cumi in + let len = AUContext.size uctx in + let inst = Instance.of_array @@ Array.init len (fun i -> Level.var (i + len)) in + let other_context = ACumulativityInfo.univ_context cumi in let uctx_other = UContext.make (inst, AUContext.instantiate inst other_context) in - let cumul_context = AUContext.repr (ACumulativityInfo.subtyp_context cumi) in - let cumul_cst = UContext.constraints cumul_context in + let cumul_cst = + Array.fold_left_i (fun i csts var -> + match var with + | Variance.Irrelevant -> csts + | Variance.Covariant -> Constraint.add (Level.var i,Le,Level.var (i+len)) csts + | Variance.Invariant -> Constraint.add (Level.var i,Eq,Level.var (i+len)) csts) + Constraint.empty (ACumulativityInfo.variance cumi) + in let env = Environ.push_context uctx_other env in let env = Environ.add_constraints cumul_cst env in + (* process individual inductive types: *) Array.iter (fun { mind_user_lc = lc; mind_arity = arity } -> match arity with diff --git a/checker/reduction.ml b/checker/reduction.ml index 29bb8901e..2297c90b3 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -158,24 +158,17 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 = let convert_inductive_instances cv_pb cumi u u' univs = let len_instance = Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in - let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in if not ((len_instance = Univ.Instance.length u) && (len_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else - let comp_cst = - let comp_subst = (Univ.Instance.append u u') in - Univ.AUContext.instantiate comp_subst ind_subtypctx - in + let variance = Univ.ACumulativityInfo.variance cumi in let comp_cst = match cv_pb with - CONV -> - let comp_cst' = - let comp_subst = (Univ.Instance.append u' u) in - Univ.AUContext.instantiate comp_subst ind_subtypctx - in - Univ.Constraint.union comp_cst comp_cst' - | CUMUL -> comp_cst + | CONV -> + Univ.Variance.eq_constraints variance u u' Univ.Constraint.empty + | CUMUL -> + Univ.Variance.leq_constraints variance u u' Univ.Constraint.empty in if (Univ.check_constraints comp_cst univs) then () else raise NotConvertible diff --git a/checker/univ.ml b/checker/univ.ml index 7d01657df..46b3ce680 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -1003,12 +1003,42 @@ end type abstract_universe_context = AUContext.t +module Variance = +struct + (** A universe position in the instance given to a cumulative + inductive can be the following. Note there is no Contravariant + case because [forall x : A, B <= forall x : A', B'] requires [A = + A'] as opposed to [A' <= A]. *) + type t = Irrelevant | Covariant | Invariant + + let leq_constraint csts variance u u' = + match variance with + | Irrelevant -> csts + | Covariant -> Constraint.add (u, Le, u') csts + | Invariant -> Constraint.add (u, Eq, u') csts + + let eq_constraint csts variance u u' = + match variance with + | Irrelevant -> csts + | Covariant | Invariant -> Constraint.add (u, Eq, u') csts + + let leq_constraints variance u u' csts = + let len = Array.length u in + assert (len = Array.length u' && len = Array.length variance); + Array.fold_left3 leq_constraint csts variance u u' + + let eq_constraints variance u u' csts = + let len = Array.length u in + assert (len = Array.length u' && len = Array.length variance); + Array.fold_left3 eq_constraint csts variance u u' +end + module CumulativityInfo = struct - type t = universe_context * universe_context + type t = universe_context * Variance.t array let univ_context (univcst, subtypcst) = univcst - let subtyp_context (univcst, subtypcst) = subtypcst + let variance (univs, variance) = variance end diff --git a/checker/univ.mli b/checker/univ.mli index 21c94d952..8c0685e0b 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -218,12 +218,25 @@ end type abstract_universe_context = AUContext.t +module Variance : +sig + (** A universe position in the instance given to a cumulative + inductive can be the following. Note there is no Contravariant + case because [forall x : A, B <= forall x : A', B'] requires [A = + A'] as opposed to [A' <= A]. *) + type t = Irrelevant | Covariant | Invariant + + val leq_constraints : t array -> Instance.t constraint_function + val eq_constraints : t array -> Instance.t constraint_function +end + + module ACumulativityInfo : sig type t val univ_context : t -> abstract_universe_context - val subtyp_context : t -> abstract_universe_context + val variance : t -> Variance.t array end diff --git a/checker/values.ml b/checker/values.ml index 313067cb6..55e1cdb6f 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -110,10 +110,12 @@ let v_cstrs = (v_tuple "univ_constraint" [|v_level;v_enum "order_request" 3;v_level|])) +let v_variance = v_enum "variance" 3 + let v_instance = Annot ("instance", Array v_level) let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|] let v_abs_context = v_context (* only for clarity *) -let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; v_context|] +let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|] let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] (** kernel/term *) diff --git a/dev/README b/dev/README index 6b83579de..453f85f0d 100644 --- a/dev/README +++ b/dev/README @@ -40,7 +40,11 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) Other development tools (directory tools) ----------------------- +coqdev.el: helper customizations for everyday Coq development, eg + making `compile' work in subdirectories + objects.el: various development utilities at emacs level + anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from the Emacs *compilation* output. diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 05fa33e97..d7a356930 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -19,6 +19,8 @@ else then export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" export CI_BRANCH="$CIRCLE_BRANCH" + else # assume local + export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" fi export COQBIN="$PWD/bin" fi diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index e3ec51aeb..ee9c8777a 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -14,7 +14,7 @@ then # skip PRs from before the linter existed if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ]; then - 2>&1 echo "Linting skipped: pull request older than the linter." + 1>&2 echo "Linting skipped: pull request older than the linter." exit 0 fi diff --git a/dev/tools/anomaly-traces-parser.el b/dev/tools/anomaly-traces-parser.el deleted file mode 100644 index 68f54266f..000000000 --- a/dev/tools/anomaly-traces-parser.el +++ /dev/null @@ -1,28 +0,0 @@ -;; This Elisp snippet adds a regexp parser for the format of Anomaly -;; backtraces (coqc -bt ...), to the error parser of the Compilation -;; mode (C-c C-c: "Compile command: ..."). Once the -;; coq-change-error-alist-for-backtraces function has run, file -;; locations in traces are recognized and can be jumped from easily -;; from the *compilation* buffer. - -;; You can just copy everything below to your .emacs and this will be -;; enabled from any compilation command launched from an OCaml file. - -(defun coq-change-error-alist-for-backtraces () - "Hook to change the compilation-error-regexp-alist variable, to - search the coq backtraces for error locations" - (interactive) - (add-to-list - 'compilation-error-regexp-alist-alist - '(coq-backtrace - "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\ - lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\ - \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)" - 2 (3 . 4) (5 . 6))) - (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) - -;; this Anomaly parser should be available when one is hacking -;; on the *OCaml* code of Coq (adding bugs), so we enable it -;; through the OCaml mode hooks. -(add-hook 'caml-mode-hook 'coq-change-error-alist-for-backtraces) -(add-hook 'tuareg-mode-hook 'coq-change-error-alist-for-backtraces) diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index d7acf01f1..e4359f703 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -50,6 +50,15 @@ else fi +if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then + echo + read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r + echo + if [[ ! $REPLY =~ ^[Yy]$ ]]; then + exit 1 + fi +fi + if [[ "${OPTION}" == "--stop-before-merging" ]]; then exit 0 fi diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el new file mode 100644 index 000000000..8c55be283 --- /dev/null +++ b/dev/tools/coqdev.el @@ -0,0 +1,106 @@ +;;; coqdev.el --- Emacs helpers for Coq development -*- lexical-binding:t -*- + +;; Copyright (C) 2018 The Coq Development Team + +;; Maintainer: coqdev@inria.fr + +;;; Commentary: + +;; Helpers to set compilation commands, proof general variables, etc +;; for Coq development + +;; You can disable individual features without editing this file by +;; using `remove-hook', for instance +;; (remove-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) + +;;; Installation: + +;; To use this, with coqdev.el located at /path/to/coqdev.el, add the +;; following to your init: + +;; (add-to-list 'load-path "/path/to/coqdev/") +;; (require 'coqdev) + +;; If you load this file from a git repository, checking out an old +;; commit will make it disappear and cause errors for your Emacs +;; startup. To ignore those errors use (require 'coqdev nil t). If you +;; check out a malicious commit Emacs startup would allow it to run +;; arbitrary code, to avoid this you can copy coqdev.el to any +;; location and adjust the load path accordingly (of course if you run +;; ./configure to compile Coq it is already too late). + +;;; Code: + +(defun coqdev-default-directory () + "Return the Coq repository containing `default-directory'." + (let ((dir (locate-dominating-file default-directory "META.coq"))) + (when dir (expand-file-name dir)))) + +(defun coqdev-setup-compile-command () + "Setup `compile-command' for Coq development." + (let ((dir (coqdev-default-directory))) + (when dir (setq-local compile-command (concat "make -C " (shell-quote-argument dir)))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) + +(defvar camldebug-command-name) ; from camldebug.el (caml package) +(defvar ocamldebug-command-name) ; from ocamldebug.el (tuareg package) +(defun coqdev-setup-camldebug () + "Setup ocamldebug for Coq development. + +Specifically `camldebug-command-name' and `ocamldebug-command-name'." + (let ((dir (coqdev-default-directory))) + (when dir + (setq-local camldebug-command-name + (concat dir "dev/ocamldebug-coq")) + (setq-local ocamldebug-command-name + (concat dir "dev/ocamldebug-coq"))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-camldebug) + +(defun coqdev-setup-tags () + "Setup `tags-file-name' for Coq development." + (let ((dir (coqdev-default-directory))) + (when dir (setq-local tags-file-name (concat dir "TAGS"))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-tags) + +(defvar coq-prog-args) +(defvar coq-prog-name) + +;; Lets us detect whether there are file local variables +;; even though PG sets it with `setq' when there's a _Coqproject. +;; Also makes sense generally, so might make it into PG someday. +(make-variable-buffer-local 'coq-prog-args) +(setq-default coq-prog-args nil) + +(defun coqdev-setup-proofgeneral () + "Setup Proofgeneral variables for Coq development. + +Note that this function is executed before _Coqproject is read if it exists." + (let ((dir (coqdev-default-directory))) + (when dir + (unless coq-prog-args + (setq coq-prog-args + `("-coqlib" ,dir "-R" ,(concat dir "plugins") + "Coq" "-R" ,(concat dir "theories") + "Coq"))) + (setq-local coq-prog-name (concat dir "bin/coqtop"))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) + +;; This Elisp snippet adds a regexp parser for the format of Anomaly +;; backtraces (coqc -bt ...), to the error parser of the Compilation +;; mode (C-c C-c: "Compile command: ..."). File locations in traces +;; are recognized and can be jumped from easily in the *compilation* +;; buffer. +(defvar compilation-error-regexp-alist-alist) +(defvar compilation-error-regexp-alist) +(with-eval-after-load 'compile + (add-to-list + 'compilation-error-regexp-alist-alist + '(coq-backtrace + "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\ + lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\ + \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)" + 2 (3 . 4) (5 . 6))) + (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) + +(provide 'coqdev) +;;; coqdev ends here diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 65926c69c..1cd23c929 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -917,9 +917,9 @@ This command displays whether some default timeout has be set or not. For debugging {\Coq} scripts, sometimes it is desirable to know whether a command or a tactic fails. If the given command or tactic fails, the {\tt Fail} statement succeeds, without changing the proof -state, and {\Coq} prints a message confirming the failure. If the -command or tactic succeeds, the statement is an error, and {\Coq} -prints a message indicating that the failure did not occur. +state, and in interactive mode, {\Coq} prints a message confirming the failure. +If the command or tactic succeeds, the statement is an error, and +{\Coq} prints a message indicating that the failure did not occur. \section{Controlling display} diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index a1a6a4391..6c84a1818 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -68,6 +68,13 @@ is only valid as long as \texttt{Top.4} is strictly smaller than monomorphic (not universe polymorphic), so the two universes (in this case \texttt{Top.3} and \texttt{Top.4}) are actually global levels. +When printing \texttt{pidentity}, we can see the universes it binds in +the annotation \texttt{@\{Top.2\}}. Additionally, when \texttt{Set + Printing Universes} is on we print the ``universe context'' of +\texttt{pidentity} consisting of the bound universes and the +constraints they must verify (for \texttt{pidentity} there are no +constraints). + Inductive types can also be declared universes polymorphic on universes appearing in their parameters or fields. A typical example is given by monoids: @@ -138,7 +145,7 @@ producing global universe constraints, one can use the \optindex{Polymorphic Inductive Cumulativity} Polymorphic inductive types, coinductive types, variants and records can be -declared cumulative using the \texttt{Cumulative}. Alternatively, +declared cumulative using the \texttt{Cumulative} prefix. Alternatively, there is an option \texttt{Set Polymorphic Inductive Cumulativity} which when set, makes all subsequent \emph{polymorphic} inductive definitions cumulative. When set, inductive types and the like can be enforced to be @@ -151,15 +158,22 @@ Polymorphic Cumulative Inductive list {A : Type} := \begin{coq_example} Print list. \end{coq_example} -When printing \texttt{list}, the part of the output of the form -\texttt{$\mathtt{\sim}$@\{i\} <= $\mathtt{\sim}$@\{j\} iff } -indicates the universe constraints in order to have the subtyping -$\WTEGLECONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ -(for fully applied instances of \texttt{list}) whenever $\WTEGCONV{A}{B}$. -In the case of \texttt{list} there is no constraint! -This also means that any two instances of \texttt{list} are convertible: -$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and -furthermore their corresponding (when fully applied to convertible arguments) constructors. +When printing \texttt{list}, the universe context indicates the +subtyping constraints by prefixing the level names with symbols. + +Because inductive subtypings are only produced by comparing inductives +to themselves with universes changed, they amount to variance +information: each universe is either invariant, covariant or +irrelevant (there are no contravariant subtypings in Coq), +respectively represented by the symbols \texttt{=}, \texttt{+} and +\texttt{*}. + +Here we see that \texttt{list} binds an irrelevant universe, so any +two instances of \texttt{list} are convertible: +$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever +$\WTEGCONV{A}{B}$ and furthermore their corresponding (when fully +applied to convertible arguments) constructors. + See Chapter~\ref{Cic} for more details on convertibility and subtyping. The following is an example of a record with non-trivial subtyping relation: \begin{coq_example*} @@ -168,8 +182,9 @@ Polymorphic Cumulative Record packType := {pk : Type}. \begin{coq_example} Print packType. \end{coq_example} -Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are -convertible if and only if \texttt{i $=$ j}. +\texttt{packType} binds a covariant universe, i.e. +$\WTEGCONV{\mathtt{packType@\{i\}}}{\mathtt{packType@\{j\}}}$ whenever +\texttt{i $\leq$ j}. Cumulative inductive types, coninductive types, variants and records only make sense when they are universe polymorphic. Therefore, an diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 9dc5d473b..3674bb943 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -107,7 +107,6 @@ struct let print_debug s = make (fun _ -> Feedback.msg_info s) let print_info s = make (fun _ -> Feedback.msg_info s) let print_warning s = make (fun _ -> Feedback.msg_warning s) - let print_error s = make (fun _ -> Feedback.msg_error s) let print_notice s = make (fun _ -> Feedback.msg_notice s) let run = fun x -> diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 8c8f9fe93..50b4abd8b 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -61,7 +61,6 @@ module NonLogical : sig val print_warning : Pp.t -> unit t val print_notice : Pp.t -> unit t val print_info : Pp.t -> unit t - val print_error : Pp.t -> unit t (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) diff --git a/engine/universes.ml b/engine/universes.ml index eaddf98a8..3a00f0fd1 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -1103,14 +1103,3 @@ let solve_constraints_system levels level_bounds level_min = done; done; v - - -(** Operations for universe_info_ind *) - -(** Given a universe context representing constraints of an inductive - this function produces a UInfoInd.t that with the trivial subtyping relation. *) -let univ_inf_ind_from_universe_context univcst = - let freshunivs = Instance.of_array - (Array.map (fun _ -> new_univ_level ()) - (Instance.to_array (UContext.instance univcst))) - in CumulativityInfo.from_universe_context univcst freshunivs diff --git a/engine/universes.mli b/engine/universes.mli index 130dcf8bb..cb6e2ba1b 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -221,9 +221,3 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.t val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array -> Universe.t array - -(** Operations for universe_info_ind *) - -(** Given a universe context representing constraints of an inductive - this function produces a UInfoInd.t that with the trivial subtyping relation. *) -val univ_inf_ind_from_universe_context : UContext.t -> CumulativityInfo.t diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 5f40a2242..6d1064d25 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -454,9 +454,11 @@ let slave_feeder fmt xml_oc msg = let msg_format = ref (fun () -> let margin = Option.default 72 (Topfmt.get_margin ()) in Xmlprotocol.Richpp margin -) + ) -let loop doc = +(* The loop ignores the command line arguments as the current model delegates + its handing to the toplevel container. *) +let loop _args doc = set_doc doc; init_signal_handler (); catch_break := false; @@ -504,8 +506,8 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let () = Coqtop.toploop_init := (fun args -> - let args = parse args in +let () = Coqtop.toploop_init := (fun coq_args extra_args -> + let args = parse extra_args in Flags.quiet := true; CoqworkmgrApi.(init High); args) diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 7cc8de85d..da04d8786 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -173,10 +173,12 @@ let rec constr_expr_eq e1 e2 = | CDelimiters(s1,e1), CDelimiters(s2,e2) -> String.equal s1 s2 && constr_expr_eq e1 e2 + | CProj(p1,c1), CProj(p2,c2) -> + eq_reference p1 p2 && constr_expr_eq c1 c2 | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _ | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _ | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _ - | CGeneralization _ | CDelimiters _), _ -> false + | CGeneralization _ | CDelimiters _ | CProj _), _ -> false and args_eq (a1,e1) (a2,e2) = Option.equal (eq_located explicitation_eq) e1 e2 && @@ -365,6 +367,8 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function (fold_local_binders g f n acc t lb) c lb) l acc | CCoFix (_,_) -> Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc + | CProj (_,c) -> + f n acc c ) let free_vars_of_constr_expr c = @@ -446,6 +450,8 @@ let map_constr_expr_with_binders g f e = CAst.map (function let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in let d' = f e'' d in (id,bl',t',d')) dl) + | CProj (p,c) -> + CProj (p, f e c) ) (* Used in constrintern *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 1330b3741..4f7d537d3 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -908,6 +908,9 @@ let rec extern inctx scopes vars r = | GCast (c, c') -> CCast (sub_extern true scopes vars c, Miscops.map_cast_type (extern_typ scopes vars) c') + | GProj (p, c) -> + let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in + CProj (pr, sub_extern inctx scopes vars c) ) r' and extern_typ (_,scopes) = diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 61b33aa41..4afe301dd 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -836,6 +836,18 @@ let intern_reference ref = in Smartlocate.global_of_extended_global r +let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option = + match info with + | Misctypes.UAnonymous -> None + | Misctypes.UUnknown -> None + | Misctypes.UNamed id -> Some (id, 0) + +let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort = + match level with + | Misctypes.GProp -> Misctypes.GProp + | Misctypes.GSet -> Misctypes.GSet + | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info] + (* Is it a global reference or a syntactic definition? *) let intern_qualid loc qid intern env lvar us args = match intern_extended_global_of_qualid (loc,qid) with @@ -867,6 +879,10 @@ let intern_qualid loc qid intern env lvar us args = DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg) | _ -> err () end + | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) + | Some [_old_level], GSort _new_sort -> + (* TODO: add old_level and new_sort to the error message *) + user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid) | Some _, _ -> err () in c, projapp, args2 @@ -1869,7 +1885,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CCast (c1, c2) -> DAst.make ?loc @@ GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2) - ) + | CProj (pr, c) -> + match intern_reference pr with + | ConstRef p -> + DAst.make ?loc @@ GProj (Projection.make p false, intern env c) + | _ -> + raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *) + ) and intern_type env = intern (set_type_scope env) and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list = diff --git a/interp/declare.ml b/interp/declare.ml index 55f825c25..72cdabfd2 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -364,13 +364,8 @@ let infer_inductive_subtyping (pth, mind_ent) = | Cumulative_ind_entry cumi -> begin let env = Global.env () in - let env' = - Environ.push_context - (Univ.CumulativityInfo.univ_context cumi) env - in (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) - let evd = Evd.from_env env' in - (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent) + (pth, InferCumulativity.infer_inductive env mind_ent) end type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry diff --git a/interp/discharge.ml b/interp/discharge.ml index 75bfca307..710f88c3f 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -92,7 +92,7 @@ let process_inductive info modlist mib = let auctx = Univ.ACumulativityInfo.univ_context cumi in let subst, auctx = Lib.discharge_abstract_universe_context info auctx in let auctx = Univ.AUContext.repr auctx in - subst, Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context auctx) + subst, Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context auctx) in let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in let inds = diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 20492e38c..326d05cba 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -86,9 +86,11 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with Miscops.glob_sort_eq s1 s2 | NCast (t1, c1), NCast (t2, c2) -> (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2 +| NProj (p1, c1), NProj (p2, c2) -> + Projection.equal p1 p2 && eq_notation_constr vars c1 c2 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NCast _), _ -> false + | NRec _ | NSort _ | NCast _ | NProj _), _ -> false (**********************************************************************) (* Re-interpret a notation as a glob_constr, taking care of binders *) @@ -189,6 +191,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = | NSort x -> GSort x | NHole (x, naming, arg) -> GHole (x, naming, arg) | NRef x -> GRef (x,None) + | NProj (p,c) -> GProj (p, f e c) let glob_constr_of_notation_constr ?loc x = let rec aux () x = @@ -383,6 +386,7 @@ let notation_constr_and_vars_of_glob_constr a = if arg != None then has_ltac := true; NHole (w, naming, arg) | GRef (r,_) -> NRef r + | GProj (p, c) -> NProj (p, aux c) | GEvar _ | GPatVar _ -> user_err Pp.(str "Existential variables not allowed in notations.") ) x @@ -576,6 +580,14 @@ let rec subst_notation_constr subst bound raw = let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in if r1' == r1 && k' == k then raw else NCast(r1',k') + | NProj (p, c) -> + let kn = Projection.constant p in + let b = Projection.unfolded p in + let kn' = subst_constant subst kn in + let c' = subst_notation_constr subst bound c in + if kn' == kn && c' == c then raw else NProj(Projection.make kn' b, c') + + let subst_interpretation subst (metas,pat) = let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in (metas,subst_notation_constr subst bound pat) @@ -1167,9 +1179,12 @@ let rec match_ inner u alp metas sigma a1 a2 = match_names metas (alp,sigma) (Name id') na in match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2 + | GProj(p1, t1), NProj(p2, t2) when Projection.equal p1 p2 -> + match_in u alp metas sigma t1 t2 + | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ - | GCast _), _ -> raise No_match + | GCast _ | GProj _ ), _ -> raise No_match and match_in u = match_ true u diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index 8bcdbcc0e..fbf9e248a 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -97,6 +97,7 @@ and constr_expr_r = | CGeneralization of binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token | CDelimiters of string * constr_expr + | CProj of reference * constr_expr and constr_expr = constr_expr_r CAst.t and case_expr = constr_expr (* expression that is being matched *) diff --git a/intf/glob_term.ml b/intf/glob_term.ml index f311d33b8..61bbe2c26 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -55,6 +55,7 @@ type 'a glob_constr_r = | GSort of glob_sort | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type + | GProj of Projection.t * 'a glob_constr_g and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 7823d3feb..cad6f4b82 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -43,6 +43,7 @@ type notation_constr = notation_constr array * notation_constr array | NSort of glob_sort | NCast of notation_constr * notation_constr cast_type + | NProj of Projection.t * notation_constr (** Note concerning NList: first constr is iterator, second is terminator; first id is where each argument of the list has to be substituted diff --git a/intf/pattern.ml b/intf/pattern.ml index 20636accf..64873a039 100644 --- a/intf/pattern.ml +++ b/intf/pattern.ml @@ -26,7 +26,7 @@ type constr_pattern = | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of patvar * constr_pattern list - | PProj of projection * constr_pattern + | PProj of Projection.t * constr_pattern | PLambda of Name.t * constr_pattern * constr_pattern | PProd of Name.t * constr_pattern * constr_pattern | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 5dab2932d..4a34dbcff 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -628,27 +628,17 @@ let rec compile_constr reloc c sz cont = of the structured constant, while the later (if any) will be applied as arguments. *) let open Univ in begin - let levels = Universe.levels u in - let global_levels = - LSet.filter (fun x -> Level.var_index x = None) levels - in - let local_levels = - List.map_filter (fun x -> Level.var_index x) - (LSet.elements levels) - in + let u,s = Universe.compact u in (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *) - let uglob = - LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m - in - if local_levels = [] then - compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type uglob))) sz cont + if List.is_empty s then + compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type u))) sz cont else let compile_get_univ reloc idx sz cont = set_max_stack_size sz; compile_fv_elem reloc (FVuniv_var idx) sz cont in comp_app compile_str_cst compile_get_univ reloc - (Bstrconst (Const_type u)) (Array.of_list local_levels) sz cont + (Bstrconst (Const_type u)) (Array.of_list s) sz cont end | LetIn(_,xb,_,body) -> compile_constr reloc xb sz diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 2bbb867cd..bbd284bc1 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -70,7 +70,7 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_bn _, _ -> false | Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 | Const_univ_level _ , _ -> false -| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2 +| Const_type u1, Const_type u2 -> Univ.Universe.equal u1 u2 | Const_type _ , _ -> false let rec hash_structured_constant c = diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b117f8714..cfca335d3 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -234,22 +234,32 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) let check_subtyping cumi paramsctxt env_ar inds = let numparams = Context.Rel.nhyps paramsctxt in - let sbsubst = CumulativityInfo.subtyping_susbst cumi in - let dosubst = subst_univs_level_constr sbsubst in let uctx = CumulativityInfo.univ_context cumi in - let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in - let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in + let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in + let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) + LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels + in + let dosubst = subst_univs_level_constr lmap in + let instance_other = Instance.of_array new_levels in + let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in let env = Environ.push_context uctx env_ar in let env = Environ.push_context uctx_other env in - let env = push_context (CumulativityInfo.subtyp_context cumi) env in + let subtyp_constraints = + CumulativityInfo.leq_constraints cumi + (UContext.instance uctx) instance_other + Constraint.empty + in + let env = Environ.add_constraints subtyp_constraints env in (* process individual inductive types: *) Array.iter (fun (id,cn,lc,(sign,arity)) -> match arity with | RegularArity (_, full_arity, _) -> check_subtyping_arity_constructor env dosubst full_arity numparams true; Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc - | TemplateArity _ -> () + | TemplateArity _ -> + anomaly ~label:"check_subtyping" + Pp.(str "template polymorphism and cumulative polymorphism are not compatible") ) inds (* Type-check an inductive definition. Does not check positivity diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 4e7d6b218..1e35f6c03 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -157,9 +157,8 @@ let call_linker ?(fatal=true) prefix f upds = register_native_file prefix with Dynlink.Error e as exn -> let exn = CErrors.push exn in - let msg = "Dynlink error, " ^ Dynlink.error_message e in - if fatal then (Feedback.msg_error (Pp.str msg); iraise exn) - else if !Flags.debug then Feedback.msg_debug (Pp.str msg)); + if fatal then iraise exn + else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); match upds with Some upds -> update_locations upds | _ -> () let link_library ~prefix ~dirname ~basename = diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1724f210d..da7042713 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -200,13 +200,9 @@ let is_cumul = function CUMUL -> true | CONV -> false type 'a universe_compare = { (* Might raise NotConvertible *) - compare : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; + compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int -> - Univ.Instance.t -> int -> 'a -> 'a; - conv_constructors : (Declarations.mutual_inductive_body * int * int) -> - Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a; - } + compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a } type 'a universe_state = 'a * 'a universe_compare @@ -215,18 +211,68 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t let sort_cmp_universes env pb s0 s1 (u, check) = - (check.compare env pb s0 s1 u, check) + (check.compare_sorts env pb s0 s1 u, check) (* [flex] should be true for constants, false for inductive types and constructors. *) let convert_instances ~flex u u' (s, check) = (check.compare_instances ~flex u u' s, check) - -let convert_inductives cv_pb ind u1 sv1 u2 sv2 (s, check) = - (check.conv_inductives cv_pb ind u1 sv1 u2 sv2 s, check) -let convert_constructors cons u1 sv1 u2 sv2 (s, check) = - (check.conv_constructors cons u1 sv1 u2 sv2 s, check) +let get_cumulativity_constraints cv_pb cumi u u' = + match cv_pb with + | CONV -> + Univ.ACumulativityInfo.eq_constraints cumi u u' Univ.Constraint.empty + | CUMUL -> + Univ.ACumulativityInfo.leq_constraints cumi u u' Univ.Constraint.empty + +let inductive_cumulativity_arguments (mind,ind) = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + +let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s = + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); + s + | Declarations.Polymorphic_ind _ -> + cmp_instances u1 u2 s + | Declarations.Cumulative_ind cumi -> + let num_param_arity = inductive_cumulativity_arguments (mind,ind) in + if not (Int.equal num_param_arity nargs) then + cmp_instances u1 u2 s + else + let csts = get_cumulativity_constraints cv_pb cumi u1 u2 in + cmp_cumul csts s + +let convert_inductives cv_pb ind nargs u1 u2 (s, check) = + convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances + cv_pb ind nargs u1 u2 s, check + +let constructor_cumulativity_arguments (mind, ind, ctor) = + let nparamsctxt = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in + nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1) + +let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s = + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); + s + | Declarations.Polymorphic_ind _ -> + cmp_instances u1 u2 s + | Declarations.Cumulative_ind cumi -> + let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in + if not (Int.equal num_cnstr_args nargs) then + cmp_instances u1 u2 s + else + let csts = get_cumulativity_constraints CONV cumi u1 u2 in + cmp_cumul csts s + +let convert_constructors ctor nargs u1 u2 (s, check) = + convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances + ctor nargs u1 u2 s, check let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else @@ -325,9 +371,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if in_whnf st1' then (st1',st2') else whd_both st1' st2' in let ((hd1,v1),(hd2,v2)) = whd_both st1 st2 in let appr1 = (lft1,(hd1,v1)) and appr2 = (lft2,(hd2,v2)) in - (* compute the lifts that apply to the head of the term (hd1 and hd2) *) - let el1 = el_stack lft1 v1 in - let el2 = el_stack lft2 v2 in + (** We delay the computation of the lifts that apply to the head of the term + with [el_stack] inside the branches where they are actually used. *) match (fterm_of hd1, fterm_of hd2) with (* case of leaves *) | (FAtom a1, FAtom a2) -> @@ -343,6 +388,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | _ -> raise NotConvertible) | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) -> if Evar.equal ev1 ev2 then + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in convert_vect l2r infos el1 el2 (Array.map (mk_clos env1) args1) @@ -351,6 +398,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* 2 index known to be bound to no constant *) | (FRel n, FRel m) -> + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in if Int.equal (reloc_rel n el1) (reloc_rel m el2) then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible @@ -395,6 +444,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | None -> if Constant.equal (Projection.constant p1) (Projection.constant p2) && compare_stack_shape v1 v2 then + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 u1 else (* Two projections in WHNF: unfold *) @@ -434,6 +485,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = anomaly (Pp.str "conversion was given ill-typed terms (FLambda)."); let (_,ty1,bd1) = destFLambda mk_clos hd1 in let (_,ty2,bd2) = destFLambda mk_clos hd2 in + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv @@ -441,6 +494,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if not (is_empty_stack v1 && is_empty_stack v2) then anomaly (Pp.str "conversion was given ill-typed terms (FProd)."); (* Luo's system *) + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv @@ -509,15 +564,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else let mind = Environ.lookup_mind (fst ind1) (info_env infos) in - let cuniv = - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> - convert_instances ~flex:false u1 u2 cuniv - | Declarations.Cumulative_ind cumi -> - convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1) - u2 (CClosure.stack_args_size v2) cuniv - in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + let nargs = CClosure.stack_args_size v1 in + if not (Int.equal nargs (CClosure.stack_args_size v2)) + then raise NotConvertible + else + let cuniv = convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> @@ -527,16 +579,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else let mind = Environ.lookup_mind (fst ind1) (info_env infos) in - let cuniv = - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> - convert_instances ~flex:false u1 u2 cuniv - | Declarations.Cumulative_ind _ -> - convert_constructors - (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1) - u2 (CClosure.stack_args_size v2) cuniv - in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + let nargs = CClosure.stack_args_size v1 in + if not (Int.equal nargs (CClosure.stack_args_size v2)) + then raise NotConvertible + else + let cuniv = convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* Eta expansion of records *) @@ -562,6 +610,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let fty2 = Array.map (mk_clos e2) tys2 in let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in let cuniv = convert_vect l2r infos @@ -577,6 +627,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let fty2 = Array.map (mk_clos e2) tys2 in let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in let cuniv = convert_vect l2r infos @@ -653,84 +705,14 @@ let check_convert_instances ~flex u u' univs = else raise NotConvertible (* general conversion and inference functions *) -let infer_check_conv_inductives - infer_check_convert_instances - infer_check_inductive_instances - cv_pb (mind, ind) u1 sv1 u2 sv2 univs = - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> - infer_check_convert_instances ~flex:false u1 u2 univs - | Declarations.Cumulative_ind cumi -> - let num_param_arity = - mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - in - if not (num_param_arity = sv1 && num_param_arity = sv2) then - infer_check_convert_instances ~flex:false u1 u2 univs - else - infer_check_inductive_instances cv_pb cumi u1 u2 univs - -let infer_check_conv_constructors - infer_check_convert_instances - infer_check_inductive_instances - (mind, ind, cns) u1 sv1 u2 sv2 univs = - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> - infer_check_convert_instances ~flex:false u1 u2 univs - | Declarations.Cumulative_ind cumi -> - let num_cnstr_args = - let nparamsctxt = - mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in - nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) - in - if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then - infer_check_convert_instances ~flex:false u1 u2 univs - else - infer_check_inductive_instances CONV cumi u1 u2 univs - -let check_inductive_instances cv_pb cumi u u' univs = - let length_ind_instance = - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) - in - let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in - if not ((length_ind_instance = Univ.Instance.length u) && - (length_ind_instance = Univ.Instance.length u')) then - anomaly (Pp.str "Invalid inductive subtyping encountered!") - else - let comp_cst = - let comp_subst = (Univ.Instance.append u u') in - Univ.AUContext.instantiate comp_subst ind_subtypctx - in - let comp_cst = - match cv_pb with - CONV -> - let comp_cst' = - let comp_subst = (Univ.Instance.append u' u) in - Univ.AUContext.instantiate comp_subst ind_subtypctx - in - Univ.Constraint.union comp_cst comp_cst' - | CUMUL -> comp_cst - in - if (UGraph.check_constraints comp_cst univs) then univs - else raise NotConvertible - -let check_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs = - infer_check_conv_inductives - check_convert_instances - check_inductive_instances - cv_pb ind u1 sv1 u2 sv2 univs - -let check_conv_constructors cns u1 sv1 u2 sv2 univs = - infer_check_conv_constructors - check_convert_instances - check_inductive_instances - cns u1 sv1 u2 sv2 univs +let check_inductive_instances csts univs = + if (UGraph.check_constraints csts univs) then univs + else raise NotConvertible let checked_universes = - { compare = checked_sort_cmp_universes; + { compare_sorts = checked_sort_cmp_universes; compare_instances = check_convert_instances; - conv_inductives = check_conv_inductives; - conv_constructors = check_conv_constructors} + compare_cumul_instances = check_inductive_instances; } let infer_eq (univs, cstrs as cuniv) u u' = if UGraph.check_eq univs u u' then cuniv @@ -773,49 +755,13 @@ let infer_convert_instances ~flex u u' (univs,cstrs) = else Univ.enforce_eq_instances u u' cstrs in (univs, cstrs') -let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) = - let length_ind_instance = - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) - in - let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in - if not ((length_ind_instance = Univ.Instance.length u) && - (length_ind_instance = Univ.Instance.length u')) then - anomaly (Pp.str "Invalid inductive subtyping encountered!") - else - let comp_cst = - let comp_subst = (Univ.Instance.append u u') in - Univ.AUContext.instantiate comp_subst ind_subtypctx - in - let comp_cst = - match cv_pb with - CONV -> - let comp_cst' = - let comp_subst = (Univ.Instance.append u' u) in - Univ.AUContext.instantiate comp_subst ind_subtypctx - in - Univ.Constraint.union comp_cst comp_cst' - | CUMUL -> comp_cst - in - (univs, Univ.Constraint.union cstrs comp_cst) - - -let infer_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs = - infer_check_conv_inductives - infer_convert_instances - infer_inductive_instances - cv_pb ind u1 sv1 u2 sv2 univs - -let infer_conv_constructors cns u1 sv1 u2 sv2 univs = - infer_check_conv_constructors - infer_convert_instances - infer_inductive_instances - cns u1 sv1 u2 sv2 univs - -let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = - { compare = infer_cmp_universes; +let infer_inductive_instances csts (univs,csts') = + (univs, Univ.Constraint.union csts csts') + +let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = + { compare_sorts = infer_cmp_universes; compare_instances = infer_convert_instances; - conv_inductives = infer_conv_inductives; - conv_constructors = infer_conv_constructors} + compare_cumul_instances = infer_inductive_instances; } let gen_conv cv_pb l2r reds env evars univs t1 t2 = let b = @@ -936,6 +882,18 @@ let hnf_prod_app env t n = let hnf_prod_applist env t nl = List.fold_left (hnf_prod_app env) t nl +let hnf_prod_applist_assum env n c l = + let rec app n subst t l = + if Int.equal n 0 then + if l == [] then substl subst t + else anomaly (Pp.str "Too many arguments.") + else match kind (whd_allnolet env t), l with + | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _, [] -> anomaly (Pp.str "Not enough arguments.") + | _ -> anomaly (Pp.str "Not enough prod/let's.") in + app n [] c l + (* Dealing with arities *) let dest_prod env = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 573e4c8bd..6f7e3f8f8 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -35,15 +35,11 @@ type 'a extended_conversion_function = type conv_pb = CONV | CUMUL -type 'a universe_compare = +type 'a universe_compare = { (* Might raise NotConvertible *) - compare : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; + compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int -> - Univ.Instance.t -> int -> 'a -> 'a; - conv_constructors : (Declarations.mutual_inductive_body * int * int) -> - Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a; - } + compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a } type 'a universe_state = 'a * 'a universe_compare @@ -51,6 +47,12 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t +val get_cumulativity_constraints : conv_pb -> Univ.ACumulativityInfo.t -> + Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t + +val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int +val constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int + val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare @@ -103,6 +105,12 @@ val beta_app : constr -> constr -> constr (** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types +(** In [hnf_prod_applist_assum n c args], [c] is supposed to (whd-)reduce to + the form [∀Γ.t] with [Γ] of length [n] and possibly with let-ins; it + returns [t] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val hnf_prod_applist_assum : env -> int -> types -> constr list -> types + (** Compatibility alias for Term.lambda_appvect_assum *) val betazeta_appvect : int -> constr -> constr array -> constr diff --git a/kernel/term.ml b/kernel/term.ml index fae990d45..a4c92bd33 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -352,10 +352,11 @@ let lambda_applist_assum n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments.") + else anomaly (Pp.str "Too many arguments.") else match kind_of_term t, l with | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _, [] -> anomaly (Pp.str "Not enough arguments.") | _ -> anomaly (Pp.str "Not enough lambda/let's.") in app n [] c l @@ -377,10 +378,11 @@ let prod_applist_assum n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments.") + else anomaly (Pp.str "Too many arguments.") else match kind_of_term t, l with | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _, [] -> anomaly (Pp.str "Not enough arguments.") | _ -> anomaly (Pp.str "Not enough prod/let's.") in app n [] c l diff --git a/kernel/term.mli b/kernel/term.mli index c9a8cf6e1..b4597676a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -242,7 +242,7 @@ val lambda_applist : constr -> constr list -> constr val lambda_appvect : constr -> constr array -> constr (** In [lambda_applist_assum n c args], [c] is supposed to have the - form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it + form [λΓ.c] with [Γ] of length [n] and possibly with let-ins; it returns [c] with the assumptions of [Γ] instantiated by [args] and the local definitions of [Γ] expanded. *) val lambda_applist_assum : int -> constr -> constr list -> constr @@ -251,15 +251,15 @@ val lambda_appvect_assum : int -> constr -> constr array -> constr (** pseudo-reduction rule *) (** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *) -val prod_appvect : constr -> constr array -> constr -val prod_applist : constr -> constr list -> constr +val prod_appvect : types -> constr array -> types +val prod_applist : types -> constr list -> types (** In [prod_appvect_assum n c args], [c] is supposed to have the - form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it + form [∀Γ.c] with [Γ] of length [n] and possibly with let-ins; it returns [c] with the assumptions of [Γ] instantiated by [args] and the local definitions of [Γ] expanded. *) -val prod_appvect_assum : int -> constr -> constr array -> constr -val prod_applist_assum : int -> constr -> constr list -> constr +val prod_appvect_assum : int -> types -> constr array -> types +val prod_applist_assum : int -> types -> constr list -> types (** {5 Other term destructors. } *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 5f501bff1..9b864440d 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -223,9 +223,8 @@ let rec unzip ctx j = unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) } let feedback_completion_typecheck = - let open Feedback in Option.iter (fun state_id -> - feedback ~id:state_id Feedback.Complete) + Feedback.feedback ~id:state_id Feedback.Complete) let abstract_constant_universes = function | Monomorphic_const_entry uctx -> diff --git a/kernel/univ.ml b/kernel/univ.ml index f72f6f26a..fbb047364 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -266,7 +266,7 @@ struct module Expr = struct type t = Level.t * int - + (* Hashing of expressions *) module ExprHash = struct @@ -487,7 +487,40 @@ struct | [] -> cons a l in List.fold_right (fun a acc -> aux a acc) u [] - + + (** [max_var_pred p u] returns the maximum variable level in [u] satisfying + [p], -1 if not found *) + let rec max_var_pred p u = + let open Level in + match u with + | [] -> -1 + | (v, _) :: u -> + match var_index v with + | Some i when p i -> max i (max_var_pred p u) + | _ -> max_var_pred p u + + let rec remap_var u i j = + let open Level in + match u with + | [] -> [] + | (v, incr) :: u when var_index v = Some i -> + (Level.var j, incr) :: remap_var u i j + | _ :: u -> remap_var u i j + + let rec compact u max_var i = + if i >= max_var then (u,[]) else + let j = max_var_pred (fun j -> j < i) u in + if Int.equal i (j+1) then + let (u,s) = compact u max_var (i+1) in + (u, i :: s) + else + let (u,s) = compact (remap_var u i j) max_var (i+1) in + (u, j+1 :: s) + + let compact u = + let max_var = max_var_pred (fun _ -> true) u in + compact u max_var 0 + (* Returns the formal universe that is greater than the universes u and v. Used to type the products. *) let sup x y = merge_univs x y @@ -712,7 +745,48 @@ type universe_level_subst = universe_level universe_map (** A full substitution might involve algebraic universes *) type universe_subst = universe universe_map -module Instance : sig +module Variance = +struct + (** A universe position in the instance given to a cumulative + inductive can be the following. Note there is no Contravariant + case because [forall x : A, B <= forall x : A', B'] requires [A = + A'] as opposed to [A' <= A]. *) + type t = Irrelevant | Covariant | Invariant + + let sup x y = + match x, y with + | Irrelevant, s | s, Irrelevant -> s + | Invariant, _ | _, Invariant -> Invariant + | Covariant, Covariant -> Covariant + + let pr = function + | Irrelevant -> str "*" + | Covariant -> str "+" + | Invariant -> str "=" + + let leq_constraint csts variance u u' = + match variance with + | Irrelevant -> csts + | Covariant -> enforce_leq_level u u' csts + | Invariant -> enforce_eq_level u u' csts + + let eq_constraint csts variance u u' = + match variance with + | Irrelevant -> csts + | Covariant | Invariant -> enforce_eq_level u u' csts + + let leq_constraints variance u u' csts = + let len = Array.length u in + assert (len = Array.length u' && len = Array.length variance); + Array.fold_left3 leq_constraint csts variance u u' + + let eq_constraints variance u u' csts = + let len = Array.length u in + assert (len = Array.length u' && len = Array.length variance); + Array.fold_left3 eq_constraint csts variance u u' +end + +module Instance : sig type t = Level.t array val empty : t @@ -732,7 +806,7 @@ module Instance : sig val subst_fn : universe_level_subst_fn -> t -> t - val pr : (Level.t -> Pp.t) -> t -> Pp.t + val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t val levels : t -> LSet.t end = struct @@ -808,8 +882,12 @@ struct let levels x = LSet.of_array x - let pr = - prvect_with_sep spc + let pr prl ?variance = + let ppu i u = + let v = Option.map (fun v -> v.(i)) variance in + pr_opt_no_spc Variance.pr v ++ prl u + in + prvecti_with_sep spc ppu let equal t u = t == u || @@ -873,9 +951,9 @@ struct let empty = (Instance.empty, Constraint.empty) let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst - let pr prl (univs, cst as ctx) = + let pr prl ?variance (univs, cst as ctx) = if is_empty ctx then mt() else - h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) + h 0 (Instance.pr prl ?variance univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) let hcons (univs, cst) = (Instance.hcons univs, hcons_constraints cst) @@ -911,66 +989,42 @@ end type abstract_universe_context = AUContext.t let hcons_abstract_universe_context = AUContext.hcons -(** Universe info for cumulative inductive types: - A context of universe levels - with universe constraints, representing local universe variables - and constraints, together with a context of universe levels with - universe constraints, representing conditions for subtyping used - for inductive types. +(** Universe info for cumulative inductive types: A context of + universe levels with universe constraints, representing local + universe variables and constraints, together with an array of + Variance.t. - This data structure maintains the invariant that the context for - subtyping constraints is exactly twice as big as the context for - universe constraints. *) + This data structure maintains the invariant that the variance + array has the same length as the universe instance. *) module CumulativityInfo = struct - type t = universe_context * universe_context + type t = universe_context * Variance.t array let make x = - if (Instance.length (UContext.instance (snd x))) = - (Instance.length (UContext.instance (fst x))) * 2 then x + if (Instance.length (UContext.instance (fst x))) = + (Array.length (snd x)) then x else anomaly (Pp.str "Invalid subtyping information encountered!") - let empty = (UContext.empty, UContext.empty) - let is_empty (univcst, subtypcst) = UContext.is_empty univcst && UContext.is_empty subtypcst - - let halve_context ctx = - let len = Array.length (Instance.to_array ctx) in - let halflen = len / 2 in - (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen), - Instance.of_array (Array.sub (Instance.to_array ctx) halflen halflen)) + let empty = (UContext.empty, [||]) + let is_empty (univs, variance) = UContext.is_empty univs && Array.is_empty variance - let pr prl (univcst, subtypcst) = - if UContext.is_empty univcst then mt() else - let (ctx, ctx') = halve_context (UContext.instance subtypcst) in - (UContext.pr prl univcst) ++ fnl () ++ fnl () ++ - h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "} iff ") - ++ fnl () ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst))) + let pr prl (univs, variance) = + UContext.pr prl ~variance univs - let hcons (univcst, subtypcst) = - (UContext.hcons univcst, UContext.hcons subtypcst) + let hcons (univs, variance) = (* should variance be hconsed? *) + (UContext.hcons univs, variance) - let univ_context (univcst, subtypcst) = univcst - let subtyp_context (univcst, subtypcst) = subtypcst - - let create_trivial_subtyping ctx ctx' = - CArray.fold_left_i - (fun i cst l -> Constraint.add (l, Eq, Array.get ctx' i) cst) - Constraint.empty (Instance.to_array ctx) + let univ_context (univs, subtypcst) = univs + let variance (univs, variance) = variance (** This function takes a universe context representing constraints - of an inductive and a Instance.t of fresh universe names for the - subtyping (with the same length as the context in the given - universe context) and produces a UInfoInd.t that with the - trivial subtyping relation. *) - let from_universe_context univcst freshunivs = - let inst = (UContext.instance univcst) in - assert (Instance.length freshunivs = Instance.length inst); - (univcst, UContext.make (Instance.append inst freshunivs, - create_trivial_subtyping inst freshunivs)) - - let subtyping_susbst (univcst, subtypcst) = - let (ctx, ctx') = (halve_context (UContext.instance subtypcst))in - Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx' + of an inductive and produces a CumulativityInfo.t with the + trivial subtyping relation. *) + let from_universe_context univs = + (univs, Array.init (UContext.size univs) (fun _ -> Variance.Invariant)) + + let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts + let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts end @@ -1138,10 +1192,9 @@ let abstract_universes ctx = let ctx = UContext.make (instance, cstrs) in instance, ctx -let abstract_cumulativity_info (univcst, substcst) = - let instance, univcst = abstract_universes univcst in - let _, substcst = abstract_universes substcst in - (instance, (univcst, substcst)) +let abstract_cumulativity_info (univs, variance) = + let subst, univs = abstract_universes univs in + subst, (univs, variance) (** Pretty-printing *) diff --git a/kernel/univ.mli b/kernel/univ.mli index 63bef1b81..c45ebe21c 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -125,6 +125,13 @@ sig val for_all : (Level.t * int -> bool) -> t -> bool val map : (Level.t * int -> 'a) -> t -> 'a list + + (** [compact u] remaps local variables in [u] such that their indices become + consecutive. It returns the new universe and the mapping. + Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] = + [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2] + *) + val compact : t -> t * int list end type universe = Universe.t @@ -238,6 +245,20 @@ type universe_level_subst_fn = Level.t -> Level.t type universe_subst = Universe.t universe_map type universe_level_subst = Level.t universe_map +module Variance : +sig + (** A universe position in the instance given to a cumulative + inductive can be the following. Note there is no Contravariant + case because [forall x : A, B <= forall x : A', B'] requires [A = + A'] as opposed to [A' <= A]. *) + type t = Irrelevant | Covariant | Invariant + + val sup : t -> t -> t + + val pr : t -> Pp.t + +end + (** {6 Universe instances} *) module Instance : @@ -273,7 +294,7 @@ sig val subst_fn : universe_level_subst_fn -> t -> t (** Substitution by a level-to-level function. *) - val pr : (Level.t -> Pp.t) -> t -> Pp.t + val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t (** Pretty-printing, no comments *) val levels : t -> LSet.t @@ -347,36 +368,32 @@ end type abstract_universe_context = AUContext.t [@@ocaml.deprecated "Use AUContext.t"] -(** Universe info for inductive types: A context of universe levels - with universe Constraint.t, representing local universe variables - and Constraint.t, together with a context of universe levels with - universe Constraint.t, representing conditions for subtyping used - for inductive types. +(** Universe info for cumulative inductive types: A context of + universe levels with universe constraints, representing local + universe variables and constraints, together with an array of + Variance.t. - This data structure maintains the invariant that the context for - subtyping Constraint.t is exactly twice as big as the context for - universe Constraint.t. *) + This data structure maintains the invariant that the variance + array has the same length as the universe instance. *) module CumulativityInfo : sig type t - val make : UContext.t * UContext.t -> t + val make : UContext.t * Variance.t array -> t val empty : t val is_empty : t -> bool val univ_context : t -> UContext.t - val subtyp_context : t -> UContext.t - - (** This function takes a universe context representing Constraint.t - of an inductive and a Instance.t of fresh universe names for the - subtyping (with the same length as the context in the given - universe context) and produces a UInfoInd.t that with the - trivial subtyping relation. *) - val from_universe_context : UContext.t -> Instance.t -> t + val variance : t -> Variance.t array - val subtyping_susbst : t -> universe_level_subst + (** This function takes a universe context representing constraints + of an inductive and produces a CumulativityInfo.t with the + trivial subtyping relation. *) + val from_universe_context : UContext.t -> t + val leq_constraints : t -> Instance.t constraint_function + val eq_constraints : t -> Instance.t constraint_function end type cumulativity_info = CumulativityInfo.t @@ -387,7 +404,9 @@ sig type t val univ_context : t -> AUContext.t - val subtyp_context : t -> AUContext.t + val variance : t -> Variance.t array + val leq_constraints : t -> Instance.t constraint_function + val eq_constraints : t -> Instance.t constraint_function end type abstract_cumulativity_info = ACumulativityInfo.t @@ -481,9 +500,11 @@ val make_abstract_instance : AUContext.t -> Instance.t val pr_constraint_type : constraint_type -> Pp.t val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t -val pr_universe_context : (Level.t -> Pp.t) -> UContext.t -> Pp.t +val pr_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array -> + UContext.t -> Pp.t val pr_cumulativity_info : (Level.t -> Pp.t) -> CumulativityInfo.t -> Pp.t -val pr_abstract_universe_context : (Level.t -> Pp.t) -> AUContext.t -> Pp.t +val pr_abstract_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array -> + AUContext.t -> Pp.t val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> ACumulativityInfo.t -> Pp.t val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t val explain_universe_inconsistency : (Level.t -> Pp.t) -> diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 1102cdec1..2d8a1d976 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -8,6 +8,7 @@ open Names open Sorts open Cbytecodes +open Univ (*******************************************) (* Initalization of the abstract machine ***) @@ -189,11 +190,11 @@ let rec whd_accu a stk = | i when Int.equal i type_atom_tag -> begin match stk with | [Zapp args] -> - let u = ref (Obj.obj (Obj.field at 0)) in - for i = 0 to nargs args - 1 do - u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i))) - done; - Vsort (Type !u) + let args = Array.init (nargs args) (arg args) in + let u = Obj.obj (Obj.field at 0) in + let inst = Instance.of_array (Array.map uni_lvl_val args) in + let u = Univ.subst_instance_universe inst u in + Vsort (Type u) | _ -> assert false end | i when i <= max_atom_tag -> diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 1e52af0be..e6f1d7e06 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -114,7 +114,7 @@ let process_cmd_line orig_dir proj args = let parsing_project_file = ref (proj.project_file <> None) in let orig_dir = (* avoids turning foo.v in ./foo.v *) if orig_dir = "." then "" else orig_dir in - let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in + let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in let mk_path d = let p = CUnix.correct_path d orig_dir in { path = CUnix.remove_path_dot (post_canonize p); diff --git a/lib/feedback.mli b/lib/feedback.mli index 62b909516..37f38c8ff 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -94,8 +94,9 @@ val msg_warning : ?loc:Loc.t -> Pp.t -> unit consequences. *) val msg_error : ?loc:Loc.t -> Pp.t -> unit -(** Message indicating that something went really wrong, though still - recoverable; otherwise an exception would have been raised. *) +[@@ocaml.deprecated "msg_error is an internal function and should not be \ + used unless you know what you are doing. Use \ + [CErrors.user_err] instead."] val msg_debug : ?loc:Loc.t -> Pp.t -> unit (** For debugging purposes *) diff --git a/library/globnames.ml b/library/globnames.ml index 9d7ab2db8..a6e75fdb6 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -30,7 +30,7 @@ let eq_gr gr1 gr2 = | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2 | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2 | VarRef v1, VarRef v2 -> Id.equal v1 v2 - | _ -> false + | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef" let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" diff --git a/plugins/.dir-locals.el b/plugins/.dir-locals.el deleted file mode 100644 index 4e8830f6c..000000000 --- a/plugins/.dir-locals.el +++ /dev/null @@ -1,4 +0,0 @@ -((coq-mode . ((eval . (let ((default-directory (locate-dominating-file - buffer-file-name ".dir-locals.el"))) - (setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq")) - (setq-local coq-prog-name (expand-file-name "../bin/coqtop"))))))) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 0b929b8ca..f7639d22d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -591,6 +591,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) build_entry_lc env funnames avoid (mkGApp(b,args)) | GRec _ -> user_err Pp.(str "Not handled GRec") + | GProj _ -> user_err Pp.(str "Funind does not support primitive projections") | GProd _ -> user_err Pp.(str "Cannot apply a type") end (* end of the application treatement *) @@ -697,6 +698,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,_) -> build_entry_lc env funnames avoid b + | GProj(_,_) -> user_err Pp.(str "Funind does not support primitive projections") and build_entry_lc_from_case env funname make_discr (el:tomatch_tuples) (brl:Glob_term.cases_clauses) avoid : @@ -1245,7 +1247,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function discrimination ones *) | GSort _ -> params | GHole _ -> params - | GIf _ | GRec _ | GCast _ -> + | GIf _ | GRec _ | GCast _ | GProj _ -> raise (UserError(Some "compute_cst_params", str "Not handled case")) ) gt and compute_cst_params_from_app acc (params,rtl) = diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index be8abb92e..b4ca1073c 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -109,6 +109,7 @@ let change_vars = | GCast(b,c) -> GCast(change_vars mapping b, Miscops.map_cast_type (change_vars mapping) c) + | GProj(p,c) -> GProj(p, change_vars mapping c) ) rt and change_vars_br mapping ((loc,(idl,patl,res)) as br) = let new_mapping = List.fold_right Id.Map.remove idl mapping in @@ -293,6 +294,7 @@ let rec alpha_rt excluded rt = GApp(alpha_rt excluded f, List.map (alpha_rt excluded) args ) + | GProj(p,c) -> GProj(p, alpha_rt excluded c) in new_rt @@ -344,6 +346,7 @@ let is_free_in id = | GHole _ -> false | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t | GCast (b,CastCoerce) -> is_free_in b + | GProj (_,c) -> is_free_in c ) x and is_free_in_br (_,(ids,_,rt)) = (not (Id.List.mem id ids)) && is_free_in rt @@ -437,6 +440,8 @@ let replace_var_by_term x_id term = | GCast(b,c) -> GCast(replace_var_by_pattern b, Miscops.map_cast_type replace_var_by_pattern c) + | GProj(p,c) -> + GProj(p,replace_var_by_pattern c) ) x and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) = if List.exists (fun id -> Id.compare id x_id == 0) idl @@ -540,6 +545,7 @@ let expand_as = | GCases(sty,po,el,brl) -> GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) + | GProj(p,c) -> GProj(p, expand_as map c) ) and expand_as_br map (loc,(idl,cpl,rt)) = (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt)) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 071bab2f3..58154d310 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -215,6 +215,7 @@ let is_rec names = | GCases(_,_,el,brl) -> List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl + | GProj(_,c) -> lookup names c and lookup_br names (_,(idl,_,rt)) = let new_names = List.fold_right Id.Set.remove idl names in lookup new_names rt @@ -779,6 +780,7 @@ let rec add_args id new_args = CAst.map (function | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.") | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.") | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.") + | CProj _ -> user_err Pp.(str "Funind does not support primitive projections") ) exception Stop of Constrexpr.constr_expr diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 23993243f..754e88139 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -581,12 +581,7 @@ and detype_r d flags avoid env sigma t = | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u) | Proj (p,c) -> let noparams () = - let pb = Environ.lookup_projection p (snd env) in - let pars = pb.Declarations.proj_npars in - let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in - let args = List.make pars hole in - GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), - (args @ [detype d flags avoid env sigma c])) + GProj (p, detype d flags avoid env sigma c) in if fst flags || !Flags.in_debugger || !Flags.in_toplevel then try noparams () @@ -1002,6 +997,13 @@ let rec subst_glob_constr subst = DAst.map (function let r1' = subst_glob_constr subst r1 in let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in if r1' == r1 && k' == k then raw else GCast (r1',k') + + | GProj (p,c) as raw -> + let kn = Projection.constant p in + let b = Projection.unfolded p in + let kn' = subst_constant subst kn in + let c' = subst_glob_constr subst c in + if kn' == kn && c' == c then raw else GProj(Projection.make kn' b, c') ) (* Utilities to transform kernel cases to simple pattern-matching problem *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 41c4616f7..dc3acbc3e 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -353,19 +353,7 @@ let exact_ise_stack2 env evd f sk1 sk2 = let check_leq_inductives evd cumi u u' = let u = EConstr.EInstance.kind evd u in let u' = EConstr.EInstance.kind evd u' in - let length_ind_instance = - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) - in - let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in - if not ((length_ind_instance = Univ.Instance.length u) && - (length_ind_instance = Univ.Instance.length u')) then - anomaly (Pp.str "Invalid inductive subtyping encountered!") - else - begin - let comp_subst = (Univ.Instance.append u u') in - let comp_cst = Univ.AUContext.instantiate comp_subst ind_sbcst in - Evd.add_constraints evd comp_cst - end + Evd.add_constraints evd (Reduction.get_cumulativity_constraints CUMUL cumi u u') let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 093f1f0b6..a21137a05 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -133,8 +133,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with Miscops.intro_pattern_naming_eq nam1 nam2 | GCast (c1, t1), GCast (c2, t2) -> f c1 c2 && cast_type_eq f t1 t2 + | GProj (p1, t1), GProj (p2, t2) -> + Projection.equal p1 p2 && f t1 t2 | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | - GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _), _ -> false + GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ | GProj _), _ -> false let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c @@ -180,6 +182,8 @@ let map_glob_constr_left_to_right f = DAst.map (function let comp1 = f c in let comp2 = Miscops.map_cast_type f k in GCast (comp1,comp2) + | GProj (p,c) -> + GProj (p, f c) | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x ) @@ -212,6 +216,8 @@ let fold_glob_constr f acc = DAst.with_val (function let acc = match k with | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in f acc c + | GProj(_,c) -> + f acc c | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc ) @@ -253,6 +259,8 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function let acc = match k with | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in f v acc c + | GProj(_,c) -> + f v acc c | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc)) let iter_glob_constr f = fold_glob_constr (fun () -> f) () diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 78e6bc6f1..275a079d5 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -84,7 +84,7 @@ let mis_is_recursive_subset listind rarg = List.exists (fun ra -> match dest_recarg ra with - | Mrec (_,i) -> Int.List.mem i listind + | Mrec (_,i) -> Int.List.mem i listind | _ -> false) rvec in Array.exists one_is_rec (dest_subterms rarg) @@ -361,20 +361,20 @@ let make_case_or_project env sigma indf ci pred c branches = if (* dependent *) not (Vars.noccurn sigma 1 t) && not (has_dependent_elim mib) then user_err ~hdr:"make_case_or_project" - Pp.(str"Dependent case analysis not allowed" ++ - str" on inductive type " ++ Names.MutInd.print (fst ind)) + Pp.(str"Dependent case analysis not allowed" ++ + str" on inductive type " ++ Names.MutInd.print (fst ind)) in let branch = branches.(0) in let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in let n, subst = List.fold_right (fun decl (i, subst) -> - match decl with - | LocalAssum (na, t) -> - let t = mkProj (Projection.make ps.(i) true, c) in - (i + 1, t :: subst) - | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst)) - ctx (0, []) + match decl with + | LocalAssum (na, t) -> + let t = mkProj (Projection.make ps.(i) true, c) in + (i + 1, t :: subst) + | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst)) + ctx (0, []) in Vars.substl subst br (* substitution in a signature *) @@ -511,25 +511,25 @@ let is_predicate_explicitly_dep env sigma pred arsign = let pv' = whd_all env sigma pval in match EConstr.kind sigma pv', arsign with | Lambda (na,t,b), (LocalAssum _)::arsign -> - srec (push_rel_assum (na, t) env) b arsign + srec (push_rel_assum (na, t) env) b arsign | Lambda (na,_,t), _ -> (* The following code has an impact on the introduction names - given by the tactics "case" and "inversion": when the - elimination is not dependent, "case" uses Anonymous for - inductive types in Prop and names created by mkProd_name for - inductive types in Set/Type while "inversion" uses anonymous - for inductive types both in Prop and Set/Type !! - - Previously, whether names were created or not relied on - whether the predicate created in Indrec.make_case_com had a - dependent arity or not. To avoid different predicates - printed the same in v8, all predicates built in indrec.ml - got a dependent arity (Aug 2004). The new way to decide - whether names have to be created or not is to use an - Anonymous or Named variable to enforce the expected - dependency status (of course, Anonymous implies non - dependent, but not conversely). + given by the tactics "case" and "inversion": when the + elimination is not dependent, "case" uses Anonymous for + inductive types in Prop and names created by mkProd_name for + inductive types in Set/Type while "inversion" uses anonymous + for inductive types both in Prop and Set/Type !! + + Previously, whether names were created or not relied on + whether the predicate created in Indrec.make_case_com had a + dependent arity or not. To avoid different predicates + printed the same in v8, all predicates built in indrec.ml + got a dependent arity (Aug 2004). The new way to decide + whether names have to be created or not is to use an + Anonymous or Named variable to enforce the expected + dependency status (of course, Anonymous implies non + dependent, but not conversely). From Coq > 8.2, using or not the the effective dependency of the predicate is parametrable! *) @@ -600,15 +600,15 @@ let rec instantiate_universes env evdref scl is = function let ctx,_ = Reduction.dest_arity env ty in let u = Univ.Universe.make l in let s = - (* Does the sort of parameter [u] appear in (or equal) + (* Does the sort of parameter [u] appear in (or equal) the sort of inductive [is] ? *) if univ_level_mem l is then scl (* constrained sort: replace by scl *) else (* unconstrained sort: replace by fresh universe *) let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in - let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in - evdref := evm; s + let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in + evdref := evm; s in (LocalAssum (na,mkArity(ctx,s))) :: instantiate_universes env evdref scl is (sign, exp) | sign, [] -> sign (* Uniform parameters are exhausted *) @@ -656,93 +656,3 @@ let control_only_guard env c = iter_constr_with_full_binders push_rel iter env c in iter env c - -(* inference of subtyping condition for inductive types *) - -let infer_inductive_subtyping_arity_constructor - (env, evd, csts) (subst : constr -> constr) (arcn : types) is_arity (params : Context.Rel.t) = - let numchecked = ref 0 in - let numparams = Context.Rel.nhyps params in - let update_contexts (env, evd, csts) csts' = - (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts') - in - let basic_check (env, evd, csts) tp = - let result = - if !numchecked >= numparams then - let csts' = - Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp) - in update_contexts (env, evd, csts) csts' - else - (env, evd, csts) - in - numchecked := !numchecked + 1; result - in - let infer_typ typ ctxs = - match typ with - | LocalAssum (_, typ') -> - begin - try - let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts) - with Reduction.NotConvertible -> - anomaly ~label:"inference of record/inductive subtyping relation failed" - (Pp.str "Can't infer subtyping for record/inductive type") - end - | _ -> anomaly (Pp.str "") - in - let arcn' = Term.it_mkProd_or_LetIn arcn params in - let typs, codom = Reduction.dest_prod env arcn' in - let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in - if not is_arity then basic_check last_contexts codom else last_contexts - -let infer_inductive_subtyping env evd mind_ent = - let { Entries.mind_entry_params = params; - Entries.mind_entry_inds = entries; - Entries.mind_entry_universes = ground_univs; - } = mind_ent - in - let uinfind = - match ground_univs with - | Entries.Monomorphic_ind_entry _ - | Entries.Polymorphic_ind_entry _ -> ground_univs - | Entries.Cumulative_ind_entry cumi -> - begin - let uctx = Univ.CumulativityInfo.univ_context cumi in - let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in - let dosubst = subst_univs_level_constr sbsubst in - let instance_other = - Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) - in - let constraints_other = - Univ.subst_univs_level_constraints - sbsubst (Univ.UContext.constraints uctx) - in - let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env = Environ.push_context uctx env in - let env = Environ.push_context uctx_other env in - let evd = - Evd.merge_universe_context - evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) - in - let (_, _, subtyp_constraints) = - List.fold_left - (fun ctxs indentry -> - let _, params = Typeops.infer_local_decls env params in - let ctxs' = infer_inductive_subtyping_arity_constructor - ctxs dosubst indentry.Entries.mind_entry_arity true params - in - List.fold_left - (fun ctxs cons -> - infer_inductive_subtyping_arity_constructor - ctxs dosubst cons false params - ) - ctxs' indentry.Entries.mind_entry_lc - ) (env, evd, Univ.Constraint.empty) entries - in - Entries.Cumulative_ind_entry - (Univ.CumulativityInfo.make - (Univ.CumulativityInfo.univ_context cumi, - Univ.UContext.make - (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi), - subtyp_constraints))) - end - in {mind_ent with Entries.mind_entry_universes = uinfind;} diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 58b1ce6c3..55149552a 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -199,12 +199,3 @@ val type_of_inductive_knowing_conclusion : (********************) val control_only_guard : env -> types -> unit - -(* inference of subtyping condition for inductive types *) -(* for debugging purposes only to be removed *) -val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t -> -(constr -> constr) -> -types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t - -val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry -> - Entries.mutual_inductive_entry diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml new file mode 100644 index 000000000..a0a8276c5 --- /dev/null +++ b/pretyping/inferCumulativity.ml @@ -0,0 +1,224 @@ +(************************************************************************) +(* 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 Reduction +open Declarations +open Constr +open Univ +open Util + +(** Throughout this module we modify a map [variances] from local + universes to [Variance.t]. It starts as a trivial mapping to + [Irrelevant] and every time we encounter a local universe we + restrict it accordingly. *) + +let infer_level_eq u variances = + if LMap.mem u variances + then LMap.set u Variance.Invariant variances + else variances + +let infer_level_leq u variances = + match LMap.find u variances with + | exception Not_found -> variances + | varu -> LMap.set u (Variance.sup varu Variance.Covariant) variances + +let infer_generic_instance_eq variances u = + Array.fold_left (fun variances u -> infer_level_eq u variances) + variances (Instance.to_array u) + +let variance_pb cv_pb var = + let open Variance in + match cv_pb, var with + | _, Irrelevant -> Irrelevant + | _, Invariant -> Invariant + | CONV, Covariant -> Invariant + | CUMUL, Covariant -> Covariant + +let infer_cumulative_ind_instance cv_pb cumi variances u = + Array.fold_left2 (fun variances varu u -> + match LMap.find u variances with + | exception Not_found -> variances + | varu' -> + LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances) + variances (ACumulativityInfo.variance cumi) (Instance.to_array u) + +let infer_inductive_instance cv_pb env variances ind nargs u = + let mind = Environ.lookup_mind (fst ind) env in + match mind.mind_universes with + | Monomorphic_ind _ -> assert (Instance.is_empty u); variances + | Polymorphic_ind _ -> infer_generic_instance_eq variances u + | Cumulative_ind cumi -> + if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs) + then infer_generic_instance_eq variances u + else infer_cumulative_ind_instance cv_pb cumi variances u + +let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u = + let mind = Environ.lookup_mind mi env in + match mind.mind_universes with + | Monomorphic_ind _ -> assert (Instance.is_empty u); variances + | Polymorphic_ind _ -> infer_generic_instance_eq variances u + | Cumulative_ind cumi -> + if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs) + then infer_generic_instance_eq variances u + else infer_cumulative_ind_instance CONV cumi variances u + +let infer_sort cv_pb variances s = + match cv_pb with + | CONV -> + LSet.fold infer_level_eq (Universe.levels (Sorts.univ_of_sort s)) variances + | CUMUL -> + LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances + +let infer_table_key infos variances c = + let open Names in + match c with + | ConstKey (_, u) -> + infer_generic_instance_eq variances u + | VarKey _ | RelKey _ -> variances + +let rec infer_fterm cv_pb infos variances hd stk = + Control.check_for_interrupt (); + let open CClosure in + let hd,stk = whd_stack infos hd stk in + match fterm_of hd with + | FAtom a -> + begin match kind a with + | Sort s -> infer_sort cv_pb variances s + | Meta _ -> infer_stack infos variances stk + | _ -> assert false + end + | FEvar ((_,args),e) -> + let variances = infer_stack infos variances stk in + infer_vect infos variances (Array.map (mk_clos e) args) + | FRel _ -> variances + | FFlex fl -> + let variances = infer_table_key infos variances fl in + infer_stack infos variances stk + | FProj (_,c) -> + let variances = infer_fterm CONV infos variances c [] in + infer_stack infos variances stk + | FLambda _ -> + let (_,ty,bd) = destFLambda mk_clos hd in + let variances = infer_fterm CONV infos variances ty [] in + infer_fterm CONV infos variances bd [] + | FProd (_,dom,codom) -> + let variances = infer_fterm CONV infos variances dom [] in + infer_fterm cv_pb infos variances codom [] + | FInd (ind, u) -> + let variances = + if Instance.is_empty u then variances + else + let nargs = stack_args_size stk in + infer_inductive_instance cv_pb (info_env infos) variances ind nargs u + in + infer_stack infos variances stk + | FConstruct (ctor,u) -> + let variances = + if Instance.is_empty u then variances + else + let nargs = stack_args_size stk in + infer_constructor_instance_eq (info_env infos) variances ctor nargs u + in + infer_stack infos variances stk + | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) -> + let n = Array.length cl in + let variances = infer_vect infos variances (Array.map (mk_clos e) tys) in + let le = Esubst.subs_liftn n e in + let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in + infer_stack infos variances stk + + (* Removed by whnf *) + | FLOCKED | FCaseT _ | FCast _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false + +and infer_stack infos variances (stk:CClosure.stack) = + match stk with + | [] -> variances + | z :: stk -> + let open CClosure in + let variances = match z with + | Zapp v -> infer_vect infos variances v + | Zproj _ -> variances + | Zfix (fx,a) -> + let variances = infer_fterm CONV infos variances fx [] in + infer_stack infos variances a + | ZcaseT (ci,p,br,e) -> + let variances = infer_fterm CONV infos variances (mk_clos e p) [] in + infer_vect infos variances (Array.map (mk_clos e) br) + | Zshift _ -> variances + | Zupdate _ -> variances + in + infer_stack infos variances stk + +and infer_vect infos variances v = + Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v + +let infer_term cv_pb env variances c = + let open CClosure in + let reds = RedFlags.red_add_transparent betaiotazeta Names.full_transparent_state in + let infos = create_clos_infos reds env in + infer_fterm cv_pb infos variances (CClosure.inject c) [] + +let infer_arity_constructor env variances arcn is_arity params = + let numchecked = ref 0 in + let numparams = Context.Rel.nhyps params in + let basic_check env variances tp = + let variances = + if !numchecked >= numparams then + infer_term CUMUL env variances tp + else + variances + in + numchecked := !numchecked + 1; variances + in + let infer_typ typ (env,variances) = + match typ with + | Context.Rel.Declaration.LocalAssum (_, typ') -> + (Environ.push_rel typ env, basic_check env variances typ') + | Context.Rel.Declaration.LocalDef _ -> assert false + in + let arcn' = Term.it_mkProd_or_LetIn arcn params in + let typs, codom = Reduction.dest_prod env arcn' in + let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in + (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j} + i is irrelevant, j is invariant. *) + if not is_arity then basic_check env variances codom else variances + +let infer_inductive env mie = + let open Entries in + let { mind_entry_params = params; + mind_entry_inds = entries; } = mie + in + let univs = + match mie.mind_entry_universes with + | Monomorphic_ind_entry _ + | Polymorphic_ind_entry _ as univs -> univs + | Cumulative_ind_entry cumi -> + let uctx = CumulativityInfo.univ_context cumi in + let uarray = Instance.to_array @@ UContext.instance uctx in + let env = Environ.push_context uctx env in + let variances = + Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances) + LMap.empty uarray + in + let variances = List.fold_left (fun variances entry -> + let _, params = Typeops.infer_local_decls env params in + let variances = infer_arity_constructor + env variances entry.mind_entry_arity true params + in + List.fold_left + (fun variances cons -> + infer_arity_constructor + env variances cons false params) + variances entry.mind_entry_lc) + variances + entries + in + let variances = Array.map (fun u -> LMap.find u variances) uarray in + Cumulative_ind_entry (CumulativityInfo.make (uctx, variances)) + in + { mie with mind_entry_universes = univs } diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli new file mode 100644 index 000000000..a5037ea47 --- /dev/null +++ b/pretyping/inferCumulativity.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> + Entries.mutual_inductive_entry diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 41e09004c..1bec4a6f1 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -137,8 +137,7 @@ let rec head_pattern_bound t = | PCase (_,p,c,br) -> head_pattern_bound c | PRef r -> r | PVar id -> VarRef id - | PProj (p,c) -> ConstRef (Projection.constant p) - | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ + | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ | PProj _ -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) | PLambda _ -> raise BoundPattern @@ -446,6 +445,9 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function one non-trivial branch. These facts are used in [Constrextern]. *) PCase (info, pred, pat_of_raw metas vars c, brs) + | GProj(p,c) -> + PProj(p, pat_of_raw metas vars c) + | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ -> err ?loc (Pp.str "Non supported pattern.")) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 92dab24e2..8809558ff 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -737,6 +737,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j = pretype_sort ?loc evdref s in inh_conv_coerce_to_tycon ?loc env evdref j tycon + | GProj (p, c) -> + (* TODO: once GProj is used as an input syntax, use bidirectional typing here *) + let cj = pretype empty_tycon env evdref lvar c in + judge_of_projection env.ExtraEnv.env !evdref p cj + | GApp (f,args) -> let fj = pretype empty_tycon env evdref lvar f in let floc = loc_of_glob_constr f in diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 1da5b4567..ae4ad0be7 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -4,6 +4,7 @@ Locusops Pretype_errors Reductionops Inductiveops +InferCumulativity Vnorm Arguments_renaming Nativenorm diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 9ff9a75b3..ab1f3cd32 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -298,29 +298,40 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) (*s High-level declaration of a canonical structure *) -let error_not_structure ref = +let error_not_structure ref description = user_err ~hdr:"object_declare" - (Id.print (basename_of_global ref) ++ str" is not a structure object.") + (str"Could not declare a canonical structure " ++ + (Id.print (basename_of_global ref) ++ str"." ++ spc() ++ + str(description))) let check_and_decompose_canonical_structure ref = - let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in + let sp = + match ref with + ConstRef sp -> sp + | _ -> error_not_structure ref "Expected an instance of a record or structure." + in let env = Global.env () in let u = Univ.make_abstract_instance (Environ.constant_context env sp) in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc - | None -> error_not_structure ref in + | None -> error_not_structure ref "Could not find its value in the global environment." in let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in let body = EConstr.Unsafe.to_constr body in let f,args = match kind body with | App (f,args) -> f,args - | _ -> error_not_structure ref in + | _ -> + error_not_structure ref "Expected a record or structure constructor applied to arguments." in let indsp = match kind f with | Construct ((indsp,1),u) -> indsp - | _ -> error_not_structure ref in - let s = try lookup_structure indsp with Not_found -> error_not_structure ref in + | _ -> error_not_structure ref "Expected an instance of a record or structure." in + let s = + try lookup_structure indsp + with Not_found -> + error_not_structure ref + ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then - error_not_structure ref; + error_not_structure ref "Got too few arguments to the record or structure constructor."; (sp,indsp) let declare_canonical_structure ref = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 1893018a9..418ea271c 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1324,79 +1324,17 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible -let sigma_check_inductive_instances cv_pb uinfind u u' sigma = - let len_instance = - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind) - in - let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in - if not ((len_instance = Univ.Instance.length u) && - (len_instance = Univ.Instance.length u')) then - anomaly (Pp.str "Invalid inductive subtyping encountered!") - else - let comp_cst = - let comp_subst = (Univ.Instance.append u u') in - Univ.AUContext.instantiate comp_subst ind_sbctx - in - let comp_cst = - match cv_pb with - Reduction.CONV -> - let comp_subst = (Univ.Instance.append u' u) in - let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in - Univ.Constraint.union comp_cst comp_cst' - | Reduction.CUMUL -> comp_cst - in - try Evd.add_constraints sigma comp_cst - with Evd.UniversesDiffer - | Univ.UniverseInconsistency _ -> - raise Reduction.NotConvertible - -let sigma_conv_inductives - cv_pb (mind, ind) u1 sv1 u2 sv2 sigma = - try sigma_compare_instances ~flex:false u1 u2 sigma with - Reduction.NotConvertible -> - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Polymorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Cumulative_ind cumi -> - let num_param_arity = - mind.Declarations.mind_nparams + - mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - in - if not (num_param_arity = sv1 && num_param_arity = sv2) then - raise Reduction.NotConvertible - else - sigma_check_inductive_instances cv_pb cumi u1 u2 sigma - -let sigma_conv_constructors - (mind, ind, cns) u1 sv1 u2 sv2 sigma = - try sigma_compare_instances ~flex:false u1 u2 sigma with - Reduction.NotConvertible -> - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Polymorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Cumulative_ind cumi -> - let num_cnstr_args = - let nparamsctxt = - mind.Declarations.mind_nparams + - mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - in - nparamsctxt + - mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) - in - if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then - raise Reduction.NotConvertible - else - sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma +let sigma_check_inductive_instances csts sigma = + try Evd.add_constraints sigma csts + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible let sigma_univ_state = - { Reduction.compare = sigma_compare_sorts; - Reduction.compare_instances = sigma_compare_instances; - Reduction.conv_inductives = sigma_conv_inductives; - Reduction.conv_constructors = sigma_conv_constructors} + let open Reduction in + { compare_sorts = sigma_compare_sorts; + compare_instances = sigma_compare_instances; + compare_cumul_instances = sigma_check_inductive_instances; } let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 9f084ae8d..153a48a71 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -53,3 +53,4 @@ val judge_of_abstraction : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment val judge_of_product : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment +val judge_of_projection : env -> evar_map -> projection -> unsafe_judgment -> unsafe_judgment diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b21fbf0eb..c93b41786 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -240,8 +240,9 @@ and nf_stk ?from:(from=0) env sigma c t stk = let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in let params,realargs = Util.Array.chop nparams allargs in + let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = - hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in + hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in let pT = whd_all env pT in let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 51735bc9e..1146b42a0 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -732,6 +732,9 @@ let tag_var = tag Tag.variable return (pr_prim_token p, prec_of_prim_token p) | CDelimiters (sc,a) -> return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim) + | CProj (p,c) -> + let p = pr_proj (pr mt) pr_app c (CAst.make (CRef (p,None))) [] in + return (p, lproj) in let loc = constr_loc a in pr_with_comments ?loc diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 2b7886d11..114a071ee 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -78,6 +78,15 @@ let print_ref reduce ref udecl = in EConstr.it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in + let variance = match ref with + | VarRef _ | ConstRef _ -> None + | IndRef (ind,_) | ConstructRef ((ind,_),_) -> + let mind = Environ.lookup_mind ind (Global.env ()) in + begin match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None + | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi) + end + in let inst = Univ.AUContext.instance univs in let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in let env = Global.env () in @@ -89,7 +98,7 @@ let print_ref reduce ref udecl = else mt () in hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ - Printer.pr_universe_ctx sigma univs) + Printer.pr_universe_ctx sigma ?variance univs) (********************************) (** Printing implicit arguments *) diff --git a/printing/printer.ml b/printing/printer.ml index a63004ceb..d720bc2f8 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -263,10 +263,10 @@ let pr_universe_ctx_set sigma c = else mt() -let pr_universe_ctx sigma c = +let pr_universe_ctx sigma ?variance c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then fnl()++pr_in_comment (fun c -> v 0 - (Univ.pr_universe_context (Termops.pr_evd_level sigma) c)) c + (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c)) c else mt() diff --git a/printing/printer.mli b/printing/printer.mli index 804014745..a3427920a 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -120,7 +120,8 @@ val pr_sort : evar_map -> Sorts.t -> Pp.t val pr_polymorphic : bool -> Pp.t val pr_cumulative : bool -> bool -> Pp.t val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t -val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t +val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> + Univ.UContext.t -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t val pr_constant_universes : evar_map -> Entries.constant_universes_entry -> Pp.t val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t diff --git a/printing/printmod.ml b/printing/printmod.ml index fb9d45a79..2cdb9be3f 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -93,10 +93,11 @@ let print_one_inductive env sigma mib ((_,i) as ind) = else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in + let nparamdecls = Context.Rel.length params in let args = Context.Rel.to_extended_list mkRel 0 params in - let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in + let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in - let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in + let cstrtypes = Array.map (fun c -> hnf_prod_applist_assum env nparamdecls c args) cstrtypes in let envpar = push_rel_context params env in let inst = if Declareops.inductive_is_polymorphic mib then @@ -113,13 +114,12 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let instantiate_cumulativity_info cumi = let open Univ in let univs = ACumulativityInfo.univ_context cumi in - let subtyp = ACumulativityInfo.subtyp_context cumi in let expose ctx = let inst = AUContext.instance ctx in let cst = AUContext.instantiate inst ctx in UContext.make (inst, cst) in - CumulativityInfo.make (expose univs, expose subtyp) + CumulativityInfo.make (expose univs, ACumulativityInfo.variance cumi) let print_mutual_inductive env mind mib udecl = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) @@ -174,10 +174,11 @@ let print_record env mind mib udecl = in let mip = mib.mind_packets.(0) in let params = Inductive.inductive_paramdecls (mib,u) in + let nparamdecls = Context.Rel.length params in let args = Context.Rel.to_extended_list mkRel 0 params in - let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in + let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in - let cstrtype = hnf_prod_applist env cstrtypes.(0) args in + let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0)) diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml index 10b42f7e9..def60d1b9 100644 --- a/stm/proofworkertop.ml +++ b/stm/proofworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ()) diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml index a1fe50c63..928a6bfb0 100644 --- a/stm/queryworkertop.ml +++ b/stm/queryworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ()) diff --git a/stm/stm.ml b/stm/stm.ml index b5848c662..6c956e134 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -85,8 +85,7 @@ let stm_purify f x = Exninfo.iraise e let execution_error ?loc state_id msg = - feedback ~id:state_id - (Message (Error, loc, msg)) + feedback ~id:state_id (Message (Error, loc, msg)) module Hooks = struct @@ -1579,12 +1578,13 @@ end = struct (* {{{ *) | ReqStates sl -> RespStates (perform_states sl) let on_marshal_error s = function - | States _ -> msg_error(Pp.strbrk("Marshalling error: "^s^". "^ - "The system state could not be sent to the master process.")) + | States _ -> + msg_warning Pp.(strbrk("Marshalling error: "^s^". "^ + "The system state could not be sent to the master process.")) | BuildProof { t_exn_info; t_stop; t_assign; t_loc; t_drop = drop_pt } -> - msg_error(Pp.strbrk("Marshalling error: "^s^". "^ - "The system state could not be sent to the worker process. "^ - "Falling back to local, lazy, evaluation.")); + msg_warning Pp.(strbrk("Marshalling error: "^s^". "^ + "The system state could not be sent to the worker process. "^ + "Falling back to local, lazy, evaluation.")); t_assign(`Comp(build_proof_here ?loc:t_loc ~drop_pt t_exn_info t_stop)); feedback (InProgress ~-1) @@ -1672,7 +1672,7 @@ end = struct (* {{{ *) let (e, info) = CErrors.push e in (try match Stateid.get info with | None -> - msg_error Pp.( + msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ spc () ++ iprint (e, info)) | Some (_, cur) -> @@ -1682,17 +1682,17 @@ end = struct (* {{{ *) | { step = `Qed ( { qast = { loc } }, _) } | { step = `Sideff (ReplayCommand { loc }, _) } -> let start, stop = Option.cata Loc.unloc (0,0) loc in - msg_error Pp.( + msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ str ": chars " ++ int start ++ str "-" ++ int stop ++ spc () ++ iprint (e, info)) | _ -> - msg_error Pp.( + msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ spc () ++ iprint (e, info)) with e -> - msg_error Pp.(str"unable to print error message: " ++ - str (Printexc.to_string e))); + msg_warning Pp.(str"unable to print error message: " ++ + str (Printexc.to_string e))); if drop then `ERROR_ADMITTED else `ERROR let finish_task name (u,cst,_) d p l i = @@ -2429,7 +2429,7 @@ let known_state ?(redefine_qed=false) ~cache id = | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> assert(redefine_qed = true); if okeep != keep then - msg_error(strbrk("The command closing the proof changed. " + msg_warning(strbrk("The command closing the proof changed. " ^"The kernel cannot take this into account and will " ^(if keep == VtKeep then "not check " else "reject ") ^"the "^(if keep == VtKeep then "new" else "incomplete") @@ -2702,7 +2702,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) = (u,a,true), p with e -> let e = CErrors.push e in - msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); + msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 let merge_proof_branch ~valid ?id qast keep brname = diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml index 17f90b7b1..f202fc7c5 100644 --- a/stm/tacworkertop.ml +++ b/stm/tacworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ()) diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml index 704119186..d606f19bf 100644 --- a/stm/workerLoop.ml +++ b/stm/workerLoop.ml @@ -15,8 +15,8 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let loop init args = - let args = parse args in +let loop init _coq_args extra_args = + let args = parse extra_args in Flags.quiet := true; init (); CoqworkmgrApi.init !async_proofs_worker_priority; diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli index da2e6fe0c..c42b48a28 100644 --- a/stm/workerLoop.mli +++ b/stm/workerLoop.mli @@ -9,4 +9,4 @@ (* Default priority *) val async_proofs_worker_priority : CoqworkmgrApi.priority ref -val loop : (unit -> unit) -> string list -> string list +val loop : (unit -> unit) -> Coqargs.coq_cmdopts -> string list -> string list diff --git a/test-suite/bugs/closed/5726.v b/test-suite/bugs/closed/5726.v new file mode 100644 index 000000000..53ef47357 --- /dev/null +++ b/test-suite/bugs/closed/5726.v @@ -0,0 +1,34 @@ +Set Universe Polymorphism. +Set Printing Universes. + +Module GlobalReference. + + Definition type' := Type. + Notation type := type'. + Check type@{Set}. + +End GlobalReference. + +Module TypeLiteral. + + Notation type := Type. + Check type@{Set}. + Check type@{Prop}. + +End TypeLiteral. + +Module ExplicitSort. + Monomorphic Universe u. + Notation foo := Type@{u}. + Fail Check foo@{Set}. + Fail Check foo@{u}. + + Notation bar := Type. + Check bar@{u}. +End ExplicitSort. + +Module PropNotationUnsupported. + Notation foo := Prop. + Fail Check foo@{Set}. + Fail Check foo@{Type}. +End PropNotationUnsupported. diff --git a/test-suite/bugs/closed/6677.v b/test-suite/bugs/closed/6677.v new file mode 100644 index 000000000..99e47bb87 --- /dev/null +++ b/test-suite/bugs/closed/6677.v @@ -0,0 +1,5 @@ +Set Universe Polymorphism. + +Definition T@{i} := Type@{i}. +Fail Definition U@{i} := (T@{i} <: Type@{i}). +Fail Definition eqU@{i j} : @eq T@{j} U@{i} T@{i} := eq_refl. diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject b/test-suite/coq-makefile/emptyprefix/_CoqProject new file mode 100644 index 000000000..5678a8edb --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject @@ -0,0 +1,11 @@ +-R theories "" +-R src "" +-I src +-arg "-w default" + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject.sub b/test-suite/coq-makefile/emptyprefix/_CoqProject.sub new file mode 100644 index 000000000..90ac541e0 --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject.sub @@ -0,0 +1,3 @@ +-R ../theories "" +-I ../src +testsub.v diff --git a/test-suite/coq-makefile/emptyprefix/run.sh b/test-suite/coq-makefile/emptyprefix/run.sh new file mode 100755 index 000000000..a10e63b42 --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/run.sh @@ -0,0 +1,17 @@ +#!/usr/bin/env bash + +set -e + +. ../template/init.sh + +mv theories/sub theories2 + +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +make + +cp ../_CoqProject.sub theories2/_CoqProject +cd theories2 +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +make diff --git a/test-suite/coq-makefile/quick2vo/_CoqProject b/test-suite/coq-makefile/quick2vo/_CoqProject new file mode 100644 index 000000000..69f47302e --- /dev/null +++ b/test-suite/coq-makefile/quick2vo/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/quick2vo/run.sh b/test-suite/coq-makefile/quick2vo/run.sh new file mode 100755 index 000000000..9e681223b --- /dev/null +++ b/test-suite/coq-makefile/quick2vo/run.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash +a=`uname` + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +# vio2vo is broken on Windows (#6720) +if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then + make quick2vo J=2 + test -f theories/test.vo + make validate +fi diff --git a/test-suite/coq-makefile/vio2vo/_CoqProject b/test-suite/coq-makefile/vio2vo/_CoqProject new file mode 100644 index 000000000..69f47302e --- /dev/null +++ b/test-suite/coq-makefile/vio2vo/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/vio2vo/run.sh b/test-suite/coq-makefile/vio2vo/run.sh new file mode 100755 index 000000000..85656da41 --- /dev/null +++ b/test-suite/coq-makefile/vio2vo/run.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash +a=`uname` + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make quick +# vio2vo is broken on Windows (#6720) +if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then + make vio2vo J=2 + test -f theories/test.vo + make validate +fi diff --git a/test-suite/output/ErrorInCanonicalStructures.out b/test-suite/output/ErrorInCanonicalStructures.out new file mode 100644 index 000000000..73da4f44f --- /dev/null +++ b/test-suite/output/ErrorInCanonicalStructures.out @@ -0,0 +1,5 @@ +File "stdin", line 3, characters 0-24: +Error: +Could not declare a canonical structure Foo. +Expected an instance of a record or structure. + diff --git a/test-suite/output/ErrorInCanonicalStructures.v b/test-suite/output/ErrorInCanonicalStructures.v new file mode 100644 index 000000000..49597df6f --- /dev/null +++ b/test-suite/output/ErrorInCanonicalStructures.v @@ -0,0 +1,3 @@ +Record Foo := MkFoo { field1 : nat; field2 : nat -> nat }. + +Canonical Structure Foo. diff --git a/test-suite/output/ErrorInCanonicalStructures2.out b/test-suite/output/ErrorInCanonicalStructures2.out new file mode 100644 index 000000000..63a2871b8 --- /dev/null +++ b/test-suite/output/ErrorInCanonicalStructures2.out @@ -0,0 +1,5 @@ +File "stdin", line 3, characters 0-24: +Error: +Could not declare a canonical structure bar. +Expected an instance of a record or structure. + diff --git a/test-suite/output/ErrorInCanonicalStructures2.v b/test-suite/output/ErrorInCanonicalStructures2.v new file mode 100644 index 000000000..10ee177aa --- /dev/null +++ b/test-suite/output/ErrorInCanonicalStructures2.v @@ -0,0 +1,3 @@ +Definition bar := 99. + +Canonical Structure bar. diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index e912003f0..af202ea01 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,3 +1,7 @@ The command has indeed failed with message: Last occurrence of "list'" must have "A" as 1st argument in "A -> list' A -> list' (A * A)%type". +Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x + +For foo: Argument scopes are [type_scope _] +For Foo: Argument scopes are [type_scope _] diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v index 8db8956e3..8ff91268a 100644 --- a/test-suite/output/Inductive.v +++ b/test-suite/output/Inductive.v @@ -1,3 +1,7 @@ Fail Inductive list' (A:Set) : Set := | nil' : list' A | cons' : A -> list' A -> list' (A*A). + +(* Check printing of let-ins *) +Inductive foo (A : Type) (x : A) (y := x) := Foo. +Print foo. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index d6d410d1a..668b4e578 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -5,7 +5,7 @@ PWrap has primitive projections with eta conversion. For PWrap: Argument scope is [type_scope] For pwrap: Argument scopes are [type_scope _] punwrap@{u} = -fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p +fun (A : Type@{u}) (p : PWrap@{u} A) => p.(punwrap) : forall A : Type@{u}, PWrap@{u} A -> A (* u |= *) diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 0ee85712e..1fb3abfe4 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -45,6 +45,15 @@ Section TpLift. End TpLift. +Record Tp' := { tp' : Tp }. + +Definition CTp := Tp. +(* here we have to reduce a constant to infer the correct subtyping. *) +Record Tp'' := { tp'' : CTp }. + +Definition LiftTp'@{i j|i < j} : Tp'@{i} -> Tp'@{j} := fun x => x. +Definition LiftTp''@{i j|i < j} : Tp''@{i} -> Tp''@{j} := fun x => x. + Lemma LiftC_Lem (t : Tp) : LiftTp t = t. Proof. reflexivity. Qed. @@ -98,3 +107,20 @@ Section down. intros H f g Hfg. exact (H f g Hfg). Defined. End down. + +Record Arrow@{i j} := { arrow : Type@{i} -> Type@{j} }. + +Fail Definition arrow_lift@{i i' j j' | i' < i, j < j'} + : Arrow@{i j} -> Arrow@{i' j'} + := fun x => x. + +Definition arrow_lift@{i i' j j' | i' = i, j < j'} + : Arrow@{i j} -> Arrow@{i' j'} + := fun x => x. + +Inductive Mut1 A := +| Base1 : Type -> Mut1 A +| Node1 : (A -> Mut2 A) -> Mut1 A +with Mut2 A := + | Base2 : Type -> Mut2 A + | Node2 : Mut1 A -> Mut2 A. diff --git a/theories/.dir-locals.el b/theories/.dir-locals.el deleted file mode 100644 index 4e8830f6c..000000000 --- a/theories/.dir-locals.el +++ /dev/null @@ -1,4 +0,0 @@ -((coq-mode . ((eval . (let ((default-directory (locate-dominating-file - buffer-file-name ".dir-locals.el"))) - (setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq")) - (setq-local coq-prog-name (expand-file-name "../bin/coqtop"))))))) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index fbf992dbf..eae2c52de 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -2110,13 +2110,13 @@ Section Exists_Forall. {Exists l} + {~ Exists l}. Proof. intro Pdec. induction l as [|a l' Hrec]. - - right. now rewrite Exists_nil. + - right. abstract now rewrite Exists_nil. - destruct Hrec as [Hl'|Hl']. * left. now apply Exists_cons_tl. * destruct (Pdec a) as [Ha|Ha]. + left. now apply Exists_cons_hd. - + right. now inversion_clear 1. - Qed. + + right. abstract now inversion 1. + Defined. Inductive Forall : list A -> Prop := | Forall_nil : Forall nil @@ -2152,9 +2152,9 @@ Section Exists_Forall. - destruct Hrec as [Hl'|Hl']. + destruct (Pdec a) as [Ha|Ha]. * left. now apply Forall_cons. - * right. now inversion_clear 1. - + right. now inversion_clear 1. - Qed. + * right. abstract now inversion 1. + + right. abstract now inversion 1. + Defined. End One_predicate. @@ -2179,6 +2179,16 @@ Section Exists_Forall. * now apply Exists_cons_hd. Qed. + Lemma neg_Forall_Exists_neg (P:A->Prop) (l:list A) : + (forall x:A, {P x} + { ~ P x }) -> + ~ Forall P l -> + Exists (fun x => ~ P x) l. + Proof. + intro Dec. + apply Exists_Forall_neg; intros. + destruct (Dec x); auto. + Qed. + Lemma Forall_Exists_dec (P:A->Prop) : (forall x:A, {P x} + { ~ P x }) -> forall l:list A, @@ -2186,9 +2196,8 @@ Section Exists_Forall. Proof. intros Pdec l. destruct (Forall_dec P Pdec l); [left|right]; trivial. - apply Exists_Forall_neg; trivial. - intro x. destruct (Pdec x); [now left|now right]. - Qed. + now apply neg_Forall_Exists_neg. + Defined. Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) -> forall l, Forall P l -> Forall Q l. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 88596eb3f..727fd3ec3 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -168,7 +168,8 @@ endif COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) COQCHKFLAGS?=-silent -o $(COQLIBS) -COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML) +COQDOCFLAGS?=-interpolate -utf8 +COQDOCLIBS?=$(COQLIBS_NOML) # The version of Coq being run and the version of coq_makefile that # generated this makefile @@ -376,7 +377,7 @@ bytefiles: $(CMOFILES) $(CMAFILES) optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) .PHONY: optfiles -# FIXME, see Ralph's bugreport +# FIXME, see Ralf's bugreport quick: $(VOFILES:.vo=.vio) .PHONY: quick @@ -385,6 +386,18 @@ vio2vo: -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) .PHONY: vio2vo +quick2vo: + $(HIDE)make -j $(J) quick + $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ + viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ + if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ + done); \ + echo "VIO2VO: $$VIOFILES"; \ + if [ -n "$$VIOFILES" ]; then \ + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; \ + fi +.PHONY: quick2vo + checkproofs: $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 091869407..1e1862220 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -124,7 +124,7 @@ let read_whole_file s = close_in ic; Buffer.contents b -let quote s = if String.contains s ' ' then "'" ^ s ^ "'" else s +let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" else s let generate_makefile oc conf_file local_file args project = let makefile_template = diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 2433cb1d0..ca14b11bc 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -539,4 +539,4 @@ let _ = coqdep () with CErrors.UserError(s,p) -> let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p)) in - Feedback.msg_error pp + Format.eprintf "%a@\n%!" Pp.pp_with pp diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml new file mode 100644 index 000000000..5b73471c5 --- /dev/null +++ b/toplevel/coqargs.ml @@ -0,0 +1,575 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +let warning s = Flags.(with_option warn Feedback.msg_warning (Pp.strbrk s)) + +let fatal_error ?extra exn = + Topfmt.print_err_exn ?extra exn; + let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in + exit exit_code + +let error_missing_arg s = + prerr_endline ("Error: extra argument expected after option "^s); + prerr_endline "See -help for the syntax of supported options"; + exit 1 + +(******************************************************************************) +(* Imperative effects! This must be fixed at some point. *) +(******************************************************************************) +let set_worker_id opt s = + assert (s <> "master"); + Flags.async_proofs_worker_id := s + +let set_type_in_type () = + let typing_flags = Environ.typing_flags (Global.env ()) in + Global.set_typing_flags { typing_flags with Declarations.check_universes = false } + +(******************************************************************************) + +type compilation_mode = BuildVo | BuildVio | Vio2Vo +type color = [`ON | `AUTO | `OFF] + +type coq_cmdopts = { + + load_init : bool; + load_rcfile : bool; + rcfile : string option; + + ml_includes : string list; + vo_includes : (string * Names.DirPath.t * bool) list; + vo_requires : (string * string option * bool option) list; + (* None = No Import; Some false = Import; Some true = Export *) + + (* XXX: Fusion? *) + batch_mode : bool; + compilation_mode : compilation_mode; + + toplevel_name : Names.DirPath.t; + toploop : string option; + + compile_list: (string * bool) list; (* bool is verbosity *) + compilation_output_name : string option; + + load_vernacular_list : (string * bool) list; + + vio_checking: bool; + vio_tasks : (int list * string) list; + vio_files : string list; + vio_files_j : int; + + color : color; + + impredicative_set : Declarations.set_predicativity; + stm_flags : Stm.AsyncOpts.stm_opt; + debug : bool; + time : bool; + + filter_opts : bool; + + glob_opt : bool; + + memory_stat : bool; + print_tags : bool; + print_where : bool; + print_config: bool; + output_context : bool; + + inputstate : string option; + outputstate : string option; + +} + +let init_args = { + + load_init = true; + load_rcfile = true; + rcfile = None; + + ml_includes = []; + vo_includes = []; + vo_requires = []; + + batch_mode = false; + compilation_mode = BuildVo; + + toplevel_name = Names.(DirPath.make [Id.of_string "Top"]); + toploop = None; + + compile_list = []; + compilation_output_name = None; + + load_vernacular_list = []; + + vio_checking = false; + vio_tasks = []; + vio_files = []; + vio_files_j = 0; + + color = `AUTO; + + impredicative_set = Declarations.PredicativeSet; + stm_flags = Stm.AsyncOpts.default_opts; + debug = false; + time = false; + + filter_opts = false; + + glob_opt = false; + + memory_stat = false; + print_tags = false; + print_where = false; + print_config = false; + output_context = false; + + inputstate = None; + outputstate = None; +} + +(******************************************************************************) +(* Functional arguments *) +(******************************************************************************) +let add_ml_include opts s = + { opts with ml_includes = s :: opts.ml_includes } + +let add_vo_include opts d p implicit = + let p = Libnames.dirpath_of_string p in + { opts with vo_includes = (d, p, implicit) :: opts.vo_includes } + +let add_vo_require opts d p export = + { opts with vo_requires = (d, p, export) :: opts.vo_requires } + +let add_compat_require opts v = + match v with + | Flags.V8_5 -> add_vo_require opts "Coq.Compat.Coq85" None (Some false) + | Flags.V8_6 -> add_vo_require opts "Coq.Compat.Coq86" None (Some false) + | Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false) + | Flags.VOld | Flags.Current -> opts + +let set_batch_mode opts = + Flags.quiet := true; + System.trust_file_cache := false; + { opts with batch_mode = true } + +let add_compile opts verbose s = + let opts = set_batch_mode opts in + if not opts.glob_opt then Dumpglob.dump_to_dotglob (); + (** make the file name explicit; needed not to break up Coq loadpath stuff. *) + let s = + let open Filename in + if is_implicit s + then concat current_dir_name s + else s + in + { opts with compile_list = (s,verbose) :: opts.compile_list } + +let add_load_vernacular opts verb s = + { opts with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.load_vernacular_list } + +let add_vio_task opts f = + let opts = set_batch_mode opts in + { opts with vio_tasks = f :: opts.vio_tasks } + +let add_vio_file opts f = + let opts = set_batch_mode opts in + { opts with vio_files = f :: opts.vio_files } + +let set_vio_checking_j opts opt j = + try { opts with vio_files_j = int_of_string j } + with Failure _ -> + prerr_endline ("The first argument of " ^ opt ^ " must the number"); + prerr_endline "of concurrent workers to be used (a positive integer)."; + prerr_endline "Makefiles generated by coq_makefile should be called"; + prerr_endline "setting the J variable like in 'make vio2vo J=3'"; + exit 1 + +(** Options for proof general *) +let set_emacs opts = + if not (Option.is_empty opts.toploop) then + CErrors.user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop"); + Coqloop.print_emacs := true; + Printer.enable_goal_tags_printing := true; + { opts with color = `OFF } + +let set_color opts = function +| "yes" | "on" -> { opts with color = `ON } +| "no" | "off" -> { opts with color = `OFF } +| "auto" -> { opts with color = `AUTO } +| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1 + +let warn_deprecated_inputstate = + CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" + (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") + +let set_inputstate opts s = + warn_deprecated_inputstate (); + { opts with inputstate = Some s } + +let warn_deprecated_outputstate = + CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated" + (fun () -> + Pp.strbrk "The outputstate option is deprecated and discouraged.") + +let set_outputstate opts s = + warn_deprecated_outputstate (); + { opts with outputstate = Some s } + +let exitcode opts = if opts.filter_opts then 2 else 0 + +(******************************************************************************) +(* Parsing helpers *) +(******************************************************************************) +let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) + +let get_bool opt = function + | "yes" | "on" -> true + | "no" | "off" -> false + | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1 + +let get_int opt n = + try int_of_string n + with Failure _ -> + prerr_endline ("Error: integer expected after option "^opt); exit 1 + +let get_float opt n = + try float_of_string n + with Failure _ -> + prerr_endline ("Error: float expected after option "^opt); exit 1 + +let get_host_port opt s = + match CString.split ':' s with + | [host; portr; portw] -> + Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) + | ["stdfds"] -> Some Spawned.AnonPipe + | _ -> + prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt); + exit 1 + +let get_error_resilience opt = function + | "on" | "all" | "yes" -> `All + | "off" | "no" -> `None + | s -> `Only (CString.split ',' s) + +let get_priority opt s = + try CoqworkmgrApi.priority_of_string s + with Invalid_argument _ -> + prerr_endline ("Error: low/high expected after "^opt); exit 1 + +let get_async_proofs_mode opt = let open Stm.AsyncOpts in function + | "no" | "off" -> APoff + | "yes" | "on" -> APon + | "lazy" -> APonLazy + | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 + +let get_cache opt = function + | "force" -> Some Stm.AsyncOpts.Force + | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 + +let is_not_dash_option = function + | Some f when String.length f > 0 && f.[0] <> '-' -> true + | _ -> false + +let rec add_vio_args peek next oval = + if is_not_dash_option (peek ()) then + let oval = add_vio_file oval (next ()) in + add_vio_args peek next oval + else oval + +let get_native_name s = + (* We ignore even critical errors because this mode has to be super silent *) + try + String.concat "/" [Filename.dirname s; + Nativelib.output_dir; Library.native_name_from_filename s] + with _ -> "" + +(*s Parsing of the command line. + We no longer use [Arg.parse], in order to use share [Usage.print_usage] + between coqtop and coqc. *) + +let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem" + (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned") + +exception NoCoqLib + +let usage batch = + begin + try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib) + with NoCoqLib -> usage_no_coqlib () + end; + let lp = Coqinit.toplevel_init_load_path () in + (* Necessary for finding the toplevels below *) + List.iter Mltop.add_coq_path lp; + if batch then Usage.print_usage_coqc () + else begin + Mltop.load_ml_objects_raw_rex + (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$")); + Usage.print_usage_coqtop () + end + +(* Main parsing routine *) +let parse_args arglist : coq_cmdopts * string list = + let args = ref arglist in + let extras = ref [] in + let rec parse oval = match !args with + | [] -> + (oval, List.rev !extras) + | opt :: rem -> + args := rem; + let next () = match !args with + | x::rem -> args := rem; x + | [] -> error_missing_arg opt + in + let peek_next () = match !args with + | x::_ -> Some x + | [] -> None + in + let noval = begin match opt with + + (* Complex options with many args *) + |"-I"|"-include" -> + begin match rem with + | d :: rem -> + args := rem; + add_ml_include oval d + | [] -> error_missing_arg opt + end + |"-Q" -> + begin match rem with + | d :: p :: rem -> + args := rem; + add_vo_include oval d p false + | _ -> error_missing_arg opt + end + |"-R" -> + begin match rem with + | d :: p :: rem -> + args := rem; + add_vo_include oval d p true + | _ -> error_missing_arg opt + end + + (* Options with two arg *) + |"-check-vio-tasks" -> + let tno = get_task_list (next ()) in + let tfile = next () in + add_vio_task oval (tno,tfile) + + |"-schedule-vio-checking" -> + let oval = { oval with vio_checking = true } in + let oval = set_vio_checking_j oval opt (next ()) in + let oval = add_vio_file oval (next ()) in + add_vio_args peek_next next oval + + |"-schedule-vio2vo" -> + let oval = set_vio_checking_j oval opt (next ()) in + let oval = add_vio_file oval (next ()) in + add_vio_args peek_next next oval + + (* Options with one arg *) + |"-coqlib" -> + Flags.coqlib_spec := true; + Flags.coqlib := (next ()); + oval + + |"-async-proofs" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next()) + }} + |"-async-proofs-j" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ())) + }} + |"-async-proofs-cache" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ()) + }} + + |"-async-proofs-tac-j" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ())) + }} + + |"-async-proofs-worker-priority" -> + WorkerLoop.async_proofs_worker_priority := get_priority opt (next ()); + oval + + |"-async-proofs-private-flags" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_private_flags = Some (next ()); + }} + + |"-async-proofs-tactic-error-resilience" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ()) + }} + + |"-async-proofs-command-error-resilience" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ()) + }} + + |"-async-proofs-delegation-threshold" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ()) + }} + + |"-worker-id" -> set_worker_id opt (next ()); oval + + |"-compat" -> + let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in + Flags.compat_version := v; + add_compat_require oval v + + |"-compile" -> + add_compile oval false (next ()) + + |"-compile-verbose" -> + add_compile oval true (next ()) + + |"-dump-glob" -> + Dumpglob.dump_into_file (next ()); + { oval with glob_opt = true } + + |"-feedback-glob" -> + Dumpglob.feedback_glob (); oval + + |"-exclude-dir" -> + System.exclude_directory (next ()); oval + + |"-init-file" -> + { oval with rcfile = Some (next ()); } + + |"-inputstate"|"-is" -> + set_inputstate oval (next ()) + + |"-outputstate" -> + set_outputstate oval (next ()) + + |"-load-ml-object" -> + Mltop.dir_ml_load (next ()); oval + + |"-load-ml-source" -> + Mltop.dir_ml_use (next ()); oval + + |"-load-vernac-object" -> + add_vo_require oval (next ()) None None + + |"-load-vernac-source"|"-l" -> + add_load_vernacular oval false (next ()) + + |"-load-vernac-source-verbose"|"-lv" -> + add_load_vernacular oval true (next ()) + + |"-print-mod-uid" -> + let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 + + |"-profile-ltac-cutoff" -> + Flags.profile_ltac := true; + Flags.profile_ltac_cutoff := get_float opt (next ()); + oval + + |"-require" -> add_vo_require oval (next ()) None (Some false) + + |"-top" -> + let topname = Libnames.dirpath_of_string (next ()) in + if Names.DirPath.is_empty topname then + CErrors.user_err Pp.(str "Need a non empty toplevel module name"); + { oval with toplevel_name = topname } + + |"-main-channel" -> + Spawned.main_channel := get_host_port opt (next()); oval + + |"-control-channel" -> + Spawned.control_channel := get_host_port opt (next()); oval + + |"-vio2vo" -> + let oval = add_compile oval false (next ()) in + { oval with compilation_mode = Vio2Vo } + + |"-toploop" -> + if !Coqloop.print_emacs then + CErrors.user_err Pp.(str "Flags -toploop and -emacs are incompatible"); + { oval with toploop = Some (next ()) } + + |"-w" | "-W" -> + let w = next () in + if w = "none" then + (CWarnings.set_flags w; oval) + else + let w = CWarnings.get_flags () ^ "," ^ w in + CWarnings.set_flags (CWarnings.normalize_flags_string w); + oval + + |"-o" -> { oval with compilation_output_name = Some (next()) } + + (* Options with zero arg *) + |"-async-queries-always-delegate" + |"-async-proofs-always-delegate" + |"-async-proofs-full" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_full = true; + }} + |"-async-proofs-never-reopen-branch" -> + { oval with stm_flags = { oval.stm_flags with + Stm.AsyncOpts.async_proofs_never_reopen_branch = true + }} + |"-batch" -> set_batch_mode oval + |"-test-mode" -> Flags.test_mode := true; oval + |"-beautify" -> Flags.beautify := true; oval + |"-boot" -> Flags.boot := true; { oval with load_rcfile = false; } + |"-bt" -> Backtrace.record_backtrace true; oval + |"-color" -> set_color oval (next ()) + |"-config"|"--config" -> { oval with print_config = true } + |"-debug" -> Coqinit.set_debug (); oval + |"-stm-debug" -> Stm.stm_debug := true; oval + |"-emacs" -> set_emacs oval + |"-filteropts" -> { oval with filter_opts = true } + |"-ideslave" -> + if !Coqloop.print_emacs then + CErrors.user_err Pp.(str "Flags -ideslave and -emacs are incompatible"); + Flags.ide_slave := true; + { oval with toploop = Some "coqidetop" } + + |"-impredicative-set" -> + { oval with impredicative_set = Declarations.ImpredicativeSet } + |"-indices-matter" -> Indtypes.enforce_indices_matter (); oval + |"-m"|"--memory" -> { oval with memory_stat = true } + |"-noinit"|"-nois" -> { oval with load_init = false } + |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with glob_opt = true } + |"-native-compiler" -> + if not Coq_config.native_compiler then + warning "Native compilation was disabled at configure time." + else Flags.output_native_objects := true; oval + |"-output-context" -> { oval with output_context = true } + |"-profile-ltac" -> Flags.profile_ltac := true; oval + |"-q" -> { oval with load_rcfile = false; } + |"-quiet"|"-silent" -> + Flags.quiet := true; + Flags.make_warn false; + oval + |"-quick" -> { oval with compilation_mode = BuildVio } + |"-list-tags" -> { oval with print_tags = true } + |"-time" -> { oval with time = true } + |"-type-in-type" -> set_type_in_type (); oval + |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) + |"-where" -> { oval with print_where = true } + |"-h"|"-H"|"-?"|"-help"|"--help" -> usage oval.batch_mode; oval + |"-v"|"--version" -> Usage.version (exitcode oval) + |"-print-version"|"--print-version" -> + Usage.machine_readable_version (exitcode oval) + + (* Unknown option *) + | s -> + extras := s :: !extras; + oval + end in + parse noval + in + try + parse init_args + with any -> fatal_error any diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli new file mode 100644 index 000000000..8ee1a8f55 --- /dev/null +++ b/toplevel/coqargs.mli @@ -0,0 +1,63 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +type compilation_mode = BuildVo | BuildVio | Vio2Vo +type color = [`ON | `AUTO | `OFF] + +type coq_cmdopts = { + + load_init : bool; + load_rcfile : bool; + rcfile : string option; + + ml_includes : string list; + vo_includes : (string * Names.DirPath.t * bool) list; + vo_requires : (string * string option * bool option) list; + + (* Fuse these two? Currently, [batch_mode] is only used to + distinguish coqc / coqtop in help display. *) + batch_mode : bool; + compilation_mode : compilation_mode; + + toplevel_name : Names.DirPath.t; + toploop : string option; + + compile_list: (string * bool) list; (* bool is verbosity *) + compilation_output_name : string option; + + load_vernacular_list : (string * bool) list; + + vio_checking: bool; + vio_tasks : (int list * string) list; + vio_files : string list; + vio_files_j : int; + + color : color; + + impredicative_set : Declarations.set_predicativity; + stm_flags : Stm.AsyncOpts.stm_opt; + debug : bool; + time : bool; + + filter_opts : bool; + + glob_opt : bool; + + memory_stat : bool; + print_tags : bool; + print_where : bool; + print_config: bool; + output_context : bool; + + inputstate : string option; + outputstate : string option; + +} + +val parse_args : string list -> coq_cmdopts * string list +val exitcode : coq_cmdopts -> int diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 10205964a..8574092b8 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -20,21 +20,15 @@ let set_debug () = does not exist. *) let rcdefaultname = "coqrc" -let rcfile = ref "" -let rcfile_specified = ref false -let set_rcfile s = rcfile := s; rcfile_specified := true -let load_rc = ref true -let no_load_rc () = load_rc := false - -let load_rcfile ~time doc sid = - if !load_rc then +let load_rcfile ~rcfile ~time doc sid = try - if !rcfile_specified then - if CUnix.file_readable_p !rcfile then - Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid !rcfile - else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) - else + match rcfile with + | Some rcfile -> + if CUnix.file_readable_p rcfile then + Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid rcfile + else raise (Sys_error ("Cannot read rcfile: "^ rcfile)) + | None -> try let warn x = Feedback.msg_warning (str x) in let inferedrc = List.find CUnix.file_readable_p [ @@ -54,9 +48,6 @@ let load_rcfile ~time doc sid = let reraise = CErrors.push reraise in let () = Feedback.msg_info (str"Load of rcfile failed.") in iraise reraise - else - (Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); - doc, sid) (* Recursively puts dir in the LoadPath if -nois was not passed *) let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml = @@ -77,13 +68,6 @@ let build_userlib_path ~unix_path = } } -(* Options -I, -I-as, and -R of the command line *) -let includes = ref [] -let push_include s alias implicit = - includes := (s, alias, implicit) :: !includes -let ml_includes = ref [] -let push_ml_include s = ml_includes := s :: !ml_includes - let ml_path_if c p = let open Mltop in let f x = { recursive = false; path_spec = MlPath x } in @@ -128,17 +112,7 @@ let libs_init_load_path ~load_init = coq_path = Libnames.default_root_prefix; implicit = false; has_ml = AddTopML } - } ] @ - - (* additional loadpaths, given with options -Q and -R *) - List.map - (fun (unix_path, coq_path, implicit) -> - { recursive = true; - path_spec = VoPath { unix_path; coq_path; has_ml = Mltop.AddNoML; implicit } }) - (List.rev !includes) @ - - (* additional ml directories, given with option -I *) - List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev !ml_includes) + } ] (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 0d2da84bb..0ceba5b38 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -10,19 +10,12 @@ val set_debug : unit -> unit -val set_rcfile : string -> unit - -val no_load_rc : unit -> unit -val load_rcfile : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t - -val push_include : string -> Names.DirPath.t -> bool -> unit -(** [push_include phys_path log_path implicit] *) - -val push_ml_include : string -> unit +val load_rcfile : rcfile:(string option) -> time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t val init_ocaml_path : unit -> unit (* LoadPath for toploop toplevels *) val toplevel_init_load_path : unit -> Mltop.coq_path list + (* LoadPath for Coq user libraries *) val libs_init_load_path : load_init:bool -> Mltop.coq_path list diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 5c1b27c33..aade101a4 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -312,7 +312,7 @@ let do_vernac ~time doc sid = top_stderr (fnl ()); raise CErrors.Quit | CErrors.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise CErrors.Drop - else (Feedback.msg_error (str "There is no ML toplevel."); doc, sid) + else (Feedback.msg_warning (str "There is no ML toplevel."); doc, sid) (* Exception printing should be done by the feedback listener, however this is not yet ready so we rely on the exception for now. *) @@ -353,7 +353,7 @@ let rec loop ~time doc = | CErrors.Drop -> doc | CErrors.Quit -> exit 0 | any -> - Feedback.msg_error (str "Anomaly: main loop exited with exception: " ++ + top_stderr (str "Anomaly: main loop exited with exception: " ++ str (Printexc.to_string any) ++ fnl() ++ str"Please report" ++ diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 400f7048d..9058f0846 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -7,8 +7,7 @@ (************************************************************************) open Pp -open CErrors -open Libnames +open Coqargs let () = at_exit flush_all @@ -31,66 +30,21 @@ let print_header () = let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) -let toploop = ref None - -let color : [`ON | `AUTO | `OFF] ref = ref `AUTO -let set_color = function -| "yes" | "on" -> color := `ON -| "no" | "off" -> color := `OFF -| "auto" -> color := `AUTO -| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1 - -let init_color () = - let has_color = match !color with - | `OFF -> false - | `ON -> true - | `AUTO -> - Terminal.has_style Unix.stdout && - Terminal.has_style Unix.stderr && - (* emacs compilation buffer does not support colors by default, - its TERM variable is set to "dumb". *) - try Sys.getenv "TERM" <> "dumb" with Not_found -> false - in - if has_color then begin - let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in - match colors with - | None -> - (** Default colors *) - Topfmt.init_terminal_output ~color:true - | Some "" -> - (** No color output *) - Topfmt.init_terminal_output ~color:false - | Some s -> - (** Overwrite all colors *) - Topfmt.clear_styles (); - Topfmt.parse_color_config s; - Topfmt.init_terminal_output ~color:true - end - else - Topfmt.init_terminal_output ~color:false - -let toploop_init = ref begin fun x -> - let () = init_color () in - let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in - x - end - (* Feedback received in the init stage, this is different as the STM will not be generally be initialized, thus stateid, etc... may be bogus. For now we just print to the console too *) let coqtop_init_feed = Coqloop.coqloop_feed let drop_last_doc = ref None -let measure_time = ref false (* Default toplevel loop *) -let console_toploop_run doc = +let console_toploop_run opts doc = (* We initialize the console only if we run the toploop_run *) let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in if Dumpglob.dump () then begin Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () end; - let doc = Coqloop.loop ~time:!measure_time doc in + let doc = Coqloop.loop ~time:opts.time doc in (* Initialise and launch the Ocaml toplevel *) drop_last_doc := Some doc; Coqinit.init_ocaml_path(); @@ -100,10 +54,7 @@ let console_toploop_run doc = let toploop_run = ref console_toploop_run -let output_context = ref false - let memory_stat = ref false - let print_memory_stat () = begin (* -m|--memory from the command-line *) if !memory_stat then @@ -124,133 +75,87 @@ let print_memory_stat () = let _ = at_exit print_memory_stat (******************************************************************************) -(* Engagement *) -(******************************************************************************) -let impredicative_set = ref Declarations.PredicativeSet -let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet -let set_type_in_type () = - let typing_flags = Environ.typing_flags (Global.env ()) in - Global.set_typing_flags { typing_flags with Declarations.check_universes = false } -let engage () = - Global.set_engagement !impredicative_set - -(******************************************************************************) -(* Interactive toplevel name *) -(******************************************************************************) -let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"]) -let toplevel_name = ref toplevel_default_name -let set_toplevel_name dir = - if Names.DirPath.is_empty dir then user_err Pp.(str "Need a non empty toplevel module name"); - toplevel_name := dir - -(******************************************************************************) (* Input/Output State *) (******************************************************************************) -let warn_deprecated_inputstate = - CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" - (fun () -> strbrk "The inputstate option is deprecated and discouraged.") - -let inputstate = ref "" -let set_inputstate s = - warn_deprecated_inputstate (); - inputstate:=s -let inputstate () = - if not (CString.is_empty !inputstate) then - let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in - States.intern_state fname - -let warn_deprecated_outputstate = - CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated" - (fun () -> - strbrk "The outputstate option is deprecated and discouraged.") - -let outputstate = ref "" -let set_outputstate s = - warn_deprecated_outputstate (); - outputstate:=s -let outputstate () = - if not (CString.is_empty !outputstate) then - let fname = CUnix.make_suffix !outputstate ".coq" in - States.extern_state fname +let inputstate opts = + Option.iter (fun istate_file -> + let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in + States.intern_state fname) opts.inputstate + +let outputstate opts = + Option.iter (fun ostate_file -> + let fname = CUnix.make_suffix ostate_file ".coq" in + States.extern_state fname) opts.outputstate (******************************************************************************) (* Interactive Load File Simulation *) (******************************************************************************) -let load_vernacular_list = ref ([] : (string * bool) list) - -let add_load_vernacular verb s = - load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list - -let load_vernacular ~time doc sid = +let load_vernacular opts doc sid = List.fold_left (fun (doc,sid) (f_in, verbosely) -> let s = Loadpath.locate_file f_in in if !Flags.beautify then - Flags.with_option Flags.beautify_file (Vernac.load_vernac ~time ~verbosely ~interactive:false ~check:true doc sid) f_in + Flags.with_option Flags.beautify_file (Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true doc sid) f_in else - Vernac.load_vernac ~time ~verbosely ~interactive:false ~check:true doc sid s) - (doc, sid) (List.rev !load_vernacular_list) - -let load_init_vernaculars ~time doc sid = - let doc, sid = Coqinit.load_rcfile ~time doc sid in - load_vernacular ~time doc sid + Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true doc sid s) + (doc, sid) (List.rev opts.load_vernacular_list) + +let load_init_vernaculars opts doc sid = + let doc, sid = if opts.load_rcfile then + Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time doc sid + else begin + Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); + doc,sid + end in + load_vernacular opts doc sid (******************************************************************************) -(* Required Modules *) +(* Startup LoadPath and Modules *) (******************************************************************************) -let set_include d p implicit = - let p = dirpath_of_string p in - Coqinit.push_include d p implicit +(* prelude_data == From Coq Require Export Prelude. *) +let prelude_data = "Prelude", Some "Coq", Some true -(* None = No Import; Some false = Import; Some true = Export *) -let require_list = ref ([] : (string * string option * bool option) list) -let add_require s = require_list := s :: !require_list +let require_libs opts = + if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires -let load_init = ref true +let cmdline_load_path opts = + let open Mltop in + (* loadpaths given by options -Q and -R *) + List.map + (fun (unix_path, coq_path, implicit) -> + { recursive = true; + path_spec = VoPath { unix_path; coq_path; has_ml = Mltop.AddNoML; implicit } }) + (List.rev opts.vo_includes) @ -(* From Coq Require Import Prelude. *) -let prelude_data = "Prelude", Some "Coq", Some true + (* additional ml directories, given with option -I *) + List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev opts.ml_includes) -let require_libs () = - if !load_init then prelude_data :: !require_list else !require_list - -let add_compat_require v = - match v with - | Flags.V8_5 -> add_require ("Coq.Compat.Coq85", None, Some false) - | Flags.V8_6 -> add_require ("Coq.Compat.Coq86", None, Some false) - | Flags.V8_7 -> add_require ("Coq.Compat.Coq87", None, Some false) - | Flags.VOld | Flags.Current -> () +let build_load_path opts = + Coqinit.libs_init_load_path ~load_init:opts.load_init @ + cmdline_load_path opts (******************************************************************************) -(* File Compilation *) +(* Fatal Errors *) (******************************************************************************) -let glob_opt = ref false - -let compile_list = ref ([] : (bool * string) list) - -type compilation_mode = BuildVo | BuildVio | Vio2Vo -let compilation_mode = ref BuildVo -let compilation_output_name = ref None - -let batch_mode = ref false -let set_batch_mode () = - System.trust_file_cache := false; - batch_mode := true - -let add_compile verbose s = - set_batch_mode (); - Flags.quiet := true; - if not !glob_opt then Dumpglob.dump_to_dotglob (); - (** make the file name explicit; needed not to break up Coq loadpath stuff. *) - let s = - let open Filename in - if is_implicit s - then concat current_dir_name s - else s +(** Prints info which is either an error or an anomaly and then exits + with the appropriate error code *) +let fatal_error msg = + Topfmt.std_logger Feedback.Error msg; + flush_all (); + exit 1 + +let fatal_error_exn ?extra exn = + Topfmt.print_err_exn ?extra exn; + flush_all (); + let exit_code = + if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in - compile_list := (verbose,s) :: !compile_list + exit exit_code +(******************************************************************************) +(* File Compilation *) +(******************************************************************************) let warn_file_no_extension = CWarnings.create ~name:"file-no-extension" ~category:"filesystem" (fun (f,ext) -> @@ -268,16 +173,11 @@ let ensure_ext ext f = let chop_extension f = try Filename.chop_extension f with _ -> f -let compile_error msg = - Topfmt.std_logger Feedback.Error msg; - flush_all (); - exit 1 - let ensure_bname src tgt = let src, tgt = Filename.basename src, Filename.basename tgt in let src, tgt = chop_extension src, chop_extension tgt in if src <> tgt then - compile_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ + fatal_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ str "Source: " ++ str src ++ fnl () ++ str "Target: " ++ str tgt) @@ -289,25 +189,23 @@ let ensure_vio v vio = ensure ".vio" v vio let ensure_exists f = if not (Sys.file_exists f) then - compile_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) - -let top_stm_options = ref Stm.AsyncOpts.default_opts + fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) (* Compile a vernac file *) -let compile ~time ~verbosely ~f_in ~f_out = +let compile opts ~verbosely ~f_in ~f_out = let check_pending_proofs () = let pfs = Proof_global.get_all_proof_names () in if not (CList.is_empty pfs) then - compile_error (str "There are pending proofs: " + fatal_error (str "There are pending proofs: " ++ (pfs |> List.rev |> prlist_with_sep pr_comma Names.Id.print) ++ str ".") in - let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in - let require_libs = require_libs () in - let stm_options = !top_stm_options in - match !compilation_mode with + let iload_path = build_load_path opts in + let require_libs = require_libs opts in + let stm_options = opts.stm_flags in + match opts.compilation_mode with | BuildVo -> Flags.record_aux_file := true; let long_f_dot_v = ensure_v f_in in @@ -319,12 +217,10 @@ let compile ~time ~verbosely ~f_in ~f_out = let doc, sid = Stm.(new_doc { doc_type = VoDoc long_f_dot_vo; - iload_path; - require_libs; - stm_options; + iload_path; require_libs; stm_options; }) in - let doc, sid = load_init_vernaculars ~time doc sid in + let doc, sid = load_init_vernaculars opts doc sid in let ldir = Stm.get_ldir ~doc in Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_vo) @@ -332,7 +228,7 @@ let compile ~time ~verbosely ~f_in ~f_out = Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); let wall_clock1 = Unix.gettimeofday () in - let doc, _ = Vernac.load_vernac ~time ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in + let doc, _ = Vernac.load_vernac ~time:opts.time ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in let _doc = Stm.join ~doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); @@ -354,17 +250,26 @@ let compile ~time ~verbosely ~f_in ~f_out = | None -> long_f_dot_v ^ "io" | Some f -> ensure_vio long_f_dot_v f in + (* We need to disable error resiliency, otherwise some errors + will be ignored in batch mode. c.f. #6707 + + This is not necessary in the vo case as it fully checks the + document anyways. *) + let stm_options = let open Stm.AsyncOpts in + { stm_options with + async_proofs_cmd_error_resilience = false; + async_proofs_tac_error_resilience = `None; + } in + let doc, sid = Stm.(new_doc { doc_type = VioDoc long_f_dot_vio; - iload_path; - require_libs; - stm_options; + iload_path; require_libs; stm_options; }) in - let doc, sid = load_init_vernaculars ~time doc sid in + let doc, sid = load_init_vernaculars opts doc sid in let ldir = Stm.get_ldir ~doc in - let doc, _ = Vernac.load_vernac ~time ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in + let doc, _ = Vernac.load_vernac ~time:opts.time ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in let doc = Stm.finish ~doc in check_pending_proofs (); let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in @@ -379,91 +284,96 @@ let compile ~time ~verbosely ~f_in ~f_out = let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in Library.save_library_raw lfdv sum lib univs proofs -let compile ~time ~verbosely ~f_in ~f_out = +let compile opts ~verbosely ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); - compile ~time ~verbosely ~f_in ~f_out; + compile opts ~verbosely ~f_in ~f_out; CoqworkmgrApi.giveback 1 -let compile_file (verbosely,f_in) = +let compile_file opts (f_in, verbosely) = if !Flags.beautify then Flags.with_option Flags.beautify_file - (fun f_in -> compile ~verbosely ~f_in ~f_out:None) f_in + (fun f_in -> compile opts ~verbosely ~f_in ~f_out:None) f_in else - compile ~verbosely ~f_in ~f_out:None + compile opts ~verbosely ~f_in ~f_out:None -let compile_files ~time = - if !compile_list == [] then () - else List.iter (compile_file ~time) (List.rev !compile_list) +let compile_files opts = + let compile_list = List.rev opts.compile_list in + List.iter (compile_file opts) compile_list (******************************************************************************) (* VIO Dispatching *) (******************************************************************************) - -let vio_tasks = ref [] -let add_vio_task f = - set_batch_mode (); - Flags.quiet := true; - vio_tasks := f :: !vio_tasks - -let check_vio_tasks () = +let check_vio_tasks opts = let rc = List.fold_left (fun acc t -> Vio_checking.check_vio t && acc) - true (List.rev !vio_tasks) in - if not rc then exit 1 + true (List.rev opts.vio_tasks) in + if not rc then fatal_error Pp.(str "VIO Task Check failed") (* vio files *) -let vio_files = ref [] -let vio_files_j = ref 0 -let vio_checking = ref false -let add_vio_file f = - set_batch_mode (); - Flags.quiet := true; - vio_files := f :: !vio_files - -let set_vio_checking_j opt j = - try vio_files_j := int_of_string j - with Failure _ -> - prerr_endline ("The first argument of " ^ opt ^ " must the number"); - prerr_endline "of concurrent workers to be used (a positive integer)."; - prerr_endline "Makefiles generated by coq_makefile should be called"; - prerr_endline "setting the J variable like in 'make vio2vo J=3'"; - exit 1 - -let schedule_vio () = +let schedule_vio opts = (* We must add update the loadpath here as the scheduling process happens outside of the STM *) - let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in + let iload_path = build_load_path opts in List.iter Mltop.add_coq_path iload_path; - if !vio_checking then - Vio_checking.schedule_vio_checking !vio_files_j !vio_files + if opts.vio_checking then + Vio_checking.schedule_vio_checking opts.vio_files_j opts.vio_files else - Vio_checking.schedule_vio_compilation !vio_files_j !vio_files + Vio_checking.schedule_vio_compilation opts.vio_files_j opts.vio_files (******************************************************************************) -(* UI Options *) +(* Color Options *) (******************************************************************************) -(** Options for proof general *) - -let set_emacs () = - if not (Option.is_empty !toploop) then - user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop"); - Coqloop.print_emacs := true; - Printer.enable_goal_tags_printing := true; - color := `OFF - -(** Options for CoqIDE *) - -let set_ideslave () = - if !Coqloop.print_emacs then user_err Pp.(str "Flags -ideslave and -emacs are incompatible"); - toploop := Some "coqidetop"; - Flags.ide_slave := true +let init_color color_mode = + let has_color = match color_mode with + | `OFF -> false + | `ON -> true + | `AUTO -> + Terminal.has_style Unix.stdout && + Terminal.has_style Unix.stderr && + (* emacs compilation buffer does not support colors by default, + its TERM variable is set to "dumb". *) + try Sys.getenv "TERM" <> "dumb" with Not_found -> false + in + if has_color then begin + let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in + match colors with + | None -> + (** Default colors *) + Topfmt.init_terminal_output ~color:true + | Some "" -> + (** No color output *) + Topfmt.init_terminal_output ~color:false + | Some s -> + (** Overwrite all colors *) + Topfmt.clear_styles (); + Topfmt.parse_color_config s; + Topfmt.init_terminal_output ~color:true + end + else + Topfmt.init_terminal_output ~color:false -(** Options for slaves *) +let toploop_init = ref begin fun opts x -> + let () = init_color opts.color in + let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in + x + end -let set_toploop name = - if !Coqloop.print_emacs then user_err Pp.(str "Flags -toploop and -emacs are incompatible"); - toploop := Some name +let print_style_tags opts = + let () = init_color opts.color in + let tags = Topfmt.dump_tags () in + let iter (t, st) = + let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in + print_string opt + in + let make (t, st) = + let tags = List.map string_of_int (Terminal.repr st) in + (t ^ "=" ^ String.concat ";" tags) + in + let repr = List.map make tags in + let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in + let () = List.iter iter tags in + flush_all () (** GC tweaking *) @@ -490,339 +400,37 @@ let init_gc () = Gc.minor_heap_size = 33554432; (** 4M *) Gc.space_overhead = 120} -(*s Parsing of the command line. - We no longer use [Arg.parse], in order to use share [Usage.print_usage] - between coqtop and coqc. *) - -let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem" - (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned") - -exception NoCoqLib - -let usage batch = - begin - try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib) - with NoCoqLib -> usage_no_coqlib () - end; - let lp = Coqinit.toplevel_init_load_path () in - (* Necessary for finding the toplevels below *) - List.iter Mltop.add_coq_path lp; - if batch then Usage.print_usage_coqc () - else begin - Mltop.load_ml_objects_raw_rex - (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$")); - Usage.print_usage_coqtop () - end - -let print_style_tags () = - let () = init_color () in - let tags = Topfmt.dump_tags () in - let iter (t, st) = - let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in - print_string opt - in - let make (t, st) = - let tags = List.map string_of_int (Terminal.repr st) in - (t ^ "=" ^ String.concat ";" tags) - in - let repr = List.map make tags in - let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in - let () = List.iter iter tags in - flush_all () - -let error_missing_arg s = - prerr_endline ("Error: extra argument expected after option "^s); - prerr_endline "See -help for the syntax of supported options"; - exit 1 - -let filter_opts = ref false -let exitcode () = if !filter_opts then 2 else 0 - -let print_where = ref false -let print_config = ref false -let print_tags = ref false - -let get_priority opt s = - try CoqworkmgrApi.priority_of_string s - with Invalid_argument _ -> - prerr_endline ("Error: low/high expected after "^opt); exit 1 - -let get_async_proofs_mode opt = let open Stm.AsyncOpts in function - | "no" | "off" -> APoff - | "yes" | "on" -> APon - | "lazy" -> APonLazy - | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 - -let get_cache opt = function - | "force" -> Some Stm.AsyncOpts.Force - | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 - - -let set_worker_id opt s = - assert (s <> "master"); - Flags.async_proofs_worker_id := s - -let get_bool opt = function - | "yes" | "on" -> true - | "no" | "off" -> false - | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1 - -let get_int opt n = - try int_of_string n - with Failure _ -> - prerr_endline ("Error: integer expected after option "^opt); exit 1 - -let get_float opt n = - try float_of_string n - with Failure _ -> - prerr_endline ("Error: float expected after option "^opt); exit 1 - -let get_host_port opt s = - match CString.split ':' s with - | [host; portr; portw] -> - Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) - | ["stdfds"] -> Some Spawned.AnonPipe - | _ -> - prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt); - exit 1 - -let get_error_resilience opt = function - | "on" | "all" | "yes" -> `All - | "off" | "no" -> `None - | s -> `Only (CString.split ',' s) - -let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) - -let is_not_dash_option = function - | Some f when String.length f > 0 && f.[0] <> '-' -> true - | _ -> false - -let get_native_name s = - (* We ignore even critical errors because this mode has to be super silent *) - try - String.concat "/" [Filename.dirname s; - Nativelib.output_dir; Library.native_name_from_filename s] - with _ -> "" - -(** Prints info which is either an error or an anomaly and then exits - with the appropriate error code *) -let fatal_error ?extra exn = - Topfmt.print_err_exn ?extra exn; - let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in - exit exit_code - -let parse_args arglist = - let args = ref arglist in - let extras = ref [] in - let rec parse () = match !args with - | [] -> List.rev !extras - | opt :: rem -> - args := rem; - let next () = match !args with - | x::rem -> args := rem; x - | [] -> error_missing_arg opt - in - let peek_next () = match !args with - | x::_ -> Some x - | [] -> None - in - begin match opt with - - (* Complex options with many args *) - |"-I"|"-include" -> - begin match rem with - | d :: rem -> Coqinit.push_ml_include d; args := rem - | [] -> error_missing_arg opt - end - |"-Q" -> - begin match rem with - | d :: p :: rem -> set_include d p false; args := rem - | _ -> error_missing_arg opt - end - |"-R" -> - begin match rem with - | d :: p :: rem -> set_include d p true; args := rem - | _ -> error_missing_arg opt - end - - (* Options with two arg *) - |"-check-vio-tasks" -> - let tno = get_task_list (next ()) in - let tfile = next () in - add_vio_task (tno,tfile) - |"-schedule-vio-checking" -> - vio_checking := true; - set_vio_checking_j opt (next ()); - add_vio_file (next ()); - while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done - |"-schedule-vio2vo" -> - set_vio_checking_j opt (next ()); - add_vio_file (next ()); - while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done - - (* Options with one arg *) - |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ()) - |"-async-proofs" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next()) - } - |"-async-proofs-j" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_n_workers = (get_int opt (next ())) - } - |"-async-proofs-cache" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ()) - } - |"-async-proofs-tac-j" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ())) - } - |"-async-proofs-worker-priority" -> - WorkerLoop.async_proofs_worker_priority := get_priority opt (next ()) - |"-async-proofs-private-flags" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_private_flags = Some (next ()); - } - |"-async-proofs-tactic-error-resilience" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ()); - } - |"-async-proofs-command-error-resilience" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_cmd_error_resilience = get_bool opt (next ()) - } - |"-async-proofs-delegation-threshold" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_delegation_threshold = get_float opt (next ()) - } - |"-worker-id" -> set_worker_id opt (next ()) - |"-compat" -> - let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in - Flags.compat_version := v; add_compat_require v - |"-compile" -> add_compile false (next ()) - |"-compile-verbose" -> add_compile true (next ()) - |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true - |"-feedback-glob" -> Dumpglob.feedback_glob () - |"-exclude-dir" -> System.exclude_directory (next ()) - |"-init-file" -> Coqinit.set_rcfile (next ()) - |"-inputstate"|"-is" -> set_inputstate (next ()) - |"-load-ml-object" -> Mltop.dir_ml_load (next ()) - |"-load-ml-source" -> Mltop.dir_ml_use (next ()) - |"-load-vernac-object" -> add_require (next (), None, None) - |"-load-vernac-source"|"-l" -> add_load_vernacular false (next ()) - |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ()) - |"-outputstate" -> set_outputstate (next ()) - |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 - |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ()) - |"-require" -> add_require (next (), None, Some false) - |"-top" -> set_toplevel_name (dirpath_of_string (next ())) - |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()) - |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) - |"-vio2vo" -> - add_compile false (next ()); - compilation_mode := Vio2Vo - |"-toploop" -> set_toploop (next ()) - |"-w" | "-W" -> - let w = next () in - if w = "none" then CWarnings.set_flags w - else - let w = CWarnings.get_flags () ^ "," ^ w in - CWarnings.set_flags (CWarnings.normalize_flags_string w) - |"-o" -> compilation_output_name := Some (next()) - - (* Options with zero arg *) - |"-async-queries-always-delegate" - |"-async-proofs-always-delegate" - |"-async-proofs-full" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_full = true; - } - |"-async-proofs-never-reopen-branch" -> - top_stm_options := - { !top_stm_options with - Stm.AsyncOpts.async_proofs_never_reopen_branch = true; - } - |"-batch" -> set_batch_mode () - |"-test-mode" -> Flags.test_mode := true - |"-beautify" -> Flags.beautify := true - |"-boot" -> Flags.boot := true; Coqinit.no_load_rc () - |"-bt" -> Backtrace.record_backtrace true - |"-color" -> set_color (next ()) - |"-config"|"--config" -> print_config := true - |"-debug" -> Coqinit.set_debug () - |"-stm-debug" -> Stm.stm_debug := true - |"-emacs" -> set_emacs () - |"-filteropts" -> filter_opts := true - |"-h"|"-H"|"-?"|"-help"|"--help" -> usage !batch_mode - |"-ideslave" -> set_ideslave () - |"-impredicative-set" -> set_impredicative_set () - |"-indices-matter" -> Indtypes.enforce_indices_matter () - |"-m"|"--memory" -> memory_stat := true - |"-noinit"|"-nois" -> load_init := false - |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true - |"-native-compiler" -> - if not Coq_config.native_compiler then - warning "Native compilation was disabled at configure time." - else Flags.output_native_objects := true - |"-output-context" -> output_context := true - |"-profile-ltac" -> Flags.profile_ltac := true - |"-q" -> Coqinit.no_load_rc () - |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false - |"-quick" -> compilation_mode := BuildVio - |"-list-tags" -> print_tags := true - |"-time" -> measure_time := true - |"-type-in-type" -> set_type_in_type () - |"-unicode" -> add_require ("Utf8_core", None, Some false) - |"-v"|"--version" -> Usage.version (exitcode ()) - |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode ()) - |"-where" -> print_where := true - - (* Unknown option *) - | s -> extras := s :: !extras - end; - parse () - in - try - parse () - with any -> fatal_error any - +(** Main init routine *) let init_toplevel arglist = (* Coq's init process, phase 1: - - OCaml parameters, and basic structures and IO + OCaml parameters, basic structures, and IO *) CProfile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) let init_feeder = Feedback.add_feeder coqtop_init_feed in Lib.init(); + (* Coq's init process, phase 2: - - Basic Coq environment, load-path, plugins. + Basic Coq environment, load-path, plugins. *) let res = begin try - let extras = parse_args arglist in + let opts,extras = parse_args arglist in + memory_stat := opts.memory_stat; + (* If we have been spawned by the Spawn module, this has to be done * early since the master waits us to connect back *) Spawned.init_channels (); Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); - if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ())); - if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ())); - if !print_tags then (print_style_tags (); exit (exitcode ())); - if !filter_opts then (print_string (String.concat "\n" extras); exit 0); + if opts.print_where then (print_endline(Envars.coqlib ()); exit(exitcode opts)); + if opts.print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode opts)); + if opts.print_tags then (print_style_tags opts; exit (exitcode opts)); + if opts.filter_opts then (print_string (String.concat "\n" extras); exit 0); let top_lp = Coqinit.toplevel_init_load_path () in List.iter Mltop.add_coq_path top_lp; - Option.iter Mltop.load_ml_object_raw !toploop; - let extras = !toploop_init extras in + Option.iter Mltop.load_ml_object_raw opts.toploop; + let extras = !toploop_init opts extras in if not (CList.is_empty extras) then begin prerr_endline ("Don't know what to do with "^String.concat " " extras); prerr_endline "See -help for the list of supported options"; @@ -830,10 +438,10 @@ let init_toplevel arglist = end; Flags.if_verbose print_header (); Mltop.init_known_plugins (); - engage (); + Global.set_engagement opts.impredicative_set; (* Allow the user to load an arbitrary state here *) - inputstate (); + inputstate opts; (* This state will be shared by all the documents *) Stm.init_core (); @@ -842,9 +450,7 @@ let init_toplevel arglist = It is essential that the module system is in a consistent state before we take the first snapshot. This was not - guaranteed in the past. In particular, we want to be sure we - have called start_library before loading the prelude and rest - of required files. + guaranteed in the past, but now is thanks to the STM API. We split the codepath here depending whether coqtop is called in interactive mode or not. *) @@ -852,39 +458,37 @@ let init_toplevel arglist = (* The condition for starting the interactive mode is a bit convoluted, we should really refactor batch/compilation_mode more. *) - if (not !batch_mode - || CList.(is_empty !compile_list && is_empty !vio_files && is_empty !vio_tasks)) + if (not opts.batch_mode + || CList.(is_empty opts.compile_list && is_empty opts.vio_files && is_empty opts.vio_tasks)) (* Interactive *) then begin - let iload_path = Coqinit.libs_init_load_path ~load_init:!load_init in - let require_libs = require_libs () in - let stm_options = !top_stm_options in - try - let doc, sid = Stm.(new_doc - { doc_type = Interactive !toplevel_name; - iload_path; - require_libs; - stm_options; - }) in - Some (load_init_vernaculars ~time:!measure_time doc sid) - with any -> flush_all(); fatal_error any - (* Non interactive *) + let iload_path = build_load_path opts in + let require_libs = require_libs opts in + let stm_options = opts.stm_flags in + try let doc, sid = + Stm.(new_doc + { doc_type = Interactive opts.toplevel_name; + iload_path; require_libs; stm_options; + }) in + Some (load_init_vernaculars opts doc sid), opts + with any -> flush_all(); fatal_error_exn any + (* Non interactive: we perform a sequence of compilation steps *) end else begin try - compile_files ~time:!measure_time; + compile_files opts; (* Vio compile pass *) - if !vio_files <> [] then schedule_vio (); + if opts.vio_files <> [] then schedule_vio opts; (* Vio task pass *) - check_vio_tasks (); + check_vio_tasks opts; (* Allow the user to output an arbitrary state *) - outputstate (); - None - with any -> flush_all(); fatal_error any + outputstate opts; + None, opts + with any -> flush_all(); fatal_error_exn any end; with any -> flush_all(); let extra = Some (str "Error during initialization: ") in - fatal_error ?extra any + fatal_error_exn ?extra any end in Feedback.del_feeder init_feeder; res @@ -892,12 +496,12 @@ let init_toplevel arglist = let start () = match init_toplevel (List.tl (Array.to_list Sys.argv)) with (* Batch mode *) - | Some (doc, sid) when not !batch_mode -> - !toploop_run doc; + | Some (doc, sid), opts when not opts.batch_mode -> + !toploop_run opts doc; exit 1 - | _ -> + | _ , opts -> flush_all(); - if !output_context then begin + if opts.output_context then begin let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) end; diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 5b9494eaa..4d625a03d 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -11,7 +11,7 @@ state, load the files given on the command line, load the resource file, produce the output state if any, and finally will launch [Coqloop.loop]. *) -val init_toplevel : string list -> (Stm.doc * Stateid.t) option +val init_toplevel : string list -> (Stm.doc * Stateid.t) option * Coqargs.coq_cmdopts val start : unit -> unit @@ -19,6 +19,6 @@ val start : unit -> unit val drop_last_doc : Stm.doc option ref (* For other toploops *) -val toploop_init : (string list -> string list) ref -val toploop_run : (Stm.doc -> unit) ref +val toploop_init : (Coqargs.coq_cmdopts -> string list -> string list) ref +val toploop_run : (Coqargs.coq_cmdopts -> Stm.doc -> unit) ref diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 10bf48647..9fb2e33d7 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -2,4 +2,5 @@ Vernac Usage Coqloop Coqinit +Coqargs Coqtop diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 1c8677e9c..41474fc63 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -340,7 +340,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = match uctx with | Polymorphic_const_entry uctx -> if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) + Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context uctx) else Polymorphic_ind_entry uctx | Monomorphic_const_entry uctx -> Monomorphic_ind_entry uctx @@ -356,7 +356,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = } in (if poly && cum then - Inductiveops.infer_inductive_subtyping env_ar sigma mind_ent + InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls (* Very syntactical equality *) diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index d328ad0cf..fc3495796 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -32,6 +32,7 @@ let explain_exn_default = function | Sys_error msg -> hov 0 (str "System error: " ++ guill msg) | Out_of_memory -> hov 0 (str "Out of memory.") | Stack_overflow -> hov 0 (str "Stack overflow.") + | Dynlink.Error e -> hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e)) | Timeout -> hov 0 (str "Timeout!") | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") (* Exceptions with pre-evaluated error messages *) diff --git a/vernac/record.ml b/vernac/record.ml index 1e464eb8b..d9af5378f 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -423,16 +423,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t mind_entry_universes = univs; } in - let mie = - match ctx with - | Polymorphic_const_entry ctx -> - let env = Global.env () in - let env' = Environ.push_context ctx env in - let evd = Evd.from_env env' in - Inductiveops.infer_inductive_subtyping env' evd mie - | Monomorphic_const_entry _ -> - mie - in + let mie = InferCumulativity.infer_inductive (Global.env ()) mie 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 @@ -501,7 +492,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari match univs with | Polymorphic_const_entry univs -> if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) + Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs) else Polymorphic_ind_entry univs | Monomorphic_const_entry univs -> @@ -632,7 +623,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf match univs with | Polymorphic_const_entry univs -> if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) + Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs) else Polymorphic_ind_entry univs | Monomorphic_const_entry univs -> diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 7e96f28de..1ad7ead72 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Feedback open Pp (** Pp control also belongs here as the terminal is private to the toplevel *) @@ -138,7 +137,7 @@ let make_body quoter info ?pre_hdr s = (* The empty quoter *) let noq x = x (* Generic logger *) -let gen_logger dbg warn ?pre_hdr level msg = match level with +let gen_logger dbg warn ?pre_hdr level msg = let open Feedback in match level with | Debug -> msgnl_with !std_ft (make_body dbg dbg_hdr ?pre_hdr msg) | Info -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg) | Notice -> msgnl_with !std_ft (make_body noq info_hdr ?pre_hdr msg) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index be09696d1..35ef4bfa4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -58,20 +58,20 @@ let show_proof () = let p = Proof_global.give_me_the_proof () in let sigma, env = Pfedit.get_current_context () in let pprf = Proof.partial_proof p in - Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) + Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) let pfts = Proof_global.give_me_the_proof () in let gls,_,_,_,sigma = Proof.proof pfts in - Feedback.msg_notice (pr_evars_int sigma 1 (Evd.undefined_map sigma)) + pr_evars_int sigma 1 (Evd.undefined_map sigma) let show_universes () = let pfts = Proof_global.give_me_the_proof () in let gls,_,_,_,sigma = Proof.proof pfts in let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in - Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma)); - Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx) + Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ + str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx (* Simulate the Intro(s) tactic *) let show_intro all = @@ -83,11 +83,12 @@ let show_intro all = let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in - Feedback.msg_notice (hov 0 (prlist_with_sep spc Id.print lid)) + hov 0 (prlist_with_sep spc Id.print lid) else if not (List.is_empty l) then let n = List.last l in - Feedback.msg_notice (Id.print (List.hd (Tactics.find_intro_names [n] gl))) - end + Id.print (List.hd (Tactics.find_intro_names [n] gl)) + else mt () + end else mt () (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name @@ -146,8 +147,8 @@ let show_match id = let pr_branch l = str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>" in - Feedback.msg_notice (v 1 (str "match # with" ++ fnl () ++ - prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ())) + v 1 (str "match # with" ++ fnl () ++ + prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ()) (* "Print" commands *) @@ -186,23 +187,23 @@ let print_module r = let globdir = Nametab.locate_dir qid in match globdir with DirModule { obj_dir; obj_mp; _ } -> - Feedback.msg_notice (Printmod.print_module (Printmod.printable_body obj_dir) obj_mp) + Printmod.print_module (Printmod.printable_body obj_dir) obj_mp | _ -> raise Not_found with - Not_found -> Feedback.msg_error (str"Unknown Module " ++ pr_qualid qid) + Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) let print_modtype r = let (loc,qid) = qualid_of_reference r in try let kn = Nametab.locate_modtype qid in - Feedback.msg_notice (Printmod.print_modtype kn) + Printmod.print_modtype kn with Not_found -> (* Is there a module of this name ? If yes we display its type *) try let mp = Nametab.locate_module qid in - Feedback.msg_notice (Printmod.print_module false mp) + Printmod.print_module false mp with Not_found -> - Feedback.msg_error (str"Unknown Module Type or Module " ++ pr_qualid qid) + user_err (str"Unknown Module Type or Module " ++ pr_qualid qid) let print_namespace ns = let ns = List.rev (Names.DirPath.repr ns) in @@ -272,7 +273,7 @@ let print_namespace ns = acc ) constants (str"") in - Feedback.msg_notice ((print_list Id.print ns)++str":"++fnl()++constants_in_namespace) + (print_list Id.print ns)++str":"++fnl()++constants_in_namespace let print_strategy r = let open Conv_oracle in @@ -302,7 +303,7 @@ let print_strategy r = else str "Constant strategies" ++ fnl () ++ hov 0 (prlist_with_sep fnl pr_strategy cst_lvl) in - Feedback.msg_notice (var_msg ++ cst_msg) + var_msg ++ cst_msg | Some r -> let r = Smartlocate.smart_global r in let key = match r with @@ -311,7 +312,7 @@ let print_strategy r = | IndRef _ | ConstructRef _ -> user_err Pp.(str "The reference is not unfoldable") in let lvl = get_strategy oracle key in - Feedback.msg_notice (pr_strategy (r, lvl)) + pr_strategy (r, lvl) let dump_universes_gen g s = let output = open_out s in @@ -345,7 +346,7 @@ let dump_universes_gen g s = try UGraph.dump_universes output_constraint g; close (); - Feedback.msg_info (str "Universes written to file \"" ++ str s ++ str "\".") + str "Universes written to file \"" ++ str s ++ str "\"." with reraise -> let reraise = CErrors.push reraise in close (); @@ -360,12 +361,9 @@ let locate_file f = let msg_found_library = function | Library.LibLoaded, fulldir, file -> - Feedback.msg_info (hov 0 - (DirPath.print fulldir ++ strbrk " has been loaded from file " ++ - str file)) + hov 0 (DirPath.print fulldir ++ strbrk " has been loaded from file " ++ str file) | Library.LibInPath, fulldir, file -> - Feedback.msg_info (hov 0 - (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file)) + hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file) let err_unmapped_library ?loc ?from qid = let dir = fst (repr_qualid qid) in @@ -944,7 +942,6 @@ let vernac_chdir = function end; Flags.if_verbose Feedback.msg_info (str (Sys.getcwd())) - (********************) (* State management *) @@ -1595,9 +1592,9 @@ let vernac_check_may_eval ~atts redexp glopt rc = let evars_of_term c = Evarutil.undefined_evars_of_term sigma' c in let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma' j.Environ.uj_type } in - Feedback.msg_notice (print_judgment env sigma' j ++ - pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ - Printer.pr_universe_ctx_set sigma uctx) + print_judgment env sigma' j ++ + pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ + Printer.pr_universe_ctx_set sigma uctx | Some r -> let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in let redfun env evm c = @@ -1605,7 +1602,7 @@ let vernac_check_may_eval ~atts redexp glopt rc = let (_, c) = redfun env evm c in c in - Feedback.msg_notice (print_eval redfun env sigma' rc j) + print_eval redfun env sigma' rc j let vernac_declare_reduction ~atts s r = let local = make_locality atts.locality in @@ -1621,8 +1618,8 @@ let vernac_global_check c = let senv = Safe_typing.push_context_set false uctx senv in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in - Feedback.msg_notice (print_safe_judgment env sigma j ++ - pr_universe_ctx_set sigma uctx) + print_safe_judgment env sigma j ++ + pr_universe_ctx_set sigma uctx let get_nth_goal n = @@ -1630,7 +1627,7 @@ let get_nth_goal n = let gls,_,_,_,sigma = Proof.proof pf in let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in gl - + exception NoHyp (* Printing "About" information of a hypothesis of the current goal. We only print the type and a small statement to this comes from the @@ -1664,31 +1661,32 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt = print_about env sigma ref_or_by_not udecl let vernac_print ~atts env sigma = - let open Feedback in let loc = atts.loc in function - | PrintTables -> msg_notice (print_tables ()) - | PrintFullContext-> msg_notice (print_full_context_typ env sigma) - | PrintSectionContext qid -> msg_notice (print_sec_context_typ env sigma qid) - | PrintInspect n -> msg_notice (inspect env sigma n) - | PrintGrammar ent -> msg_notice (Metasyntax.pr_grammar ent) - | PrintLoadPath dir -> (* For compatibility ? *) msg_notice (print_loadpath dir) - | PrintModules -> msg_notice (print_modules ()) + | PrintTables -> print_tables () + | PrintFullContext-> print_full_context_typ env sigma + | PrintSectionContext qid -> print_sec_context_typ env sigma qid + | PrintInspect n -> inspect env sigma n + | PrintGrammar ent -> Metasyntax.pr_grammar ent + | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir + | PrintModules -> print_modules () | PrintModule qid -> print_module qid | PrintModuleType qid -> print_modtype qid | PrintNamespace ns -> print_namespace ns - | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ()) - | PrintMLModules -> msg_notice (Mltop.print_ml_modules ()) - | PrintDebugGC -> msg_notice (Mltop.print_gc ()) - | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl) - | PrintGraph -> msg_notice (Prettyp.print_graph env sigma) - | PrintClasses -> msg_notice (Prettyp.print_classes()) - | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses()) - | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c)) - | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma) + | PrintMLLoadPath -> Mltop.print_ml_path () + | PrintMLModules -> Mltop.print_ml_modules () + | PrintDebugGC -> Mltop.print_gc () + | PrintName (qid,udecl) -> + dump_global qid; + print_name env sigma qid udecl + | PrintGraph -> Prettyp.print_graph env sigma + | PrintClasses -> Prettyp.print_classes() + | PrintTypeClasses -> Prettyp.print_typeclasses() + | PrintInstances c -> Prettyp.print_instances (smart_global c) + | PrintCoercions -> Prettyp.print_coercions env sigma | PrintCoercionPaths (cls,clt) -> - msg_notice (Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt)) - | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma) + Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt) + | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma | PrintUniverses (b, dst) -> let univ = Global.universes () in let univ = if b then UGraph.sort_universes univ else univ in @@ -1697,23 +1695,24 @@ let vernac_print ~atts env sigma = else str"There may remain asynchronous universe constraints" in begin match dst with - | None -> msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) + | None -> UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining | Some s -> dump_universes_gen univ s end - | PrintHint r -> msg_notice (Hints.pr_hint_ref env sigma (smart_global r)) - | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) - | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name env sigma s) - | PrintHintDb -> msg_notice (Hints.pr_searchtable env sigma) + | PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r) + | PrintHintGoal -> Hints.pr_applicable_hint () + | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s + | PrintHintDb -> Hints.pr_searchtable env sigma | PrintScopes -> - msg_notice (Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env))) + Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env)) | PrintScope s -> - msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s) + Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s | PrintVisibility s -> - msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s) + Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s | PrintAbout (ref_or_by_not,udecl,glnumopt) -> - msg_notice (print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt) + print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt | PrintImplicit qid -> - dump_global qid; msg_notice (print_impargs qid) + dump_global qid; + print_impargs qid | PrintAssumptions (o,t,r) -> (* Prints all the axioms and section variables used by a term *) let gr = smart_global r in @@ -1721,7 +1720,7 @@ let vernac_print ~atts env sigma = let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in let nassums = Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in - msg_notice (Printer.pr_assumptionset env sigma nassums) + Printer.pr_assumptionset env sigma nassums | PrintStrategy r -> print_strategy r let global_module r = @@ -1807,19 +1806,18 @@ let vernac_search ~atts s gopt r = | SearchAbout sl -> (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r |> Search.prioritize_search) pr_search -let vernac_locate = let open Feedback in function - | LocateAny (AN qid) -> msg_notice (print_located_qualid qid) - | LocateTerm (AN qid) -> msg_notice (print_located_term qid) +let vernac_locate = function + | LocateAny (AN qid) -> print_located_qualid qid + | LocateTerm (AN qid) -> print_located_term qid | LocateAny (ByNotation (_, (ntn, sc))) (** TODO : handle Ltac notations *) | LocateTerm (ByNotation (_, (ntn, sc))) -> let _, env = Pfedit.get_current_context () in - msg_notice - (Notation.locate_notation - (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc) + Notation.locate_notation + (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc | LocateLibrary qid -> print_located_library qid - | LocateModule qid -> msg_notice (print_located_module qid) - | LocateOther (s, qid) -> msg_notice (print_located_other s qid) - | LocateFile f -> msg_notice (locate_file f) + | LocateModule qid -> print_located_module qid + | LocateOther (s, qid) -> print_located_other s qid + | LocateFile f -> locate_file f let vernac_register id r = if Proof_global.there_are_pending_proofs () then @@ -1851,7 +1849,7 @@ let vernac_unfocus () = let vernac_unfocused () = let p = Proof_global.give_me_the_proof () in if Proof.unfocused p then - Feedback.msg_notice (str"The proof is indeed fully unfocused.") + str"The proof is indeed fully unfocused." else user_err Pp.(str "The proof is not fully unfocused.") @@ -1878,21 +1876,20 @@ let vernac_bullet (bullet : Proof_bullet.t) = Proof_global.simple_with_current_proof (fun _ p -> Proof_bullet.put p bullet) -let vernac_show = let open Feedback in function +let vernac_show = function | ShowScript -> assert false (* Only the stm knows the script *) | ShowGoal goalref -> let proof = Proof_global.give_me_the_proof () in - let info = match goalref with - | OpenSubgoals -> pr_open_subgoals ~proof - | NthGoal n -> pr_nth_open_subgoal ~proof n - | GoalId id -> pr_goal_by_id ~proof id - in - msg_notice info + begin match goalref with + | OpenSubgoals -> pr_open_subgoals ~proof + | NthGoal n -> pr_nth_open_subgoal ~proof n + | GoalId id -> pr_goal_by_id ~proof id + end | ShowProof -> show_proof () | ShowExistentials -> show_top_evars () | ShowUniverses -> show_universes () | ShowProofNames -> - msg_notice (pr_sequence Id.print (Proof_global.get_all_proof_names())) + pr_sequence Id.print (Proof_global.get_all_proof_names()) | ShowIntros all -> show_intro all | ShowMatch id -> show_match id @@ -1907,8 +1904,7 @@ let vernac_check_guard () = (str "The condition holds up to here") with UserError(_,s) -> (str ("Condition violated: ") ++s) - in - Feedback.msg_notice message + in message exception End_of_input @@ -2063,26 +2059,32 @@ let interp ?proof ~atts ~st c = | VernacAddOption (key,v) -> vernac_add_option key v | VernacMemOption (key,v) -> vernac_mem_option key v | VernacPrintOption key -> vernac_print_option key - | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ~atts r g c + | VernacCheckMayEval (r,g,c) -> + Feedback.msg_notice @@ vernac_check_may_eval ~atts r g c | VernacDeclareReduction (s,r) -> vernac_declare_reduction ~atts s r - | VernacGlobalCheck c -> vernac_global_check c + | VernacGlobalCheck c -> + Feedback.msg_notice @@ vernac_global_check c | VernacPrint p -> let sigma, env = Pfedit.get_current_context () in - vernac_print ~atts env sigma p + Feedback.msg_notice @@ vernac_print ~atts env sigma p | VernacSearch (s,g,r) -> vernac_search ~atts s g r - | VernacLocate l -> vernac_locate l + | VernacLocate l -> + Feedback.msg_notice @@ vernac_locate l | VernacRegister (id, r) -> vernac_register id r | VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n") (* Proof management *) | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () - | VernacUnfocused -> vernac_unfocused () + | VernacUnfocused -> + Feedback.msg_notice @@ vernac_unfocused () | VernacBullet b -> vernac_bullet b | VernacSubproof n -> vernac_subproof n | VernacEndSubproof -> vernac_end_subproof () - | VernacShow s -> vernac_show s - | VernacCheckGuard -> vernac_check_guard () + | VernacShow s -> + Feedback.msg_notice @@ vernac_show s + | VernacCheckGuard -> + Feedback.msg_notice @@ vernac_check_guard () | VernacProof (tac, using) -> let using = Option.append using (Proof_using.get_default_proof_using ()) in let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in @@ -2277,8 +2279,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = then Flags.verbosely control c else control c -(* XXX: There is a bug here in case of an exception, see @gares - comments on the PR *) +(* Be careful with the cache here in case of an exception. *) let interp ?verbosely ?proof ~st cmd = Vernacstate.unfreeze_interp_state st; try |