diff options
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | proofs/monads.ml | 227 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 1 | ||||
| -rw-r--r-- | proofs/proofview.ml | 357 | ||||
| -rw-r--r-- | proofs/proofview.mli | 13 |
5 files changed, 404 insertions, 195 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index a6d93aa8c..45da00a72 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -126,6 +126,7 @@ Logic Refiner Clenv Evar_refiner +Monads Proofview Proof Proof_global diff --git a/proofs/monads.ml b/proofs/monads.ml new file mode 100644 index 000000000..1337931b1 --- /dev/null +++ b/proofs/monads.ml @@ -0,0 +1,227 @@ +module type Type = sig + type t +end + +module type S = sig + type +'a t + + val return : 'a -> 'a t + val bind : 'a t -> ('a -> 'b t) -> 'b t + val seq : unit t -> 'a t -> 'a t + val ignore : 'a t -> unit t +(* spiwack: these will suffice for now, if we would use monads more + globally, then I would add map/join/List.map and such functions, + plus default implementations *) +end + +module type State = sig + type s (* type of the state *) + include S + + val set : s -> unit t + val get : s t +end + +module Id : S with type 'a t = 'a = struct + type 'a t = 'a + + let return x = x + let bind x k = k x + let ignore x = Pervasives.ignore x + let seq () x = x +end + +(* State monad transformer, adapted from Haskell's StateT *) +module State (X:Type) (T:S) : sig + (* spiwack: it is not essential that both ['a result] and ['a t] be + private (or either, for that matter). I just hope it will help + catch more programming errors. *) + type +'a result = private { result : 'a ; state : X.t } + include State with type s = X.t and type +'a t = private X.t -> 'a result T.t + (* a function version of the coercion from the private type ['a t].*) + val run : 'a t -> s -> 'a result T.t + val lift : 'a T.t -> 'a t +end = struct + type s = X.t + type 'a result = { result : 'a ; state : s } + type 'a t = s -> 'a result T.t + + let run x = x + (*spiwack: convenience notation, waiting for ocaml 3.12 *) + let (>>=) = T.bind + let return x s = T.return { result=x ; state=s } + let bind x k s = + x s >>= fun { result=a ; state=s } -> + k a s + let ignore x s = + x s >>= fun x' -> + T.return { x' with result=() } + let seq x t s = + (x s) >>= fun x' -> + t x'.state + let lift x s = + x >>= fun a -> + T.return { result=a ; state=s } + + let set s _ = + T.return { result=() ; state=s } + let get s = + T.return { result=s ; state=s } +end + +(* Double-continuation backtracking monads are reasonable folklore for + "search" implementations (including Tac interactive prover's + tactics). Yet it's quite hard to wrap your head around these. I + recommand reading a few times the "Backtracking, Interleaving, and + Terminating Monad Transformers" paper by O. Kiselyov, C. Chen, + D. Fridman. The peculiar shape of the monadic type is reminiscent + of that of the continuation monad transformer. + + The paper also contains the rational for the [split] abstraction. + + An explanation of how to derive such a monad from mathematical + principle can be found in "Kan Extensions for Program Optimisation" by + Ralf Hinze. *) +module type Logic = sig + include S + + (* [zero] is usually argument free, but Coq likes to explain errors, + hence error messages should be carried around. *) + val zero : exn -> 'a t + val plus : 'a t -> 'a t -> 'a t +(** Writing (+) for plus and (>>=) for bind, we shall require that + + zero+x = x + + x+zero = x + + (x+y)>>=k = (x>>=k)+(y>>=k) *) + + (** [split x] runs [x] until it either fails with [zero e] or finds + a result [a]. In the former case it returns [Inr e], otherwise + it returns [Inl (a,y)] where [y] can be run to get more results + from [x]. It is a variant of prolog's cut. *) + val split : 'a t -> ('a * 'a t , exn ) Util.union t +end +(* The [T] argument represents the "global" effect: it is not + backtracked when backtracking occurs at a [plus]. *) +(* spiwack: hence, [T] will not be instanciated with a state monad + representing the proofs, we will use a surrounding state transformer + to that effect. In fact at the time I'm writing this comment, I have + no immediate use for [T]. We might, however, consider instantiating it + with a "writer" monad around [Pp] to implement [idtac "msg"] for + instance. *) +module Logic (T:S) : sig + include Logic + + (** [run x] raises [e] if [x] is [zero e]. *) + val run : 'a t -> 'a T.t + + val lift : 'a T.t -> 'a t +end = struct +(* spiwack: the implementation is an adaptation of the aforementionned + "Backtracking, Interleaving, and Terminating Monad Transformers" + paper *) + (* spiwack: [fk] stands for failure continuation, and [sk] for success + continuation. *) + type +'r fk = exn -> 'r + type (-'a,'r) sk = 'a -> 'r fk -> 'r + type 'a t = { go : 'r. ('a,'r T.t) sk -> 'r T.t fk -> 'r T.t } + + let return x = { go = fun sk fk -> + sk x fk + } + let bind x k = { go = fun sk fk -> + x.go (fun a fk -> (k a).go sk fk) fk + } + let ignore x = { go = fun sk fk -> + x.go (fun _ fk -> sk () fk) fk + } + let seq x t = { go = fun sk fk -> + x.go (fun () fk -> t.go sk fk) fk + } + + let zero e = { go = fun _ fk -> fk e } + (* [plus x y] ignores any error raised by [x]. *) + let plus x y = { go = fun sk fk -> + x.go sk (fun _ -> y.go sk fk) + } + + let lift x = { go = fun sk fk -> + T.bind x (fun a -> sk a fk) + } + + let run x = + let sk a _ = T.return a in + let fk e = raise e in + x.go sk fk + + (* For [reflect] and [split] see the "Backtracking, Interleaving, + and Terminating Monad Transformers" paper *) + let reflect : ('a*'a t , exn) Util.union -> 'a t = function + | Util.Inr e -> zero e + | Util.Inl (a,x) -> plus (return a) x + + let split x = + (* spiwack: I cannot be sure right now, but [anomaly] shouldn't be + reachable. If it is reachable there may be some redesign to be + done around success continuations. *) + let anomaly = Errors.Anomaly ("Monads.Logic(T).split", Pp.str"[fk] should ignore this error") in + let fk e = T.return (Util.Inr e) in + let sk a fk = T.return (Util.Inl (a,bind (lift (fk anomaly)) reflect)) in + lift (x.go sk fk) +end + + +(* [State(X)(T:Logic)] can be lifted to [Logic] by backtracking on state on [plus].*) +module StateLogic(X:Type)(T:Logic) : sig + (* spiwack: some duplication from interfaces as we need ocaml 3.12 + to substitute inside signatures. *) + type s = X.t + type +'a result = private { result : 'a ; state : s } + include Logic with type +'a t = private X.t -> 'a result T.t + + val set : s -> unit t + val get : s t + + val run : 'a t -> s -> 'a result T.t +end = struct + + module S = State(X)(T) + include S + + let zero e = lift (T.zero e) + let plus x y = + (* spiwack: convenience notation, waiting for ocaml 3.12 *) + let (>>=) = bind in + let (>>) = seq in + get >>= fun initial -> + lift begin + (T.plus (run x initial) (run y initial)) + end >>= fun { result = a ; state = final } -> + set final >> + return a + (* spiwack: the definition of [plus] is essentially [plus x y = fun s + -> T.plus (run x s) (run y s)]. But the [private] annotation + prevents us from writing that. Maybe I should remove [private] + around [+'a t] (it would be unnecessary to remove that of ['a + result]) after all. I'll leave it like that for now. *) + + let split x = + (* spiwack: convenience notation, waiting for ocaml 3.12 *) + let (>>=) = bind in + let (>>) = seq in + get >>= fun initial -> + lift (T.split (run x initial)) >>= function + | Util.Inr _ as e -> return e + | Util.Inl (a,y) -> + let y' = + lift y >>= fun b -> + set b.state >> + return b.result + in + set a.state >> + return (Util.Inl(a.result,y')) +end + + diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index ca0c7dd0d..96af73b71 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,5 +1,6 @@ Goal Evar_refiner +Monads Proofview Proof Proof_global diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 00e311cc9..347783a66 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -173,104 +173,78 @@ let unfocus c sp = specialized bind on unit-returning tactics). *) -(* type of tactics *) -(* spiwack: double-continuation backtracking monads are reasonable - folklore for "search" implementations (including Tac interactive prover's - tactics). Yet it's quite hard to wrap your head around these. - I recommand reading a few times the "Backtracking, Interleaving, and Terminating - Monad Transformers" paper by O. Kiselyov, C. Chen, D. Fridman. - The peculiar shape of the monadic type is reminiscent of that of the continuation - monad transformer. - A good way to get a feel of what's happening is to look at what happens when - executing [apply (tclUNIT ())]. - The disjunction function is unlike that of the LogicT paper, because we want and - need to backtrack over state as well as values. Therefore we cannot be - polymorphic over the inner monad. *) -type proof_step = { goals : Goal.goal list ; defs : Evd.evar_map } -type +'a result = { proof_step : proof_step ; - content : 'a } - -(* nb=non-backtracking *) -type +'a nb_tactic = proof_step -> 'a result - -(* double-continutation backtracking *) -(* "sk" stands for "success continuation", "fk" for "failure continuation" *) -type 'r fk = exn -> 'r -type (-'a,'r) sk = 'a -> 'r fk -> 'r -type +'a tactic0 = { go : 'r. ('a, 'r nb_tactic) sk -> 'r nb_tactic fk -> 'r nb_tactic } - -(* We obtain a tactic by parametrizing with an environment *) -(* spiwack: alternatively the environment could be part of the "nb_tactic" state - monad. As long as we do not intend to change the environment during a tactic, - it's probably better here. *) -type +'a tactic = Environ.env -> 'a tactic0 - -(* unit of [nb_tactic] *) -let nb_tac_unit a step = { proof_step = step ; content = a } +(* type of tactics: + + tactics can + - access the environment, + - access and change the current [proofview] + - backtrack on previous changes of the proofview *) +(* spiwack: it seems lighter, for now, to deal with the environment here rather than in [Monads]. *) + +module LocalState = struct + type t = proofview +end +module Backtrack = Monads.Logic(Monads.Id) +module Inner = Monads.StateLogic(LocalState)(Backtrack) + +type +'a tactic = Environ.env -> 'a Inner.t (* Applies a tactic to the current proofview. *) -let apply env t sp = - let start = { goals = sp.comb ; defs = sp.solution } in - let res = (t env).go (fun a _ step -> nb_tac_unit a step) (fun e _ -> raise e) start in - let next = res.proof_step in - {sp with - solution = next.defs ; - comb = next.goals - } +let apply env t sp = + let next = Backtrack.run (Inner.run (t env) sp) in + next.Inner.state (*** tacticals ***) (* Unit of the tactic monad *) -let tclUNIT a _ = { go = fun sk fk step -> sk a fk step } +let tclUNIT a _ = Inner.return a (* Bind operation of the tactic monad *) -let tclBIND t k env = { go = fun sk fk step -> - (t env).go (fun a fk -> (k a env).go sk fk) fk step -} +let tclBIND t k env = + Inner.bind (t env) (fun a -> k a env) (* 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") *) -let tclTHEN t1 t2 env = { go = fun sk fk step -> - (t1 env).go (fun () fk -> (t2 env).go sk fk) fk step -} +let tclTHEN t1 t2 env = + Inner.seq (t1 env) (t2 env) (* [tclIGNORE t] has the same operational content as [t], but drops the value at the end. *) -let tclIGNORE tac env = { go = fun sk fk step -> - (tac env).go (fun _ fk -> sk () fk) fk step -} - -(* [tclOR t1 t2 = t1] if t1 succeeds and [tclOR t1 t2 = t2] if t1 fails. - No interleaving for the moment. *) -(* spiwack: compared to the LogicT paper, we backtrack at the same state - where [t1] has been called, not the state where [t1] failed. *) -let tclOR t1 t2 env = { go = fun sk fk step -> - (t1 env).go sk (fun _ _ -> (t2 env).go sk fk step) step -} - -(* [tclZERO e] always fails with error message [e]*) -let tclZERO e env = { go = fun _ fk step -> fk e step } +let tclIGNORE tac env = Inner.ignore (tac env) +(* [tclOR t1 t2 = t1] as long as [t1] succeeds. Whenever the successes + of [t1] have been depleted, then it behaves as [t2]. No + interleaving at this point. *) +let tclOR t1 t2 env = + Inner.plus (t1 env) (t2 env) -(* Focusing operation on proof_steps. *) -let focus_proof_step i j ps = - let (new_subgoals, context) = focus_sublist i j ps.goals in - ( { ps with goals = new_subgoals } , context ) +(* [tclZERO e] always fails with error message [e]*) +let tclZERO e _ = Inner.zero e -(* Unfocusing operation of proof_steps. *) -let unfocus_proof_step c ps = - { ps with - goals = undefined ps.defs (unfocus_sublist c ps.goals) - } +(* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once + or [t2] if [t1] fails. *) +let tclORELSE t1 t2 env = + (* spiwack: convenience notations, waiting for ocaml 3.12 *) + let (>>=) = Inner.bind in + Inner.split (t1 env) >>= function + | Util.Inr _ -> t2 env + | Util.Inl (a,t1') -> Inner.plus (Inner.return a) t1' (* Focuses a tactic at a range of subgoals, found by their indices. *) (* arnaud: bug if 0 goals ! *) -let tclFOCUS i j t env = { go = fun sk fk step -> - let (focused,context) = focus_proof_step i j step in - (t env).go (fun a fk step -> sk a fk (unfocus_proof_step context step)) fk focused -} +let tclFOCUS i j t env = + (* spiwack: convenience notations, waiting for ocaml 3.12 *) + let (>>=) = Inner.bind in + let (>>) = Inner.seq in + Inner.get >>= fun initial -> + let (focused,context) = focus i j initial in + Inner.set focused >> + t (env) >>= fun result -> + Inner.get >>= fun next -> + Inner.set (unfocus context next) >> + Inner.return result (* Dispatch tacticals are used to apply a different tactic to each goal under consideration. They come in two flavours: @@ -292,111 +266,67 @@ end the return value at two given lists of subgoals are combined when both lists are being concatenated. [join] and [null] need be some sort of comutative monoid. *) -let rec tclDISPATCHGEN null join tacs env = { go = fun sk fk step -> - match tacs,step.goals with - | [] , [] -> (tclUNIT null env).go sk fk step - | t::tacs , first::goals -> - (tclDISPATCHGEN null join tacs env).go - begin fun x fk step -> - match Goal.advance step.defs first with - | None -> sk x fk step - | Some first -> - (t env).go - begin fun y fk step' -> - sk (join x y) fk { step' with - goals = step'.goals@step.goals - } - end - fk - { step with goals = [first] } - end - fk - { step with goals = goals } - | _ -> raise SizeMismatch -} - -(* takes a tactic which can raise exception and makes it pure by *failing* - on with these exceptions. Does not catch anomalies. *) -let purify t = - let t' env = { go = fun sk fk step -> try (t env).go (fun x -> sk (Util.Inl x)) fk step - with Errors.Anomaly _ as e -> raise e - | e -> sk (Util.Inr e) fk step - } - in - tclBIND t' begin function - | Util.Inl x -> tclUNIT x - | Util.Inr e -> tclZERO e - end -let tclDISPATCHGEN null join tacs = purify (tclDISPATCHGEN null join tacs) +let rec tclDISPATCHGEN null join tacs env = + (* spiwack: convenience notations, waiting for ocaml 3.12 *) + let (>>=) = Inner.bind in + let (>>) = Inner.seq in + Inner.get >>= fun initial -> + match tacs,initial.comb with + | [], [] -> tclUNIT null env + | t::tacs , first::goals -> + Inner.set {initial with comb=goals} >> + tclDISPATCHGEN null join tacs env >>= fun x -> + Inner.get >>= fun step -> + begin match Goal.advance step.solution first with + | None -> Inner.return x (* If [first] has been solved by side effect: do nothing. *) + | Some first -> + Inner.set {step with comb=[first]} >> + t env >>= fun y -> + Inner.get >>= fun step' -> + Inner.set {step' with comb=step'.comb@step.comb} >> + Inner.return (join x y) + end + | _ , _ -> raise SizeMismatch let unitK () () = () let tclDISPATCH = tclDISPATCHGEN () unitK -let extend_to_list = - let rec copy n x l = - if n < 0 then raise SizeMismatch - else if n = 0 then l - else copy (n-1) x (x::l) - in - fun startxs rx endxs l -> - let ns = List.length startxs in - let ne = List.length endxs in - let n = List.length l in - startxs@(copy (n-ne-ns) rx endxs) -let tclEXTEND tacs1 rtac tacs2 env = { go = fun sk fk step -> - let tacs = extend_to_list tacs1 rtac tacs2 step.goals in - (tclDISPATCH tacs env).go sk fk step -} - -(* [tclGOALBIND] and [tclGOALBINDU] are sorts of bind which take a - [Goal.sensitive] as a first argument, the tactic then acts on each goal separately. - Allows backtracking between goals. *) -let list_of_sensitive s k env step = - Goal.list_map begin fun defs g -> - let (a,defs) = Goal.eval s env defs g in - (k a) , defs - end step.goals step.defs -(* In form of a tactic *) -let list_of_sensitive s k env = { go = fun sk fk step -> - let (tacs,defs) = list_of_sensitive s k env step in - sk tacs fk { step with defs = defs } -} - (* This is a helper function for the dispatching tactics (like [tclGOALBIND] and [tclDISPATCHS]). It takes an ['a sensitive] value, and returns a tactic whose return value is, again, ['a sensitive] but only has value in the (unmodified) goals under focus. *) -let here_s b env = { go = fun sk fk step -> - sk (Goal.bind (Goal.here_list step.goals b) (fun b -> b)) fk step -} +let here_s b env = + (* spiwack: convenience notations, waiting for ocaml 3.12 *) + let (>>=) = Inner.bind in + Inner.get >>= fun step -> + Inner.return (Goal.bind (Goal.here_list step.comb b) (fun b -> b)) -let rec tclGOALBIND s k = - (* spiwack: the first line ensures that the value returned by the tactic [k] will - not "escape its scope". *) - let k a = tclBIND (k a) here_s in - purify begin - tclBIND (list_of_sensitive s k) begin fun tacs -> - tclDISPATCHGEN Goal.null Goal.plus tacs - end - end - -(* spiwack: this should probably be moved closer to the [tclDISPATCH] tactical. *) +(* see .mli for documentation. *) let tclDISPATCHS tacs = let tacs = List.map begin fun tac -> tclBIND tac here_s end tacs in - purify begin - tclDISPATCHGEN Goal.null Goal.plus tacs - end + tclDISPATCHGEN Goal.null Goal.plus tacs -let rec tclGOALBINDU s k = - purify begin - tclBIND (list_of_sensitive s k) begin fun tacs -> - tclDISPATCHGEN () unitK tacs - end - end +let extend_to_list = + let rec copy n x l = + if n < 0 then raise SizeMismatch + else if n = 0 then l + else copy (n-1) x (x::l) + in + fun startxs rx endxs l -> + let ns = List.length startxs in + let ne = List.length endxs in + let n = List.length l in + startxs@(copy (n-ne-ns) rx endxs) +let tclEXTEND tacs1 rtac tacs2 env = + (* spiwack: convenience notations, waiting for ocaml 3.12 *) + let (>>=) = Inner.bind in + Inner.get >>= fun step -> + let tacs = extend_to_list tacs1 rtac tacs2 step.comb in + tclDISPATCH tacs env (* spiwack: up to a few details, same errors are in the Logic module. this should be maintained synchronized, probably. *) @@ -416,9 +346,48 @@ let rec catchable_exception = function (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true | _ -> false + +(* [tclGOALBIND] and [tclGOALBINDU] are sorts of bind which take a + [Goal.sensitive] as a first argument, the tactic then acts on each goal separately. + Allows backtracking between goals. *) + +(* [list_of_sensitive s k] where [s] is and ['a Goal.sensitive] [k] + has type ['a -> 'b] returns the list of ['b] obtained by evualating + [s] to each goal successively and applying [k] to each result. *) +let list_of_sensitive s k env step = + Goal.list_map begin fun defs g -> + let (a,defs) = Goal.eval s env defs g in + (k a) , defs + end step.comb step.solution +(* In form of a tactic *) +let list_of_sensitive s k env = + (* spiwack: convenience notations, waiting for ocaml 3.12 *) + let (>>=) = Inner.bind in + let (>>) = Inner.seq in + Inner.get >>= fun step -> + try + let (tacs,defs) = list_of_sensitive s k env step in + Inner.set { step with solution = defs } >> + Inner.return tacs + with e when catchable_exception e -> + tclZERO e env + +let rec tclGOALBIND s k = + (* spiwack: the first line ensures that the value returned by the tactic [k] will + not "escape its scope". *) + let k a = tclBIND (k a) here_s in + tclBIND (list_of_sensitive s k) begin fun tacs -> + tclDISPATCHGEN Goal.null Goal.plus tacs + end + +let rec tclGOALBINDU s k = + tclBIND (list_of_sensitive s k) begin fun tacs -> + tclDISPATCHGEN () unitK tacs + end + (* No backtracking can happen here, hence, as opposed to the dispatch tacticals, everything is done in one step. *) -let sensitive_on_step s env step = +let sensitive_on_proofview s env step = let wrap g ((defs, partial_list) as partial_res) = match Goal.advance defs g with | None ->partial_res @@ -427,14 +396,20 @@ let sensitive_on_step s env step = (d',sg::partial_list) in let ( new_defs , combed_subgoals ) = - List.fold_right wrap step.goals (step.defs,[]) + List.fold_right wrap step.comb (step.solution,[]) in - { defs = new_defs; - goals = List.flatten combed_subgoals } -let tclSENSITIVE s = - purify begin - fun env -> { go = fun sk fk step -> sk () fk (sensitive_on_step s env step) } - end + { step with + solution = new_defs; + comb = List.flatten combed_subgoals } +let tclSENSITIVE s env = + (* spiwack: convenience notations, waiting for ocaml 3.12 *) + let (>>=) = Inner.bind in + Inner.get >>= fun step -> + try + let next = sensitive_on_proofview s env step in + Inner.set next + with e when catchable_exception e -> + tclZERO e env (*** Commands ***) @@ -457,23 +432,28 @@ end module V82 = struct type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma - let tactic tac _ = { go = fun sk fk ps -> + let tactic tac env = (* spiwack: we ignore the dependencies between goals here, expectingly - preserving the semantics of <= 8.2 tactics *) - let tac evd gl = - let glsigma = tac { Evd.it = gl ; Evd.sigma = evd } in - let sigma = glsigma.Evd.sigma in - let g = glsigma.Evd.it in - ( g , sigma ) - in + preserving the semantics of <= 8.2 tactics *) + (* spiwack: convenience notations, waiting for ocaml 3.12 *) + let (>>=) = Inner.bind in + Inner.get >>= fun ps -> + try + let tac evd gl = + let glsigma = tac { Evd.it = gl ; Evd.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) = - Goal.list_map Goal.V82.nf_evar ps.goals ps.defs - in - let (goalss,evd) = Goal.list_map tac initgoals initevd in - let sgs = List.flatten goalss in - sk () fk { defs = evd ; goals = sgs } -} + let (initgoals,initevd) = + Goal.list_map Goal.V82.nf_evar ps.comb ps.solution + in + let (goalss,evd) = Goal.list_map tac initgoals initevd in + let sgs = List.flatten goalss in + Inner.set { ps with solution=evd ; comb=sgs } + with e when catchable_exception e -> + tclZERO e env let has_unresolved_evar pv = Evd.has_undefined pv.solution @@ -517,5 +497,4 @@ module V82 = struct { pv with solution = Evar_refiner.instantiate_pf_com evk com pv.solution } - let purify = purify end diff --git a/proofs/proofview.mli b/proofs/proofview.mli index d9cc43e50..ade8be1a3 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -134,13 +134,18 @@ val tclTHEN : unit tactic -> 'a tactic -> 'a tactic but drops the value at the end. *) val tclIGNORE : 'a tactic -> unit tactic -(* [tclOR t1 t2 = t1] if t1 succeeds and [tclOR t1 t2 = t2] if t2 fails. - No interleaving at this point. *) +(* [tclOR t1 t2 = t1] as long as [t1] succeeds. Whenever the successes + of [t1] have been depleted, then it behaves as [t2]. No + interleaving at this point. *) val tclOR : 'a tactic -> 'a tactic -> 'a tactic (* [tclZERO] always fails *) val tclZERO : exn -> 'a tactic +(* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once + or [t2] if [t1] fails. *) +val tclORELSE : 'a tactic -> 'a tactic -> 'a tactic + (* Focuses a tactic at a range of subgoals, found by their indices. *) val tclFOCUS : int -> int -> 'a tactic -> 'a tactic @@ -229,8 +234,4 @@ module V82 : sig (* Implements the Existential command *) val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview - - (* spiwack: [purify] might be useful while writing tactics manipulating exception - explicitely or from the [V82] submodule (neither being advised, though *) - val purify : 'a tactic -> 'a tactic end |