diff options
39 files changed, 498 insertions, 225 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index f2df99dcd6..d20eea7874 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -142,8 +142,12 @@ let check_inductive env mind mb = mind_universes; mind_variance; mind_private; mind_typing_flags; } = - (* Locally set the oracle for further typechecking *) - let env = Environ.set_oracle env mb.mind_typing_flags.conv_oracle in + (* Locally set typing flags for further typechecking *) + let mb_flags = mb.mind_typing_flags in + let env = Environ.set_typing_flags {env.env_typing_flags with check_guarded = mb_flags.check_guarded; + check_positive = mb_flags.check_positive; + check_universes = mb_flags.check_universes; + conv_oracle = mb_flags.conv_oracle} env in Indtypes.check_inductive env mind entry in let check = check mind in diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 62f72c8edc..a67945ae94 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -31,14 +31,31 @@ let pr_engagement env = | PredicativeSet -> str "Theory: Set is predicative" end -let is_ax _ cb = not (Declareops.constant_has_body cb) -let pr_ax env = - let axs = fold_constants (fun c ce acc -> if is_ax c ce then c::acc else acc) env [] in +let pr_assumptions ass axs = if axs = [] then - str "Axioms: <none>" + str ass ++ str ": <none>" else - hv 2 (str "Axioms:" ++ fnl() ++ prlist_with_sep fnl Constant.print axs) + hv 2 (str ass ++ str ":" ++ fnl() ++ prlist_with_sep fnl str axs) + +let pr_axioms env = + let csts = fold_constants (fun c cb acc -> if not (Declareops.constant_has_body cb) then Constant.to_string c :: acc else acc) env [] in + pr_assumptions "Axioms" csts + +let pr_type_in_type env = + let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_universes then Constant.to_string c :: acc else acc) env [] in + let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_universes then MutInd.to_string c :: acc else acc) env csts in + pr_assumptions "Constants/Inductives relying on type-in-type" csts + +let pr_unguarded env = + let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_guarded then Constant.to_string c :: acc else acc) env [] in + let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_guarded then MutInd.to_string c :: acc else acc) env csts in + pr_assumptions "Constants/Inductives relying on unsafe (co)fixpoints" csts + +let pr_nonpositive env = + let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in + pr_assumptions "Inductives whose positivity is assumed" inds + let print_context env = if !output_context then begin @@ -47,7 +64,10 @@ let print_context env = (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++ str"===============" ++ fnl() ++ fnl() ++ str "* " ++ hov 0 (pr_engagement env ++ fnl()) ++ fnl() ++ - str "* " ++ hov 0 (pr_ax env))); + str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++ + str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++ + str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++ + str "* " ++ hov 0 (pr_nonpositive env))) end let stats env = diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 9b41fbcb7a..09b8c48c15 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -17,9 +17,12 @@ let set_indirect_accessor f = indirect_accessor := f let check_constant_declaration env kn cb = Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn); - (* Locally set the oracle for further typechecking *) - let oracle = env.env_typing_flags.conv_oracle in - let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in + (* Locally set typing flags for further typechecking *) + let orig_flags = env.env_typing_flags in + let cb_flags = cb.const_typing_flags in + let env = Environ.set_typing_flags {orig_flags with check_guarded = cb_flags.check_guarded; + check_universes = cb_flags.check_universes; + conv_oracle = cb_flags.conv_oracle} env in (* [env'] contains De Bruijn universe variables *) let poly, env' = match cb.const_universes with @@ -57,8 +60,8 @@ let check_constant_declaration env kn cb = if poly then add_constant kn cb env else add_constant kn cb env' in - (* Reset the value of the oracle *) - Environ.set_oracle env oracle + (* Reset the value of the typing flags *) + Environ.set_typing_flags orig_flags env (** {6 Checking modules } *) diff --git a/checker/values.ml b/checker/values.ml index 8dc09aed87..ac9bc26344 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -219,7 +219,7 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 408d36df7f..9ed7180807 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -120,15 +120,18 @@ Currently available artifacts are: Additionally, an experimental Dune build is provided: https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune:dev -- the Coq documentation, built in the `doc:*` jobs. When submitting - a documentation PR, this can help reviewers checking the rendered result: - - + Coq's Reference Manual [master branch] - https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman - + Coq's Standard Library Documentation [master branch] - https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=build:base - + Coq's ML API Documentation [master branch] - https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc +- the Coq documentation, built in the `doc:*` jobs. When submitting a + documentation PR, this can help reviewers checking the rendered + result. **@coqbot** will automatically post links to these + artifacts in the PR checks section. Furthemore, these artifacts are + automatically deployed at: + + + Coq's Reference Manual [master branch]: + <https://coq.github.io/doc/master/refman/> + + Coq's Standard Library Documentation [master branch]: + <https://coq.github.io/doc/master/stdlib/> + + Coq's ML API Documentation [master branch]: + <https://coq.github.io/doc/master/api/> ### GitLab and Windows diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index ad22c394d8..3923fea30e 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -56,14 +56,14 @@ # NB: stdpp and Iris refs are gotten from the opam files in the Iris # and lambdaRust repos respectively. -: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}" +: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/iris/stdpp}" : "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}" -: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}" +: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}" : "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}" : "${lambdaRust_CI_REF:=master}" -: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq}" +: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}" : "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}" ######################################################################## diff --git a/doc/changelog/07-commands-and-options/10291-typing-flags.rst b/doc/changelog/07-commands-and-options/10291-typing-flags.rst new file mode 100644 index 0000000000..ef7adde801 --- /dev/null +++ b/doc/changelog/07-commands-and-options/10291-typing-flags.rst @@ -0,0 +1,4 @@ +- Adding unsafe commands to enable/disable guard checking, positivity checking + and universes checking (providing a local `-type-in-type`). + See :ref:`controlling-typing-flags`. + (`#10291 <https://github.com/coq/coq/pull/10291>`_ by Simon Boulier). diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 91dfa34494..2cbd41af8b 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -778,7 +778,8 @@ Simple inductive types The types of the constructors have to satisfy a *positivity condition* (see Section :ref:`positivity`). This condition ensures the soundness of - the inductive definition. + the inductive definition. The positivity checking can be disabled using + the option :flag:`Positivity Checking` (see :ref:`controlling-typing-flags`). .. exn:: The conclusion of @type is not valid; it must be built from @ident. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 774732825a..c391cc949d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1204,6 +1204,79 @@ Controlling the locality of commands occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. +.. _controlling-typing-flags: + +Controlling Typing Flags +---------------------------- + +.. flag:: Guard Checking + + This option can be used to enable/disable the guard checking of + fixpoints. Warning: this can break the consistency of the system, use at your + own risk. Decreasing argument can still be specified: the decrease is not checked + anymore but it still affects the reduction of the term. Unchecked fixpoints are + printed by :cmd:`Print Assumptions`. + +.. flag:: Positivity Checking + + This option can be used to enable/disable the positivity checking of inductive + types and the productivity checking of coinductive types. Warning: this can + break the consistency of the system, use at your own risk. Unchecked + (co)inductive types are printed by :cmd:`Print Assumptions`. + +.. flag:: Universe Checking + + This option can be used to enable/disable the checking of universes, providing a + form of "type in type". Warning: this breaks the consistency of the system, use + at your own risk. Constants relying on "type in type" are printed by + :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line + argument (see :ref:`command-line-options`). + +.. cmd:: Print Typing Flags + + Print the status of the three typing flags: guard checking, positivity checking + and universe checking. + +.. example:: + + .. coqtop:: all reset + + Unset Guard Checking. + + Print Typing Flags. + + Fixpoint f (n : nat) : False + := f n. + + Fixpoint ackermann (m n : nat) {struct m} : nat := + match m with + | 0 => S n + | S m => + match n with + | 0 => ackermann m 1 + | S n => ackermann m (ackermann (S m) n) + end + end. + + Print Assumptions ackermann. + + Note that the proper way to define the Ackermann function is to use + an inner fixpoint: + + .. coqtop:: all reset + + Fixpoint ack m := + fix ackm n := + match m with + | 0 => S n + | S m' => + match n with + | 0 => ack m' 1 + | S n' => ack m' (ackm n') + end + end. + + .. _internal-registration-commands: Internal registration commands diff --git a/ide/idetop.ml b/ide/idetop.ml index 7c6fa8951b..7e55eb4d13 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -56,7 +56,7 @@ let coqide_known_option table = List.mem table [ ["Printing";"Unfocused"]; ["Diffs"]] -let is_known_option cmd = match Vernacprop.under_control cmd with +let is_known_option cmd = match cmd with | VernacSetOption (_, o, OptionSetTrue) | VernacSetOption (_, o, OptionSetString _) | VernacSetOption (_, o, OptionUnset) -> coqide_known_option o @@ -64,7 +64,7 @@ let is_known_option cmd = match Vernacprop.under_control cmd with (** Check whether a command is forbidden in the IDE *) -let ide_cmd_checks ~last_valid ({ CAst.loc; _ } as cmd) = +let ide_cmd_checks ~last_valid { CAst.loc; v } = let user_error s = try CErrors.user_err ?loc ~hdr:"IDE" (str s) with e -> @@ -72,14 +72,14 @@ let ide_cmd_checks ~last_valid ({ CAst.loc; _ } as cmd) = let info = Stateid.add info ~valid:last_valid Stateid.dummy in Exninfo.raise ~info e in - if is_debug cmd then + if is_debug v.expr then user_error "Debug mode not available in the IDE" -let ide_cmd_warns ~id ({ CAst.loc; _ } as cmd) = +let ide_cmd_warns ~id { CAst.loc; v } = let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in - if is_known_option cmd then + if is_known_option v.expr then warn "Set this option from the IDE menu instead"; - if is_navigation_vernac cmd || is_undo cmd then + if is_navigation_vernac v.expr || is_undo v.expr then warn "Use IDE navigation instead" (** Interpretation (cf. [Ide_intf.interp]) *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index dff19dee5e..8d32684b09 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -66,6 +66,10 @@ type typing_flags = { (** If [false] then fixed points and co-fixed points are assumed to be total. *) + check_positive : bool; + (** If [false] then inductive types are assumed positive and co-inductive + types are assumed productive. *) + check_universes : bool; (** If [false] universe constraints are not checked *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 7a553700e8..391b139496 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -19,6 +19,7 @@ module RelDecl = Context.Rel.Declaration let safe_flags oracle = { check_guarded = true; + check_positive = true; check_universes = true; conv_oracle = oracle; share_reduction = true; diff --git a/kernel/environ.ml b/kernel/environ.ml index 9a75f0b682..655094e88b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -216,6 +216,9 @@ let lookup_named_ctxt id ctxt = let fold_constants f env acc = Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc +let fold_inductives f env acc = + Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_inductives acc + (* Global constants *) let lookup_constant_key kn env = @@ -418,6 +421,7 @@ let set_engagement c env = (* Unsafe *) (* It's convenient to use [{flags with foo = bar}] so we're smart wrt to it. *) let same_flags { check_guarded; + check_positive; check_universes; conv_oracle; indices_matter; @@ -426,6 +430,7 @@ let same_flags { enable_native_compiler; } alt = check_guarded == alt.check_guarded && + check_positive == alt.check_positive && check_universes == alt.check_universes && conv_oracle == alt.conv_oracle && indices_matter == alt.indices_matter && diff --git a/kernel/environ.mli b/kernel/environ.mli index 6cd4f96645..e6d814ac7d 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -176,6 +176,7 @@ val pop_rel_context : int -> env -> env (** Useful for printing *) val fold_constants : (Constant.t -> Opaqueproof.opaque constant_body -> 'a -> 'a) -> env -> 'a -> 'a +val fold_inductives : (MutInd.t -> Declarations.mutual_inductive_body -> 'a -> 'a) -> env -> 'a -> 'a (** {5 Global constants } {6 Add entries to global environment } *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b0366d6ec0..aa3ef715db 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -546,7 +546,7 @@ let check_inductive env kn mie = (* First type-check the inductive definition *) let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in (* Then check positivity conditions *) - let chkpos = (Environ.typing_flags env).check_guarded in + let chkpos = (Environ.typing_flags env).check_positive in let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames) mie.mind_entry_inds in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ea45f699ce..6970a11e72 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -194,6 +194,18 @@ let set_typing_flags c senv = if env == senv.env then senv else { senv with env } +let set_check_guarded b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_guarded = b } senv + +let set_check_positive b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_positive = b } senv + +let set_check_universes b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_universes = b } senv + let set_indices_matter indices_matter senv = set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 2406b6add1..fa53fa33fa 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -130,6 +130,9 @@ val set_engagement : Declarations.engagement -> safe_transformer0 val set_indices_matter : bool -> safe_transformer0 val set_typing_flags : Declarations.typing_flags -> safe_transformer0 val set_share_reduction : bool -> safe_transformer0 +val set_check_guarded : bool -> safe_transformer0 +val set_check_positive : bool -> safe_transformer0 +val set_check_universes : bool -> safe_transformer0 val set_VM : bool -> safe_transformer0 val set_native_compiler : bool -> safe_transformer0 val make_sprop_cumulative : safe_transformer0 diff --git a/library/global.ml b/library/global.ml index ca774dbd74..0fc9e11364 100644 --- a/library/global.ml +++ b/library/global.ml @@ -89,6 +89,9 @@ let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) +let set_check_guarded c = globalize0 (Safe_typing.set_check_guarded c) +let set_check_positive c = globalize0 (Safe_typing.set_check_positive c) +let set_check_universes c = globalize0 (Safe_typing.set_check_universes c) let typing_flags () = Environ.typing_flags (env ()) let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) diff --git a/library/global.mli b/library/global.mli index d034bc4208..b089b7dd80 100644 --- a/library/global.mli +++ b/library/global.mli @@ -31,6 +31,9 @@ val named_context : unit -> Constr.named_context val set_engagement : Declarations.engagement -> unit val set_indices_matter : bool -> unit val set_typing_flags : Declarations.typing_flags -> unit +val set_check_guarded : bool -> unit +val set_check_positive : bool -> unit +val set_check_universes : bool -> unit val typing_flags : unit -> Declarations.typing_flags val make_sprop_cumulative : unit -> unit val set_allow_sprop : bool -> unit diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index d220058120..92a93489f4 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -180,7 +180,7 @@ let is_proof_termination_interactively_checked recsl = let classify_as_Fixpoint recsl = Vernac_classifier.classify_vernac - (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(NoDischarge, List.map snd recsl)))) + (Vernacexpr.(CAst.make @@ { control = []; attrs = []; expr = VernacFixpoint(NoDischarge, List.map snd recsl)})) let classify_funind recsl = match classify_as_Fixpoint recsl with diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 798c62d549..6eb8c42d1d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1517,7 +1517,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(CAst.make @@ VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)}) ++ fnl () ++ msg in @@ -1532,7 +1532,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(CAst.make @@ VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)}) ++ fnl () ++ CErrors.print reraise in diff --git a/printing/printer.ml b/printing/printer.ml index ec1b9b8e49..e3225fadd5 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -853,7 +853,8 @@ let pr_goal_emacs ~proof gid sid = type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) - | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) @@ -873,7 +874,7 @@ struct | Positive m1 , Positive m2 -> MutInd.CanOrd.compare m1 m2 | Guarded k1 , Guarded k2 -> - Constant.CanOrd.compare k1 k2 + GlobRef.Ordered.compare k1 k2 | _ , Constant _ -> 1 | _ , Positive _ -> 1 | _ -> -1 @@ -903,14 +904,20 @@ let pr_assumptionset env sigma s = let safe_pr_constant env kn = try pr_constant env kn with Not_found -> - (* FIXME? *) - let mp,lab = Constant.repr2 kn in - str (ModPath.to_string mp) ++ str "." ++ Label.print lab + Names.Constant.print kn + in + let safe_pr_global env gr = + try pr_global_env (Termops.vars_of_env env) gr + with Not_found -> + let open GlobRef in match gr with + | VarRef id -> Id.print id + | ConstRef con -> Constant.print con + | IndRef (mind,_) -> MutInd.print mind + | ConstructRef _ -> assert false in let safe_pr_inductive env kn = try pr_inductive env (kn,0) with Not_found -> - (* FIXME? *) MutInd.print kn in let safe_pr_ltype env sigma typ = @@ -927,9 +934,11 @@ let pr_assumptionset env sigma s = | Constant kn -> safe_pr_constant env kn ++ safe_pr_ltype env sigma typ | Positive m -> - hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.") - | Guarded kn -> - hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.") + hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.") + | Guarded gr -> + hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.") + | TypeInType gr -> + hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.") in let fold t typ accu = let (v, a, o, tr) = accu in @@ -1003,3 +1012,8 @@ let print_and_diff oldp newp = pr_open_subgoals ~proof in Feedback.msg_notice output;; + +let pr_typing_flags flags = + str "check_guarded: " ++ bool flags.check_guarded ++ fnl () + ++ str "check_positive: " ++ bool flags.check_positive ++ fnl () + ++ str "check_universes: " ++ bool flags.check_universes diff --git a/printing/printer.mli b/printing/printer.mli index a72f319636..788f303aee 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -191,7 +191,8 @@ val print_and_diff : Proof.t option -> Proof.t option -> unit type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) - | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) @@ -207,3 +208,5 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t + +val pr_typing_flags : Declarations.typing_flags -> Pp.t diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 129444c3b3..a487799b74 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -77,17 +77,18 @@ include Util (* ****************** - foo - bar - baz *********************************** *) let static_bullet ({ entry_point; prev_node } as view) = + let open Vernacexpr in assert (not (Vernacprop.has_Fail entry_point.ast)); - match Vernacprop.under_control entry_point.ast with - | Vernacexpr.VernacBullet b -> + match entry_point.ast.CAst.v.expr with + | VernacBullet b -> let base = entry_point.indentation in let last_tac = prev_node entry_point in crawl view ~init:last_tac (fun prev node -> if node.indentation < base then `Stop else if node.indentation > base then `Cont node else if Vernacprop.has_Fail node.ast then `Stop - else match Vernacprop.under_control node.ast with - | Vernacexpr.VernacBullet b' when b = b' -> + else match node.ast.CAst.v.expr with + | VernacBullet b' when b = b' -> `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = of_bullet_val b } | _ -> `Stop) entry_point @@ -99,7 +100,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b))) + recovery_command = Some (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacBullet (to_bullet_val b)}) } | `Not -> `Leaks @@ -109,16 +110,17 @@ let () = register_proof_block_delimiter (* ******************** { block } ***************************************** *) let static_curly_brace ({ entry_point; prev_node } as view) = - assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof); + let open Vernacexpr in + assert(entry_point.ast.CAst.v.expr = VernacEndSubproof); crawl view (fun (nesting,prev) node -> if Vernacprop.has_Fail node.ast then `Cont (nesting,node) - else match Vernacprop.under_control node.ast with - | Vernacexpr.VernacSubproof _ when nesting = 0 -> + else match node.ast.CAst.v.expr with + | VernacSubproof _ when nesting = 0 -> `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = unit_val } - | Vernacexpr.VernacSubproof _ -> + | VernacSubproof _ -> `Cont (nesting - 1,node) - | Vernacexpr.VernacEndSubproof -> + | VernacEndSubproof -> `Cont (nesting + 1,node) | _ -> `Cont (nesting,node)) (-1, entry_point) @@ -128,7 +130,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof)) + recovery_command = Some (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacEndSubproof }) } | `Not -> `Leaks diff --git a/stm/stm.ml b/stm/stm.ml index 69dbebbc57..7f0632bd7c 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -571,7 +571,7 @@ end = struct (* {{{ *) vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch let reachable id = reachable !vcs id let mk_branch_name { expr = x } = Branch.make - (match Vernacprop.under_control x with + (match x.CAst.v.Vernacexpr.expr with | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i | VernacInstance (({CAst.v=Name i},_),_,_,_,_) -> Id.to_string i @@ -1054,9 +1054,9 @@ end = struct (* {{{ *) end (* }}} *) (* Wrapper for the proof-closing special path for Qed *) -let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc pending : Vernacstate.t = +let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc ~control pending : Vernacstate.t = set_id_for_feedback ?route dummy_doc id; - Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ?loc:loc pending + Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending) (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly @@ -1078,7 +1078,7 @@ let stm_vernac_interp ?route id st { verbose; expr } : Vernacstate.t = | _ -> false in (* XXX unsupported attributes *) - let cmd = Vernacprop.under_control expr in + let cmd = expr.CAst.v.expr in if is_filtered_command cmd then (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) else begin @@ -1141,7 +1141,7 @@ end = struct (* {{{ *) | { step = `Fork ((_,_,_,l),_) } -> l, false,0 | { step = `Cmd { cids = l; ctac } } -> l, ctac,0 | { step = `Alias (_,{ expr }) } when not (Vernacprop.has_Fail expr) -> - begin match Vernacprop.under_control expr with + begin match expr.CAst.v.expr with | VernacUndo n -> [], false, n | _ -> [],false,0 end @@ -1171,7 +1171,7 @@ end = struct (* {{{ *) if not (VCS.is_interactive ()) && !cur_opt.async_proofs_cache <> Some Force then undo_costly_in_batch_mode v; try - match Vernacprop.under_control v with + match v.CAst.v.expr with | VernacResetInitial -> Stateid.initial | VernacResetName {CAst.v=name} -> @@ -1532,7 +1532,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_qed_delay_proof ~st ~id:stop - ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc (Proved (opaque,None))) in + ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1683,7 +1683,7 @@ end = struct (* {{{ *) *) (* STATE We use the state resulting from reaching start. *) let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc (Proved (opaque,None))); + ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None))); `OK proof end with e -> @@ -1977,13 +1977,14 @@ end = struct (* {{{ *) let vernac_interp ~solve ~abstract ~cancel_switch nworkers priority safe_id id { indentation; verbose; expr = e; strlen } : unit = - let e, time, batch, fail = - let rec find ~time ~batch ~fail v = CAst.with_loc_val (fun ?loc -> function - | VernacTime (batch,e) -> find ~time:true ~batch ~fail e - | VernacRedirect (_,e) -> find ~time ~batch ~fail e - | VernacFail e -> find ~time ~batch ~fail:true e - | e -> CAst.make ?loc e, time, batch, fail) v in - find ~time:false ~batch:false ~fail:false e in + let cl, time, batch, fail = + let rec find ~time ~batch ~fail cl = match cl with + | ControlTime batch :: cl -> find ~time:true ~batch ~fail cl + | ControlRedirect _ :: cl -> find ~time ~batch ~fail cl + | ControlFail :: cl -> find ~time ~batch ~fail:true cl + | cl -> cl, time, batch, fail in + find ~time:false ~batch:false ~fail:false e.CAst.v.control in + let e = CAst.map (fun cmd -> { cmd with control = cl }) e in let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_fail ~st fail (fun () -> (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> @@ -2151,14 +2152,14 @@ let collect_proof keep cur hd brkind id = | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true | _ -> false in let is_defined = function - | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e) + | _, { expr = e } -> is_defined_expr e.CAst.v.expr && (not (Vernacprop.has_Fail e)) in let proof_using_ast = function | VernacProof(_,Some _) -> true | _ -> false in let proof_using_ast = function - | Some (_, v) when proof_using_ast (Vernacprop.under_control v.expr) + | Some (_, v) when proof_using_ast v.expr.CAst.v.expr && (not (Vernacprop.has_Fail v.expr)) -> Some v | _ -> None in let has_proof_using x = proof_using_ast x <> None in @@ -2167,14 +2168,14 @@ let collect_proof keep cur hd brkind id = | _ -> assert false in let proof_no_using = function - | Some (_, v) -> proof_no_using (Vernacprop.under_control v.expr), v + | Some (_, v) -> proof_no_using v.expr.CAst.v.expr, v | _ -> assert false in let has_proof_no_using = function | VernacProof(_,None) -> true | _ -> false in let has_proof_no_using = function - | Some (_, v) -> has_proof_no_using (Vernacprop.under_control v.expr) + | Some (_, v) -> has_proof_no_using v.expr.CAst.v.expr && (not (Vernacprop.has_Fail v.expr)) | _ -> false in let too_complex_to_delegate = function @@ -2191,7 +2192,7 @@ let collect_proof keep cur hd brkind id = let view = VCS.visit id in match view.step with | (`Sideff (ReplayCommand x,_) | `Cmd { cast = x }) - when too_complex_to_delegate (Vernacprop.under_control x.expr) -> + when too_complex_to_delegate x.expr.CAst.v.expr -> `Sync(no_name,`Print) | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next | `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next @@ -2212,7 +2213,7 @@ let collect_proof keep cur hd brkind id = (try let name, hint = name ids, get_hint_ctx loc in let t, v = proof_no_using last in - v.expr <- CAst.map (fun _ -> VernacExpr([], VernacProof(t, Some hint))) v.expr; + v.expr <- CAst.map (fun _ -> { control = []; attrs = []; expr = VernacProof(t, Some hint)}) v.expr; `ASync (parent last,accn,name,delegate name) with Not_found -> let name = name ids in @@ -2235,7 +2236,7 @@ let collect_proof keep cur hd brkind id = | _ -> false in match cur, (VCS.visit id).step, brkind with - | (parent, x), `Fork _, _ when is_vernac_exact (Vernacprop.under_control x.expr) + | (parent, x), `Fork _, _ when is_vernac_exact x.expr.CAst.v.expr && (not (Vernacprop.has_Fail x.expr)) -> `Sync (no_name,`Immediate) | _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id) @@ -2350,8 +2351,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = term.` could also fail in this case, however that'd be a bug I do believe as proof injection shouldn't happen here. *) let extract_pe (x : aast) = - match Vernacprop.under_control x.expr with - | VernacEndProof pe -> pe + match x.expr.CAst.v.expr with + | VernacEndProof pe -> x.expr.CAst.v.control, pe | _ -> CErrors.anomaly Pp.(str "Non-qed command classified incorrectly") in (* ugly functions to process nested lemmas, i.e. hard to reproduce @@ -2486,7 +2487,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = if not delegate then ignore(Future.compute fp); reach view.next; let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc (extract_pe x)); + let control, pe = extract_pe x in + ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe); feedback ~id:id Incomplete | { VCS.kind = `Master }, _ -> assert false end; @@ -2526,7 +2528,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let _st = match proof with | None -> stm_vernac_interp id st x | Some (proof, info) -> - stm_qed_delay_proof ~id ~st ~proof ~info ~loc (extract_pe x) + let control, pe = extract_pe x in + stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe in let wall_clock3 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc:x.expr.CAst.loc "proof_check_time" @@ -2873,7 +2876,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) let queue = if VCS.is_vio_doc () && VCS.((get_branch head).kind = `Master) && - may_pierce_opaque (Vernacprop.under_control x.expr) + may_pierce_opaque x.expr.CAst.v.expr then `SkipQueue else `MainQueue in VCS.commit id (mkTransCmd x [] false queue); @@ -2939,7 +2942,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) VCS.commit id (mkTransCmd x l true `MainQueue); (* We can't replay a Definition since universes may be differently * inferred. This holds in Coq >= 8.5 *) - let action = match Vernacprop.under_control x.expr with + let action = match x.expr.CAst.v.expr with | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv | _ -> ReplayCommand x in VCS.propagate_sideff ~action diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 5af576dad2..8d600c2859 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -202,18 +202,17 @@ let classify_vernac e = try Vernacextend.get_vernac_classifier s l with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in - let rec static_control_classifier v = v |> CAst.with_val (function - | VernacExpr (atts, e) -> - static_classifier ~atts e - | VernacTimeout (_,e) -> static_control_classifier e - | VernacTime (_,e) | VernacRedirect (_, e) -> - static_control_classifier e - | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) - (* XXX why is Fail not always Query? *) - (match static_control_classifier e with + let static_control_classifier ({ CAst.v ; _ } as cmd) = + (* Fail Qed or Fail Lemma must not join/fork the DAG *) + (* XXX why is Fail not always Query? *) + if Vernacprop.has_Fail cmd then + (match static_classifier ~atts:v.attrs v.expr with | VtQuery | VtProofStep _ | VtSideff _ | VtMeta as x -> x | VtQed _ -> VtProofStep { parallel = `No; proof_block_detection = None } - | VtStartProof _ | VtProofMode _ -> VtQuery)) + | VtStartProof _ | VtProofMode _ -> VtQuery) + else + static_classifier ~atts:v.attrs v.expr + in static_control_classifier e diff --git a/tactics/declare.ml b/tactics/declare.ml index e093a27728..391524ebda 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -246,7 +246,7 @@ let get_roles export eff = let feedback_axiom () = Feedback.(feedback AddedAxiom) let is_unsafe_typing_flags () = let flags = Environ.typing_flags (Global.env()) in - not (flags.check_universes && flags.check_guarded) + not (flags.check_universes && flags.check_guarded && flags.check_positive) let define_constant ~side_effect ~name cd = let open Proof_global in diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v new file mode 100644 index 0000000000..bd20d9c804 --- /dev/null +++ b/test-suite/success/typing_flags.v @@ -0,0 +1,43 @@ + +Print Typing Flags. +Unset Guard Checking. +Fixpoint f' (n : nat) : nat := f' n. + +Fixpoint f (n : nat) : nat. +Proof. + exact (f n). +Defined. + +Fixpoint bla (A:Type) (n:nat) := match n with 0 =>0 | S n => n end. + +Print Typing Flags. + +Set Guard Checking. + +Print Assumptions f. + +Unset Universe Checking. + +Definition T := Type. +Fixpoint g (n : nat) : T := T. + +Print Typing Flags. +Set Universe Checking. + +Fail Definition g2 (n : nat) : T := T. + +Fail Definition e := fix e (n : nat) : nat := e n. + +Unset Positivity Checking. + +Inductive Cor := +| Over : Cor +| Next : ((Cor -> list nat) -> list nat) -> Cor. + +Set Positivity Checking. +Print Assumptions Cor. + +Inductive Box := +| box : forall n, f n = n -> g 2 -> Box. + +Print Assumptions Box. diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index f37feb24de..78640334e2 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -340,8 +340,8 @@ let print_anyway_opts = [ let print_anyway c = let open Vernacexpr in - match c with - | VernacExpr (_, VernacSetOption (_, opt, _)) -> List.mem opt print_anyway_opts + match c.expr with + | VernacSetOption (_, opt, _) -> List.mem opt print_anyway_opts | _ -> false (* We try to behave better when goal printing raises an exception diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7a59a4dd12..e9d8263b85 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -20,14 +20,10 @@ open Vernacprop Use the module Coqtoplevel, which catches these exceptions (the exceptions are explained only at the toplevel). *) -let checknav_simple ({ CAst.loc; _ } as cmd) = - if is_navigation_vernac cmd && not (is_reset cmd) then +let checknav { CAst.loc; v = { expr } } = + if is_navigation_vernac expr && not (is_reset expr) then CErrors.user_err ?loc (str "Navigation commands forbidden in files.") -let checknav_deep ({ CAst.loc; _ } as cmd) = - if is_deep_navigation_vernac cmd then - CErrors.user_err ?loc (str "Navigation commands forbidden in nested commands.") - (* Echo from a buffer based on position. XXX: Should move to utility file. *) let vernac_echo ?loc in_chan = let open Loc in @@ -60,7 +56,7 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = due to the way it prints. *) let com = if state.time then begin - CAst.make ?loc @@ VernacTime(state.time,com) + CAst.map (fun cmd -> { cmd with control = ControlTime state.time :: cmd.control }) com end else com in let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in @@ -108,7 +104,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file = (* Printing of AST for -compile-verbose *) Option.iter (vernac_echo ?loc:ast.CAst.loc) in_echo; - checknav_simple ast; + checknav ast; let state = Flags.silently (interp_vernac ~check ~interactive ~state) ast in @@ -122,7 +118,6 @@ let load_vernac_core ~echo ~check ~interactive ~state file = iraise (e, info) let process_expr ~state loc_ast = - checknav_deep loc_ast; interp_vernac ~interactive:true ~check:true ~state loc_ast (******************************************************************************) diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index ab341e4ab8..a72e43de01 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -313,9 +313,15 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = if cb.const_typing_flags.check_guarded then accu else let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in - ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu + ContextObjectMap.add (Axiom (Guarded obj, l)) Constr.mkProp accu in - if not (Declareops.constant_has_body cb) || not cb.const_typing_flags.check_universes then + let accu = + if cb.const_typing_flags.check_universes then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu + in + if not (Declareops.constant_has_body cb) then let t = type_of_constant cb in let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (Constant kn,l)) t accu @@ -329,10 +335,24 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = accu | IndRef (m,_) | ConstructRef ((m,_),_) -> let mind = lookup_mind m in - if mind.mind_typing_flags.check_guarded then - accu - else - let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in - ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu - in - GlobRef.Map_env.fold fold graph ContextObjectMap.empty + let accu = + if mind.mind_typing_flags.check_positive then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu + in + let accu = + if mind.mind_typing_flags.check_guarded then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (Guarded obj, l)) Constr.mkProp accu + in + let accu = + if mind.mind_typing_flags.check_universes then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu + in + accu + + in GlobRef.Map_env.fold fold graph ContextObjectMap.empty diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index dcd1979a85..8a94a010a0 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -72,16 +72,29 @@ let parse_compat_version = let open Flags in function CErrors.user_err ~hdr:"get_compat_version" Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") +(* For now we just keep the top-level location of the whole + vernacular, that is to say, including attributes and control flags; + this is not very convenient for advanced clients tho, so in the + future it'd be cool to actually locate the attributes and control + flags individually too. *) +let add_control_flag ~loc ~flag { CAst.v = cmd } = + CAst.make ~loc { cmd with control = flag :: cmd.control } + } GRAMMAR EXTEND Gram GLOBAL: vernac_control quoted_attributes gallina_ext noedit_mode subprf; vernac_control: FIRST - [ [ IDENT "Time"; c = vernac_control -> { CAst.make ~loc @@ VernacTime (false,c) } - | IDENT "Redirect"; s = ne_string; c = vernac_control -> { CAst.make ~loc @@ VernacRedirect (s, c) } - | IDENT "Timeout"; n = natural; v = vernac_control -> { CAst.make ~loc @@ VernacTimeout(n,v) } - | IDENT "Fail"; v = vernac_control -> { CAst.make ~loc @@ VernacFail v } - | v = decorated_vernac -> { let (f, v) = v in CAst.make ~loc @@ VernacExpr(f, v) } ] + [ [ IDENT "Time"; c = vernac_control -> + { add_control_flag ~loc ~flag:(ControlTime false) c } + | IDENT "Redirect"; s = ne_string; c = vernac_control -> + { add_control_flag ~loc ~flag:(ControlRedirect s) c } + | IDENT "Timeout"; n = natural; c = vernac_control -> + { add_control_flag ~loc ~flag:(ControlTimeout n) c } + | IDENT "Fail"; c = vernac_control -> + { add_control_flag ~loc ~flag:ControlFail c } + | v = decorated_vernac -> + { let (attrs, expr) = v in CAst.make ~loc { control = []; attrs; expr = expr } } ] ] ; decorated_vernac: @@ -1035,6 +1048,7 @@ GRAMMAR EXTEND Gram | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> { PrintCoercionPaths (s,t) } | IDENT "Canonical"; IDENT "Projections" -> { PrintCanonicalConversions } + | IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags } | IDENT "Tables" -> { PrintTables } | IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) } | IDENT "Hint" -> { PrintHintGoal } diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 23a8bf20a3..cf87646905 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -553,7 +553,7 @@ let declare_default_schemes kn = let mib = Global.lookup_mind kn in let n = Array.length mib.mind_packets in if !elim_flag && (mib.mind_finite <> Declarations.BiFinite || !bifinite_elim_flag) - && mib.mind_typing_flags.check_guarded then + && mib.mind_typing_flags.check_positive then declare_induction_schemes kn; if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n; if is_eq_flag() then try_declare_beq_scheme kn; diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 0eb0b1b6f6..f91983d31c 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -514,6 +514,8 @@ let string_of_theorem_kind = let open Decls in function ++ pr_class_rawexpr t | PrintCanonicalConversions -> keyword "Print Canonical Structures" + | PrintTypingFlags -> + keyword "Print Typing Flags" | PrintTables -> keyword "Print Tables" | PrintHintGoal -> @@ -1266,6 +1268,16 @@ let string_of_definition_object_kind = let open Decls in function | VernacEndSubproof -> return (str "}") +let pr_control_flag (p : control_flag) = + let w = match p with + | ControlTime _ -> keyword "Time" + | ControlRedirect s -> keyword "Redirect" ++ spc() ++ qs s + | ControlTimeout n -> keyword "Timeout " ++ int n + | ControlFail -> keyword "Fail" in + w ++ spc () + +let pr_vernac_control flags = Pp.prlist pr_control_flag flags + let rec pr_vernac_flag (k, v) = let k = keyword k in let open Attributes in @@ -1281,19 +1293,11 @@ let pr_vernac_attributes = | [] -> mt () | flags -> str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut () - let rec pr_vernac_control v = - let return = tag_vernac v in - match v.v with - | VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v' - | VernacTime (_,v) -> - return (keyword "Time" ++ spc() ++ pr_vernac_control v) - | VernacRedirect (s, v) -> - return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v) - | VernacTimeout(n,v) -> - return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v) - | VernacFail v-> - return (keyword "Fail" ++ spc() ++ pr_vernac_control v) - - let pr_vernac v = - try pr_vernac_control v - with e -> CErrors.print e +let pr_vernac ({v = {control; attrs; expr}} as v) = + try + tag_vernac v + (pr_vernac_control control ++ + pr_vernac_attributes attrs ++ + pr_vernac_expr expr ++ + sep_end expr) + with e -> CErrors.print e diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index bc51dd46f3..4ae9d6d54f 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1724,6 +1724,30 @@ let () = optread = Nativenorm.get_profiling_enabled; optwrite = Nativenorm.set_profiling_enabled } +let _ = + declare_bool_option + { optdepr = false; + optname = "guard checking"; + optkey = ["Guard"; "Checking"]; + optread = (fun () -> (Global.typing_flags ()).Declarations.check_guarded); + optwrite = (fun b -> Global.set_check_guarded b) } + +let _ = + declare_bool_option + { optdepr = false; + optname = "positivity/productivity checking"; + optkey = ["Positivity"; "Checking"]; + optread = (fun () -> (Global.typing_flags ()).Declarations.check_positive); + optwrite = (fun b -> Global.set_check_positive b) } + +let _ = + declare_bool_option + { optdepr = false; + optname = "universes checking"; + optkey = ["Universe"; "Checking"]; + optread = (fun () -> (Global.typing_flags ()).Declarations.check_universes); + optwrite = (fun b -> Global.set_check_universes b) } + let vernac_set_strategy ~local l = let local = Option.default false local in let glob_ref r = @@ -1928,6 +1952,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = let vernac_print ~pstate ~atts = let sigma, env = get_current_or_global_context ~pstate in function + | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ())) | PrintTables -> print_tables () | PrintFullContext-> print_full_context_typ env sigma | PrintSectionContext qid -> print_sec_context_typ env sigma qid @@ -2249,7 +2274,33 @@ let locate_if_not_already ?loc (e, info) = | None -> (e, Option.cata (Loc.add_loc info) info loc) | Some l -> (e, info) -exception End_of_input +let mk_time_header = + (* Drop the time header to print the command, we should indeed use a + different mechanism to `-time` commands than the current hack of + adding a time control to the AST. *) + let pr_time_header vernac = + let vernac = match vernac with + | { v = { control = ControlTime _ :: control; attrs; expr }; loc } -> + CAst.make ?loc { control; attrs; expr } + | _ -> vernac + in + Topfmt.pr_cmd_header vernac + in + fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac) + +let interp_control_flag ~time_header (f : control_flag) ~st + (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) = + match f with + | ControlFail -> + with_fail ~st (fun () -> fn ~st); + st.Vernacstate.lemmas + | ControlTimeout timeout -> + vernac_timeout ~timeout (fun () -> fn ~st) () + | ControlTime batch -> + let header = if batch then Lazy.force time_header else Pp.mt () in + System.with_time ~batch ~header (fun () -> fn ~st) () + | ControlRedirect s -> + Topfmt.with_output_to_file s (fun () -> fn ~st) () (* EJGA: We may remove this, only used twice below *) let vernac_require_open_lemma ~stack f = @@ -2610,7 +2661,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with * is the outdated/deprecated "Local" attribute of some vernacular commands * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) -and interp_expr ?proof ~atts ~st c = +and interp_expr ~atts ~st c = let stack = st.Vernacstate.lemmas in vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); match c with @@ -2640,6 +2691,8 @@ and interp_expr ?proof ~atts ~st c = without a considerable amount of refactoring. *) and vernac_load ~verbosely fname = + let exception End_of_input in + (* Note that no proof should be open here, so the state here is just token for now *) let st = Vernacstate.freeze_interp_state ~marshallable:false in let fname = @@ -2660,7 +2713,7 @@ and vernac_load ~verbosely fname = try let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in let stack = - v_mod (interp_control ?proof:None ~st:{ st with Vernacstate.lemmas = stack }) + v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack }) (parse_sentence proof_mode input) in load_loop ~stack with @@ -2673,23 +2726,36 @@ and vernac_load ~verbosely fname = CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); () -and interp_control ?proof ~st v = match v with - | { v=VernacExpr (atts, cmd) } -> - let before_univs = Global.universes () in - let pstack = interp_expr ?proof ~atts ~st cmd in - if before_univs == Global.universes () then pstack - else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack - | { v=VernacFail v } -> - with_fail ~st (fun () -> interp_control ?proof ~st v); - st.Vernacstate.lemmas - | { v=VernacTimeout (timeout,v) } -> - vernac_timeout ~timeout (interp_control ?proof ~st) v - | { v=VernacRedirect (s, v) } -> - Topfmt.with_output_to_file s (interp_control ?proof ~st) v - | { v=VernacTime (batch, cmd) }-> - let header = if batch then Topfmt.pr_cmd_header cmd else Pp.mt () in - System.with_time ~batch ~header (interp_control ?proof ~st) cmd - +and interp_control ~st ({ v = cmd } as vernac) = + let time_header = mk_time_header vernac in + List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) + cmd.control + (fun ~st -> + let before_univs = Global.universes () in + let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in + if before_univs == Global.universes () then pstack + else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack) + ~st + +(* Interpreting a possibly delayed proof *) +let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option = + let stack = st.Vernacstate.lemmas in + let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in + let () = match pe with + | Admitted -> + save_lemma_admitted_delayed ~proof ~info + | Proved (_,idopt) -> + save_lemma_proved_delayed ~proof ~info ~idopt in + stack + +let interp_qed_delayed_control ~proof ~info ~st ~control { loc; v=pe } = + let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in + List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) + control + (fun ~st -> interp_qed_delayed ~proof ~info ~st pe) + ~st + +(* General interp with management of state *) let () = declare_int_option { optdepr = false; @@ -2699,11 +2765,11 @@ let () = optwrite = ((:=) default_timeout) } (* Be careful with the cache here in case of an exception. *) -let interp ?(verbosely=true) ~st cmd = +let interp_gen ~verbosely ~st ~interp_fn cmd = Vernacstate.unfreeze_interp_state st; try vernac_timeout (fun st -> let v_mod = if verbosely then Flags.verbosely else Flags.silently in - let ontop = v_mod (interp_control ~st) cmd in + let ontop = v_mod (interp_fn ~st) cmd in Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"]; Vernacstate.freeze_interp_state ~marshallable:false ) st @@ -2713,18 +2779,10 @@ let interp ?(verbosely=true) ~st cmd = Vernacstate.invalidate_cache (); iraise exn -let interp_qed_delayed_proof ~proof ~info ~st ?loc pe : Vernacstate.t = - let stack = st.Vernacstate.lemmas in - let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in - try - let () = match pe with - | Admitted -> - save_lemma_admitted_delayed ~proof ~info - | Proved (_,idopt) -> - save_lemma_proved_delayed ~proof ~info ~idopt in - { st with Vernacstate.lemmas = stack } - with exn -> - let exn = CErrors.push exn in - let exn = locate_if_not_already ?loc exn in - Vernacstate.invalidate_cache (); - iraise exn +(* Regular interp *) +let interp ?(verbosely=true) ~st cmd = + interp_gen ~verbosely ~st ~interp_fn:interp_control cmd + +let interp_qed_delayed_proof ~proof ~info ~st ~control pe : Vernacstate.t = + interp_gen ~verbosely:false ~st + ~interp_fn:(interp_qed_delayed_control ~proof ~info ~control) pe diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index e618cdcefe..e65f9d3cfe 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -17,8 +17,8 @@ val interp_qed_delayed_proof : proof:Proof_global.proof_object -> info:Lemmas.Info.t -> st:Vernacstate.t - -> ?loc:Loc.t - -> Vernacexpr.proof_end + -> control:Vernacexpr.control_flag list + -> Vernacexpr.proof_end CAst.t -> Vernacstate.t (** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *) diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 0968632c2d..d4b2029e99 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -24,6 +24,7 @@ type goal_reference = | GoalId of Id.t type printable = + | PrintTypingFlags | PrintTables | PrintFullContext | PrintSectionContext of qualid @@ -414,12 +415,17 @@ type nonrec vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list -type vernac_control_r = - | VernacExpr of Attributes.vernac_flags * vernac_expr +type control_flag = + | ControlTime of bool (* boolean is true when the `-time` batch-mode command line flag was set. the flag is used to print differently in `-time` vs `Time foo` *) - | VernacTime of bool * vernac_control - | VernacRedirect of string * vernac_control - | VernacTimeout of int * vernac_control - | VernacFail of vernac_control + | ControlRedirect of string + | ControlTimeout of int + | ControlFail + +type vernac_control_r = + { control : control_flag list + ; attrs : Attributes.vernac_flags + ; expr : vernac_expr + } and vernac_control = vernac_control_r CAst.t diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 747998c6cc..903a28e953 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -13,47 +13,26 @@ open Vernacexpr -let rec under_control v = v |> CAst.with_val (function - | VernacExpr (_, c) -> c - | VernacRedirect (_,c) - | VernacTime (_,c) - | VernacFail c - | VernacTimeout (_,c) -> under_control c - ) - -let rec has_Fail v = v |> CAst.with_val (function - | VernacExpr _ -> false - | VernacRedirect (_,c) - | VernacTime (_,c) - | VernacTimeout (_,c) -> has_Fail c - | VernacFail _ -> true) +(* Does this vernacular involve Fail? *) +let has_Fail { CAst.v } = List.mem ControlFail v.control (* Navigation commands are allowed in a coqtop session but not in a .v file *) -let is_navigation_vernac_expr = function +let is_navigation_vernac = function | VernacResetInitial | VernacResetName _ | VernacBack _ -> true | _ -> false -let is_navigation_vernac c = - is_navigation_vernac_expr (under_control c) - -let rec is_deep_navigation_vernac v = v |> CAst.with_val (function - | VernacTime (_,c) -> is_deep_navigation_vernac c - | VernacRedirect (_, c) - | VernacTimeout (_, c) | VernacFail c -> is_navigation_vernac c - | VernacExpr _ -> false) - (* NB: Reset is now allowed again as asked by A. Chlipala *) -let is_reset = CAst.with_val (function - | VernacExpr ( _, VernacResetInitial) - | VernacExpr (_, VernacResetName _) -> true - | _ -> false) +let is_reset = function + | VernacResetInitial + | VernacResetName _ -> true + | _ -> false -let is_debug cmd = match under_control cmd with +let is_debug = function | VernacSetOption (_, ["Ltac";"Debug"], _) -> true | _ -> false -let is_undo cmd = match under_control cmd with +let is_undo = function | VernacUndo _ | VernacUndoTo _ -> true | _ -> false diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli index 8875b86d94..320878e401 100644 --- a/vernac/vernacprop.mli +++ b/vernac/vernacprop.mli @@ -13,16 +13,9 @@ open Vernacexpr -(* Return the vernacular command below control (Time, Timeout, Redirect, Fail). - Beware that Fail can change many properties of the underlying command, since - a success of Fail means the command was backtracked over. *) -val under_control : vernac_control -> vernac_expr - val has_Fail : vernac_control -> bool - -val is_navigation_vernac : vernac_control -> bool -val is_deep_navigation_vernac : vernac_control -> bool -val is_reset : vernac_control -> bool -val is_debug : vernac_control -> bool -val is_undo : vernac_control -> bool +val is_navigation_vernac : vernac_expr -> bool +val is_reset : vernac_expr -> bool +val is_debug : vernac_expr -> bool +val is_undo : vernac_expr -> bool |