diff options
author | 2016-09-04 08:33:51 +0200 | |
---|---|---|
committer | 2016-09-16 15:30:09 +0200 | |
commit | 1a1af4f2119715245b8d4488664a8b57f4bdce08 (patch) | |
tree | c76d6383b9761ce5042b2062efd381057cdc5600 /engine | |
parent | 753248c145cdac846528d809a1f085c18408e17f (diff) |
Adding variants enter_one and refine_one which assume that exactly one
goal is under focus and which support returning a relevant output.
Diffstat (limited to 'engine')
-rw-r--r-- | engine/proofview.ml | 20 | ||||
-rw-r--r-- | engine/proofview.mli | 4 |
2 files changed, 24 insertions, 0 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 576569cf5..a2838a2de 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1058,6 +1058,26 @@ module Goal = struct end end + exception NotExactlyOneSubgoal + let _ = CErrors.register_handler begin function + | NotExactlyOneSubgoal -> + CErrors.errorlabstrm "" (Pp.str"Not exactly one subgoal.") + | _ -> raise CErrors.Unhandled + end + + let enter_one f = + let open Proof in + Comb.get >>= function + | [goal] -> begin + Env.get >>= fun env -> + tclEVARMAP >>= fun sigma -> + try f.enter (gmake env sigma goal) + with e when catchable_exception e -> + let (e, info) = CErrors.push e in + tclZERO ~info e + end + | _ -> tclZERO NotExactlyOneSubgoal + type ('a, 'b) s_enter = { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } diff --git a/engine/proofview.mli b/engine/proofview.mli index 901cf26e0..bc68f11ff 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -499,6 +499,10 @@ module Goal : sig (** Like {!nf_enter}, but does not normalize the goal beforehand. *) val enter : ([ `LZ ], unit tactic) enter -> unit tactic + (** Like {!enter}, but assumes exactly one goal under focus, raising *) + (** an error otherwise. *) + val enter_one : ([ `LZ ], 'a tactic) enter -> 'a tactic + type ('a, 'b) s_enter = { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } |