A view type for IStream.

View types are better practice than option types for pattern-matching. (Plus, they save a minute amount of allocations)

3 files changed, 20 insertions, 13 deletions

diff --git a/lib/iStream.ml b/lib/iStream.ml
index f7d50612f9..ba08ffd24e 100644
--- a/lib/iStream.ml
+++ b/lib/iStream.ml
@@ -6,9 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-type 'a node =
+type ('a,'r) peek =
 | Nil
-| Cons of 'a * 'a t
+| Cons of 'a * 'r
+
+type 'a node = ('a,'a t) peek
 
 and 'a t = 'a node Lazy.t
 
@@ -32,9 +34,7 @@ let rec is_empty s = match Lazy.force s with
 | Nil -> true
 | Cons (_, _) -> false
 
-let peek s = match Lazy.force s with
-| Nil -> None
-| Cons (x, s) -> Some (x, s)
+let peek = Lazy.force
 
 let rec of_list = function
 | [] -> empty
diff --git a/lib/iStream.mli b/lib/iStream.mli
index caae0ad35a..fd3fa6c503 100644
--- a/lib/iStream.mli
+++ b/lib/iStream.mli
@@ -31,7 +31,12 @@ val thunk : 'a t Lazy.t -> 'a t
 val is_empty : 'a t -> bool
 (** Whethere a stream is empty. *)
 
-val peek : 'a t -> ('a * 'a t) option
+type ('a,'r) peek =
+| Nil
+| Cons of 'a * 'r
+(** View type for {!peek} *)
+
+val peek : 'a t -> ('a , 'a t) peek
 (** Return the head and the tail of a stream, if any. *)
 
 (** {6 Standard operations}
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1e3eda0328..a8180f4929 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1245,16 +1245,17 @@ and interp_match_successes lz ist s =
         relying on the fact that it will always be applied to a single
         goal, by virtue of an earlier [Proofview.Goal.enter]. *)
   let rec tclOR_stream t e =
-    match IStream.peek t with
-    | Some (t1,t') ->
+    let open IStream in
+    match peek t with
+    | Cons (t1,t') ->
         Proofview.tclORELSE
           t1
           begin fun e ->
               (* Honors Ltac's failure level. *)
               Tacticals.New.catch_failerror e <*> tclOR_stream t' e
             end
-      | None ->
-          Proofview.tclZERO e
+    | Nil ->
+        Proofview.tclZERO e
     in
     let matching_failure =
       UserError ("Tacinterp.apply_match" , str "No matching clauses for match.")
@@ -1264,9 +1265,10 @@ and interp_match_successes lz ist s =
     in
     if lz then
       (** lazymatch *)
-      begin match IStream.peek successes with
-      | Some (s,_) -> s
-      | None -> Proofview.tclZERO matching_failure
+      let open IStream in
+      begin match peek successes with
+      | Cons (s,_) -> s
+      | Nil -> Proofview.tclZERO matching_failure
       end
     else
       (** match *)