summaryrefslogtreecommitdiff
path: root/proofs/pfedit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/pfedit.ml')
-rw-r--r--proofs/pfedit.ml88
1 files changed, 60 insertions, 28 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 07:20:18 +0000