diff options
author | 2016-11-07 16:03:53 +0100 | |
---|---|---|
committer | 2017-02-10 13:05:23 +0100 | |
commit | f30822ba46d08d65597e0e3230ea6ad86c98453f (patch) | |
tree | 0b938d18a8f38f3ca08969e022ffa55f1fd676fa /engine | |
parent | ebbc4a8cf3dde3b18388f3723b1641ba5511db9b (diff) |
Proofview: tclINDEPENDENTL
Diffstat (limited to 'engine')
-rw-r--r-- | engine/proofview.ml | 29 | ||||
-rw-r--r-- | engine/proofview.mli | 1 |
2 files changed, 29 insertions, 1 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 2fbabb749..721389af4 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -453,6 +453,25 @@ let iter_goal i = Solution.get >>= fun evd -> Comb.set CList.(undefined evd (flatten (rev subgoals))) +(** List iter but allocates a list of results *) +let map_goal i = + let rev = List.rev in (* hem... Proof masks List... *) + let open Proof in + Comb.get >>= fun initial -> + Proof.List.fold_left begin fun (acc, subgoals as cur) goal -> + Solution.get >>= fun step -> + match Evarutil.advance step goal with + | None -> return cur + | Some goal -> + Comb.set [goal] >> + i goal >>= fun res -> + Proof.map (fun comb -> comb :: subgoals) Comb.get >>= fun x -> + return (res :: acc, x) + end ([],[]) initial >>= fun (results_rev, subgoals) -> + Solution.get >>= fun evd -> + Comb.set CList.(undefined evd (flatten (rev subgoals))) >> + return (rev results_rev) + (** A variant of [Monad.List.fold_left2] where the first list is the list of focused goals. The argument tactic is executed in a focus comprising only of the current goal, a goal which has been solved @@ -585,7 +604,15 @@ let tclINDEPENDENT tac = let tac = InfoL.tag (Info.DBranch) tac in InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac)) - +let tclINDEPENDENTL tac = + let open Proof in + Pv.get >>= fun initial -> + match initial.comb with + | [] -> tclUNIT [] + | [_] -> tac >>= fun x -> return [x] + | _ -> + let tac = InfoL.tag (Info.DBranch) tac in + InfoL.tag (Info.Dispatch) (map_goal (fun _ -> tac)) (** {7 Goal manipulation} *) diff --git a/engine/proofview.mli b/engine/proofview.mli index 90be2f90a..294b03dca 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -292,6 +292,7 @@ val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tact independent of backtracking in another. It is equivalent to [tclEXTEND [] tac []]. *) val tclINDEPENDENT : unit tactic -> unit tactic +val tclINDEPENDENTL: 'a tactic -> 'a list tactic (** {7 Goal manipulation} *) |