diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/monads.ml | 496 | ||||
| -rw-r--r-- | proofs/proof_errors.ml | 12 | ||||
| -rw-r--r-- | proofs/proof_errors.mli | 18 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 4 | ||||
| -rw-r--r-- | proofs/proofview.ml | 196 | ||||
| -rw-r--r-- | proofs/proofview.mli | 7 | ||||
| -rw-r--r-- | proofs/proofview_gen.ml | 377 | ||||
| -rw-r--r-- | proofs/proofview_monad.ml | 1 | ||||
| -rw-r--r-- | proofs/proofview_monad.mli | 81 |
9 files changed, 600 insertions, 592 deletions
diff --git a/proofs/monads.ml b/proofs/monads.ml deleted file mode 100644 index 803715a450..0000000000 --- a/proofs/monads.ml +++ /dev/null @@ -1,496 +0,0 @@ -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 type Writer = sig - type m (* type of the messages *) - include S - - val put : m -> unit t -end - -module type IO = sig - include S - - type 'a ref - - val ref : 'a -> 'a ref t - val (:=) : 'a ref -> 'a -> unit t - val (!) : 'a ref -> 'a t - - val raise : exn -> 'a t - val catch : 'a t -> (exn -> 'a t) -> 'a t - - (** In the basic IO monad, [timeout n x] acts as [x] unless it runs for more than [n] - seconds in which case it raises [IO.Timeout]. *) - val timeout : int -> 'a t -> 'a t -end - -module IO : sig - include IO - - (** To help distinguish between exceptions raised by the [IO] monad - from the one used natively by Coq, the former are wrapped in - [Exception]. *) - exception Exception of exn - (** This exception is used to signal abortion in [timeout] functions. *) - exception Timeout - (** runs the suspension for its effects *) - val run : 'a t -> 'a -end = struct - type 'a t = unit -> 'a - - let run x = x () - - let return x () = x - let bind x k () = k (x ()) () - let seq x k () = x (); k () - let ignore x () = ignore (x ()) - - type 'a ref = 'a Pervasives.ref - - let ref x () = Pervasives.ref x - let (:=) r x () = Pervasives.(:=) r x - let (!) r () = Pervasives.(!) r - - exception Exception of exn - let raise e () = raise (Exception e) - let catch s h () = - try s () - with Exception e -> h e () - - exception Timeout - let timeout n t () = - let timeout_handler _ = Pervasives.raise (Exception Timeout) in - let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in - Pervasives.ignore (Unix.alarm n); - let restore_timeout () = - Pervasives.ignore (Unix.alarm 0); - Sys.set_signal Sys.sigalrm psh - in - try - let res = t () in - restore_timeout (); - res - with - | e -> restore_timeout (); Pervasives.raise e - - let _ = Errors.register_handler begin function - | Timeout -> Errors.errorlabstrm "Monads.IO.timeout" (Pp.str"Timeout!") - | Exception e -> Errors.print e - | _ -> Pervasives.raise Errors.Unhandled - end -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 - -module type Monoid = sig - type t - - val zero : t - val ( * ) : t -> t -> t -end - -module Writer (M:Monoid) (T:S) : sig - include Writer with type +'a t = private ('a*M.t) T.t and type m = M.t - - val lift : 'a T.t -> 'a t - (* The coercion from private ['a t] in function form. *) - val run : 'a t -> ('a*m) T.t -end = struct - - type 'a t = ('a*M.t) T.t - type m = M.t - - let run x = x - - (*spiwack: convenience notation, waiting for ocaml 3.12 *) - let (>>=) = T.bind - - let bind x k = - x >>= fun (a,m) -> - k a >>= fun (r,m') -> - T.return (r,M.( * ) m m') - - let seq x k = - x >>= fun ((),m) -> - k >>= fun (r,m') -> - T.return (r,M.( * ) m m') - - let return x = - T.return (x,M.zero) - - let ignore x = - x >>= fun (_,m) -> - T.return ((),m) - - let lift x = - x >>= fun r -> - T.return (r,M.zero) - - let put m = - T.return ((),m) -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 - principles can be found in "Kan Extensions for Program - Optimisation" by Ralf Hinze. - - One way to think of the [Logic] functor is to imagine ['a - Logic(X).t] to represent list of ['a] with an exception at the - bottom (leaving the monad-transforming issues aside, as they don't - really work well with lists). Each of the element is a valid - result, sequentialising with a [f:'a -> 'b t] is done by applying - [f] to each element and then flatten the list, [plus] is - concatenation, and [split] is pattern-matching. *) -(* spiwack: I added the primitives from [IO] directly in the [Logic] - signature for convenience. It doesn't really make sense, strictly - speaking, as they are somewhat deconnected from the semantics of - [Logic], but without an appropriate language for composition (some - kind of mixins?) I would be going nowhere with a gazillion - functors. *) -module type Logic = sig - include IO - - (* [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 -> (exn -> 'a t) -> 'a t -(** Writing (+) for plus and (>>=) for bind, we shall require that - - x+(y+z) = (x+y)+z - - 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 * (exn -> '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:IO) : 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 } - - let plus x y = { go = fun sk fk -> - x.go sk (fun e -> (y e).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*(exn -> 'a t) , exn) Util.union -> 'a t = function - | Util.Inr e -> zero e - | Util.Inl (a,x) -> plus (return a) x - - let lower x = - let fk e = T.return (Util.Inr e) in - let sk a fk = T.return (Util.Inl (a,fun e -> bind (lift (fk e)) reflect)) in - x.go sk fk - - let split x = - lift (lower x) - - (*** IO ***) - - type 'a ref = 'a T.ref - let ref x = lift (T.ref x) - let (:=) r x = lift (T.(:=) r x) - let (!) r = lift (T.(!) r) - - let raise e = lift (T.raise e) - let catch t h = - let h' e = lower (h e) in - bind (lift (T.catch (lower t) h')) reflect - - (** [timeout n x] can have several success. It succeeds as long as, - individually, each of the past successes run in less than [n] - seconds. - In case of timeout if fails with [zero Timeout]. *) - let rec timeout n x = - (* spiwack: adds a [T.return] in front of [x] in order to force - [lower] to go into [T] before running [x]. The problem is that - in a continuation-passing monad transformer, the monadic - operations don't make use of the underlying ones. Hence, when - going back to a lower monad, much computation can be done - before returning (and running the lower monad). It is - undesirable for timeout, obviously. *) - let x = seq (lift (T.return ())) x in - let x' = - (* spiwack: this could be a [T.map] if provided *) - T.bind (lower x) begin function - | Util.Inr _ as e -> T.return e - | Util.Inl (a,h) -> T.return (Util.Inl (a, fun e -> timeout n (h e))) - end - in - (* spiwack: we report timeouts as resumable failures. *) - bind (catch (lift (T.timeout n x')) begin function - | IO.Timeout -> zero IO.Timeout - | e -> raise e - end) reflect -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 lift : 'a T.t -> 'a 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) (fun e -> run (y e) 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' e = - lift (y e) >>= fun b -> - set b.state >> - return b.result - in - set a.state >> - return (Util.Inl(a.result,y')) - - - (*** IO ***) - - type 'a ref = 'a T.ref - let ref x = lift (T.ref x) - let (:=) r x = lift (T.(:=) r x) - let (!) r = lift (T.(!) r) - - let raise e = lift (T.raise e) - let catch t h = - (* spiwack: convenience notation, waiting for ocaml 3.12 *) - let (>>=) = bind in - let (>>) = seq in - get >>= fun initial -> - let h' e = run (h e) initial in - lift (T.catch (run t initial) h') >>= fun a -> - set a.state >> - return a.result - - exception Timeout - let timeout n t = - (* spiwack: convenience notation, waiting for ocaml 3.12 *) - let (>>=) = bind in - let (>>) = seq in - get >>= fun initial -> - lift (T.timeout n (run t initial)) >>= fun a -> - set a.state >> - return a.result -end - -(* [Writer(M)(T:Logic)] can be lifted to [Logic] by backtracking on state on [plus].*) -module WriterLogic(M:Monoid)(T:Logic) : sig - (* spiwack: some duplication from interfaces as we need ocaml 3.12 - to substitute inside signatures. *) - type m = M.t - include Logic with type +'a t = private ('a*m) T.t - - val put : m -> unit t - - val lift : 'a T.t -> 'a t - val run : 'a t -> ('a*m) T.t -end = struct - module W = Writer(M)(T) - include W - - 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 - lift begin - (T.plus (run x) (fun e -> run (y e))) - end >>= fun (r,m) -> - put m >> - return r - - let split x = - (* spiwack: convenience notation, waiting for ocaml 3.12 *) - let (>>=) = bind in - let (>>) = seq in - lift (T.split (run x)) >>= function - | Util.Inr _ as e -> return e - | Util.Inl ((a,m),y) -> - let y' e = - lift (y e) >>= fun (b,m) -> - put m >> - return b - in - put m >> - return (Util.Inl(a,y')) - - - (*** IO ***) - - type 'a ref = 'a T.ref - let ref x = lift (T.ref x) - let (:=) r x = lift (T.(:=) r x) - let (!) r = lift (T.(!) r) - - let raise e = lift (T.raise e) - let catch t h = - (* spiwack: convenience notation, waiting for ocaml 3.12 *) - let (>>=) = bind in - let (>>) = seq in - let h' e = run (h e) in - lift (T.catch (run t) h') >>= fun (a,m) -> - put m >> - return a - - exception Timeout - let timeout n t = - (* spiwack: convenience notation, waiting for ocaml 3.12 *) - let (>>=) = bind in - let (>>) = seq in - lift (T.timeout n (run t)) >>= fun (a,m) -> - put m >> - return a -end diff --git a/proofs/proof_errors.ml b/proofs/proof_errors.ml new file mode 100644 index 0000000000..e543b0c8fd --- /dev/null +++ b/proofs/proof_errors.ml @@ -0,0 +1,12 @@ +exception Exception of exn +exception Timeout +exception TacticFailure of exn + +let _ = Errors.register_handler begin function + | Timeout -> Errors.errorlabstrm "Some timeout function" (Pp.str"Timeout!") + | Exception e -> Errors.print e + | TacticFailure e -> Errors.print e + | _ -> Pervasives.raise Errors.Unhandled +end + + diff --git a/proofs/proof_errors.mli b/proofs/proof_errors.mli new file mode 100644 index 0000000000..dd21d539c9 --- /dev/null +++ b/proofs/proof_errors.mli @@ -0,0 +1,18 @@ +(** This small files declares the exceptions needed by Proofview_gen, + as Coq's extraction cannot produce exception declarations. *) + +(** To help distinguish between exceptions raised by the IO monad from + the one used natively by Coq, the former are wrapped in + [Exception]. It is only used internally so that [catch] blocks of + the IO monad would only catch exceptions raised by the [raise] + function of the IO monad, and not for instance, by system + interrupts. Also used in [Proofview] to avoid capturing exception + from the IO monad ([Proofview] catches errors in its compatibility + layer, and when lifting goal-level expressions). *) +exception Exception of exn +(** This exception is used to signal abortion in [timeout] functions. *) +exception Timeout +(** This exception is used by the tactics to signal failure by lack of + successes, rather than some other exceptions (like system + interrupts). *) +exception TacticFailure of exn diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 19f289316f..4a7efb029c 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,7 +1,9 @@ Goal Evar_refiner -Monads Proof_type +Proof_errors +Proofview_gen +Proofview_monad Proofview Proof Proof_global diff --git a/proofs/proofview.ml b/proofs/proofview.ml index eed792fd7f..9496b51ea8 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -23,11 +23,8 @@ open Util (* Type of proofviews. *) -type proofview = { - initial : (Term.constr * Term.types) list; - solution : Evd.evar_map; - comb : Goal.goal list; - } +type proofview = Proofview_monad.proofview +open Proofview_monad let proofview p = p.comb , p.solution @@ -188,79 +185,68 @@ let unfocus c sp = - 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 ProofState = struct - type t = proofview -end -module MessageType = struct - type t = bool (* [false] if an unsafe tactic has been used. *) - - let zero = true - let ( * ) s1 s2 = s1 && s2 -end -module Backtrack = Monads.Logic(Monads.IO) -module Message = Monads.WriterLogic(MessageType)(Backtrack) -module Proof = Monads.StateLogic(ProofState)(Message) - -type +'a tactic = Environ.env -> 'a Proof.t +module Proof = Proofview_monad.Logical +type +'a tactic = 'a Proof.t (* Applies a tactic to the current proofview. *) let apply env t sp = - let (next,status) = Monads.IO.run (Backtrack.run (Message.run (Proof.run (t env) sp))) in - next.Proof.result , next.Proof.state , status + let (((next_r,next_state),status)) = Proofview_monad.NonLogical.run (Proof.run t env sp) in + next_r , next_state , status (*** tacticals ***) +let rec catchable_exception = function + | Proof_errors.Exception _ -> false + | e -> Errors.noncritical e + + (* Unit of the tactic monad *) -let tclUNIT a _ = Proof.return a +let tclUNIT a = (Proof.ret a:'a Proof.t) (* Bind operation of the tactic monad *) -let tclBIND t k env = - Proof.bind (t env) (fun a -> k a env) +let tclBIND = Proof.bind (* 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 = - Proof.seq (t1 env) (t2 env) +let tclTHEN = Proof.seq (* [tclIGNORE t] has the same operational content as [t], but drops the value at the end. *) -let tclIGNORE tac env = Proof.ignore (tac env) +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 t1 t2 env = - Proof.plus (t1 env) (fun e -> t2 e env) +let tclOR t1 t2 = + Proof.plus t1 t2 (* [tclZERO e] always fails with error message [e]*) -let tclZERO e _ = Proof.zero e +let tclZERO = Proof.zero (* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once or [t2] if [t1] fails. *) -let tclORELSE t1 t2 env = +let tclORELSE t1 t2 = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in - Proof.split (t1 env) >>= function - | Util.Inr e -> t2 e env - | Util.Inl (a,t1') -> Proof.plus (Proof.return a) t1' + Proof.split t1 >>= function + | Util.Inr e -> t2 e + | Util.Inl (a,t1') -> Proof.plus (Proof.ret 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 env = +let tclIFCATCH a s f = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in - Proof.split (a env) >>= function - | Util.Inr e -> f e env - | Util.Inl (x,a') -> Proof.plus (s x env) (fun e -> (a' e) >>= fun x' -> (s x' env)) + Proof.split a >>= function + | Util.Inr e -> f e + | Util.Inl (x,a') -> Proof.plus (s x) (fun e -> (a' e) >>= fun x' -> (s x')) (* Focuses a tactic at a range of subgoals, found by their indices. *) (* arnaud: bug if 0 goals ! *) -let tclFOCUS i j t env = +let tclFOCUS i j t = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in let (>>) = Proof.seq in @@ -268,14 +254,14 @@ let tclFOCUS i j t env = try let (focused,context) = focus i j initial in Proof.set focused >> - t (env) >>= fun result -> + t >>= fun result -> Proof.get >>= fun next -> Proof.set (unfocus context next) >> - Proof.return result + Proof.ret result with e -> (* spiwack: a priori the only possible exceptions are that of focus, of course I haven't made them algebraic yet. *) - tclZERO e env + tclZERO e (* Dispatch tacticals are used to apply a different tactic to each goal under consideration. They come in two flavours: @@ -299,27 +285,27 @@ end both lists are being concatenated. [join] and [null] need be some sort of comutative monoid. *) -let rec tclDISPATCHGEN null join tacs env = +let rec tclDISPATCHGEN null join tacs = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in let (>>) = Proof.seq in Proof.get >>= fun initial -> match tacs,initial.comb with - | [], [] -> tclUNIT null env + | [], [] -> tclUNIT null | t::tacs , first::goals -> begin match Goal.advance initial.solution first with - | None -> Proof.return null (* If [first] has been solved by side effect: do nothing. *) + | None -> Proof.ret null (* If [first] has been solved by side effect: do nothing. *) | Some first -> Proof.set {initial with comb=[first]} >> - t env + t end >>= fun y -> Proof.get >>= fun step -> Proof.set {step with comb=goals} >> - tclDISPATCHGEN null join tacs env >>= fun x -> + tclDISPATCHGEN null join tacs >>= fun x -> Proof.get >>= fun step' -> Proof.set {step' with comb=step.comb@step'.comb} >> - Proof.return (join y x) - | _ , _ -> tclZERO SizeMismatch env + Proof.ret (join y x) + | _ , _ -> tclZERO SizeMismatch let unitK () () = () let tclDISPATCH = tclDISPATCHGEN () unitK @@ -343,12 +329,12 @@ let extend_to_list = 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 = +let tclEXTEND tacs1 rtac tacs2 = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in Proof.get >>= fun step -> let tacs = extend_to_list tacs1 rtac tacs2 step.comb in - tclDISPATCH tacs env + tclDISPATCH tacs (* No backtracking can happen here, hence, as opposed to the dispatch tacticals, @@ -367,44 +353,79 @@ let sensitive_on_proofview s env step = { step with solution = new_defs; comb = List.flatten combed_subgoals; } - let tclSENSITIVE s env = +let tclSENSITIVE s = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in + Proof.current >>= fun env -> Proof.get >>= fun step -> try let next = sensitive_on_proofview s env step in Proof.set next - with e when Errors.noncritical e -> - tclZERO e env + with e when catchable_exception e -> + tclZERO e -let tclPROGRESS t env = +let tclPROGRESS t = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in Proof.get >>= fun initial -> - t env >>= fun res -> + t >>= fun res -> Proof.get >>= fun final -> let test = Evd.progress_evar_map initial.solution final.solution && not (Util.List.for_all2eq (fun i f -> Goal.equal initial.solution i final.solution f) initial.comb final.comb) in if test then - tclUNIT res env + tclUNIT res else - tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) env + tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) -let tclEVARMAP _ = +let tclEVARMAP = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in Proof.get >>= fun initial -> - Proof.return (initial.solution) + Proof.ret (initial.solution) -let tclENV env = - Proof.return env +let tclENV = Proof.current -let tclTIMEOUT n t env = Proof.timeout n (t env) +exception Timeout +let _ = Errors.register_handler begin function + | Timeout -> Errors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | _ -> Pervasives.raise Errors.Unhandled +end -let mark_as_unsafe env = - Proof.lift (Message.put false) +let tclTIMEOUT n t = + (* spiwack: convenience notations, waiting for ocaml 3.12 *) + let (>>=) = Proof.bind in + let (>>) = Proof.seq 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 (Proofview_monad.NonLogical.ret ()) >> t in + Proof.current >>= fun env -> + Proof.get >>= fun initial -> + Proof.lift begin + Proofview_monad.NonLogical.catch + begin + Proofview_monad.NonLogical.bind + (Proofview_monad.NonLogical.timeout n (Proof.run t env initial)) + (fun r -> Proofview_monad.NonLogical.ret (Util.Inl r)) + end + begin function + | Proof_errors.Timeout -> Proofview_monad.NonLogical.ret (Util.Inr Timeout) + | Proof_errors.TacticFailure e -> Proofview_monad.NonLogical.ret (Util.Inr e) + | e -> Proofview_monad.NonLogical.raise e + end + end >>= function + | Util.Inl ((res,s),m) -> + Proof.set s >> + Proof.put m >> + Proof.ret res + | Util.Inr e -> tclZERO e + +let mark_as_unsafe = + Proof.put false (*** Commands ***) @@ -430,7 +451,7 @@ module Notations = struct end >= fun l' -> tclUNIT (List.flatten l') let (<*>) = tclTHEN - let (<+>) t1 t2 = tclOR t2 (fun _ -> t2) + let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) end open Notations @@ -446,7 +467,7 @@ let rec list_map f = function module V82 = struct type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma - let tactic tac env = + 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 *) @@ -467,8 +488,8 @@ module V82 = struct let (goalss,evd) = Goal.list_map tac initgoals initevd in let sgs = List.flatten goalss in Proof.set { ps with solution=evd ; comb=sgs; } - with e when Errors.noncritical e -> - tclZERO e env + with e when catchable_exception e -> + tclZERO e let has_unresolved_evar pv = Evd.has_undefined pv.solution @@ -515,14 +536,16 @@ module V82 = struct solution = Evar_refiner.instantiate_pf_com evk com pv.solution } let of_tactic t gls = - let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] ; initial = [] } in - let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in - { Evd.sigma = final.solution ; it = final.comb } + try + let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] ; initial = [] } in + let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in + { Evd.sigma = final.solution ; it = final.comb } + with Proof_errors.TacticFailure e -> raise e - let put_status b _env = - Proof.lift (Message.put b) + let put_status b = + Proof.put b - let catchable_exception = Errors.noncritical + let catchable_exception = catchable_exception end @@ -530,10 +553,11 @@ module Goal = struct type 'a u = 'a list - let lift s env = + let lift s = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in let (>>) = Proof.seq in + Proof.current >>= fun env -> Proof.get >>= fun step -> try let (res,sigma) = @@ -542,22 +566,12 @@ module Goal = struct end step.comb step.solution in Proof.set { step with solution=sigma } >> - Proof.return res - with e when Errors.noncritical e -> - tclZERO e env + Proof.ret res + with e when catchable_exception e -> + tclZERO e let return x = lift (Goal.return x) let concl = lift Goal.concl let hyps = lift Goal.hyps let env = lift Goal.env end - - - - - - - - - - diff --git a/proofs/proofview.mli b/proofs/proofview.mli index a2a5746933..136a44332e 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -194,10 +194,9 @@ val tclEVARMAP : Evd.evar_map tactic environment is returned by {!Proofview.Goal.env}. *) val tclENV : Environ.env tactic -(** [tclTIMEOUT n t] can have several success. It succeeds as long as, - individually, each of the past successes run in less than [n] - seconds. - In case of timeout if fails with [tclZERO Timeout]. *) +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 (** [mark_as_unsafe] signals that the current tactic is unsafe. *) diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml new file mode 100644 index 0000000000..577aa2ddb0 --- /dev/null +++ b/proofs/proofview_gen.ml @@ -0,0 +1,377 @@ +(* This file has been generated by extraction + of bootstrap/Monad.v. It shouldn't be + modified directly. To regenerate it run + coqtop -batch -impredicative-set + bootstrap/Monad.v in Coq's source + directory. *) + +type __ = Obj.t +let __ = let rec f _ = Obj.repr f in Obj.repr f + +module IOBase = + struct + type 'a coq_T = unit -> 'a + + type 'a coq_Ref = 'a Pervasives.ref + + (** val ret : 'a1 -> 'a1 coq_T **) + + let ret = fun a () -> a + + (** val bind : + 'a1 coq_T -> ('a1 -> 'a2 coq_T) -> 'a2 + coq_T **) + + let bind = fun a k () -> k (a ()) () + + (** val ignore : + 'a1 coq_T -> unit coq_T **) + + let ignore = fun a () -> ignore (a ()) + + (** val seq : + unit coq_T -> 'a1 coq_T -> 'a1 coq_T **) + + let seq = fun a k () -> a (); k () + + (** val ref : 'a1 -> 'a1 coq_Ref coq_T **) + + let ref = fun a () -> Pervasives.ref a + + (** val set : + 'a1 coq_Ref -> 'a1 -> unit coq_T **) + + let set = fun r a () -> Pervasives.(:=) r a + + (** val get : 'a1 coq_Ref -> 'a1 coq_T **) + + let get = fun r () -> Pervasives.(!) r + + (** val raise : exn -> 'a1 coq_T **) + + let raise = fun e () -> raise (Proof_errors.Exception e) + + (** val catch : + 'a1 coq_T -> (exn -> 'a1 coq_T) -> 'a1 + coq_T **) + + let catch = fun s h () -> try s () with Proof_errors.Exception e -> h e () + + type coq_Int = int + + (** val timeout : + coq_Int -> 'a1 coq_T -> 'a1 coq_T **) + + let timeout = fun n t () -> + let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in + let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in + Pervasives.ignore (Unix.alarm n); + let restore_timeout () = + Pervasives.ignore (Unix.alarm 0); + Sys.set_signal Sys.sigalrm psh + in + try + let res = t () in + restore_timeout (); + res + with + | e -> restore_timeout (); Pervasives.raise e + + end + +type proofview = { initial : (Term.constr*Term.types) + list; + solution : Evd.evar_map; + comb : Goal.goal list } + +type logicalState = proofview + +type logicalMessageType = bool + +type logicalEnvironment = Environ.env + +module NonLogical = + struct + type 'a t = 'a IOBase.coq_T + + type 'a ref = 'a IOBase.coq_Ref + + (** val ret : 'a1 -> 'a1 t **) + + let ret x = + IOBase.ret x + + (** val bind : + 'a1 t -> ('a1 -> 'a2 t) -> 'a2 t **) + + let bind x k = + IOBase.bind x k + + (** val ignore : 'a1 t -> unit t **) + + let ignore x = + IOBase.ignore x + + (** val seq : unit t -> 'a1 t -> 'a1 t **) + + let seq x k = + IOBase.seq x k + + (** val new_ref : 'a1 -> 'a1 ref t **) + + let new_ref x = + IOBase.ref x + + (** val set : 'a1 ref -> 'a1 -> unit t **) + + let set r x = + IOBase.set r x + + (** val get : 'a1 ref -> 'a1 t **) + + let get r = + IOBase.get r + + (** val raise : exn -> 'a1 t **) + + let raise e = + IOBase.raise e + + (** val catch : + 'a1 t -> (exn -> 'a1 t) -> 'a1 t **) + + let catch s h = + IOBase.catch s h + + (** val timeout : + IOBase.coq_Int -> 'a1 t -> 'a1 t **) + + let timeout n x = + IOBase.timeout n x + + (** val run : 'a1 t -> 'a1 **) + + let run = fun x -> try x () with Proof_errors.Exception e -> Pervasives.raise e + end + +module Logical = + struct + type 'a t = + proofview -> Environ.env -> __ -> + ((('a*proofview)*bool) -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn + -> __ IOBase.coq_T) -> __ IOBase.coq_T + + (** val ret : + 'a1 -> proofview -> Environ.env -> __ + -> ((('a1*proofview)*bool) -> (exn -> + 'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T) + -> (exn -> 'a2 IOBase.coq_T) -> 'a2 + IOBase.coq_T **) + + let ret x s e r sk fk = + sk ((x,s),true) fk + + (** val bind : + 'a1 t -> ('a1 -> 'a2 t) -> proofview -> + Environ.env -> __ -> + ((('a2*proofview)*bool) -> (exn -> 'a3 + IOBase.coq_T) -> 'a3 IOBase.coq_T) -> + (exn -> 'a3 IOBase.coq_T) -> 'a3 + IOBase.coq_T **) + + let bind x k s e r sk fk = + Obj.magic x s e __ (fun a fk0 -> + let x0,c = a in + let x1,s0 = x0 in + Obj.magic k x1 s0 e __ (fun a0 fk1 -> + let y,c' = a0 in + sk (y,(if c then c' else false)) fk1) + fk0) fk + + (** val ignore : + 'a1 t -> proofview -> Environ.env -> __ + -> (((unit*proofview)*bool) -> (exn -> + 'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T) + -> (exn -> 'a2 IOBase.coq_T) -> 'a2 + IOBase.coq_T **) + + let ignore x s e r sk fk = + Obj.magic x s e __ (fun a fk0 -> + let x0,c = a in + let sk0 = fun a0 fk1 -> + let y,c' = a0 in + sk (y,(if c then c' else false)) fk1 + in + let a0,s0 = x0 in + sk0 (((),s0),true) fk0) fk + + (** val seq : + unit t -> 'a1 t -> proofview -> + Environ.env -> __ -> + ((('a1*proofview)*bool) -> (exn -> 'a2 + IOBase.coq_T) -> 'a2 IOBase.coq_T) -> + (exn -> 'a2 IOBase.coq_T) -> 'a2 + IOBase.coq_T **) + + let seq x k s e r sk fk = + Obj.magic x s e __ (fun a fk0 -> + let x0,c = a in + let u,s0 = x0 in + Obj.magic k s0 e __ (fun a0 fk1 -> + let y,c' = a0 in + sk (y,(if c then c' else false)) fk1) + fk0) fk + + (** val set : + logicalState -> proofview -> + Environ.env -> __ -> + (((unit*proofview)*bool) -> (exn -> 'a1 + IOBase.coq_T) -> 'a1 IOBase.coq_T) -> + (exn -> 'a1 IOBase.coq_T) -> 'a1 + IOBase.coq_T **) + + let set s s0 e r sk fk = + sk (((),s),true) fk + + (** val get : + proofview -> Environ.env -> __ -> + (((logicalState*proofview)*bool) -> + (exn -> 'a1 IOBase.coq_T) -> 'a1 + IOBase.coq_T) -> (exn -> 'a1 + IOBase.coq_T) -> 'a1 IOBase.coq_T **) + + let get s e r sk fk = + sk ((s,s),true) fk + + (** val put : + logicalMessageType -> proofview -> + Environ.env -> __ -> + (((unit*proofview)*bool) -> (exn -> 'a1 + IOBase.coq_T) -> 'a1 IOBase.coq_T) -> + (exn -> 'a1 IOBase.coq_T) -> 'a1 + IOBase.coq_T **) + + let put m s e r sk fk = + sk (((),s),m) fk + + (** val current : + proofview -> Environ.env -> __ -> + (((logicalEnvironment*proofview)*bool) + -> (exn -> 'a1 IOBase.coq_T) -> 'a1 + IOBase.coq_T) -> (exn -> 'a1 + IOBase.coq_T) -> 'a1 IOBase.coq_T **) + + let current s e r sk fk = + sk ((e,s),true) fk + + (** val zero : + exn -> proofview -> Environ.env -> __ + -> ((('a1*proofview)*bool) -> (exn -> + 'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T) + -> (exn -> 'a2 IOBase.coq_T) -> 'a2 + IOBase.coq_T **) + + let zero e s e0 r sk fk = + fk e + + (** val plus : + 'a1 t -> (exn -> 'a1 t) -> proofview -> + Environ.env -> __ -> + ((('a1*proofview)*bool) -> (exn -> 'a2 + IOBase.coq_T) -> 'a2 IOBase.coq_T) -> + (exn -> 'a2 IOBase.coq_T) -> 'a2 + IOBase.coq_T **) + + let plus x y s env r sk fk = + Obj.magic x s env __ sk (fun e -> + Obj.magic y e s env __ sk fk) + + (** val split : + 'a1 t -> proofview -> Environ.env -> __ + -> (((('a1*(exn -> 'a1 t), exn) + Util.union*proofview)*bool) -> (exn -> + 'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T) + -> (exn -> 'a2 IOBase.coq_T) -> 'a2 + IOBase.coq_T **) + + let split x s e r sk fk = + IOBase.bind + (Obj.magic x s e __ (fun a fk0 -> + IOBase.ret (Util.Inl + (a,(fun e0 _ sk0 fk1 -> + IOBase.bind (fk0 e0) (fun x0 -> + match x0 with + | Util.Inl p -> + let a0,x1 = p in + sk0 a0 (fun e1 -> + x1 e1 __ sk0 fk1) + | Util.Inr e1 -> fk1 e1))))) + (fun e0 -> IOBase.ret (Util.Inr e0))) + (fun x0 -> + let sk0 = fun a fk0 -> + let sk0 = fun a0 fk1 -> + let x1,c = a0 in + let sk0 = fun a1 fk2 -> + let y,c' = a1 in + sk (y,(if c then c' else false)) + fk2 + in + (match x1 with + | Util.Inl p -> + let p0,y = p in + let a1,s0 = p0 in + sk0 (((Util.Inl + (a1,(fun e0 x2 -> + y e0))),s0),true) fk1 + | Util.Inr e0 -> + sk0 (((Util.Inr e0),s),true) fk1) + in + let x1,c = a in + let sk1 = fun a0 fk1 -> + let y,c' = a0 in + sk0 (y,(if c then c' else false)) + fk1 + in + (match x1 with + | Util.Inl p -> + let a0,y = p in + sk1 ((Util.Inl (a0,(fun e0 x2 -> + y e0))),true) fk0 + | Util.Inr e0 -> + sk1 ((Util.Inr e0),true) fk0) + in + (match x0 with + | Util.Inl p -> + let p0,y = p in + let a,c = p0 in + sk0 ((Util.Inl (a,y)),c) fk + | Util.Inr e0 -> + sk0 ((Util.Inr e0),true) fk)) + + (** val lift : + 'a1 NonLogical.t -> proofview -> + Environ.env -> __ -> + ((('a1*proofview)*bool) -> (exn -> 'a2 + IOBase.coq_T) -> 'a2 IOBase.coq_T) -> + (exn -> 'a2 IOBase.coq_T) -> 'a2 + IOBase.coq_T **) + + let lift x s e r sk fk = + IOBase.bind x (fun x0 -> + sk ((x0,s),true) fk) + + (** val run : + 'a1 t -> logicalEnvironment -> + logicalState -> + (('a1*logicalState)*logicalMessageType) + NonLogical.t **) + + let run x e s = + Obj.magic x s e __ (fun a x0 -> + IOBase.ret a) (fun e0 -> + IOBase.raise + ((fun e -> Proof_errors.TacticFailure e) + e0)) + end + diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml new file mode 100644 index 0000000000..ebbb040877 --- /dev/null +++ b/proofs/proofview_monad.ml @@ -0,0 +1 @@ +include Proofview_gen diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli new file mode 100644 index 0000000000..02550aebc0 --- /dev/null +++ b/proofs/proofview_monad.mli @@ -0,0 +1,81 @@ +(* This is an interface for the code extracted from bootstrap/Monad.v. + The relevant comments are overthere. *) + + +type proofview = { initial : (Term.constr * Term.types) list; + solution : Evd.evar_map; comb : Goal.goal list } + +type logicalState = proofview + +type logicalEnvironment = Environ.env + +type logicalMessageType = bool + + + +module NonLogical : sig + + type +'a t + type 'a ref + + val ret : 'a -> 'a t + val bind : 'a t -> ('a -> 'b t) -> 'b t + val ignore : 'a t -> unit t + val seq : unit t -> 'a t -> 'a t + + val new_ref : 'a -> 'a ref t + val set : 'a ref -> 'a -> unit t + val get : 'a ref -> 'a t + + val raise : exn -> 'a t + val catch : 'a t -> (exn -> 'a t) -> 'a t + val timeout : int -> 'a t -> 'a t + + + (* [run] performs effects. *) + val run : 'a t -> 'a + +end + + +module Logical : sig + + type +'a t + + val ret : 'a -> 'a t + val bind : 'a t -> ('a -> 'b t) -> 'b t + val ignore : 'a t -> unit t + val seq : unit t -> 'a t -> 'a t + + val set : logicalState -> unit t + val get : logicalState t + val put : logicalMessageType -> unit t + val current : logicalEnvironment t + + val zero : exn -> 'a t + val plus : 'a t -> (exn -> 'a t) -> 'a t + val split : 'a t -> (('a*(exn->'a t),exn) Util.union) t + + val lift : 'a NonLogical.t -> 'a t + + val run : 'a t -> logicalEnvironment -> logicalState -> (('a*logicalState)*logicalMessageType) NonLogical.t +end + + + + + + + + + + + + + + + + + + + |