(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)
(** This files defines the basic mechanism of proofs: the [proofview] type is the state which tactics manipulate (a global state for existential variables, together with the list of goals), and the type ['a tactic] is the (abstract) type of tactics modifying the proof
state and returning a value of type ['a]. *)
open Pp open Util open Proofview_monad open Context.Named.Declaration
(** Main state of tactics *) type proofview = Proofview_monad.proofview
(* evar env * proofs (under construction).
* statements that are being proved. *) type entry = (Environ.named_context_val * EConstr.constr * EConstr.types) list
(** Returns a stylised view of a proofview for use by, for instance,
ide-s. *) (* spiwack: the type of [proofview] will change as we push more refined functions to ide-s. This would be better than spawning a
new nearly identical function every time. Hence the generic name. *) (* In this version: returns the list of focused goals together with
the [evar_map] context. *) let proofview p = List.map drop_state p.comb , p.solution
let compact el ({ solution } as pv) = let nf c = Evarutil.nf_evar solution c in let nf0 c = EConstr.(to_constr ~abort_on_undefined_evars:false solution (of_constr c)) in let nf_hyps hyps = Environ.map_named_val (fun d -> map_constr nf0 d) hyps in letsize = Evd.fold (fun _ _ i -> i+1) solution 0 in let new_el = List.map (fun (hyps,t,ty) -> nf_hyps hyps, nf t, nf ty) el in let pruned_solution = Evd.drop_all_defined solution in let apply_subst_einfo _ ei = Evd.map_evar_info nf ei in let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n"size new_size));
new_el, { pv with solution = new_solution; }
(** {6 Starting and querying a proof view} *)
type telescope =
| TNil of Evd.evar_map
| TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
let map_telescope_evd f = function
| TNil sigma -> TNil (f sigma)
| TCons (env,sigma,ty,g) -> TCons(env,(f sigma),ty,g)
let dependent_init = (* Goals don't have a source location. *) let src = Loc.tag @@ Evar_kinds.GoalEvar in (* Main routine *) let rec aux = function
| TNil sigma -> [], { solution = sigma; comb = [] }
| TCons (env, sigma, typ, t) -> let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~typeclass_candidate:false typ in let (gl, _) = EConstr.destEvar sigma econstr in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let entry = (Environ.named_context_val env, econstr, typ) :: ret in
entry, { solution = sol; comb = with_empty_state gl :: comb } in fun t -> let t = map_telescope_evd Evd.push_future_goals t in let entry, v = aux t in (* The created goal are not to be shelved. *) let _goals, solution = Evd.pop_future_goals v.solution in
entry, { v with solution }
let init = let rec aux sigma = function
| [] -> TNil sigma
| (env,g)::l -> TCons (env,sigma,g,(fun sigma _ -> aux sigma l)) in fun sigma l -> dependent_init (aux sigma l)
let initial_goals initial = initial
let finished = function
| {comb = []} -> true
| _ -> false
let return { solution=defs } = defs
let return_constr { solution = defs } c = Evarutil.nf_evar defs c
let cleared_alias evd g = let evk = drop_state g in let state = get_state g in Option.map (fun g -> goal_with_state g state) (Evarutil.advance evd evk)
(** [undefined defs l] is the list of goals in [l] which are still
unsolved (after advancing cleared goals). Note that order matters. *) let undefined_evars defs l = let fold evk (seen, ans as accu) = match Evarutil.advance defs evk with
| None -> accu
| Some evk -> if Evar.Set.mem evk seen then accu else (Evar.Set.add evk seen, evk :: ans) in
snd @@ List.fold_right fold l (Evar.Set.empty, [])
let undefined defs l = let fold gl (seen, ans as accu) = match cleared_alias defs gl with
| None -> accu
| Some gl -> let evk = drop_state gl in if Evar.Set.mem evk seen then accu else (Evar.Set.add evk seen, gl :: ans) in
snd @@ List.fold_right fold l (Evar.Set.empty, [])
(** {6 Focusing commands} *)
(** A [focus_context] represents the part of the proof view which has been removed by a focusing action, it can be used to unfocus later
on. *) (* First component is a reverse list of the goals which come before and second component is the list of the goals which go after (in
the expected order). *) type focus_context = goal_with_state list * goal_with_state list
(** Returns a stylised view of a focus_context for use by, for
instance, ide-s. *) (* spiwack: the type of [focus_context] will change as we push more refined functions to ide-s. This would be better than spawning a
new nearly identical function every time. Hence the generic name. *) (* In this version: the goals in the context, as a "zipper" (the first
list is in reversed order). *) let focus_context sigma (left,right) =
(undefined_evars sigma (List.map drop_state left), undefined_evars sigma (List.map drop_state right))
(** This (internal) function extracts a sublist between two indices, and returns this sublist together with its context: if it returns [(a,(b,c))] then [a] is the sublist and [(rev b) @ a @ c] is the original list. The focused list has length [j-i-1] and contains the goals from number [i] to number [j] (both included) the first goal of the list being numbered [1]. [focus_sublist i j l] raises [IndexOutOfRange] if [i > length l], or [j > length l] or [j <
i]. *) let focus_sublist i j l = let (left,sub_right) = CList.goto (i-1) l in let (sub, right) = try CList.chop (j-i+1) sub_right with Failure _ -> raise CList.IndexOutOfRange in
(sub, (left,right))
(** Inverse operation to the previous one. *) let unfocus_sublist (left,right) s =
CList.rev_append left (s@right)
(** [focus i j] focuses a proofview on the goals from index [i] to index [j] (inclusive, goals are indexed from [1]). I.e. goals number [i] to [j] become the only focused goals of the returned proofview. It returns the focused proofview, and a context for
the focus stack. *) let focus i j sp = let (new_comb, (left, right)) = focus_sublist i j sp.comb in
( { sp with comb = new_comb } , (left, right) )
(* Returns [ev, Some n] if [n] is the index of evar [ev] with name [id] in the list of currently focused goals, or [ev, None] if [ev] is shelved.
Raises [Not_found] if the evar does not exist. *) let find_evar_in_pv id pv = let ev = Evd.evar_key id pv.solution in let comb = CList.map drop_state pv.comb in try ev, Some (CList.index Evar.equal ev comb) with Not_found -> ev, None
(** Unfocuses a proofview with respect to a context. *) let unfocus (left, right) sp =
{ sp with comb = undefined sp.solution (unfocus_sublist (left, right) sp.comb) }
let with_empty_state = Proofview_monad.with_empty_state let drop_state = Proofview_monad.drop_state let goal_with_state = Proofview_monad.goal_with_state
(** {6 The tactic monad} *)
(** - Tactics are objects which apply a transformation to all the subgoals of the current view at the same time. By opposition to the old vision of applying it to a single goal. It allows tactics such as [shelve_unifiable], tactics to reorder the focused goals, or global automation tactic for dependent subgoals (instantiating an evar has influences on the other goals of the proof in progress, not being able to take that into account causes the current eauto tactic to fail on some instances where it could succeed). Another benefit is that it is possible to write tactics that can be executed even if there are no focused goals. - Tactics form a monad ['a tactic], in a sense a tactic can be seen as a function (without argument) which returns a value of type 'a and modifies the environment (in our case: the view). Tactics of course have arguments, but these are given at the meta-level as OCaml functions. Most tactics in the sense we are used to return [()], that is no really interesting values. But some might pass information around. The tactics seen in Rocq's Ltac are (for now at least) only [unit tactic], the return values are kept for the OCaml toolkit. The operation or the monad are [Proofview.tclUNIT] (which is the "return" of the tactic monad) [Proofview.tclBIND] (which is the "bind") and [Proofview.tclTHEN] (which is a specialized bind on unit-returning tactics). - Tactics have support for full-backtracking. Tactics can be seen having multiple success: if after returning the first success a failure is encountered, the tactic can backtrack and use a second success if available. The state is backtracked to its previous value, except the non-logical state defined in the {!NonLogical} module below.
*) (* spiwack: as far as I'm aware this doesn't really relate to
F. Kirchner and C. Muñoz. *)
module Proof = Logical
(** type of tactics:
tactics can - access the environment, - report unsafe status, shelved goals and given up goals - access and change the current [proofview]
- backtrack on previous changes of the proofview *) type +'a tactic = 'a Proof.t
(** Applies a tactic to the current proofview. *) let apply ~name ~poly env t sp = letopen Logic_monad in
NewProfile.profile "Proofview.apply" (fun () -> let ans = Proof.repr (Proof.run t P.{trace=false; name; poly} (sp,env)) in let ans = Logic_monad.NonLogical.run ans in match ans with
| Nil (e, info) -> Exninfo.iraise (TacticFailure e, info)
| Cons ((r, (state, env), status, info), _) ->
r, state, env, status, Trace.to_tree info)
()
(** {7 Monadic primitives} *)
(** Unit of the tactic monad. *) let tclUNIT = Proof.return
(** Bind operation of the tactic monad. *) let tclBIND = Proof.(>>=)
(** Interprets the ";" (semicolon) of Ltac. As a monadic operation,
it's a specialized "bind". *) let tclTHEN = Proof.(>>)
(** [tclIGNORE t] has the same operational content as [t], but drops
the returned value. *) let tclIGNORE = Proof.ignore
module Monad = Proof
(** {7 Failure and backtracking} *)
(** [tclZERO e] fails with exception [e]. It has no success. *) let tclZERO ?(info=Exninfo.null) e = ifnot (CErrors.noncritical e) then
CErrors.anomaly (Pp.str "tclZERO receiving critical error: " ++ CErrors.print e);
Proof.zero (e, info)
(** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever the successes of [t1] have been depleted and it failed with [e], then it behaves as [t2 e]. In other words, [tclOR] inserts a
backtracking point. *) let tclOR = Proof.plus
(** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one success or [t2 e] if [t1] fails with [e]. It is analogous to [try/with] handler of exception in that it is not a backtracking
point. *) let tclORELSE t1 t2 = letopen Logic_monad in letopen Proof in
split t1 >>= function
| Nil e -> t2 e
| Cons (a,t1') -> plus (return a) t1'
(** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a] succeeds at least once then it behaves as [tclBIND a s] otherwise,
if [a] fails with [e], then it behaves as [f e]. *) let tclIFCATCH a s f = letopen Logic_monad in letopen Proof in
split a >>= function
| Nil e -> f e
| Cons (x,a') -> plus (s x) (fun e -> (a' e) >>= fun x' -> (s x'))
(** [tclONCE t] behave like [t] except it has at most one success: [tclONCE t] stops after the first success of [t]. If [t] fails
with [e], [tclONCE t] also fails with [e]. *) let tclONCE = Proof.once
exception MoreThanOneSuccess let _ = CErrors.register_handler begin function
| MoreThanOneSuccess ->
Some (Pp.str "This tactic has more than one success.")
| _ -> None end
(** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one success. Otherwise it fails. The tactic [t] is run until its first success, then a failure with exception [e] is simulated. It [t] yields another success, then [tclEXACTLY_ONCE e t] fails with [MoreThanOneSuccess] (it is a user error). Otherwise, [tclEXACTLY_ONCE e t] succeeds with the first success of [t]. Notice that the choice of [e] is relevant, as the presence of
further successes may depend on [e] (see {!tclOR}). *) let tclEXACTLY_ONCE e t = letopen Logic_monad in letopen Proof in
split t >>= function
| Nil (e, info) -> tclZERO ~info e
| Cons (x,k) -> let info = Exninfo.null in
Proof.split (k (e, Exninfo.null)) >>= function
| Nil _ -> tclUNIT x
| _ -> tclZERO ~info MoreThanOneSuccess
(** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *) type'a case =
| Fail of Exninfo.iexn
| Next of'a * (Exninfo.iexn -> 'a tactic) let tclCASE t = letopen Logic_monad in letmap = function
| Nil e -> Fail e
| Cons (x, t) -> Next (x, t) in
Proof.mapmap (Proof.split t)
let tclBREAK = Proof.break
(** {7 Focusing tactics} *)
(** Represents a range selector as accepted by [tclFOCUSSELECTORLIST]. *) type goal_range_selector =
| NthSelector of int
| RangeSelector of (int * int)
| IdSelector of Names.Id.t
exception NoSuchGoals of int
exception CannotSelectShelvedAndFocused
let _ = CErrors.register_handler begin function
| NoSuchGoals n ->
Some (str "No such " ++ str (String.plural n "goal") ++ str ".")
| CannotSelectShelvedAndFocused ->
Some (str "Cannot simultaneously select shelved and unshelved goals.")
| _ -> None end
(** [tclFOCUS ?nosuchgoal i j t] applies [t] in a context where only the goals numbered [i] to [j] are focused (the rest of the goals is restored at the end of the tactic). If the range [i]-[j] is not
valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *) let tclFOCUS ?nosuchgoal i j t = let nosuchgoal ~info = Option.default (tclZERO ~info (NoSuchGoals (j+1-i))) nosuchgoal in letopen Proof in
Pv.get >>= fun initial -> try let (focused,context) = focus i j initial in
Pv.set focused >>
t >>= fun result ->
Pv.modify (fun next -> unfocus context next) >>
return result with CList.IndexOutOfRange as exn -> let _, info = Exninfo.capture exn in
nosuchgoal ~info
let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t
(** Like {!tclFOCUS} but selects goals on the shelf, applies [t], and shelves generated subgoals.
This method assumes that the list [evs] is a list of existing evars. *) let tclFOCUSSHELF ?(nosuchgoal=tclZERO (NoSuchGoals 1)) evs t = if CList.is_empty evs then nosuchgoal else letopen Proof in
Comb.get >>= fun initial_comb ->
Comb.set (CList.map with_empty_state evs) >>
t >>= fun result ->
Comb.get >>= fun subgoals ->
Comb.set initial_comb >> let subgoals = CList.filter_map (fun ev -> let ev = drop_state ev in (* If ev is still undefined, leave it on its original shelf *) if (CList.mem_f Evar.equal ev evs) then None else Some ev)
subgoals in
Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution (undefined_evars pv.solution subgoals) }) >>
return result
let tclFOCUSLIST ?(nosuchgoal=tclZERO (NoSuchGoals 0)) l t = letopen Proof in
Comb.get >>= fun comb -> let n = CList.length comb in let ok (i, j) = 1 <= i && i <= j && j <= n in ifnot (CList.for_all ok l) then nosuchgoal else match l with
| [] -> nosuchgoal
| (mi, _) :: _ -> (* Get the left-most goal to focus. This goal won't move, and we
will then place all the other goals to focus to the right. *) let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in (* [CList.goto] returns a zipper, so that
[(rev left) @ sub_right = comb]. *) let left, sub_right = CList.goto (mi-1) comb in let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in letsub, right = CList.partitioni p sub_right in let mj = mi - 1 + CList.length subin
Comb.set (CList.rev_append left (sub @ right)) >>
tclFOCUS mi mj t
let tclFOCUSSELECTORLIST ?(nosuchgoal=tclZERO (NoSuchGoals 0)) l t = letopen Proof in
Pv.get >>= fun initial -> try let (ranges, shelved_evars) =
CList.partition_map (function
| NthSelector n -> Left (n, n)
| RangeSelector r -> Left r
| IdSelector id -> match find_evar_in_pv id initial with
| ev, Some n -> Left (n, n) (* goal is focused with index n *)
| ev, None -> Right ev (* goal is shelved *)) l in match CList.is_empty ranges, CList.is_empty shelved_evars with
| true, true -> nosuchgoal
| true, false -> tclFOCUSSHELF ~nosuchgoal shelved_evars t
| false, true -> tclFOCUSLIST ~nosuchgoal ranges t
| false, false -> tclZERO CannotSelectShelvedAndFocused with Not_found -> nosuchgoal
(** Like {!tclFOCUS} but selects a single goal by name. *) let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t = letopen Proof in
Pv.get >>= fun initial -> try match find_evar_in_pv id initial with
| ev, Some n -> (* Goal is under focus with index n *) let (focused,context) = focus n n initial in
Pv.set focused >>
t >>= fun result ->
Pv.modify (fun next -> unfocus context next) >>
return result
| ev, None -> (* Goal is shelved. *)
tclFOCUSSHELF ~nosuchgoal [ev] t with Not_found -> nosuchgoal
(** {7 Dispatching on goals} *)
exception SizeMismatch of int*int let _ = CErrors.register_handler begin function
| SizeMismatch (i,j) -> letopen Pp in
Some (
str"Incorrect number of goals" ++ spc() ++
str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str").")
| _ -> None end
(** A variant of [Monad.List.iter] where we iter over the focused list of goals. The argument tactic is executed in a focus comprising only of the current goal, a goal which has been solved by side effect is skipped. The generated subgoals are concatenated in
order. *) let iter_goal i = letopen Proof in
Comb.get >>= fun initial ->
Proof.List.fold_left beginfun (subgoals as cur) goal ->
Solution.get >>= fun step -> match cleared_alias step goal with
| None -> return cur
| Some goal ->
Comb.set [goal] >>
i goal >>
Proof.map (fun comb -> comb :: subgoals) Comb.get end [] initial >>= fun subgoals ->
Solution.get >>= fun evd ->
Comb.set CList.(undefined evd (flatten (rev subgoals)))
(** List iter but allocates a list of results *) let map_goal i = let rev = List.rev in(* hem... Proof masks List... *) letopen Proof in
Comb.get >>= fun initial ->
Proof.List.fold_left beginfun (acc, subgoals as cur) goal ->
Solution.get >>= fun step -> match cleared_alias step goal with
| None -> return cur
| Some goal ->
Comb.set [goal] >>
i goal >>= fun res ->
Proof.map (fun comb -> comb :: subgoals) Comb.get >>= fun x ->
return (res :: acc, x) end ([],[]) initial >>= fun (results_rev, subgoals) ->
Solution.get >>= fun evd ->
Comb.set CList.(undefined evd (flatten (rev subgoals))) >>
return (rev results_rev)
(** A variant of [Monad.List.fold_left2] where the first list is the list of focused goals. The argument tactic is executed in a focus comprising only of the current goal, a goal which has been solved by side effect is skipped. The generated subgoals are concatenated
in order. *) let fold_left2_goal i s l = letopen Proof in
Pv.get >>= fun initial -> let err =
return () >>= fun () -> (* Delay the computation of list lengths. *)
tclZERO (SizeMismatch (CList.length initial.comb,CList.length l)) in
Proof.List.fold_left2 err beginfun ((r,subgoals) as cur) goal a ->
Solution.get >>= fun step -> match cleared_alias step goal with
| None -> return cur
| Some goal ->
Comb.set [goal] >>
i goal a r >>= fun r ->
Proof.map (fun comb -> (r, comb :: subgoals)) Comb.get end (s,[]) initial.comb l >>= fun (r,subgoals) ->
Solution.get >>= fun evd ->
Comb.set CList.(undefined evd (flatten (rev subgoals))) >>
return r
(** Dispatch tacticals are used to apply a different tactic to each goal under focus. They come in two flavours: [tclDISPATCH] takes a list of [unit tactic]-s and build a [unit tactic]. [tclDISPATCHL] takes a list of ['a tactic] and returns an ['a list tactic].
They both work by applying each of the tactic in a focus restricted to the corresponding goal (starting with the first goal). In the case of [tclDISPATCHL], the tactic returns a list of the same size as the argument list (of tactics), each element being the result of the tactic executed in the corresponding goal.
When the length of the tactic list is not the number of goal, raises [SizeMismatch (g,t)] where [g] is the number of available goals, and [t] the number of tactics passed.
[tclDISPATCHGEN join tacs] generalises both functions as the successive results of [tacs] are stored in reverse order in a list, and [join] is used to convert the result into the expected
form. *) let tclDISPATCHGEN0 join tacs = match tacs with
| [] -> begin letopen Proof in
Comb.get >>= function
| [] -> tclUNIT (join [])
| comb -> tclZERO (SizeMismatch (CList.length comb,0)) end
| [tac] -> begin letopen Proof in
Pv.get >>= function
| { comb=[goal] ; solution } -> beginmatch cleared_alias solution goal with
| None -> tclUNIT (join [])
| Some _ -> Proof.map (fun res -> join [res]) tac end
| {comb} -> tclZERO (SizeMismatch(CList.length comb,1)) end
| _ -> let iter _ t cur = Proof.map (fun y -> y :: cur) t in let ans = fold_left2_goal iter [] tacs in
Proof.map join ans
let tclDISPATCHGEN join tacs = let branch t = InfoL.tag (Info.DBranch) t in let tacs = CList.map branch tacs in
InfoL.tag (Info.Dispatch) (tclDISPATCHGEN0 join tacs)
let tclDISPATCH tacs = tclDISPATCHGEN ignore tacs
let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs
(** [extend_to_list startxs rx endxs l] builds a list [startxs @ [rx,...,rx] @ endxs] of the same length as [l]. Raises
[SizeMismatch] if [startxs @ endxs] is already longer than [l]. *) let extend_to_list startxs rx endxs l = (* spiwack: I use [l] essentially as a natural number *) let rec duplicate acc = function
| [] -> acc
| _::rest -> duplicate (rx::acc) rest in let rec tail to_match rest = match rest, to_match with
| [] , _::_ -> raise (SizeMismatch(0,0)) (* placeholder *)
| _::rest , _::to_match -> tail to_match rest
| _ , [] -> duplicate endxs rest in let rec copy pref rest = match rest,pref with
| [] , _::_ -> raise (SizeMismatch(0,0)) (* placeholder *)
| _::rest, a::pref -> a::(copy pref rest)
| _ , [] -> tail endxs rest in
copy startxs l
(** [tclEXTEND b r e] is a variant of {!tclDISPATCH}, where the [r] tactic is "repeated" enough time such that every goal has a tactic assigned to it ([b] is the list of tactics applied to the first goals, [e] to the last goals, and [r] is applied to every goal in
between). *) let tclEXTEND tacs1 rtac tacs2 = letopen Proof in
Comb.get >>= fun comb -> try let tacs = extend_to_list tacs1 rtac tacs2 comb in
tclDISPATCH tacs with SizeMismatch _ ->
tclZERO (SizeMismatch(
CList.length comb,
(CList.length tacs1)+(CList.length tacs2))) (* spiwack: failure occurs only when the number of goals is too small. Hence we can assume that [rtac] is replicated 0 times for
any error message. *)
(** [tclEXTEND [] tac []]. *) let tclINDEPENDENT tac = letopen Proof in
Pv.get >>= fun initial -> match initial.comb with
| [] -> tclUNIT ()
| [_] -> tac
| _ -> let tac = InfoL.tag (Info.DBranch) tac in
InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac))
let tclINDEPENDENTL tac = letopen Proof in
Pv.get >>= fun initial -> match initial.comb with
| [] -> tclUNIT []
| [_] -> tac >>= fun x -> return [x]
| _ -> let tac = InfoL.tag (Info.DBranch) tac in
InfoL.tag (Info.Dispatch) (map_goal (fun _ -> tac))
(** {7 Goal manipulation} *)
(** Shelves all the goals under focus. *) let shelve = letopen Proof in
Comb.get >>= fun initial ->
Comb.set [] >>
InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >> let initial = CList.map drop_state initial in
Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution initial })
let shelve_goals l = letopen Proof in
Comb.get >>= fun initial -> let comb = CList.filter (fun g -> not (CList.mem (drop_state g) l)) initial in
Comb.set comb >>
InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_goals")) >>
Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution l })
(** [depends_on sigma src tgt] checks whether the goal [src] appears as an existential variable in the definition of the goal [tgt] in
[sigma]. *) let depends_on sigma src tgt = let evi = Evd.find_undefined sigma tgt in
Evar.Set.mem src (Evd.evars_of_filtered_evar_info sigma (Evarutil.nf_evar_info sigma evi))
let unifiable_delayed g l =
CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) l
let free_evars sigma l = let cache = Evarutil.create_undefined_evars_cache () in letmap ev = (* Computes the set of evars appearing in the hypotheses, the conclusion or the body of the evar_info [evi]. Note: since we want to use it on goals,
the body is actually supposed to be empty. *) let EvarInfo evi = Evd.find sigma ev in let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
(ev, fevs) in List.mapmap l
let free_evars_with_state sigma l = let cache = Evarutil.create_undefined_evars_cache () in letmap ev = (* Computes the set of evars appearing in the hypotheses, the conclusion or the body of the evar_info [evi]. Note: since we want to use it on goals,
the body is actually supposed to be empty. *) let ev = drop_state ev in let EvarInfo evi = Evd.find sigma ev in let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
(ev, fevs) in List.mapmap l
(** [unifiable sigma g l] checks whether [g] appears in another subgoal of [l]. The list [l] may contain [g], but it does not
affect the result. *) let unifiable_delayed_with_state sigma g l = let g = drop_state g in
unifiable_delayed g l
let unifiable sigma g l = let l = free_evars sigma l in
unifiable_delayed g l
(** [partition_unifiable sigma l] partitions [l] into a pair [(u,n)] where [u] is composed of the unifiable goals, i.e. the goals on whose definition other goals of [l] depend, and [n] are the
non-unifiable goals. *) let partition_unifiable sigma l = let fevs = free_evars_with_state sigma l in
CList.partition (fun g -> unifiable_delayed_with_state sigma g fevs) l
(** Shelves the unifiable goals under focus, i.e. the goals which appear in other goals under focus (the unfocused goals are not
considered). *) let shelve_unifiable_informative = letopen Proof in
Pv.get >>= fun initial -> let (u,n) = partition_unifiable initial.solution initial.comb in
Comb.set n >>
InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >> let u = CList.map drop_state u in
Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution u }) >>
tclUNIT u
let shelve_unifiable = letopen Proof in
shelve_unifiable_informative >>= fun _ -> tclUNIT ()
(** [guard_no_unifiable] returns the list of unifiable goals if some
goals are unifiable (see {!shelve_unifiable}) in the current focus. *) let guard_no_unifiable = letopen Proof in
Pv.get >>= fun initial -> let (u,n) = partition_unifiable initial.solution initial.comb in match u with
| [] -> tclUNIT None
| gls -> let l = CList.map (fun g -> Evd.dependent_evar_ident (drop_state g) initial.solution) gls in let l = CList.map (fun id -> Names.Name id) l in
tclUNIT (Some l)
(** [unshelve l p] moves all the goals in [l] from the shelf and put them at
the end of the focused goals of p, if they are still undefined after [advance] *) let unshelve l p = let solution = Evd.unshelve p.solution l in let l = List.map with_empty_state l in (* advance the goals in case of clear *) let l = undefined p.solution l in
{ comb = p.comb@l; solution }
let filter_shelf f pv =
{ pv with solution = Evd.filter_shelf f pv.solution }
let mark_in_evm ~goal evd evars = let evd = if goal then let mark evd content = let EvarInfo info = Evd.find evd content in let source = match Evd.evar_source info with (* Two kinds for goal evars: - GoalEvar (morally not dependent) - VarInstance (morally dependent of some name).
This is a heuristic for naming these evars. *)
| loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} |
Evar_kinds.ImplicitArg (_,(_,id),_)) -> loc, Evar_kinds.VarInstance id
| _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
| loc,_ -> loc,Evar_kinds.GoalEvar in
Evd.update_source evd content source in CList.fold_left mark evd evars else evd in let tcs = Evd.get_typeclass_evars evd in let evset = Evar.Set.of_list evars in
Evd.set_typeclass_evars evd (Evar.Set.diff tcs evset)
let with_shelf tac = letopen Proof in
Pv.get >>= fun pv -> let { solution } = pv in
Pv.set { pv with solution = Evd.push_shelf @@ Evd.push_future_goals solution } >>
tac >>= fun ans ->
Pv.get >>= fun npv -> let { solution = sigma } = npv in let gls, sigma = Evd.pop_shelf sigma in (* The pending future goals are necessarily coming from legacy tactics *) (* and thus considered as to shelve, as in Proof.run_tactic *) (* TODO: is it still relevant since the removal of the compat layer? *) let fgl, sigma = Evd.pop_future_goals sigma in (* Ensure we mark and return only unsolved goals *) let gls' = CList.rev_append (Evd.FutureGoals.comb fgl) gls in let gls' = undefined_evars sigma gls'in let sigma = mark_in_evm ~goal:false sigma gls' in let npv = { npv with solution = sigma } in
Pv.set npv >> tclUNIT (gls', ans)
(** [goodmod p m] computes the representative of [p] modulo [m] in the
interval [[0,m-1]].*) let goodmod p m = if m = 0 then 0 else let p' = p mod m in (* if [n] is negative [n mod l] is negative of absolute value less than [l], so [(n mod l)+l] is the representative of [n] in the
interval [[0,l-1]].*) if p' < 0 then p'+m else p'
let cycle n = letopen Proof in
InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle "++int n))) >>
Comb.modify beginfun initial -> let l = CList.length initial in let n' = goodmod n l in let (front,rear) = CList.chop n' initial in
rear@front end
let swap i j = letopen Proof in
InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >>
Comb.modify beginfun initial -> let l = CList.length initial in let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in let i = goodmod i l and j = goodmod j l in
CList.map_i beginfun k x -> match k with
| k when Int.equal k i -> CList.nth initial j
| k when Int.equal k j -> CList.nth initial i
| _ -> x end 0 initial end
let revgoals = letopen Proof in
InfoL.leaf (Info.Tactic (fun () -> Pp.str"revgoals")) >>
Comb.modify CList.rev
let numgoals = letopen Proof in
Comb.get >>= fun comb ->
return (CList.length comb)
(** {7 Access primitives} *)
let tclEVARMAP = Solution.get
let tclENV = Env.get
(** {7 Put-like primitives} *)
let emit_side_effects eff x =
{ x with solution = Evd.emit_side_effects eff x.solution }
let tclEFFECTS eff = letopen Proof in
return () >>= fun () -> (* The Global.env should be taken at exec time *)
Env.set (Global.env ()) >>
Pv.modify (fun initial -> emit_side_effects eff initial)
let mark_as_unsafe = Status.put false
(** Gives up on the goal under focus. Reports an unsafe status. Proofs
with given up goals cannot be closed. *)
let give_up evs pv = let solution = List.fold_left (fun sigma ev -> Evd.give_up (drop_state ev) sigma) pv.solution evs in
{ pv with solution }
let give_up = letopen Proof in
Comb.get >>= fun initial ->
Comb.set [] >>
mark_as_unsafe >>
InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >>
Pv.modify (give_up initial)
(** {7 Control primitives} *)
module Progress = struct
let eq_constr evd extended_evd =
Evarutil.eq_constr_univs_test ~evd ~extended_evd
(** equality function on hypothesis contexts *) let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = let r_eq _ _ = true(* ignore relevances *) in let c1 = EConstr.named_context_of_val ctx1 and c2 = EConstr.named_context_of_val ctx2 in let eq_named_declaration d1 d2 = match d1, d2 with
| LocalAssum (i1,t1), LocalAssum (i2,t2) ->
Context.eq_annot Names.Id.equal r_eq i1 i2 && eq_constr sigma1 sigma2 t1 t2
| LocalDef (i1,c1,t1), LocalDef (i2,c2,t2) ->
Context.eq_annot Names.Id.equal r_eq i1 i2 && eq_constr sigma1 sigma2 c1 c2
&& eq_constr sigma1 sigma2 t1 t2
| _ -> false in (* NB: can't use List.equal because it shortcuts on physical equality *) List.for_all2eq eq_named_declaration c1 c2
(** Equality function on goals *) let goal_equal ~evd ~extended_evd evar extended_evar = let EvarInfo evi = Evd.find evd evar in let EvarInfo extended_evi = Evd.find extended_evd extended_evar in if fast_eq_evar_info evi extended_evi then
eq_evar_info evd extended_evd evi extended_evi elsefalse
end
let tclPROGRESS t = letopen Proof in
Pv.get >>= fun initial ->
t >>= fun res ->
Pv.get >>= fun final -> (* [*_test] test absence of progress. [quick_test] is approximate
whereas [exhaustive_test] is complete. *) let quick_test =
initial.solution == final.solution && initial.comb == final.comb in lettest =
quick_test ||
(CList.same_length initial.comb final.comb &&
Util.List.for_all2eq beginfun i f ->
Progress.goal_equal ~evd:initial.solution
~extended_evd:final.solution (drop_state i) (drop_state f) end initial.comb final.comb) in ifnottestthen
tclUNIT res else let info = Exninfo.reify () in
tclZERO ~info (CErrors.UserError Pp.(str "Failed to progress."))
let _ = CErrors.register_handler begin function
| Logic_monad.Tac_Timeout ->
Some (Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!")
| _ -> None end
let tclTIMEOUTF n t = letopen Proof in (* spiwack: as one of the monad is a continuation passing monad, it doesn't force the computation to be threaded inside the underlying (IO) monad. Hence I force it myself by asking for the evaluation of a dummy value first, lest [timeout] be called when everything has
already been computed. *) let t = Proof.lift (Logic_monad.NonLogical.return ()) >> t in
Proof.get >>= fun initial ->
Proof.current >>= fun envvar ->
Proof.lift begin letopen Logic_monad.NonLogical in
timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r -> match r with
| None -> return (Util.Inr (Logic_monad.Tac_Timeout, Exninfo.null))
| Some (Logic_monad.Nil e) -> return (Util.Inr e)
| Some (Logic_monad.Cons (r, _)) -> return (Util.Inl r) end >>= function
| Util.Inl (res,s,m,i) ->
Proof.set s >>
Proof.put m >>
Proof.update (fun _ -> i) >>
return res
| Util.Inr (e, info) -> tclZERO ~info e
let tclTIMEOUT n t = tclTIMEOUTF (float_of_int n) t
let tclTIME s t = let pr_time t1 t2 n msg = let msg = if n = 0 then
str msg else
str (msg ^ " after ") ++ int n ++ str (String.plural n " backtracking") in
Feedback.msg_info(str "Tactic call" ++ pr_opt str s ++ str " ran for " ++
System.fmt_time_difference t1 t2 ++ str " " ++ surround msg) in let rec aux n t = letopen Proof in
tclUNIT () >>= fun () -> let tstart = System.get_time() in
Proof.split t >>= letopen Logic_monad in function
| Nil (e, info) -> begin let tend = System.get_time() in
pr_time tstart tend n "failure";
tclZERO ~info e end
| Cons (x,k) -> let tend = System.get_time() in
pr_time tstart tend n "success";
tclOR (tclUNIT x) (fun e -> aux (n+1) (k e)) in aux 0 t
let tclProofInfo = letopen Proof in
Logical.current >>= fun P.{name; poly} ->
tclUNIT (name, poly)
(** {7 Unsafe primitives} *)
module Unsafe = struct
let (>>=) = tclBIND
let tclEVARS evd =
Pv.modify (fun ps -> { ps with solution = evd })
let tclNEWGOALS ?(before = false) gls =
Pv.modify beginfun step -> let gls = undefined step.solution gls in let comb = if before then gls @ step.comb else step.comb @ gls in
{ step with comb } end
let tclNEWSHELVED gls =
Pv.modify beginfun step -> let gls = undefined_evars step.solution gls in
{ step with solution = Evd.shelve step.solution gls } end
let tclGETSHELF = tclEVARMAP >>= fun sigma -> tclUNIT @@ Evd.shelf sigma
let tclEVARUNIVCONTEXT ctx =
Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
let push_future_goals p =
{ p with solution = Evd.push_future_goals p.solution }
let mark_as_goals evd content =
mark_in_evm ~goal:true evd content
let advance = Evarutil.advance
let undefined = undefined
let mark_unresolvables evm evs =
mark_in_evm ~goal:false evm evs
let mark_as_unresolvables p evs =
{ p with solution = mark_in_evm ~goal:false p.solution evs }
let update_sigma_univs ugraph pv =
{ pv with solution = Evd.update_sigma_univs ugraph pv.solution }
end
module UnsafeRepr = Proof.Unsafe
let (>>=) = tclBIND
(** {6 Goal-dependent tactics} *)
let catchable_exception = function
| Logic_monad.Exception _ -> false
| e -> CErrors.noncritical e
module Goal = struct
type t = {
env : Environ.env;
sigma : Evd.evar_map;
concl : EConstr.constr ;
state : StateStore.t;
self : Evar.t ; (* for compatibility with old-style definitions *)
}
let state { state=state } = state
let env {env} = env let sigma {sigma} = sigma let hyps {env} = EConstr.named_context env let concl {concl} = concl let relevance {sigma; self} =
Evd.evar_relevance (Evd.find_undefined sigma self)
let gmake_with info env sigma goal state =
{ env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
sigma = sigma ;
concl = Evd.evar_concl info;
state = state ;
self = goal }
let gmake env sigma goal = let state = get_state goal in let goal = drop_state goal in let info = Evd.find_undefined sigma goal in
gmake_with info env sigma goal state
let enter f = let f gl = InfoL.tag (Info.DBranch) (f gl) in
InfoL.tag (Info.Dispatch) begin
iter_goal beginfun goal ->
Env.get >>= fun env ->
tclEVARMAP >>= fun sigma -> try f (gmake env sigma goal) with e when catchable_exception e -> let (e, info) = Exninfo.capture e in
tclZERO ~info e end end
let enter_one ?(__LOC__=__LOC__) f = letopen Proof in
Comb.get >>= function
| [goal] -> begin
Env.get >>= fun env ->
tclEVARMAP >>= fun sigma -> try f (gmake env sigma goal) with e when catchable_exception e -> let (e, info) = Exninfo.capture e in
tclZERO ~info e end
| _ ->
CErrors.anomaly Pp.(str __LOC__ ++ str " enter_one")
let goals =
Pv.get >>= fun step -> let sigma = step.solution in letmap goal = match cleared_alias sigma goal with
| None -> None (* ppedrot: Is this check really necessary? *)
| Some goal -> let oinfo = Evd.find_undefined sigma (drop_state goal) in let gl =
Env.get >>= fun env ->
tclEVARMAP >>= fun sigma -> let state = get_state goal in let goal = drop_state goal in let EvarInfo info = Evd.find sigma goal in let goal = {
env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
sigma = sigma ;
concl = Evd.evar_concl oinfo;
state = state;
self = goal;
} in
tclUNIT goal in
Some gl in
tclUNIT (CList.map_filter map step.comb)
let unsolved { self=self } =
tclEVARMAP >>= fun sigma ->
tclUNIT (not (Option.is_empty (Evarutil.advance sigma self)))
(* compatibility *) let goal { self=self } = self
end
(** {6 Trace} *)
module Trace = struct
let record_info_trace = InfoL.record_trace
let log m = InfoL.leaf (Info.Msg m) let name_tactic m t = InfoL.tag (Info.Tactic m) t
let pr_info env sigma ?(lvl=0) info =
assert (lvl >= 0);
Info.(print env sigma (collapse lvl info))
end
(** {6 Non-logical state} *)
module NonLogical = Logic_monad.NonLogical
let tclLIFT = Proof.lift
let tclCHECKINTERRUPT =
tclLIFT (NonLogical.make Control.check_for_interrupt)
let wrap_exceptions f = try f () with e when catchable_exception e -> let (e, info) = Exninfo.capture e in tclZERO ~info e
(** {7 Notations} *)
module Notations = struct let (>>=) = tclBIND let (<*>) = tclTHEN let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) end
¤ Dauer der Verarbeitung: 0.48 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
