aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml109
-rw-r--r--vernac/classes.mli9
-rw-r--r--vernac/egramcoq.ml3
-rw-r--r--vernac/g_vernac.mlg20
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/mltop.ml2
-rw-r--r--vernac/ppvernac.ml17
-rw-r--r--vernac/pvernac.ml38
-rw-r--r--vernac/pvernac.mli28
-rw-r--r--vernac/vernacentries.ml68
-rw-r--r--vernac/vernacentries.mli5
-rw-r--r--vernac/vernacexpr.ml10
-rw-r--r--vernac/vernacextend.ml6
-rw-r--r--vernac/vernacextend.mli6
-rw-r--r--vernac/vernacstate.ml32
-rw-r--r--vernac/vernacstate.mli17
16 files changed, 258 insertions, 114 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index a342f5bf98..748a2628c5 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -28,7 +28,7 @@ module RelDecl = Context.Rel.Declaration
open Decl_kinds
open Entries
-let refine_instance = ref true
+let refine_instance = ref false
let () = Goptions.(declare_bool_option {
optdepr = false;
@@ -105,8 +105,6 @@ let id_of_class cl =
mip.(0).Declarations.mind_typename
| _ -> assert false
-open Pp
-
let instance_hook k info global imps ?hook cst =
Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
let info = intern_info info in
@@ -128,7 +126,7 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t
Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
instance_hook k info global imps ?hook (ConstRef kn)
-let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id =
+let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst id =
let subst = List.fold_left2
(fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
[] subst (snd k.cl_context)
@@ -144,7 +142,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp
(None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
in
Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
- instance_hook k pri global imps ?hook (ConstRef cst); id
+ instance_hook k pri global imps (ConstRef cst)
let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype =
let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
@@ -191,7 +189,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
else ignore (Pfedit.by (Tactics.auto_intros_tac ids));
(match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ()
-let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
+let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
let props =
match props with
| Some (true, { CAst.v = CRecord fs }) ->
@@ -278,69 +276,74 @@ let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~pro
else CErrors.user_err Pp.(str "Unsolved obligations remaining.");
id
-let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~program_mode
- poly ctx (instid, bk, cl) props
- ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
- let env = Global.env() in
- let ({CAst.loc;v=instid}, pl) = instid in
+let interp_instance_context env ctx ?(generalize=false) pl bk cl =
let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
let tclass, ids =
match bk with
| Decl_kinds.Implicit ->
- Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
- (fun avoid (clname, _) ->
- match clname with
- | Some cl ->
- let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in
- t, avoid
- | None -> failwith ("new instance: under-applied typeclass"))
- cl
+ Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
+ (fun avoid (clname, _) ->
+ match clname with
+ | Some cl ->
+ let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in
+ t, avoid
+ | None -> failwith ("new instance: under-applied typeclass"))
+ cl
| Explicit -> cl, Id.Set.empty
in
let tclass =
if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass)
else tclass
in
- let sigma, k, u, cty, ctx', ctx, imps, subst =
- let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in
- let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in
- let len = Context.Rel.nhyps ctx in
- let imps = imps @ Impargs.lift_implicits len imps' in
- let ctx', c = decompose_prod_assum sigma c' in
- let ctx'' = ctx' @ ctx in
- let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in
- let u_s = EInstance.kind sigma u in
- let cl = Typeclasses.typeclass_univ_instance (k, u_s) in
- let args = List.map of_constr args in
- let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in
- let _, args =
- List.fold_right (fun decl (args, args') ->
- match decl with
- | LocalAssum _ -> (List.tl args, List.hd args :: args')
+ let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in
+ let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in
+ let len = Context.Rel.nhyps ctx in
+ let imps = imps @ Impargs.lift_implicits len imps' in
+ let ctx', c = decompose_prod_assum sigma c' in
+ let ctx'' = ctx' @ ctx in
+ let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in
+ let u_s = EInstance.kind sigma u in
+ let cl = Typeclasses.typeclass_univ_instance (k, u_s) in
+ let args = List.map of_constr args in
+ let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in
+ let _, args =
+ List.fold_right (fun decl (args, args') ->
+ match decl with
+ | LocalAssum _ -> (List.tl args, List.hd args :: args')
| LocalDef (_,b,_) -> (args, Vars.substl args' b :: args'))
- cl_context (args, [])
- in
- sigma, cl, u, c', ctx', ctx, imps, args
+ cl_context (args, [])
+ in
+ let sigma = Evarutil.nf_evar_map sigma in
+ let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
+ sigma, cl, u, c', ctx', ctx, imps, args, decl
+
+
+let new_instance ?(global=false) ?(refine= !refine_instance) ~program_mode
+ poly ctx (instid, bk, cl) props
+ ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
+ let env = Global.env() in
+ let ({CAst.loc;v=instid}, pl) = instid in
+ let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
+ interp_instance_context env ~generalize ctx pl bk cl
in
let id =
match instid with
- Name id ->
- let sp = Lib.make_path id in
- if Nametab.exists_cci sp then
- user_err ~hdr:"new_instance" (Id.print id ++ Pp.str " already exists.");
- id
- | Anonymous ->
- let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
- Namegen.next_global_ident_away i (Termops.vars_of_env env)
+ | Name id -> id
+ | Anonymous ->
+ let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
+ Namegen.next_global_ident_away i (Termops.vars_of_env env)
in
let env' = push_rel_context ctx env in
- let sigma = Evarutil.nf_evar_map sigma in
- let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
- if abstract then
- do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id
- else
- do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
- cty k u ctx ctx' pri decl imps subst id props
+ do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
+ cty k u ctx ctx' pri decl imps subst id props
+
+let declare_new_instance ?(global=false) poly ctx (instid, bk, cl) pri =
+ let env = Global.env() in
+ let ({CAst.loc;v=instid}, pl) = instid in
+ let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
+ interp_instance_context env ctx pl bk cl
+ in
+ do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid
let named_of_rel_context l =
let open Vars in
diff --git a/vernac/classes.mli b/vernac/classes.mli
index eb6c0c92e1..6f61da66cf 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -40,7 +40,6 @@ val declare_instance_constant :
unit
val new_instance :
- ?abstract:bool (** Not abstract by default. *) ->
?global:bool (** Not global by default. *) ->
?refine:bool (** Allow refinement *) ->
program_mode:bool ->
@@ -54,6 +53,14 @@ val new_instance :
Hints.hint_info_expr ->
Id.t
+val declare_new_instance :
+ ?global:bool (** Not global by default. *) ->
+ Decl_kinds.polymorphic ->
+ local_binder_expr list ->
+ ident_decl * Decl_kinds.binding_kind * constr_expr ->
+ Hints.hint_info_expr ->
+ unit
+
(** Setting opacity *)
val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 43abc0a200..1a07d74a0e 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -146,7 +146,8 @@ let register_empty_levels accu forpat levels =
(where, ans) :: rem, save_levels accu where nlev
else rem, accu
in
- filter accu levels
+ let (l,accu) = filter accu levels in
+ List.rev l, accu
let find_position accu custom forpat assoc level =
let accu, (clev, plev) = find_levels accu custom in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 22528a607f..79adefdcf7 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -61,7 +61,8 @@ let make_bullet s =
| _ -> assert false
let parse_compat_version = let open Flags in function
- | "8.9" -> Current
+ | "8.10" -> Current
+ | "8.9" -> V8_9
| "8.8" -> V8_8
| "8.7" -> V8_7
| ("8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
@@ -683,19 +684,19 @@ GRAMMAR EXTEND Gram
info = hint_info ;
props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } |
":="; c = lconstr -> { Some (false,c) } | -> { None } ] ->
- { VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) }
+ { VernacInstance (snd namesup,(fst namesup,expl,t),props,info) }
| IDENT "Existing"; IDENT "Instance"; id = global;
info = hint_info ->
- { VernacDeclareInstances [id, info] }
+ { VernacExistingInstance [id, info] }
| IDENT "Existing"; IDENT "Instances"; ids = LIST1 global;
pri = OPT [ "|"; i = natural -> { i } ] ->
{ let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in
let insts = List.map (fun i -> (i, info)) ids in
- VernacDeclareInstances insts }
+ VernacExistingInstance insts }
- | IDENT "Existing"; IDENT "Class"; is = global -> { VernacDeclareClass is }
+ | IDENT "Existing"; IDENT "Class"; is = global -> { VernacExistingClass is }
(* Arguments *)
| IDENT "Arguments"; qid = smart_global;
@@ -809,9 +810,8 @@ GRAMMAR EXTEND Gram
| IDENT "transparent" -> { Conv_oracle.transparent } ] ]
;
instance_name:
- [ [ name = ident_decl; sup = OPT binders ->
- { (CAst.map (fun id -> Name id) (fst name), snd name),
- (Option.default [] sup) }
+ [ [ name = ident_decl; bl = binders ->
+ { (CAst.map (fun id -> Name id) (fst name), snd name), bl }
| -> { ((CAst.make ~loc Anonymous), None), [] } ] ]
;
hint_info:
@@ -845,10 +845,10 @@ GRAMMAR EXTEND Gram
[ [ IDENT "Comments"; l = LIST0 comment -> { VernacComments l }
(* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
- | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
+ | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":";
expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200";
info = hint_info ->
- { VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) }
+ { VernacDeclareInstance (bl, (id, expl, t), info) }
(* Should be in syntax, but camlp5 would not factorize *)
| IDENT "Declare"; IDENT "Scope"; sc = IDENT ->
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 8f155adb8a..0dfbba0e83 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -340,7 +340,7 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
| None -> standard_proof_terminator ?hook compute_guard
| Some terminator -> terminator ?hook compute_guard
in
- let sign =
+ let sign =
match sign with
| Some sign -> sign
| None -> initialize_named_context_for_proof ()
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 8d6268753e..78e26c65d4 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -215,7 +215,7 @@ let add_vo_path ~recursive lp =
let () = match lp.has_ml with
| AddNoML -> ()
| AddTopML -> add_ml_dir unix_path
- | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs in
+ | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs; add_ml_dir unix_path in
let add (path, dir) =
Loadpath.add_load_path path ~implicit dir in
let () = List.iter add dirs in
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e0dd3380f9..5eeeaada2d 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -887,10 +887,9 @@ open Pputils
spc() ++ pr_class_rawexpr c2)
)
- | VernacInstance (abst, sup, (instid, bk, cl), props, info) ->
+ | VernacInstance (sup, (instid, bk, cl), props, info) ->
return (
hov 1 (
- (if abst then keyword "Declare" ++ spc () else mt ()) ++
keyword "Instance" ++
(match instid with
| {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc ()
@@ -906,13 +905,23 @@ open Pputils
| None -> mt()))
)
+ | VernacDeclareInstance (sup, (instid, bk, cl), info) ->
+ return (
+ hov 1 (
+ keyword "Declare Instance" ++ spc () ++ pr_ident_decl instid ++ spc () ++
+ pr_and_type_binders_arg sup ++
+ str":" ++ spc () ++
+ (match bk with Implicit -> str "! " | Explicit -> mt ()) ++
+ pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info)
+ )
+
| VernacContext l ->
return (
hov 1 (
keyword "Context" ++ pr_and_type_binders_arg l)
)
- | VernacDeclareInstances insts ->
+ | VernacExistingInstance insts ->
let pr_inst (id, info) =
pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info
in
@@ -922,7 +931,7 @@ open Pputils
spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts)
)
- | VernacDeclareClass id ->
+ | VernacExistingClass id ->
return (
hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_qualid id)
)
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index a647b2ef73..0e46df2320 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -12,6 +12,27 @@ open Pcoq
let uvernac = create_universe "vernac"
+type proof_mode = string
+
+(* Tactic parsing modes *)
+let register_proof_mode, find_proof_mode, lookup_proof_mode =
+ let proof_mode : (string, Vernacexpr.vernac_expr Entry.t) Hashtbl.t =
+ Hashtbl.create 19 in
+ let register_proof_mode ename e = Hashtbl.add proof_mode ename e; ename in
+ let find_proof_mode ename =
+ try Hashtbl.find proof_mode ename
+ with Not_found ->
+ CErrors.anomaly Pp.(str "proof mode not found: " ++ str ename) in
+ let lookup_proof_mode name =
+ if Hashtbl.mem proof_mode name then Some name
+ else None
+ in
+ register_proof_mode, find_proof_mode, lookup_proof_mode
+
+let proof_mode_to_string name = name
+
+let command_entry_ref = ref None
+
module Vernac_ =
struct
let gec_vernac s = Entry.create ("vernac:" ^ s)
@@ -39,17 +60,24 @@ module Vernac_ =
] in
Pcoq.grammar_extend main_entry None (None, [None, None, rule])
- let command_entry_ref = ref noedit_mode
+ let select_tactic_entry spec =
+ match spec with
+ | None -> noedit_mode
+ | Some ename -> find_proof_mode ename
+
let command_entry =
Pcoq.Entry.of_parser "command_entry"
- (fun strm -> Pcoq.Entry.parse_token_stream !command_entry_ref strm)
+ (fun strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
end
-let main_entry = Vernac_.main_entry
+module Unsafe = struct
+ let set_tactic_entry oname = command_entry_ref := oname
+end
-let set_command_entry e = Vernac_.command_entry_ref := e
-let get_command_entry () = !Vernac_.command_entry_ref
+let main_entry proof_mode =
+ Unsafe.set_tactic_entry proof_mode;
+ Vernac_.main_entry
let () =
register_grammar Genredexpr.wit_red_expr (Vernac_.red_expr);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index b2f8f71462..fa251281dc 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -14,6 +14,8 @@ open Vernacexpr
val uvernac : gram_universe
+type proof_mode
+
module Vernac_ :
sig
val gallina : vernac_expr Entry.t
@@ -24,13 +26,31 @@ module Vernac_ :
val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
val noedit_mode : vernac_expr Entry.t
val command_entry : vernac_expr Entry.t
+ val main_entry : (Loc.t * vernac_control) option Entry.t
val red_expr : raw_red_expr Entry.t
val hint_info : Hints.hint_info_expr Entry.t
end
+(* To be removed when the parser is made functional wrt the tactic
+ * non terminal *)
+module Unsafe : sig
+ (* To let third party grammar entries reuse Vernac_ and
+ * do something with the proof mode *)
+ val set_tactic_entry : proof_mode option -> unit
+end
+
(** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_control) option Entry.t
+val main_entry : proof_mode option -> (Loc.t * vernac_control) option Entry.t
+
+(** Grammar entry for tactics: proof mode(s).
+ By default Coq's grammar has an empty entry (non-terminal) for
+ tactics. A plugin can register its non-terminal by providing a name
+ and a grammar entry.
+
+ For example the Ltac plugin register the "Classic" grammar
+ entry for parsing its tactics.
+ *)
-(** Handling of the proof mode entry *)
-val get_command_entry : unit -> vernac_expr Entry.t
-val set_command_entry : vernac_expr Entry.t -> unit
+val register_proof_mode : string -> Vernacexpr.vernac_expr Entry.t -> proof_mode
+val lookup_proof_mode : string -> proof_mode option
+val proof_mode_to_string : proof_mode -> string
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index dbccea1117..996fe320f9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -489,6 +489,28 @@ let vernac_notation ~module_local =
let vernac_custom_entry ~module_local s =
Metasyntax.declare_custom_entry module_local s
+(* Default proof mode, to be set at the beginning of proofs for
+ programs that cannot be statically classified. *)
+let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode)
+let get_default_proof_mode () = !default_proof_mode
+
+let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode
+let set_default_proof_mode_opt name =
+ default_proof_mode :=
+ match Pvernac.lookup_proof_mode name with
+ | Some pm -> pm
+ | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name))
+
+let proof_mode_opt_name = ["Default";"Proof";"Mode"]
+let () =
+ Goptions.declare_string_option Goptions.{
+ optdepr = false;
+ optname = "default proof mode" ;
+ optkey = proof_mode_opt_name;
+ optread = get_default_proof_mode_opt;
+ optwrite = set_default_proof_mode_opt;
+ }
+
(***********)
(* Gallina *)
@@ -1005,22 +1027,29 @@ let vernac_identity_coercion ~atts id qids qidt =
(* Type classes *)
-let vernac_instance ~atts abst sup inst props pri =
+let vernac_instance ~atts sup inst props pri =
let open DefAttributes in
let atts = parse atts in
let global = not (make_section_locality atts.locality) in
Dumpglob.dump_constraint (fst (pi1 inst)) false "inst";
let program_mode = Flags.is_program_mode () in
- ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri)
+ ignore(Classes.new_instance ~program_mode ~global atts.polymorphic sup inst props pri)
+
+let vernac_declare_instance ~atts sup inst pri =
+ let open DefAttributes in
+ let atts = parse atts in
+ let global = not (make_section_locality atts.locality) in
+ Dumpglob.dump_definition (fst (pi1 inst)) false "inst";
+ Classes.declare_new_instance ~global atts.polymorphic sup inst pri
let vernac_context ~poly l =
if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
-let vernac_declare_instances ~section_local insts =
+let vernac_existing_instance ~section_local insts =
let glob = not section_local in
List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts
-let vernac_declare_class id =
+let vernac_existing_class id =
Record.declare_existing_class (Nametab.global id)
(***********)
@@ -2108,13 +2137,9 @@ exception End_of_input
let vernac_load interp fname =
if Proof_global.there_are_pending_proofs () then
CErrors.user_err Pp.(str "Load is not supported inside proofs.");
- let interp x =
- let proof_mode = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] in
- Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
- interp x in
- let parse_sentence = Flags.with_option Flags.we_are_parsing
+ let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
(fun po ->
- match Pcoq.Entry.parse Pvernac.main_entry po with
+ match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with
| Some x -> x
| None -> raise End_of_input) in
let fname =
@@ -2125,7 +2150,15 @@ let vernac_load interp fname =
let in_chan = open_utf8_file_in longfname in
Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
begin
- try while true do interp (snd (parse_sentence input)) done
+ try while true do
+ let proof_mode =
+ if Proof_global.there_are_pending_proofs () then
+ Some (get_default_proof_mode ())
+ else
+ None
+ in
+ interp (snd (parse_sentence proof_mode input));
+ done
with End_of_input -> ()
end;
(* If Load left a proof open, we fail too. *)
@@ -2227,11 +2260,13 @@ let interp ?proof ~atts ~st c =
vernac_identity_coercion ~atts id s t
(* Type classes *)
- | VernacInstance (abst, sup, inst, props, info) ->
- vernac_instance ~atts abst sup inst props info
+ | VernacInstance (sup, inst, props, info) ->
+ vernac_instance ~atts sup inst props info
+ | VernacDeclareInstance (sup, inst, info) ->
+ vernac_declare_instance ~atts sup inst info
| VernacContext sup -> vernac_context ~poly:(only_polymorphism atts) sup
- | VernacDeclareInstances insts -> with_section_locality ~atts vernac_declare_instances insts
- | VernacDeclareClass id -> unsupported_attributes atts; vernac_declare_class id
+ | VernacExistingInstance insts -> with_section_locality ~atts vernac_existing_instance insts
+ | VernacExistingClass id -> unsupported_attributes atts; vernac_existing_class id
(* Solving *)
| VernacSolveExistential (n,c) -> unsupported_attributes atts; vernac_solve_existential n c
@@ -2303,8 +2338,7 @@ let interp ?proof ~atts ~st c =
Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings);
Option.iter vernac_set_end_tac tac;
Option.iter vernac_set_used_variables using
- | VernacProofMode mn -> unsupported_attributes atts;
- Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
+ | VernacProofMode mn -> unsupported_attributes atts; ()
(* Extensions *)
| VernacExtend (opn,args) ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 8d8d7cfcf0..4fbd3849b0 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -10,6 +10,11 @@
val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit
+(** Default proof mode set by `start_proof` *)
+val get_default_proof_mode : unit -> Pvernac.proof_mode
+
+val proof_mode_opt_name : string list
+
(** Vernacular entries *)
val vernac_require :
Libnames.qualid option -> bool option -> Libnames.qualid list -> unit
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 417c9ebfbd..68a17e316e 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -300,18 +300,22 @@ type nonrec vernac_expr =
(* Type classes *)
| VernacInstance of
- bool * (* abstract instance *)
local_binder_expr list * (* super *)
typeclass_constraint * (* instance name, class name, params *)
(bool * constr_expr) option * (* props *)
Hints.hint_info_expr
+ | VernacDeclareInstance of
+ local_binder_expr list * (* super *)
+ (ident_decl * Decl_kinds.binding_kind * constr_expr) * (* instance name, class name, params *)
+ Hints.hint_info_expr
+
| VernacContext of local_binder_expr list
- | VernacDeclareInstances of
+ | VernacExistingInstance of
(qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *)
- | VernacDeclareClass of qualid (* inductive or definition name *)
+ | VernacExistingClass of qualid (* inductive or definition name *)
(* Modules and Module Types *)
| VernacDeclareModule of bool option * lident *
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 05687afd8b..f5cf3401d0 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -29,15 +29,15 @@ type vernac_type =
parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
proof_block_detection : proof_block_name option
}
- (* To be removed *)
- | VtProofMode of string
(* Queries are commands assumed to be "pure", that is to say, they
don't modify the interpretation state. *)
| VtQuery
+ (* Commands that change the current proof mode *)
+ | VtProofMode of string
(* To be removed *)
| VtMeta
| VtUnknown
-and vernac_start = string * opacity_guarantee * Names.Id.t list
+and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 0d43eb1ee8..118907c31b 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -45,15 +45,15 @@ type vernac_type =
parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
proof_block_detection : proof_block_name option
}
- (* To be removed *)
- | VtProofMode of string
(* Queries are commands assumed to be "pure", that is to say, they
don't modify the interpretation state. *)
| VtQuery
+ (* Commands that change the current proof mode *)
+ | VtProofMode of string
(* To be removed *)
| VtMeta
| VtUnknown
-and vernac_start = string * opacity_guarantee * Names.Id.t list
+and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 61540024ef..c691dc8559 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -8,10 +8,30 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+module Parser = struct
+
+ type state = Pcoq.frozen_t
+
+ let init () = Pcoq.freeze ~marshallable:false
+
+ let cur_state () = Pcoq.freeze ~marshallable:false
+
+ let parse ps entry pa =
+ Pcoq.unfreeze ps;
+ Flags.with_option Flags.we_are_parsing (fun () ->
+ try Pcoq.Entry.parse entry pa
+ with e when CErrors.noncritical e ->
+ let (e, info) = CErrors.push e in
+ Exninfo.iraise (e, info))
+ ()
+
+end
+
type t = {
- system : States.state; (* summary + libstack *)
- proof : Proof_global.t; (* proof state *)
- shallow : bool (* is the state trimmed down (libstack) *)
+ parsing: Parser.state;
+ system : States.state; (* summary + libstack *)
+ proof : Proof_global.t; (* proof state *)
+ shallow : bool; (* is the state trimmed down (libstack) *)
}
let s_cache = ref None
@@ -37,11 +57,13 @@ let freeze_interp_state ~marshallable =
{ system = update_cache s_cache (States.freeze ~marshallable);
proof = update_cache s_proof (Proof_global.freeze ~marshallable);
shallow = false;
+ parsing = Parser.cur_state ();
}
-let unfreeze_interp_state { system; proof } =
+let unfreeze_interp_state { system; proof; parsing } =
do_if_not_cached s_cache States.unfreeze system;
- do_if_not_cached s_proof Proof_global.unfreeze proof
+ do_if_not_cached s_proof Proof_global.unfreeze proof;
+ Pcoq.unfreeze parsing
let make_shallow st =
let lib = States.lib_of_state st.system in
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index ed20cb935a..581c23386a 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -8,10 +8,21 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+module Parser : sig
+ type state
+
+ val init : unit -> state
+ val cur_state : unit -> state
+
+ val parse : state -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a
+
+end
+
type t = {
- system : States.state; (* summary + libstack *)
- proof : Proof_global.t; (* proof state *)
- shallow : bool (* is the state trimmed down (libstack) *)
+ parsing: Parser.state;
+ system : States.state; (* summary + libstack *)
+ proof : Proof_global.t; (* proof state *)
+ shallow : bool; (* is the state trimmed down (libstack) *)
}
val freeze_interp_state : marshallable:bool -> t
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 15:54:27 +0000