diff options
| -rw-r--r-- | proofs/proofview.ml | 617 | ||||
| -rw-r--r-- | proofs/proofview.mli | 503 |
2 files changed, 641 insertions, 479 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 4b46417e9..5f2a5b786 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -6,19 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* The proofview datastructure is a pure datastructure underlying the notion - of proof (namely, a proof is a proofview which can evolve and has safety - mechanisms attached). - The general idea of the structure is that it is composed of a chemical - solution: an unstructured bag of stuff which has some relations with - one another, which represents the various subnodes of the proof. Together - with a comb: a datastructure that gives some order to some of these nodes, - namely the (focused) open goals. - The natural candidate for the solution is an {!Evd.evar_map}, that is - a calculus of evars. The comb is then a list of goals (evars wrapped - with some extra information, like possible name anotations). - There is also need of a list of the evars which initialised the proofview - to be able to return information about the proofview. *) + +(** 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 @@ -29,9 +22,20 @@ 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 + + +(** {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) @@ -55,8 +59,6 @@ let dependent_init = let solution = Evd.reset_future_goals solution in entry, { v with solution } -(* Initialises a proofview, the argument is a list of environement, - conclusion types, and optional names, creating that many initial goals. *) let init = let rec aux sigma = function | [] -> TNil sigma @@ -66,14 +68,10 @@ let init = let initial_goals initial = initial -(* Returns whether this proofview is finished or not. That is, - if it has empty subgoals in the comb. There could still be unsolved - subgoaled, but they would then be out of the view, focused out. *) let finished = function | {comb = []} -> true | _ -> false -(* Returns the current value of the proofview partial proofs. *) let return { solution=defs } = defs let return_constr { solution = defs } c = Evarutil.nf_evar defs c @@ -81,23 +79,34 @@ 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) -(* Type of the object which allow to unfocus a view.*) -(* First component is a reverse list of what comes before - and second component is what goes after (in the expected - order) *) +(** {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 ]. *) +(** 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) = @@ -106,23 +115,25 @@ let focus_sublist i j l = in (sub, (left,right)) -(* Inverse operation to the previous one. *) +(** 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). (i.e. goals number [i] to [j] become the only goals of the - returned proofview). The first goal has index 1. - It returns the focus proof, and a context for the focus trace. *) +(** [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. *) +(** [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 @@ -146,49 +157,48 @@ let rec advance sigma g = unsolved (after advancing cleared goals). *) let undefined defs l = CList.map_filter (advance defs) l -(* Unfocuses a proofview with respect to a context. *) +(** Unfocuses a proofview with respect to a context. *) let unfocus c sp = { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) } -(* 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] or tactics to reorder - the focused goals (not done yet). - (* spiwack: the ordering of goals, though, is actually rather - brittle. It would be much more interesting to find a more - robust way to adress goals, I have no idea at this time - though*) - 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 - seens as a function (without argument) which returns a value - of type 'a and modifies the environement (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. - (* spiwack: as far as I'm aware this doesn't really relate to - F. Kirchner and C. Muñoz. - *) - 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). +(** {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 + seens as a function (without argument) which returns a value of + type 'a and modifies the environement (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: +(** type of tactics: tactics can - access the environment, @@ -197,59 +207,51 @@ module Proof = Logical - backtrack on previous changes of the proofview *) type +'a tactic = 'a Proof.t -type 'a case = -| Fail of exn -| Next of 'a * (exn -> 'a tactic) - -(* Applies a tactic to the current proofview. *) +(** Applies a tactic to the current proofview. *) let apply env t sp = let (next_r,(next_state,_),status) = Logic_monad.NonLogical.run (Proof.run t () (sp,env)) in next_r,next_state,status -(*** tacticals ***) - -let catchable_exception = function - | Logic_monad.Exception _ -> false - | e -> Errors.noncritical e +(** {7 Monadic primitives} *) -(* Unit of the tactic monad *) +(** Unit of the tactic monad. *) let tclUNIT = Proof.return -(* Bind operation of the tactic monad *) +(** Bind operation of the tactic monad. *) let tclBIND = Proof.(>>=) -(* Interpretes the ";" (semicolon) of Ltac. - As a monadic operation, it's a specialized "bind" - on unit-returning tactic (meaning "there is no value to bind") *) +(** 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 value at the end. *) +(** [tclIGNORE t] has the same operational content as [t], but drops + the returned value. *) let tclIGNORE = Proof.ignore -(* [tclOR t1 t2 = 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]. No interleaving at this point. *) -let tclOR = Proof.plus +module Monad = Proof + + -(* [tclZERO e] always fails with error message [e]*) +(** {7 Failure and backtracking} *) + + +(** [tclZERO e] fails with exception [e]. It has no success. *) let tclZERO = Proof.zero -(* [tclCASE t] observes the head of the tactic and returns it as a value *) -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) +(** [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] behaves like [t1] if [t1] succeeds at least once - or [t2] if [t1] fails. *) +(** [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 @@ -257,9 +259,9 @@ let tclORELSE t1 t2 = | 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]. *) +(** [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 @@ -267,23 +269,25 @@ let tclIFCATCH a s f = | Nil e -> f e | Cons (x,a') -> plus (s x) (fun e -> (a' e) >>= fun x' -> (s x')) -(* [tclONCE t] fails if [t] fails, otherwise it has exactly one - success. *) +(** [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 -let tclBREAK = Proof.break - exception MoreThanOneSuccess let _ = Errors.register_handler begin function | MoreThanOneSuccess -> Errors.error "This tactic has more than one success." | _ -> raise Errors.Unhandled end -(* [tclONCE e t] succeeds as [t] if [t] has exactly one - success. Otherwise it fails. It may behave differently than [t] as - there may be extra non-logical effects used to discover that [t] - does not have a second success. Moreover the second success may be - conditional on the error recieved: [e] is used. *) +(** [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 @@ -295,12 +299,34 @@ let tclEXACTLY_ONCE e t = | _ -> tclZERO MoreThanOneSuccess -(* Focuses a tactic at a range of subgoals, found by their indices. *) +(** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *) +type 'a case = +| Fail of exn +| Next of 'a * (exn -> '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 let _ = Errors.register_handler begin function | NoSuchGoals n -> Errors.error ("No such " ^ String.plural n "goal" ^".") | _ -> 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 -> @@ -315,6 +341,7 @@ let tclFOCUS_gen nosuchgoal i j t = 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 -> @@ -332,16 +359,9 @@ let tclFOCUSID id t = aux 1 initial.comb -(* Dispatch tacticals are used to apply a different tactic to each goal under - consideration. 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 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. *) +(** {7 Dispatching on goals} *) + exception SizeMismatch of int*int let _ = Errors.register_handler begin function | SizeMismatch (i,_) -> @@ -398,10 +418,26 @@ let fold_left2_goal i s l = | reraise -> tclZERO reraise end -(* spiwack: we use an parametrised function to generate the dispatch - tacticals. [tclDISPATCHGEN] takes an argument [join] to reify the - list of produced value into the final value. *) -let tclDISPATCHGEN f join tacs = +(** 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 tclDISPATCHGEN join tacs = match tacs with | [] -> begin @@ -417,20 +453,23 @@ let tclDISPATCHGEN f join tacs = | { comb=[goal] ; solution } -> begin match advance solution goal with | None -> tclUNIT (join []) - | Some _ -> Proof.map (fun res -> join [res]) (f tac) + | 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) (f t) in + 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 tclDISPATCH tacs = tclDISPATCHGEN Util.identity Pervasives.ignore tacs +let tclDISPATCH tacs = tclDISPATCHGEN Pervasives.ignore tacs -let tclDISPATCHL tacs = - tclDISPATCHGEN Util.identity CList.rev 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 @@ -451,6 +490,11 @@ let extend_to_list startxs rx endxs l = 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 -> @@ -461,10 +505,11 @@ let tclEXTEND tacs1 rtac tacs2 = tclZERO (SizeMismatch( CList.length comb, (CList.length tacs1)+(CList.length tacs2))) -(* spiwack: failure occur only when the number of goals is too +(* 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 -> @@ -473,7 +518,152 @@ let tclINDEPENDENT tac = | [_] -> tac | _ -> iter_goal (fun _ -> tac) -(* Equality function on goals *) + + +(** {7 Goal manipulation} *) + +(** Shelves all the goals under focus. *) +let shelve = + let open Proof in + Comb.get >>= fun initial -> + Comb.set [] >> + Shelf.put 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 >> + Shelf.put u + +(** [guard_no_unifiable] fails with error [UnresolvedBindings] 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 () + | 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 + tclZERO (Logic.RefinerError (Logic.UnresolvedBindings 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 } + + +(** [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 = + 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 = + 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 = + 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 >> + Giveup.put initial + + + +(** {7 Control primitives} *) + +(** 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 @@ -493,20 +683,6 @@ let tclPROGRESS t = else tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) -let tclEVARMAP = Solution.get - -let tclENV = Env.get - - -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) - exception Timeout let _ = Errors.register_handler begin function | Timeout -> Errors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") @@ -570,120 +746,12 @@ let tclTIME s t = tclOR (tclUNIT x) (fun e -> aux (n+1) (k e)) in aux 0 t -let mark_as_unsafe = Status.put false - -(* Shelves all the goals under focus. *) -let shelve = - let open Proof in - Comb.get >>= fun initial -> - Comb.set [] >> - Shelf.put 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 >> - Shelf.put u - -let check_no_dependencies = - let open Proof in - Pv.get >>= fun initial -> - let (u,n) = partition_unifiable initial.solution initial.comb in - match u with - | [] -> tclUNIT () - | 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 - tclZERO (Logic.RefinerError (Logic.UnresolvedBindings 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 } - -(* 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 >> - Giveup.put initial -(** [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 = - 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 = - 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 = - Comb.modify CList.rev - -let numgoals = - let open Proof in - Comb.get >>= fun comb -> - return (CList.length comb) +(** {7 Unsafe primitives} *) module Unsafe = struct - (* A [Proofview.tactic] version of [Refiner.tclEVARS] *) let tclEVARS evd = Pv.modify (fun ps -> { ps with solution = evd }) @@ -702,10 +770,12 @@ module Unsafe = struct let reset_future_goals p = { p with solution = Evd.reset_future_goals p.solution } - end -module Monad = Proof + + +(** {7 Notations} *) + module Notations = struct let (>>=) = tclBIND let (<*>) = tclTHEN @@ -714,9 +784,18 @@ end open Notations + + +(** {6 Goal-dependent tactics} *) + (* To avoid shadowing by the local [Goal] module *) module GoalV82 = Goal.V82 +let catchable_exception = function + | Logic_monad.Exception _ -> false + | e -> Errors.noncritical e + + module Goal = struct type 'a t = { @@ -800,6 +879,10 @@ module Goal = struct end + + +(** {6 The refine tactic} *) + module Refine = struct @@ -873,6 +956,10 @@ struct end end + + +(** {6 Non-logical state} *) + module NonLogical = Logic_monad.NonLogical let tclLIFT = Proof.lift diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 914af982d..3529c3c1b 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -6,26 +6,19 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* The proofview datastructure is a pure datastructure underlying the notion - of proof (namely, a proof is a proofview which can evolve and has safety - mechanisms attached). - The general idea of the structure is that it is composed of a chemical - solution: an unstructured bag of stuff which has some relations with - one another, which represents the various subnodes of the proof. Together - with a comb: a datastructure that gives some order to some of these nodes, - namely the (focused) open goals. - The natural candidate for the solution is an {!Evd.evar_map}, that is - a calculus of evars. The comb is then a list of goals (evars wrapped - with some extra information, like possible name anotations). - There is also need of a list of the evars which initialised the proofview - to be able to return information about the proofview. *) +(** 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 Term +(** Main state of tactics *) type proofview -(* Returns a stylised view of a proofview for use by, for instance, - ide-s. *) +(** 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. *) @@ -33,243 +26,272 @@ type proofview 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 -(* Initialises a proofview, the argument is a list of environement, - conclusion types, creating that many initial goals. *) +(** Initialises a proofview, the main argument is a list of + environements (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 depedenent on one - another. Dependencies between goals is represented with the type - [telescope] instead of [list]. *) +(** 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 -(* Returns whether this proofview is finished or not. That is, - if it has empty subgoals in the comb. There could still be unsolved - subgoaled, but they would then be out of the view, focused out. *) +(** [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 value of the proofview partial proofs. *) +(** 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 -(*** Focusing operations ***) -(* Type of the object which allow to unfocus a view.*) + +(** {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. *) +(** 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: returns the number of goals that are held *) +(* 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). (i.e. goals number [i] to [j] become the only goals of the - returned proofview). - It returns the focus proof, and a context for the focus trace. *) +(** [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. *) +(** Unfocuses a proofview with respect to a context. *) val unfocus : focus_context -> proofview -> proofview -(* 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] or tactics to reorder - the focused goals (not done yet). - (* spiwack: the ordering of goals, though, is actually rather - brittle. It would be much more interesting to find a more - robust way to adress goals, I have no idea at this time - though*) - 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 - seens as a function (without argument) which returns a value - of type 'a and modifies the environement (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. - (* spiwack: as far as I'm aware this doesn't really relate to - F. Kirchner and C. Muñoz. - *) - 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). + +(** {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 + seens as a function (without argument) which returns a value of + type 'a and modifies the environement (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 -type 'a case = -| Fail of exn -| Next of 'a * (exn -> 'a tactic) - -(* Applies a tactic to the current proofview. *) -(* the return boolean signals the use of an unsafe tactic, in which - case it is [false]. *) +(** 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) -(*** tacticals ***) +(** {7 Monadic primitives} *) -(* Unit of the tactic monad *) +(** Unit of the tactic monad. *) val tclUNIT : 'a -> 'a tactic -(* Bind operation of the tactic monad *) +(** 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" - on unit-returning tactic (meaning "there is no value to bind") *) +(** 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 value at the end. *) +(** [tclIGNORE t] has the same operational content as [t], but drops + the returned value. *) val tclIGNORE : 'a tactic -> unit tactic -(* [tclOR t1 t2 = 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]. No interleaving at this point. *) -val tclOR : 'a tactic -> (exn -> 'a tactic) -> 'a tactic +(** Generic monadic combinators for tactics. *) +module Monad : Monad.S with type +'a t = 'a tactic + +(** {7 Failure and backtracking} *) -(* [tclZERO] always fails *) +(** [tclZERO e] fails with exception [e]. It has no success. *) val tclZERO : exn -> 'a tactic -(* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once - or [t2 e] if [t1] fails with [e]. *) -val tclORELSE : 'a tactic -> (exn -> 'a tactic) -> '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 -> (exn -> 'a tactic) -> 'a tactic -(* [tclCASE t] observes the head of the tactic and returns it as a value *) -val tclCASE : 'a tactic -> 'a case 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 -> (exn -> '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]. *) +(** [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) -> (exn -> 'b tactic) -> 'b tactic -(* [tclONCE t] fails if [t] fails, otherwise it has exactly one - success. *) +(** [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 -(* [tclBREAK f t] is a generalization of [tclONCE t]. Instead of stopping at the - first element encountered, it waits for the tactic to return an exception - satisfying [f], and drop the remaining results. [tclONCE t] is equivalent to - [tclBREAK (fun _ -> true) t]. *) +(** [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 exn + | Next of 'a * (exn -> '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=true] is raised. At + which point it drop the remaining successes. [tclONCE t] is + equivalent to [tclBREAK (fun _ -> true) t]. *) val tclBREAK : (exn -> bool) -> 'a tactic -> 'a tactic -(* [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one - success. Otherwise it fails. It may behave differently than [t] as - there may be extra non-logical effects used to discover that [t] - does not have a second success. Moreover the second success may be - conditional on the error received: [e] is used. *) -val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic -(* Focuses a tactic at a range of subgoals, found by their indices. - The other goals are restored to the focus when the tactic is done. +(** {7 Focusing tactics} *) - If the specified range doesn't correspond to existing goals, fails - with [NoSuchGoals]. *) +(** [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). *) exception NoSuchGoals of int 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 -(* Focuses a tactic at a range of subgoals, found by their indices. - The other goals are restored to the focus when the tactic is done. - - If the specified range doesn't correspond to existing goals, behaves - like [tclUNIT ()]. *) +(** [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 -(* Dispatch tacticals are used to apply a different tactic to each goal under - consideration. 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 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. +(** {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]. - 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. *) + 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 to [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. *) +(** [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. *) +(** [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 -(* [tclPROGRESS t] behaves has [t] as long as [t] progresses. *) -val tclPROGRESS : 'a tactic -> 'a tactic - -(* [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 returned by {!Proofview.Goal.env}. *) -val tclENV : Environ.env tactic - -(* [tclEFFECTS eff] add the effects [eff] to the current state. *) -val tclEFFECTS : Declareops.side_effects -> unit tactic -(* Checks for interrupts *) -val tclCHECKINTERRUPT : 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). *) +(** 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). *) +(** 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 -(* This fails with error UnresolvedBindings if some goals are - dependent in the current list of goals under focus *) -val check_no_dependencies : unit tactic +(** [guard_no_unifiable] fails with error [UnresolvedBindings] if some + goals are unifiable (see {!shelve_unifiable}) in the current focus. *) +val guard_no_unifiable : unit tactic -(* [unshelve l p] adds all the goals in [l] at the end of the focused - goals of p *) +(** [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 - -(* Gives up on the goal under focus. Reports an unsafe status. Proofs - with given up goals cannot be closed. *) -val give_up : unit 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 @@ -280,12 +302,49 @@ val cycle : int -> unit tactic [1] as well, rather than raising an error. *) val swap : int -> int -> unit tactic -(** [revgoals] reverse the list of focused goals. *) +(** [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 : Declareops.side_effects -> 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]. *) @@ -295,48 +354,51 @@ val tclTIMEOUT : int -> 'a tactic -> 'a tactic identifying annotation if present *) val tclTIME : string option -> 'a tactic -> 'a tactic -(** [mark_as_unsafe] signals that the current tactic is unsafe. *) -val mark_as_unsafe : unit 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 - (* Assumes the new evar_map does not change existing goals *) + (** [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 - - (* [tclNEWGOALS gls] adds the goals [gls] to the ones currently - being proved, appending them to the list of focussed goals. If a - goal is already solved, it is not added. Prefer the other - primitives when possible. *) - val tclNEWGOALS : Goal.goal list -> unit tactic - - (* Assumes the new evar_map might be solving some existing goals *) + (** Like {!tclEVARS} but also checks whether goals have been solved. *) val tclEVARSADVANCE : Evd.evar_map -> unit tactic - (* Set the evar universe context *) + (** [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 + + (** Sets the evar universe context. *) val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic - (* Clears the future goals store in the proof. *) + (** Clears the future goals store in the proof view. *) val reset_future_goals : proofview -> proofview end -module Monad : Monad.S with type +'a t = 'a tactic +(** {7 Notations} *) -(* Notations for building tactics. *) module Notations : sig - (* tclBIND *) + (** {!tclBIND} *) val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic - (* tclTHEN *) + (** {!tclTHEN} *) val (<*>) : unit tactic -> 'a tactic -> 'a tactic - (* tclOR *) + (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *) val (<+>) : 'a tactic -> 'a tactic -> 'a tactic + end -(* The module goal provides an interface for goal-dependent tactics. *) -(* spiwack: there are still parts of the code which depend on proofs/goal.ml. - Eventually I'll try to remove it in favour of [Proofview.Goal] *) +(** {6 Goal-dependent tactics} *) + module Goal : sig (** The type of goals. The parameter type is a phantom argument indicating @@ -352,65 +414,78 @@ module Goal : sig (** Normalises the argument goal. *) val normalize : 'a t -> [ `NF ] 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. *) + (** [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 ] t -> Term.constr val hyps : [ `NF ] t -> Context.named_context val env : 'a t -> Environ.env val sigma : 'a t -> Evd.evar_map + (** Returns the goal's conclusion even if the goal is not + normalised. *) val raw_concl : 'a t -> Term.constr - (* [nf_enter t] execute the goal-dependent tactic [t] in each goal - independently. In particular [t] need not backtrack the same way in - each goal. *) + (** [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 ] t -> unit tactic) -> unit tactic - (** Same as nf_enter, but does not normalize the goal beforehand. *) + (** Like {!nf_enter}, but does not normalize the goal beforehand. *) val enter : ([ `LZ ] t -> unit tactic) -> unit tactic (** Recover the list of current goals under focus, without evar-normalization *) val goals : [ `LZ ] t tactic list tactic - (* compatibility: avoid if possible *) + (** Compatibility: avoid if possible *) val goal : [ `NF ] t -> Evar.t end -(** A light interface for building tactics out of partial term. Be careful, - the [refine] function does not do any typechecking, so you may construct - ill-typed terms without noticing. *) + +(** {6 The refine tactic} *) + module Refine : sig + (** {7 Refinement primitives} *) + + val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic + (** In [refine ?unsafe t], [t] is a term with holes under some + [evar_map] context. The term [t] is used as a partial solution + for the current goal (refine is a goal-dependent tactic), the + new holes created by [t] become the new subgoals. Exception + raised during the interpretation of [t] are caught and result in + tactic failures. If [unsafe] is [true] (default) [t] is + type-checked beforehand. *) + + (** {7 Helper functions} *) + val with_type : Environ.env -> Evd.evar_map -> Term.constr -> Term.types -> Evd.evar_map * Term.constr (** [with_type env sigma c t] ensures that [c] is of type [t] inserting a coercion if needed. *) - val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic - (** Given a term with holes that have been generated through - {!new_evar}, this function fills the current hole with the given - constr and creates goals for all the holes in their generation - order. The [evar_map] in the argument function is assumed to - only increase. Exceptions raised by the function are caught. *) - - val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic -(** Like {!refine} except the refined term is coerced to the conclusion of the - current goal. *) + val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*Constr.t) -> unit tactic + (** Like {!refine} except the refined term is coerced to the conclusion of the + current goal. *) end -(* The [NonLogical] module allows the execution of side effects in tactics - (non-logical side-effects are not discarded at failures). *) + +(** {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] includes the non-logical command [c] in a tactic. *) +(** [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 |