Pushing lazy lists into Ltac. Now, the control flow is explicit

in Tacinterp, and it allows to remove a lot of entangled exception
matchings in MatchGoal. Performance should not be affected, because
the structures manipulated are somehow similar.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16533 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 127 insertions, 130 deletions

diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index edd1ec0a7..1af1eae67 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -263,12 +263,11 @@ let matches pat c = snd (matches_core_closed None true pat c)
 
 let special_meta = (-1)
 
-type 'a matching_result =
+type matching_result =
     { m_sub : bound_ident_map * patvar_map;
-      m_ctx : 'a;
-      m_nxt : unit -> 'a matching_result }
+      m_ctx : constr; }
 
-let mkresult s c n = { m_sub=s; m_ctx=c; m_nxt=n }
+let mkresult s c n = IStream.cons { m_sub=s; m_ctx=c; } (IStream.thunk n)
 
 let isPMeta = function PMeta _ -> true | _ -> false
 
@@ -288,64 +287,70 @@ 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 && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma))
-    then next ()
+    then Lazy.force next
     else mkresult sigma (mk_ctx (mkMeta special_meta)) next
-  with
-    PatternMatchingFailure -> next ()
+  with PatternMatchingFailure -> Lazy.force next
 
 (* Tries to match a subterm of [c] with [pat] *)
 let sub_match ?(partial_app=false) ?(closed=true) pat c =
   let rec aux c mk_ctx next =
   match kind_of_term c with
   | Cast (c1,k,c2) ->
-      authorized_occ partial_app closed pat c mk_ctx (fun () ->
-        let mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in
-        try_aux [c1] mk_ctx next)
+      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
+      authorized_occ partial_app closed pat c mk_ctx next
   | Lambda (x,c1,c2) ->
-      authorized_occ partial_app closed pat c mk_ctx (fun () ->
-        let mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in
-        try_aux [c1;c2] mk_ctx next)
+      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
+      authorized_occ partial_app closed pat c mk_ctx next
   | Prod (x,c1,c2) ->
-      authorized_occ partial_app closed pat c mk_ctx (fun () ->
-        let mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in
-        try_aux [c1;c2] mk_ctx next)
+      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
+      authorized_occ partial_app closed pat c mk_ctx next
   | LetIn (x,c1,t,c2) ->
-      authorized_occ partial_app closed pat c mk_ctx (fun () ->
-        let mk_ctx = function [c1;c2] -> mkLetIn (x,c1,t,c2) | _ -> assert false
-        in try_aux [c1;c2] mk_ctx next)
+      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
+      authorized_occ partial_app closed pat c mk_ctx next
   | App (c1,lc) ->
-      authorized_occ partial_app closed pat c mk_ctx (fun () ->
+      let next = lazy (
         let topdown = true in
-	if partial_app then
+        if partial_app then
           if topdown then
             let lc1 = Array.sub lc 0 (Array.length lc - 1) in
             let app = mkApp (c1,lc1) in
             let mk_ctx = function
               | [app';c] -> mk_ctx (mkApp (app',[|c|]))
               | _ -> assert false in
-	    try_aux [app;Array.last lc] mk_ctx next
+            try_aux [app;Array.last lc] mk_ctx next
           else
             let rec aux2 app args next =
               match args with
               | [] ->
                   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
-	      | arg :: args ->
+                  try_aux (c1::Array.to_list lc) mk_ctx next
+              | arg :: args ->
                   let app = mkApp (app,[|arg|]) in
-                  let next () = aux2 app args next in
+                  let next = lazy (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) ->
-      authorized_occ partial_app closed pat c mk_ctx (fun () ->
-        let mk_ctx le =
-          mk_ctx (mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))) in
-        try_aux (c1::Array.to_list lc) mk_ctx next)
+      let next_mk_ctx = function
+      | [] -> 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
+      authorized_occ partial_app closed pat c mk_ctx next
   | Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _
   | Rel _|Meta _|Var _|Sort _ ->
       authorized_occ partial_app closed pat c mk_ctx next
@@ -353,13 +358,15 @@ 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
-      | [] -> next ()
+      | [] -> Lazy.force next
       | c::tl ->
           let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in
-          let next () = try_sub_match_rec (c::lacc) tl in
+          let next = lazy (try_sub_match_rec (c::lacc) tl) in
           aux c mk_ctx next in
     try_sub_match_rec [] lc in
-  aux c (fun x -> x) (fun () -> raise PatternMatchingFailure)
+  let lempty = lazy IStream.empty in
+  let result = lazy (aux c (fun x -> x) lempty) in
+  IStream.thunk result
 
 let match_subterm pat c = sub_match pat c
 
@@ -376,8 +383,8 @@ let is_matching_head pat c =
   with PatternMatchingFailure -> false
 
 let is_matching_appsubterm ?(closed=true) pat c =
-  try let _ = sub_match ~partial_app:true ~closed pat c in true
-  with PatternMatchingFailure -> false
+  let results = sub_match ~partial_app:true ~closed pat c in
+  not (IStream.is_empty results)
 
 let matches_conv env sigma c p =
   snd (matches_core_closed (Some (env,sigma)) false c p)
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 5ce18931d..c9bf60ad2 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -60,27 +60,23 @@ val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
 (** The type of subterm matching results: a substitution + a context
    (whose hole is denoted here with [special_meta]) + a continuation that
    either returns the next matching subterm or raise PatternMatchingFailure *)
-type 'a matching_result =
+type matching_result =
     { m_sub : bound_ident_map * patvar_map;
-      m_ctx : 'a;
-      m_nxt : unit -> 'a matching_result }
+      m_ctx : constr }
 
 (** [match_subterm n pat c] returns the substitution and the context
    corresponding to the first **closed** subterm of [c] matching [pat], and
-   a continuation that looks for the next matching subterm.
-   It raises PatternMatchingFailure if no subterm matches the pattern *)
-val match_subterm : constr_pattern -> constr -> constr matching_result
+   a continuation that looks for the next matching subterm. *)
+val match_subterm : constr_pattern -> constr -> matching_result IStream.t
 
 (** [match_appsubterm pat c] returns the substitution and the context
    corresponding to the first **closed** subterm of [c] matching [pat],
-   considering application contexts as well. It also returns a
-   continuation that looks for the next matching subterm.
-   It raises PatternMatchingFailure if no subterm matches the pattern *)
-val match_appsubterm : constr_pattern -> constr -> constr matching_result
+   considering application contexts as well. *)
+val match_appsubterm : constr_pattern -> constr -> matching_result IStream.t
 
 (** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
 val match_subterm_gen : bool (** true = with app context *) ->
-   constr_pattern -> constr -> constr matching_result
+   constr_pattern -> constr -> matching_result IStream.t
 
 (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches
    against [pat] taking partial subterms into consideration *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f7129b9ba..1c7ce8a7b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -927,82 +927,73 @@ let adjust (l,lc) = (l,List.map (fun (id,c) -> (id,([],c))) lc)
 
 type 'a extended_matching_result =
     { e_ctx : 'a;
-      e_sub : bound_ident_map * extended_patvar_map;
-      e_nxt : unit -> 'a extended_matching_result }
+      e_sub : bound_ident_map * extended_patvar_map; }
+
+let push_id_couple id name env = match name with
+| Name idpat ->
+  let binding = idpat, VConstr ([], mkVar id) in
+  binding :: env
+| Anonymous -> env
+
+let match_pat refresh lmatch hyp gl = function
+| Term t ->
+  let hyp = if refresh then refresh_universes_strict hyp else hyp in
+  begin
+    try
+      let lmeta = extended_matches t hyp in
+      let lmeta = verify_metas_coherence gl lmatch lmeta in
+      let ans = { e_ctx = []; e_sub = lmeta; } in
+      IStream.cons ans IStream.lempty
+    with PatternMatchingFailure | Not_coherent_metas -> IStream.empty
+  end
+| Subterm (b,ic,t) ->
+  let hyp = if refresh then refresh_universes_strict hyp else hyp in
+  let matches = match_subterm_gen b t hyp in
+  let filter s =
+    try
+      let lmeta = verify_metas_coherence gl lmatch (adjust s.m_sub) in
+      let context = give_context s.m_ctx ic in
+      Some { e_ctx = context; e_sub = lmeta; }
+    with Not_coherent_metas -> None
+  in
+  IStream.map_filter filter matches
 
 (* Tries to match one hypothesis pattern with a list of hypotheses *)
 let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
-  let get_id_couple id = function
-    | Name idpat -> [idpat,VConstr ([],mkVar id)]
-    | Anonymous -> [] in
-  let match_pat lmatch hyp pat =
-    match pat with
-    | Term t ->
-        let lmeta = extended_matches t hyp in
-        (try
-            let lmeta = verify_metas_coherence gl lmatch lmeta in
-            { e_ctx = [];
-	      e_sub = lmeta;
-	      e_nxt = fun () -> raise PatternMatchingFailure }
-          with
-            | Not_coherent_metas -> raise PatternMatchingFailure)
-    | Subterm (b,ic,t) ->
-        let rec match_next_pattern find_next () =
-          let s = find_next () in
-          try
-            let lmeta = verify_metas_coherence gl lmatch (adjust s.m_sub) in
-            { e_ctx = give_context s.m_ctx ic;
-	      e_sub = lmeta;
-	      e_nxt = match_next_pattern s.m_nxt }
-          with
-            | Not_coherent_metas -> match_next_pattern s.m_nxt ()
-	in
-        match_next_pattern (fun () -> match_subterm_gen b t hyp) ()
-  in
   let rec apply_one_mhyp_context_rec = function
-    | (id,b,hyp as hd)::tl ->
-	(match patv with
-	| None ->
-            let rec match_next_pattern find_next () =
-              try
-                let s = find_next () in
-		{ e_ctx = (get_id_couple id hypname @ s.e_ctx), hd;
-		  e_sub = s.e_sub;
-                  e_nxt = match_next_pattern s.e_nxt }
-              with
-                | PatternMatchingFailure -> apply_one_mhyp_context_rec tl in
-            match_next_pattern (fun () ->
-	      let hyp = if Option.is_empty b then hyp else refresh_universes_strict hyp in
-	      match_pat lmatch hyp pat) ()
-	| Some patv ->
-	    match b with
-	    | Some body ->
-                let rec match_next_pattern_in_body next_in_body () =
-                  try
-                    let s1 = next_in_body() in
-                    let rec match_next_pattern_in_typ next_in_typ () =
-                      try
-			let s2 = next_in_typ() in
-		        { e_ctx = (get_id_couple id hypname@s1.e_ctx@s2.e_ctx), hd;
-			  e_sub = s2.e_sub;
-			  e_nxt = match_next_pattern_in_typ s2.e_nxt }
-                      with
-                        | PatternMatchingFailure ->
-                            match_next_pattern_in_body s1.e_nxt () in
-                    match_next_pattern_in_typ
-                      (fun () ->
-			let hyp = refresh_universes_strict hyp in
-			match_pat s1.e_sub hyp pat) ()
-                  with PatternMatchingFailure -> apply_one_mhyp_context_rec tl
-                in
-                match_next_pattern_in_body
-                  (fun () -> match_pat lmatch body patv) ()
-            | None -> apply_one_mhyp_context_rec tl)
     | [] ->
-        db_hyp_pattern_failure ist.debug env (hypname,pat);
-        raise PatternMatchingFailure
+(*      db_hyp_pattern_failure ist.debug env (hypname,pat);*)
+      IStream.empty
+    | (id, b, hyp as hd) :: tl ->
+      (match patv with
+      | None ->
+        let refresh = not (Option.is_empty b) in
+        let ans = IStream.thunk (lazy (match_pat refresh lmatch hyp gl pat)) in
+        let map s =
+          let context = (push_id_couple id hypname s.e_ctx), hd in
+          { e_ctx = context; e_sub = s.e_sub; }
+        in
+        let next = lazy (apply_one_mhyp_context_rec tl) in
+        IStream.app (IStream.map map ans) (IStream.thunk next)
+      | Some patv ->
+        match b with
+        | Some body ->
+          let body = match_pat false lmatch body gl patv in
+          let map_body s1 =
+            let types = lazy (match_pat true s1.e_sub hyp gl pat) in
+            let map_types s2 =
+              let env = push_id_couple id hypname s1.e_ctx in
+              let context = (env @s2.e_ctx), hd in
+              { e_ctx = context; e_sub = s2.e_sub; }
+            in
+            IStream.map map_types (IStream.thunk types)
+          in
+          let next = IStream.thunk (lazy (apply_one_mhyp_context_rec tl)) in
+          let body = IStream.map map_body body in
+          IStream.app (IStream.concat body) next
+        | None -> apply_one_mhyp_context_rec tl)
   in
-    apply_one_mhyp_context_rec lhyps
+  apply_one_mhyp_context_rec lhyps
 
 (* misc *)
 
@@ -1261,12 +1252,15 @@ and interp_match_goal ist goal lz lr lmr =
   let concl = pf_concl goal in
   let env = pf_env goal in
   let apply_goal_sub app ist (id,c) csr mt mhyps hyps =
-    let rec match_next_pattern find_next () =
-      let { m_sub=lgoal; m_ctx=ctxt; m_nxt=find_next' } = find_next () in
+    let matches = match_subterm_gen app c csr in
+    let rec match_next_pattern next = match IStream.peek next with
+    | None -> raise PatternMatchingFailure
+    | Some ({ m_sub=lgoal; m_ctx=ctxt }, next) ->
       let lctxt = give_context ctxt id in
       try apply_hyps_context ist env lz goal mt lctxt (adjust lgoal) mhyps hyps
-      with e when is_match_catchable e -> match_next_pattern find_next' () in
-    match_next_pattern (fun () -> match_subterm_gen app c csr) () in
+      with e when is_match_catchable e -> match_next_pattern next in
+    match_next_pattern matches
+  in
   let rec apply_match_goal ist env goal nrs lex lpt =
     begin
       let () = match lex with
@@ -1320,8 +1314,9 @@ and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
 	  | Hyp ((_,hypname),mhyp) -> hypname,  None, mhyp
 	  | Def ((_,hypname),mbod,mhyp) -> hypname, Some mbod, mhyp
 	in
-        let rec match_next_pattern find_next =
-          let s = find_next () in
+        let rec match_next_pattern next = match IStream.peek next with
+        | None -> raise PatternMatchingFailure
+        | Some (s, next) ->
 	  let lids,hyp_match = s.e_ctx in
           db_matched_hyp ist.debug (pf_env goal) hyp_match hypname;
 	  try
@@ -1329,9 +1324,8 @@ and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
             let nextlhyps = List.remove_assoc_in_triple id_match lhyps_rest in
             apply_hyps_context_rec (lfun@lids) s.e_sub nextlhyps tl
           with e when is_match_catchable e ->
-	    match_next_pattern s.e_nxt in
-        let init_match_pattern () =
-          apply_one_mhyp_context ist env goal lmatch hyp_pat lhyps_rest in
+	    match_next_pattern next in
+        let init_match_pattern = apply_one_mhyp_context ist env goal lmatch hyp_pat lhyps_rest in
         match_next_pattern init_match_pattern
     | [] ->
         let lfun = extend_values_with_bindings lmatch (lfun@ist.lfun) in
@@ -1460,14 +1454,14 @@ and interp_genarg_var_list1 ist gl x =
 (* Interprets the Match expressions *)
 and interp_match ist g lz constr lmr =
   let apply_match_subterm app ist (id,c) csr mt =
-    let rec match_next_pattern find_next () =
-      let { m_sub=lmatch; m_ctx=ctxt; m_nxt=find_next' } = find_next () in
+    let rec match_next_pattern next = match IStream.peek next with
+    | None -> raise PatternMatchingFailure
+    | Some ({ m_sub=lmatch; m_ctx=ctxt; }, next) ->
       let lctxt = give_context ctxt id in
       let lfun = extend_values_with_bindings (adjust lmatch) (lctxt@ist.lfun) in
       try eval_with_fail {ist with lfun=lfun} lz g mt
-      with e when is_match_catchable e ->
-        match_next_pattern find_next' () in
-    match_next_pattern (fun () -> match_subterm_gen app c csr) () in
+      with e when is_match_catchable e -> match_next_pattern next in
+    match_next_pattern (match_subterm_gen app c csr) in
   let rec apply_match ist sigma csr = let g = { g with sigma=sigma } in function
     | (All t)::tl ->
         (try eval_with_fail ist lz g t