From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- proofs/pfedit.ml | 179 ++++++++++++++++++++++++++----------------------------- 1 file changed, 84 insertions(+), 95 deletions(-) (limited to 'proofs/pfedit.ml') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 77e7b324..fdc93bcb 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* = d then raise Proof.EmptyUndoStack; - for i = 1 to n do - Proof.undo p - done - -let current_proof_depth () = - try - let p = Proof_global.give_me_the_proof () in - Proof.V82.depth p - with Proof_global.NoCurrentProof -> -1 - -(* [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d - is the depth of the focus stack). *) -let undo_todepth n = - try - undo ((current_proof_depth ()) - n ) - with Proof_global.NoCurrentProof when n=0 -> () - -let set_undo _ = () -let get_undo _ = None - - -let start_proof id str hyps c ?init_tac ?compute_guard hook = +let start_proof (id : Id.t) str sigma hyps c ?init_tac terminator = let goals = [ (Global.env_of_context hyps , c) ] in - Proof_global.start_proof id str goals ?compute_guard hook; - let tac = match init_tac with - | Some tac -> Proofview.V82.tactic tac - | None -> Proofview.tclUNIT () - in - try Proof_global.run_tactic tac - with reraise -> Proof_global.discard_current (); raise reraise - -let restart_proof () = undo_todepth 1 - -let cook_proof hook = - let prf = Proof_global.give_me_the_proof () in - hook prf; - match Proof_global.close_proof () with - | (i,([e],cg,str,h)) -> (i,(e,cg,str,h)) - | _ -> Util.anomaly "Pfedit.cook_proof: more than one proof term." - -let xml_cook_proof = ref (fun _ -> ()) -let set_xml_cook_proof f = xml_cook_proof := f - + Proof_global.start_proof sigma id str goals terminator; + let env = Global.env () in + ignore (Proof_global.with_current_proof (fun _ p -> + match init_tac with + | None -> p,(true,[]) + | Some tac -> Proof.run_tactic env tac p)) + +let cook_this_proof p = + match p with + | { Proof_global.id;entries=[constr];persistence;universes } -> + (id,(constr,universes,persistence)) + | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") + +let cook_proof () = + cook_this_proof (fst + (Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x))) let get_pftreestate () = Proof_global.give_me_the_proof () let set_end_tac tac = - let tac = Proofview.V82.tactic tac in Proof_global.set_endline_tactic tac let set_used_variables l = @@ -96,25 +56,25 @@ let get_used_variables () = exception NoSuchGoal let _ = Errors.register_handler begin function - | NoSuchGoal -> Util.error "No such goal." + | NoSuchGoal -> Errors.error "No such goal." | _ -> raise Errors.Unhandled end let get_nth_V82_goal i = let p = Proof_global.give_me_the_proof () in - let { it=goals ; sigma = sigma } = Proof.V82.subgoals p in + let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in try - { it=(List.nth goals (i-1)) ; sigma=sigma } + { it=(List.nth goals (i-1)) ; sigma=sigma; } with Failure _ -> raise NoSuchGoal let get_goal_context_gen i = try - let { it=goal ; sigma=sigma } = get_nth_V82_goal i in - (sigma, Refiner.pf_env { it=goal ; sigma=sigma }) - with Proof_global.NoCurrentProof -> Util.error "No focused proof." +let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in +(sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) + with Proof_global.NoCurrentProof -> Errors.error "No focused proof." let get_goal_context i = try get_goal_context_gen i - with NoSuchGoal -> Util.error "No such goal." + with NoSuchGoal -> Errors.error "No such goal." let get_current_goal_context () = try get_goal_context_gen 1 @@ -125,29 +85,44 @@ let get_current_goal_context () = let current_proof_statement () = match Proof_global.V82.get_current_initial_conclusions () with - | (id,([concl],strength,hook)) -> id,strength,concl,hook - | _ -> Util.anomaly "Pfedit.current_proof_statement: more than one statement" + | (id,([concl],strength)) -> id,strength,concl + | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement") -let solve_nth ?(with_end_tac=false) gi tac = +let solve ?with_end_tac gi info_lvl tac pr = try - let tac = Proofview.V82.tactic tac in - let tac = if with_end_tac then - Proof_global.with_end_tac tac - else - tac + let tac = match with_end_tac with + | None -> tac + | Some etac -> Proofview.tclTHEN tac etac in + let tac = match info_lvl with + | None -> tac + | Some _ -> Proofview.Trace.record_info_trace tac in - Proof_global.run_tactic (Proofview.tclFOCUS gi gi tac) - with - | Proof_global.NoCurrentProof -> Util.error "No focused proof" - | Proofview.IndexOutOfRange | Failure "list_chop" -> - let msg = str "No such goal: " ++ int gi ++ str "." in - Util.errorlabstrm "" msg + let tac = match gi with + | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac + | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac + | Vernacexpr.SelectAll -> tac + | Vernacexpr.SelectAllParallel -> + Errors.anomaly(str"SelectAllParallel not handled by Stm") + in + let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in + let () = + match info_lvl with + | None -> () + | Some i -> Pp.ppnl (hov 0 (Proofview.Trace.pr_info ~lvl:i info)) + in + (p,status) + with + | Proof_global.NoCurrentProof -> Errors.error "No focused proof" + | CList.IndexOutOfRange -> + match gi with + | Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in + Errors.errorlabstrm "" msg + | _ -> assert false -let by = solve_nth 1 +let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) let instantiate_nth_evar_com n com = - let pf = Proof_global.give_me_the_proof () in - Proof.V82.instantiate_evar n com pf + Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p) (**********************************************************************) @@ -157,21 +132,29 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n -let build_constant_by_tactic id sign typ tac = - start_proof id (Global,Proof Theorem) sign typ (fun _ _ -> ()); +let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = + let evd = Evd.from_env ~ctx Environ.empty_env in + start_proof id goal_kind evd sign typ (fun _ -> ()); try - by tac; - let _,(const,_,_,_) = cook_proof (fun _ -> ()) in + let status = by tac in + let _,(const,univs,_) = cook_proof () in delete_current_proof (); - const + const, status, univs with reraise -> + let reraise = Errors.push reraise in delete_current_proof (); - raise reraise + iraise reraise -let build_by_tactic env typ tac = - let id = id_of_string ("temporary_proof"^string_of_int (next())) in +let build_by_tactic env ctx ?(poly=false) typ tac = + let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in - (build_constant_by_tactic id sign typ tac).const_entry_body + let gk = Global, poly, Proof Theorem in + let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in + let ce = Term_typing.handle_entry_side_effects env ce in + let (cb, ctx), se = Future.force ce.const_entry_body in + assert(Declareops.side_effects_is_empty se); + assert(Univ.ContextSet.is_empty ctx); + cb, status, univs (**********************************************************************) (* Support for resolution of evars in tactic interpretation, including @@ -181,13 +164,19 @@ let implicit_tactic = ref None let declare_implicit_tactic tac = implicit_tactic := Some tac -let solve_by_implicit_tactic env sigma (evk,args) = +let clear_implicit_tactic () = implicit_tactic := None + +let solve_by_implicit_tactic env sigma evk = let evi = Evd.find_undefined sigma evk in match (!implicit_tactic, snd (evar_source evk sigma)) with - | Some tac, (ImplicitArg _ | QuestionMark _) + | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when - Sign.named_context_equal (Environ.named_context_of_val evi.evar_hyps) + Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> - (try build_by_tactic env evi.evar_concl (tclCOMPLETE tac) + let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in + (try + let (ans, _, _) = + build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in + ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit -- cgit v1.2.3