diff options
41 files changed, 381 insertions, 343 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e56693eac2..6b52870ce6 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -136,7 +136,6 @@ before_script: stage: test script: - INSTALLDIR=$(readlink -f _install_ci) - - ./configure -prefix "$INSTALLDIR" ${EXTRA_CONF} - cp "$INSTALLDIR/lib/coq/tools/coqdoc/coqdoc.sty" . - LIB="$INSTALLDIR/lib/coq" diff --git a/API/API.mli b/API/API.mli index a69766901b..e46bca85fc 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4159,10 +4159,6 @@ sig type vernac_expr = | VernacLoad of verbose_flag * string - | VernacTime of vernac_expr Loc.located - | VernacRedirect of string * vernac_expr Loc.located - | VernacTimeout of int * vernac_expr - | VernacFail of vernac_expr | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) | VernacOpenCloseScope of bool * scope_name | VernacDelimiters of scope_name * string option @@ -4294,6 +4290,16 @@ sig and vernac_classification = vernac_type * vernac_when and one_inductive_expr = ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list + +type vernac_control = + | VernacExpr of vernac_expr + (* Control *) + | VernacTime of vernac_control Loc.located + | VernacRedirect of string * vernac_control Loc.located + | VernacTimeout of int * vernac_control + | VernacFail of vernac_control + + end (* XXX: end of moved from intf *) @@ -4302,7 +4308,7 @@ sig type typeclass = { cl_univs : Univ.AUContext.t; cl_impl : Globnames.global_reference; - cl_context : (Globnames.global_reference * bool) option list * Context.Rel.t; + cl_context : Globnames.global_reference option list * Context.Rel.t; cl_props : Context.Rel.t; cl_projs : (Names.Name.t * (direction * Vernacexpr.hint_info_expr) option * Names.Constant.t option) list; @@ -5175,9 +5181,7 @@ sig val gallina_ext : vernac_expr Gram.entry val command : vernac_expr Gram.entry val syntax : vernac_expr Gram.entry - val vernac : vernac_expr Gram.entry val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry - val vernac_eoi : vernac_expr Gram.entry val noedit_mode : vernac_expr Gram.entry val command_entry : vernac_expr Gram.entry val red_expr : raw_red_expr Gram.entry @@ -5973,7 +5977,7 @@ end module Ppvernac : sig - val pr_vernac : Vernacexpr.vernac_expr -> Pp.t + val pr_vernac : Vernacexpr.vernac_control -> Pp.t val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t end @@ -6221,7 +6225,7 @@ sig val classify_as_proofstep : Vernacexpr.vernac_classification val classify_as_query : Vernacexpr.vernac_classification val classify_as_sideeff : Vernacexpr.vernac_classification - val classify_vernac : Vernacexpr.vernac_expr -> Vernacexpr.vernac_classification + val classify_vernac : Vernacexpr.vernac_control -> Vernacexpr.vernac_classification end module Stm : diff --git a/dev/base_include b/dev/base_include index d7059fe74f..4dc9a0bee8 100644 --- a/dev/base_include +++ b/dev/base_include @@ -193,7 +193,7 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; +let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;; let parse_tac = API.Pcoq.parse_string Ltac_plugin.Pltac.tactic;; (* build a term of type glob_constr without type-checking or resolution of diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 58599a14dc..aafc3fc59a 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -54,7 +54,7 @@ let coqide_known_option table = List.mem table [ ["Printing";"Universes"]; ["Printing";"Unfocused"]] -let is_known_option cmd = match cmd with +let is_known_option cmd = match Vernacprop.under_control cmd with | VernacSetOption (o,BoolValue true) | VernacUnsetOption o -> coqide_known_option o | _ -> false diff --git a/interp/declare.ml b/interp/declare.ml index 8781c87192..5be07e09ec 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -231,11 +231,24 @@ let cache_variable ((sp,_),o) = | SectionLocalDef (de) -> let (de, eff) = Global.export_private_constants ~in_section:true de in let () = List.iter register_side_effect eff in - let univs = Global.push_named_def (id,de) in - let poly = match de.const_entry_universes with - | Monomorphic_const_entry _ -> false - | Polymorphic_const_entry _ -> true + (** The body should already have been forced upstream because it is a + section-local definition, but it's not enforced by typing *) + let (body, uctx), () = Future.force de.const_entry_body in + let poly, univs = match de.const_entry_universes with + | Monomorphic_const_entry uctx -> false, uctx + | Polymorphic_const_entry uctx -> true, Univ.ContextSet.of_context uctx in + let univs = Univ.ContextSet.union uctx univs in + (** We must declare the universe constraints before type-checking the + term. *) + let () = Global.push_context_set (not poly) univs in + let se = { + secdef_body = body; + secdef_secctx = de.const_entry_secctx; + secdef_feedback = de.const_entry_feedback; + secdef_type = de.const_entry_type; + } in + let () = Global.push_named_def (id, se) in Explicit, de.const_entry_opaque, poly, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index f7c36c4e5f..bfe73160bb 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -38,10 +38,10 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits val combine_params_freevar : - Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t -> + Id.Set.t -> global_reference option * Context.Rel.Declaration.t -> Constrexpr.constr_expr * Id.Set.t val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t -> + (Id.Set.t -> global_reference option * Context.Rel.Declaration.t -> Constrexpr.constr_expr * Id.Set.t) -> constr_expr -> constr_expr * Id.Set.t diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index c7a9db1cbc..a90e5501a5 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -315,13 +315,8 @@ type cumulative_inductive_parsing_flag = (** {6 The type of vernacular expressions} *) type vernac_expr = - (* Control *) - | VernacLoad of verbose_flag * string - | VernacTime of vernac_expr located - | VernacRedirect of string * vernac_expr located - | VernacTimeout of int * vernac_expr - | VernacFail of vernac_expr + | VernacLoad of verbose_flag * string (* Syntax *) | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) | VernacOpenCloseScope of bool * scope_name @@ -482,6 +477,14 @@ and vernac_argument_status = { implicit_status : vernac_implicit_status; } +type vernac_control = + | VernacExpr of vernac_expr + (* Control *) + | VernacTime of vernac_control located + | VernacRedirect of string * vernac_control located + | VernacTimeout of int * vernac_control + | VernacFail of vernac_control + (* A vernac classifier provides information about the exectuion of a command: diff --git a/kernel/entries.ml b/kernel/entries.ml index ca79de404d..36b75668b2 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -81,6 +81,13 @@ type 'a definition_entry = { const_entry_opaque : bool; const_entry_inline_code : bool } +type section_def_entry = { + secdef_body : constr; + secdef_secctx : Context.Named.t option; + secdef_feedback : Stateid.t option; + secdef_type : types option; +} + type inline = int option (* inlining level, None for no inlining *) type parameter_entry = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index fa984515a7..93b8e278fa 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -382,22 +382,9 @@ let safe_push_named d env = let push_named_def (id,de) senv = - let open Entries in - let c,typ,univs = Term_typing.translate_local_def senv.env id de in - let poly = match de.Entries.const_entry_universes with - | Monomorphic_const_entry _ -> false - | Polymorphic_const_entry _ -> true - in - let c, univs = match c with - | Def c -> Mod_subst.force_constr c, univs - | OpaqueDef o -> - Opaqueproof.force_proof (Environ.opaque_tables senv.env) o, - Univ.ContextSet.union univs - (Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o) - | _ -> assert false in - let senv' = push_context_set poly univs senv in - let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in - univs, {senv' with env=env''} + let c, typ = Term_typing.translate_local_def senv.env id de in + let env'' = safe_push_named (LocalDef (id, c, typ)) senv.env in + { senv with env = env'' } let push_named_assum ((id,t,poly),ctx) senv = let senv' = push_context_set poly ctx senv in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index fbc398a2aa..757b803a39 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -90,7 +90,7 @@ val push_named_assum : (** Returns the full universe context necessary to typecheck the definition (futures are forced) *) val push_named_def : - Id.t * unit Entries.definition_entry -> Univ.ContextSet.t safe_transformer + Id.t * Entries.section_def_entry -> safe_transformer0 (** Insertion of global axioms or definitions *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 761eab511a..2e4426d621 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -227,17 +227,14 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> feedback ~id:state_id Feedback.Complete) -let abstract_constant_universes abstract = function +let abstract_constant_universes = function | Monomorphic_const_entry uctx -> Univ.empty_level_subst, Monomorphic_const uctx | Polymorphic_const_entry uctx -> - if not abstract then - Univ.empty_level_subst, Monomorphic_const (Univ.ContextSet.of_context uctx) - else - let sbst, auctx = Univ.abstract_universes uctx in - sbst, Polymorphic_const auctx + let sbst, auctx = Univ.abstract_universes uctx in + sbst, Polymorphic_const auctx -let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) = +let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = match dcl with | ParameterEntry (ctx,(t,uctx),nl) -> let env = match uctx with @@ -245,10 +242,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env in let j = infer env t in - let abstract = not (Option.is_empty kn) in - let usubst, univs = - abstract_constant_universes abstract uctx - in + let usubst, univs = abstract_constant_universes uctx in let c = Typeops.assumption_of_judgment env j in let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in { @@ -316,12 +310,11 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry | SideEffects _ -> inline_side_effects env body ctx side_eff in let env = push_context_set ~strict:(not poly) ctx env in - let abstract = not (Option.is_empty kn) in let ctx = if poly then Polymorphic_const_entry (Univ.ContextSet.to_context ctx) else Monomorphic_const_entry ctx in - let usubst, univs = abstract_constant_universes abstract ctx in + let usubst, univs = abstract_constant_universes ctx in let j = infer env body in let typ = match typ with | None -> @@ -493,7 +486,7 @@ let build_constant_declaration kn env result = let translate_constant mb env kn ce = build_constant_declaration kn env - (infer_declaration ~trust:mb env (Some kn) ce) + (infer_declaration ~trust:mb env ce) let constant_entry_of_side_effect cb u = let univs = @@ -607,7 +600,17 @@ let translate_recipe env kn r = let translate_local_def env id centry = let open Cooking in - let decl = infer_declaration ~trust:Pure env None (DefinitionEntry centry) in + let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in + let centry = { + const_entry_body = body; + const_entry_secctx = centry.secdef_secctx; + const_entry_feedback = centry.secdef_feedback; + const_entry_type = centry.secdef_type; + const_entry_universes = Monomorphic_const_entry Univ.ContextSet.empty; + const_entry_opaque = false; + const_entry_inline_code = false; + } in + let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in let typ = decl.cook_type in if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin match decl.cook_body with @@ -619,11 +622,22 @@ let translate_local_def env id centry = (Opaqueproof.force_proof (opaque_tables env) lc) in record_aux env ids_typ ids_def end; - let univs = match decl.cook_universes with - | Monomorphic_const ctx -> ctx + let () = match decl.cook_universes with + | Monomorphic_const ctx -> assert (Univ.ContextSet.is_empty ctx) | Polymorphic_const _ -> assert false in - decl.cook_body, typ, univs + let c = match decl.cook_body with + | Def c -> Mod_subst.force_constr c + | OpaqueDef o -> + let p = Opaqueproof.force_proof (Environ.opaque_tables env) o in + let cst = Opaqueproof.force_constraints (Environ.opaque_tables env) o in + (** Let definitions are ensured to have no extra constraints coming from + the body by virtue of the typing of [Entries.section_def_entry]. *) + let () = assert (Univ.ContextSet.is_empty cst) in + p + | Undef _ -> assert false + in + c, typ (* Insertion of inductive types. *) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index c771452a19..7bc029010f 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -18,8 +18,8 @@ type _ trust = | Pure : unit trust | SideEffects : structure_body -> side_effects trust -val translate_local_def : env -> Id.t -> unit definition_entry -> - constant_def * types * Univ.ContextSet.t +val translate_local_def : env -> Id.t -> section_def_entry -> + constr * types val translate_local_assum : env -> types -> types @@ -72,7 +72,7 @@ val translate_recipe : env -> Constant.t -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:'a trust -> env -> Constant.t option -> +val infer_declaration : trust:'a trust -> env -> 'a constant_entry -> Cooking.result val build_constant_declaration : diff --git a/library/global.ml b/library/global.ml index ce37dfecff..ed847b7cdb 100644 --- a/library/global.ml +++ b/library/global.ml @@ -81,7 +81,7 @@ let globalize_with_summary fs f = let i2l = Label.of_id let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) -let push_named_def d = globalize (Safe_typing.push_named_def d) +let push_named_def d = globalize0 (Safe_typing.push_named_def d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) let push_context b c = globalize0 (Safe_typing.push_context b c) diff --git a/library/global.mli b/library/global.mli index 2a646386e7..03bc945dad 100644 --- a/library/global.mli +++ b/library/global.mli @@ -32,7 +32,7 @@ val set_typing_flags : Declarations.typing_flags -> unit (** Variables, Local definitions, constants, inductive types *) val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * unit Entries.definition_entry) -> Univ.ContextSet.t +val push_named_def : (Id.t * Entries.section_def_entry) -> unit val export_private_constants : in_section:bool -> Safe_typing.private_constants Entries.definition_entry -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 444f36833b..c18c6810f7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -65,14 +65,17 @@ let parse_compat_version ?(allow_old = true) = let open Flags in function Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") GEXTEND Gram - GLOBAL: vernac gallina_ext noedit_mode subprf; - vernac: FIRST + GLOBAL: vernac_control gallina_ext noedit_mode subprf; + vernac_control: FIRST [ [ IDENT "Time"; c = located_vernac -> VernacTime c | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c) - | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) - | IDENT "Fail"; v = vernac -> VernacFail v - - | IDENT "Local"; v = vernac_poly -> VernacLocal (true, v) + | IDENT "Timeout"; n = natural; v = vernac_control -> VernacTimeout(n,v) + | IDENT "Fail"; v = vernac_control -> VernacFail v + | v = vernac -> VernacExpr(v) ] + ] + ; + vernac: + [ [ IDENT "Local"; v = vernac_poly -> VernacLocal (true, v) | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v) | v = vernac_poly -> v ] @@ -111,7 +114,7 @@ GEXTEND Gram ; located_vernac: - [ [ v = vernac -> Loc.tag ~loc:!@loc v ] ] + [ [ v = vernac_control -> Loc.tag ~loc:!@loc v ] ] ; END diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index b766f0c6bb..c934d38a25 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -503,8 +503,7 @@ module Vernac_ = let gallina_ext = gec_vernac "gallina_ext" let command = gec_vernac "command" let syntax = gec_vernac "syntax_command" - let vernac = gec_vernac "Vernac.vernac" - let vernac_eoi = eoi_entry vernac + let vernac_control = gec_vernac "Vernac.vernac_control" let rec_definition = gec_vernac "Vernac.rec_definition" let red_expr = make_gen_entry utactic "red_expr" let hint_info = gec_vernac "hint_info" @@ -517,7 +516,7 @@ module Vernac_ = let act_eoi = Gram.action (fun _ loc -> None) in let rule = [ ([ Symbols.stoken Tok.EOI ], act_eoi); - ([ Symbols.snterm (Gram.Entry.obj vernac) ], act_vernac ); + ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac ); ] in uncurry (Gram.extend main_entry) (None, make_rule rule) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 3ca013a968..756d9487df 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -251,9 +251,8 @@ module Vernac_ : val gallina_ext : vernac_expr Gram.entry val command : vernac_expr Gram.entry val syntax : vernac_expr Gram.entry - val vernac : vernac_expr Gram.entry + val vernac_control : vernac_control Gram.entry val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry - val vernac_eoi : vernac_expr Gram.entry val noedit_mode : vernac_expr Gram.entry val command_entry : vernac_expr Gram.entry val red_expr : raw_red_expr Gram.entry @@ -261,7 +260,7 @@ module Vernac_ : end (** The main entry: reads an optional vernac command *) -val main_entry : (Loc.t * vernac_expr) option Gram.entry +val main_entry : (Loc.t * vernac_control) option Gram.entry (** Handling of the proof mode entry *) val get_command_entry : unit -> vernac_expr Gram.entry diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 87609296bc..2fd6f53c4a 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)) + (Vernacexpr.(VernacExpr(VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 889c064b24..97066e5312 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1509,7 +1509,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))) ++ fnl () ++ msg in @@ -1524,7 +1524,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 9ae112d371..e5933de2a6 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -61,12 +61,9 @@ struct type t = Val.t -let normalize v = v - let of_constr c = in_gen (topwit wit_constr) c let to_constr v = - let v = normalize v in if has_type v (topwit wit_constr) then let c = out_gen (topwit wit_constr) v in Some c @@ -78,7 +75,6 @@ let to_constr v = let of_uconstr c = in_gen (topwit wit_uconstr) c let to_uconstr v = - let v = normalize v in if has_type v (topwit wit_uconstr) then Some (out_gen (topwit wit_uconstr) v) else None @@ -86,7 +82,6 @@ let to_uconstr v = let of_int i = in_gen (topwit wit_int) i let to_int v = - let v = normalize v in if has_type v (topwit wit_int) then Some (out_gen (topwit wit_int) v) else None @@ -108,14 +103,12 @@ let constr_of_id env id = (* Gives the constr corresponding to a Constr_context tactic_arg *) let coerce_to_constr_context v = - let v = Value.normalize v in if has_type v (topwit wit_constr_context) then out_gen (topwit wit_constr_context) v else raise (CannotCoerceTo "a term context") (* Interprets an identifier which must be fresh *) let coerce_var_to_ident fresh env sigma v = - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "a fresh identifier") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -140,7 +133,6 @@ let g = sigma in let id_of_name = function | Name.Anonymous -> Id.of_string "x" | Name.Name x -> x in - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "an identifier") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -179,7 +171,6 @@ let id_of_name = function let coerce_to_intro_pattern env sigma v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then snd (out_gen (topwit wit_intro_pattern) v) else if has_type v (topwit wit_var) then @@ -198,7 +189,6 @@ let coerce_to_intro_pattern_naming env sigma v = | _ -> raise (CannotCoerceTo "a naming introduction pattern") let coerce_to_hint_base v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with | _, IntroNaming (IntroIdentifier id) -> Id.to_string id @@ -206,13 +196,11 @@ let coerce_to_hint_base v = else raise (CannotCoerceTo "a hint base name") let coerce_to_int v = - let v = Value.normalize v in if has_type v (topwit wit_int) then out_gen (topwit wit_int) v else raise (CannotCoerceTo "an integer") let coerce_to_constr env v = - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "a term") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -230,7 +218,6 @@ let coerce_to_constr env v = else fail () let coerce_to_uconstr env v = - let v = Value.normalize v in if has_type v (topwit wit_uconstr) then out_gen (topwit wit_uconstr) v else @@ -243,7 +230,6 @@ let coerce_to_closed_constr env v = let coerce_to_evaluable_ref env sigma v = let fail () = raise (CannotCoerceTo "an evaluable reference") in - let v = Value.normalize v in let ev = if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -284,7 +270,6 @@ let coerce_to_intro_pattern_list ?loc env sigma v = let coerce_to_hyp env sigma v = let fail () = raise (CannotCoerceTo "a variable") in - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id @@ -306,7 +291,6 @@ let coerce_to_hyp_list env sigma v = (* Interprets a qualified name *) let coerce_to_reference env sigma v = - let v = Value.normalize v in match Value.to_constr v with | Some c -> begin @@ -318,7 +302,6 @@ let coerce_to_reference env sigma v = (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) let coerce_to_quantified_hypothesis sigma v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in match v with @@ -336,7 +319,6 @@ let coerce_to_quantified_hypothesis sigma v = (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) let coerce_to_decl_or_quant_hyp env sigma v = - let v = Value.normalize v in if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) else diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index d7b253a687..dce16b7333 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -31,9 +31,6 @@ module Value : sig type t = Val.t - val normalize : t -> t - (** Eliminated the leading dynamic type casts. *) - val of_constr : constr -> t val to_constr : t -> constr option val of_uconstr : Ltac_pretype.closed_glob_constr -> t diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index ccded44179..f2720954d0 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -136,7 +136,6 @@ let to_tacvalue v = out_gen (topwit wit_tacvalue) v (** More naming applications *) let name_vfun appl vle = - let vle = Value.normalize vle in if has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with | VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t)) @@ -235,7 +234,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with (* Displays a value *) let pr_value env v = - let v = Value.normalize v in let pr_with_env pr = match env with | Some (env,sigma) -> pr env sigma @@ -285,7 +283,6 @@ let push_trace call ist = match TacStore.get ist.extra f_trace with | Some trace -> Proofview.tclUNIT (call :: trace) let propagate_trace ist loc id v = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let tacv = to_tacvalue v in match tacv with @@ -298,7 +295,6 @@ let propagate_trace ist loc id v = else Proofview.tclUNIT v let append_trace trace v = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then match to_tacvalue v with | VFun (appl,trace',lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,lfun,it,b)) @@ -307,11 +303,9 @@ let append_trace trace v = (* Dynamically check that an argument is a tactic *) let coerce_to_tactic loc id v = - let v = Value.normalize v in let fail () = user_err ?loc (str "Variable " ++ Id.print id ++ str " should be bound to a tactic.") in - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let tacv = to_tacvalue v in match tacv with @@ -514,7 +508,6 @@ let rec intropattern_ids accu (loc,pat) = match pat with let extract_ids ids lfun accu = let fold id v accu = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let (_, ipat) = out_gen (topwit wit_intro_pattern) v in if Id.List.mem id ids then accu @@ -816,7 +809,6 @@ let interp_constr_may_eval ist env sigma c = (** TODO: should use dedicated printers *) let message_of_value v = - let v = Value.normalize v in let pr_with_env pr = Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in let open Genprint in @@ -986,7 +978,6 @@ let interp_destruction_arg ist gl arg = try (** FIXME: should be moved to taccoerce *) let v = Id.Map.find id ist.lfun in - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in match v with @@ -1248,7 +1239,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.run args tac and force_vrec ist v : Val.t Ftactic.t = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let v = to_tacvalue v in match v with @@ -1324,7 +1314,6 @@ and interp_tacarg ist arg : Val.t Ftactic.t = and interp_app loc ist fv largs : Val.t Ftactic.t = let (>>=) = Ftactic.bind in let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in - let fv = Value.normalize fv in if has_type fv (topwit wit_tacvalue) then match to_tacvalue fv with (* if var=[] and body has been delayed by val_interp, then body @@ -1377,7 +1366,6 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = (* Gives the tactic corresponding to the tactic value *) and tactic_of_value ist vle = - let vle = Value.normalize vle in if has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with | VFun (appl,trace,lfun,[],t) -> @@ -1604,7 +1592,6 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t = Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - let result = Value.normalize result in try let cresult = coerce_to_closed_constr env result in Proofview.tclLIFT begin diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index bbb3a1bb2b..bc9990d026 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -65,7 +65,7 @@ type typeclass = { cl_impl : global_reference; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : (global_reference * bool) option list * Context.Rel.t; + cl_context : global_reference option list * Context.Rel.t; (* Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; @@ -175,7 +175,7 @@ let subst_class (subst,cl) = and do_subst_gr gr = fst (subst_global subst gr) in let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = - List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs, + List.smartmap (Option.smartmap do_subst_gr) grs, do_subst_ctx ctx in let do_subst_projs projs = List.smartmap (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in @@ -213,10 +213,10 @@ let discharge_class (_,cl) = let newgrs = List.map (fun decl -> match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr Evd.empty with | None -> None - | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true)) + | Some (_, ((tc,_), _)) -> Some tc.cl_impl) ctx' in - List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs + List.smartmap (Option.smartmap Lib.discharge_global) grs @ newgrs in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 8ee061330a..0cbe1c71c0 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -25,9 +25,8 @@ type typeclass = { cl_impl : global_reference; (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. - The boolean indicates if the typeclass argument is a direct superclass and the global reference - gives a direct link to the class itself. *) - cl_context : (global_reference * bool) option list * Context.Rel.t; + The global reference gives a direct link to the class itself. *) + cl_context : global_reference option list * Context.Rel.t; (** Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 46ef2ac031..418d4a0b8f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -535,16 +535,25 @@ open Decl_kinds | SsFwdClose e -> "("^aux e^")*" in Pp.str (aux e) - let rec pr_vernac_body v = + let rec pr_vernac_expr v = let return = tag_vernac v in match v with | VernacPolymorphic (poly, v) -> let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in - return (s ++ spc () ++ pr_vernac_body v) + return (s ++ spc () ++ pr_vernac_expr v) | VernacProgram v -> - return (keyword "Program" ++ spc() ++ pr_vernac_body v) + return (keyword "Program" ++ spc() ++ pr_vernac_expr v) | VernacLocal (local, v) -> - return (pr_locality local ++ spc() ++ pr_vernac_body v) + return (pr_locality local ++ spc() ++ pr_vernac_expr v) + + | VernacLoad (f,s) -> + return ( + keyword "Load" + ++ if f then + (spc() ++ keyword "Verbose" ++ spc()) + else + spc() ++ qs s + ) (* Proof management *) | VernacAbortAll -> @@ -607,24 +616,6 @@ open Decl_kinds | VernacRestoreState s -> return (keyword "Restore State" ++ spc() ++ qs s) - (* Control *) - | VernacLoad (f,s) -> - return ( - keyword "Load" - ++ if f then - (spc() ++ keyword "Verbose" ++ spc()) - else - spc() ++ qs s - ) - | VernacTime (_,v) -> - return (keyword "Time" ++ spc() ++ pr_vernac_body v) - | VernacRedirect (s, (_,v)) -> - return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_body v) - | VernacTimeout(n,v) -> - return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_body v) - | VernacFail v -> - return (keyword "Fail" ++ spc() ++ pr_vernac_body v) - (* Syntax *) | VernacOpenCloseScope (opening,sc) -> return ( @@ -1228,6 +1219,19 @@ open Decl_kinds with Not_found -> hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") - let pr_vernac v = - try pr_vernac_body v ++ sep_end v - with e -> CErrors.print e + let rec pr_vernac_control v = + let return = tag_vernac v in + match v with + | VernacExpr v' -> 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 diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index cf27b413c0..34b4fb97f6 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -12,11 +12,11 @@ (** Prints a fixpoint body *) val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t -(** Prints a vernac expression *) -val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.t +(** Prints a vernac expression without dot *) +val pr_vernac_expr : Vernacexpr.vernac_expr -> Pp.t (** Prints a "proof using X" clause. *) val pr_using : Vernacexpr.section_subset_expr -> Pp.t (** Prints a vernac expression and closes it with a dot. *) -val pr_vernac : Vernacexpr.vernac_expr -> Pp.t +val pr_vernac : Vernacexpr.vernac_control -> Pp.t diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 77642946cd..01b5b9a016 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -23,8 +23,8 @@ val crawl : val unit_val : Stm.DynBlockData.t val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet -val of_vernac_expr_val : Vernacexpr.vernac_expr -> Stm.DynBlockData.t -val to_vernac_expr_val : Stm.DynBlockData.t -> Vernacexpr.vernac_expr +val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t +val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control end = struct @@ -32,7 +32,7 @@ let unit_tag = DynBlockData.create "unit" let unit_val = DynBlockData.Easy.inj () unit_tag let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet" -let of_vernac_expr_val, to_vernac_expr_val = DynBlockData.Easy.make_dyn "vernac_expr" +let of_vernac_control_val, to_vernac_control_val = DynBlockData.Easy.make_dyn "vernac_control" let simple_goal sigma g gs = let open Evar in @@ -74,14 +74,16 @@ include Util (* ****************** - foo - bar - baz *********************************** *) let static_bullet ({ entry_point; prev_node } as view) = - match entry_point.ast with + assert (not (Vernacprop.has_Fail entry_point.ast)); + match Vernacprop.under_control entry_point.ast with | Vernacexpr.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 - match node.ast with + if Vernacprop.has_Fail node.ast then `Stop + else match Vernacprop.under_control node.ast with | Vernacexpr.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 } @@ -94,7 +96,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some (Vernacexpr.VernacBullet (to_bullet_val b)) + recovery_command = Some (Vernacexpr.VernacExpr(Vernacexpr.VernacBullet (to_bullet_val b))) } | `Not -> `Leaks @@ -104,9 +106,10 @@ let () = register_proof_block_delimiter (* ******************** { block } ***************************************** *) let static_curly_brace ({ entry_point; prev_node } as view) = - assert(entry_point.ast = Vernacexpr.VernacEndSubproof); + assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof); crawl view (fun (nesting,prev) node -> - match node.ast with + if Vernacprop.has_Fail node.ast then `Cont (nesting,node) + else match Vernacprop.under_control node.ast with | Vernacexpr.VernacSubproof _ when nesting = 0 -> `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = unit_val } @@ -122,7 +125,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some Vernacexpr.VernacEndSubproof + recovery_command = Some (Vernacexpr.VernacExpr Vernacexpr.VernacEndSubproof) } | `Not -> `Leaks @@ -164,7 +167,7 @@ let static_indent ({ entry_point; prev_node } as view) = else `Found { block_stop = entry_point.id; block_start = node.id; dynamic_switch = node.id; - carry_on_data = of_vernac_expr_val entry_point.ast } + carry_on_data = of_vernac_control_val entry_point.ast } ) last_tac let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } = @@ -176,7 +179,7 @@ let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } = `ValidBlock { base_state = id; goals_to_admit = but_last; - recovery_command = Some (to_vernac_expr_val e); + recovery_command = Some (to_vernac_control_val e); } | `Not -> `Leaks diff --git a/stm/stm.ml b/stm/stm.ml index 3cb6bd9b60..afb6fabcb1 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -20,6 +20,7 @@ let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else open Pp open CErrors +open Names open Feedback open Vernacexpr @@ -111,7 +112,7 @@ type aast = { loc : Loc.t option; indentation : int; strlen : int; - mutable expr : vernac_expr; (* mutable: Proof using hinted by aux file *) + mutable expr : vernac_control; (* mutable: Proof using hinted by aux file *) } let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr) @@ -119,14 +120,14 @@ let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml. (* Commands piercing opaque *) let may_pierce_opaque = function - | { expr = VernacPrint _ } -> true - | { expr = VernacExtend (("Extraction",_), _) } -> true - | { expr = VernacExtend (("SeparateExtraction",_), _) } -> true - | { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true - | { expr = VernacExtend (("RecursiveExtractionLibrary",_), _) } -> true - | { expr = VernacExtend (("ExtractionConstant",_), _) } -> true - | { expr = VernacExtend (("ExtractionInlinedConstant",_), _) } -> true - | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true + | VernacPrint _ + | VernacExtend (("Extraction",_), _) + | VernacExtend (("SeparateExtraction",_), _) + | VernacExtend (("ExtractionLibrary",_), _) + | VernacExtend (("RecursiveExtractionLibrary",_), _) + | VernacExtend (("ExtractionConstant",_), _) + | VernacExtend (("ExtractionInlinedConstant",_), _) + | VernacExtend (("ExtractionInductive",_), _) -> true | _ -> false let update_global_env () = @@ -545,12 +546,10 @@ 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 - (let rec aux x = match x with - | VernacDefinition (_,((_,i),_),_) -> Names.Id.to_string i - | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.Id.to_string i - | VernacTime (_, e) - | VernacTimeout (_, e) -> aux e - | _ -> "branch" in aux x) + (match Vernacprop.under_control x with + | VernacDefinition (_,((_,i),_),_) -> Id.to_string i + | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Id.to_string i + | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind let get_info id = @@ -984,7 +983,7 @@ let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = in (* Some special handling of bullets and { }, to get a nicer display *) let pred n = max 0 (n-1) in - let ind, nl, new_beginend = match cmd with + let ind, nl, new_beginend = match Vernacprop.under_control cmd with | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend | VernacEndSubproof -> List.hd beginend, false, List.tl beginend | VernacBullet _ -> pred ind, nl, beginend @@ -1049,25 +1048,26 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t (* We need to check if a command should be filtered from * vernac_entries, as it cannot handle it. This should go away in * future refactorings. - *) - let rec is_filtered_command = function - | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ - | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true - | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e - | _ -> false + *) + let is_filtered_command = function + | VernacResetName _ | VernacResetInitial | VernacBack _ + | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ + | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true + | _ -> false in - let aux_interp st cmd = - if is_filtered_command cmd then - (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) - else match cmd with - | VernacShow ShowScript -> ShowScript.show_script (); st - | expr -> - stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); - try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (Loc.tag ?loc expr) - with e -> - let e = CErrors.push e in - Exninfo.iraise Hooks.(call_process_error_once e) + let aux_interp st expr = + let cmd = Vernacprop.under_control expr in + if is_filtered_command cmd then + (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) + else + match cmd with + | VernacShow ShowScript -> ShowScript.show_script (); st (** XX we are ignoring control here *) + | _ -> + stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); + try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (Loc.tag ?loc expr) + with e -> + let e = CErrors.push e in + Exninfo.iraise Hooks.(call_process_error_once e) in aux_interp st expr (****************************** CRUFT *****************************************) @@ -1083,7 +1083,7 @@ module Backtrack : sig val branches_of : Stateid.t -> backup (* Returns the state that the command should backtract to *) - val undo_vernac_classifier : vernac_expr -> Stateid.t * vernac_when + val undo_vernac_classifier : vernac_control -> Stateid.t * vernac_when end = struct (* {{{ *) @@ -1131,7 +1131,11 @@ end = struct (* {{{ *) match VCS.visit id with | { step = `Fork ((_,_,_,l),_) } -> l, false,0 | { step = `Cmd { cids = l; ctac } } -> l, ctac,0 - | { step = `Alias (_,{ expr = VernacUndo n}) } -> [], false, n + | { step = `Alias (_,{ expr }) } when not (Vernacprop.has_Fail expr) -> + begin match Vernacprop.under_control expr with + | VernacUndo n -> [], false, n + | _ -> [],false,0 + end | _ -> [],false,0 in match f acc (id, vcs, ids, tactic, undo) with | `Stop x -> x @@ -1149,7 +1153,7 @@ end = struct (* {{{ *) if VCS.is_interactive () = `No && !async_proofs_cache <> Some Force then undo_costly_in_batch_mode v; try - match v with + match Vernacprop.under_control v with | VernacResetInitial -> Stateid.initial, VtNow | VernacResetName (_,name) -> @@ -1242,7 +1246,7 @@ let _ = CErrors.register_handler (function type document_node = { indentation : int; - ast : Vernacexpr.vernac_expr; + ast : Vernacexpr.vernac_control; id : Stateid.t; } @@ -1257,7 +1261,7 @@ type static_block_detection = type recovery_action = { base_state : Stateid.t; goals_to_admit : Goal.goal list; - recovery_command : Vernacexpr.vernac_expr option; + recovery_command : Vernacexpr.vernac_control option; } type dynamic_block_error_recovery = @@ -1494,7 +1498,7 @@ end = struct (* {{{ *) stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; - expr = (VernacEndProof (Proved (Opaque,None))) }) in + expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) }) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1642,7 +1646,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; - expr = (VernacEndProof (Proved (Opaque,None))) }); + expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) }); `OK proof end with e -> @@ -2107,30 +2111,43 @@ let collect_proof keep cur hd brkind id = | [] -> no_name | id :: _ -> Names.Id.to_string id in let loc = (snd cur).loc in - let rec is_defined_expr = function + let is_defined_expr = function | VernacEndProof (Proved (Transparent,_)) -> true - | VernacTime (_, e) -> is_defined_expr e - | VernacRedirect (_, (_, e)) -> is_defined_expr e - | VernacTimeout (_, e) -> is_defined_expr e | _ -> false in let is_defined = function - | _, { expr = e } -> is_defined_expr e in + | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e) + && (not (Vernacprop.has_Fail e)) in + let proof_using_ast = function + | VernacProof(_,Some _) -> true + | _ -> false + in let proof_using_ast = function - | Some (_, ({ expr = VernacProof(_,Some _) } as v)) -> Some v + | Some (_, v) when proof_using_ast (Vernacprop.under_control v.expr) + && (not (Vernacprop.has_Fail v.expr)) -> Some v | _ -> None in let has_proof_using x = proof_using_ast x <> None in let proof_no_using = function - | Some (_, ({ expr = VernacProof(t,None) } as v)) -> t,v + | VernacProof(t,None) -> t + | _ -> assert false + in + let proof_no_using = function + | Some (_, v) -> proof_no_using (Vernacprop.under_control v.expr), v | _ -> assert false in let has_proof_no_using = function - | Some (_, { expr = VernacProof(_,None) }) -> true + | VernacProof(_,None) -> true + | _ -> false + in + let has_proof_no_using = function + | Some (_, v) -> has_proof_no_using (Vernacprop.under_control v.expr) + && (not (Vernacprop.has_Fail v.expr)) | _ -> false in let too_complex_to_delegate = function - | { expr = (VernacDeclareModule _ - | VernacDefineModule _ - | VernacDeclareModuleType _ - | VernacInclude _) } -> true - | { expr = (VernacRequire _ | VernacImport _) } -> true + | VernacDeclareModule _ + | VernacDefineModule _ + | VernacDeclareModuleType _ + | VernacInclude _ + | VernacRequire _ + | VernacImport _ -> true | ast -> may_pierce_opaque ast in let parent = function Some (p, _) -> p | None -> assert false in let is_empty = function `Async(_,[],_,_) | `MaybeASync(_,[],_,_) -> true | _ -> false in @@ -2138,7 +2155,8 @@ 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 x -> `Sync(no_name,`Print) + when too_complex_to_delegate (Vernacprop.under_control x.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 (* An Alias could jump everywhere... we hope we can ignore it*) @@ -2158,7 +2176,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 <- VernacProof(t, Some hint); + v.expr <- VernacExpr(VernacProof(t, Some hint)); `ASync (parent last,accn,name,delegate name) with Not_found -> let name = name ids in @@ -2177,9 +2195,13 @@ let collect_proof keep cur hd brkind id = | `ASync(_,_,name,_) -> `Sync (name,why) in let check_policy rc = if async_policy () then rc else make_sync `Policy rc in + let is_vernac_exact = function + | VernacExactProof _ -> true + | _ -> false + in match cur, (VCS.visit id).step, brkind with - | (parent, { expr = VernacExactProof _ }), `Fork _, _ - | (parent, { expr = VernacTime (_, VernacExactProof _) }), `Fork _, _ -> + | (parent, x), `Fork _, _ when is_vernac_exact (Vernacprop.under_control x.expr) + && (not (Vernacprop.has_Fail x.expr)) -> `Sync (no_name,`Immediate) | _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id) | _ -> @@ -2752,7 +2774,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) if !async_proofs_full then `QueryQueue (ref false) else if VCS.is_vio_doc () && VCS.((get_branch head).kind = `Master) && - may_pierce_opaque x + may_pierce_opaque (Vernacprop.under_control x.expr) then `SkipQueue else `MainQueue in VCS.commit id (mkTransCmd x [] false queue); @@ -2814,7 +2836,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) rc (* Side effect on all branches *) - | VtUnknown, _ when expr = VernacToplevelControl Drop -> + | VtUnknown, _ when Vernacprop.under_control expr = VernacToplevelControl Drop -> let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp (VCS.get_branch_pos head) st x); `Ok @@ -2826,7 +2848,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) VCS.commit id (mkTransCmd x l in_proof `MainQueue); (* We can't replay a Definition since universes may be differently * inferred. This holds in Coq >= 8.5 *) - let action = match x.expr with + let action = match Vernacprop.under_control x.expr with | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv | _ -> ReplayCommand x in VCS.propagate_sideff ~action; @@ -2854,7 +2876,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity | VernacLocal (_,e) -> opacity_of_produced_term e | _ -> Doesn'tGuaranteeOpacity in - VCS.commit id (Fork (x,bname,opacity_of_produced_term x.expr,[])); + VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[])); let proof_mode = default_proof_mode () in VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"]; diff --git a/stm/stm.mli b/stm/stm.mli index ef95be0e42..587b756422 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -39,7 +39,7 @@ val new_doc : stm_init_options -> doc * Stateid.t (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable -> - Vernacexpr.vernac_expr Loc.located + Vernacexpr.vernac_control Loc.located (* Reminder: A parsable [pa] is constructed using [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *) @@ -53,7 +53,7 @@ exception End_of_input If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> - bool -> Vernacexpr.vernac_expr Loc.located -> + bool -> Vernacexpr.vernac_control Loc.located -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* [query at ?report_with cmd] Executes [cmd] at a given state [at], @@ -111,7 +111,7 @@ val get_current_state : doc:doc -> Stateid.t val get_ldir : doc:doc -> Names.DirPath.t (* This returns the node at that position *) -val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option +val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_control Loc.located) option (* Filename *) val set_compilation_hints : string -> unit @@ -174,7 +174,7 @@ type static_block_declaration = { type document_node = { indentation : int; - ast : Vernacexpr.vernac_expr; + ast : Vernacexpr.vernac_control; id : Stateid.t; } @@ -189,7 +189,7 @@ type static_block_detection = type recovery_action = { base_state : Stateid.t; goals_to_admit : Goal.goal list; - recovery_command : Vernacexpr.vernac_expr option; + recovery_command : Vernacexpr.vernac_control option; } type dynamic_block_error_recovery = diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index c5ae27a110..1291b76426 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -8,6 +8,7 @@ open Vernacexpr open CErrors +open Util open Pp let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] @@ -47,36 +48,18 @@ let declare_vernac_classifier = classifiers := !classifiers @ [s,f] -let make_polymorphic (a, b as x) = - match a with - | VtStartProof (x, _, ids) -> - VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b - | _ -> x - -let rec classify_vernac e = - let static_classifier e = match e with +let classify_vernac e = + let rec static_classifier ~poly e = match e with (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) - | VernacSetOption (["Universe"; "Polymorphism"],_) - | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow + | ( VernacSetOption (l,_) | VernacUnsetOption l) + when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name -> + VtSideff [], VtNow (* Nested vernac exprs *) - | VernacProgram e -> classify_vernac e - | VernacLocal (_,e) -> classify_vernac e - | VernacPolymorphic (b, e) -> - if b || Flags.is_universe_polymorphism () (* Ok or not? *) then - make_polymorphic (classify_vernac e) - else classify_vernac e - | VernacTimeout (_,e) -> classify_vernac e - | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> classify_vernac e - | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) - (match classify_vernac e with - | ( VtQuery _ | VtProofStep _ | VtSideff _ - | VtProofMode _ | VtMeta), _ as x -> x - | VtQed _, _ -> - VtProofStep { parallel = `No; proof_block_detection = None }, - VtNow - | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) + | VernacProgram e -> static_classifier ~poly e + | VernacLocal (_,e) -> static_classifier ~poly e + | VernacPolymorphic (b, e) -> static_classifier ~poly:b e (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater @@ -106,17 +89,20 @@ let rec classify_vernac e = | VernacDefinition ((Decl_kinds.DoDischarge,_),((_,i),_),ProveBody _) -> VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater | VernacDefinition (_,((_,i),_),ProveBody _) -> - VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater + let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof(default_proof_mode (),guarantee,[i]), VtLater | VernacStartTheoremProof (_,l) -> let ids = CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in - VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater - | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater + let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (default_proof_mode (),guarantee,ids), VtLater + | VernacGoal _ -> + let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (default_proof_mode (),guarantee,[]), VtLater | VernacFixpoint (discharge,l) -> let guarantee = - match discharge with - | Decl_kinds.NoDischarge -> GuaranteesOpacity - | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity + if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + else GuaranteesOpacity in let ids, open_proof = List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) -> @@ -126,9 +112,8 @@ let rec classify_vernac e = else VtSideff ids, VtLater | VernacCoFixpoint (discharge,l) -> let guarantee = - match discharge with - | Decl_kinds.NoDischarge -> GuaranteesOpacity - | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity + if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + else GuaranteesOpacity in let ids, open_proof = List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) -> @@ -207,10 +192,21 @@ let rec classify_vernac e = try List.assoc s !classifiers l () with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in - let res = static_classifier e in - if Flags.is_universe_polymorphism () then - make_polymorphic res - else res + let rec static_control_classifier ~poly = function + | VernacExpr e -> static_classifier ~poly e + | VernacTimeout (_,e) -> static_control_classifier ~poly e + | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> + static_control_classifier ~poly e + | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) + (match static_control_classifier ~poly e with + | ( VtQuery _ | VtProofStep _ | VtSideff _ + | VtProofMode _ | VtMeta), _ as x -> x + | VtQed _, _ -> + VtProofStep { parallel = `No; proof_block_detection = None }, + VtNow + | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) + in + static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e let classify_as_query = VtQuery (true,Feedback.default_route), VtLater let classify_as_sideeff = VtSideff [], VtLater diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index fe42a03a3d..c0571c1d6f 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -12,7 +12,7 @@ open Genarg val string_of_vernac_classification : vernac_classification -> string (** What does a vernacular do *) -val classify_vernac : vernac_expr -> vernac_classification +val classify_vernac : vernac_control -> vernac_classification (** Install a vernacular classifier for VernacExtend *) val declare_vernac_classifier : diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v index b1769da3d8..31bc1cc31d 100644 --- a/theories/FSets/FSetCompat.v +++ b/theories/FSets/FSetCompat.v @@ -165,13 +165,13 @@ End Backport_WSets. (** * From new Sets to new ones *) Module Backport_Sets - (E:OrderedType.OrderedType) - (M:MSetInterface.Sets with Definition E.t := E.t - with Definition E.eq := E.eq - with Definition E.lt := E.lt) - <: FSetInterface.S with Module E:=E. + (O:OrderedType.OrderedType) + (M:MSetInterface.Sets with Definition E.t := O.t + with Definition E.eq := O.eq + with Definition E.lt := O.lt) + <: FSetInterface.S with Module E:=O. - Include Backport_WSets E M. + Include Backport_WSets O M. Implicit Type s : t. Implicit Type x y : elt. @@ -182,21 +182,21 @@ Module Backport_Sets Definition min_elt_1 : forall s x, min_elt s = Some x -> In x s := M.min_elt_spec1. Definition min_elt_2 : forall s x y, - min_elt s = Some x -> In y s -> ~ E.lt y x + min_elt s = Some x -> In y s -> ~ O.lt y x := M.min_elt_spec2. Definition min_elt_3 : forall s, min_elt s = None -> Empty s := M.min_elt_spec3. Definition max_elt_1 : forall s x, max_elt s = Some x -> In x s := M.max_elt_spec1. Definition max_elt_2 : forall s x y, - max_elt s = Some x -> In y s -> ~ E.lt x y + max_elt s = Some x -> In y s -> ~ O.lt x y := M.max_elt_spec2. Definition max_elt_3 : forall s, max_elt s = None -> Empty s := M.max_elt_spec3. - Definition elements_3 : forall s, sort E.lt (elements s) + Definition elements_3 : forall s, sort O.lt (elements s) := M.elements_spec2. Definition choose_3 : forall s s' x y, - choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y + choose s = Some x -> choose s' = Some y -> Equal s s' -> O.eq x y := M.choose_spec3. Definition lt_trans : forall s s' s'', lt s s' -> lt s' s'' -> lt s s'' := @StrictOrder_Transitive _ _ M.lt_strorder. @@ -211,7 +211,7 @@ Module Backport_Sets [ apply EQ | apply LT | apply GT ]; auto. Defined. - Module E := E. + Module E := O. End Backport_Sets. @@ -342,13 +342,13 @@ End Update_WSets. (** * From old Sets to new ones. *) Module Update_Sets - (E:Orders.OrderedType) - (M:FSetInterface.S with Definition E.t := E.t - with Definition E.eq := E.eq - with Definition E.lt := E.lt) - <: MSetInterface.Sets with Module E:=E. + (O:Orders.OrderedType) + (M:FSetInterface.S with Definition E.t := O.t + with Definition E.eq := O.eq + with Definition E.lt := O.lt) + <: MSetInterface.Sets with Module E:=O. - Include Update_WSets E M. + Include Update_WSets O M. Implicit Type s : t. Implicit Type x y : elt. @@ -359,21 +359,21 @@ Module Update_Sets Definition min_elt_spec1 : forall s x, min_elt s = Some x -> In x s := M.min_elt_1. Definition min_elt_spec2 : forall s x y, - min_elt s = Some x -> In y s -> ~ E.lt y x + min_elt s = Some x -> In y s -> ~ O.lt y x := M.min_elt_2. Definition min_elt_spec3 : forall s, min_elt s = None -> Empty s := M.min_elt_3. Definition max_elt_spec1 : forall s x, max_elt s = Some x -> In x s := M.max_elt_1. Definition max_elt_spec2 : forall s x y, - max_elt s = Some x -> In y s -> ~ E.lt x y + max_elt s = Some x -> In y s -> ~ O.lt x y := M.max_elt_2. Definition max_elt_spec3 : forall s, max_elt s = None -> Empty s := M.max_elt_3. - Definition elements_spec2 : forall s, sort E.lt (elements s) + Definition elements_spec2 : forall s, sort O.lt (elements s) := M.elements_3. Definition choose_spec3 : forall s s' x y, - choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y + choose s = Some x -> choose s' = Some y -> Equal s s' -> O.eq x y := M.choose_3. Instance lt_strorder : StrictOrder lt. @@ -407,6 +407,6 @@ Module Update_Sets Lemma compare_spec : forall s s', CompSpec eq lt s s' (compare s s'). Proof. intros; unfold compare; destruct M.compare; auto. Qed. - Module E := E. + Module E := O. End Update_Sets. diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 8fdaedbaf7..24d414c883 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -111,13 +111,14 @@ let pr_open_cur_subgoals () = (* | _ -> false *) let rec interp_vernac ~check ~interactive doc sid (loc,com) = - let interp = function + let interp v = + match under_control v with | VernacLoad (verbosely, fname) -> - let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in + let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let f = Loadpath.locate_file fname in load_vernac ~verbosely ~check ~interactive doc sid f - | v -> + | _ -> (* XXX: We need to run this before add as the classification is highly dynamic and depends on the structure of the diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index f9a4300267..8a798a98e9 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -12,7 +12,7 @@ expected to handle and print errors in form of exceptions, however care is taken so the state machine is left in a consistent state. *) -val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stm.doc * Stateid.t +val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_control Loc.located -> Stm.doc * Stateid.t (** [load_vernac echo sid file] Loads [file] on top of [sid], will echo the commands if [echo] is set. Callers are expected to handle diff --git a/vernac/classes.ml b/vernac/classes.ml index c2e9a5ab44..6914f899b7 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -141,7 +141,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false (fun avoid (clname, _) -> match clname with - | Some (cl, b) -> + | Some cl -> let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 6c3dfec7d1..1bb9e0da19 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -80,8 +80,8 @@ let pr_grammar = function | "pattern" -> pr_entry Pcoq.Constr.pattern | "vernac" -> - str "Entry vernac is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.vernac ++ + str "Entry vernac_control is" ++ fnl () ++ + pr_entry Pcoq.Vernac_.vernac_control ++ str "Entry command is" ++ fnl () ++ pr_entry Pcoq.Vernac_.command ++ str "Entry syntax is" ++ fnl () ++ diff --git a/vernac/record.ml b/vernac/record.ml index 114b55cb40..a7eb19dc8f 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -523,7 +523,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari let ctx_context = List.map (fun decl -> match Typeclasses.class_of_constr Evd.empty (EConstr.of_constr (RelDecl.get_type decl)) with - | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true) + | Some (_, ((cl,_), _)) -> Some cl.cl_impl | None -> None) params, params in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index a581043ac1..aa6121c39a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1380,11 +1380,13 @@ let _ = optread = (fun () -> !Flags.program_mode); optwrite = (fun b -> Flags.program_mode:=b) } +let universe_polymorphism_option_name = ["Universe"; "Polymorphism"] + let _ = declare_bool_option { optdepr = false; optname = "universe polymorphism"; - optkey = ["Universe"; "Polymorphism"]; + optkey = universe_polymorphism_option_name; optread = Flags.is_universe_polymorphism; optwrite = Flags.make_universe_polymorphism } @@ -1933,19 +1935,11 @@ let vernac_load interp fname = * loc is the Loc.t of the vernacular command being interpreted. *) let interp ?proof ~atts ~st c = let open Vernacinterp in - vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c); + vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); match c with - (* The below vernac are candidates for removal from the main type - and to be put into a new doc_command datatype: *) | VernacLoad _ -> assert false - (* Done later in this file *) - | VernacFail _ -> assert false - | VernacTime _ -> assert false - | VernacRedirect _ -> assert false - | VernacTimeout _ -> assert false - (* The STM should handle that, but LOAD bypasses the STM... *) | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command") | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command") @@ -2209,7 +2203,20 @@ let with_fail st b f = let interp ?(verbosely=true) ?proof ~st (loc,c) = let orig_program_mode = Flags.is_program_mode () in - let rec aux ?polymorphism ~atts isprogcmd = function + let rec control = function + | VernacExpr v -> + let atts = { loc; locality = None; polymorphic = false; } in + aux ~atts orig_program_mode v + | VernacFail v -> with_fail st true (fun () -> control v) + | VernacTimeout (n,v) -> + current_timeout := Some n; + control v + | VernacRedirect (s, (_,v)) -> + Topfmt.with_output_to_file s control v + | VernacTime (_,v) -> + System.with_time !Flags.time control v; + + and aux ?polymorphism ~atts isprogcmd = function | VernacProgram c when not isprogcmd -> aux ?polymorphism ~atts true c @@ -2229,20 +2236,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = | VernacLocal _ -> user_err Pp.(str "Locality specified twice") - | VernacFail v -> - with_fail st true (fun () -> aux ?polymorphism ~atts isprogcmd v) - - | VernacTimeout (n,v) -> - current_timeout := Some n; - aux ?polymorphism ~atts isprogcmd v - - | VernacRedirect (s, (_,v)) -> - Topfmt.with_output_to_file s (aux ?polymorphism ~atts isprogcmd) v - - | VernacTime (_,v) -> - System.with_time !Flags.time (aux ?polymorphism ~atts isprogcmd) v; - - | VernacLoad (_,fname) -> vernac_load (aux ?polymorphism ~atts false) fname + | VernacLoad (_,fname) -> vernac_load control fname | c -> check_vernac_supports_locality c atts.locality; @@ -2272,10 +2266,9 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = ignore (Flags.use_polymorphic_flag ()); iraise e in - let atts = { loc; locality = None; polymorphic = false; } in if verbosely - then Flags.verbosely (aux ~atts orig_program_mode) c - else aux ~atts orig_program_mode 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 *) diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index a559912a09..e99a62fe6c 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -18,7 +18,7 @@ val vernac_require : val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - st:Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t + st:Vernacstate.t -> Vernacexpr.vernac_control Loc.located -> Vernacstate.t (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name @@ -36,3 +36,5 @@ val command_focus : unit Proof.focus_kind val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t + +val universe_polymorphism_option_name : string list diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 3cff1f14c0..4a01ef2efa 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -11,32 +11,49 @@ open Vernacexpr +let rec under_control = function + | VernacExpr c -> c + | VernacRedirect (_,(_,c)) + | VernacTime (_,c) + | VernacFail c + | VernacTimeout (_,c) -> under_control c + +let rec has_Fail = function + | VernacExpr c -> false + | VernacRedirect (_,(_,c)) + | VernacTime (_,c) + | VernacTimeout (_,c) -> has_Fail c + | VernacFail _ -> true + (* Navigation commands are allowed in a coqtop session but not in a .v file *) -let rec is_navigation_vernac = function +let is_navigation_vernac_expr = function | VernacResetInitial | VernacResetName _ | VernacBacktrack _ | VernacBackTo _ | VernacBack _ -> true - | VernacRedirect (_, (_,c)) - | VernacTime (_,c) -> - is_navigation_vernac c (* Time Back* is harmless *) - | c -> is_deep_navigation_vernac c + | _ -> false -and is_deep_navigation_vernac = function +let is_navigation_vernac c = + is_navigation_vernac_expr (under_control c) + +let rec is_deep_navigation_vernac = function + | VernacTime (_,c) -> is_deep_navigation_vernac c + | VernacRedirect (_, (_,c)) | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c - | _ -> false + | VernacExpr _ -> false (* NB: Reset is now allowed again as asked by A. Chlipala *) let is_reset = function - | VernacResetInitial | VernacResetName _ -> true + | VernacExpr VernacResetInitial + | VernacExpr (VernacResetName _) -> true | _ -> false -let is_debug cmd = match cmd with +let is_debug cmd = match under_control cmd with | VernacSetOption (["Ltac";"Debug"], _) -> true | _ -> false -let is_query cmd = match cmd with +let is_query cmd = match under_control cmd with | VernacChdir None | VernacMemOption _ | VernacPrintOption _ @@ -47,6 +64,6 @@ let is_query cmd = match cmd with | VernacLocate _ -> true | _ -> false -let is_undo cmd = match cmd with +let is_undo cmd = match under_control cmd with | VernacUndo _ | VernacUndoTo _ -> true | _ -> false diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli index fbdba6bacb..eb7c7055ac 100644 --- a/vernac/vernacprop.mli +++ b/vernac/vernacprop.mli @@ -11,9 +11,16 @@ open Vernacexpr -val is_navigation_vernac : vernac_expr -> bool -val is_deep_navigation_vernac : vernac_expr -> bool -val is_reset : vernac_expr -> bool -val is_query : vernac_expr -> bool -val is_debug : vernac_expr -> bool -val is_undo : vernac_expr -> bool +(* 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_query : vernac_control -> bool +val is_debug : vernac_control -> bool +val is_undo : vernac_control -> bool |