diff options
| author | Pierre-Marie Pédrot | 2014-07-03 10:34:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-07-03 16:07:59 +0200 |
| commit | b17fb013f1810106b8cd88a12a2df3f26dc7c289 (patch) | |
| tree | 60ee5af1548858855b00a15c92acec384b03303f | |
| parent | f222f46e7d231c5afe72e146de92dc8dcadbdcb6 (diff) | |
More efficient implementation of Ltac match, by inlining a stream map.
| -rw-r--r-- | tactics/tacinterp.ml | 34 |
1 files changed, 15 insertions, 19 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 06ec278cc3..c749e2d720 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1241,32 +1241,28 @@ and interp_match_successes lz ist s : typed_generic_argument GTac.t = let rec tclOR_stream t e = let open IStream in match peek t with + | Nil -> Proofview.tclZERO e | Cons (t1,t') -> Proofview.tclORELSE - t1 + (interp_match_success ist t1) begin fun e -> (* Honors Ltac's failure level. *) Tacticals.New.catch_failerror e <*> tclOR_stream t' e end - | Nil -> - Proofview.tclZERO e in - let matching_failure = - UserError ("Tacinterp.apply_match" , str "No matching clauses for match.") - in - let successes = - IStream.map (fun s -> interp_match_success ist s) s - in - if lz then - (** lazymatch *) - let open IStream in - begin match peek successes with - | Cons (s,_) -> s - | Nil -> Proofview.tclZERO matching_failure - end - else - (** match *) - Proofview.tclONCE (tclOR_stream successes matching_failure) + let matching_failure = + UserError ("Tacinterp.apply_match" , str "No matching clauses for match.") + in + if lz then + (** lazymatch *) + let open IStream in + begin match peek s with + | Cons (s,_) -> interp_match_success ist s + | Nil -> Proofview.tclZERO matching_failure + end + else + (** match *) + Proofview.tclONCE (tclOR_stream s matching_failure) (* Interprets the Match expressions *) |