aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenvtac.ml11
-rw-r--r--proofs/evar_refiner.ml2
-rw-r--r--proofs/goal.ml2
-rw-r--r--proofs/goal_select.ml26
-rw-r--r--proofs/proof.ml129
-rw-r--r--proofs/proof.mli40
-rw-r--r--proofs/proof_bullet.ml35
-rw-r--r--proofs/proof_bullet.mli2
-rw-r--r--proofs/refiner.ml4
-rw-r--r--proofs/refiner.mli3
10 files changed, 197 insertions, 57 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 767f93787d..695e103082 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -61,10 +61,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 +75,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/evar_refiner.ml b/proofs/evar_refiner.ml
index 000b34ed0a..53254e9511 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -50,7 +50,7 @@ let w_refine (evk,evi) (ltac_var,rawc) env sigma =
let env = Evd.evar_filtered_env env evi in
let sigma',typed_c =
let flags = {
- Pretyping.use_typeclasses = true;
+ Pretyping.use_typeclasses = Pretyping.UseTC;
Pretyping.solve_unification_constraints = true;
Pretyping.fail_evar = false;
Pretyping.expand_evars = true;
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/goal_select.ml b/proofs/goal_select.ml
index 29e19778e4..e847535aaf 100644
--- a/proofs/goal_select.ml
+++ b/proofs/goal_select.ml
@@ -22,11 +22,6 @@ type t =
| SelectId of Id.t
| SelectAll
-(* Default goal selector: selector chosen when a tactic is applied
- without an explicit selector. *)
-let default_goal_selector = ref (SelectNth 1)
-let get_default_goal_selector () = !default_goal_selector
-
let pr_range_selector (i, j) =
if i = j then Pp.int i
else Pp.(int i ++ str "-" ++ int j)
@@ -53,15 +48,12 @@ let parse_goal_selector = function
with Failure _ -> CErrors.user_err Pp.(str err_msg)
end
-let () = let open Goptions in
- declare_string_option
- { optdepr = false;
- optkey = ["Default";"Goal";"Selector"] ;
- optread = begin fun () ->
- Pp.string_of_ppcmds
- (pr_goal_selector !default_goal_selector)
- end;
- optwrite = begin fun n ->
- default_goal_selector := parse_goal_selector n
- end
- }
+(* Default goal selector: selector chosen when a tactic is applied
+ without an explicit selector. *)
+let get_default_goal_selector =
+ Goptions.declare_interpreted_string_option_and_ref
+ ~depr:false
+ ~key:["Default";"Goal";"Selector"]
+ ~value:(SelectNth 1)
+ parse_goal_selector
+ (fun v -> Pp.string_of_ppcmds @@ pr_goal_selector v)
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 f1f7361317..41cb7399da 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -174,34 +174,25 @@ module Strict = struct
end
(* Current bullet behavior, controlled by the option *)
-let current_behavior = ref Strict.strict
-
-let () =
- Goptions.(declare_string_option {
- optdepr = false;
- optkey = ["Bullet";"Behavior"];
- optread = begin fun () ->
- (!current_behavior).name
- end;
- optwrite = begin fun n ->
- current_behavior :=
- try Hashtbl.find behaviors n
- with Not_found ->
- CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\"."))
- end
- })
+let current_behavior =
+ Goptions.declare_interpreted_string_option_and_ref
+ ~depr:false
+ ~key:["Bullet";"Behavior"]
+ ~value:Strict.strict
+ (fun n ->
+ try Hashtbl.find behaviors n
+ with Not_found ->
+ CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\".")))
+ (fun v -> v.name)
let put p b =
- (!current_behavior).put p b
+ (current_behavior ()).put p b
let suggest p =
- (!current_behavior).suggest p
-
-(* Better printing for bullet exceptions *)
-exception SuggestNoSuchGoals of int * Proof.t
+ (current_behavior ()).suggest p
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..29a47c5acd 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -37,6 +37,8 @@ let refiner ~check =
CProfile.profile2 refiner_key (refiner ~check)
else refiner ~check
+let refiner ~check c = Proofview.V82.tactic ~nf_evars:false (refiner ~check c)
+
(*********************)
(* Tacticals *)
(*********************)
@@ -269,5 +271,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..3471f38e9e 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -22,7 +22,7 @@ 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. } *)
@@ -32,7 +32,6 @@ val tclIDTAC_MESSAGE : Pp.t -> tactic
(** [tclEVARS sigma] changes the current evar map *)
val tclEVARS : evar_map -> tactic
-val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic
(** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 13:48:11 +0000