diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/proofview.ml | 42 |
1 files changed, 17 insertions, 25 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index c00c90e5e9..d4f6fe3aef 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -373,32 +373,24 @@ let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t let tclFOCUSLIST ?(nosuchgoal=tclZERO (NoSuchGoals 0)) l t = let open Proof in Comb.get >>= fun comb -> - let n = CList.length comb in - (* First, remove empty intervals, and bound the intervals to the number - of goals. *) - let sanitize (i, j) = - if i > j then None - else if i > n then None - else if j < 1 then None - else Some ((max i 1), (min j n)) - in - let l = CList.map_filter sanitize l in + let n = CList.length comb in + let ok (i, j) = 1 <= i && i <= j && j <= n in + if not (CList.for_all ok l) then nosuchgoal + else match l with - | [] -> nosuchgoal - | (mi, _) :: _ -> - (* Get the left-most goal to focus. This goal won't move, and we - will then place all the other goals to focus to the right. *) - let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in - (* [CList.goto] returns a zipper, so that - [(rev left) @ sub_right = comb]. *) - let left, sub_right = CList.goto (mi-1) comb in - let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in - let sub, right = CList.partitioni p sub_right in - let mj = mi - 1 + CList.length sub in - Comb.set (CList.rev_append left (sub @ right)) >> - tclFOCUS mi mj t - - + | [] -> nosuchgoal + | (mi, _) :: _ -> + (* Get the left-most goal to focus. This goal won't move, and we + will then place all the other goals to focus to the right. *) + let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in + (* [CList.goto] returns a zipper, so that + [(rev left) @ sub_right = comb]. *) + let left, sub_right = CList.goto (mi-1) comb in + let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in + let sub, right = CList.partitioni p sub_right in + let mj = mi - 1 + CList.length sub in + Comb.set (CList.rev_append left (sub @ right)) >> + tclFOCUS mi mj t (** Like {!tclFOCUS} but selects a single goal by name. *) let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t = |