aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacentries.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacentries.ml')
-rw-r--r--vernac/vernacentries.ml570
1 files changed, 295 insertions, 275 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 41f63644d..161e0c535 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
@@ -56,20 +57,19 @@ let scope_class_of_qualid qid =
let show_proof () =
(* spiwack: this would probably be cooler with a bit of polishing. *)
let p = Proof_global.give_me_the_proof () in
+ let sigma, env = Pfedit.get_current_context () in
let pprf = Proof.partial_proof p in
- Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf)
+ Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
let show_top_evars () =
(* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
let pfts = Proof_global.give_me_the_proof () in
- let gls = Proof.V82.subgoals pfts in
- let sigma = gls.Evd.sigma in
+ let gls,_,_,_,sigma = Proof.proof pfts in
Feedback.msg_notice (pr_evars_int sigma 1 (Evd.undefined_map sigma))
let show_universes () =
let pfts = Proof_global.give_me_the_proof () in
- let gls = Proof.V82.subgoals pfts in
- let sigma = gls.Evd.sigma in
+ let gls,_,_,_,sigma = Proof.proof pfts in
let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma));
Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx)
@@ -78,16 +78,16 @@ let show_universes () =
let show_intro all =
let open EConstr in
let pf = Proof_global.give_me_the_proof() in
- let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
+ let gls,_,_,_,sigma = Proof.proof pf in
if not (List.is_empty gls) then begin
let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in
if all then
let lid = Tactics.find_intro_names l gl in
- Feedback.msg_notice (hov 0 (prlist_with_sep spc pr_id lid))
+ Feedback.msg_notice (hov 0 (prlist_with_sep spc Id.print lid))
else if not (List.is_empty l) then
let n = List.last l in
- Feedback.msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
+ Feedback.msg_notice (Id.print (List.hd (Tactics.find_intro_names [n] gl)))
end
(** Prepare a "match" template for a given inductive type.
@@ -153,8 +153,8 @@ let show_match id =
(* "Print" commands *)
let print_path_entry p =
- let dir = pr_dirpath (Loadpath.logical p) in
- let path = str (Loadpath.physical p) in
+ let dir = DirPath.print (Loadpath.logical p) in
+ let path = str (CUnix.escaped_string_of_physical_path (Loadpath.physical p)) in
Pp.hov 2 (dir ++ spc () ++ path)
let print_loadpath dir =
@@ -176,9 +176,9 @@ let print_modules () =
let loaded_opened = List.intersect DirPath.equal opened loaded
and only_loaded = List.subtract DirPath.equal loaded opened in
str"Loaded and imported library files: " ++
- pr_vertical_list pr_dirpath loaded_opened ++ fnl () ++
+ pr_vertical_list DirPath.print loaded_opened ++ fnl () ++
str"Loaded and not imported library files: " ++
- pr_vertical_list pr_dirpath only_loaded
+ pr_vertical_list DirPath.print only_loaded
let print_module r =
@@ -186,8 +186,8 @@ let print_module r =
try
let globdir = Nametab.locate_dir qid in
match globdir with
- DirModule (dirpath,(mp,_)) ->
- Feedback.msg_notice (Printmod.print_module (Printmod.printable_body dirpath) mp)
+ DirModule { obj_dir; obj_mp; _ } ->
+ Feedback.msg_notice (Printmod.print_module (Printmod.printable_body obj_dir) obj_mp)
| _ -> raise Not_found
with
Not_found -> Feedback.msg_error (str"Unknown Module " ++ pr_qualid qid)
@@ -250,14 +250,15 @@ let print_namespace ns =
let print_list pr l = prlist_with_sep (fun () -> str".") pr l in
let print_kn kn =
(* spiwack: I'm ignoring the dirpath, is that bad? *)
- let (mp,_,lbl) = Names.repr_kn kn in
+ let (mp,_,lbl) = Names.KerName.repr kn in
let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in
- print_list pr_id qn
+ print_list Id.print qn
in
let print_constant k body =
(* FIXME: universes *)
let t = body.Declarations.const_type in
- print_kn k ++ str":" ++ spc() ++ Printer.pr_type t
+ let sigma, env = Pfedit.get_current_context () in
+ print_kn k ++ str":" ++ spc() ++ Printer.pr_type_env env sigma t
in
let matches mp = match match_modulepath ns mp with
| Some [] -> true
@@ -265,14 +266,14 @@ let print_namespace ns =
let constants = (Environ.pre_env (Global.env ())).Pre_env.env_globals.Pre_env.env_constants in
let constants_in_namespace =
Cmap_env.fold (fun c (body,_) acc ->
- let kn = user_con c in
- if matches (modpath kn) then
+ let kn = Constant.user c in
+ if matches (KerName.modpath kn) then
acc++fnl()++hov 2 (print_constant kn body)
else
acc
) constants (str"")
in
- Feedback.msg_notice ((print_list pr_id ns)++str":"++fnl()++constants_in_namespace)
+ Feedback.msg_notice ((print_list Id.print ns)++str":"++fnl()++constants_in_namespace)
let print_strategy r =
let open Conv_oracle in
@@ -361,29 +362,29 @@ let locate_file f =
let msg_found_library = function
| Library.LibLoaded, fulldir, file ->
Feedback.msg_info (hov 0
- (pr_dirpath fulldir ++ strbrk " has been loaded from file " ++
+ (DirPath.print fulldir ++ strbrk " has been loaded from file " ++
str file))
| Library.LibInPath, fulldir, file ->
Feedback.msg_info (hov 0
- (pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file))
+ (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file))
let err_unmapped_library ?loc ?from qid =
let dir = fst (repr_qualid qid) in
let prefix = match from with
| None -> str "."
| Some from ->
- str " and prefix " ++ pr_dirpath from ++ str "."
+ str " and prefix " ++ DirPath.print from ++ str "."
in
user_err ?loc
~hdr:"locate_library"
(strbrk "Cannot find a physical path bound to logical path matching suffix " ++
- pr_dirpath dir ++ prefix)
+ DirPath.print dir ++ prefix)
let err_notfound_library ?loc ?from qid =
let prefix = match from with
| None -> str "."
| Some from ->
- str " with prefix " ++ pr_dirpath from ++ str "."
+ str " with prefix " ++ DirPath.print from ++ str "."
in
user_err ?loc ~hdr:"locate_library"
(strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
@@ -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 infix l =
+ let local = enforce_module_locality atts.locality 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 (b,s) =
+ let local = enforce_section_locality atts.locality 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 =
+ let local = enforce_module_locality atts.locality in
Metasyntax.add_infix local (Global.env())
-let vernac_notation locality local =
- let local = enforce_module_locality locality local in
+let vernac_notation ~atts =
+ let local = enforce_module_locality atts.locality 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 discharge kind ((loc,id as lid),pl) def =
+ let local = enforce_locality_exp atts.locality discharge in
+ let hook = vernac_definition_hook atts.polymorphic kind 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 kind)
[Some (lid,pl), (bl,t)] hook
| DefineBody (bl,red_option,c,typ_opt) ->
- let red_option = match red_option with
+ let red_option = match red_option with
| None -> None
| Some r ->
- let (evc,env)= get_current_context () in
- Some (snd (Hook.get f_interp_redexp env evc r)) in
- do_definition id (local,p,k) pl bl red_option c typ_opt hook)
+ let sigma, env = Pfedit.get_current_context () in
+ Some (snd (Hook.get f_interp_redexp env sigma r)) in
+ do_definition id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook)
-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 NoDischarge 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 discharge kind l nl =
+ let local = enforce_locality_exp atts.locality discharge 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 discharge l =
+ let local = enforce_locality_exp atts.locality discharge in
if Dumpglob.dump () then
List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
- 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 discharge l =
+ let local = enforce_locality_exp atts.locality discharge in
if Dumpglob.dump () then
List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
- 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 *)
@@ -656,7 +657,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
id binders_ast (Enforce mty_ast) []
in
Dumpglob.dump_moddef ?loc mp "mod";
- Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared");
+ Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export
let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
@@ -678,7 +679,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
in
Dumpglob.dump_moddef ?loc mp "mod";
Flags.if_verbose Feedback.msg_info
- (str "Interactive Module " ++ pr_id id ++ str " started");
+ (str "Interactive Module " ++ Id.print id ++ str " started");
List.iter
(fun (export,id) ->
Option.iter
@@ -696,14 +697,14 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
in
Dumpglob.dump_moddef ?loc mp "mod";
Flags.if_verbose Feedback.msg_info
- (str "Module " ++ pr_id id ++ str " is defined");
+ (str "Module " ++ Id.print id ++ str " is defined");
Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)])
export
let vernac_end_module export (loc,id as lid) =
let mp = Declaremods.end_module () in
Dumpglob.dump_modref ?loc mp "mod";
- Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined");
+ Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined");
Option.iter (fun export -> vernac_import export [Ident lid]) export
let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
@@ -725,7 +726,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
in
Dumpglob.dump_moddef ?loc mp "modtype";
Flags.if_verbose Feedback.msg_info
- (str "Interactive Module Type " ++ pr_id id ++ str " started");
+ (str "Interactive Module Type " ++ Id.print id ++ str " started");
List.iter
(fun (export,id) ->
Option.iter
@@ -744,12 +745,12 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
in
Dumpglob.dump_moddef ?loc mp "modtype";
Flags.if_verbose Feedback.msg_info
- (str "Module Type " ++ pr_id id ++ str " is defined")
+ (str "Module Type " ++ Id.print id ++ str " is defined")
let vernac_end_modtype (loc,id) =
let mp = Declaremods.end_modtype () in
Dumpglob.dump_modref ?loc mp "modtype";
- Flags.if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
+ Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined")
let vernac_include l =
Declaremods.declare_include Modintern.interp_module_ast l
@@ -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 ref qids qidt =
+ let local = enforce_locality atts.locality 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 id qids qidt =
+ let local = enforce_locality atts.locality 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 =
@@ -874,7 +875,7 @@ let vernac_set_used_variables e =
List.iter (fun id ->
if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
user_err ~hdr:"vernac_set_used_variables"
- (str "Unknown variable: " ++ pr_id id))
+ (str "Unknown variable: " ++ Id.print id))
l;
let _, to_clear = Proof_global.set_used_variables l in
let to_clear = List.map snd to_clear in
@@ -893,7 +894,7 @@ let expand filename =
let vernac_add_loadpath implicit pdir ldiropt =
let pdir = expand pdir in
- let alias = Option.default Nameops.default_root_prefix ldiropt in
+ let alias = Option.default Libnames.default_root_prefix ldiropt in
Mltop.add_rec_path Mltop.AddTopML ~unix_path:pdir ~coq_root:alias ~implicit
let vernac_remove_loadpath path =
@@ -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 lb h =
+ let local = enforce_module_locality atts.locality 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 y =
Dumpglob.dump_definition lid false "syndef";
- let local = enforce_module_locality locality local in
+ let local = enforce_module_locality atts.locality 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
@@ -1539,7 +1540,7 @@ let vernac_print_option key =
let get_current_context_of_args = function
| Some n -> Pfedit.get_goal_context n
- | None -> get_current_context ()
+ | None -> Pfedit.get_current_context ()
let query_command_selector ?loc = function
| None -> None
@@ -1547,16 +1548,16 @@ 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
let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in
Evarconv.check_problems_are_solved env sigma';
let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
- let pl, uctx = Evd.universe_context ~names:[] ~extensible:true sigma' in
- let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in
+ let uctx = Evd.universe_context_set sigma' in
+ let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in
let c = nf c in
let j =
if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then
@@ -1572,7 +1573,7 @@ let vernac_check_may_eval ?loc redexp glopt rc =
let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
Feedback.msg_notice (print_judgment env sigma' j ++
pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
- Printer.pr_universe_ctx sigma uctx)
+ Printer.pr_universe_ctx_set sigma uctx)
| Some r ->
let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in
let redfun env evm c =
@@ -1582,26 +1583,27 @@ 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 *)
let vernac_global_check c =
let env = Global.env() in
let sigma = Evd.from_env env in
- let c,ctx = interp_constr env sigma c in
+ let c,uctx = interp_constr env sigma c in
let senv = Global.safe_env() in
- let cstrs = snd (UState.context_set ctx) in
- let senv = Safe_typing.add_constraints cstrs senv in
+ let uctx = UState.context_set uctx in
+ let senv = Safe_typing.push_context_set false uctx senv in
let j = Safe_typing.typing senv c in
let env = Safe_typing.env_of_safe_env senv in
- Feedback.msg_notice (print_safe_judgment env sigma j)
+ Feedback.msg_notice (print_safe_judgment env sigma j ++
+ pr_universe_ctx_set sigma uctx)
let get_nth_goal n =
let pf = Proof_global.give_me_the_proof() in
- let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
+ let gls,_,_,_,sigma = Proof.proof pf in
let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in
gl
@@ -1609,9 +1611,10 @@ exception NoHyp
(* Printing "About" information of a hypothesis of the current goal.
We only print the type and a small statement to this comes from the
goal. Precondition: there must be at least one current goal. *)
-let print_about_hyp_globs ?loc ref_or_by_not glopt =
+let print_about_hyp_globs ?loc ref_or_by_not udecl glopt =
let open Context.Named.Declaration in
try
+ (* FIXME error on non None udecl if we find the hyp. *)
let glnumopt = query_command_selector ?loc glopt in
let gl,id =
match glnumopt,ref_or_by_not with
@@ -1628,17 +1631,22 @@ let print_about_hyp_globs ?loc ref_or_by_not glopt =
let natureofid = match decl with
| LocalAssum _ -> "Hypothesis"
| LocalDef (_,bdy,_) ->"Constant (let in)" in
- v 0 (pr_id id ++ str":" ++ pr_econstr (NamedDecl.get_type decl) ++ fnl() ++ fnl()
+ let sigma, env = Pfedit.get_current_context () in
+ v 0 (Id.print id ++ str":" ++ pr_econstr_env env sigma (NamedDecl.get_type decl) ++ fnl() ++ fnl()
++ str natureofid ++ str " of the goal context.")
with (* fallback to globals *)
- | NoHyp | Not_found -> print_about ref_or_by_not
+ | NoHyp | Not_found ->
+ let sigma, env = Pfedit.get_current_context () in
+ print_about env sigma ref_or_by_not udecl
-
-let vernac_print ?loc = 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 ())
- | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid)
- | PrintInspect n -> msg_notice (inspect n)
+ | PrintFullContext-> msg_notice (print_full_context_typ env sigma)
+ | PrintSectionContext qid -> msg_notice (print_sec_context_typ env sigma qid)
+ | PrintInspect n -> msg_notice (inspect env sigma n)
| PrintGrammar ent -> msg_notice (Metasyntax.pr_grammar ent)
| PrintLoadPath dir -> (* For compatibility ? *) msg_notice (print_loadpath dir)
| PrintModules -> msg_notice (print_modules ())
@@ -1648,15 +1656,15 @@ let vernac_print ?loc = let open Feedback in function
| PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ())
| PrintMLModules -> msg_notice (Mltop.print_ml_modules ())
| PrintDebugGC -> msg_notice (Mltop.print_gc ())
- | PrintName qid -> dump_global qid; msg_notice (print_name qid)
- | PrintGraph -> msg_notice (Prettyp.print_graph())
+ | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl)
+ | PrintGraph -> msg_notice (Prettyp.print_graph env sigma)
| PrintClasses -> msg_notice (Prettyp.print_classes())
| PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
| PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c))
- | PrintCoercions -> msg_notice (Prettyp.print_coercions())
+ | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma)
| PrintCoercionPaths (cls,clt) ->
- msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
- | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ())
+ msg_notice (Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt))
+ | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma)
| PrintUniverses (b, dst) ->
let univ = Global.universes () in
let univ = if b then UGraph.sort_universes univ else univ in
@@ -1668,18 +1676,18 @@ let vernac_print ?loc = let open Feedback in function
| None -> msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining)
| Some s -> dump_universes_gen univ s
end
- | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r))
+ | PrintHint r -> msg_notice (Hints.pr_hint_ref env sigma (smart_global r))
| PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ())
- | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s)
- | PrintHintDb -> msg_notice (Hints.pr_searchtable ())
+ | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name env sigma s)
+ | PrintHintDb -> msg_notice (Hints.pr_searchtable env sigma)
| PrintScopes ->
- msg_notice (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr))
+ msg_notice (Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env)))
| PrintScope s ->
- msg_notice (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s)
+ msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
| PrintVisibility s ->
- msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
- | PrintAbout (ref_or_by_not,glnumopt) ->
- msg_notice (print_about_hyp_globs ?loc ref_or_by_not glnumopt)
+ msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
+ | PrintAbout (ref_or_by_not,udecl,glnumopt) ->
+ msg_notice (print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt)
| PrintImplicit qid ->
dump_global qid; msg_notice (print_impargs qid)
| PrintAssumptions (o,t,r) ->
@@ -1689,7 +1697,7 @@ let vernac_print ?loc = let open Feedback in function
let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in
let nassums =
Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in
- msg_notice (Printer.pr_assumptionset (Global.env ()) nassums)
+ msg_notice (Printer.pr_assumptionset env sigma nassums)
| PrintStrategy r -> print_strategy r
let global_module r =
@@ -1743,8 +1751,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 ->
@@ -1780,9 +1788,10 @@ let vernac_locate = let open Feedback in function
| LocateTerm (AN qid) -> msg_notice (print_located_term qid)
| LocateAny (ByNotation (_, (ntn, sc))) (** TODO : handle Ltac notations *)
| LocateTerm (ByNotation (_, (ntn, sc))) ->
- msg_notice
- (Notation.locate_notation
- (Constrextern.without_symbols pr_lglob_constr) ntn sc)
+ let _, env = Pfedit.get_current_context () in
+ msg_notice
+ (Notation.locate_notation
+ (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc)
| LocateLibrary qid -> print_located_library qid
| LocateModule qid -> msg_notice (print_located_module qid)
| LocateOther (s, qid) -> msg_notice (print_located_other s qid)
@@ -1849,17 +1858,18 @@ let vernac_bullet (bullet : Proof_bullet.t) =
let vernac_show = let open Feedback in function
| ShowScript -> assert false (* Only the stm knows the script *)
| ShowGoal goalref ->
+ let proof = Proof_global.give_me_the_proof () in
let info = match goalref with
- | OpenSubgoals -> pr_open_subgoals ()
- | NthGoal n -> pr_nth_open_subgoal n
- | GoalId id -> pr_goal_by_id id
+ | OpenSubgoals -> pr_open_subgoals ~proof
+ | NthGoal n -> pr_nth_open_subgoal ~proof n
+ | GoalId id -> pr_goal_by_id ~proof id
in
msg_notice info
| ShowProof -> show_proof ()
| ShowExistentials -> show_top_evars ()
| ShowUniverses -> show_universes ()
| ShowProofNames ->
- msg_notice (pr_sequence pr_id (Proof_global.get_all_proof_names()))
+ msg_notice (pr_sequence Id.print (Proof_global.get_all_proof_names()))
| ShowIntros all -> show_intro all
| ShowMatch id -> show_match id
@@ -1909,7 +1919,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 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
@@ -1948,31 +1959,33 @@ let interp ?proof ?loc locality poly c =
| VernacLocal _ -> assert false
(* Syntax *)
- | VernacSyntaxExtension (infix, local,sl) ->
- vernac_syntax_extension locality local infix sl
+ | VernacSyntaxExtension (infix, sl) ->
+ vernac_syntax_extension atts 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
- | VernacNotation (local,c,infpl,sc) ->
- vernac_notation locality local c infpl sc
+ | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s)
+ | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope ~atts qid scl
+ | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc
+ | VernacNotation (c,infpl,sc) ->
+ vernac_notation ~atts 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 ((discharge,kind),lid,d) ->
+ vernac_definition ~atts discharge kind 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 ((discharge,kind),nl,l) ->
+ vernac_assumption ~atts discharge kind l nl
+ | VernacInductive (cum, priv,finite,l) -> vernac_inductive ~atts cum priv finite l
+ | VernacFixpoint (discharge, l) -> vernac_fixpoint ~atts discharge l
+ | VernacCoFixpoint (discharge, l) -> vernac_cofixpoint ~atts discharge 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) ->
@@ -1993,15 +2006,15 @@ let interp ?proof ?loc locality poly 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
- | VernacIdentityCoercion (local,(_,id),s,t) ->
- vernac_identity_coercion locality poly local id s t
+ | VernacCoercion (r,s,t) -> vernac_coercion ~atts r s t
+ | VernacIdentityCoercion ((_,id),s,t) ->
+ vernac_identity_coercion ~atts 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 *)
@@ -2011,7 +2024,7 @@ let interp ?proof ?loc locality poly 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 *)
@@ -2019,38 +2032,40 @@ let interp ?proof ?loc locality poly 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
- | VernacHints (local,dbnames,hints) ->
- vernac_hints locality poly local dbnames hints
- | VernacSyntacticDefinition (id,c,local,b) ->
- vernac_syntactic_definition locality id c local b
+ | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb ~atts dbname b
+ | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints ~atts dbnames ids
+ | VernacHints (dbnames,hints) ->
+ vernac_hints ~atts dbnames hints
+ | VernacSyntacticDefinition (id,c,b) ->
+ vernac_syntactic_definition ~atts id c 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 -> vernac_print ?loc p
- | VernacSearch (s,g,r) -> vernac_search ?loc s g r
+ | VernacPrint p ->
+ let sigma, env = Pfedit.get_current_context () in
+ 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 ()
@@ -2063,13 +2078,16 @@ let interp ?proof ?loc locality poly 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"]
(* Extensions *)
- | VernacExtend (opn,args) -> Vernacinterp.call ?locality ?loc (opn,args)
+ | VernacExtend (opn,args) ->
+ (* XXX: Here we are returning the state! :) *)
+ let _st : Vernacstate.t = Vernacinterp.call ~atts opn args ~st in
+ ()
(* Vernaculars that take a locality flag *)
let check_vernac_supports_locality c l =
@@ -2100,7 +2118,7 @@ let check_vernac_supports_polymorphism c p =
| None, _ -> ()
| Some _, (
VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
- | VernacAssumption _ | VernacInductive _
+ | VernacAssumption _ | VernacInductive _
| VernacStartTheoremProof _
| VernacCoercion _ | VernacIdentityCoercion _
| VernacInstance _ | VernacDeclareInstances _
@@ -2109,7 +2127,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".
@@ -2134,7 +2152,7 @@ let vernac_timeout f =
match !current_timeout, !default_timeout with
| Some n, _ | None, Some n ->
let f () = f (); current_timeout := None in
- Control.timeout n f Timeout
+ Control.timeout n f () Timeout
| None, None -> f ()
let restore_timeout () = current_timeout := None
@@ -2147,28 +2165,6 @@ let locate_if_not_already ?loc (e, info) =
exception HasNotFailed
exception HasFailed of Pp.t
-type interp_state = { (* TODO: inline records in OCaml 4.03 *)
- system : States.state; (* summary + libstack *)
- proof : Proof_global.state; (* proof state *)
- shallow : bool (* is the state trimmed down (libstack) *)
-}
-
-let s_cache = ref (States.freeze ~marshallable:`No)
-let s_proof = ref (Proof_global.freeze ~marshallable:`No)
-
-let invalidate_cache () =
- s_cache := Obj.magic 0;
- s_proof := Obj.magic 0
-
-let freeze_interp_state marshallable =
- { system = (s_cache := States.freeze ~marshallable; !s_cache);
- proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof);
- shallow = marshallable = `Shallow }
-
-let unfreeze_interp_state { system; proof } =
- if (!s_cache != system) then (s_cache := system; States.unfreeze system);
- if (!s_proof != proof) then (s_proof := proof; Proof_global.unfreeze proof)
-
(* XXX STATE: this type hints that restoring the state should be the
caller's responsibility *)
let with_fail st b f =
@@ -2187,8 +2183,8 @@ let with_fail st b f =
(ExplainErr.process_vernac_interp_error ~allow_uncaught:false e)))
with e when CErrors.noncritical e ->
(* Restore the previous state XXX Careful here with the cache! *)
- invalidate_cache ();
- unfreeze_interp_state st;
+ Vernacstate.invalidate_cache ();
+ Vernacstate.unfreeze_interp_state st;
let (e, _) = CErrors.push e in
match e with
| HasNotFailed ->
@@ -2199,42 +2195,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) c
- else Flags.silently (interp ?proof ?loc locality poly) 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
@@ -2249,10 +2260,19 @@ 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 interp ?verbosely ?proof st cmd =
- unfreeze_interp_state st;
- interp ?verbosely ?proof st cmd;
- freeze_interp_state `No
+ 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 =
+ Vernacstate.unfreeze_interp_state st;
+ try
+ interp ?verbosely ?proof ~st cmd;
+ Vernacstate.freeze_interp_state `No
+ with exn ->
+ let exn = CErrors.push exn in
+ Vernacstate.invalidate_cache ();
+ iraise exn
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 23:08:45 +0000