diff options
Diffstat (limited to 'vernac/vernacentries.ml')
-rw-r--r-- | vernac/vernacentries.ml | 361 |
1 files changed, 191 insertions, 170 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 2f278ceb1..7f3410bc1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -29,6 +29,7 @@ open Redexpr open Lemmas open Misctypes open Locality +open Vernacinterp module NamedDecl = Context.Named.Declaration @@ -408,8 +409,8 @@ let dump_global r = (**********) (* Syntax *) -let vernac_syntax_extension locality local infix l = - let local = enforce_module_locality locality local in +let vernac_syntax_extension atts local infix l = + let local = enforce_module_locality atts.locality local in if infix then Metasyntax.check_infix_modifiers (snd l); Metasyntax.add_syntax_extension local l @@ -420,20 +421,20 @@ let vernac_delimiters sc = function let vernac_bind_scope sc cll = Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll) -let vernac_open_close_scope locality local (b,s) = - let local = enforce_section_locality locality local in +let vernac_open_close_scope ~atts local (b,s) = + let local = enforce_section_locality atts.locality local in Notation.open_close_scope (local,b,s) -let vernac_arguments_scope locality r scl = - let local = make_section_locality locality in +let vernac_arguments_scope ~atts r scl = + let local = make_section_locality atts.locality in Notation.declare_arguments_scope local (smart_global r) scl -let vernac_infix locality local = - let local = enforce_module_locality locality local in +let vernac_infix ~atts local = + let local = enforce_module_locality atts.locality local in Metasyntax.add_infix local (Global.env()) -let vernac_notation locality local = - let local = enforce_module_locality locality local in +let vernac_notation ~atts local = + let local = enforce_module_locality atts.locality local in Metasyntax.add_notation local (Global.env()) (***********) @@ -471,33 +472,33 @@ let vernac_definition_hook p = function | SubClass -> Class.add_subclass_hook p | _ -> no_hook -let vernac_definition locality p (local,k) ((loc,id as lid),pl) def = - let local = enforce_locality_exp locality local in - let hook = vernac_definition_hook p k in +let vernac_definition ~atts (local,k) ((loc,id as lid),pl) def = + let local = enforce_locality_exp atts.locality local in + let hook = vernac_definition_hook atts.polymorphic k in let () = match local with | Discharge -> Dumpglob.dump_definition lid true "var" | Local | Global -> Dumpglob.dump_definition lid false "def" in (match def with | ProveBody (bl,t) -> (* local binders, typ *) - start_proof_and_print (local,p,DefinitionBody k) + start_proof_and_print (local, atts.polymorphic, DefinitionBody k) [Some (lid,pl), (bl,t)] hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None | Some r -> - let sigma, env= Pfedit.get_current_context () in + let sigma, env = Pfedit.get_current_context () in Some (snd (Hook.get f_interp_redexp env sigma r)) in - do_definition id (local,p,k) pl bl red_option c typ_opt hook) + do_definition id (local, atts.polymorphic,k) pl bl red_option c typ_opt hook) -let vernac_start_proof locality p kind l = - let local = enforce_locality_exp locality None in +let vernac_start_proof ~atts kind l = + let local = enforce_locality_exp atts.locality None in if Dumpglob.dump () then List.iter (fun (id, _) -> match id with | Some (lid,_) -> Dumpglob.dump_definition lid false "prf" | None -> ()) l; - start_proof_and_print (local, p, Proof kind) l no_hook + start_proof_and_print (local, atts.polymorphic, Proof kind) l no_hook let vernac_end_proof ?proof = function | Admitted -> save_proof ?proof Admitted @@ -510,10 +511,10 @@ let vernac_exact_proof c = save_proof (Vernacexpr.(Proved(Opaque,None))); if not status then Feedback.feedback Feedback.AddedAxiom -let vernac_assumption locality poly (local, kind) l nl = - let local = enforce_locality_exp locality local in +let vernac_assumption ~atts (local, kind) l nl = + let local = enforce_locality_exp atts.locality local in let global = local == Global in - let kind = local, poly, kind in + let kind = local, atts.polymorphic, kind in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then List.iter (fun (lid, _) -> @@ -553,8 +554,8 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs = then the type is declared private (as per the [Private] keyword). [finite] indicates whether the type is inductive, co-inductive or neither. *) -let vernac_inductive cum poly lo finite indl = - let is_cumulative = should_treat_as_cumulative cum poly in +let vernac_inductive ~atts cum lo finite indl = + let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -571,13 +572,13 @@ let vernac_inductive cum poly lo finite indl = user_err Pp.(str "The Variant keyword does not support syntax { ... }.") | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> vernac_record cum (match b with Class _ -> Class false | _ -> b) - poly finite id bl c oc fs + atts.polymorphic finite id bl c oc fs | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> let f = let (coe, ((loc, id), ce)) = l in let coe' = if coe then Some true else None in (((coe', AssumExpr ((loc, Name id), ce)), None), []) - in vernac_record cum (Class true) poly finite id bl c None [f] + in vernac_record cum (Class true) atts.polymorphic finite id bl c None [f] | [ ( _ , _, _, Class _, Constructors _), [] ] -> user_err Pp.(str "Inductive classes not supported") | [ ( id , bl , c , Class _, _), _ :: _ ] -> @@ -591,19 +592,19 @@ let vernac_inductive cum poly lo finite indl = | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") in let indl = List.map unpack indl in - do_mutual_inductive indl is_cumulative poly lo finite + do_mutual_inductive indl is_cumulative atts.polymorphic lo finite -let vernac_fixpoint locality poly local l = - let local = enforce_locality_exp locality local in +let vernac_fixpoint ~atts local l = + let local = enforce_locality_exp atts.locality local in if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - do_fixpoint local poly l + do_fixpoint local atts.polymorphic l -let vernac_cofixpoint locality poly local l = - let local = enforce_locality_exp locality local in +let vernac_cofixpoint ~atts local l = + let local = enforce_locality_exp atts.locality local in if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - do_cofixpoint local poly l + do_cofixpoint local atts.polymorphic l let vernac_scheme l = if Dumpglob.dump () then @@ -621,19 +622,19 @@ let vernac_combined_scheme lid l = List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l); Indschemes.do_combined_scheme lid l -let vernac_universe loc poly l = - if poly && not (Lib.sections_are_opened ()) then - user_err ?loc ~hdr:"vernac_universe" +let vernac_universe ~atts l = + if atts.polymorphic && not (Lib.sections_are_opened ()) then + user_err ?loc:atts.loc ~hdr:"vernac_universe" (str"Polymorphic universes can only be declared inside sections, " ++ str "use Monomorphic Universe instead"); - do_universe poly l + do_universe atts.polymorphic l -let vernac_constraint loc poly l = - if poly && not (Lib.sections_are_opened ()) then - user_err ?loc ~hdr:"vernac_constraint" +let vernac_constraint ~atts l = + if atts.polymorphic && not (Lib.sections_are_opened ()) then + user_err ?loc:atts.loc ~hdr:"vernac_constraint" (str"Polymorphic universe constraints can only be declared" ++ str " inside sections, use Monomorphic Constraint instead"); - do_constraint poly l + do_constraint atts.polymorphic l (**********************) (* Modules *) @@ -811,32 +812,32 @@ let vernac_require from import qidl = let vernac_canonical r = Recordops.declare_canonical_structure (smart_global r) -let vernac_coercion locality poly local ref qids qidt = - let local = enforce_locality locality local in +let vernac_coercion ~atts local ref qids qidt = + let local = enforce_locality atts.locality local in let target = cl_of_qualid qidt in let source = cl_of_qualid qids in let ref' = smart_global ref in - Class.try_add_new_coercion_with_target ref' ~local poly ~source ~target; + Class.try_add_new_coercion_with_target ref' ~local atts.polymorphic ~source ~target; Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion") -let vernac_identity_coercion locality poly local id qids qidt = - let local = enforce_locality locality local in +let vernac_identity_coercion ~atts local id qids qidt = + let local = enforce_locality atts.locality local in let target = cl_of_qualid qidt in let source = cl_of_qualid qids in - Class.try_add_new_identity_coercion id ~local poly ~source ~target + Class.try_add_new_identity_coercion id ~local atts.polymorphic ~source ~target (* Type classes *) -let vernac_instance abst locality poly sup inst props pri = - let global = not (make_section_locality locality) in +let vernac_instance ~atts abst sup inst props pri = + let global = not (make_section_locality atts.locality) in Dumpglob.dump_constraint inst false "inst"; - ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri) + ignore(Classes.new_instance ~abstract:abst ~global atts.polymorphic sup inst props pri) -let vernac_context poly l = - if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom +let vernac_context ~atts l = + if not (Classes.context atts.polymorphic l) then Feedback.feedback Feedback.AddedAxiom -let vernac_declare_instances locality insts = - let glob = not (make_section_locality locality) in +let vernac_declare_instances ~atts insts = + let glob = not (make_section_locality atts.locality) in List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts let vernac_declare_class id = @@ -904,8 +905,8 @@ let vernac_remove_loadpath path = let vernac_add_ml_path isrec path = (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (expand path) -let vernac_declare_ml_module locality l = - let local = make_locality locality in +let vernac_declare_ml_module ~atts l = + let local = make_locality atts.locality in Mltop.declare_ml_modules local (List.map expand l) let vernac_chdir = function @@ -938,25 +939,25 @@ let vernac_restore_state file = (************) (* Commands *) -let vernac_create_hintdb locality id b = - let local = make_module_locality locality in +let vernac_create_hintdb ~atts id b = + let local = make_module_locality atts.locality in Hints.create_hint_db local id full_transparent_state b -let vernac_remove_hints locality dbs ids = - let local = make_module_locality locality in +let vernac_remove_hints ~atts dbs ids = + let local = make_module_locality atts.locality in Hints.remove_hints local dbs (List.map Smartlocate.global_with_alias ids) -let vernac_hints locality poly local lb h = - let local = enforce_module_locality locality local in - Hints.add_hints local lb (Hints.interp_hints poly h) +let vernac_hints ~atts local lb h = + let local = enforce_module_locality atts.locality local in + Hints.add_hints local lb (Hints.interp_hints atts.polymorphic h) -let vernac_syntactic_definition locality lid x local y = +let vernac_syntactic_definition ~atts lid x local y = Dumpglob.dump_definition lid false "syndef"; - let local = enforce_module_locality locality local in + let local = enforce_module_locality atts.locality local in Metasyntax.add_syntactic_definition (Global.env()) (snd lid) x local y -let vernac_declare_implicits locality r l = - let local = make_section_locality locality in +let vernac_declare_implicits ~atts r l = + let local = make_section_locality atts.locality in match l with | [] -> Impargs.declare_implicits local (smart_global r) @@ -976,7 +977,7 @@ let warn_arguments_assert = (* [nargs_for_red] is the number of arguments required to trigger reduction, [args] is the main list of arguments statuses, [more_implicits] is a list of extra lists of implicit statuses *) -let vernac_arguments locality reference args more_implicits nargs_for_red flags = +let vernac_arguments ~atts reference args more_implicits nargs_for_red flags = let assert_flag = List.mem `Assert flags in let rename_flag = List.mem `Rename flags in let clear_scopes_flag = List.mem `ClearScopes flags in @@ -1184,7 +1185,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags (* Actions *) if renaming_specified then begin - let local = make_section_locality locality in + let local = make_section_locality atts.locality in Arguments_renaming.rename_arguments local sr names end; @@ -1194,20 +1195,20 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags with UserError _ -> Notation.find_delimiters_scope ?loc k)) scopes in - vernac_arguments_scope locality reference scopes + vernac_arguments_scope ~atts reference scopes end; if implicits_specified || clear_implicits_flag then - vernac_declare_implicits locality reference implicits; + vernac_declare_implicits ~atts reference implicits; if default_implicits_flag then - vernac_declare_implicits locality reference []; + vernac_declare_implicits ~atts reference []; if red_modifiers_specified then begin match sr with | ConstRef _ as c -> Reductionops.ReductionBehaviour.set - (make_section_locality locality) c + (make_section_locality atts.locality) c (rargs, Option.default ~-1 nargs_for_red, red_flags) | _ -> user_err (strbrk "Modifiers of the behavior of the simpl tactic "++ @@ -1235,8 +1236,8 @@ let vernac_reserve bl = Reserve.declare_reserved_type idl t) in List.iter sb_decl bl -let vernac_generalizable locality = - let local = make_non_locality locality in +let vernac_generalizable ~atts = + let local = make_non_locality atts.locality in Implicit_quantifiers.declare_generalizable local let _ = @@ -1473,8 +1474,8 @@ let _ = optread = Nativenorm.get_profiling_enabled; optwrite = Nativenorm.set_profiling_enabled } -let vernac_set_strategy locality l = - let local = make_locality locality in +let vernac_set_strategy ~atts l = + let local = make_locality atts.locality in let glob_ref r = match smart_global r with | ConstRef sp -> EvalConstRef sp @@ -1484,8 +1485,8 @@ let vernac_set_strategy locality l = let l = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) l in Redexpr.set_strategy local l -let vernac_set_opacity locality (v,l) = - let local = make_non_locality locality in +let vernac_set_opacity ~atts (v,l) = + let local = make_non_locality atts.locality in let glob_ref r = match smart_global r with | ConstRef sp -> EvalConstRef sp @@ -1495,18 +1496,18 @@ let vernac_set_opacity locality (v,l) = let l = List.map glob_ref l in Redexpr.set_strategy local [v,l] -let vernac_set_option locality key = function - | StringValue s -> set_string_option_value_gen locality key s - | StringOptValue (Some s) -> set_string_option_value_gen locality key s - | StringOptValue None -> unset_option_value_gen locality key - | IntValue n -> set_int_option_value_gen locality key n - | BoolValue b -> set_bool_option_value_gen locality key b +let vernac_set_option ~atts key = function + | StringValue s -> set_string_option_value_gen atts.locality key s + | StringOptValue (Some s) -> set_string_option_value_gen atts.locality key s + | StringOptValue None -> unset_option_value_gen atts.locality key + | IntValue n -> set_int_option_value_gen atts.locality key n + | BoolValue b -> set_bool_option_value_gen atts.locality key b -let vernac_set_append_option locality key s = - set_string_option_append_value_gen locality key s +let vernac_set_append_option ~atts key s = + set_string_option_append_value_gen atts.locality key s -let vernac_unset_option locality key = - unset_option_value_gen locality key +let vernac_unset_option ~atts key = + unset_option_value_gen atts.locality key let vernac_add_option key lv = let f = function @@ -1547,8 +1548,8 @@ let query_command_selector ?loc = function | _ -> user_err ?loc ~hdr:"query_command_selector" (str "Query commands only support the single numbered goal selector.") -let vernac_check_may_eval ?loc redexp glopt rc = - let glopt = query_command_selector ?loc glopt in +let vernac_check_may_eval ~atts redexp glopt rc = + let glopt = query_command_selector ?loc:atts.loc glopt in let (sigma, env) = get_current_context_of_args glopt in let sigma', c = interp_open_constr env sigma rc in let c = EConstr.Unsafe.to_constr c in @@ -1582,8 +1583,8 @@ let vernac_check_may_eval ?loc redexp glopt rc = in Feedback.msg_notice (print_eval redfun env sigma' rc j) -let vernac_declare_reduction locality s r = - let local = make_locality locality in +let vernac_declare_reduction ~atts s r = + let local = make_locality atts.locality in declare_red_expr local s (snd (Hook.get f_interp_redexp (Global.env()) Evd.empty r)) (* The same but avoiding the current goal context if any *) @@ -1637,8 +1638,10 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt = let sigma, env = Pfedit.get_current_context () in print_about env sigma ref_or_by_not udecl - -let vernac_print ?loc env sigma = let open Feedback in function +let vernac_print ~atts env sigma = + let open Feedback in + let loc = atts.loc in + function | PrintTables -> msg_notice (print_tables ()) | PrintFullContext-> msg_notice (print_full_context_typ env sigma) | PrintSectionContext qid -> msg_notice (print_sec_context_typ env sigma qid) @@ -1747,8 +1750,8 @@ let _ = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } -let vernac_search ?loc s gopt r = - let gopt = query_command_selector ?loc gopt in +let vernac_search ~atts s gopt r = + let gopt = query_command_selector ?loc:atts.loc gopt in let r = interp_search_restriction r in let env,gopt = match gopt with | None -> @@ -1915,7 +1918,8 @@ let vernac_load interp fname = * 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. *) -let interp ?proof ?loc locality poly st c = +let interp ?proof ~atts ~st c = + let open Vernacinterp in vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c); match c with (* The below vernac are candidates for removal from the main type @@ -1955,30 +1959,30 @@ let interp ?proof ?loc locality poly st c = (* Syntax *) | VernacSyntaxExtension (infix, local,sl) -> - vernac_syntax_extension locality local infix sl + vernac_syntax_extension atts local infix sl | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl - | VernacOpenCloseScope (local, s) -> vernac_open_close_scope locality local s - | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope locality qid scl - | VernacInfix (local,mv,qid,sc) -> vernac_infix locality local mv qid sc + | VernacOpenCloseScope (local, s) -> vernac_open_close_scope ~atts local s + | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope ~atts qid scl + | VernacInfix (local,mv,qid,sc) -> vernac_infix ~atts local mv qid sc | VernacNotation (local,c,infpl,sc) -> - vernac_notation locality local c infpl sc + vernac_notation ~atts local c infpl sc | VernacNotationAddFormat(n,k,v) -> Metasyntax.add_notation_extra_printing_rule n k v (* Gallina *) - | VernacDefinition (k,lid,d) -> vernac_definition locality poly k lid d - | VernacStartTheoremProof (k,l) -> vernac_start_proof locality poly k l + | VernacDefinition (k,lid,d) -> vernac_definition ~atts k lid d + | VernacStartTheoremProof (k,l) -> vernac_start_proof ~atts k l | VernacEndProof e -> vernac_end_proof ?proof e | VernacExactProof c -> vernac_exact_proof c - | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl - | VernacInductive (cum, priv,finite,l) -> vernac_inductive cum poly priv finite l - | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l - | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l + | VernacAssumption (stre,nl,l) -> vernac_assumption ~atts stre l nl + | VernacInductive (cum, priv,finite,l) -> vernac_inductive ~atts cum priv finite l + | VernacFixpoint (local, l) -> vernac_fixpoint ~atts local l + | VernacCoFixpoint (local, l) -> vernac_cofixpoint ~atts local l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l - | VernacUniverse l -> vernac_universe loc poly l - | VernacConstraint l -> vernac_constraint loc poly l + | VernacUniverse l -> vernac_universe ~atts l + | VernacConstraint l -> vernac_constraint ~atts l (* Modules *) | VernacDeclareModule (export,lid,bl,mtyo) -> @@ -1999,15 +2003,15 @@ let interp ?proof ?loc locality poly st c = | VernacRequire (from, export, qidl) -> vernac_require from export qidl | VernacImport (export,qidl) -> vernac_import export qidl | VernacCanonical qid -> vernac_canonical qid - | VernacCoercion (local,r,s,t) -> vernac_coercion locality poly local r s t + | VernacCoercion (local,r,s,t) -> vernac_coercion ~atts local r s t | VernacIdentityCoercion (local,(_,id),s,t) -> - vernac_identity_coercion locality poly local id s t + vernac_identity_coercion ~atts local id s t (* Type classes *) | VernacInstance (abst, sup, inst, props, info) -> - vernac_instance abst locality poly sup inst props info - | VernacContext sup -> vernac_context poly sup - | VernacDeclareInstances insts -> vernac_declare_instances locality insts + vernac_instance ~atts abst sup inst props info + | VernacContext sup -> vernac_context ~atts sup + | VernacDeclareInstances insts -> vernac_declare_instances ~atts insts | VernacDeclareClass id -> vernac_declare_class id (* Solving *) @@ -2017,7 +2021,7 @@ let interp ?proof ?loc locality poly st c = | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias | VernacRemoveLoadPath s -> vernac_remove_loadpath s | VernacAddMLPath (isrec,s) -> vernac_add_ml_path isrec s - | VernacDeclareMLModule l -> vernac_declare_ml_module locality l + | VernacDeclareMLModule l -> vernac_declare_ml_module ~atts l | VernacChdir s -> vernac_chdir s (* State management *) @@ -2025,40 +2029,40 @@ let interp ?proof ?loc locality poly st c = | VernacRestoreState s -> vernac_restore_state s (* Commands *) - | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b - | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids + | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb ~atts dbname b + | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints ~atts dbnames ids | VernacHints (local,dbnames,hints) -> - vernac_hints locality poly local dbnames hints + vernac_hints ~atts local dbnames hints | VernacSyntacticDefinition (id,c,local,b) -> - vernac_syntactic_definition locality id c local b + vernac_syntactic_definition ~atts id c local b | VernacDeclareImplicits (qid,l) -> - vernac_declare_implicits locality qid l + vernac_declare_implicits ~atts qid l | VernacArguments (qid, args, more_implicits, nargs, flags) -> - vernac_arguments locality qid args more_implicits nargs flags + vernac_arguments ~atts qid args more_implicits nargs flags | VernacReserve bl -> vernac_reserve bl - | VernacGeneralizable gen -> vernac_generalizable locality gen - | VernacSetOpacity qidl -> vernac_set_opacity locality qidl - | VernacSetStrategy l -> vernac_set_strategy locality l - | VernacSetOption (key,v) -> vernac_set_option locality key v - | VernacSetAppendOption (key,v) -> vernac_set_append_option locality key v - | VernacUnsetOption key -> vernac_unset_option locality key + | VernacGeneralizable gen -> vernac_generalizable ~atts gen + | VernacSetOpacity qidl -> vernac_set_opacity ~atts qidl + | VernacSetStrategy l -> vernac_set_strategy ~atts l + | VernacSetOption (key,v) -> vernac_set_option ~atts key v + | VernacSetAppendOption (key,v) -> vernac_set_append_option ~atts key v + | VernacUnsetOption key -> vernac_unset_option ~atts key | VernacRemoveOption (key,v) -> vernac_remove_option key v | VernacAddOption (key,v) -> vernac_add_option key v | VernacMemOption (key,v) -> vernac_mem_option key v | VernacPrintOption key -> vernac_print_option key - | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ?loc r g c - | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r + | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ~atts r g c + | VernacDeclareReduction (s,r) -> vernac_declare_reduction ~atts s r | VernacGlobalCheck c -> vernac_global_check c | VernacPrint p -> let sigma, env = Pfedit.get_current_context () in - vernac_print ?loc env sigma p - | VernacSearch (s,g,r) -> vernac_search ?loc s g r + vernac_print ~atts env sigma p + | VernacSearch (s,g,r) -> vernac_search ~atts s g r | VernacLocate l -> vernac_locate l | VernacRegister (id, r) -> vernac_register id r | VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n") (* Proof management *) - | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)] + | VernacGoal t -> vernac_start_proof ~atts Theorem [None,([],t)] | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () | VernacUnfocused -> vernac_unfocused () @@ -2071,7 +2075,7 @@ let interp ?proof ?loc locality poly st c = let using = Option.append using (Proof_using.get_default_proof_using ()) in let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in let usings = if Option.is_empty using then "using:no" else "using:yes" in - Aux_file.record_in_aux_at ?loc "VernacProof" (tacs^" "^usings); + Aux_file.record_in_aux_at ?loc:atts.loc "VernacProof" (tacs^" "^usings); Option.iter vernac_set_end_tac tac; Option.iter vernac_set_used_variables using | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"] @@ -2079,7 +2083,7 @@ let interp ?proof ?loc locality poly st c = (* Extensions *) | VernacExtend (opn,args) -> (* XXX: Here we are returning the state! :) *) - let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) ~st in + let _st : Vernacstate.t = Vernacinterp.call ~atts opn args ~st in () (* Vernaculars that take a locality flag *) @@ -2111,7 +2115,7 @@ let check_vernac_supports_polymorphism c p = | None, _ -> () | Some _, ( VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _ - | VernacAssumption _ | VernacInductive _ + | VernacAssumption _ | VernacInductive _ | VernacStartTheoremProof _ | VernacCoercion _ | VernacIdentityCoercion _ | VernacInstance _ | VernacDeclareInstances _ @@ -2120,7 +2124,7 @@ let check_vernac_supports_polymorphism c p = | Some _, _ -> user_err Pp.(str "This command does not support Polymorphism") let enforce_polymorphism = function - | None -> Flags.is_universe_polymorphism () + | None -> Flags.is_universe_polymorphism () | Some b -> Flags.make_polymorphic_flag b; b (** A global default timeout, controlled by option "Set Default Timeout n". @@ -2188,42 +2192,57 @@ let with_fail st b f = | _ -> assert false end -let interp ?(verbosely=true) ?proof st (loc,c) = +let interp ?(verbosely=true) ?proof ~st (loc,c) = let orig_program_mode = Flags.is_program_mode () in - let rec aux ?locality ?polymorphism isprogcmd = function - - | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c - | VernacProgram _ -> user_err Pp.(str "Program mode specified twice") - | VernacLocal (b, c) when Option.is_empty locality -> - aux ~locality:b ?polymorphism isprogcmd c - | VernacPolymorphic (b, c) when polymorphism = None -> - aux ?locality ~polymorphism:b isprogcmd c - | VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice") - | VernacLocal _ -> user_err Pp.(str "Locality specified twice") + let rec aux ?polymorphism ~atts isprogcmd = function + + | VernacProgram c when not isprogcmd -> + aux ?polymorphism ~atts true c + + | VernacProgram _ -> + user_err Pp.(str "Program mode specified twice") + + | VernacPolymorphic (b, c) when polymorphism = None -> + aux ~polymorphism:b ~atts:atts isprogcmd c + + | VernacPolymorphic (b, c) -> + user_err Pp.(str "Polymorphism specified twice") + + | VernacLocal (b, c) when Option.is_empty atts.locality -> + aux ?polymorphism ~atts:{atts with locality = Some b} isprogcmd c + + | VernacLocal _ -> + user_err Pp.(str "Locality specified twice") + | VernacFail v -> - with_fail st true (fun () -> aux ?locality ?polymorphism isprogcmd v) + with_fail st true (fun () -> aux ?polymorphism ~atts isprogcmd v) + | VernacTimeout (n,v) -> - current_timeout := Some n; - aux ?locality ?polymorphism isprogcmd v + current_timeout := Some n; + aux ?polymorphism ~atts isprogcmd v + | VernacRedirect (s, (_,v)) -> - Topfmt.with_output_to_file s (aux ?locality ?polymorphism isprogcmd) v + Topfmt.with_output_to_file s (aux ?polymorphism ~atts isprogcmd) v + | VernacTime (_,v) -> - System.with_time !Flags.time - (aux ?locality ?polymorphism isprogcmd) v; - | VernacLoad (_,fname) -> vernac_load (aux false) fname - | c -> - check_vernac_supports_locality c locality; - check_vernac_supports_polymorphism c polymorphism; - let poly = enforce_polymorphism polymorphism in - Obligations.set_program_mode isprogcmd; - try - vernac_timeout begin fun () -> + System.with_time !Flags.time (aux ?polymorphism ~atts isprogcmd) v; + + | VernacLoad (_,fname) -> vernac_load (aux ?polymorphism ~atts false) fname + + | c -> + check_vernac_supports_locality c atts.locality; + check_vernac_supports_polymorphism c polymorphism; + let polymorphic = enforce_polymorphism polymorphism in + Obligations.set_program_mode isprogcmd; + try + vernac_timeout begin fun () -> + let atts = { atts with polymorphic } in if verbosely - then Flags.verbosely (interp ?proof ?loc locality poly st) c - else Flags.silently (interp ?proof ?loc locality poly st) c; + then Flags.verbosely (interp ?proof ~atts ~st) c + else Flags.silently (interp ?proof ~atts ~st) c; if orig_program_mode || not !Flags.program_mode || isprogcmd then Flags.program_mode := orig_program_mode; - ignore (Flags.use_polymorphic_flag ()) + ignore (Flags.use_polymorphic_flag ()) end with | reraise when @@ -2238,12 +2257,14 @@ let interp ?(verbosely=true) ?proof st (loc,c) = ignore (Flags.use_polymorphic_flag ()); iraise e in - if verbosely then Flags.verbosely (aux false) c - else aux false c + 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 (* XXX: There is a bug here in case of an exception, see @gares comments on the PR *) -let interp ?verbosely ?proof st cmd = +let interp ?verbosely ?proof ~st cmd = Vernacstate.unfreeze_interp_state st; - interp ?verbosely ?proof st cmd; + interp ?verbosely ?proof ~st cmd; Vernacstate.freeze_interp_state `No |