diff options
| -rw-r--r-- | lib/monad.ml | 16 | ||||
| -rw-r--r-- | lib/monad.mli | 13 | ||||
| -rw-r--r-- | proofs/proofview.ml | 51 |
3 files changed, 34 insertions, 46 deletions
diff --git a/lib/monad.ml b/lib/monad.ml index bc58c4d17..4a52684da 100644 --- a/lib/monad.ml +++ b/lib/monad.ml @@ -67,16 +67,11 @@ module type ListS = sig (** {6 Two-list iterators} *) - (** Raised when an combinator expects several lists of the same size - but finds that they are not. Exceptions must be raised inside - the monad, so two-list combinators take an extra argument to - raise the exception. *) - exception SizeMismatch - (** [fold_left2 r f s l1 l2] behaves like {!fold_left} but acts - simultaneously on two lists. Returns [r SizeMismatch] if both lists - do not have the same length. *) - val fold_left2 : (exn->'a t) -> + simultaneously on two lists. Runs [r] (presumably an + exception-raising computation) if both lists do not have the + same length. *) + val fold_left2 : 'a t -> ('a -> 'b -> 'c -> 'a t) -> 'a -> 'b list -> 'c list -> 'a t end @@ -143,7 +138,6 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct | a::b::l -> f a >> f b >> iter f l - exception SizeMismatch let rec fold_left2 r f x l1 l2 = match l1,l2 with @@ -153,7 +147,7 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct f x a1 b1 >>= fun x' -> f x' a2 b2 >>= fun x'' -> fold_left2 r f x'' l1 l2 - | _ , _ -> r SizeMismatch + | _ , _ -> r end diff --git a/lib/monad.mli b/lib/monad.mli index a6be1df7a..c8655efa0 100644 --- a/lib/monad.mli +++ b/lib/monad.mli @@ -69,16 +69,11 @@ module type ListS = sig (** {6 Two-list iterators} *) - (** Raised when an combinator expects several lists of the same size - but finds that they are not. Exceptions must be raised inside - the monad, so two-list combinators take an extra argument to - raise the exception. *) - exception SizeMismatch - (** [fold_left2 r f s l1 l2] behaves like {!fold_left} but acts - simultaneously on two lists. Returns [r SizeMismatch] if both lists - do not have the same length. *) - val fold_left2 : (exn->'a t) -> + simultaneously on two lists. Runs [r] (presumably an + exception-raising computation) if both lists do not have the + same length. *) + val fold_left2 : 'a t -> ('a -> 'b -> 'c -> 'a t) -> 'a -> 'b list -> 'c list -> 'a t end diff --git a/proofs/proofview.ml b/proofs/proofview.ml index a4ccdd687..569ae148a 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -374,10 +374,11 @@ let _ = Errors.register_handler begin function | _ -> raise Errors.Unhandled end -(* A variant of [Monad.List.iter] where we iter over the focused list of - goals. The argument tactic is executed in a focus comprising only - of the current goal, a goal which has been solved by side effect is - skipped. The generated subgoals are concatenated in order. *) +(** A variant of [Monad.List.iter] where we iter over the focused list + of goals. The argument tactic is executed in a focus comprising + only of the current goal, a goal which has been solved by side + effect is skipped. The generated subgoals are concatenated in + order. *) let iter_goal i = let open Proof in Comb.get >>= fun initial -> @@ -392,31 +393,29 @@ let iter_goal i = end [] initial >>= fun subgoals -> Comb.set (CList.flatten (CList.rev subgoals)) -(* 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 - by side effect is skipped. The generated subgoals are concatenated - in order. *) +(** 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 + by side effect is skipped. The generated subgoals are concatenated + in order. *) let fold_left2_goal i s l = let open Proof in Pv.get >>= fun initial -> - tclORELSE begin - Proof.List.fold_left2 tclZERO begin fun ((r,subgoals) as cur) goal a -> - Solution.get >>= fun step -> - match advance step goal with - | None -> return cur - | Some goal -> - Comb.set [goal] >> - i goal a r >>= fun r -> - Proof.map (fun comb -> (r, comb :: subgoals)) Comb.get - end (s,[]) initial.comb l >>= fun (r,subgoals) -> - Comb.set (CList.flatten (CList.rev subgoals)) >> - return r - end - begin function - | Proof.List.SizeMismatch -> tclZERO (SizeMismatch (CList.length initial.comb,CList.length l)) - | reraise -> tclZERO reraise - end + let err = + return () >>= fun () -> (* Delay the computation of list lengths. *) + tclZERO (SizeMismatch (CList.length initial.comb,CList.length l)) + in + Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a -> + Solution.get >>= fun step -> + match advance step goal with + | None -> return cur + | Some goal -> + Comb.set [goal] >> + i goal a r >>= fun r -> + Proof.map (fun comb -> (r, comb :: subgoals)) Comb.get + end (s,[]) initial.comb l >>= fun (r,subgoals) -> + Comb.set (CList.flatten (CList.rev subgoals)) >> + return r (** Dispatch tacticals are used to apply a different tactic to each goal under focus. They come in two flavours: [tclDISPATCH] takes a |