diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 8 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_mode.mli | 4 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 43 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 14 |
4 files changed, 39 insertions, 30 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 8c5aec38b..0cbd26316 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -99,11 +99,13 @@ let proof_cond = Proof.no_cond proof_focus let focus p = let inf = get_stack p in - Proof.focus proof_cond inf 1 p + Proof_global.with_current_proof (fun _ -> Proof.focus proof_cond inf 1) -let unfocus = Proof.unfocus proof_focus +let unfocus () = + Proof_global.with_current_proof (fun _ p -> Proof.unfocus proof_focus p ()) -let maximal_unfocus = Proof_global.maximal_unfocus proof_focus +let maximal_unfocus () = + Proof_global.with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus) let get_top_stack pts = try diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index c54dcdc28..8e691f508 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -75,6 +75,6 @@ val get_last: Environ.env -> Id.t val focus : Proof.proof -> unit -val unfocus : Proof.proof -> unit +val unfocus : unit -> unit -val maximal_unfocus : Proof.proof -> unit +val maximal_unfocus : unit -> unit diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index a06b44083..e3ef0671c 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -51,12 +51,13 @@ let _ = let tcl_change_info_gen info_gen = (fun gls -> + let it, eff = sig_it gls, sig_eff gls in let concl = pf_concl gls in - let hyps = Goal.V82.hyps (project gls) (sig_it gls) in - let extra = Goal.V82.extra (project gls) (sig_it gls) in + let hyps = Goal.V82.hyps (project gls) it in + let extra = Goal.V82.extra (project gls) it in let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in - let sigma = Goal.V82.partial_solution sigma (sig_it gls) ev in - { it = [gl] ; sigma= sigma } ) + let sigma = Goal.V82.partial_solution sigma it ev in + { it = [gl] ; sigma= sigma; eff = eff } ) let tcl_change_info info gls = let info_gen s = Store.set s Decl_mode.info info in @@ -128,34 +129,34 @@ let go_to_proof_mode () = let daimon_tac gls = set_daimon_flag (); - {it=[];sigma=sig_sig gls} + {it=[];sigma=sig_sig gls;eff=gls.eff} (* post-instruction focus management *) (* spiwack: This used to fail if there was no focusing command above, but I don't think it ever happened. I hope it doesn't mess things up*) -let goto_current_focus pts = - Decl_mode.maximal_unfocus pts +let goto_current_focus () = + Decl_mode.maximal_unfocus () -let goto_current_focus_or_top pts = - goto_current_focus pts +let goto_current_focus_or_top () = + goto_current_focus () (* return *) -let close_tactic_mode pts = - try goto_current_focus pts +let close_tactic_mode () = + try goto_current_focus () with Not_found -> error "\"return\" cannot be used outside of Declarative Proof Mode." let return_from_tactic_mode () = - close_tactic_mode (Proof_global.give_me_the_proof ()) + close_tactic_mode () (* end proof/claim *) let close_block bt pts = if Proof.no_focused_goal pts then - goto_current_focus pts + goto_current_focus () else let stack = if Proof.is_done pts then @@ -165,7 +166,7 @@ let close_block bt pts = in match bt,stack with B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> - (goto_current_focus pts) + (goto_current_focus ()) | _, Claim::_ -> error "\"end claim\" expected." | _, Focus_claim::_ -> @@ -190,13 +191,13 @@ let close_previous_case pts = match get_top_stack pts with Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...") | Suppose_case :: Per (et,_,_,_) :: _ -> - goto_current_focus (pts) + goto_current_focus () | _ -> error "Not inside a proof per cases or induction." else match get_stack pts with Per (et,_,_,_) :: _ -> () | Suppose_case :: Per (et,_,_,_) :: _ -> - goto_current_focus ((pts)) + goto_current_focus () | _ -> error "Not inside a proof per cases or induction." (* Proof instructions *) @@ -1443,21 +1444,21 @@ let rec postprocess pts instr = in try Inductiveops.control_only_guard env pfterm; - goto_current_focus_or_top pts + goto_current_focus_or_top () with Type_errors.TypeError(env, Type_errors.IllFormedRecBody(_,_,_,_,_)) -> anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint") end | Pend _ -> - goto_current_focus_or_top (pts) + goto_current_focus_or_top () let do_instr raw_instr pts = let has_tactic = preprocess pts raw_instr.instr in begin if has_tactic then - let { it=gls ; sigma=sigma } = Proof.V82.subgoals pts in - let gl = { it=List.hd gls ; sigma=sigma } in + let { it=gls ; sigma=sigma; eff=eff } = Proof.V82.subgoals pts in + let gl = { it=List.hd gls ; sigma=sigma; eff=eff } in let env= pf_env gl in let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; gsigma = sigma; genv = env} in @@ -1469,7 +1470,7 @@ let do_instr raw_instr pts = postprocess pts raw_instr.instr; (* spiwack: this should restore a compatible semantics with v8.3 where we never stayed focused on 0 goal. *) - Decl_mode.maximal_unfocus pts + Decl_mode.maximal_unfocus () let proof_instr raw_instr = let p = Proof_global.give_me_the_proof () in diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 8f570af7e..072737dab 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -65,7 +65,7 @@ let vernac_decl_proof () = if Proof.is_done pf then Errors.error "Nothing left to prove here." else - Proof.transaction pf begin fun () -> + begin Decl_proof_instr.go_to_proof_mode () ; Proof_global.set_proof_mode "Declarative" ; Vernacentries.print_subgoals () @@ -73,14 +73,14 @@ let vernac_decl_proof () = (* spiwack: some bureaucracy is not performed here *) let vernac_return () = - Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () -> + begin Decl_proof_instr.return_from_tactic_mode () ; Proof_global.set_proof_mode "Declarative" ; Vernacentries.print_subgoals () end let vernac_proof_instr instr = - Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () -> + begin Decl_proof_instr.proof_instr instr; Vernacentries.print_subgoals () end @@ -397,4 +397,10 @@ GLOBAL: proof_instr; ; END;; - +open Vernacexpr + +let () = + Vernac_classifier.declare_vernac_classifier "decl_mode" (function + | VernacExtend (("DeclProof"|"DeclReturn"), _) -> VtProofStep, VtNow + | VernacExtend ("ProofInstr", _) -> VtProofStep, VtLater + | _ -> VtUnknown, VtNow) |