aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml73
-rw-r--r--vernac/classes.mli10
-rw-r--r--vernac/comAssumption.ml12
-rw-r--r--vernac/comAssumption.mli25
-rw-r--r--vernac/comDefinition.ml4
-rw-r--r--vernac/comDefinition.mli17
-rw-r--r--vernac/comFixpoint.ml47
-rw-r--r--vernac/comFixpoint.mli17
-rw-r--r--vernac/declareDef.ml8
-rw-r--r--vernac/declareDef.mli6
-rw-r--r--vernac/egramcoq.ml85
-rw-r--r--vernac/egramml.ml16
-rw-r--r--vernac/egramml.mli2
-rw-r--r--vernac/lemmas.ml145
-rw-r--r--vernac/lemmas.mli34
-rw-r--r--vernac/metasyntax.ml9
-rw-r--r--vernac/obligations.ml45
-rw-r--r--vernac/obligations.mli15
-rw-r--r--vernac/pvernac.ml2
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/search.ml33
-rw-r--r--vernac/search.mli12
-rw-r--r--vernac/vernacentries.ml802
-rw-r--r--vernac/vernacentries.mli8
-rw-r--r--vernac/vernacextend.ml2
-rw-r--r--vernac/vernacstate.ml84
-rw-r--r--vernac/vernacstate.mli58
27 files changed, 1023 insertions, 550 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 6ce2a3f0a5..d61d324941 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -32,7 +32,7 @@ open Entries
let refine_instance = ref false
let () = Goptions.(declare_bool_option {
- optdepr = false;
+ optdepr = true;
optname = "definition of instances by refining";
optkey = ["Refine";"Instance";"Mode"];
optread = (fun () -> !refine_instance);
@@ -147,7 +147,7 @@ let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst
Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
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 declare_instance_open ~pstate 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
if program_mode then
let hook _ _ vis gr =
@@ -166,33 +166,44 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
in
let hook = Lemmas.mk_hook hook in
let ctx = Evd.evar_universe_context sigma in
- ignore (Obligations.add_definition id ?term:constr
- ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls)
+ let _progress = Obligations.add_definition id ?term:constr
+ ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls in
+ pstate
else
- Flags.silently (fun () ->
+ Some Flags.(silently (fun () ->
(* spiwack: it is hard to reorder the actions to do
the pretyping after the proof has opened. As a
consequence, we use the low-level primitives to code
the refinement manually.*)
let gls = List.rev (Evd.future_goals sigma) in
let sigma = Evd.reset_future_goals sigma in
- Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
+ let pstate = Lemmas.start_proof ~ontop:pstate id ~pl:decl kind sigma (EConstr.of_constr termtype)
~hook:(Lemmas.mk_hook
- (fun _ _ _ -> instance_hook k pri global imps ?hook));
+ (fun _ _ _ -> instance_hook k pri global imps ?hook)) in
(* spiwack: I don't know what to do with the status here. *)
- if not (Option.is_empty term) then
- let init_refine =
- Tacticals.New.tclTHENLIST [
- Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term)));
- Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
- Tactics.New.reduce_after_refine;
- ]
- in
- ignore (Pfedit.by init_refine)
- else ignore (Pfedit.by (Tactics.auto_intros_tac ids));
- (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ()
+ let pstate =
+ if not (Option.is_empty term) then
+ let init_refine =
+ Tacticals.New.tclTHENLIST [
+ Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term)));
+ Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
+ Tactics.New.reduce_after_refine;
+ ]
+ in
+ let pstate, _ = Pfedit.by init_refine pstate in
+ pstate
+ else
+ let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in
+ pstate
+ in
+ match tac with
+ | Some tac ->
+ let pstate, _ = Pfedit.by tac pstate in
+ pstate
+ | None ->
+ pstate) ())
-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 do_instance ~pstate 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 }) ->
@@ -272,12 +283,14 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct
Pretyping.check_evars env (Evd.from_env env) sigma termtype;
let termtype = to_constr sigma termtype in
let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
- if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
- declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype
- else if program_mode || refine || Option.is_empty props then
- declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
- else CErrors.user_err Pp.(str "Unsolved obligations remaining.");
- id
+ let pstate =
+ if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
+ (declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype;
+ None)
+ else if program_mode || refine || Option.is_empty props then
+ declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
+ else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in
+ id, pstate
let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl =
let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
@@ -321,7 +334,7 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl =
sigma, cl, u, c', ctx', ctx, imps, args, decl
-let new_instance ?(global=false) ?(refine= !refine_instance) ~program_mode
+let new_instance ~pstate ?(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
@@ -337,7 +350,7 @@ let new_instance ?(global=false) ?(refine= !refine_instance) ~program_mode
Namegen.next_global_ident_away i (Termops.vars_of_env env)
in
let env' = push_rel_context ctx env in
- do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
+ do_instance ~pstate 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) ~program_mode poly ctx (instid, bk, cl) pri =
@@ -361,7 +374,7 @@ let named_of_rel_context l =
l ([], [])
in ctx
-let context poly l =
+let context ~pstate poly l =
let env = Global.env() in
let sigma = Evd.from_env env in
let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
@@ -429,12 +442,12 @@ let context poly l =
let decl = (Discharge, poly, Definitional) in
let nstatus = match b with
| None ->
- pi3 (ComAssumption.declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl
+ pi3 (ComAssumption.declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl
Declaremods.NoInline (CAst.make id))
| Some b ->
let decl = (Discharge, poly, Definition) in
let entry = Declare.definition_entry ~univs ~types:t b in
- let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] in
+ let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in
Lib.sections_are_opened () || Lib.is_modtype_strict ()
in
status && nstatus
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 7e0ec42625..73e4b024ef 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -40,6 +40,7 @@ val declare_instance_constant :
unit
val new_instance :
+ pstate:Proof_global.t option ->
?global:bool (** Not global by default. *) ->
?refine:bool (** Allow refinement *) ->
program_mode:bool ->
@@ -51,7 +52,8 @@ val new_instance :
?tac:unit Proofview.tactic ->
?hook:(GlobRef.t -> unit) ->
Hints.hint_info_expr ->
- Id.t
+ (* May open a proof *)
+ Id.t * Proof_global.t option
val declare_new_instance :
?global:bool (** Not global by default. *) ->
@@ -74,4 +76,8 @@ val id_of_class : typeclass -> Id.t
(** returns [false] if, for lack of section, it declares an assumption
(unless in a module type). *)
-val context : Decl_kinds.polymorphic -> local_binder_expr list -> bool
+val context
+ : pstate:Proof_global.t option
+ -> Decl_kinds.polymorphic
+ -> local_binder_expr list
+ -> bool
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 37a33daf8f..d7bd64067b 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -42,7 +42,7 @@ let should_axiom_into_instance = function
true
| Global | Local -> !axiom_into_instance
-let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
+let declare_assumption ~pstate is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
match local with
| Discharge when Lib.sections_are_opened () ->
let ctx = match ctx with
@@ -53,7 +53,7 @@ match local with
let _ = declare_variable ident decl in
let () = assumption_message ident in
let () =
- if not !Flags.quiet && Proof_global.there_are_pending_proofs () then
+ if not !Flags.quiet && Option.has_some pstate then
Feedback.msg_info Pp.(str"Variable" ++ spc () ++ Id.print ident ++
strbrk " is not visible from current goals")
in
@@ -96,11 +96,11 @@ let next_uctx =
| Polymorphic_entry _ as uctx -> uctx
| Monomorphic_entry _ -> empty_uctx
-let declare_assumptions idl is_coe k (c,uctx) pl imps nl =
+let declare_assumptions ~pstate idl is_coe k (c,uctx) pl imps nl =
let refs, status, _ =
List.fold_left (fun (refs,status,uctx) id ->
let ref',u',status' =
- declare_assumption is_coe k (c,uctx) pl imps false nl id in
+ declare_assumption ~pstate is_coe k (c,uctx) pl imps false nl id in
(ref',u')::refs, status' && status, next_uctx uctx)
([],true,uctx) idl
in
@@ -132,7 +132,7 @@ let process_assumptions_udecls kind l =
in
udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l
-let do_assumptions ~program_mode kind nl l =
+let do_assumptions ~pstate ~program_mode kind nl l =
let open Context.Named.Declaration in
let env = Global.env () in
let udecl, l = process_assumptions_udecls kind l in
@@ -173,7 +173,7 @@ let do_assumptions ~program_mode kind nl l =
let ubinders = Evd.universe_binders sigma in
pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) ->
let t = replace_vars subst t in
- let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in
+ let refs, status' = declare_assumptions ~pstate idl is_coe kind (t,uctx) ubinders imps nl in
let subst' = List.map2
(fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
idl refs
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 2b794b001a..32914cc11b 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -17,8 +17,13 @@ open Decl_kinds
(** {6 Parameters/Assumptions} *)
-val do_assumptions : program_mode:bool -> locality * polymorphic * assumption_object_kind ->
- Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool
+val do_assumptions
+ : pstate:Proof_global.t option
+ -> program_mode:bool
+ -> locality * polymorphic * assumption_object_kind
+ -> Declaremods.inline
+ -> (ident_decl list * constr_expr) with_coercion list
+ -> bool
(************************************************************************)
(** Internal API *)
@@ -28,10 +33,16 @@ val do_assumptions : program_mode:bool -> locality * polymorphic * assumption_ob
(** returns [false] if the assumption is neither local to a section,
nor in a module type and meant to be instantiated. *)
-val declare_assumption : coercion_flag -> assumption_kind ->
- types in_universes_entry ->
- UnivNames.universe_binders -> Impargs.manual_implicits ->
- bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
- GlobRef.t * Univ.Instance.t * bool
+val declare_assumption
+ : pstate:Proof_global.t option
+ -> coercion_flag
+ -> assumption_kind
+ -> types in_universes_entry
+ -> UnivNames.universe_binders
+ -> Impargs.manual_implicits
+ -> bool (** implicit *)
+ -> Declaremods.inline
+ -> variable CAst.t
+ -> GlobRef.t * Univ.Instance.t * bool
val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 28773a3965..feaf47df18 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -90,7 +90,7 @@ let check_definition ~program_mode (ce, evd, _, imps) =
check_evars_are_solved ~program_mode env evd;
ce
-let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
+let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
let (ce, evd, univdecl, imps as def) =
interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt
in
@@ -114,4 +114,4 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
let ce = check_definition ~program_mode def in
let uctx = Evd.evar_universe_context evd in
let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
- ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps )
+ ignore(DeclareDef.declare_definition ~ontop ident k ?hook_data ce (Evd.universe_binders evd) imps)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 9cb6190fcc..12853d83e0 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -16,11 +16,18 @@ open Constrexpr
(** {6 Definitions/Let} *)
-val do_definition : program_mode:bool ->
- ?hook:Lemmas.declaration_hook ->
- Id.t -> definition_kind -> universe_decl_expr option ->
- local_binder_expr list -> red_expr option -> constr_expr ->
- constr_expr option -> unit
+val do_definition
+ : ontop:Proof_global.t option
+ -> program_mode:bool
+ -> ?hook:Lemmas.declaration_hook
+ -> Id.t
+ -> definition_kind
+ -> universe_decl_expr option
+ -> local_binder_expr list
+ -> red_expr option
+ -> constr_expr
+ -> constr_expr option
+ -> unit
(************************************************************************)
(** Internal API *)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 2f00b41b7c..2aadbd224f 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -255,7 +255,8 @@ let interp_fixpoint ~cofix l ntns =
let uctx,fix = ground_fixpoint env evd fix in
(fix,pl,uctx,info)
-let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+ let pstate =
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
@@ -265,8 +266,9 @@ let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximp
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
fixdefs) in
let evd = Evd.from_ctx ctx in
- Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint)
- evd pl (Some(false,indexes,init_tac)) thms None
+ Some
+ (Lemmas.start_proof_with_initialization ~ontop (local,poly,DefinitionBody Fixpoint)
+ evd pl (Some(false,indexes,init_tac)) thms None)
else begin
(* We shortcut the proof process *)
let fixdefs = List.map Option.get fixdefs in
@@ -282,15 +284,18 @@ let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximp
let ctx = Evd.check_univ_decl ~poly evd pl in
let pl = Evd.universe_binders evd in
let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
- ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
+ ignore (List.map4 (DeclareDef.declare_fix ~ontop (local, poly, Fixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
fixpoint_message (Some indexes) fixnames;
- end;
+ None
+ end in
(* Declare notations *)
- List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
+ pstate
-let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+ let pstate =
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
@@ -300,8 +305,8 @@ let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fixi
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
fixdefs) in
let evd = Evd.from_ctx ctx in
- Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
- evd pl (Some(true,[],init_tac)) thms None
+ Some (Lemmas.start_proof_with_initialization ~ontop (Global,poly, DefinitionBody CoFixpoint)
+ evd pl (Some(true,[],init_tac)) thms None)
else begin
(* We shortcut the proof process *)
let fixdefs = List.map Option.get fixdefs in
@@ -314,13 +319,15 @@ let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fixi
let evd = Evd.restrict_universe_context evd vars in
let ctx = Evd.check_univ_decl ~poly evd pl in
let pl = Evd.universe_binders evd in
- ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
+ ignore (List.map4 (DeclareDef.declare_fix ~ontop (local, poly, CoFixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
- cofixpoint_message fixnames
- end;
+ cofixpoint_message fixnames;
+ None
+ end in
(* Declare notations *)
- List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
+ pstate
let extract_decreasing_argument limit = function
| (na,CStructRec) -> na
@@ -348,16 +355,18 @@ let check_safe () =
let flags = Environ.typing_flags (Global.env ()) in
flags.check_universes && flags.check_guarded
-let do_fixpoint local poly l =
+let do_fixpoint ~ontop local poly l =
let fixl, ntns = extract_fixpoint_components true l in
let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
let possible_indexes =
List.map compute_possible_guardness_evidences info in
- declare_fixpoint local poly fix possible_indexes ntns;
- if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+ let pstate = declare_fixpoint ~ontop local poly fix possible_indexes ntns in
+ if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
+ pstate
-let do_cofixpoint local poly l =
+let do_cofixpoint ~ontop local poly l =
let fixl,ntns = extract_cofixpoint_components l in
let cofix = interp_fixpoint ~cofix:true fixl ntns in
- declare_cofixpoint local poly cofix ntns;
- if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+ let pstate = declare_cofixpoint ~ontop local poly cofix ntns in
+ if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
+ pstate
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 9bcb53697b..15ff5f4498 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -19,12 +19,14 @@ open Vernacexpr
(** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
val do_fixpoint :
+ ontop:Proof_global.t option ->
(* When [false], assume guarded. *)
- locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
+ locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t option
val do_cofixpoint :
+ ontop:Proof_global.t option ->
(* When [false], assume guarded. *)
- locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
+ locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t option
(************************************************************************)
(** Internal API *)
@@ -81,15 +83,20 @@ val interp_fixpoint :
(** [Not used so far] *)
val declare_fixpoint :
+ ontop:Proof_global.t option ->
locality -> polymorphic ->
recursive_preentry * UState.universe_decl * UState.t *
(Constr.rel_context * Impargs.manual_implicits * int option) list ->
- Proof_global.lemma_possible_guards -> decl_notation list -> unit
+ Proof_global.lemma_possible_guards -> decl_notation list ->
+ Proof_global.t option
-val declare_cofixpoint : locality -> polymorphic ->
+val declare_cofixpoint :
+ ontop:Proof_global.t option ->
+ locality -> polymorphic ->
recursive_preentry * UState.universe_decl * UState.t *
(Constr.rel_context * Impargs.manual_implicits * int option) list ->
- decl_notation list -> unit
+ decl_notation list ->
+ Proof_global.t option
(** Very private function, do not use *)
val compute_possible_guardness_evidences :
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 7dcd098183..052832244b 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -33,12 +33,12 @@ let get_locality id ~kind = function
| Local -> true
| Global -> false
-let declare_definition ident (local, p, k) ?hook_data ce pl imps =
+let declare_definition ~ontop ident (local, p, k) ?hook_data ce pl imps =
let fix_exn = Future.fix_exn_of ce.const_entry_body in
let gr = match local with
| Discharge when Lib.sections_are_opened () ->
let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in
- let () = if Proof_global.there_are_pending_proofs () then warn_definition_not_visible ident in
+ let () = if Option.has_some ontop then warn_definition_not_visible ident in
VarRef ident
| Discharge | Local | Global ->
let local = get_locality ident ~kind:"definition" local in
@@ -57,9 +57,9 @@ let declare_definition ident (local, p, k) ?hook_data ce pl imps =
end;
gr
-let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+let declare_fix ~ontop ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
- declare_definition f kind ?hook_data ce pl imps
+ declare_definition ~ontop f kind ?hook_data ce pl imps
let check_definition_evars ~allow_evars sigma =
let env = Global.env () in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 3f95ec7107..8e4f4bf7fb 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -14,7 +14,8 @@ open Decl_kinds
val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
val declare_definition
- : Id.t
+ : ontop:Proof_global.t option
+ -> Id.t
-> definition_kind
-> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
-> Safe_typing.private_constants Entries.definition_entry
@@ -23,7 +24,8 @@ val declare_definition
-> GlobRef.t
val declare_fix
- : ?opaque:bool
+ : ontop:Proof_global.t option
+ -> ?opaque:bool
-> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
-> definition_kind
-> UnivNames.universe_binders
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 1a07d74a0e..f1a08cc9b3 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -247,10 +247,10 @@ type (_, _) entry =
| TTReference : ('self, qualid) entry
| TTBigint : ('self, Constrexpr.raw_natural_number) entry
| TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
-| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
+| TTConstrList : prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
| TTPattern : int -> ('self, cases_pattern_expr) entry
| TTOpenBinderList : ('self, local_binder_expr list) entry
-| TTClosedBinderList : Tok.t list -> ('self, local_binder_expr list list) entry
+| TTClosedBinderList : string Tok.p list -> ('self, local_binder_expr list list) entry
type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
@@ -319,41 +319,49 @@ let is_binder_level from e = match e with
let make_sep_rules = function
| [tk] -> Atoken tk
| tkl ->
- let rec mkrule : Tok.t list -> string rules = function
- | [] -> Rules ({ norec_rule = Stop }, fun _ -> (* dropped anyway: *) "")
+ let rec mkrule : 'a Tok.p list -> 'a rules = function
+ | [] -> Rules (Stop, fun _ -> (* dropped anyway: *) "")
| tkn :: rem ->
- let Rules ({ norec_rule = r }, f) = mkrule rem in
- let r = { norec_rule = Next (r, Atoken tkn) } in
+ let Rules (r, f) = mkrule rem in
+ let r = NextNoRec (r, Atoken tkn) in
Rules (r, fun _ -> f)
in
let r = mkrule (List.rev tkl) in
Arules [r]
-let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) symbol = fun custom p assoc from forpat ->
- if custom = InConstrEntry && is_binder_level from p then Aentryl (target_entry InConstrEntry forpat, "200")
- else if is_self from p then Aself
+type ('s, 'a) mayrec_symbol =
+| MayRecNo : ('s, norec, 'a) symbol -> ('s, 'a) mayrec_symbol
+| MayRecMay : ('s, mayrec, 'a) symbol -> ('s, 'a) mayrec_symbol
+
+let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat ->
+ if custom = InConstrEntry && is_binder_level from p then MayRecNo (Aentryl (target_entry InConstrEntry forpat, "200"))
+ else if is_self from p then MayRecMay Aself
else
let g = target_entry custom forpat in
let lev = adjust_level assoc from p in
begin match lev with
- | None -> Aentry g
- | Some None -> Anext
- | Some (Some (lev, cur)) -> Aentryl (g, string_of_int lev)
+ | None -> MayRecNo (Aentry g)
+ | Some None -> MayRecMay Anext
+ | Some (Some (lev, cur)) -> MayRecNo (Aentryl (g, string_of_int lev))
end
-let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with
+let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with
| TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat
| TTConstrList (typ', [], forpat) ->
- Alist1 (symbol_of_target InConstrEntry typ' assoc from forpat)
+ begin match symbol_of_target InConstrEntry typ' assoc from forpat with
+ | MayRecNo s -> MayRecNo (Alist1 s)
+ | MayRecMay s -> MayRecMay (Alist1 s) end
| TTConstrList (typ', tkl, forpat) ->
- Alist1sep (symbol_of_target InConstrEntry typ' assoc from forpat, make_sep_rules tkl)
-| TTPattern p -> Aentryl (Constr.pattern, string_of_int p)
-| TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
-| TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
-| TTName -> Aentry Prim.name
-| TTOpenBinderList -> Aentry Constr.open_binders
-| TTBigint -> Aentry Prim.bigint
-| TTReference -> Aentry Constr.global
+ begin match symbol_of_target InConstrEntry typ' assoc from forpat with
+ | MayRecNo s -> MayRecNo (Alist1sep (s, make_sep_rules tkl))
+ | MayRecMay s -> MayRecMay (Alist1sep (s, make_sep_rules tkl)) end
+| TTPattern p -> MayRecNo (Aentryl (Constr.pattern, string_of_int p))
+| TTClosedBinderList [] -> MayRecNo (Alist1 (Aentry Constr.binder))
+| TTClosedBinderList tkl -> MayRecNo (Alist1sep (Aentry Constr.binder, make_sep_rules tkl))
+| TTName -> MayRecNo (Aentry Prim.name)
+| TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders)
+| TTBigint -> MayRecNo (Aentry Prim.bigint)
+| TTReference -> MayRecNo (Aentry Constr.global)
let interp_entry forpat e = match e with
| ETProdName -> TTAny TTName
@@ -406,8 +414,8 @@ match e with
| TTConstrList _ -> { subst with constrlists = v :: subst.constrlists }
type (_, _) ty_symbol =
-| TyTerm : Tok.t -> ('s, string) ty_symbol
-| TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) symbol * bool -> ('s, 'a) ty_symbol
+| TyTerm : string Tok.p -> ('s, string) ty_symbol
+| TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) mayrec_symbol * bool -> ('s, 'a) ty_symbol
type ('self, _, 'r) ty_rule =
| TyStop : ('self, 'r, 'r) ty_rule
@@ -444,11 +452,23 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env ->
in
ty_eval rem f { env with constrs; constrlists; }
-let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function
-| TyStop -> Stop
+type ('s, 'a, 'r) mayrec_rule =
+| MayRecRNo : ('s, Extend.norec, 'a, 'r) Extend.rule -> ('s, 'a, 'r) mayrec_rule
+| MayRecRMay : ('s, Extend.mayrec, 'a, 'r) Extend.rule -> ('s, 'a, 'r) mayrec_rule
+
+let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) mayrec_rule = function
+| TyStop -> MayRecRNo Stop
| TyMark (_, _, _, r) -> ty_erase r
-| TyNext (rem, TyTerm tok) -> Next (ty_erase rem, Atoken tok)
-| TyNext (rem, TyNonTerm (_, _, s, _)) -> Next (ty_erase rem, s)
+| TyNext (rem, TyTerm tok) ->
+ begin match ty_erase rem with
+ | MayRecRNo rem -> MayRecRMay (Next (rem, Atoken tok))
+ | MayRecRMay rem -> MayRecRMay (Next (rem, Atoken tok)) end
+| TyNext (rem, TyNonTerm (_, _, s, _)) ->
+ begin match ty_erase rem, s with
+ | MayRecRNo rem, MayRecNo s -> MayRecRMay (Next (rem, s))
+ | MayRecRNo rem, MayRecMay s -> MayRecRMay (Next (rem, s))
+ | MayRecRMay rem, MayRecNo s -> MayRecRMay (Next (rem, s))
+ | MayRecRMay rem, MayRecMay s -> MayRecRMay (Next (rem, s)) end
type ('self, 'r) any_ty_rule =
| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
@@ -485,7 +505,7 @@ let rec pure_sublevels' custom assoc from forpat level = function
let rem = pure_sublevels' custom assoc from forpat level rem in
let push where p rem =
match symbol_of_target custom p assoc from forpat with
- | Aentryl (_,i) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem
+ | MayRecNo (Aentryl (_,i)) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem
| _ -> rem in
(match e with
| ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem
@@ -507,7 +527,6 @@ let extend_constr state forpat ng =
let (entry, level) = interp_constr_entry_key custom forpat n in
let fold (accu, state) pt =
let AnyTyRule r = make_ty_rule assoc n forpat pt in
- let symbs = ty_erase r in
let pure_sublevels = pure_sublevels' custom assoc n forpat level pt in
let isforpat = target_to_bool forpat in
let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
@@ -515,7 +534,11 @@ let extend_constr state forpat ng =
let empty_rules = List.map (prepare_empty_levels forpat) needed_levels in
let empty = { constrs = []; constrlists = []; binders = []; binderlists = [] } in
let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
- let rule = (name, p4assoc, [Rule (symbs, act)]) in
+ let rule =
+ let r = match ty_erase r with
+ | MayRecRNo symbs -> Rule (symbs, act)
+ | MayRecRMay symbs -> Rule (symbs, act) in
+ name, p4assoc, [r] in
let r = ExtendRule (entry, reinit, (pos, [rule])) in
(accu @ empty_rules @ [r], state)
in
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 89caff847f..bc58993a2e 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -19,17 +19,17 @@ open Vernacexpr
type 's grammar_prod_item =
| GramTerminal of string
| GramNonTerminal :
- ('a raw_abstract_argument_type * ('s, 'a) symbol) Loc.located -> 's grammar_prod_item
+ ('a raw_abstract_argument_type * ('s, _, 'a) symbol) Loc.located -> 's grammar_prod_item
type 'a ty_arg = ('a -> raw_generic_argument)
-type ('self, _, 'r) ty_rule =
-| TyStop : ('self, 'r, 'r) ty_rule
-| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) Extend.symbol * 'b ty_arg option ->
- ('self, 'b -> 'a, 'r) ty_rule
+type ('self, 'tr, _, 'r) ty_rule =
+| TyStop : ('self, Extend.norec, 'r, 'r) ty_rule
+| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Extend.symbol * 'b ty_arg option ->
+ ('self, Extend.mayrec, 'b -> 'a, 'r) ty_rule
type ('self, 'r) any_ty_rule =
-| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
+| AnyTyRule : ('self, _, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
let rec ty_rule_of_gram = function
| [] -> AnyTyRule TyStop
@@ -44,13 +44,13 @@ let rec ty_rule_of_gram = function
let r = TyNext (rem, tok, inj) in
AnyTyRule r
-let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function
+let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Extend.rule = function
| TyStop -> Extend.Stop
| TyNext (rem, tok, _) -> Extend.Next (ty_erase rem, tok)
type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r
-let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function
+let rec ty_eval : type s tr a. (s, tr, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function
| TyStop -> fun f loc -> f loc []
| TyNext (rem, tok, None) -> fun f _ -> ty_eval rem f
| TyNext (rem, tok, Some inj) -> fun f x ->
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index 3689f60383..1cf75a55b1 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -18,7 +18,7 @@ open Vernacexpr
type 's grammar_prod_item =
| GramTerminal of string
| GramNonTerminal : ('a Genarg.raw_abstract_argument_type *
- ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
+ ('s, _, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
val extend_vernac_command_grammar :
extend_name -> vernac_expr Pcoq.Entry.t option ->
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 0d0732cbb4..1c7cc5e636 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -213,8 +213,11 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes
let default_thm_id = Id.of_string "Unnamed_thm"
-let fresh_name_for_anonymous_theorem () =
- let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in
+let fresh_name_for_anonymous_theorem ~pstate =
+ let avoid = match pstate with
+ | None -> Id.Set.empty
+ | Some pstate -> Id.Set.of_list (Proof_global.get_all_proof_names pstate)
+ in
next_global_ident_away default_thm_id avoid
let check_name_freshness locality {CAst.loc;v=id} : unit =
@@ -224,7 +227,7 @@ let check_name_freshness locality {CAst.loc;v=id} : unit =
then
user_err ?loc (Id.print id ++ str " already exists.")
-let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) =
+let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) =
let t_i = norm t_i in
let k = IsAssumption Conjectural in
match body with
@@ -260,7 +263,6 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,
| Lambda(na,ty,t) -> mkLambda(na,ty,body_i t)
| App (t, args) -> mkApp (body_i t, args)
| _ ->
- let sigma, env = Pfedit.get_current_context () in
anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in
let body_i = body_i body in
match locality with
@@ -333,7 +335,7 @@ let initialize_named_context_for_proof () =
let d = if variable_opacity id then NamedDecl.drop_body d else d in
Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
-let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?(hook : declaration_hook option) c =
+let start_proof ~ontop id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
let terminator = match terminator with
| None -> standard_proof_terminator ?hook compute_guard
| Some terminator -> terminator ?hook compute_guard
@@ -344,7 +346,7 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?(hook :
| None -> initialize_named_context_for_proof ()
in
let goals = [ Global.env_of_context sign , c ] in
- Proof_global.start_proof sigma id ?pl kind goals terminator
+ Proof_global.start_proof ~ontop sigma id ?pl kind goals terminator
let rec_tac_initializer finite guard thms snl =
if finite then
@@ -360,7 +362,7 @@ let rec_tac_initializer finite guard thms snl =
| (id,n,_)::l -> Tactics.mutual_fix id n l 0
| _ -> assert false
-let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
+let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms snl =
let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in
let init_tac,guard = match recguard with
| Some (finite,guard,init_tac) ->
@@ -386,18 +388,20 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in
let body = Option.map EConstr.of_constr body in
let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
- List.map_i (save_remaining_recthms kind norm uctx body opaq) 1 other_thms in
+ let env = Global.env () in
+ List.map_i (save_remaining_recthms env sigma kind norm uctx body opaq) 1 other_thms in
let thms_data = (strength,ref,imps)::other_thms_data in
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
call_hook ?hook ctx [] strength ref) thms_data in
- start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard;
- ignore (Proof_global.with_current_proof (fun _ p ->
+ let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
+ let pstate, _ = Proof_global.with_current_proof (fun _ p ->
match init_tac with
| None -> p,(true,[])
- | Some tac -> Proof.run_tactic Global.(env ()) tac p))
+ | Some tac -> Proof.run_tactic Global.(env ()) tac p) pstate in
+ pstate
-let start_proof_com ~program_mode ?inference_hook ?hook kind thms =
+let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms =
let env0 = Global.env () in
let decl = fst (List.hd thms) in
let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
@@ -429,7 +433,7 @@ let start_proof_com ~program_mode ?inference_hook ?hook kind thms =
else (* We fix the variables to ensure they won't be lowered to Set *)
Evd.fix_undefined_variables evd
in
- start_proof_with_initialization ?hook kind evd decl recguard thms snl
+ start_proof_with_initialization ~ontop ?hook kind evd decl recguard thms snl
(* Saving a proof *)
@@ -444,58 +448,65 @@ let () =
optread = (fun () -> !keep_admitted_vars);
optwrite = (fun b -> keep_admitted_vars := b) }
-let save_proof ?proof = function
- | Vernacexpr.Admitted ->
- let pe =
- let open Proof_global in
- match proof with
- | Some ({ id; entries; persistence = k; universes }, _) ->
- if List.length entries <> 1 then
- user_err Pp.(str "Admitted does not support multiple statements");
- let { const_entry_secctx; const_entry_type } = List.hd entries in
- if const_entry_type = None then
- user_err Pp.(str "Admitted requires an explicit statement");
- let typ = Option.get const_entry_type in
- let ctx = UState.univ_entry ~poly:(pi2 k) universes in
- let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
- Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
- | None ->
- let pftree = Proof_global.give_me_the_proof () in
- let gk = Proof_global.get_current_persistence () in
- let Proof.{ name; poly; entry } = Proof.data pftree in
- let typ = match Proofview.initial_goals entry with
- | [typ] -> snd typ
- | _ ->
- CErrors.anomaly
- ~label:"Lemmas.save_proof" (Pp.str "more than one statement.")
- in
- let typ = EConstr.Unsafe.to_constr typ in
- let universes = Proof.((data pftree).initial_euctx) in
- (* This will warn if the proof is complete *)
- let pproofs, _univs =
- Proof_global.return_proof ~allow_partial:true () in
- let sec_vars =
- if not !keep_admitted_vars then None
- else match Proof_global.get_used_variables(), pproofs with
- | Some _ as x, _ -> x
- | None, (pproof, _) :: _ ->
- let env = Global.env () in
- let ids_typ = Environ.global_vars_set env typ in
- let ids_def = Environ.global_vars_set env pproof in
- Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
- | _ -> None in
- let decl = Proof_global.get_universe_decl () in
- let ctx = UState.check_univ_decl ~poly universes decl in
- Admitted(name,gk,(sec_vars, (typ, ctx), None), universes)
- in
- Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
- | Vernacexpr.Proved (opaque,idopt) ->
- let (proof_obj,terminator) =
- match proof with
- | None ->
- Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)
- | Some proof -> proof
+let save_proof_admitted ?proof ~pstate =
+ let pe =
+ let open Proof_global in
+ match proof with
+ | Some ({ id; entries; persistence = k; universes }, _) ->
+ if List.length entries <> 1 then
+ user_err Pp.(str "Admitted does not support multiple statements");
+ let { const_entry_secctx; const_entry_type } = List.hd entries in
+ if const_entry_type = None then
+ user_err Pp.(str "Admitted requires an explicit statement");
+ let typ = Option.get const_entry_type in
+ let ctx = UState.univ_entry ~poly:(pi2 k) universes in
+ let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
+ Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
+ | None ->
+ let pftree = Proof_global.give_me_the_proof pstate in
+ let gk = Proof_global.get_current_persistence pstate in
+ let Proof.{ name; poly; entry } = Proof.data pftree in
+ let typ = match Proofview.initial_goals entry with
+ | [typ] -> snd typ
+ | _ ->
+ CErrors.anomaly
+ ~label:"Lemmas.save_proof" (Pp.str "more than one statement.")
in
- (* if the proof is given explicitly, nothing has to be deleted *)
- if Option.is_empty proof then Proof_global.discard_current ();
- Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj)))
+ let typ = EConstr.Unsafe.to_constr typ in
+ let universes = Proof.((data pftree).initial_euctx) in
+ (* This will warn if the proof is complete *)
+ let pproofs, _univs =
+ Proof_global.return_proof ~allow_partial:true pstate in
+ let sec_vars =
+ if not !keep_admitted_vars then None
+ else match Proof_global.get_used_variables pstate, pproofs with
+ | Some _ as x, _ -> x
+ | None, (pproof, _) :: _ ->
+ let env = Global.env () in
+ let ids_typ = Environ.global_vars_set env typ in
+ let ids_def = Environ.global_vars_set env pproof in
+ Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
+ | _ -> None in
+ let decl = Proof_global.get_universe_decl pstate in
+ let ctx = UState.check_univ_decl ~poly universes decl in
+ Admitted(name,gk,(sec_vars, (typ, ctx), None), universes)
+ in
+ Proof_global.apply_terminator (Proof_global.get_terminator pstate) pe
+
+let save_proof_proved ?proof ?pstate ~opaque ~idopt =
+ (* Invariant (uh) *)
+ if Option.is_empty pstate && Option.is_empty proof then
+ user_err (str "No focused proof (No proof-editing in progress).");
+ let (proof_obj,terminator) =
+ match proof with
+ | None ->
+ (* XXX: The close_proof and proof state API should be refactored
+ so it is possible to insert proofs properly into the state *)
+ let pstate = Option.get pstate in
+ Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pstate
+ | Some proof -> proof
+ in
+ (* if the proof is given explicitly, nothing has to be deleted *)
+ let pstate = if Option.is_empty proof then Proof_global.discard_current Option.(get pstate) else pstate in
+ Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj)));
+ pstate
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 72c666e903..1f70cfa1ad 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -37,30 +37,32 @@ val call_hook
-> ?fix_exn:Future.fix_exn
-> hook_type
-val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
+val start_proof : ontop:Proof_global.t option -> Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val ->
?compute_guard:Proof_global.lemma_possible_guards ->
- ?hook:declaration_hook -> EConstr.types -> unit
+ ?hook:declaration_hook -> EConstr.types -> Proof_global.t
-val start_proof_com :
- program_mode:bool -> ?inference_hook:Pretyping.inference_hook ->
- ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list ->
- unit
+val start_proof_com
+ : program_mode:bool
+ -> ontop:Proof_global.t option
+ -> ?inference_hook:Pretyping.inference_hook
+ -> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list
+ -> Proof_global.t
-val start_proof_with_initialization :
+val start_proof_with_initialization : ontop:Proof_global.t option ->
?hook:declaration_hook ->
goal_kind -> Evd.evar_map -> UState.universe_decl ->
(bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
(Id.t (* name of thm *) *
- (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list ->
- int list option -> unit
+ (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
+ -> int list option -> Proof_global.t
val standard_proof_terminator :
?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
Proof_global.proof_terminator
-val fresh_name_for_anonymous_theorem : unit -> Id.t
+val fresh_name_for_anonymous_theorem : pstate:Proof_global.t option -> Id.t
(* Prepare global named context for proof session: remove proofs of
opaque section definitions and remove vm-compiled code *)
@@ -69,4 +71,14 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
(** {6 ... } *)
-val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
+val save_proof_admitted
+ : ?proof:Proof_global.closed_proof
+ -> pstate:Proof_global.t
+ -> unit
+
+val save_proof_proved
+ : ?proof:Proof_global.closed_proof
+ -> ?pstate:Proof_global.t
+ -> opaque:Proof_global.opacity_flag
+ -> idopt:Names.lident option
+ -> Proof_global.t option
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 3da12e7714..b5e9e1b0d5 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -23,7 +23,6 @@ open Libobject
open Constrintern
open Vernacexpr
open Libnames
-open Tok
open Notation
open Nameops
@@ -575,20 +574,20 @@ let is_not_small_constr = function
| _ -> false
let rec define_keywords_aux = function
- | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
+ | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(Tok.PIDENT (Some k)) :: l
when is_not_small_constr e ->
Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
CLexer.add_keyword k;
- n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
+ n1 :: GramConstrTerminal(Tok.PKEYWORD k) :: define_keywords_aux l
| n :: l -> n :: define_keywords_aux l
| [] -> []
(* Ensure that IDENT articulation terminal symbols are keywords *)
let define_keywords = function
- | GramConstrTerminal(IDENT k)::l ->
+ | GramConstrTerminal(Tok.PIDENT (Some k))::l ->
Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
CLexer.add_keyword k;
- GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
+ GramConstrTerminal(Tok.PKEYWORD k) :: define_keywords_aux l
| l -> define_keywords_aux l
let distribute a ll = List.map (fun l -> a @ l) ll
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 9aca48f529..07194578c1 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -456,7 +456,7 @@ let obligation_substitution expand prg =
let ints = intset_to (pred (Array.length obls)) in
obl_substitution expand obls ints
-let declare_definition prg =
+let declare_definition ~ontop prg =
let varsubst = obligation_substitution true prg in
let body, typ = subst_prog varsubst prg in
let nf = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None)
@@ -475,7 +475,7 @@ let declare_definition prg =
let () = progmap_remove prg in
let ubinders = UState.universe_binders uctx in
let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
- DeclareDef.declare_definition prg.prg_name
+ DeclareDef.declare_definition ~ontop prg.prg_name
prg.prg_kind ce ubinders prg.prg_implicits ?hook_data
let rec lam_index n t acc =
@@ -554,16 +554,14 @@ let declare_mutual_definition l =
(* Declare the recursive definitions *)
let univs = UState.univ_entry ~poly first.prg_ctx in
let fix_exn = Hook.get get_fix_exn () in
- let kns = List.map4
- (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
- fixnames fixdecls fixtypes fiximps
- in
- (* Declare notations *)
- List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
- Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
- let gr = List.hd kns in
- Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
- List.iter progmap_remove l; gr
+ let kns = List.map4 (DeclareDef.declare_fix ~ontop:None ~opaque (local, poly, kind) UnivNames.empty_binders univs)
+ fixnames fixdecls fixtypes fiximps in
+ (* Declare notations *)
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
+ Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
+ let gr = List.hd kns in
+ Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
+ List.iter progmap_remove l; gr
let decompose_lam_prod c ty =
let open Context.Rel.Declaration in
@@ -763,7 +761,7 @@ let update_obls prg obls rem =
else (
match prg'.prg_deps with
| [] ->
- let kn = declare_definition prg' in
+ let kn = declare_definition ~ontop:None prg' in
progmap_remove prg';
Defined kn
| l ->
@@ -948,7 +946,7 @@ let obligation_hook prg obl num auto ctx' _ _ gr =
ignore (auto (Some prg.prg_name) None deps)
end
-let rec solve_obligation prg num tac =
+let rec solve_obligation ~ontop prg num tac =
let user_num = succ num in
let obls, rem = prg.prg_obligations in
let obl = obls.(num) in
@@ -967,20 +965,21 @@ let rec solve_obligation prg num tac =
let auto n tac oblset = auto_solve_obligations n ~oblset tac in
let terminator ?hook guard =
Proof_global.make_terminator
- (obligation_terminator ?hook prg.prg_name num guard auto) in
+ (obligation_terminator prg.prg_name num guard ?hook auto) in
let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
- let () = Lemmas.start_proof ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
- let _ = Pfedit.by !default_tactic in
- Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac
+ let pstate = Lemmas.start_proof ~ontop ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
+ let pstate = fst @@ Pfedit.by !default_tactic pstate in
+ let pstate = Option.cata (fun tac -> Proof_global.set_endline_tactic tac pstate) pstate tac in
+ pstate
-and obligation (user_num, name, typ) tac =
+and obligation ~ontop (user_num, name, typ) tac =
let num = pred user_num in
let prg = get_prog_err name in
let obls, rem = prg.prg_obligations in
if num >= 0 && num < Array.length obls then
let obl = obls.(num) in
match obl.obl_body with
- None -> solve_obligation prg num tac
+ | None -> solve_obligation ~ontop prg num tac
| Some r -> error "Obligation already solved"
else error (sprintf "Unknown obligation number %i" (succ num))
@@ -1113,7 +1112,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
let obls,_ = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
Flags.if_verbose Feedback.msg_info (info ++ str ".");
- let cst = declare_definition prg in
+ let cst = declare_definition ~ontop:None prg in
Defined cst)
else (
let len = Array.length obls in
@@ -1180,7 +1179,7 @@ let admit_obligations n =
let prg = get_prog_err n in
admit_prog prg
-let next_obligation n tac =
+let next_obligation ~ontop n tac =
let prg = match n with
| None -> get_any_prog_err ()
| Some _ -> get_prog_err n
@@ -1191,7 +1190,7 @@ let next_obligation n tac =
| Some i -> i
| None -> anomaly (Pp.str "Could not find a solvable obligation.")
in
- solve_obligation prg i tac
+ solve_obligation ~ontop prg i tac
let check_program_libraries () =
Coqlib.check_required_library Coqlib.datatypes_module_name;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index c5720363b4..b1b7b1ec90 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -85,10 +85,17 @@ val add_mutual_definitions :
notations ->
fixpoint_kind -> unit
-val obligation : int * Names.Id.t option * Constrexpr.constr_expr option ->
- Genarg.glob_generic_argument option -> unit
-
-val next_obligation : Names.Id.t option -> Genarg.glob_generic_argument option -> unit
+val obligation
+ : ontop:Proof_global.t option
+ -> int * Names.Id.t option * Constrexpr.constr_expr option
+ -> Genarg.glob_generic_argument option
+ -> Proof_global.t
+
+val next_obligation
+ : ontop:Proof_global.t option
+ -> Names.Id.t option
+ -> Genarg.glob_generic_argument option
+ -> Proof_global.t
val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress
(* Number of remaining obligations to be solved for this program *)
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 994fad85f0..d474ef8637 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -55,7 +55,7 @@ module Vernac_ =
let act_vernac v loc = Some CAst.(make ~loc v) in
let act_eoi _ loc = None in
let rule = [
- Rule (Next (Stop, Atoken Tok.EOI), act_eoi);
+ Rule (Next (Stop, Atoken Tok.PEOI), act_eoi);
Rule (Next (Stop, Aentry vernac_control), act_vernac);
] in
Pcoq.grammar_extend main_entry None (None, [None, None, rule])
diff --git a/vernac/record.ml b/vernac/record.ml
index 23274040b0..cb67548667 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -443,7 +443,7 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
let build = ConstructRef cstr in
let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
- let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in
+ let () = Recordops.declare_structure(cstr, List.rev kinds, List.rev sp_projs) in
rsp
in
List.mapi map record_data
diff --git a/vernac/search.ml b/vernac/search.ml
index 6610789626..e41378908f 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -59,11 +59,16 @@ let iter_constructors indsp u fn env nconstr =
let iter_named_context_name_type f =
List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl))
+let get_current_or_goal_context ?pstate glnum =
+ match pstate with
+ | None -> let env = Global.env () in Evd.(from_env env, env)
+ | Some p -> Pfedit.get_goal_context p glnum
+
(* General search over hypothesis of a goal *)
-let iter_hypothesis glnum (fn : GlobRef.t -> env -> constr -> unit) =
+let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) =
let env = Global.env () in
let iter_hyp idh typ = fn (VarRef idh) env typ in
- let evmap,e = Pfedit.get_goal_context glnum in
+ let evmap,e = get_current_or_goal_context ?pstate glnum in
let pfctxt = named_context e in
iter_named_context_name_type iter_hyp pfctxt
@@ -99,10 +104,10 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
try Declaremods.iter_all_segments iter_obj
with Not_found -> ()
-let generic_search glnumopt fn =
+let generic_search ?pstate glnumopt fn =
(match glnumopt with
| None -> ()
- | Some glnum -> iter_hypothesis glnum fn);
+ | Some glnum -> iter_hypothesis ?pstate glnum fn);
iter_declarations fn
(** This module defines a preference on constrs in the form of a
@@ -221,7 +226,7 @@ let search_about_filter query gr env typ = match query with
(** SearchPattern *)
-let search_pattern gopt pat mods pr_search =
+let search_pattern ?pstate gopt pat mods pr_search =
let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
module_filter mods ref env typ &&
@@ -231,7 +236,7 @@ let search_pattern gopt pat mods pr_search =
let iter ref env typ =
if filter ref env typ then pr_search ref env typ
in
- generic_search gopt iter
+ generic_search ?pstate gopt iter
(** SearchRewrite *)
@@ -243,7 +248,7 @@ let rewrite_pat1 pat =
let rewrite_pat2 pat =
PApp (PRef (eq ()), [| PMeta None; PMeta None; pat |])
-let search_rewrite gopt pat mods pr_search =
+let search_rewrite ?pstate gopt pat mods pr_search =
let pat1 = rewrite_pat1 pat in
let pat2 = rewrite_pat2 pat in
let blacklist_filter = blacklist_filter_aux () in
@@ -256,11 +261,11 @@ let search_rewrite gopt pat mods pr_search =
let iter ref env typ =
if filter ref env typ then pr_search ref env typ
in
- generic_search gopt iter
+ generic_search ?pstate gopt iter
(** Search *)
-let search_by_head gopt pat mods pr_search =
+let search_by_head ?pstate gopt pat mods pr_search =
let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
module_filter mods ref env typ &&
@@ -270,11 +275,11 @@ let search_by_head gopt pat mods pr_search =
let iter ref env typ =
if filter ref env typ then pr_search ref env typ
in
- generic_search gopt iter
+ generic_search ?pstate gopt iter
(** SearchAbout *)
-let search_about gopt items mods pr_search =
+let search_about ?pstate gopt items mods pr_search =
let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
let eqb b1 b2 = if b1 then b2 else not b2 in
@@ -286,7 +291,7 @@ let search_about gopt items mods pr_search =
let iter ref env typ =
if filter ref env typ then pr_search ref env typ
in
- generic_search gopt iter
+ generic_search ?pstate gopt iter
type search_constraint =
| Name_Pattern of Str.regexp
@@ -301,7 +306,7 @@ type 'a coq_object = {
coq_object_object : 'a;
}
-let interface_search =
+let interface_search ?pstate =
let rec extract_flags name tpe subtpe mods blacklist = function
| [] -> (name, tpe, subtpe, mods, blacklist)
| (Name_Pattern regexp, b) :: l ->
@@ -371,7 +376,7 @@ let interface_search =
let iter ref env typ =
if filter_function ref env typ then print_function ref env typ
in
- let () = generic_search glnum iter in
+ let () = generic_search ?pstate glnum iter in
!ans
let blacklist_filter ref env typ =
diff --git a/vernac/search.mli b/vernac/search.mli
index ecbb02bc68..0f94ddc5b6 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -39,13 +39,13 @@ val search_about_filter : glob_search_about_item -> filter_function
goal and the global environment for things matching [pattern] and
satisfying module exclude/include clauses of [modinout]. *)
-val search_by_head : int option -> constr_pattern -> DirPath.t list * bool
+val search_by_head : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
-> display_function -> unit
-val search_rewrite : int option -> constr_pattern -> DirPath.t list * bool
+val search_rewrite : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
-> display_function -> unit
-val search_pattern : int option -> constr_pattern -> DirPath.t list * bool
+val search_pattern : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
-> display_function -> unit
-val search_about : int option -> (bool * glob_search_about_item) list
+val search_about : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list
-> DirPath.t list * bool -> display_function -> unit
type search_constraint =
@@ -66,12 +66,12 @@ type 'a coq_object = {
coq_object_object : 'a;
}
-val interface_search : ?glnum:int -> (search_constraint * bool) list ->
+val interface_search : ?pstate:Proof_global.t -> ?glnum:int -> (search_constraint * bool) list ->
constr coq_object list
(** {6 Generic search function} *)
-val generic_search : int option -> display_function -> unit
+val generic_search : ?pstate:Proof_global.t -> int option -> display_function -> unit
(** This function iterates over all hypothesis of the goal numbered
[glnum] (if present) and all known declarations. *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4250ddb02c..d2ba882521 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -44,6 +44,28 @@ let vernac_pperr_endline pp =
(* Misc *)
+let there_are_pending_proofs ~pstate =
+ not Option.(is_empty pstate)
+
+let check_no_pending_proof ~pstate =
+ if there_are_pending_proofs ~pstate then
+ user_err Pp.(str "Command not supported (Open proofs remain)")
+
+let vernac_require_open_proof ~pstate f =
+ match pstate with
+ | Some pstate -> f ~pstate
+ | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)")
+
+let get_current_or_global_context ~pstate =
+ match pstate with
+ | None -> let env = Global.env () in Evd.(from_env env, env)
+ | Some p -> Pfedit.get_current_context p
+
+let get_goal_or_global_context ~pstate glnum =
+ match pstate with
+ | None -> let env = Global.env () in Evd.(from_env env, env)
+ | Some p -> Pfedit.get_goal_context p glnum
+
let cl_of_qualid = function
| FunClass -> Classops.CL_FUN
| SortClass -> Classops.CL_SORT
@@ -72,30 +94,37 @@ end
(*******************)
(* "Show" commands *)
-let show_proof () =
+let show_proof ~pstate =
(* 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
- Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
+ try
+ let pstate = Option.get pstate in
+ let p = Proof_global.give_me_the_proof pstate in
+ let sigma, env = Pfedit.get_current_context pstate in
+ let pprf = Proof.partial_proof p in
+ Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
+ (* We print nothing if there are no goals left *)
+ with
+ | Pfedit.NoSuchGoal
+ | Option.IsNone ->
+ user_err (str "No goals to show.")
-let show_top_evars () =
+let show_top_evars ~pstate =
(* 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 pfts = Proof_global.give_me_the_proof pstate in
let Proof.{goals;shelf;given_up;sigma} = Proof.data pfts in
pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma)
-let show_universes () =
- let pfts = Proof_global.give_me_the_proof () in
+let show_universes ~pstate =
+ let pfts = Proof_global.give_me_the_proof pstate in
let Proof.{goals;sigma} = Proof.data pfts in
let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in
Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++
str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx
(* Simulate the Intro(s) tactic *)
-let show_intro all =
+let show_intro ~pstate all =
let open EConstr in
- let pf = Proof_global.give_me_the_proof() in
+ let pf = Proof_global.give_me_the_proof pstate in
let Proof.{goals;sigma} = Proof.data pf in
if not (List.is_empty goals) then begin
let gl = {Evd.it=List.hd goals ; sigma = sigma; } in
@@ -224,7 +253,7 @@ let print_modtype qid =
with Not_found ->
user_err (str"Unknown Module Type or Module " ++ pr_qualid qid)
-let print_namespace ns =
+let print_namespace ~pstate ns =
let ns = List.rev (Names.DirPath.repr ns) in
(* [match_dirpath], [match_modulpath] are helpers for [matches]
which checks whether a constant is in the namespace [ns]. *)
@@ -272,10 +301,10 @@ let print_namespace ns =
let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in
print_list Id.print qn
in
- let print_constant k body =
+ let print_constant ~pstate k body =
(* FIXME: universes *)
let t = body.Declarations.const_type in
- let sigma, env = Pfedit.get_current_context () in
+ let sigma, env = get_current_or_global_context ~pstate in
print_kn k ++ str":" ++ spc() ++ Printer.pr_type_env env sigma t
in
let matches mp = match match_modulepath ns mp with
@@ -285,7 +314,7 @@ let print_namespace ns =
Environ.fold_constants (fun c body acc ->
let kn = Constant.user c in
if matches (KerName.modpath kn)
- then acc++fnl()++hov 2 (print_constant kn body)
+ then acc++fnl()++hov 2 (print_constant ~pstate kn body)
else acc)
(Global.env ()) (str"")
in
@@ -515,7 +544,7 @@ let () =
(***********)
(* Gallina *)
-let start_proof_and_print ~program_mode ?hook k l =
+let start_proof_and_print ~program_mode ~pstate ?hook k l =
let inference_hook =
if program_mode then
let hook env sigma ev =
@@ -537,7 +566,7 @@ let start_proof_and_print ~program_mode ?hook k l =
in Some hook
else None
in
- start_proof_com ~program_mode ?inference_hook ?hook k l
+ start_proof_com ~program_mode ~ontop:pstate ?inference_hook ?hook k l
let vernac_definition_hook p = function
| Coercion ->
@@ -548,7 +577,7 @@ let vernac_definition_hook p = function
Some (Class.add_subclass_hook p)
| _ -> None
-let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
+let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
let hook = vernac_definition_hook atts.polymorphic kind in
@@ -563,41 +592,47 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
let program_mode = atts.program in
let name =
match id with
- | Anonymous -> fresh_name_for_anonymous_theorem ()
+ | Anonymous -> fresh_name_for_anonymous_theorem ~pstate
| Name n -> n
in
(match def with
| ProveBody (bl,t) -> (* local binders, typ *)
- start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind)
- ?hook [(CAst.make ?loc name, pl), (bl, t)]
+ Some (start_proof_and_print ~program_mode ~pstate (local, atts.polymorphic, DefinitionBody kind)
+ ?hook [(CAst.make ?loc name, pl), (bl, t)])
| 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
- Some (snd (Hook.get f_interp_redexp env sigma r)) in
- ComDefinition.do_definition ~program_mode name
- (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook)
-
-let vernac_start_proof ~atts kind l =
+ | None -> None
+ | Some r ->
+ let sigma, env = get_current_or_global_context ~pstate in
+ Some (snd (Hook.get f_interp_redexp env sigma r)) in
+ ComDefinition.do_definition ~ontop:pstate ~program_mode name
+ (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook;
+ pstate
+ )
+
+let vernac_start_proof ~atts ~pstate kind l =
let open DefAttributes in
let local = enforce_locality_exp atts.locality NoDischarge in
if Dumpglob.dump () then
List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
- start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l
+ Some (start_proof_and_print ~pstate ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l)
-let vernac_end_proof ?proof = function
- | Admitted -> save_proof ?proof Admitted
- | Proved (_,_) as e -> save_proof ?proof e
+let vernac_end_proof ?pstate ?proof = function
+ | Admitted ->
+ vernac_require_open_proof ~pstate (save_proof_admitted ?proof);
+ pstate
+ | Proved (opaque,idopt) ->
+ save_proof_proved ?pstate ?proof ~opaque ~idopt
-let vernac_exact_proof c =
+let vernac_exact_proof ~pstate c =
(* spiwack: for simplicity I do not enforce that "Proof proof_term" is
called only at the begining of a proof. *)
- let status = Pfedit.by (Tactics.exact_proof c) in
- save_proof (Vernacexpr.(Proved(Proof_global.Opaque,None)));
- if not status then Feedback.feedback Feedback.AddedAxiom
+ let pstate, status = Pfedit.by (Tactics.exact_proof c) pstate in
+ let pstate = save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Opaque ~idopt:None in
+ if not status then Feedback.feedback Feedback.AddedAxiom;
+ pstate
-let vernac_assumption ~atts discharge kind l nl =
+let vernac_assumption ~atts ~pstate discharge kind l nl =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
let global = local == Global in
@@ -607,7 +642,7 @@ let vernac_assumption ~atts discharge kind l nl =
List.iter (fun (lid, _) ->
if global then Dumpglob.dump_definition lid false "ax"
else Dumpglob.dump_definition lid true "var") idl) l;
- let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in
+ let status = ComAssumption.do_assumptions ~pstate ~program_mode:atts.program kind nl l in
if not status then Feedback.feedback Feedback.AddedAxiom
let is_polymorphic_inductive_cumulativity =
@@ -772,28 +807,28 @@ let vernac_inductive ~atts cum lo finite indl =
in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
*)
-let vernac_fixpoint ~atts discharge l =
+let vernac_fixpoint ~atts ~pstate discharge l : Proof_global.t option =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
if Dumpglob.dump () then
List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
(* XXX: Switch to the attribute system and match on ~atts *)
let do_fixpoint = if atts.program then
- ComProgramFixpoint.do_fixpoint
+ fun local sign l -> ComProgramFixpoint.do_fixpoint local sign l; None
else
- ComFixpoint.do_fixpoint
+ ComFixpoint.do_fixpoint ~ontop:pstate
in
do_fixpoint local atts.polymorphic l
-let vernac_cofixpoint ~atts discharge l =
+let vernac_cofixpoint ~atts ~pstate discharge l =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
if Dumpglob.dump () then
List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
let do_cofixpoint = if atts.program then
- ComProgramFixpoint.do_cofixpoint
+ fun local sign l -> ComProgramFixpoint.do_cofixpoint local sign l; None
else
- ComFixpoint.do_cofixpoint
+ ComFixpoint.do_cofixpoint ~ontop:pstate
in
do_cofixpoint local atts.polymorphic l
@@ -851,14 +886,14 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export
-let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
+let vernac_define_module ~pstate export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
if Lib.sections_are_opened () then
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
match mexpr_ast_l with
| [] ->
- Proof_global.check_no_pending_proof ();
+ check_no_pending_proof ~pstate;
let binders_ast,argsexport =
List.fold_right
(fun (export,idl,ty) (args,argsexport) ->
@@ -898,13 +933,13 @@ let vernac_end_module export {loc;v=id} =
Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined");
Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
-let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
+let vernac_declare_module_type ~pstate {loc;v=id} binders_ast mty_sign mty_ast_l =
if Lib.sections_are_opened () then
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
match mty_ast_l with
| [] ->
- Proof_global.check_no_pending_proof ();
+ check_no_pending_proof ~pstate;
let binders_ast,argsexport =
List.fold_right
(fun (export,idl,ty) (args,argsexport) ->
@@ -951,8 +986,8 @@ let vernac_include l =
(* Sections *)
-let vernac_begin_section ({v=id} as lid) =
- Proof_global.check_no_pending_proof ();
+let vernac_begin_section ~pstate ({v=id} as lid) =
+ check_no_pending_proof ~pstate;
Dumpglob.dump_definition lid true "sec";
Lib.open_section id
@@ -965,8 +1000,8 @@ let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set
(* Dispatcher of the "End" command *)
-let vernac_end_segment ({v=id} as lid) =
- Proof_global.check_no_pending_proof ();
+let vernac_end_segment ~pstate ({v=id} as lid) =
+ check_no_pending_proof ~pstate;
match Lib.find_opening_node id with
| Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
| Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid
@@ -1031,7 +1066,7 @@ let vernac_instance ~atts sup inst props pri =
let global = not (make_section_locality atts.locality) in
Dumpglob.dump_constraint (fst (pi1 inst)) false "inst";
let program_mode = atts.program in
- ignore(Classes.new_instance ~program_mode ~global atts.polymorphic sup inst props pri)
+ Classes.new_instance ~program_mode ~global atts.polymorphic sup inst props pri
let vernac_declare_instance ~atts sup inst pri =
let open DefAttributes in
@@ -1039,8 +1074,8 @@ let vernac_declare_instance ~atts sup inst pri =
Dumpglob.dump_definition (fst (pi1 inst)) false "inst";
Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri
-let vernac_context ~poly l =
- if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
+let vernac_context ~pstate ~poly l =
+ if not (Classes.context ~pstate poly l) then Feedback.feedback Feedback.AddedAxiom
let vernac_existing_instance ~section_local insts =
let glob = not section_local in
@@ -1061,21 +1096,19 @@ let focus_command_cond = Proof.no_cond command_focus
there are no more goals to solve. It cannot be a tactic since
all tactics fail if there are no further goals to prove. *)
-let vernac_solve_existential = Pfedit.instantiate_nth_evar_com
+let vernac_solve_existential ~pstate i e = Pfedit.instantiate_nth_evar_com i e pstate
-let vernac_set_end_tac tac =
+let vernac_set_end_tac ~pstate tac =
let env = Genintern.empty_glob_sign (Global.env ()) in
let _, tac = Genintern.generic_intern env tac in
- if not (Proof_global.there_are_pending_proofs ()) then
- user_err Pp.(str "Unknown command of the non proof-editing mode.");
- Proof_global.set_endline_tactic tac
- (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
+ (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
+ Proof_global.set_endline_tactic tac pstate
-let vernac_set_used_variables e =
+let vernac_set_used_variables ~(pstate : Proof_global.t) e : Proof_global.t =
let env = Global.env () in
let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
let tys =
- List.map snd (initial_goals (Proof_global.give_me_the_proof ())) in
+ List.map snd (initial_goals (Proof_global.give_me_the_proof pstate)) in
let tys = List.map EConstr.Unsafe.to_constr tys in
let l = Proof_using.process_expr env e tys in
let vars = Environ.named_context env in
@@ -1084,10 +1117,10 @@ let vernac_set_used_variables e =
user_err ~hdr:"vernac_set_used_variables"
(str "Unknown variable: " ++ Id.print id))
l;
- ignore (Proof_global.set_used_variables l);
- Proof_global.with_current_proof begin fun _ p ->
+ let _, pstate = Proof_global.set_used_variables pstate l in
+ fst @@ Proof_global.with_current_proof begin fun _ p ->
(p, ())
- end
+ end pstate
(*****************************)
(* Auxiliary file management *)
@@ -1132,12 +1165,10 @@ let vernac_chdir = function
(* State management *)
let vernac_write_state file =
- Proof_global.discard_all ();
let file = CUnix.make_suffix file ".coq" in
States.extern_state file
let vernac_restore_state file =
- Proof_global.discard_all ();
let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in
States.intern_state file
@@ -1730,9 +1761,14 @@ let vernac_print_option key =
try print_option_value key
with Not_found -> error_undeclared_key key
-let get_current_context_of_args = function
- | Some n -> Pfedit.get_goal_context n
- | None -> Pfedit.get_current_context ()
+let get_current_context_of_args ~pstate =
+ match pstate with
+ | None -> fun _ ->
+ let env = Global.env () in Evd.(from_env env, env)
+ | Some pstate ->
+ function
+ | Some n -> Pfedit.get_goal_context pstate n
+ | None -> Pfedit.get_current_context pstate
let query_command_selector ?loc = function
| None -> None
@@ -1740,9 +1776,9 @@ 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 ~atts redexp glopt rc =
+let vernac_check_may_eval ~pstate ~atts redexp glopt rc =
let glopt = query_command_selector glopt in
- let (sigma, env) = get_current_context_of_args glopt in
+ let sigma, env = get_current_context_of_args ~pstate glopt in
let sigma, c = interp_open_constr env sigma rc in
let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
Evarconv.check_problems_are_solved env sigma;
@@ -1796,27 +1832,33 @@ let vernac_global_check c =
pr_universe_ctx_set sigma uctx
-let get_nth_goal n =
- let pf = Proof_global.give_me_the_proof() in
+let get_nth_goal ~pstate n =
+ let pf = Proof_global.give_me_the_proof pstate in
let Proof.{goals;sigma} = Proof.data pf in
let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in
gl
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 udecl glopt =
+let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
let open Context.Named.Declaration in
try
+ (* Fallback early to globals *)
+ let pstate = match pstate with
+ | None -> raise Not_found
+ | Some pstate -> pstate
+ in
(* 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.v with
| None,AN qid when qualid_is_ident qid -> (* goal number not given, catch any failure *)
- (try get_nth_goal 1, qualid_basename qid with _ -> raise NoHyp)
+ (try get_nth_goal ~pstate 1, qualid_basename qid with _ -> raise NoHyp)
| Some n,AN qid when qualid_is_ident qid -> (* goal number given, catch if wong *)
- (try get_nth_goal n, qualid_basename qid
+ (try get_nth_goal ~pstate n, qualid_basename qid
with
Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs"
(str "No such goal: " ++ int n ++ str "."))
@@ -1826,15 +1868,16 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt =
let natureofid = match decl with
| LocalAssum _ -> "Hypothesis"
| LocalDef (_,bdy,_) ->"Constant (let in)" in
- let sigma, env = Pfedit.get_current_context () in
+ let sigma, env = Pfedit.get_current_context pstate 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 ->
- let sigma, env = Pfedit.get_current_context () in
+ let sigma, env = get_current_or_global_context ~pstate in
print_about env sigma ref_or_by_not udecl
-let vernac_print ~atts env sigma =
+let vernac_print ~(pstate : Proof_global.t option) ~atts =
+ let sigma, env = get_current_or_global_context ~pstate in
function
| PrintTables -> print_tables ()
| PrintFullContext-> print_full_context_typ env sigma
@@ -1845,7 +1888,7 @@ let vernac_print ~atts env sigma =
| PrintModules -> print_modules ()
| PrintModule qid -> print_module qid
| PrintModuleType qid -> print_modtype qid
- | PrintNamespace ns -> print_namespace ns
+ | PrintNamespace ns -> print_namespace ~pstate ns
| PrintMLLoadPath -> Mltop.print_ml_path ()
| PrintMLModules -> Mltop.print_ml_modules ()
| PrintDebugGC -> Mltop.print_gc ()
@@ -1862,7 +1905,13 @@ let vernac_print ~atts env sigma =
| PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma
| PrintUniverses (sort, subgraph, dst) -> print_universes ~sort ~subgraph dst
| PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r)
- | PrintHintGoal -> Hints.pr_applicable_hint ()
+ | PrintHintGoal ->
+ begin match pstate with
+ | Some pstate ->
+ Hints.pr_applicable_hint pstate
+ | None ->
+ str "No proof in progress"
+ end
| PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s
| PrintHintDb -> Hints.pr_searchtable env sigma
| PrintScopes ->
@@ -1872,7 +1921,7 @@ let vernac_print ~atts env sigma =
| PrintVisibility s ->
Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s
| PrintAbout (ref_or_by_not,udecl,glnumopt) ->
- print_about_hyp_globs ref_or_by_not udecl glnumopt
+ print_about_hyp_globs ~pstate ref_or_by_not udecl glnumopt
| PrintImplicit qid ->
dump_global qid;
print_impargs qid
@@ -1937,16 +1986,16 @@ let () =
optread = (fun () -> !search_output_name_only);
optwrite = (:=) search_output_name_only }
-let vernac_search ~atts s gopt r =
+let vernac_search ~pstate ~atts s gopt r =
let gopt = query_command_selector gopt in
let r = interp_search_restriction r in
let env,gopt =
match gopt with | None ->
(* 1st goal by default if it exists, otherwise no goal at all *)
- (try snd (Pfedit.get_goal_context 1) , Some 1
+ (try snd (get_goal_or_global_context ~pstate 1) , Some 1
with _ -> Global.env (),None)
(* if goal selector is given and wrong, then let exceptions be raised. *)
- | Some g -> snd (Pfedit.get_goal_context g) , Some g
+ | Some g -> snd (get_goal_or_global_context ~pstate g) , Some g
in
let get_pattern c = snd (intern_constr_pattern env Evd.(from_env env) c) in
let pr_search ref env c =
@@ -1961,21 +2010,21 @@ let vernac_search ~atts s gopt r =
in
match s with
| SearchPattern c ->
- (Search.search_pattern gopt (get_pattern c) r |> Search.prioritize_search) pr_search
+ (Search.search_pattern ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
| SearchRewrite c ->
- (Search.search_rewrite gopt (get_pattern c) r |> Search.prioritize_search) pr_search
+ (Search.search_rewrite ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
| SearchHead c ->
- (Search.search_by_head gopt (get_pattern c) r |> Search.prioritize_search) pr_search
+ (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
| SearchAbout sl ->
- (Search.search_about gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |>
+ (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |>
Search.prioritize_search) pr_search
-let vernac_locate = function
+let vernac_locate ~pstate = function
| LocateAny {v=AN qid} -> print_located_qualid qid
| LocateTerm {v=AN qid} -> print_located_term qid
| LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *)
| LocateTerm {v=ByNotation (ntn, sc)} ->
- let _, env = Pfedit.get_current_context () in
+ let _, env = get_current_or_global_context ~pstate in
Notation.locate_notation
(Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc
| LocateLibrary qid -> print_located_library qid
@@ -1983,9 +2032,9 @@ let vernac_locate = function
| LocateOther (s, qid) -> print_located_other s qid
| LocateFile f -> locate_file f
-let vernac_register qid r =
+let vernac_register ~pstate qid r =
let gr = Smartlocate.global_with_alias qid in
- if Proof_global.there_are_pending_proofs () then
+ if there_are_pending_proofs ~pstate then
user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
match r with
| RegisterInline ->
@@ -2029,8 +2078,8 @@ let vernac_unfocus () =
(fun _ p -> Proof.unfocus command_focus p ())
(* Checks that a proof is fully unfocused. Raises an error if not. *)
-let vernac_unfocused () =
- let p = Proof_global.give_me_the_proof () in
+let vernac_unfocused ~pstate =
+ let p = Proof_global.give_me_the_proof pstate in
if Proof.unfocused p then
str"The proof is indeed fully unfocused."
else
@@ -2060,25 +2109,39 @@ let vernac_bullet (bullet : Proof_bullet.t) =
Proof_global.simple_with_current_proof (fun _ p ->
Proof_bullet.put p bullet)
-let vernac_show = function
- | ShowScript -> assert false (* Only the stm knows the script *)
- | ShowGoal goalref ->
- let proof = Proof_global.give_me_the_proof () in
- begin match goalref with
- | OpenSubgoals -> pr_open_subgoals ~proof
- | NthGoal n -> pr_nth_open_subgoal ~proof n
- | GoalId id -> pr_goal_by_id ~proof id
+let vernac_show ~pstate =
+ match pstate with
+ (* Show functions that don't require a proof state *)
+ | None ->
+ begin function
+ | ShowProof -> show_proof ~pstate
+ | ShowMatch id -> show_match id
+ | ShowScript -> assert false (* Only the stm knows the script *)
+ | _ ->
+ user_err (str "This command requires an open proof.")
end
- | ShowProof -> show_proof ()
- | ShowExistentials -> show_top_evars ()
- | ShowUniverses -> show_universes ()
- | ShowProofNames ->
- pr_sequence Id.print (Proof_global.get_all_proof_names())
- | ShowIntros all -> show_intro all
- | ShowMatch id -> show_match id
-
-let vernac_check_guard () =
- let pts = Proof_global.give_me_the_proof () in
+ (* Show functions that require a proof state *)
+ | Some pstate ->
+ begin function
+ | ShowGoal goalref ->
+ let proof = Proof_global.give_me_the_proof pstate in
+ begin match goalref with
+ | OpenSubgoals -> pr_open_subgoals ~proof
+ | NthGoal n -> pr_nth_open_subgoal ~proof n
+ | GoalId id -> pr_goal_by_id ~proof id
+ end
+ | ShowExistentials -> show_top_evars ~pstate
+ | ShowUniverses -> show_universes ~pstate
+ | ShowProofNames ->
+ pr_sequence Id.print (Proof_global.get_all_proof_names pstate)
+ | ShowIntros all -> show_intro ~pstate all
+ | ShowProof -> show_proof ~pstate:(Some pstate)
+ | ShowMatch id -> show_match id
+ | ShowScript -> assert false (* Only the stm knows the script *)
+ end
+
+let vernac_check_guard ~pstate =
+ let pts = Proof_global.give_me_the_proof pstate in
let pfterm = List.hd (Proof.partial_proof pts) in
let message =
try
@@ -2097,8 +2160,9 @@ exception End_of_input
the way the proof mode is set there makes the task non trivial
without a considerable amount of refactoring.
*)
-let vernac_load interp fname =
- if Proof_global.there_are_pending_proofs () then
+let vernac_load ~st interp fname =
+ let pstate = st.Vernacstate.proof in
+ if there_are_pending_proofs ~pstate then
CErrors.user_err Pp.(str "Load is not supported inside proofs.");
let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
(fun po ->
@@ -2111,22 +2175,22 @@ let vernac_load interp fname =
let input =
let longfname = Loadpath.locate_file fname in
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
- let proof_mode =
- if Proof_global.there_are_pending_proofs () then
- Some (get_default_proof_mode ())
- else
- None
- in
- interp (parse_sentence proof_mode input).CAst.v;
- done
- with End_of_input -> ()
- end;
+ Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in
+ let rec load_loop ~pstate =
+ try
+ let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) pstate in
+ let pstate = interp ~st:{ st with Vernacstate.proof = pstate }
+ (parse_sentence proof_mode input).CAst.v in
+ load_loop ~pstate
+ with
+ End_of_input ->
+ pstate
+ in
+ let pstate = load_loop ~pstate in
(* If Load left a proof open, we fail too. *)
- if Proof_global.there_are_pending_proofs () then
- CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.")
+ if there_are_pending_proofs ~pstate then
+ CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
+ pstate
let with_locality ~atts f =
let local = Attributes.(parse locality atts) in
@@ -2151,7 +2215,8 @@ let with_def_attributes ~atts f =
* 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 ~atts ~st c =
+let interp ?proof ~atts ~st c : Proof_global.t option =
+ let pstate = st.Vernacstate.proof in
vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
match c with
@@ -2175,145 +2240,309 @@ let interp ?proof ~atts ~st c =
(* Syntax *)
| VernacSyntaxExtension (infix, sl) ->
- with_module_locality ~atts vernac_syntax_extension infix sl
- | VernacDeclareScope sc -> with_module_locality ~atts vernac_declare_scope sc
- | VernacDelimiters (sc,lr) -> with_module_locality ~atts vernac_delimiters sc lr
- | VernacBindScope (sc,rl) -> with_module_locality ~atts vernac_bind_scope sc rl
- | VernacOpenCloseScope (b, s) -> with_section_locality ~atts vernac_open_close_scope (b,s)
- | VernacInfix (mv,qid,sc) -> with_module_locality ~atts vernac_infix mv qid sc
- | VernacNotation (c,infpl,sc) -> with_module_locality ~atts vernac_notation c infpl sc
+ with_module_locality ~atts vernac_syntax_extension infix sl;
+ pstate
+ | VernacDeclareScope sc ->
+ with_module_locality ~atts vernac_declare_scope sc;
+ pstate
+ | VernacDelimiters (sc,lr) ->
+ with_module_locality ~atts vernac_delimiters sc lr;
+ pstate
+ | VernacBindScope (sc,rl) ->
+ with_module_locality ~atts vernac_bind_scope sc rl;
+ pstate
+ | VernacOpenCloseScope (b, s) ->
+ with_section_locality ~atts vernac_open_close_scope (b,s);
+ pstate
+ | VernacInfix (mv,qid,sc) ->
+ with_module_locality ~atts vernac_infix mv qid sc;
+ pstate
+ | VernacNotation (c,infpl,sc) ->
+ with_module_locality ~atts vernac_notation c infpl sc;
+ pstate
| VernacNotationAddFormat(n,k,v) ->
unsupported_attributes atts;
- Metasyntax.add_notation_extra_printing_rule n k v
+ Metasyntax.add_notation_extra_printing_rule n k v;
+ pstate
| VernacDeclareCustomEntry s ->
- with_module_locality ~atts vernac_custom_entry s
+ with_module_locality ~atts vernac_custom_entry s;
+ pstate
(* Gallina *)
| VernacDefinition ((discharge,kind),lid,d) ->
- with_def_attributes ~atts vernac_definition discharge kind lid d
- | VernacStartTheoremProof (k,l) -> with_def_attributes vernac_start_proof ~atts k l
- | VernacEndProof e -> unsupported_attributes atts; vernac_end_proof ?proof e
- | VernacExactProof c -> unsupported_attributes atts; vernac_exact_proof c
+ with_def_attributes ~atts vernac_definition ~pstate discharge kind lid d
+ | VernacStartTheoremProof (k,l) ->
+ with_def_attributes ~atts vernac_start_proof ~pstate k l
+ | VernacEndProof e ->
+ unsupported_attributes atts;
+ vernac_end_proof ?proof ?pstate e
+ | VernacExactProof c ->
+ unsupported_attributes atts;
+ vernac_require_open_proof ~pstate (vernac_exact_proof c)
| VernacAssumption ((discharge,kind),nl,l) ->
- with_def_attributes vernac_assumption ~atts discharge kind l nl
- | VernacInductive (cum, priv, finite, l) -> vernac_inductive ~atts cum priv finite l
- | VernacFixpoint (discharge, l) -> with_def_attributes vernac_fixpoint ~atts discharge l
- | VernacCoFixpoint (discharge, l) -> with_def_attributes vernac_cofixpoint ~atts discharge l
- | VernacScheme l -> unsupported_attributes atts; vernac_scheme l
- | VernacCombinedScheme (id, l) -> unsupported_attributes atts; vernac_combined_scheme id l
- | VernacUniverse l -> vernac_universe ~poly:(only_polymorphism atts) l
- | VernacConstraint l -> vernac_constraint ~poly:(only_polymorphism atts) l
+ with_def_attributes ~atts vernac_assumption ~pstate discharge kind l nl;
+ pstate
+ | VernacInductive (cum, priv, finite, l) ->
+ vernac_inductive ~atts cum priv finite l;
+ pstate
+ | VernacFixpoint (discharge, l) ->
+ with_def_attributes ~atts vernac_fixpoint ~pstate discharge l
+ | VernacCoFixpoint (discharge, l) ->
+ with_def_attributes ~atts vernac_cofixpoint ~pstate discharge l
+ | VernacScheme l ->
+ unsupported_attributes atts;
+ vernac_scheme l;
+ pstate
+ | VernacCombinedScheme (id, l) ->
+ unsupported_attributes atts;
+ vernac_combined_scheme id l;
+ pstate
+ | VernacUniverse l ->
+ vernac_universe ~poly:(only_polymorphism atts) l;
+ pstate
+ | VernacConstraint l ->
+ vernac_constraint ~poly:(only_polymorphism atts) l;
+ pstate
(* Modules *)
| VernacDeclareModule (export,lid,bl,mtyo) ->
- unsupported_attributes atts; vernac_declare_module export lid bl mtyo
+ unsupported_attributes atts;
+ vernac_declare_module export lid bl mtyo;
+ pstate
| VernacDefineModule (export,lid,bl,mtys,mexprl) ->
- unsupported_attributes atts; vernac_define_module export lid bl mtys mexprl
+ unsupported_attributes atts;
+ vernac_define_module ~pstate export lid bl mtys mexprl;
+ pstate
| VernacDeclareModuleType (lid,bl,mtys,mtyo) ->
- unsupported_attributes atts; vernac_declare_module_type lid bl mtys mtyo
+ unsupported_attributes atts;
+ vernac_declare_module_type ~pstate lid bl mtys mtyo;
+ pstate
| VernacInclude in_asts ->
- unsupported_attributes atts; vernac_include in_asts
+ unsupported_attributes atts;
+ vernac_include in_asts;
+ pstate
(* Gallina extensions *)
- | VernacBeginSection lid -> unsupported_attributes atts; vernac_begin_section lid
+ | VernacBeginSection lid ->
+ unsupported_attributes atts;
+ vernac_begin_section ~pstate lid;
+ pstate
- | VernacEndSegment lid -> unsupported_attributes atts; vernac_end_segment lid
+ | VernacEndSegment lid ->
+ unsupported_attributes atts;
+ vernac_end_segment ~pstate lid;
+ pstate
- | VernacNameSectionHypSet (lid, set) -> unsupported_attributes atts; vernac_name_sec_hyp lid set
+ | VernacNameSectionHypSet (lid, set) ->
+ unsupported_attributes atts;
+ vernac_name_sec_hyp lid set;
+ pstate
- | VernacRequire (from, export, qidl) -> unsupported_attributes atts; vernac_require from export qidl
- | VernacImport (export,qidl) -> unsupported_attributes atts; vernac_import export qidl
- | VernacCanonical qid -> unsupported_attributes atts; vernac_canonical qid
- | VernacCoercion (r,s,t) -> vernac_coercion ~atts r s t
+ | VernacRequire (from, export, qidl) ->
+ unsupported_attributes atts;
+ vernac_require from export qidl;
+ pstate
+ | VernacImport (export,qidl) ->
+ unsupported_attributes atts;
+ vernac_import export qidl;
+ pstate
+ | VernacCanonical qid ->
+ unsupported_attributes atts;
+ vernac_canonical qid;
+ pstate
+ | VernacCoercion (r,s,t) ->
+ vernac_coercion ~atts r s t;
+ pstate
| VernacIdentityCoercion ({v=id},s,t) ->
- vernac_identity_coercion ~atts id s t
+ vernac_identity_coercion ~atts id s t;
+ pstate
(* Type classes *)
| VernacInstance (sup, inst, props, info) ->
- with_def_attributes vernac_instance ~atts sup inst props info
+ snd @@ with_def_attributes ~atts (vernac_instance ~pstate sup inst props info)
| VernacDeclareInstance (sup, inst, info) ->
- with_def_attributes vernac_declare_instance ~atts sup inst info
- | VernacContext sup -> vernac_context ~poly:(only_polymorphism atts) sup
- | VernacExistingInstance insts -> with_section_locality ~atts vernac_existing_instance insts
- | VernacExistingClass id -> unsupported_attributes atts; vernac_existing_class id
+ with_def_attributes ~atts vernac_declare_instance sup inst info;
+ pstate
+ | VernacContext sup ->
+ let () = vernac_context ~pstate ~poly:(only_polymorphism atts) sup in
+ pstate
+ | VernacExistingInstance insts ->
+ with_section_locality ~atts vernac_existing_instance insts;
+ pstate
+ | VernacExistingClass id ->
+ unsupported_attributes atts;
+ vernac_existing_class id;
+ pstate
(* Solving *)
- | VernacSolveExistential (n,c) -> unsupported_attributes atts; vernac_solve_existential n c
+ | VernacSolveExistential (n,c) ->
+ unsupported_attributes atts;
+ Some (vernac_require_open_proof ~pstate (vernac_solve_existential n c))
(* Auxiliary file and library management *)
- | VernacAddLoadPath (isrec,s,alias) -> unsupported_attributes atts; vernac_add_loadpath isrec s alias
- | VernacRemoveLoadPath s -> unsupported_attributes atts; vernac_remove_loadpath s
- | VernacAddMLPath (isrec,s) -> unsupported_attributes atts; vernac_add_ml_path isrec s
- | VernacDeclareMLModule l -> with_locality ~atts vernac_declare_ml_module l
- | VernacChdir s -> unsupported_attributes atts; vernac_chdir s
+ | VernacAddLoadPath (isrec,s,alias) ->
+ unsupported_attributes atts;
+ vernac_add_loadpath isrec s alias;
+ pstate
+ | VernacRemoveLoadPath s ->
+ unsupported_attributes atts;
+ vernac_remove_loadpath s;
+ pstate
+ | VernacAddMLPath (isrec,s) ->
+ unsupported_attributes atts;
+ vernac_add_ml_path isrec s;
+ pstate
+ | VernacDeclareMLModule l ->
+ with_locality ~atts vernac_declare_ml_module l;
+ pstate
+ | VernacChdir s ->
+ unsupported_attributes atts;
+ vernac_chdir s;
+ pstate
(* State management *)
- | VernacWriteState s -> unsupported_attributes atts; vernac_write_state s
- | VernacRestoreState s -> unsupported_attributes atts; vernac_restore_state s
+ | VernacWriteState s ->
+ unsupported_attributes atts;
+ vernac_write_state s;
+ pstate
+ | VernacRestoreState s ->
+ unsupported_attributes atts;
+ vernac_restore_state s;
+ pstate
(* Commands *)
| VernacCreateHintDb (dbname,b) ->
- with_module_locality ~atts vernac_create_hintdb dbname b
+ with_module_locality ~atts vernac_create_hintdb dbname b;
+ pstate
| VernacRemoveHints (dbnames,ids) ->
- with_module_locality ~atts vernac_remove_hints dbnames ids
+ with_module_locality ~atts vernac_remove_hints dbnames ids;
+ pstate
| VernacHints (dbnames,hints) ->
- vernac_hints ~atts dbnames hints
+ vernac_hints ~atts dbnames hints;
+ pstate
| VernacSyntacticDefinition (id,c,b) ->
- with_module_locality ~atts vernac_syntactic_definition id c b
+ with_module_locality ~atts vernac_syntactic_definition id c b;
+ pstate
| VernacArguments (qid, args, more_implicits, nargs, flags) ->
- with_section_locality ~atts vernac_arguments qid args more_implicits nargs flags
- | VernacReserve bl -> unsupported_attributes atts; vernac_reserve bl
- | VernacGeneralizable gen -> with_locality ~atts vernac_generalizable gen
- | VernacSetOpacity qidl -> with_locality ~atts vernac_set_opacity qidl
- | VernacSetStrategy l -> with_locality ~atts vernac_set_strategy l
- | VernacSetOption (export, key,v) -> vernac_set_option ~local:(only_locality atts) export key v
- | VernacUnsetOption (export, key) -> vernac_unset_option ~local:(only_locality atts) export key
- | VernacRemoveOption (key,v) -> unsupported_attributes atts; vernac_remove_option key v
- | VernacAddOption (key,v) -> unsupported_attributes atts; vernac_add_option key v
- | VernacMemOption (key,v) -> unsupported_attributes atts; vernac_mem_option key v
- | VernacPrintOption key -> unsupported_attributes atts; vernac_print_option key
+ with_section_locality ~atts vernac_arguments qid args more_implicits nargs flags;
+ pstate
+ | VernacReserve bl ->
+ unsupported_attributes atts;
+ vernac_reserve bl;
+ pstate
+ | VernacGeneralizable gen ->
+ with_locality ~atts vernac_generalizable gen;
+ pstate
+ | VernacSetOpacity qidl ->
+ with_locality ~atts vernac_set_opacity qidl;
+ pstate
+ | VernacSetStrategy l ->
+ with_locality ~atts vernac_set_strategy l;
+ pstate
+ | VernacSetOption (export, key,v) ->
+ vernac_set_option ~local:(only_locality atts) export key v;
+ pstate
+ | VernacUnsetOption (export, key) ->
+ vernac_unset_option ~local:(only_locality atts) export key;
+ pstate
+ | VernacRemoveOption (key,v) ->
+ unsupported_attributes atts;
+ vernac_remove_option key v;
+ pstate
+ | VernacAddOption (key,v) ->
+ unsupported_attributes atts;
+ vernac_add_option key v;
+ pstate
+ | VernacMemOption (key,v) ->
+ unsupported_attributes atts;
+ vernac_mem_option key v;
+ pstate
+ | VernacPrintOption key ->
+ unsupported_attributes atts;
+ vernac_print_option key;
+ pstate
| VernacCheckMayEval (r,g,c) ->
- Feedback.msg_notice @@ vernac_check_may_eval ~atts r g c
- | VernacDeclareReduction (s,r) -> with_locality ~atts vernac_declare_reduction s r
+ Feedback.msg_notice @@
+ vernac_check_may_eval ~pstate ~atts r g c;
+ pstate
+ | VernacDeclareReduction (s,r) ->
+ with_locality ~atts vernac_declare_reduction s r;
+ pstate
| VernacGlobalCheck c ->
unsupported_attributes atts;
- Feedback.msg_notice @@ vernac_global_check c
+ Feedback.msg_notice @@ vernac_global_check c;
+ pstate
| VernacPrint p ->
- let sigma, env = Pfedit.get_current_context () in
- Feedback.msg_notice @@ vernac_print ~atts env sigma p
- | VernacSearch (s,g,r) -> unsupported_attributes atts; vernac_search ~atts s g r
+ Feedback.msg_notice @@ vernac_print ~pstate ~atts p;
+ pstate
+ | VernacSearch (s,g,r) ->
+ unsupported_attributes atts;
+ vernac_search ~pstate ~atts s g r;
+ pstate
| VernacLocate l -> unsupported_attributes atts;
- Feedback.msg_notice @@ vernac_locate l
- | VernacRegister (qid, r) -> unsupported_attributes atts; vernac_register qid r
- | VernacPrimitive (id, prim, typopt) -> unsupported_attributes atts; ComAssumption.do_primitive id prim typopt
- | VernacComments l -> unsupported_attributes atts;
- Flags.if_verbose Feedback.msg_info (str "Comments ok\n")
+ Feedback.msg_notice @@ vernac_locate ~pstate l;
+ pstate
+ | VernacRegister (qid, r) ->
+ unsupported_attributes atts;
+ vernac_register ~pstate qid r;
+ pstate
+ | VernacPrimitive (id, prim, typopt) ->
+ unsupported_attributes atts;
+ ComAssumption.do_primitive id prim typopt;
+ pstate
+ | VernacComments l ->
+ unsupported_attributes atts;
+ Flags.if_verbose Feedback.msg_info (str "Comments ok\n");
+ pstate
(* Proof management *)
- | VernacFocus n -> unsupported_attributes atts; vernac_focus n
- | VernacUnfocus -> unsupported_attributes atts; vernac_unfocus ()
- | VernacUnfocused -> unsupported_attributes atts;
- Feedback.msg_notice @@ vernac_unfocused ()
- | VernacBullet b -> unsupported_attributes atts; vernac_bullet b
- | VernacSubproof n -> unsupported_attributes atts; vernac_subproof n
- | VernacEndSubproof -> unsupported_attributes atts; vernac_end_subproof ()
- | VernacShow s -> unsupported_attributes atts;
- Feedback.msg_notice @@ vernac_show s
- | VernacCheckGuard -> unsupported_attributes atts;
- Feedback.msg_notice @@ vernac_check_guard ()
- | VernacProof (tac, using) -> unsupported_attributes atts;
+ | VernacFocus n ->
+ unsupported_attributes atts;
+ Option.map (vernac_focus n) pstate
+ | VernacUnfocus ->
+ unsupported_attributes atts;
+ Option.map (vernac_unfocus ()) pstate
+ | VernacUnfocused ->
+ unsupported_attributes atts;
+ Option.iter (fun pstate -> Feedback.msg_notice @@ vernac_unfocused ~pstate) pstate;
+ pstate
+ | VernacBullet b ->
+ unsupported_attributes atts;
+ Option.map (vernac_bullet b) pstate
+ | VernacSubproof n ->
+ unsupported_attributes atts;
+ Option.map (vernac_subproof n) pstate
+ | VernacEndSubproof ->
+ unsupported_attributes atts;
+ Option.map (vernac_end_subproof ()) pstate
+ | VernacShow s ->
+ unsupported_attributes atts;
+ Feedback.msg_notice @@ vernac_show ~pstate s;
+ pstate
+ | VernacCheckGuard ->
+ unsupported_attributes atts;
+ Feedback.msg_notice @@
+ vernac_require_open_proof ~pstate (vernac_check_guard);
+ pstate
+ | VernacProof (tac, using) ->
+ unsupported_attributes atts;
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 "VernacProof" (tacs^" "^usings);
- Option.iter vernac_set_end_tac tac;
- Option.iter vernac_set_used_variables using
- | VernacProofMode mn -> unsupported_attributes atts; ()
+ let pstate =
+ vernac_require_open_proof ~pstate (fun ~pstate ->
+ let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in
+ Option.cata (vernac_set_used_variables ~pstate) pstate using)
+ in Some pstate
+ | VernacProofMode mn ->
+ unsupported_attributes atts;
+ pstate
(* Extensions *)
| VernacExtend (opn,args) ->
(* XXX: Here we are returning the state! :) *)
- let _st : Vernacstate.t = Vernacextend.call ~atts opn args ~st in
- ()
+ let st : Vernacstate.t = Vernacextend.call ~atts opn args ~st in
+ st.Vernacstate.proof
(** A global default timeout, controlled by option "Set Default Timeout n".
Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
@@ -2333,12 +2562,18 @@ let () =
let current_timeout = ref None
-let vernac_timeout f =
+let vernac_timeout (f : 'a -> 'b) (x : 'a) : 'b =
match !current_timeout, !default_timeout with
- | Some n, _ | None, Some n ->
- let f () = f (); current_timeout := None in
- Control.timeout n f () Timeout
- | None, None -> f ()
+ | Some n, _
+ | None, Some n ->
+ let f v =
+ let res = f v in
+ current_timeout := None;
+ res
+ in
+ Control.timeout n f x Timeout
+ | None, None ->
+ f x
let restore_timeout () = current_timeout := None
@@ -2354,84 +2589,87 @@ let test_mode = ref false
(* XXX STATE: this type hints that restoring the state should be the
caller's responsibility *)
-let with_fail st b f =
- if not b
- then f ()
- else begin try
- (* If the command actually works, ignore its effects on the state.
+let with_fail ~st f =
+ try
+ (* If the command actually works, ignore its effects on the state.
* Note that error has to be printed in the right state, hence
* within the purified function *)
- try f (); raise HasNotFailed
- with
- | HasNotFailed as e -> raise e
- | e ->
- let e = CErrors.push e in
- raise (HasFailed (CErrors.iprint
- (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! *)
- Vernacstate.invalidate_cache ();
- Vernacstate.unfreeze_interp_state st;
- let (e, _) = CErrors.push e in
- match e with
- | HasNotFailed ->
- user_err ~hdr:"Fail" (str "The command has not failed!")
- | HasFailed msg ->
- if not !Flags.quiet || !test_mode then Feedback.msg_info
- (str "The command has indeed failed with message:" ++ fnl () ++ msg)
- | _ -> assert false
- end
-
-let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
- let rec control = function
+ try let _ = f () in raise HasNotFailed
+ with
+ | HasNotFailed as e -> raise e
+ | e ->
+ let e = CErrors.push e in
+ raise (HasFailed (CErrors.iprint
+ (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! *)
+ Vernacstate.invalidate_cache ();
+ Vernacstate.unfreeze_interp_state st;
+ let (e, _) = CErrors.push e in
+ match e with
+ | HasNotFailed ->
+ user_err ~hdr:"Fail" (str "The command has not failed!")
+ | HasFailed msg ->
+ if not !Flags.quiet || !test_mode then Feedback.msg_info
+ (str "The command has indeed failed with message:" ++ fnl () ++ msg)
+ | _ -> assert false
+
+let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} : Proof_global.t option =
+ let rec control ~st = function
| VernacExpr (atts, v) ->
- aux ~atts v
- | VernacFail v -> with_fail st true (fun () -> control v)
+ aux ~atts ~st v
+ | VernacFail v ->
+ with_fail ~st (fun () -> ignore(control ~st v));
+ st.Vernacstate.proof
| VernacTimeout (n,v) ->
current_timeout := Some n;
- control v
+ control ~st v
| VernacRedirect (s, {v}) ->
- Topfmt.with_output_to_file s control v
- | VernacTime (batch, com) ->
+ Topfmt.with_output_to_file s (control ~st) v
+ | VernacTime (batch, ({v} as com)) ->
let header = if batch then Topfmt.pr_cmd_header com else Pp.mt () in
- System.with_time ~batch ~header control com.CAst.v;
+ System.with_time ~batch ~header (control ~st) v;
- and aux ~atts : _ -> unit =
+ and aux ~atts ~st : _ -> Proof_global.t option =
function
| VernacLoad (_,fname) ->
unsupported_attributes atts;
- vernac_load control fname
+ vernac_load ~st control fname
| c ->
(* NB: we keep polymorphism and program in the attributes, we're
just parsing them to do our option magic. *)
try
- vernac_timeout begin fun () ->
- if verbosely
- then Flags.verbosely (interp ?proof ~atts ~st) c
- else Flags.silently (interp ?proof ~atts ~st) c;
- end
- with
- | reraise when
- (match reraise with
- | Timeout -> true
- | e -> CErrors.noncritical e)
- ->
- let e = CErrors.push reraise in
- let e = locate_if_not_already ?loc e in
- let () = restore_timeout () in
- iraise e
+ vernac_timeout begin fun st ->
+ let pstate : Proof_global.t option =
+ if verbosely
+ then Flags.verbosely (interp ?proof ~atts ~st) c
+ else Flags.silently (interp ?proof ~atts ~st) c
+ in
+ pstate
+ end st
+ with
+ | reraise when
+ (match reraise with
+ | Timeout -> true
+ | e -> CErrors.noncritical e)
+ ->
+ let e = CErrors.push reraise in
+ let e = locate_if_not_already ?loc e in
+ let () = restore_timeout () in
+ iraise e
in
if verbosely
- then Flags.verbosely control c
- else control c
+ then Flags.verbosely (control ~st) c
+ else (control ~st) c
(* Be careful with the cache here in case of an exception. *)
let interp ?verbosely ?proof ~st cmd =
Vernacstate.unfreeze_interp_state st;
try
- interp ?verbosely ?proof ~st cmd;
+ let pstate = interp ?verbosely ?proof ~st cmd in
+ Vernacstate.Proof_global.set pstate;
Vernacstate.freeze_interp_state ~marshallable:false
with exn ->
let exn = CErrors.push exn in
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index f43cec48e9..71cc29b6e1 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -33,15 +33,17 @@ val interp :
val make_cases : string -> string list list
-(* XXX STATE: this type hints that restoring the state should be the
- caller's responsibility *)
-val with_fail : Vernacstate.t -> bool -> (unit -> unit) -> unit
+(** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *)
+val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit
val command_focus : unit Proof.focus_kind
val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
Evd.evar_map * Redexpr.red_expr) Hook.t
+(** Helper *)
+val vernac_require_open_proof : pstate:Proof_global.t option -> (pstate:Proof_global.t -> 'a) -> 'a
+
(* Flag set when the test-suite is called. Its only effect to display
verbose information for `Fail` *)
val test_mode : bool ref
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 4bfe5c66b5..ef06e59316 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -169,7 +169,7 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_comm
| Some Refl -> untype_command ty (f v) args
end
-let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol =
+let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Extend.norec, a) Extend.symbol =
let open Extend in function
| TUlist1 l -> Alist1 (untype_user_symbol l)
| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s))
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index c691dc8559..77f54361da 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -28,10 +28,10 @@ module Parser = struct
end
type t = {
- parsing: Parser.state;
- 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 option; (* proof state *)
+ shallow : bool (* is the state trimmed down (libstack) *)
}
let s_cache = ref None
@@ -55,14 +55,14 @@ let do_if_not_cached rf f v =
let freeze_interp_state ~marshallable =
{ system = update_cache s_cache (States.freeze ~marshallable);
- proof = update_cache s_proof (Proof_global.freeze ~marshallable);
+ proof = !s_proof;
shallow = false;
parsing = Parser.cur_state ();
}
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;
+ s_proof := proof;
Pcoq.unfreeze parsing
let make_shallow st =
@@ -71,3 +71,75 @@ let make_shallow st =
system = States.replace_lib st.system @@ Lib.drop_objects lib;
shallow = true;
}
+
+(* Compatibility module *)
+module Proof_global = struct
+
+ let get () = !s_proof
+ let set x = s_proof := x
+
+ let freeze ~marshallable:_ = get ()
+ let unfreeze x = s_proof := Some x
+
+ exception NoCurrentProof
+
+ let () =
+ CErrors.register_handler begin function
+ | NoCurrentProof ->
+ CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).")
+ | _ -> raise CErrors.Unhandled
+ end
+
+ open Proof_global
+
+ let cc f = match !s_proof with
+ | None -> raise NoCurrentProof
+ | Some x -> f x
+
+ let dd f = match !s_proof with
+ | None -> raise NoCurrentProof
+ | Some x -> s_proof := Some (f x)
+
+ let there_are_pending_proofs () = !s_proof <> None
+ let get_open_goals () = cc get_open_goals
+
+ let set_terminator x = dd (set_terminator x)
+ let give_me_the_proof_opt () = Option.map give_me_the_proof !s_proof
+ let give_me_the_proof () = cc give_me_the_proof
+ let get_current_proof_name () = cc get_current_proof_name
+
+ let simple_with_current_proof f =
+ dd (simple_with_current_proof f)
+
+ let with_current_proof f =
+ let pf, res = cc (with_current_proof f) in
+ s_proof := Some pf; res
+
+ let install_state s = s_proof := Some s
+
+ let return_proof ?allow_partial () =
+ cc (return_proof ?allow_partial)
+
+ let close_future_proof ~opaque ~feedback_id pf =
+ cc (fun st -> close_future_proof ~opaque ~feedback_id st pf)
+
+ let close_proof ~opaque ~keep_body_ucst_separate f =
+ cc (close_proof ~opaque ~keep_body_ucst_separate f)
+
+ let discard_all () = s_proof := None
+ let update_global_env () = dd update_global_env
+
+ let get_current_context () = cc Pfedit.get_current_context
+
+ let get_all_proof_names () =
+ try cc get_all_proof_names
+ with NoCurrentProof -> []
+
+ let copy_terminators ~src ~tgt =
+ match src, tgt with
+ | None, None -> None
+ | Some _ , None -> None
+ | None, Some x -> Some x
+ | Some src, Some tgt -> Some (copy_terminators ~src ~tgt)
+
+end
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 581c23386a..b79f97796f 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -19,10 +19,10 @@ module Parser : sig
end
type t = {
- parsing: Parser.state;
- 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 option; (* proof state *)
+ shallow : bool (* is the state trimmed down (libstack) *)
}
val freeze_interp_state : marshallable:bool -> t
@@ -32,3 +32,53 @@ val make_shallow : t -> t
(* WARNING: Do not use, it will go away in future releases *)
val invalidate_cache : unit -> unit
+
+(* Compatibility module: Do Not Use *)
+module Proof_global : sig
+
+ open Proof_global
+
+ (* Low-level stuff *)
+ val get : unit -> t option
+ val set : t option -> unit
+
+ val freeze : marshallable:bool -> t option
+ val unfreeze : t -> unit
+
+ exception NoCurrentProof
+
+ val there_are_pending_proofs : unit -> bool
+ val get_open_goals : unit -> int
+
+ val set_terminator : proof_terminator -> unit
+ val give_me_the_proof : unit -> Proof.t
+ val give_me_the_proof_opt : unit -> Proof.t option
+ val get_current_proof_name : unit -> Names.Id.t
+
+ val simple_with_current_proof :
+ (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit
+
+ val with_current_proof :
+ (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
+
+ val install_state : t -> unit
+
+ val return_proof : ?allow_partial:bool -> unit -> closed_proof_output
+
+ val close_future_proof :
+ opaque:opacity_flag ->
+ feedback_id:Stateid.t ->
+ closed_proof_output Future.computation -> closed_proof
+
+ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
+
+ val discard_all : unit -> unit
+ val update_global_env : unit -> unit
+
+ val get_current_context : unit -> Evd.evar_map * Environ.env
+
+ val get_all_proof_names : unit -> Names.Id.t list
+
+ val copy_terminators : src:t option -> tgt:t option -> t option
+
+end
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 22:41:08 +0000