diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/monads.ml | 117 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 20 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 15 | ||||
| -rw-r--r-- | proofs/proof.ml | 4 | ||||
| -rw-r--r-- | proofs/proof.mli | 4 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 8 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 7 | ||||
| -rw-r--r-- | proofs/proofview.ml | 124 | ||||
| -rw-r--r-- | proofs/proofview.mli | 10 |
9 files changed, 227 insertions, 82 deletions
diff --git a/proofs/monads.ml b/proofs/monads.ml index ba14408641..803715a450 100644 --- a/proofs/monads.ml +++ b/proofs/monads.ml @@ -22,6 +22,13 @@ module type State = sig 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 @@ -133,6 +140,54 @@ end = struct 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 @@ -301,6 +356,7 @@ module StateLogic(X:Type)(T:Logic) : sig 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 @@ -370,14 +426,71 @@ end = struct 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/pfedit.ml b/proofs/pfedit.ml index 55c46a3401..6c0ddfc11a 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -33,10 +33,10 @@ let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook = let goals = [ (Global.env_of_context hyps , c) ] in Proof_global.start_proof id str goals ?compute_guard hook; let env = Global.env () in - Proof_global.with_current_proof (fun _ p -> + ignore (Proof_global.with_current_proof (fun _ p -> match init_tac with - | None -> p - | Some tac -> Proof.run_tactic env tac p) + | None -> p,true + | Some tac -> Proof.run_tactic env tac p)) let cook_this_proof hook p = match p with @@ -105,7 +105,7 @@ let solve_nth ?with_end_tac gi tac pr = let by tac = Proof_global.with_current_proof (fun _ -> solve_nth 1 tac) let instantiate_nth_evar_com n com = - Proof_global.with_current_proof (fun _ -> Proof.V82.instantiate_evar n com) + Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p) (**********************************************************************) @@ -118,10 +118,10 @@ let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac = start_proof id goal_kind sign typ (fun _ _ -> ()); try - by tac; + let status = by tac in let _,(const,_,_,_) = cook_proof (fun _ -> ()) in delete_current_proof (); - const + const, status with reraise -> delete_current_proof (); raise reraise @@ -134,11 +134,11 @@ let constr_of_def = function let build_by_tactic env typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in - let ce = build_constant_by_tactic id sign typ tac in + let ce,status = build_constant_by_tactic id sign typ tac in let ce = Term_typing.handle_side_effects env ce in let cb, se = Future.force ce.const_entry_body in - assert(Declareops.side_effects_is_empty se); - cb + assert(Declareops.side_effects_is_empty (Declareops.no_seff)); + cb,status (**********************************************************************) (* Support for resolution of evars in tactic interpretation, including @@ -155,7 +155,7 @@ let solve_by_implicit_tactic env sigma evk = when Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> - (try build_by_tactic env evi.evar_concl (Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) [])) + (try fst (build_by_tactic env evi.evar_concl (Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []))) with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 3a0c25c46a..73f12db987 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -136,13 +136,14 @@ val get_used_variables : unit -> Context.section_context option if there is no [n]th subgoal *) val solve_nth : ?with_end_tac:unit Proofview.tactic -> int -> unit Proofview.tactic -> - Proof.proof -> Proof.proof + Proof.proof -> Proof.proof*bool (** [by tac] applies tactic [tac] to the 1st subgoal of the current focused proof or raises a UserError if there is no focused proof or - if there is no more subgoals *) + if there is no more subgoals. + Returns [false] if an unsafe tactic has been used. *) -val by : unit Proofview.tactic -> unit +val by : unit Proofview.tactic -> bool (** [instantiate_nth_evar_com n c] instantiate the [n]th undefined existential variable of the current focused proof by [c] or raises a @@ -151,12 +152,14 @@ val by : unit Proofview.tactic -> unit val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit -(** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *) +(** [build_by_tactic typ tac] returns a term of type [typ] by calling + [tac]. The return boolean, if [false] indicates the use of an unsafe + tactic. *) val build_constant_by_tactic : Id.t -> named_context_val -> ?goal_kind:goal_kind -> - types -> unit Proofview.tactic -> Entries.definition_entry -val build_by_tactic : env -> types -> unit Proofview.tactic -> constr + types -> unit Proofview.tactic -> Entries.definition_entry * bool +val build_by_tactic : env -> types -> unit Proofview.tactic -> constr * bool (** Declare the default tactic to fill implicit arguments *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 89f3638a10..3a00d76f06 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -252,8 +252,8 @@ let initial_goals p = Proofview.initial_goals p.proofview let run_tactic env tac pr = let sp = pr.proofview in - let (_,tacticced_proofview) = Proofview.apply env tac sp in - { pr with proofview = tacticced_proofview } + let (_,tacticced_proofview,status) = Proofview.apply env tac sp in + { pr with proofview = tacticced_proofview },status let emit_side_effects eff pr = {pr with proofview = Proofview.emit_side_effects eff pr.proofview} diff --git a/proofs/proof.mli b/proofs/proof.mli index fa6007061b..66aee03138 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -128,7 +128,9 @@ val no_focused_goal : proof -> bool (*** Tactics ***) -val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof +(* the returned boolean signal whether an unsafe tactic has been + used. In which case it is [false]. *) +val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof*bool val emit_side_effects : Declareops.side_effects -> proof -> proof diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 3f84f6500d..5e11cfdb2d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -154,8 +154,12 @@ let with_current_proof f = match p.endline_tactic with | None -> Proofview.tclUNIT () | Some tac -> !interp_tac tac in - let p = { p with proof = f et p.proof } in - pstates := p :: rest + let (newpr,status) = f et p.proof in + let p = { p with proof = newpr } in + pstates := p :: rest; + status +let simple_with_current_proof f = + ignore (with_current_proof (fun t p -> f t p , true)) (* Sets the tactic to be used when a tactic line is closed with [...] *) let set_endline_tactic tac = diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 9b5015e0c3..867010fb05 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -79,9 +79,12 @@ exception NoSuchProof val get_open_goals : unit -> int -(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is - no current proof. *) +(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is + no current proof. + The return boolean is set to [false] if an unsafe tactic has been used. *) val with_current_proof : + (unit Proofview.tactic -> Proof.proof -> Proof.proof*bool) -> bool +val simple_with_current_proof : (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit (** Sets the tactic to be used when a tactic line is closed with [...] *) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 3f80da785c..a3791e7a42 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -190,81 +190,88 @@ let unfocus c sp = - 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 +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 Inner = Monads.StateLogic(LocalState)(Backtrack) +module Message = Monads.WriterLogic(MessageType)(Backtrack) +module Proof = Monads.StateLogic(ProofState)(Message) -type +'a tactic = Environ.env -> 'a Inner.t +type +'a tactic = Environ.env -> 'a Proof.t (* Applies a tactic to the current proofview. *) let apply env t sp = - let next = Monads.IO.run (Backtrack.run (Inner.run (t env) sp)) in - next.Inner.result , next.Inner.state + let (next,status) = Monads.IO.run (Backtrack.run (Message.run (Proof.run (t env) sp))) in + next.Proof.result , next.Proof.state , status (*** tacticals ***) (* Unit of the tactic monad *) -let tclUNIT a _ = Inner.return a +let tclUNIT a _ = Proof.return a (* Bind operation of the tactic monad *) let tclBIND t k env = - Inner.bind (t env) (fun a -> k a env) + Proof.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 = - Inner.seq (t1 env) (t2 env) + Proof.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 = Inner.ignore (tac env) +let tclIGNORE tac env = Proof.ignore (tac env) (* [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 = - Inner.plus (t1 env) (fun e -> t2 e env) + Proof.plus (t1 env) (fun e -> t2 e env) (* [tclZERO e] always fails with error message [e]*) -let tclZERO e _ = Inner.zero e +let tclZERO e _ = Proof.zero e (* [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 + let (>>=) = Proof.bind in + Proof.split (t1 env) >>= function | Util.Inr e -> t2 e env - | Util.Inl (a,t1') -> Inner.plus (Inner.return a) t1' + | Util.Inl (a,t1') -> Proof.plus (Proof.return a) t1' (* [tclIFCATCH a s f] is a generalisation of [tclORELSE]: if [a] succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a] fails with [e], then it behaves as [f e]. *) let tclIFCATCH a s f env = (* spiwack: convenience notations, waiting for ocaml 3.12 *) - let (>>=) = Inner.bind in - Inner.split (a env) >>= function + let (>>=) = Proof.bind in + Proof.split (a env) >>= function | Util.Inr e -> f e env - | Util.Inl (x,a') -> Inner.plus (s x env) (fun e -> (a' e) >>= fun x' -> (s x' env)) + | Util.Inl (x,a') -> Proof.plus (s x env) (fun e -> (a' e) >>= fun x' -> (s x' env)) (* Focuses a tactic at a range of subgoals, found by their indices. *) (* arnaud: bug if 0 goals ! *) 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 (>>=) = Proof.bind in + let (>>) = Proof.seq in + Proof.get >>= fun initial -> try let (focused,context) = focus i j initial in - Inner.set focused >> + Proof.set focused >> t (env) >>= fun result -> - Inner.get >>= fun next -> - Inner.set (unfocus context next) >> - Inner.return result + Proof.get >>= fun next -> + Proof.set (unfocus context next) >> + Proof.return result with e -> (* spiwack: a priori the only possible exceptions are that of focus, of course I haven't made them algebraic yet. *) @@ -294,24 +301,24 @@ end 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 -> + let (>>=) = Proof.bind in + let (>>) = Proof.seq in + Proof.get >>= fun initial -> match tacs,initial.comb with | [], [] -> tclUNIT null env | t::tacs , first::goals -> begin match Goal.advance initial.solution first with - | None -> Inner.return null (* If [first] has been solved by side effect: do nothing. *) + | None -> Proof.return null (* If [first] has been solved by side effect: do nothing. *) | Some first -> - Inner.set {initial with comb=[first]} >> + Proof.set {initial with comb=[first]} >> t env end >>= fun y -> - Inner.get >>= fun step -> - Inner.set {step with comb=goals} >> + Proof.get >>= fun step -> + Proof.set {step with comb=goals} >> tclDISPATCHGEN null join tacs env >>= fun x -> - Inner.get >>= fun step' -> - Inner.set {step' with comb=step.comb@step'.comb} >> - Inner.return (join y x) + Proof.get >>= fun step' -> + Proof.set {step' with comb=step.comb@step'.comb} >> + Proof.return (join y x) | _ , _ -> tclZERO SizeMismatch env let unitK () () = () @@ -338,8 +345,8 @@ let extend_to_list = 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 (>>=) = Proof.bind in + Proof.get >>= fun step -> let tacs = extend_to_list tacs1 rtac tacs2 step.comb in tclDISPATCH tacs env @@ -362,20 +369,20 @@ let sensitive_on_proofview s env step = 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 -> + let (>>=) = Proof.bind in + Proof.get >>= fun step -> try let next = sensitive_on_proofview s env step in - Inner.set next + Proof.set next with e when Errors.noncritical e -> tclZERO e env let tclPROGRESS t env = (* spiwack: convenience notations, waiting for ocaml 3.12 *) - let (>>=) = Inner.bind in - Inner.get >>= fun initial -> + let (>>=) = Proof.bind in + Proof.get >>= fun initial -> t env >>= fun res -> - Inner.get >>= fun final -> + 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) @@ -387,14 +394,17 @@ let tclPROGRESS t env = let tclEVARMAP _ = (* spiwack: convenience notations, waiting for ocaml 3.12 *) - let (>>=) = Inner.bind in - Inner.get >>= fun initial -> - Inner.return (initial.solution) + let (>>=) = Proof.bind in + Proof.get >>= fun initial -> + Proof.return (initial.solution) let tclENV env = - Inner.return env + Proof.return env + +let tclTIMEOUT n t env = Proof.timeout n (t env) -let tclTIMEOUT n t env = Inner.timeout n (t env) +let mark_as_unsafe env = + Proof.lift (Message.put false) (*** Commands ***) @@ -450,8 +460,8 @@ module V82 = struct (* spiwack: we ignore the dependencies between goals here, expectingly preserving the semantics of <= 8.2 tactics *) (* spiwack: convenience notations, waiting for ocaml 3.12 *) - let (>>=) = Inner.bind in - Inner.get >>= fun ps -> + let (>>=) = Proof.bind in + Proof.get >>= fun ps -> try let tac evd gl = let glsigma = @@ -466,7 +476,7 @@ module V82 = struct 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; } + Proof.set { ps with solution=evd ; comb=sgs; } with e when Errors.noncritical e -> tclZERO e env @@ -516,9 +526,11 @@ module V82 = struct 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 + let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = final.comb } + let put_status b _env = + Proof.lift (Message.put b) end @@ -528,17 +540,17 @@ module Goal = struct let lift s env = (* spiwack: convenience notations, waiting for ocaml 3.12 *) - let (>>=) = Inner.bind in - let (>>) = Inner.seq in - Inner.get >>= fun step -> + let (>>=) = Proof.bind in + let (>>) = Proof.seq in + Proof.get >>= fun step -> try let (res,sigma) = Goal.list_map begin fun sigma g -> Goal.eval s env sigma g end step.comb step.solution in - Inner.set { step with solution=sigma } >> - Inner.return res + Proof.set { step with solution=sigma } >> + Proof.return res with e when Errors.noncritical e -> tclZERO e env diff --git a/proofs/proofview.mli b/proofs/proofview.mli index d2db5be9a3..4536180e2e 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -118,7 +118,9 @@ val unfocus : focus_context -> proofview -> proofview type +'a tactic (* Applies a tactic to the current proofview. *) -val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview +(* the return boolean signals the use of an unsafe tactic, in which + case it is [false]. *) +val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview * bool (*** tacticals ***) @@ -198,6 +200,9 @@ val tclENV : Environ.env tactic 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. *) +val mark_as_unsafe : unit tactic + val list_map : ('a -> 'b tactic) -> 'a list -> 'b list tactic (*** Commands ***) @@ -260,6 +265,9 @@ module V82 : sig should be avoided as much as possible. It should work as expected for a tactic obtained from {!V82.tactic} though. *) val of_tactic : 'a tactic -> tac + + (* marks as unsafe if the argument is [false] *) + val put_status : bool -> unit tactic end |