From 80f2f9462205193885f054338ab28bfcd17de965 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Sat, 2 Nov 2013 15:35:11 +0000 Subject: The tactic [admit] exits with the "unsafe" status. It is highlighted in yellow in Coqide. The unsafe status is tracked throughout the execution of tactics such that nested calls to admit are caught. Many function (mainly those building constr with tactics such as typeclass related stuff, and Function, and a few other like eauto's use of Hint Extern) drop the unsafe status. This is unfortunate, but a lot of refactoring would be in order. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16977 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/monads.ml | 117 ++++++++++++++++++++++++++++++++++++++++++++- proofs/pfedit.ml | 20 ++++---- proofs/pfedit.mli | 15 +++--- proofs/proof.ml | 4 +- proofs/proof.mli | 4 +- proofs/proof_global.ml | 8 +++- proofs/proof_global.mli | 7 ++- proofs/proofview.ml | 124 ++++++++++++++++++++++++++---------------------- proofs/proofview.mli | 10 +++- 9 files changed, 227 insertions(+), 82 deletions(-) (limited to 'proofs') diff --git a/proofs/monads.ml b/proofs/monads.ml index ba1440864..803715a45 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 55c46a340..6c0ddfc11 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 3a0c25c46..73f12db98 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 89f3638a1..3a00d76f0 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 fa6007061..66aee0313 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 3f84f6500..5e11cfdb2 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 9b5015e0c..867010fb0 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 3f80da785..a3791e7a4 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 d2db5be9a..4536180e2 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 -- cgit v1.2.3