diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 19:38:36 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 19:48:38 +0100 |
commit | ea4e09c26747fa9c49882580a72139fe748a0d64 (patch) | |
tree | 40364a6bb2100e102bc16e465b6d6289b1340314 /proofs | |
parent | 93a77f3cb8ee36072f93b4c0ace6f0f9c19f51a3 (diff) |
Moving Proofview to pretyping/.
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/proofs.mllib | 1 | ||||
-rw-r--r-- | proofs/proofview.ml | 1204 | ||||
-rw-r--r-- | proofs/proofview.mli | 586 |
3 files changed, 0 insertions, 1791 deletions
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 236d47932..9130a186b 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -4,7 +4,6 @@ Evar_refiner Proof_using Proof_errors Logic -Proofview Refine Proof Proof_global diff --git a/proofs/proofview.ml b/proofs/proofview.ml deleted file mode 100644 index 20be02e76..000000000 --- a/proofs/proofview.ml +++ /dev/null @@ -1,1204 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - - -(** 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 Sigma.Notations -open Context.Named.Declaration - -(** Main state of tactics *) -type proofview = Proofview_monad.proofview - -type entry = (Term.constr * Term.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 everytime. Hence the generic name. *) -(* In this version: returns the list of focused goals together with - the [evar_map] context. *) -let proofview p = - p.comb , p.solution - -let compact el ({ solution } as pv) = - let nf = Evarutil.nf_evar solution in - let size = Evd.fold (fun _ _ i -> i+1) solution 0 in - let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in - let pruned_solution = Evd.drop_all_defined solution in - let apply_subst_einfo _ ei = - Evd.({ ei with - evar_concl = nf ei.evar_concl; - evar_hyps = Environ.map_named_val nf ei.evar_hyps; - evar_candidates = Option.map (List.map nf) ei.evar_candidates }) 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 - 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 * Term.types * (Evd.evar_map -> Term.constr -> telescope) - -let dependent_init = - (* Goals are created with a store which marks them as unresolvable - for type classes. *) - let store = Typeclasses.set_resolvable Evd.Store.empty false in - (* Goals don't have a source location. *) - let src = (Loc.ghost,Evar_kinds.GoalEvar) in - (* Main routine *) - let rec aux = function - | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } - | TCons (env, sigma, typ, t) -> - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in - let sigma = Sigma.to_evar_map sigma in - let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in - let (gl, _) = Term.destEvar econstr in - let entry = (econstr, typ) :: ret in - entry, { solution = sol; comb = gl :: comb; shelf = [] } - in - fun t -> - let entry, v = aux t in - (* The created goal are not to be shelved. *) - let solution = Evd.reset_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 partial_proof entry pv = CList.map (return_constr pv) (CList.map fst entry) - - -(** {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 = Evar.t list * Evar.t 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 everytime. 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 f = f - -(** 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 lenght [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, context) = focus_sublist i j sp.comb in - ( { sp with comb = new_comb } , context ) - - -(** [advance sigma g] returns [Some g'] if [g'] is undefined and is - the current avatar of [g] (for instance [g] was changed by [clear] - into [g']). It returns [None] if [g] has been (partially) - solved. *) -(* spiwack: [advance] is probably performance critical, and the good - behaviour of its definition may depend sensitively to the actual - definition of [Evd.find]. Currently, [Evd.find] starts looking for - a value in the heap of undefined variable, which is small. Hence in - the most common case, where [advance] is applied to an unsolved - goal ([advance] is used to figure if a side effect has modified the - goal) it terminates quickly. *) -let rec advance sigma g = - let open Evd in - let evi = Evd.find sigma g in - match evi.evar_body with - | Evar_empty -> Some g - | Evar_defined v -> - if Option.default false (Store.get evi.evar_extra Evarutil.cleared) then - let (e,_) = Term.destEvar v in - advance sigma e - else - None - -(** [undefined defs l] is the list of goals in [l] which are still - unsolved (after advancing cleared goals). *) -let undefined defs l = CList.map_filter (advance defs) l - -(** Unfocuses a proofview with respect to a context. *) -let unfocus c sp = - { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) } - - -(** {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 Coq'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 env t sp = - let open Logic_monad in - let ans = Proof.repr (Proof.run t false (sp,env)) in - let ans = Logic_monad.NonLogical.run ans in - match ans with - | Nil (e, info) -> iraise (TacticFailure e, info) - | Cons ((r, (state, _), status, info), _) -> - let (status, gaveup) = status in - let status = (status, state.shelf, gaveup) in - let state = { state with shelf = [] } in - r, state, 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.(>>=) - -(** Interpretes 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 e = - let info = match info with - | None -> Exninfo.null - | Some info -> info - in - 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 = - let open Logic_monad in - let open 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 = - let open Logic_monad in - let open 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 _ = Errors.register_handler begin function - | MoreThanOneSuccess -> Errors.error "This tactic has more than one success." - | _ -> raise Errors.Unhandled -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 = - let open Logic_monad in - let open Proof in - split t >>= function - | Nil (e, info) -> tclZERO ~info e - | Cons (x,k) -> - Proof.split (k (e, Exninfo.null)) >>= function - | Nil _ -> tclUNIT x - | _ -> tclZERO MoreThanOneSuccess - - -(** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *) -type 'a case = -| Fail of iexn -| Next of 'a * (iexn -> 'a tactic) -let tclCASE t = - let open Logic_monad in - let map = function - | Nil e -> Fail e - | Cons (x, t) -> Next (x, t) - in - Proof.map map (Proof.split t) - -let tclBREAK = Proof.break - - - -(** {7 Focusing tactics} *) - -exception NoSuchGoals of int - -(* This hook returns a string to be appended to the usual message. - Primarily used to add a suggestion about the right bullet to use to - focus the next goal, if applicable. *) -let nosuchgoals_hook:(int -> std_ppcmds) ref = ref (fun n -> mt ()) -let set_nosuchgoals_hook f = nosuchgoals_hook := f - - - -(* This uses the hook above *) -let _ = Errors.register_handler begin function - | NoSuchGoals n -> - let suffix = !nosuchgoals_hook n in - Errors.errorlabstrm "" - (str "No such " ++ str (String.plural n "goal") ++ str "." ++ suffix) - | _ -> raise Errors.Unhandled -end - -(** [tclFOCUS_gen 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_gen nosuchgoal i j t = - let open 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 -> nosuchgoal - -let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t -let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t - -(** Like {!tclFOCUS} but selects a single goal by name. *) -let tclFOCUSID id t = - let open Proof in - Pv.get >>= fun initial -> - try - let ev = Evd.evar_key id initial.solution in - try - let n = CList.index Evar.equal ev initial.comb in - (* goal is already under focus *) - let (focused,context) = focus n n initial in - Pv.set focused >> - t >>= fun result -> - Pv.modify (fun next -> unfocus context next) >> - return result - with Not_found -> - (* otherwise, save current focus and work purely on the shelve *) - Comb.set [ev] >> - t >>= fun result -> - Comb.set initial.comb >> - return result - with Not_found -> tclZERO (NoSuchGoals 1) - -(** {7 Dispatching on goals} *) - -exception SizeMismatch of int*int -let _ = Errors.register_handler begin function - | SizeMismatch (i,_) -> - let open Pp in - let errmsg = - str"Incorrect number of goals" ++ spc() ++ - str"(expected "++int i++str(String.plural i " tactic") ++ str")." - in - Errors.errorlabstrm "" errmsg - | _ -> raise Errors.Unhandled -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 = - let open Proof in - Comb.get >>= fun initial -> - Proof.List.fold_left begin fun (subgoals as cur) goal -> - Solution.get >>= fun step -> - match advance 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))) - -(** 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 = - let open 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 begin fun ((r,subgoals) as cur) goal a -> - Solution.get >>= fun step -> - match advance 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 - let open Proof in - Comb.get >>= function - | [] -> tclUNIT (join []) - | comb -> tclZERO (SizeMismatch (CList.length comb,0)) - end - | [tac] -> - begin - let open Proof in - Pv.get >>= function - | { comb=[goal] ; solution } -> - begin match advance 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 Pervasives.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 = - let open 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 = - let open 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)) - - - -(** {7 Goal manipulation} *) - -(** Shelves all the goals under focus. *) -let shelve = - let open Proof in - Comb.get >>= fun initial -> - Comb.set [] >> - InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >> - Shelf.modify (fun gls -> gls @ initial) - - -(** [contained_in_info e evi] checks whether the evar [e] appears 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 contained_in_info sigma e evi = - Evar.Set.mem e (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi)) - -(** [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 sigma tgt in - contained_in_info sigma src evi - -(** [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 sigma g l = - CList.exists (fun tgt -> not (Evar.equal g tgt) && depends_on sigma g tgt) 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 = - CList.partition (fun g -> unifiable sigma g l) 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 = - let open 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")) >> - Shelf.modify (fun gls -> gls @ u) - -(** [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 = - let open 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 g initial.solution) gls in - let l = CList.map (fun id -> Names.Name id) l in - tclUNIT (Some l) - -(** [unshelve l p] adds all the goals in [l] at the end of the focused - goals of p *) -let unshelve l p = - (* advance the goals in case of clear *) - let l = undefined p.solution l in - { p with comb = p.comb@l } - -let with_shelf tac = - let open Proof in - Pv.get >>= fun pv -> - let { shelf; solution } = pv in - Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >> - tac >>= fun ans -> - Pv.get >>= fun npv -> - let { shelf = gls; solution = sigma } = npv in - let gls' = Evd.future_goals sigma in - let fgoals = Evd.future_goals solution in - let pgoal = Evd.principal_future_goal solution in - let sigma = Evd.restore_future_goals sigma fgoals pgoal in - Pv.set { npv with shelf; solution = sigma } >> - tclUNIT (CList.rev_append gls' gls, ans) - -(** [goodmod p m] computes the representative of [p] modulo [m] in the - interval [[0,m-1]].*) -let goodmod p m = - 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 = - let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle "++int n))) >> - Comb.modify begin fun 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 = - let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >> - Comb.modify begin fun 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 begin fun 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 = - let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.str"revgoals")) >> - Comb.modify CList.rev - -let numgoals = - let open 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 = - let open 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 = - let open Proof in - Comb.get >>= fun initial -> - Comb.set [] >> - mark_as_unsafe >> - InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >> - Giveup.put initial - - - -(** {7 Control primitives} *) - - -module Progress = struct - - let eq_constr = Evarutil.eq_constr_univs_test - - (** equality function on hypothesis contexts *) - let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = - let open Environ in - let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in - let eq_named_declaration d1 d2 = - match d1, d2 with - | LocalAssum (i1,t1), LocalAssum (i2,t2) -> - Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 t1 t2 - | LocalDef (i1,c1,t1), LocalDef (i2,c2,t2) -> - Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 c1 c2 - && eq_constr sigma1 sigma2 t1 t2 - | _ -> - false - in List.equal eq_named_declaration c1 c2 - - let eq_evar_body sigma1 sigma2 b1 b2 = - let open Evd in - match b1, b2 with - | Evar_empty, Evar_empty -> true - | Evar_defined t1, Evar_defined t2 -> eq_constr sigma1 sigma2 t1 t2 - | _ -> false - - let eq_evar_info sigma1 sigma2 ei1 ei2 = - let open Evd in - eq_constr sigma1 sigma2 ei1.evar_concl ei2.evar_concl && - eq_named_context_val sigma1 sigma2 (ei1.evar_hyps) (ei2.evar_hyps) && - eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body - - (** Equality function on goals *) - let goal_equal evars1 gl1 evars2 gl2 = - let evi1 = Evd.find evars1 gl1 in - let evi2 = Evd.find evars2 gl2 in - eq_evar_info evars1 evars2 evi1 evi2 - -end - -let tclPROGRESS t = - let open 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 - let exhaustive_test = - Util.List.for_all2eq begin fun i f -> - Progress.goal_equal initial.solution i final.solution f - end initial.comb final.comb - in - let test = - quick_test || exhaustive_test - in - if not test then - tclUNIT res - else - tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) - -exception Timeout -let _ = Errors.register_handler begin function - | Timeout -> Errors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") - | _ -> Pervasives.raise Errors.Unhandled -end - -let tclTIMEOUT n t = - let open 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 - Logic_monad.NonLogical.catch - begin - let open Logic_monad.NonLogical in - timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r -> - match r with - | Logic_monad.Nil e -> return (Util.Inr e) - | Logic_monad.Cons (r, _) -> return (Util.Inl r) - end - begin let open Logic_monad.NonLogical in function (e, info) -> - match e with - | Logic_monad.Timeout -> return (Util.Inr (Timeout, info)) - | Logic_monad.TacticFailure e -> - return (Util.Inr (e, info)) - | e -> Logic_monad.NonLogical.raise ~info e - end - 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 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 - 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 = - let open Proof in - tclUNIT () >>= fun () -> - let tstart = System.get_time() in - Proof.split t >>= let open 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 - - - -(** {7 Unsafe primitives} *) - -module Unsafe = struct - - let tclEVARS evd = - Pv.modify (fun ps -> { ps with solution = evd }) - - let tclNEWGOALS gls = - Pv.modify begin fun step -> - let gls = undefined step.solution gls in - { step with comb = step.comb @ gls } - end - - let tclGETGOALS = Comb.get - - let tclSETGOALS = Comb.set - - let tclEVARSADVANCE evd = - Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb }) - - let tclEVARUNIVCONTEXT ctx = - Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) - - let reset_future_goals p = - { p with solution = Evd.reset_future_goals p.solution } - - let mark_as_goal evd content = - let info = Evd.find evd content in - let info = - { info with Evd.evar_source = match info.Evd.evar_source with - | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x - | loc,_ -> loc,Evar_kinds.GoalEvar } - in - let info = Typeclasses.mark_unresolvable info in - Evd.add evd content info - - let advance = advance - -end - -module UnsafeRepr = Proof.Unsafe - -let (>>=) = tclBIND -let (<*>) = tclTHEN -let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) - -(** {6 Goal-dependent tactics} *) - -let goal_env evars gl = - let evi = Evd.find evars gl in - Evd.evar_filtered_env evi - -let goal_nf_evar sigma gl = - let evi = Evd.find sigma gl in - let evi = Evarutil.nf_evar_info sigma evi in - let sigma = Evd.add sigma gl evi in - (gl, sigma) - -let goal_extra evars gl = - let evi = Evd.find evars gl in - evi.Evd.evar_extra - - -let catchable_exception = function - | Logic_monad.Exception _ -> false - | e -> Errors.noncritical e - - -module Goal = struct - - type ('a, 'r) t = { - env : Environ.env; - sigma : Evd.evar_map; - concl : Term.constr ; - self : Evar.t ; (* for compatibility with old-style definitions *) - } - - type ('a, 'b) enter = - { enter : 'r. ('a, 'r) t -> 'b } - - let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t) - - let env { env=env } = env - let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma - let hyps { env=env } = Environ.named_context env - let concl { concl=concl } = concl - let extra { sigma=sigma; self=self } = goal_extra sigma self - - let raw_concl { concl=concl } = concl - - - let gmake_with info env sigma goal = - { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; - sigma = sigma ; - concl = Evd.evar_concl info ; - self = goal } - - let nf_gmake env sigma goal = - let info = Evarutil.nf_evar_info sigma (Evd.find sigma goal) in - let sigma = Evd.add sigma goal info in - gmake_with info env sigma goal , sigma - - let nf_enter f = - InfoL.tag (Info.Dispatch) begin - iter_goal begin fun goal -> - Env.get >>= fun env -> - tclEVARMAP >>= fun sigma -> - try - let (gl, sigma) = nf_gmake env sigma goal in - tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f.enter gl)) - with e when catchable_exception e -> - let (e, info) = Errors.push e in - tclZERO ~info e - end - end - - let normalize { self } = - Env.get >>= fun env -> - tclEVARMAP >>= fun sigma -> - let (gl,sigma) = nf_gmake env sigma self in - tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl) - - let gmake env sigma goal = - let info = Evd.find sigma goal in - gmake_with info env sigma goal - - let enter f = - let f gl = InfoL.tag (Info.DBranch) (f.enter gl) in - InfoL.tag (Info.Dispatch) begin - iter_goal begin fun goal -> - Env.get >>= fun env -> - tclEVARMAP >>= fun sigma -> - try f (gmake env sigma goal) - with e when catchable_exception e -> - let (e, info) = Errors.push e in - tclZERO ~info e - end - end - - type ('a, 'b) s_enter = - { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } - - let s_enter f = - InfoL.tag (Info.Dispatch) begin - iter_goal begin fun goal -> - Env.get >>= fun env -> - tclEVARMAP >>= fun sigma -> - try - let gl = gmake env sigma goal in - let Sigma (tac, sigma, _) = f.s_enter gl in - let sigma = Sigma.to_evar_map sigma in - tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) - with e when catchable_exception e -> - let (e, info) = Errors.push e in - tclZERO ~info e - end - end - - let nf_s_enter f = - InfoL.tag (Info.Dispatch) begin - iter_goal begin fun goal -> - Env.get >>= fun env -> - tclEVARMAP >>= fun sigma -> - try - let (gl, sigma) = nf_gmake env sigma goal in - let Sigma (tac, sigma, _) = f.s_enter gl in - let sigma = Sigma.to_evar_map sigma in - tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) - with e when catchable_exception e -> - let (e, info) = Errors.push e in - tclZERO ~info e - end - end - - let goals = - Pv.get >>= fun step -> - let sigma = step.solution in - let map goal = - match advance sigma goal with - | None -> None (** ppedrot: Is this check really necessary? *) - | Some goal -> - let gl = - Env.get >>= fun env -> - tclEVARMAP >>= fun sigma -> - tclUNIT (gmake env sigma goal) - in - Some gl - in - tclUNIT (CList.map_filter map step.comb) - - (* compatibility *) - let goal { self=self } = self - - let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t) - -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 ?(lvl=0) info = - assert (lvl >= 0); - Info.(print (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) - - - - - -(*** Compatibility layer with <= 8.2 tactics ***) -module V82 = struct - type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - - let tactic tac = - (* spiwack: we ignore the dependencies between goals here, - expectingly preserving the semantics of <= 8.2 tactics *) - (* spiwack: convenience notations, waiting for ocaml 3.12 *) - let open Proof in - Pv.get >>= fun ps -> - try - let tac gl evd = - let glsigma = - tac { Evd.it = gl ; sigma = evd; } in - let sigma = glsigma.Evd.sigma in - let g = glsigma.Evd.it in - ( g, sigma ) - in - (* Old style tactics expect the goals normalized with respect to evars. *) - let (initgoals,initevd) = - Evd.Monad.List.map (fun g s -> goal_nf_evar s g) ps.comb ps.solution - in - let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in - let sgs = CList.flatten goalss in - let sgs = undefined evd sgs in - InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >> - Pv.set { ps with solution = evd; comb = sgs; } - with e when catchable_exception e -> - let (e, info) = Errors.push e in - tclZERO ~info e - - - (* normalises the evars in the goals, and stores the result in - solution. *) - let nf_evar_goals = - Pv.modify begin fun ps -> - let map g s = goal_nf_evar s g in - let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in - { ps with solution = evd; comb = goals; } - end - - let has_unresolved_evar pv = - Evd.has_undefined pv.solution - - (* Main function in the implementation of Grab Existential Variables.*) - let grab pv = - let undef = Evd.undefined_map pv.solution in - let goals = CList.rev_map fst (Evar.Map.bindings undef) in - { pv with comb = goals } - - - - (* Returns the open goals of the proofview together with the evar_map to - interpret them. *) - let goals { comb = comb ; solution = solution; } = - { Evd.it = comb ; sigma = solution } - - let top_goals initial { solution=solution; } = - let goals = CList.map (fun (t,_) -> fst (Term.destEvar t)) initial in - { Evd.it = goals ; sigma=solution; } - - let top_evars initial = - let evars_of_initial (c,_) = - Evar.Set.elements (Evd.evars_of_term c) - in - CList.flatten (CList.map evars_of_initial initial) - - let of_tactic t gls = - try - let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in - let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in - { Evd.sigma = final.solution ; it = final.comb } - with Logic_monad.TacticFailure e as src -> - let (_, info) = Errors.push src in - iraise (e, info) - - let put_status = Status.put - - let catchable_exception = catchable_exception - - let wrap_exceptions f = - try f () - with e when catchable_exception e -> - let (e, info) = Errors.push e in tclZERO ~info e - -end - -(** {7 Notations} *) - -module Notations = struct - let (>>=) = tclBIND - let (<*>) = tclTHEN - let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) - type ('a, 'b) enter = ('a, 'b) Goal.enter = - { enter : 'r. ('a, 'r) Goal.t -> 'b } - type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter = - { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma } -end diff --git a/proofs/proofview.mli b/proofs/proofview.mli deleted file mode 100644 index 6bc2e9a0e..000000000 --- a/proofs/proofview.mli +++ /dev/null @@ -1,586 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** 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 Util -open Term - -(** Main state of tactics *) -type proofview - -(** 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 everytime. Hence the generic name. *) -(* In this version: returns the list of focused goals together with - the [evar_map] context. *) -val proofview : proofview -> Goal.goal list * Evd.evar_map - - -(** {6 Starting and querying a proof view} *) - -(** Abstract representation of the initial goals of a proof. *) -type entry - -(** Optimize memory consumption *) -val compact : entry -> proofview -> entry * proofview - -(** Initialises a proofview, the main argument is a list of - environments (including a [named_context] which are used as - hypotheses) pair with conclusion types, creating accordingly many - initial goals. Because a proof does not necessarily starts in an - empty [evar_map] (indeed a proof can be triggered by an incomplete - pretyping), [init] takes an additional argument to represent the - initial [evar_map]. *) -val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview - -(** A [telescope] is a list of environment and conclusion like in - {!init}, except that each element may depend on the previous - goals. The telescope passes the goals in the form of a - [Term.constr] which represents the goal as an [evar]. The - [evar_map] is threaded in state passing style. *) -type telescope = - | TNil of Evd.evar_map - | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope) - -(** Like {!init}, but goals are allowed to be dependent on one - another. Dependencies between goals is represented with the type - [telescope] instead of [list]. Note that the first [evar_map] of - the telescope plays the role of the [evar_map] argument in - [init]. *) -val dependent_init : telescope -> entry * proofview - -(** [finished pv] is [true] if and only if [pv] is complete. That is, - if it has an empty list of focused goals. There could still be - unsolved subgoaled, but they would then be out of focus. *) -val finished : proofview -> bool - -(** Returns the current [evar] state. *) -val return : proofview -> Evd.evar_map - -val partial_proof : entry -> proofview -> constr list -val initial_goals : entry -> (constr * types) list - - - -(** {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. *) -type focus_context - -(** 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 everytime. Hence the generic name. *) -(* In this version: the goals in the context, as a "zipper" (the first - list is in reversed order). *) -val focus_context : focus_context -> Goal.goal list * Goal.goal list - -(** [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. *) -val focus : int -> int -> proofview -> proofview * focus_context - -(** Unfocuses a proofview with respect to a context. *) -val unfocus : focus_context -> proofview -> proofview - - -(** {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 Coq'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. -*) - - -(** The abstract type of tactics *) -type +'a tactic - -(** Applies a tactic to the current proofview. Returns a tuple - [a,pv,(b,sh,gu)] where [a] is the return value of the tactic, [pv] - is the updated proofview, [b] a boolean which is [true] if the - tactic has not done any action considered unsafe (such as - admitting a lemma), [sh] is the list of goals which have been - shelved by the tactic, and [gu] the list of goals on which the - tactic has given up. In case of multiple success the first one is - selected. If there is no success, fails with - {!Logic_monad.TacticFailure}*) -val apply : Environ.env -> 'a tactic -> proofview -> 'a - * proofview - * (bool*Goal.goal list*Goal.goal list) - * Proofview_monad.Info.tree - -(** {7 Monadic primitives} *) - -(** Unit of the tactic monad. *) -val tclUNIT : 'a -> 'a tactic - -(** Bind operation of the tactic monad. *) -val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic - -(** Interprets the ";" (semicolon) of Ltac. As a monadic operation, - it's a specialized "bind". *) -val tclTHEN : unit tactic -> 'a tactic -> 'a tactic - -(** [tclIGNORE t] has the same operational content as [t], but drops - the returned value. *) -val tclIGNORE : 'a tactic -> unit tactic - -(** Generic monadic combinators for tactics. *) -module Monad : Monad.S with type +'a t = 'a tactic - -(** {7 Failure and backtracking} *) - -(** [tclZERO e] fails with exception [e]. It has no success. *) -val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic - -(** [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. *) -val tclOR : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic - -(** [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. *) -val tclORELSE : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic - -(** [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]. *) -val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (iexn -> 'b tactic) -> 'b tactic - -(** [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]. *) -val tclONCE : 'a tactic -> 'a tactic - -(** [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}). *) -exception MoreThanOneSuccess -val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic - -(** [tclCASE t] splits [t] into its first success and a - continuation. It is the most general primitive to control - backtracking. *) -type 'a case = - | Fail of iexn - | Next of 'a * (iexn -> 'a tactic) -val tclCASE : 'a tactic -> 'a case tactic - -(** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of - stopping after the first success, it succeeds like [t] until a - failure with an exception [e] such that [p e = Some e'] is raised. At - which point it drops the remaining successes, failing with [e']. - [tclONCE t] is equivalent to [tclBREAK (fun e -> Some e) t]. *) -val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic - - -(** {7 Focusing tactics} *) - -(** [tclFOCUS i j t] applies [t] after focusing on the goals number - [i] to [j] (see {!focus}). The rest of the goals is restored after - the tactic action. If the specified range doesn't correspond to - existing goals, fails with [NoSuchGoals] (a user error). this - exception is caught at toplevel with a default message + a hook - message that can be customized by [set_nosuchgoals_hook] below. - This hook is used to add a suggestion about bullets when - applicable. *) -exception NoSuchGoals of int -val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit - -val tclFOCUS : int -> int -> 'a tactic -> 'a tactic - -(** [tclFOCUSID x t] applies [t] on a (single) focused goal like - {!tclFOCUS}. The goal is found by its name rather than its - number.*) -val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic - -(** [tclTRYFOCUS i j t] behaves like {!tclFOCUS}, except that if the - specified range doesn't correspond to existing goals, behaves like - [tclUNIT ()] instead of failing. *) -val tclTRYFOCUS : int -> int -> unit tactic -> unit tactic - - -(** {7 Dispatching on goals} *) - -(** 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. *) -exception SizeMismatch of int*int -val tclDISPATCH : unit tactic list -> unit tactic -val tclDISPATCHL : 'a tactic list -> 'a list tactic - -(** [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). *) -val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic - -(** [tclINDEPENDENT tac] runs [tac] on each goal successively, from - the first one to the last one. Backtracking in one goal is - independent of backtracking in another. It is equivalent to - [tclEXTEND [] tac []]. *) -val tclINDEPENDENT : unit tactic -> unit tactic - - -(** {7 Goal manipulation} *) - -(** Shelves all the goals under focus. The goals are placed on the - shelf for later use (or being solved by side-effects). *) -val shelve : unit tactic - -(** Shelves the unifiable goals under focus, i.e. the goals which - appear in other goals under focus (the unfocused goals are not - considered). *) -val shelve_unifiable : unit tactic - -(** [guard_no_unifiable] returns the list of unifiable goals if some - goals are unifiable (see {!shelve_unifiable}) in the current focus. *) -val guard_no_unifiable : Names.Name.t list option tactic - -(** [unshelve l p] adds all the goals in [l] at the end of the focused - goals of p *) -val unshelve : Goal.goal list -> proofview -> proofview - -(** [with_shelf tac] executes [tac] and returns its result together with the set - of goals shelved by [tac]. The current shelf is unchanged. *) -val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic - -(** If [n] is positive, [cycle n] puts the [n] first goal last. If [n] - is negative, then it puts the [n] last goals first.*) -val cycle : int -> unit tactic - -(** [swap i j] swaps the position of goals number [i] and [j] - (negative numbers can be used to address goals from the end. Goals - are indexed from [1]. For simplicity index [0] corresponds to goal - [1] as well, rather than raising an error. *) -val swap : int -> int -> unit tactic - -(** [revgoals] reverses the list of focused goals. *) -val revgoals : unit tactic - -(** [numgoals] returns the number of goals under focus. *) -val numgoals : int tactic - - -(** {7 Access primitives} *) - -(** [tclEVARMAP] doesn't affect the proof, it returns the current - [evar_map]. *) -val tclEVARMAP : Evd.evar_map tactic - -(** [tclENV] doesn't affect the proof, it returns the current - environment. It is not the environment of a particular goal, - rather the "global" environment of the proof. The goal-wise - environment is obtained via {!Proofview.Goal.env}. *) -val tclENV : Environ.env tactic - - -(** {7 Put-like primitives} *) - -(** [tclEFFECTS eff] add the effects [eff] to the current state. *) -val tclEFFECTS : Safe_typing.private_constants -> unit tactic - -(** [mark_as_unsafe] declares the current tactic is unsafe. *) -val mark_as_unsafe : unit tactic - -(** Gives up on the goal under focus. Reports an unsafe status. Proofs - with given up goals cannot be closed. *) -val give_up : unit tactic - - -(** {7 Control primitives} *) - -(** [tclPROGRESS t] checks the state of the proof after [t]. It it is - identical to the state before, then [tclePROGRESS t] fails, otherwise - it succeeds like [t]. *) -val tclPROGRESS : 'a tactic -> 'a tactic - -(** Checks for interrupts *) -val tclCHECKINTERRUPT : unit tactic - -exception Timeout -(** [tclTIMEOUT n t] can have only one success. - In case of timeout if fails with [tclZERO Timeout]. *) -val tclTIMEOUT : int -> 'a tactic -> 'a tactic - -(** [tclTIME s t] displays time for each atomic call to t, using s as an - identifying annotation if present *) -val tclTIME : string option -> 'a tactic -> 'a tactic - -(** {7 Unsafe primitives} *) - -(** The primitives in the [Unsafe] module should be avoided as much as - possible, since they can make the proof state inconsistent. They are - nevertheless helpful, in particular when interfacing the pretyping and - the proof engine. *) -module Unsafe : sig - - (** [tclEVARS sigma] replaces the current [evar_map] by [sigma]. If - [sigma] has new unresolved [evar]-s they will not appear as - goal. If goals have been solved in [sigma] they will still - appear as unsolved goals. *) - val tclEVARS : Evd.evar_map -> unit tactic - - (** Like {!tclEVARS} but also checks whether goals have been solved. *) - val tclEVARSADVANCE : Evd.evar_map -> unit tactic - - (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently - being proved, appending them to the list of focused goals. If a - goal is already solved, it is not added. *) - val tclNEWGOALS : Goal.goal list -> unit tactic - - (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a - goal is already solved, it is not set. *) - val tclSETGOALS : Goal.goal list -> unit tactic - - (** [tclGETGOALS] returns the list of goals under focus. *) - val tclGETGOALS : Goal.goal list tactic - - (** Sets the evar universe context. *) - val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic - - (** Clears the future goals store in the proof view. *) - val reset_future_goals : proofview -> proofview - - (** Give an evar the status of a goal (changes its source location - and makes it unresolvable for type classes. *) - val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map - - (** [advance sigma g] returns [Some g'] if [g'] is undefined and is - the current avatar of [g] (for instance [g] was changed by [clear] - into [g']). It returns [None] if [g] has been (partially) - solved. *) - val advance : Evd.evar_map -> Evar.t -> Evar.t option -end - -(** This module gives access to the innards of the monad. Its use is - restricted to very specific cases. *) -module UnsafeRepr : -sig - type state = Proofview_monad.Logical.Unsafe.state - val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t - val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic -end - -(** {6 Goal-dependent tactics} *) - -module Goal : sig - - (** Type of goals. - - The first parameter type is a phantom argument indicating whether the data - contained in the goal has been normalized w.r.t. the current sigma. If it - is the case, it is flagged [ `NF ]. You may still access the un-normalized - data using {!assume} if you known you do not rely on the assumption of - being normalized, at your own risk. - - The second parameter is a stage indicating where the goal belongs. See - module {!Sigma}. - *) - type ('a, 'r) t - - (** Assume that you do not need the goal to be normalized. *) - val assume : ('a, 'r) t -> ([ `NF ], 'r) t - - (** Normalises the argument goal. *) - val normalize : ('a, 'r) t -> ([ `NF ], 'r) t tactic - - (** [concl], [hyps], [env] and [sigma] given a goal [gl] return - respectively the conclusion of [gl], the hypotheses of [gl], the - environment of [gl] (i.e. the global environment and the - hypotheses) and the current evar map. *) - val concl : ([ `NF ], 'r) t -> Term.constr - val hyps : ([ `NF ], 'r) t -> Context.Named.t - val env : ('a, 'r) t -> Environ.env - val sigma : ('a, 'r) t -> 'r Sigma.t - val extra : ('a, 'r) t -> Evd.Store.t - - (** Returns the goal's conclusion even if the goal is not - normalised. *) - val raw_concl : ('a, 'r) t -> Term.constr - - type ('a, 'b) enter = - { enter : 'r. ('a, 'r) t -> 'b } - - (** [nf_enter t] applies the goal-dependent tactic [t] in each goal - independently, in the manner of {!tclINDEPENDENT} except that - the current goal is also given as an argument to [t]. The goal - is normalised with respect to evars. *) - val nf_enter : ([ `NF ], unit tactic) enter -> unit tactic - - (** Like {!nf_enter}, but does not normalize the goal beforehand. *) - val enter : ([ `LZ ], unit tactic) enter -> unit tactic - - type ('a, 'b) s_enter = - { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } - - (** A variant of {!enter} allows to work with a monotonic state. The evarmap - returned by the argument is put back into the current state before firing - the returned tactic. *) - val s_enter : ([ `LZ ], unit tactic) s_enter -> unit tactic - - (** Like {!s_enter}, but normalizes the goal beforehand. *) - val nf_s_enter : ([ `NF ], unit tactic) s_enter -> unit tactic - - (** Recover the list of current goals under focus, without evar-normalization. - FIXME: encapsulate the level in an existential type. *) - val goals : ([ `LZ ], 'r) t tactic list tactic - - (** Compatibility: avoid if possible *) - val goal : ([ `NF ], 'r) t -> Evar.t - - (** Every goal is valid at a later stage. FIXME: take a later evarmap *) - val lift : ('a, 'r) t -> ('r, 's) Sigma.le -> ('a, 's) t - -end - - -(** {6 Trace} *) - -module Trace : sig - - (** [record_info_trace t] behaves like [t] except the [info] trace - is stored. *) - val record_info_trace : 'a tactic -> 'a tactic - - val log : Proofview_monad.lazy_msg -> unit tactic - val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic - - val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.std_ppcmds - -end - - -(** {6 Non-logical state} *) - -(** The [NonLogical] module allows the execution of effects (including - I/O) in tactics (non-logical side-effects are not discarded at - failures). *) -module NonLogical : module type of Logic_monad.NonLogical - -(** [tclLIFT c] is a tactic which behaves exactly as [c]. *) -val tclLIFT : 'a NonLogical.t -> 'a tactic - - -(**/**) - -(*** Compatibility layer with <= 8.2 tactics ***) -module V82 : sig - type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - val tactic : tac -> unit tactic - - (* normalises the evars in the goals, and stores the result in - solution. *) - val nf_evar_goals : unit tactic - - val has_unresolved_evar : proofview -> bool - - (* Main function in the implementation of Grab Existential Variables. - Resets the proofview's goals so that it contains all unresolved evars - (in chronological order of insertion). *) - val grab : proofview -> proofview - - (* Returns the open goals of the proofview together with the evar_map to - interpret them. *) - val goals : proofview -> Evar.t list Evd.sigma - - val top_goals : entry -> proofview -> Evar.t list Evd.sigma - - (* returns the existential variable used to start the proof *) - val top_evars : entry -> Evd.evar list - - (* Caution: this function loses quite a bit of information. It - should be avoided as much as possible. It should work as - expected for a tactic obtained from {!V82.tactic} though. *) - val of_tactic : 'a tactic -> tac - - (* marks as unsafe if the argument is [false] *) - val put_status : bool -> unit tactic - - (* exception for which it is deemed to be safe to transmute into - tactic failure. *) - val catchable_exception : exn -> bool - - (* transforms every Ocaml (catchable) exception into a failure in - the monad. *) - val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic -end - -(** {7 Notations} *) - -module Notations : sig - - (** {!tclBIND} *) - val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic - (** {!tclTHEN} *) - val (<*>) : unit tactic -> 'a tactic -> 'a tactic - (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *) - val (<+>) : 'a tactic -> 'a tactic -> 'a tactic - - type ('a, 'b) enter = ('a, 'b) Goal.enter = - { enter : 'r. ('a, 'r) Goal.t -> 'b } - type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter = - { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma } -end |