From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- proofs/pfedit.ml | 88 ++++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 60 insertions(+), 28 deletions(-) (limited to 'proofs/pfedit.ml') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index b635cc96..eddbf72a 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -13,6 +13,17 @@ open Entries open Environ open Evd +let use_unification_heuristics_ref = ref true +let _ = Goptions.declare_bool_option { + Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optname = "Solve unification constraints at every \".\""; + Goptions.optkey = ["Solve";"Unification";"Constraints"]; + Goptions.optread = (fun () -> !use_unification_heuristics_ref); + Goptions.optwrite = (fun a -> use_unification_heuristics_ref:=a); +} + +let use_unification_heuristics () = !use_unification_heuristics_ref + let refining = Proof_global.there_are_pending_proofs let check_no_pending_proofs = Proof_global.check_no_pending_proof @@ -39,7 +50,7 @@ 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.") + | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") let cook_proof () = cook_this_proof (fst @@ -59,9 +70,9 @@ let get_universe_binders () = Proof_global.get_universe_binders () exception NoSuchGoal -let _ = Errors.register_handler begin function - | NoSuchGoal -> Errors.error "No such goal." - | _ -> raise Errors.Unhandled +let _ = CErrors.register_handler begin function + | NoSuchGoal -> CErrors.error "No such goal." + | _ -> raise CErrors.Unhandled end let get_nth_V82_goal i = let p = Proof_global.give_me_the_proof () in @@ -71,26 +82,38 @@ let get_nth_V82_goal i = 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 -> Errors.error "No focused proof." + let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in + (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) let get_goal_context i = try get_goal_context_gen i - with NoSuchGoal -> Errors.error "No such goal." + with Proof_global.NoCurrentProof -> CErrors.error "No focused proof." + | NoSuchGoal -> CErrors.error "No such goal." let get_current_goal_context () = try get_goal_context_gen 1 - with NoSuchGoal -> + with Proof_global.NoCurrentProof -> CErrors.error "No focused proof." + | NoSuchGoal -> (* spiwack: returning empty evar_map, since if there is no goal, under focus, there is no accessible evar either *) - (Evd.empty, Global.env ()) + let env = Global.env () in + (Evd.from_env env, env) + +let get_current_context () = + try get_goal_context_gen 1 + with Proof_global.NoCurrentProof -> + let env = Global.env () in + (Evd.from_env env, env) + | NoSuchGoal -> + (* No more focused goals ? *) + let p = get_pftreestate () in + let evd = Proof.in_proof p (fun x -> x) in + (evd, Global.env ()) let current_proof_statement () = match Proof_global.V82.get_current_initial_conclusions () with | (id,([concl],strength)) -> id,strength,concl - | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement") + | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement") let solve ?with_end_tac gi info_lvl tac pr = try @@ -103,24 +126,28 @@ let solve ?with_end_tac gi info_lvl tac pr = in let tac = match gi with | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac + | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac | Vernacexpr.SelectAll -> tac - | Vernacexpr.SelectAllParallel -> - Errors.anomaly(str"SelectAllParallel not handled by Stm") + in + let tac = + if use_unification_heuristics () then + Proofview.tclTHEN tac Refine.solve_constraints + else tac in let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in let () = match info_lvl with | None -> () - | Some i -> Pp.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info)) + | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info)) in (p,status) with - | Proof_global.NoCurrentProof -> Errors.error "No focused proof" + | Proof_global.NoCurrentProof -> CErrors.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 + CErrors.errorlabstrm "" msg | _ -> assert false let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) @@ -138,22 +165,24 @@ let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = let evd = Evd.from_ctx ctx in - start_proof id goal_kind evd sign typ (fun _ -> ()); + let terminator = Proof_global.make_terminator (fun _ -> ()) in + start_proof id goal_kind evd sign typ terminator; try let status = by tac in let _,(const,univs,_) = cook_proof () in delete_current_proof (); const, status, fst univs with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in delete_current_proof (); iraise reraise -let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = +let build_by_tactic ?(side_eff=true) env sigma ?(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 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, status, univs = + build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in let ce = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce else { ce with @@ -176,7 +205,7 @@ let refine_by_tactic env sigma ty tac = try Proof.run_tactic env tac prf with Logic_monad.TacticFailure e as src -> (** Catch the inner error of the monad tactic *) - let (_, info) = Errors.push src in + let (_, info) = CErrors.push src in iraise (e, info) in (** Plug back the retrieved sigma *) @@ -203,7 +232,7 @@ let refine_by_tactic env sigma ty tac = (* Support for resolution of evars in tactic interpretation, including resolution by application of tactics *) -let implicit_tactic = ref None +let implicit_tactic = Summary.ref None ~name:"implicit-tactic" let declare_implicit_tactic tac = implicit_tactic := Some tac @@ -214,12 +243,15 @@ let solve_by_implicit_tactic env sigma evk = match (!implicit_tactic, snd (evar_source evk sigma)) with | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when - Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps) + Context.Named.equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> - let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in + let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.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 + let c = Evarutil.nf_evars_universes sigma evi.evar_concl in + if Evarutil.has_undefined_evars sigma c then raise Exit; + let (ans, _, ctx) = + build_by_tactic env (Evd.evar_universe_context sigma) c tac in + let sigma = Evd.set_universe_context sigma ctx in + sigma, ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit -- cgit v1.2.3