IStream: change type of thunk, spare allocations.

Two changes:
- 'a Lazy.t  becomes unit -> 'a
- 'a t becomes 'a u (the view type)

This spares two Lazy.force, and leverages Lazy.lazy_from_fun. Considering Lazy.force is fairly slow, in particular because of the write-barrier, this should be beneficial.

3 files changed, 30 insertions, 30 deletions

diff --git a/lib/iStream.ml b/lib/iStream.ml
index 65a336daf..1d9f55998 100644
--- a/lib/iStream.ml
+++ b/lib/iStream.ml
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-type ('a,'r) peek =
+type ('a,'r) u =
 | Nil
 | Cons of 'a * 'r
 
-type 'a node = ('a,'a t) peek
+type 'a node = ('a,'a t) u
 
 and 'a t = 'a node Lazy.t
 
@@ -18,7 +18,7 @@ let empty = Lazy.lazy_from_val Nil
 
 let cons x s = Lazy.lazy_from_val (Cons (x, s))
 
-let thunk s = lazy (Lazy.force (Lazy.force s))
+let thunk = Lazy.lazy_from_fun
 
 let rec force s = match Lazy.force s with
 | Nil -> ()
diff --git a/lib/iStream.mli b/lib/iStream.mli
index fd3fa6c50..9e4dec415 100644
--- a/lib/iStream.mli
+++ b/lib/iStream.mli
@@ -15,6 +15,11 @@
 type +'a t
 (** Type of pure streams. *)
 
+type ('a,'r) u =
+| Nil
+| Cons of 'a * 'r
+(** View type to decompose and build streams. *)
+
 (** {6 Constructors} *)
 
 val empty : 'a t
@@ -23,7 +28,7 @@ val empty : 'a t
 val cons : 'a -> 'a t -> 'a t
 (** Append an element in front of a stream. *)
 
-val thunk : 'a t Lazy.t -> 'a t
+val thunk : (unit -> ('a,'a t) u) -> 'a t
 (** Internalize the lazyness of a stream. *)
 
 (** {6 Destructors} *)
@@ -31,12 +36,7 @@ val thunk : 'a t Lazy.t -> 'a t
 val is_empty : 'a t -> bool
 (** Whethere a stream is empty. *)
 
-type ('a,'r) peek =
-| Nil
-| Cons of 'a * 'r
-(** View type for {!peek} *)
-
-val peek : 'a t -> ('a , 'a t) peek
+val peek : 'a t -> ('a , 'a t) u
 (** Return the head and the tail of a stream, if any. *)
 
 (** {6 Standard operations}
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 8e77de9c5..0d3f24928 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -266,7 +266,7 @@ type matching_result =
     { m_sub : bound_ident_map * patvar_map;
       m_ctx : constr; }
 
-let mkresult s c n = IStream.cons { m_sub=s; m_ctx=c; } (IStream.thunk n)
+let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) )
 
 let isPMeta = function PMeta _ -> true | _ -> false
 
@@ -286,9 +286,9 @@ let authorized_occ partial_app closed pat c mk_ctx next =
   try
     let sigma = matches_core_closed None partial_app pat c in
     if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd sigma)
-    then Lazy.force next
+    then next ()
     else mkresult sigma (mk_ctx (mkMeta special_meta)) next
-  with PatternMatchingFailure -> Lazy.force next
+  with PatternMatchingFailure -> next ()
 
 (* Tries to match a subterm of [c] with [pat] *)
 let sub_match ?(partial_app=false) ?(closed=true) pat c =
@@ -296,25 +296,25 @@ let sub_match ?(partial_app=false) ?(closed=true) pat c =
   match kind_of_term c with
   | Cast (c1,k,c2) ->
       let next_mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in
-      let next = lazy (try_aux [c1] next_mk_ctx next) in
+      let next () = try_aux [c1] next_mk_ctx next in
       authorized_occ partial_app closed pat c mk_ctx next
   | Lambda (x,c1,c2) ->
       let next_mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in
-      let next = lazy (try_aux [c1;c2] next_mk_ctx next) in
+      let next () = try_aux [c1;c2] next_mk_ctx next in
       authorized_occ partial_app closed pat c mk_ctx next
   | Prod (x,c1,c2) ->
       let next_mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in
-      let next = lazy (try_aux [c1;c2] next_mk_ctx next) in
+      let next () = try_aux [c1;c2] next_mk_ctx next in
       authorized_occ partial_app closed pat c mk_ctx next
   | LetIn (x,c1,t,c2) ->
       let next_mk_ctx = function
       | [c1;c2] -> mkLetIn (x,c1,t,c2)
       | _ -> assert false
       in
-      let next = lazy (try_aux [c1;c2] next_mk_ctx next) in
+      let next () = try_aux [c1;c2] next_mk_ctx next in
       authorized_occ partial_app closed pat c mk_ctx next
   | App (c1,lc) ->
-      let next = lazy (
+      let next () =
         let topdown = true in
         if partial_app then
           if topdown then
@@ -333,14 +333,14 @@ let sub_match ?(partial_app=false) ?(closed=true) pat c =
                   try_aux (c1::Array.to_list lc) mk_ctx next
               | arg :: args ->
                   let app = mkApp (app,[|arg|]) in
-                  let next = lazy (aux2 app args next) in
+                  let next () = aux2 app args next in
                   let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in
                   aux app mk_ctx next in
             aux2 c1 (Array.to_list lc) next
         else
           let mk_ctx le =
             mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
-          try_aux (c1::Array.to_list lc) mk_ctx next)
+          try_aux (c1::Array.to_list lc) mk_ctx next
       in
       authorized_occ partial_app closed pat c mk_ctx next
   | Case (ci,hd,c1,lc) ->
@@ -348,24 +348,24 @@ let sub_match ?(partial_app=false) ?(closed=true) pat c =
       | [] -> assert false
       | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
       in
-      let next = lazy (try_aux (c1 :: Array.to_list lc) next_mk_ctx next) in
+      let next () = try_aux (c1 :: Array.to_list lc) next_mk_ctx next in
       authorized_occ partial_app closed pat c mk_ctx next
   | Fix (indx,(names,types,bodies)) ->
     let nb_fix = Array.length types in
     let next_mk_ctx le =
       let (ntypes,nbodies) = CList.chop nb_fix le in
       mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in
-    let next = lazy
-      (try_aux
-	 ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next) in
+    let next () =
+      try_aux
+	((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in
     authorized_occ partial_app closed pat c mk_ctx next
   | CoFix (i,(names,types,bodies)) ->
     let nb_fix = Array.length types in
     let next_mk_ctx le =
       let (ntypes,nbodies) = CList.chop nb_fix le in
       mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in
-    let next = lazy
-      (try_aux ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next) in
+    let next () =
+      try_aux ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in
     authorized_occ partial_app closed pat c mk_ctx next
   | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
       authorized_occ partial_app closed pat c mk_ctx next
@@ -373,14 +373,14 @@ let sub_match ?(partial_app=false) ?(closed=true) pat c =
   (* Tries [sub_match] for all terms in the list *)
   and try_aux lc mk_ctx next =
     let rec try_sub_match_rec lacc = function
-      | [] -> Lazy.force next
+      | [] -> next ()
       | c::tl ->
           let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in
-          let next = lazy (try_sub_match_rec (c::lacc) tl) in
+          let next () = try_sub_match_rec (c::lacc) tl in
           aux c mk_ctx next in
     try_sub_match_rec [] lc in
-  let lempty = lazy IStream.empty in
-  let result = lazy (aux c (fun x -> x) lempty) in
+  let lempty () = IStream.Nil in
+  let result () = aux c (fun x -> x) lempty in
   IStream.thunk result
 
 let match_subterm pat c = sub_match pat c