aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml4
-rw-r--r--proofs/clenv.mli3
-rw-r--r--proofs/clenvtac.ml12
-rw-r--r--proofs/goal.ml2
-rw-r--r--proofs/logic.ml139
-rw-r--r--proofs/logic.mli6
-rw-r--r--proofs/proof.ml129
-rw-r--r--proofs/proof.mli40
-rw-r--r--proofs/proof_bullet.ml5
-rw-r--r--proofs/proof_bullet.mli2
-rw-r--r--proofs/refiner.ml14
-rw-r--r--proofs/refiner.mli30
12 files changed, 268 insertions, 118 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 37d54a4eea..08178052bf 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -321,10 +321,6 @@ let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl =
clenv_unify CUMUL ~flags
(meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
-let old_clenv_unique_resolver ?flags clenv gl =
- let concl = Goal.V82.concl clenv.evd (sig_it gl) in
- clenv_unique_resolver_gen ?flags clenv concl
-
let clenv_unique_resolver ?flags clenv gl =
let concl = Proofview.Goal.concl gl in
clenv_unique_resolver_gen ?flags clenv concl
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 1adfdb885a..4279ab4768 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -63,9 +63,6 @@ val clenv_unify :
?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
(** unifies the concl of the goal with the type of the clenv *)
-val old_clenv_unique_resolver :
- ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
-
val clenv_unique_resolver :
?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 767f93787d..c5e341c720 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -13,7 +13,6 @@ open Constr
open Termops
open Evd
open EConstr
-open Refiner
open Logic
open Reduction
open Clenv
@@ -61,10 +60,7 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv =
clenv_pose_metas_as_evars clenv dep_mvs
let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
- (* ppedrot: a Goal.enter here breaks things, because the tactic below may
- solve goals by side effects, while the compatibility layer keeps those
- useless goals. That deserves a FIXME. *)
- Proofview.V82.tactic begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in
let evd' =
if with_classes then
@@ -78,9 +74,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
else clenv.evd
in
let clenv = { clenv with evd = evd' } in
- tclTHEN
- (tclEVARS (Evd.clear_metas evd'))
- (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl
+ Proofview.tclTHEN
+ (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd'))
+ (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv))))
end
let clenv_pose_dependent_evars ?(with_evars=false) clenv =
diff --git a/proofs/goal.ml b/proofs/goal.ml
index b1f8fd3e97..53d3047bc7 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -69,7 +69,7 @@ module V82 = struct
let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in
let evars = Evd.restore_future_goals evars prev_future_goals in
let ctxt = Environ.named_context_of_val hyps in
- let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
+ let inst = List.map (NamedDecl.get_id %> EConstr.mkVar) ctxt in
let ev = EConstr.mkEvar (evk,inst) in
(evk, ev, evars)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 406e71aafc..c7a1c32e7c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -28,16 +28,14 @@ module NamedDecl = Context.Named.Declaration
type refiner_error =
(* Errors raised by the refiner *)
- | BadType of constr * constr * constr
+ | BadType of constr * constr * EConstr.t
| UnresolvedBindings of Name.t list
| CannotApply of constr * constr
- | NotWellTyped of constr
| NonLinearProof of constr
| MetaInType of EConstr.constr
(* Errors raised by the tactics *)
| IntroNeedsProduct
- | DoesNotOccurIn of constr * Id.t
| NoSuchHyp of Id.t
exception RefinerError of Environ.env * Evd.evar_map * refiner_error
@@ -73,13 +71,11 @@ let catchable_exception = function
let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id))
-(* Tells if the refiner should check that the submitted rules do not
- produce invalid subgoals *)
-let check = ref false
-let with_check = Flags.with_option check
+(* The check flag tells if the refiner should check that the submitted rules do
+ not produce invalid subgoals *)
-let check_typability env sigma c =
- if !check then fst (type_of env sigma (EConstr.of_constr c)) else sigma
+let check_typability ~check env sigma c =
+ if check then fst (type_of env sigma (EConstr.of_constr c)) else sigma
(************************************************************************)
(************************************************************************)
@@ -316,9 +312,9 @@ let check_meta_variables env sigma c =
if not (List.distinct_f Int.compare (collect_meta_variables c)) then
raise (RefinerError (env, sigma, NonLinearProof c))
-let check_conv_leq_goal env sigma arg ty conclty =
- if !check then
- let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
+let check_conv_leq_goal ~check env sigma arg ty conclty =
+ if check then
+ let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) conclty in
match ans with
| Some evm -> evm
| None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
@@ -334,28 +330,27 @@ let meta_free_prefix sigma a =
in a
with Stop acc -> Array.rev_of_list acc
-let goal_type_of env sigma c =
- if !check then
+let goal_type_of ~check env sigma c =
+ if check then
let (sigma,t) = type_of env sigma (EConstr.of_constr c) in
(sigma, EConstr.Unsafe.to_constr t)
else (sigma, EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c)))
-let rec mk_refgoals sigma goal goalacc conclty trm =
- let env = Goal.V82.env sigma goal in
- let hyps = Goal.V82.hyps sigma goal in
+let rec mk_refgoals ~check env sigma goalacc conclty trm =
+ let hyps = Environ.named_context_val env in
let mk_goal hyps concl =
Goal.V82.mk_goal sigma hyps concl
in
- if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then
+ if (not check) && not (occur_meta sigma (EConstr.of_constr trm)) then
let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in
let t'ty = EConstr.Unsafe.to_constr t'ty in
- let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
+ let sigma = check_conv_leq_goal ~check env sigma trm t'ty conclty in
(goalacc,t'ty,sigma,trm)
else
match kind trm with
| Meta _ ->
- let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in
- if !check && occur_meta sigma conclty then
+ let conclty = nf_betaiota env sigma conclty in
+ if check && occur_meta sigma conclty then
raise (RefinerError (env, sigma, MetaInType conclty));
let (gl,ev,sigma) = mk_goal hyps conclty in
let ev = EConstr.Unsafe.to_constr ev in
@@ -363,9 +358,9 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
gl::goalacc, conclty, sigma, ev
| Cast (t,k, ty) ->
- let sigma = check_typability env sigma ty in
- let sigma = check_conv_leq_goal env sigma trm ty conclty in
- let res = mk_refgoals sigma goal goalacc ty t in
+ let sigma = check_typability ~check env sigma ty in
+ let sigma = check_conv_leq_goal ~check env sigma trm ty conclty in
+ let res = mk_refgoals ~check env sigma goalacc (EConstr.of_constr ty) t in
(* we keep the casts (in particular VMcast and NATIVEcast) except
when they are annotating metas *)
if isMeta t then begin
@@ -388,24 +383,24 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
let ty = EConstr.Unsafe.to_constr ty in
goalacc, ty, sigma, f
else
- mk_hdgoals sigma goal goalacc f
+ mk_hdgoals ~check env sigma goalacc f
in
- let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
- let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
+ let ((acc'',conclty',sigma), args) = mk_arggoals ~check env sigma acc' hdty l in
+ let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in
let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
(acc'',conclty',sigma, ans)
| Proj (p,c) ->
- let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
+ let (acc',cty,sigma,c') = mk_hdgoals ~check env sigma goalacc c in
let c = mkProj (p, c') in
let ty = get_type_of env sigma (EConstr.of_constr c) in
let ty = EConstr.Unsafe.to_constr ty in
(acc',ty,sigma,c)
| Case (ci,p,c,lf) ->
- let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
- let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
- let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in
+ let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in
+ let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in
+ let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in
let lf' = Array.rev_of_list rbranches in
let ans =
if p' == p && c' == c && Array.equal (==) lf' lf then trm
@@ -416,28 +411,27 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
| _ ->
if occur_meta sigma (EConstr.of_constr trm) then
anomaly (Pp.str "refiner called with a meta in non app/case subterm.");
- let (sigma, t'ty) = goal_type_of env sigma trm in
- let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
+ let (sigma, t'ty) = goal_type_of ~check env sigma trm in
+ let sigma = check_conv_leq_goal ~check env sigma trm t'ty conclty in
(goalacc,t'ty,sigma, trm)
(* Same as mkREFGOALS but without knowing the type of the term. Therefore,
* Metas should be casted. *)
-and mk_hdgoals sigma goal goalacc trm =
- let env = Goal.V82.env sigma goal in
- let hyps = Goal.V82.hyps sigma goal in
+and mk_hdgoals ~check env sigma goalacc trm =
+ let hyps = Environ.named_context_val env in
let mk_goal hyps concl =
Goal.V82.mk_goal sigma hyps concl in
match kind trm with
| Cast (c,_, ty) when isMeta c ->
- let sigma = check_typability env sigma ty in
+ let sigma = check_typability ~check env sigma ty in
let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in
let ev = EConstr.Unsafe.to_constr ev in
gl::goalacc,ty,sigma,ev
| Cast (t,_, ty) ->
- let sigma = check_typability env sigma ty in
- mk_refgoals sigma goal goalacc ty t
+ let sigma = check_typability ~check env sigma ty in
+ mk_refgoals ~check env sigma goalacc (EConstr.of_constr ty) t
| App (f,l) ->
let (acc',hdty,sigma,applicand) =
@@ -445,15 +439,15 @@ and mk_hdgoals sigma goal goalacc trm =
then
let l' = meta_free_prefix sigma l in
(goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f)
- else mk_hdgoals sigma goal goalacc f
+ else mk_hdgoals ~check env sigma goalacc f
in
- let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
+ let ((acc'',conclty',sigma), args) = mk_arggoals ~check env sigma acc' hdty l in
let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
(acc'',conclty',sigma, ans)
| Case (ci,p,c,lf) ->
- let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
- let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in
+ let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in
+ let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in
let lf' = Array.rev_of_list rbranches in
let ans =
if p' == p && c' == c && Array.equal (==) lf' lf then trm
@@ -462,21 +456,21 @@ and mk_hdgoals sigma goal goalacc trm =
(acc'',conclty',sigma, ans)
| Proj (p,c) ->
- let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
+ let (acc',cty,sigma,c') = mk_hdgoals ~check env sigma goalacc c in
let c = mkProj (p, c') in
let ty = get_type_of env sigma (EConstr.of_constr c) in
let ty = EConstr.Unsafe.to_constr ty in
(acc',ty,sigma,c)
| _ ->
- if !check && occur_meta sigma (EConstr.of_constr trm) then
+ if check && occur_meta sigma (EConstr.of_constr trm) then
anomaly (Pp.str "refine called with a dependent meta.");
- let (sigma, ty) = goal_type_of env sigma trm in
+ let (sigma, ty) = goal_type_of env ~check sigma trm in
goalacc, ty, sigma, trm
-and mk_arggoals sigma goal goalacc funty allargs =
+and mk_arggoals ~check env sigma goalacc funty allargs =
let foldmap (goalacc, funty, sigma) harg =
- let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in
+ let t = whd_all env sigma (EConstr.of_constr funty) in
let t = EConstr.Unsafe.to_constr t in
let rec collapse t = match kind t with
| LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
@@ -485,19 +479,17 @@ and mk_arggoals sigma goal goalacc funty allargs =
let t = collapse t in
match kind t with
| Prod (_, c1, b) ->
- let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in
+ let (acc, hargty, sigma, arg) = mk_refgoals ~check env sigma goalacc (EConstr.of_constr c1) harg in
(acc, subst1 harg b, sigma), arg
| _ ->
- let env = Goal.V82.env sigma goal in
raise (RefinerError (env,sigma,CannotApply (t, harg)))
in
Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs
-and mk_casegoals sigma goal goalacc p c =
- let env = Goal.V82.env sigma goal in
- let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in
+and mk_casegoals ~check env sigma goalacc p c =
+ let (acc',ct,sigma,c') = mk_hdgoals ~check env sigma goalacc c in
let ct = EConstr.of_constr ct in
- let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in
+ let (acc'',pt,sigma,p') = mk_hdgoals ~check env sigma acc' p in
let ((ind, u), spec) =
try Tacred.find_hnf_rectype env sigma ct
with Not_found -> anomaly (Pp.str "mk_casegoals.") in
@@ -505,20 +497,19 @@ and mk_casegoals sigma goal goalacc p c =
let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in
(acc'',lbrty,conclty,sigma,p',c')
-and treat_case sigma goal ci lbrty lf acc' =
+and treat_case ~check env sigma ci lbrty lf acc' =
let rec strip_outer_cast c = match kind c with
| Cast (c,_,_) -> strip_outer_cast c
| _ -> c in
let decompose_app_vect c = match kind c with
| App (f,cl) -> (f, cl)
| _ -> (c,[||]) in
- let env = Goal.V82.env sigma goal in
Array.fold_left3
(fun (lacc,sigma,bacc) ty fi l ->
if isMeta (strip_outer_cast fi) then
(* Support for non-eta-let-expanded Meta as found in *)
(* destruct/case with an non eta-let expanded elimination scheme *)
- let (r,_,s,fi') = mk_refgoals sigma goal lacc ty fi in
+ let (r,_,s,fi') = mk_refgoals ~check env sigma lacc ty fi in
r,s,(fi'::bacc)
else
(* Deal with a branch in expanded form of the form
@@ -539,14 +530,14 @@ and treat_case sigma goal ci lbrty lf acc' =
if isMeta head then begin
assert (args = Context.Rel.to_extended_vect mkRel 0 ctx);
let head' = lift (-n) head in
- let (r,_,s,head'') = mk_refgoals sigma goal lacc ty head' in
+ let (r,_,s,head'') = mk_refgoals ~check env sigma lacc ty head' in
let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in
(r,s,fi'::bacc)
end
else
(* Supposed to be meta-free *)
- let sigma, t'ty = goal_type_of env sigma fi in
- let sigma = check_conv_leq_goal env sigma fi t'ty ty in
+ let sigma, t'ty = goal_type_of ~check env sigma fi in
+ let sigma = check_conv_leq_goal ~check env sigma fi t'ty ty in
(lacc,sigma,fi::bacc))
(acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags
@@ -574,18 +565,18 @@ let convert_hyp ~check ~reorder env sigma d =
(************************************************************************)
(* Primitive tactics are handled here *)
-let prim_refiner r sigma goal =
- let env = Goal.V82.env sigma goal in
- let cl = Goal.V82.concl sigma goal in
- let cl = EConstr.Unsafe.to_constr cl in
+let refiner ~check r =
+ let open Proofview.Notations in
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let st = Proofview.Goal.state gl in
+ let cl = Proofview.Goal.concl gl in
check_meta_variables env sigma r;
- let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl r in
- let sgl = List.rev sgl in
- let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in
- (sgl, sigma)
-
-let prim_refiner ~check r sigma goal =
- if check then
- with_check (prim_refiner r sigma) goal
- else
- prim_refiner r sigma goal
+ let (sgl,cl',sigma,oterm) = mk_refgoals ~check env sigma [] cl r in
+ let map gl = Proofview.goal_with_state gl st in
+ let sgl = List.rev_map map sgl in
+ let sigma = Goal.V82.partial_solution env sigma (Proofview.Goal.goal gl) (EConstr.of_constr oterm) in
+ Proofview.Unsafe.tclEVARS sigma <*>
+ Proofview.Unsafe.tclSETGOALS sgl
+ end
diff --git a/proofs/logic.mli b/proofs/logic.mli
index ef8b2731b2..9dc75000a1 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -26,23 +26,21 @@ open Evd
(** The primitive refiner. *)
-val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal list * evar_map
+val refiner : check:bool -> constr -> unit Proofview.tactic
(** {6 Refiner errors. } *)
type refiner_error =
(*i Errors raised by the refiner i*)
- | BadType of constr * constr * constr
+ | BadType of constr * constr * EConstr.t
| UnresolvedBindings of Name.t list
| CannotApply of constr * constr
- | NotWellTyped of constr
| NonLinearProof of constr
| MetaInType of EConstr.constr
(*i Errors raised by the tactics i*)
| IntroNeedsProduct
- | DoesNotOccurIn of constr * Id.t
| NoSuchHyp of Id.t
exception RefinerError of Environ.env * evar_map * refiner_error
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 21006349d2..75aca7e7ff 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -63,7 +63,7 @@ exception CannotUnfocusThisWay
(* Cannot focus on non-existing subgoals *)
exception NoSuchGoals of int * int
-exception NoSuchGoal of Names.Id.t
+exception NoSuchGoal of Names.Id.t option
exception FullyUnfocused
@@ -74,8 +74,10 @@ let _ = CErrors.register_handler begin function
Some Pp.(str "[Focus] No such goal (" ++ int i ++ str").")
| NoSuchGoals (i,j) ->
Some Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.")
- | NoSuchGoal id ->
+ | NoSuchGoal (Some id) ->
Some Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
+ | NoSuchGoal None ->
+ Some Pp.(str "[Focus] No such goal.")
| FullyUnfocused ->
Some (Pp.str "The proof is not focused")
| _ -> None
@@ -233,7 +235,7 @@ let focus_id cond inf id pr =
raise CannotUnfocusThisWay
end
| None ->
- raise (NoSuchGoal id)
+ raise (NoSuchGoal (Some id))
end
let rec unfocus kind pr () =
@@ -506,3 +508,124 @@ let pr_proof p =
str "given up: " ++ pr_goal_list given_up ++
str "]"
)
+
+let use_unification_heuristics =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Solve";"Unification";"Constraints"]
+ ~value:true
+
+exception SuggestNoSuchGoals of int * t
+
+let solve ?with_end_tac gi info_lvl tac pr =
+ 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
+ let nosuchgoal = Proofview.tclZERO (SuggestNoSuchGoals (1,pr)) in
+ let tac = let open Goal_select in match gi with
+ | SelectAlreadyFocused ->
+ let open Proofview.Notations in
+ Proofview.numgoals >>= fun n ->
+ if n == 1 then tac
+ else
+ let e = CErrors.UserError
+ (None,
+ Pp.(str "Expected a single focused goal but " ++
+ int n ++ str " goals are focused."))
+ in
+ Proofview.tclZERO e
+
+ | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
+ | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
+ | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac
+ | SelectAll -> tac
+ in
+ let tac =
+ if use_unification_heuristics () then
+ Proofview.tclTHEN tac Refine.solve_constraints
+ else tac
+ in
+ let env = Global.env () in
+ let (p,(status,info),()) = run_tactic env tac pr in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let () =
+ match info_lvl with
+ | None -> ()
+ | Some i -> Feedback.msg_info (Pp.hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info))
+ in
+ (p,status)
+
+(**********************************************************************)
+(* Shortcut to build a term using tactics *)
+
+let refine_by_tactic ~name ~poly env sigma ty tac =
+ (* Save the initial side-effects to restore them afterwards. We set the
+ current set of side-effects to be empty so that we can retrieve the
+ ones created during the tactic invocation easily. *)
+ let eff = Evd.eval_side_effects sigma in
+ let sigma = Evd.drop_side_effects sigma in
+ (* Save the existing goals *)
+ let prev_future_goals = Evd.save_future_goals sigma in
+ (* Start a proof *)
+ let prf = start ~name ~poly sigma [env, ty] in
+ let (prf, _, ()) =
+ try run_tactic env tac prf
+ with Logic_monad.TacticFailure e as src ->
+ (* Catch the inner error of the monad tactic *)
+ let (_, info) = Exninfo.capture src in
+ Exninfo.iraise (e, info)
+ in
+ (* Plug back the retrieved sigma *)
+ let { goals; stack; shelf; given_up; sigma; entry } = data prf in
+ assert (stack = []);
+ let ans = match Proofview.initial_goals entry with
+ | [c, _] -> c
+ | _ -> assert false
+ in
+ let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in
+ (* [neff] contains the freshly generated side-effects *)
+ let neff = Evd.eval_side_effects sigma in
+ (* Reset the old side-effects *)
+ let sigma = Evd.drop_side_effects sigma in
+ let sigma = Evd.emit_side_effects eff sigma in
+ (* Restore former goals *)
+ let sigma = Evd.restore_future_goals sigma prev_future_goals in
+ (* Push remaining goals as future_goals which is the only way we
+ have to inform the caller that there are goals to collect while
+ not being encapsulated in the monad *)
+ (* Goals produced by tactic "shelve" *)
+ let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in
+ (* Goals produced by tactic "give_up" *)
+ let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in
+ (* Other goals *)
+ let sigma = List.fold_right Evd.declare_future_goal goals sigma in
+ (* Get rid of the fresh side-effects by internalizing them in the term
+ itself. Note that this is unsound, because the tactic may have solved
+ other goals that were already present during its invocation, so that
+ those goals rely on effects that are not present anymore. Hopefully,
+ this hack will work in most cases. *)
+ let neff = neff.Evd.seff_private in
+ let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in
+ ans, sigma
+
+let get_nth_V82_goal p i =
+ let { sigma; goals } = data p in
+ try { Evd.it = List.nth goals (i-1) ; sigma }
+ with Failure _ -> raise (NoSuchGoal None)
+
+let get_goal_context_gen pf i =
+ let { Evd.it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in
+ (sigma, Global.env_of_context (Goal.V82.hyps sigma goal))
+
+let get_proof_context p =
+ try get_goal_context_gen p 1
+ with
+ | NoSuchGoal _ ->
+ (* No more focused goals *)
+ let { sigma } = data p in
+ sigma, Global.env ()
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 1a0b105723..0e5bdaf07d 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -143,6 +143,8 @@ exception CannotUnfocusThisWay
Bullet.push. *)
exception NoSuchGoals of int * int
+exception NoSuchGoal of Names.Id.t option
+
(* Unfocusing command.
Raises [FullyUnfocused] if the proof is not focused.
Raises [CannotUnfocusThisWay] if the proof the unfocusing condition
@@ -207,3 +209,41 @@ end
(* returns the set of all goals in the proof *)
val all_goals : t -> Goal.Set.t
+
+(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
+ subgoal of the current focused proof. [solve SelectAll
+ tac] applies [tac] to all subgoals. *)
+
+val solve :
+ ?with_end_tac:unit Proofview.tactic
+ -> Goal_select.t
+ -> int option
+ -> unit Proofview.tactic
+ -> t
+ -> t * bool
+
+(** Option telling if unification heuristics should be used. *)
+val use_unification_heuristics : unit -> bool
+
+val refine_by_tactic
+ : name:Names.Id.t
+ -> poly:bool
+ -> Environ.env
+ -> Evd.evar_map
+ -> EConstr.types
+ -> unit Proofview.tactic
+ -> Constr.constr * Evd.evar_map
+(** A variant of the above function that handles open terms as well.
+ Caveat: all effects are purged in the returned term at the end, but other
+ evars solved by side-effects are NOT purged, so that unexpected failures may
+ occur. Ideally all code using this function should be rewritten in the
+ monad. *)
+
+exception SuggestNoSuchGoals of int * t
+
+(** {6 Helpers to obtain proof state when in an interactive proof } *)
+val get_goal_context_gen : t -> int -> Evd.evar_map * Environ.env
+
+(** [get_proof_context ()] gets the goal context for the first subgoal
+ of the proof *)
+val get_proof_context : t -> Evd.evar_map * Environ.env
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index f619bc86a1..41cb7399da 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -191,11 +191,8 @@ let put p b =
let suggest p =
(current_behavior ()).suggest p
-(* Better printing for bullet exceptions *)
-exception SuggestNoSuchGoals of int * Proof.t
-
let _ = CErrors.register_handler begin function
- | SuggestNoSuchGoals(n,proof) ->
+ | Proof.SuggestNoSuchGoals(n,proof) ->
let suffix = suggest proof in
Some (Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++
pr_non_empty_arg (fun x -> x) suffix))
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index 687781361c..f15b7824ff 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -44,5 +44,3 @@ val register_behavior : behavior -> unit
*)
val put : Proof.t -> t -> Proof.t
val suggest : Proof.t -> Pp.t
-
-exception SuggestNoSuchGoals of int * Proof.t
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 75c3436cf4..874bab277d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -12,7 +12,6 @@ open Pp
open CErrors
open Util
open Evd
-open Logic
type tactic = Proofview.V82.tac
@@ -26,16 +25,7 @@ let project x = x.sigma
let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls))
let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
-let refiner ~check pr goal_sigma =
- let (sgl,sigma') = prim_refiner ~check pr goal_sigma.sigma goal_sigma.it in
- { it = sgl; sigma = sigma'; }
-
-(* Profiling refiner *)
-let refiner ~check =
- if Flags.profile then
- let refiner_key = CProfile.declare_profile "refiner" in
- CProfile.profile2 refiner_key (refiner ~check)
- else refiner ~check
+let refiner = Logic.refiner
(*********************)
(* Tacticals *)
@@ -269,5 +259,3 @@ let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
(* Change evars *)
let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
-let tclPUSHEVARUNIVCONTEXT ctx gl =
- tclEVARS (Evd.merge_universe_context (project gl) ctx) gl
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 66eae1db81..a3cbfb5d5d 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -22,49 +22,59 @@ val project : 'a sigma -> evar_map
val pf_env : Goal.goal sigma -> Environ.env
val pf_hyps : Goal.goal sigma -> named_context
-val refiner : check:bool -> Constr.t -> tactic
+val refiner : check:bool -> Constr.t -> unit Proofview.tactic
(** {6 Tacticals. } *)
(** [tclIDTAC] is the identity tactic without message printing*)
val tclIDTAC : tactic
+[@@ocaml.deprecated "Use Tactical.New.tclIDTAC"]
val tclIDTAC_MESSAGE : Pp.t -> tactic
+[@@ocaml.deprecated]
(** [tclEVARS sigma] changes the current evar map *)
val tclEVARS : evar_map -> tactic
-val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic
+[@@ocaml.deprecated "Use Proofview.Unsafe.tclEVARS"]
(** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
[tac2] to every resulting subgoals *)
val tclTHEN : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHEN"]
(** [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More
convenient than [tclTHEN] when [n] is large *)
val tclTHENLIST : tactic list -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENLIST"]
(** [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
val tclMAP : ('a -> tactic) -> 'a list -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclMAP"]
(** [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
[(tac2 i)] to the [i]{^ th} resulting subgoal (starting from 1) *)
val tclTHEN_i : tactic -> (int -> tactic) -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHEN_i"]
(** [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
to the last resulting subgoal (previously called [tclTHENL]) *)
val tclTHENLAST : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENLAST"]
(** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
to the first resulting subgoal *)
val tclTHENFIRST : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENFIRST"]
(** [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to
[gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
an error if the number of resulting subgoals is not [n] *)
val tclTHENSV : tactic -> tactic array -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENSV"]
(** Same with a list of tactics *)
val tclTHENS : tactic -> tactic list -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENS"]
(** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
@@ -72,15 +82,18 @@ val tclTHENS : tactic -> tactic list -> tactic
subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
error if the number of resulting subgoals is strictly less than [n+m] *)
val tclTHENS3PARTS : tactic -> tactic array -> tactic -> tactic array -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENS3PARTS"]
(** [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the
last [n] resulting subgoals and [tac2] on the remaining first subgoals *)
val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENSLASTn"]
(** [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then
applies [t1],...,[tn] on the first [n] resulting subgoals and
[tac2] for the remaining last subgoals (previously called tclTHENST) *)
val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENSFIRSTn"]
(** A special exception for levels for the Fail tactic *)
exception FailError of int * Pp.t Lazy.t
@@ -90,15 +103,28 @@ exception FailError of int * Pp.t Lazy.t
val catch_failerror : Exninfo.iexn -> unit
val tclORELSE0 : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclORELSE0"]
val tclORELSE : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclORELSE"]
val tclREPEAT : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclREPEAT"]
val tclFIRST : tactic list -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclFIRST"]
val tclTRY : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTRY"]
val tclTHENTRY : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENTRY"]
val tclCOMPLETE : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclCOMPLETE"]
val tclAT_LEAST_ONCE : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclAT_LEAST_ONCE"]
val tclFAIL : int -> Pp.t -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclFAIL"]
val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclFAIL_lazy"]
val tclDO : int -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclDO"]
val tclPROGRESS : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclPROGRESS"]
val tclSHOWHYPS : tactic -> tactic
+[@@ocaml.deprecated "Internal tactic. Do not use."]
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 05:18:13 +0000