Implementation of Ltac's match and match goal fully based on IStream.

The implementation was partly based on IStream and partly on a control flow with exception. The latter does not mix well with the monadic tactics.

I've moved the algorithmic part of pattern-matching to a new file (tactics/tacticMatching.ml), in order to de-entangle the pattern-matching procedure from the interpretation. This shaves off 300 lines of code from Tacinterp, which is still over 2000 lines of code. It is a first step towards refactoring tacinterp. To be fair, part of what disapeared are lines which sent messages to the debugger. I was not too concerned with them because I understand people found the debugger much too fine-grain on Ltac's pattern matching. But conversely, there may be too few debugging hooks now. This is worth looking into.

In TacticMatching itself, I used a monadic style to express the pattern-matching procedure concisely. I implemented the monad in a fairly brute-force way, using the existing primitive of IStream. It may be worth experimenting with specialized primitive. I am less worried about the monadic style than about the number of allocation of list cells that the primitives entail.

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

5 files changed, 498 insertions, 356 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a2c461731..ffe027474 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -877,10 +877,9 @@ let head_with_value (lvar,lval) =
   in
   head_with_value_rec [] (lvar,lval)
 
-(* Gives a context couple if there is a context identifier *)
-let give_context ctxt = function
-  | None -> Id.Map.empty
-  | Some id -> Id.Map.singleton id (in_gen (topwit wit_constr_context) ctxt)
+(** [interp_context ctxt] interprets a context (as in
+    {!Matching.matching_result}) into a context value of Ltac.  *)
+let interp_context ctxt = in_gen (topwit wit_constr_context) ctxt
 
 (* Reads a pattern by substituting vars of lfun *)
 let use_types = false
@@ -922,104 +921,6 @@ let rec read_match_rule lfun ist env sigma = function
       :: read_match_rule lfun ist env sigma tl
   | [] -> []
 
-(* For Match Context and Match *)
-exception Not_coherent_metas
-exception Eval_fail of std_ppcmds
-
-let is_match_catchable = function
-  | PatternMatchingFailure | Eval_fail _ -> true
-  | e -> Logic.catchable_exception e
-
-let equal_instances gl (ctx',c') (ctx,c) =
-  (* How to compare instances? Do we want the terms to be convertible?
-     unifiable? Do we want the universe levels to be relevant? 
-     (historically, conv_x is used) *)
-  List.equal Id.equal ctx ctx' && pf_conv_x gl c' c
-
-(* Verifies if the matched list is coherent with respect to lcm *)
-(* While non-linear matching is modulo eq_constr in matches, merge of *)
-(* different instances of the same metavars is here modulo conversion... *)
-let verify_metas_coherence gl (ln1,lcm) (ln,lm) =
-  let merge id oc1 oc2 = match oc1, oc2 with
-  | None, None -> None
-  | None, Some c | Some c, None -> Some c
-  | Some c1, Some c2 ->
-    if equal_instances gl c1 c2 then Some c1
-    else raise Not_coherent_metas
-  in
-  (** ppedrot: Is that even correct? *)
-  let merged = ln +++ ln1 in
-  (merged, Id.Map.merge merge lcm lm)
-
-let adjust (l, lc) = (l, Id.Map.map (fun c -> [], c) lc)
-
-type 'a _extended_matching_result =
-    { e_ctx : 'a;
-      e_sub : bound_ident_map * extended_patvar_map; }
-
-let push_id_couple id name env = match name with
-| Name idpat ->
-  Id.Map.add idpat (Value.of_constr (mkVar id)) 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 = Id.Map.empty; e_sub = lmeta; } in
-      IStream.cons ans IStream.empty
-    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 gl lmatch (hypname,patv,pat) lhyps =
-  let rec apply_one_mhyp_context_rec = function
-    | [] ->
-      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
 
 (* misc *)
 
@@ -1281,29 +1182,17 @@ and tactic_of_value ist vle =
   | (VFun _|VRec _) -> Proofview.tclZERO (UserError ("" , str "A fully applied tactic is expected."))
   else Proofview.tclZERO (UserError ("" , str"Expression does not evaluate to a tactic."))
 
-(* Evaluation with FailError catching *)
-and eval_with_fail ist is_lazy tac =
-  Proofview.tclORELSE
-    begin
-      val_interp ist tac >>== fun v ->
-      (if has_type v (topwit wit_tacvalue) then match to_tacvalue v with
-      | VFun (trace,lfun,[],t) when not is_lazy ->
-          let ist = {
-            lfun = lfun;
-            extra = TacStore.set ist.extra f_trace trace; } in
-	  let tac = eval_tactic ist t in
-	  catch_error_tac trace (tac <*> Proofview.Goal.return (of_tacvalue VRTactic))
-      | _ -> Proofview.Goal.return v
-       else Proofview.Goal.return v)
-    end
-    begin function
-      (** FIXME: Should we add [Errors.push]? *)
-      | FailError (0,s)  ->
-          Proofview.tclZERO (Eval_fail (Lazy.force s))
-      | FailError (lvl,s) as e ->
-          Proofview.tclZERO (Exninfo.copy e (FailError (lvl - 1, s)))
-      | e -> Proofview.tclZERO e
-    end
+and eval_value ist tac =
+  val_interp ist tac >>== fun v ->
+  if has_type v (topwit wit_tacvalue) then match to_tacvalue v with
+  | VFun (trace,lfun,[],t) ->
+      let ist = {
+        lfun = lfun;
+        extra = TacStore.set ist.extra f_trace trace; } in
+      let tac = eval_tactic ist t in
+      catch_error_tac trace (tac <*> Proofview.Goal.return (of_tacvalue VRTactic))
+  | _ -> Proofview.Goal.return v
+  else Proofview.Goal.return v
 
 (* Interprets the clauses of a recursive LetIn *)
 and interp_letrec ist llc u =
@@ -1330,136 +1219,85 @@ and interp_letin ist llc u =
   let ist = { ist with lfun } in
   val_interp ist u
 
-(* Interprets the Match Context expressions *)
-and interp_match_goal ist lz lr lmr =
-  Proofview.Goal.enterl begin fun gl ->
-  let sigma = Proofview.Goal.sigma gl in
-  let env = Proofview.Goal.env gl in
-  let hyps = Proofview.Goal.hyps gl in
-  let hyps = if lr then List.rev hyps else hyps in
-  let concl = Proofview.Goal.concl gl in
-  let rec apply_goal_sub app ist (id,c) csr mt mhyps hyps =
-    let rec match_next_pattern next = match IStream.peek next with
-    | None -> Proofview.tclZERO PatternMatchingFailure
-    | Some ({ m_sub=lgoal; m_ctx=ctxt }, next) ->
-      let lctxt = give_context ctxt id in
-      Proofview.tclORELSE
-        (apply_hyps_context ist env lz mt lctxt (adjust lgoal) mhyps hyps)
-        begin function
-          | e when is_match_catchable e -> match_next_pattern next
-          | e -> Proofview.tclZERO e
-        end
+
+(** [interp_match_success lz ist succ] interprets a single matching success
+    (of type {!TacticMatching.t}). *)
+and interp_match_success ist { TacticMatching.subst ; context ; terms ; lhs } =
+  let lctxt = Id.Map.map interp_context context in
+  let hyp_subst = Id.Map.map Value.of_constr terms in
+  let lfun = extend_values_with_bindings subst (lctxt +++ hyp_subst +++ ist.lfun) in
+  eval_value {ist with lfun=lfun} lhs
+
+(** [interp_match_successes lz ist s] interprets the stream of
+    matching of successes [s]. If [lz] is set to true, then only the
+    first success is considered, otherwise further successes are tried
+    if the left-hand side fails. *)
+and interp_match_successes lz ist s =
+    (** iterates [tclORELSE] lazily on the stream [t], if [t] is
+        exhausted, raises [e]. Beware: there is no [tclINDEPENDENT],
+        relying on the fact that it will always be applied to a single
+        goal, by virtue of an earlier [Proofview.Goal.enter]. *)
+    let rec tclORELSE_stream t e =
+      match IStream.peek t with
+      | Some (t1,t') ->
+          Proofview.tclORELSE
+            t1
+            begin fun e ->
+              (* Honors Ltac's failure level. *)
+              Tacticals.New.catch_failerror e <*> tclORELSE_stream t' e
+            end
+      | None ->
+          Proofview.tclZERO e
     in
-    match_next_pattern (match_subterm_gen app c csr) in
-  let rec apply_match_goal ist env nrs lex lpt =
-    begin
-      begin match lex with
-      | r :: _ -> Proofview.tclLIFT (db_pattern_rule (curr_debug ist) nrs r)
-      | _ -> Proofview.tclUNIT ()
-      end <*>
-      match lpt with
-      | (All t)::tl ->
-	  begin
-            Proofview.tclLIFT (db_mc_pattern_success (curr_debug ist)) <*>
-            Proofview.tclORELSE (eval_with_fail ist lz t)
-              begin function
-                | e when is_match_catchable e ->
-	      apply_match_goal ist env (nrs+1) (List.tl lex) tl
-                | e -> Proofview.tclZERO e
-              end
-	  end
-      | (Pat (mhyps,mgoal,mt))::tl ->
-          let mhyps = List.rev mhyps (* Sens naturel *) in
-	  begin match mgoal with
-          | Term mg ->
-              let matches =
-                try Some (extended_matches mg concl)
-                with PatternMatchingFailure -> None
-              in
-                            begin match matches with
-              | None ->
-                Proofview.tclLIFT (db_matching_failure (curr_debug ist)) <*>
-                apply_match_goal ist env (nrs+1) (List.tl lex) tl
-              | Some lmatch ->
-                Proofview.tclORELSE
-                  begin
-                    Proofview.tclLIFT (db_matched_concl (curr_debug ist) env concl) <*>
-                    apply_hyps_context ist env lz mt Id.Map.empty lmatch mhyps hyps
-                  end
-                 begin function
-                   | e when is_match_catchable e ->
-                       (Proofview.tclLIFT (match e with
-                       | PatternMatchingFailure -> db_matching_failure (curr_debug ist)
-                       | Eval_fail s -> db_eval_failure (curr_debug ist) s
-                       | _ -> db_logic_failure (curr_debug ist) e) <*>
-                        apply_match_goal ist env (nrs+1) (List.tl lex) tl)
-                   | e -> Proofview.tclZERO e
-                 end
-                end
-	  | Subterm (b,id,mg) ->
-	      Proofview.tclORELSE (apply_goal_sub b ist (id,mg) concl mt mhyps hyps)
-                begin function
-	       | PatternMatchingFailure ->
-		   apply_match_goal ist env (nrs+1) (List.tl lex) tl
-               | e -> Proofview.tclZERO e
-                end
-          end
-      | _ ->
-          Proofview.tclZERO (UserError (
-	    "Tacinterp.apply_match_goal" ,
-            (v 0 (str "No matching clauses for match goal" ++
-		    (if curr_debug ist==DebugOff then
-			fnl() ++ str "(use \"Set Ltac Debug\" for more info)"
-		     else mt()) ++ str"."))
-          ))
-    end in
-  apply_match_goal ist env 0 lmr
-    (read_match_rule (extract_ltac_constr_values ist env)
-       ist env sigma lmr)
+    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 *)
+      begin match IStream.peek successes with
+      | Some (s,_) -> s
+      | None -> Proofview.tclZERO matching_failure
+      end
+    else
+      (** match *)
+      tclORELSE_stream successes matching_failure
+
+
+(* Interprets the Match expressions *)
+and interp_match ist lz constr lmr =
+  begin Proofview.tclORELSE
+    (interp_ltac_constr ist constr)
+    begin function
+      | e ->
+          (* spiwack: [Errors.push] here is unlikely to do what
+             it's intended to, or anything meaningful for that
+             matter. *)
+          let e = Errors.push e in
+          Proofview.tclLIFT (debugging_exception_step ist true e
+          (fun () -> str "evaluation of the matched expression")) <*>
+          Proofview.tclZERO e
+    end
+  end >>== fun constr ->
+  Proofview.Goal.enterl begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
+    interp_match_successes lz ist (TacticMatching.match_term env sigma constr ilr)
   end
 
-(* Tries to match the hypotheses in a Match Context *)
-and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps =
+(* Interprets the Match Context expressions *)
+and interp_match_goal ist lz lr lmr =
   Proofview.Goal.enterl begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-  let rec apply_hyps_context_rec lfun lmatch lhyps_rest = function
-    | hyp_pat::tl ->
-	let (hypname, _, pat as hyp_pat) =
-	  match hyp_pat with
-	  | Hyp ((_,hypname),mhyp) -> hypname,  None, mhyp
-	  | Def ((_,hypname),mbod,mhyp) -> hypname, Some mbod, mhyp
-	in
-        let rec match_next_pattern next = match IStream.peek next with
-        | None ->
-          Proofview.tclLIFT (db_hyp_pattern_failure (curr_debug ist) env (hypname, pat)) <*>
-          Proofview.tclZERO PatternMatchingFailure
-        | Some (s, next) ->
-          let lids, hyp_match = s.e_ctx in
-          Proofview.tclLIFT (db_matched_hyp (curr_debug ist) env hyp_match hypname) <*>
-          Proofview.tclORELSE
-            begin
-              let id_match = pi1 hyp_match in
-              let select_match (id,_,_) = Id.equal id id_match in
-              let nextlhyps = List.remove_first select_match lhyps_rest in
-              let lfun = lfun +++ lids in
-              apply_hyps_context_rec lfun s.e_sub nextlhyps tl
-            end
-            begin function
-              | e when is_match_catchable e ->
-                  match_next_pattern next
-              | e -> Proofview.tclZERO e
-            end
-        in
-        let init_match_pattern = Tacmach.New.of_old (fun gl ->
-          apply_one_mhyp_context gl lmatch hyp_pat lhyps_rest) gl in
-        match_next_pattern init_match_pattern
-    | [] ->
-        let lfun = lfun +++ ist.lfun in
-        let lfun = extend_values_with_bindings lmatch lfun in
-        Proofview.tclLIFT (db_mc_pattern_success (curr_debug ist)) <*>
-        eval_with_fail {ist with lfun=lfun} lz mt
-  in
-  apply_hyps_context_rec lctxt lgmatch hyps mhyps
+    let hyps = Proofview.Goal.hyps gl in
+    let hyps = if lr then List.rev hyps else hyps in
+    let concl = Proofview.Goal.concl gl in
+    let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
+    interp_match_successes lz ist (TacticMatching.match_goal env sigma hyps concl ilr)
   end
 
 and interp_external loc ist gl com req la =
@@ -1541,112 +1379,6 @@ and interp_genarg_var_list ist gl x =
   let lc = interp_hyp_list ist gl lc in
   in_gen (topwit (wit_list wit_var)) lc
 
-(* Interprets the Match expressions *)
-and interp_match ist lz constr lmr =
-  let apply_match_subterm app ist (id,c) csr mt =
-    let rec match_next_pattern next = match IStream.peek next with
-    | None -> Proofview.tclZERO 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
-      Proofview.tclORELSE
-        (eval_with_fail {ist with lfun=lfun} lz mt)
-        begin function
-          | e when is_match_catchable e ->
-              match_next_pattern next
-          | e -> Proofview.tclZERO e
-        end
-    in
-    match_next_pattern (match_subterm_gen app c csr) in
-
-  let rec apply_match ist csr = function
-    | (All t)::tl ->
-        Proofview.tclORELSE
-        (eval_with_fail ist lz t)
-          begin function
-            | e when is_match_catchable e -> apply_match ist csr tl
-            | e -> Proofview.tclZERO e
-          end
-    | (Pat ([],Term c,mt))::tl ->
-        let matches =
-          try Some (extended_matches c csr)
-          with PatternMatchingFailure -> None
-        in
-        Proofview.tclORELSE begin match matches with
-        | None -> let e = PatternMatchingFailure in
-                  (Proofview.Goal.enter begin fun gl ->
-                   let env = Proofview.Goal.env gl in
-                   Proofview.tclLIFT begin
-                     debugging_exception_step ist false e (fun () ->
-                       str "matching with pattern" ++ fnl () ++
-                         pr_constr_pattern_env env c)
-                   end
-                  end) <*> Proofview.tclZERO e
-        | Some lmatch ->
-           Proofview.tclORELSE
-             begin
-               let lfun = extend_values_with_bindings lmatch ist.lfun in
-               eval_with_fail { ist with lfun=lfun } lz mt
-             end
-             begin function
-               | e ->
-                   (Proofview.Goal.enter begin fun gl ->
-                     let env = Proofview.Goal.env gl in
-                     Proofview.tclLIFT begin
-                       debugging_exception_step ist false e (fun () ->
-                         str "rule body for pattern" ++
-                           pr_constr_pattern_env env c)
-                     end
-                   end) <*>
-                   Proofview.tclZERO e
-             end
-        end
-        begin function 
-          | e when is_match_catchable e ->
-              Proofview.tclLIFT (debugging_step ist (fun () -> str "switching to the next rule")) <*>
-              apply_match ist csr tl
-          | e -> Proofview.tclZERO e
-        end
-
-    | (Pat ([],Subterm (b,id,c),mt))::tl ->
-        Proofview.tclORELSE
-          (apply_match_subterm b ist (id,c) csr mt)
-          begin function
-            | PatternMatchingFailure -> apply_match ist csr tl
-            | e -> Proofview.tclZERO e
-          end
-    | _ ->
-        Proofview.tclZERO (UserError ("Tacinterp.apply_match" , str
-                                                "No matching clauses for match.")) in
-  begin Proofview.tclORELSE
-    (interp_ltac_constr ist constr)
-    begin function
-      | e ->
-          (* spiwack: [Errors.push] here is unlikely to do what
-             it's intended to, or anything meaningful for that
-             matter. *)
-          let e = Errors.push e in
-          Proofview.tclLIFT (debugging_exception_step ist true e
-          (fun () -> str "evaluation of the matched expression")) <*>
-          Proofview.tclZERO e
-    end
-  end >>== fun csr ->
-  Proofview.Goal.enterl begin fun gl ->
-    let env = Proofview.Goal.env gl in
-    let sigma = Proofview.Goal.sigma gl in
-    let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
-    Proofview.tclORELSE
-      (apply_match ist csr ilr)
-      begin function
-        | e ->
-            Proofview.tclLIFT (debugging_exception_step ist true e (fun () -> str "match expression")) <*>
-            Proofview.tclZERO e
-      end >>== fun res ->
-      Proofview.tclLIFT (debugging_step ist (fun () ->
-        str "match expression returns " ++ pr_value (Some env) res)) <*>
-      (Proofview.Goal.return res)
-  end
-
 (* Interprets tactic expressions : returns a "constr" *)
 and interp_ltac_constr ist e =
   begin Proofview.tclORELSE
diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml
new file mode 100644
index 000000000..8d9503318
--- /dev/null
+++ b/tactics/tacticMatching.ml
@@ -0,0 +1,357 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This file extends Matching with the main logic for Ltac's
+    (lazy)match and (lazy)match goal. *)
+
+open Tacexpr
+
+(** [t] is the type of matching successes. It ultimately contains a
+    {!Tacexpr.glob_tactic_expr} representing the left-hand side of the
+    corresponding matching rule, a matching substitution to be
+    applied, a context substitution mapping identifier to context like
+    those of {!Matching.matching_result}), and a {!Term.constr}
+    substitution mapping corresponding to matched hypotheses. *)
+type 'a t = {
+  subst : Matching.bound_ident_map * Pattern.extended_patvar_map ;
+  context : Term.constr Names.Id.Map.t;
+  terms : Term.constr Names.Id.Map.t;
+  lhs : 'a;
+}
+
+
+
+(** {6 Utilities} *)
+
+
+(** Some of the functions of {!Matching} return the substitution with a
+    [patvar_map] instead of an [extended_patvar_map]. [adjust] coerces
+    substitution of the former type to the latter. *)
+let adjust : Matching.bound_ident_map * Pattern.patvar_map ->
+             Matching.bound_ident_map * Pattern.extended_patvar_map = fun (l, lc) ->
+  (l, Names.Id.Map.map (fun c -> [], c) lc)
+
+
+(** Adds a binding to a {!Names.Id.Map.t} if the identifier is [Some id] *)
+let id_map_try_add id x m =
+  match id with
+  | Some id -> Names.Id.Map.add id x m
+  | None -> m
+
+(** Adds a binding to a {!Names.Id.Map.t} if the name is [Name id] *)
+let id_map_try_add_name id x m =
+  let open Names.Name in
+  match id with
+  | Name id -> Names.Id.Map.add id x m
+  | Anonymous -> m
+
+(** Takes the union of two {!Names.Id.Map.t}. If there is conflict,
+    the binding of the right-hand argument shadows that of the left-hand
+    argument. *)
+let id_map_right_biased_union m1 m2 =
+    Names.Id.Map.merge begin fun _ x1 x2 ->
+      match x1 , x2 with
+      | _ , Some x | Some x , None -> Some x
+      | _ , _ -> None
+    end m1 m2
+
+(** Tests whether the substitution [s] is empty. *)
+let is_empty_subst (ln,lm) =
+  Names.Id.Map.(is_empty ln && is_empty lm)
+
+(** {6 Non-linear patterns} *)
+
+
+(** The patterns of Ltac are not necessarily linear. Non-linear
+    pattern are partially handled by the {!Matching} module, however
+    goal patterns are not primitive to {!Matching}, hence we must deal
+    with non-linearity between hypotheses and conclusion. Subterms are
+    considered equal up to the equality implemented in
+    [equal_instances]. *)
+(* spiwack: it doesn't seem to be quite the same rule for non-linear
+   term patterns and non-linearity between hypotheses and/or
+   conclusion. Indeed, in [Matching], matching is made modulo
+   syntactic equality, and here we merge modulo conversion. It may be
+   a good idea to have an entry point of [Matching] with a partial
+   substitution as argument instead of merging substitution here. That
+   would ensure consistency. *)
+let equal_instances env sigma (ctx',c') (ctx,c) =
+  (* How to compare instances? Do we want the terms to be convertible?
+     unifiable? Do we want the universe levels to be relevant? 
+     (historically, conv_x is used) *)
+  CList.equal Names.Id.equal ctx ctx' && Reductionops.is_conv env sigma c' c
+
+
+(** Merges two substitutions. Raises [Not_coherent_metas] when
+    encountering two instances of the same metavariable which are not
+    equal according to {!equal_instances}. *)
+exception Not_coherent_metas
+let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) =
+  let merge id oc1 oc2 = match oc1, oc2 with
+    | None, None -> None
+    | None, Some c | Some c, None -> Some c
+    | Some c1, Some c2 ->
+        if equal_instances env sigma c1 c2 then Some c1
+        else raise Not_coherent_metas
+  in
+  let (+++) lfun1 lfun2 = Names.Id.Map.fold Names.Id.Map.add lfun1 lfun2 in
+  (** ppedrot: Is that even correct? *)
+  let merged = ln +++ ln1 in
+  (merged, Names.Id.Map.merge merge lcm lm)
+
+
+(** A functor is introduced to share the environment and the
+    evar_map. They do not change and it would be a pity to introduce
+    closures everywhere just for the occasional calls to
+    {!equal_instances}. *)
+module type StaticEnvironment = sig
+  val env : Environ.env
+  val sigma : Evd.evar_map
+end
+module PatternMatching (E:StaticEnvironment) = struct
+
+
+  (** {6 The pattern-matching monad } *)
+
+
+  (** To focus on the algorithmic portion of pattern-matching, the
+      bookkeeping is relegated to a monad: the composition of the
+      bactracking monad of {!IStream.t} with a "writer" effect. *)
+  (* spiwack: as we don't benefit from the various stream optimisations
+     of Haskell, it may be costly to give the monad in direct style such as
+     here. We may want to use some continuation passing style. *)
+  type 'a m = 'a t IStream.t
+
+
+  (** The empty substitution. *)
+  let empty_subst = Names.Id.Map.empty , Names.Id.Map.empty
+
+  (** Composes two substitutions using {!verify_metas_coherence}. It
+      must be a monoid with neutral element {!empty_subst}. Raises
+      [Not_coherent_metas] when composition cannot be achieved. *)
+  let subst_prod s1 s2 =
+    if is_empty_subst s1 then s2
+    else if is_empty_subst s2 then s1
+    else verify_metas_coherence E.env E.sigma s1 s2
+
+  (** The empty context substitution. *)
+  let empty_context_subst = Names.Id.Map.empty
+
+  (** Compose two context substitutions, in case of conflict the
+      right hand substitution shadows the left hand one. *)
+  let context_subst_prod = id_map_right_biased_union
+
+  (** The empty term substitution. *)
+  let empty_term_subst = Names.Id.Map.empty
+
+  (** Compose two terms substitutions, in case of conflict the
+      right hand substitution shadows the left hand one. *)
+  let term_subst_prod = id_map_right_biased_union
+
+
+  (** Monadic [return]: returns a single success with empty substitutions. *)
+  let return (type a) (lhs:a) : a m =
+    let success = {
+      subst = empty_subst ;
+      context = empty_context_subst ;
+      terms = empty_term_subst ;
+      lhs = lhs ; }
+    in
+    IStream.(cons success empty)
+
+  (** Monadic bind: each success of [x] is replaced by the successes
+      of [f x]. The substitutions of [x] and [f x] are composed,
+      dropping the apparent successes when the substitutions are not
+      coherent. *)
+  let (>>=) (type a) (type b) (x:a m) (f:a -> b m) : b m =
+    let open IStream in
+    concat (map begin fun { subst=substx; context=contextx; terms=termsx; lhs=lhsx } ->
+      map_filter begin fun { subst=substf; context=contextf; terms=termsf; lhs=lhsf } ->
+        try 
+          Some { 
+            subst = subst_prod substx substf ;
+            context = context_subst_prod contextx contextf ;
+            terms = term_subst_prod termsx termsf ;
+            lhs = lhsf
+          }
+        with Not_coherent_metas -> None
+      end (f lhsx)
+    end x)
+
+  (** A variant of [(>>=)] when the first argument returns [unit]. *)
+  let (<*>) (type a) (x:unit m) (y:a m) : a m =
+    x >>= fun () -> y
+
+  (** Failure of the pattern-matching monad: no success. *)
+  let fail (type a) : a m = IStream.empty
+
+  (** Chooses in a list, in the same order as the list *)
+  let pick (type a) (l:a list) : a m =
+    IStream.map begin fun x ->
+      { subst = empty_subst ;
+        context = empty_context_subst ;
+        terms = empty_term_subst ;
+        lhs = x }
+    end (IStream.of_list l)
+
+  (** Declares a subsitution, a context substitution and a term substitution. *)
+  let put subst context terms : unit m =
+    IStream.(cons { subst ; context ; terms ; lhs = () } empty)
+
+  (** Declares a substitution. *)
+  let put_subst subst : unit m = put subst empty_context_subst empty_term_subst
+
+  (** Declares a context substitution. *)
+  let put_context context : unit m = put empty_subst context empty_term_subst
+
+  (** Declares a term substitution. *)
+  let put_terms terms : unit m = put empty_subst empty_context_subst terms
+
+
+
+  (** {6 Pattern-matching} *)
+
+
+  (** [wildcard_match_term lhs] matches a term against a wildcard
+      pattern ([_ => lhs]). It has a single success with an empty
+      substitution. *)
+  let wildcard_match_term = return
+
+  (** [pattern_match_term refresh pat term lhs] returns the possible
+      matchings of [term] with the pattern [pat => lhs]. If refresh is
+      true, refreshes the universes of [term]. *)
+  let pattern_match_term refresh pat term lhs = 
+    let term = if refresh then Termops.refresh_universes_strict term else term in
+    match pat with
+    | Term p ->
+        begin 
+          try
+            put_subst (Matching.extended_matches p term) <*>
+            return lhs
+          with Matching.PatternMatchingFailure -> fail
+        end
+    | Subterm (with_app_context,id_ctxt,p) ->
+        (* spiwack: this branch is easier in direct style, would need to be
+           changed if the implementation of the monad changes. *)
+        IStream.map begin fun { Matching.m_sub ; m_ctx } ->
+          let subst = adjust m_sub in
+          let context = id_map_try_add id_ctxt m_ctx Names.Id.Map.empty in
+          let terms = empty_term_subst in
+          { subst ; context ; terms ; lhs }
+        end (Matching.match_subterm_gen with_app_context p term)
+
+
+  (** [rule_match_term term rule] matches the term [term] with the
+      matching rule [rule]. *)
+  let rule_match_term term = function
+    | All lhs -> wildcard_match_term lhs
+    | Pat ([],pat,lhs) -> pattern_match_term false pat term lhs
+    | Pat _ ->
+        (** Rules with hypotheses, only work in match goal. *)
+        fail
+
+  (** [match_term term rules] matches the term [term] with the set of
+      matching rules [rules].*)
+  let match_term term rules =
+    IStream.(concat (map (fun r -> rule_match_term term r) (of_list rules)))
+
+
+
+
+  (** [hyp_match_type hypname pat hyps] matches a single
+      hypothesis pattern [hypname:pat] against the hypotheses in
+      [hyps]. Tries the hypotheses in order. For each success returns
+      the name of the matched hypothesis. *)
+  let hyp_match_type hypname pat hyps =
+    pick hyps >>= fun (id,b,hyp) ->
+    let refresh = not (Option.is_empty b) in
+    pattern_match_term refresh pat hyp () <*>
+    put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
+    return id
+
+  (** [hyp_match_type hypname bodypat typepat hyps] matches a single
+      hypothesis pattern [hypname := bodypat : typepat] against the
+      hypotheses in [hyps].Tries the hypotheses in order. For each
+      success returns the name of the matched hypothesis. *)
+  let hyp_match_body_and_type hypname bodypat typepat hyps =
+    pick hyps >>= function
+      | (id,Some body,hyp) ->
+          pattern_match_term false bodypat body () <*>
+          pattern_match_term true typepat hyp () <*>
+          put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
+          return id
+      | (id,None,hyp) -> fail
+
+  (** [hyp_match pat hyps] dispatches to
+      {!hyp_match_type} or {!hyp_match_body_and_type} depending on whether
+      [pat] is [Hyp _] or [Def _]. *)
+  let hyp_match pat hyps =
+    match pat with
+    | Hyp ((_,hypname),typepat) ->
+        hyp_match_type hypname typepat hyps
+    | Def ((_,hypname),bodypat,typepat) ->
+        hyp_match_body_and_type hypname bodypat typepat hyps
+
+  (** [hyp_pattern_list_match pats hyps lhs], matches the list of
+      patterns [pats] against the hypotheses in [hyps], and eventually
+      returns [lhs]. *)
+  let rec hyp_pattern_list_match pats hyps lhs =
+    match pats with
+    | pat::pats ->
+        hyp_match pat hyps >>= fun matched_hyp ->
+        (* spiwack: alternatively it is possible to return the list
+           with the matched hypothesis removed directly in
+           [hyp_match]. *)
+        let select_matched_hyp (id,_,_) = Names.Id.equal id matched_hyp in
+        let hyps = CList.remove_first select_matched_hyp hyps in
+        hyp_pattern_list_match pats hyps lhs
+    | [] -> return lhs
+
+  (** [rule_match_goal hyps concl rule] matches the rule [rule]
+      against the goal [hyps|-concl]. *)
+  let rule_match_goal hyps concl = function
+    | All lhs -> wildcard_match_term lhs
+    | Pat (hyppats,conclpat,lhs) ->
+        (* the rules are applied from the topmost one (in the concrete
+           syntax) to the bottommost. *)
+        let hyppats = List.rev hyppats in
+        pattern_match_term false conclpat concl () <*>
+        hyp_pattern_list_match hyppats hyps lhs
+
+  (** [match_goal hyps concl rules] matches the goal [hyps|-concl]
+      with the set of matching rules [rules]. *)
+  let match_goal hyps concl rules =
+    IStream.(concat (map (fun r -> rule_match_goal hyps concl r) (of_list rules)))
+
+end
+
+(** [match_term env sigma term rules] matches the term [term] with the
+    set of matching rules [rules]. The environment [env] and the
+    evar_map [sigma] are not currently used, but avoid code
+    duplication. *)
+let match_term env sigma term rules =
+  let module E = struct
+    let env = env
+    let sigma = sigma
+  end in
+  let module M = PatternMatching(E) in
+  M.match_term term rules
+
+
+(** [match_goal env sigma hyps concl rules] matches the goal
+    [hyps|-concl] with the set of matching rules [rules]. The
+    environment [env] and the evar_map [sigma] are used to check
+    convertibility for pattern variables shared between hypothesis
+    patterns or the conclusion pattern. *)
+let match_goal env sigma hyps concl rules =
+  let module E = struct
+    let env = env
+    let sigma = sigma
+  end in
+  let module M = PatternMatching(E) in
+  M.match_goal hyps concl rules
diff --git a/tactics/tacticMatching.mli b/tactics/tacticMatching.mli
new file mode 100644
index 000000000..1b440e195
--- /dev/null
+++ b/tactics/tacticMatching.mli
@@ -0,0 +1,49 @@
+ (************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This file extends Matching with the main logic for Ltac's
+    (lazy)match and (lazy)match goal. *)
+
+
+(** [t] is the type of matching successes. It ultimately contains a
+    {!Tacexpr.glob_tactic_expr} representing the left-hand side of the
+    corresponding matching rule, a matching substitution to be
+    applied, a context substitution mapping identifier to context like
+    those of {!Matching.matching_result}), and a {!Term.constr}
+    substitution mapping corresponding to matched hypotheses. *)
+type 'a t = {
+  subst : Matching.bound_ident_map * Pattern.extended_patvar_map ;
+  context : Term.constr Names.Id.Map.t;
+  terms : Term.constr Names.Id.Map.t;
+  lhs : 'a;
+}
+
+
+(** [match_term env sigma term rules] matches the term [term] with the
+    set of matching rules [rules]. The environment [env] and the
+    evar_map [sigma] are not currently used, but avoid code
+    duplication. *)
+val match_term :
+  Environ.env ->
+  Evd.evar_map ->
+  Term.constr ->
+  (Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
+   Tacexpr.glob_tactic_expr t IStream.t
+
+(** [match_goal env sigma hyps concl rules] matches the goal
+    [hyps|-concl] with the set of matching rules [rules]. The
+    environment [env] and the evar_map [sigma] are used to check
+    convertibility for pattern variables shared between hypothesis
+    patterns or the conclusion pattern. *)
+val match_goal:
+  Environ.env ->
+  Evd.evar_map ->
+  Context.named_context ->
+  Term.constr ->
+  (Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
+   Tacexpr.glob_tactic_expr t IStream.t
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index f1e8a3403..310023e54 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -189,6 +189,9 @@ val case_on_ba : (branch_assumptions -> tactic) -> branch_args  -> tactic
 module New : sig
   open Proofview
 
+  (** [catch_failerror e] fails and decreases the level if [e] is an
+      Ltac error with level more than 0. Otherwise succeeds. *)
+  val catch_failerror : exn -> unit tactic
 
   val tclTHEN : unit tactic -> unit tactic -> unit tactic
   (* [tclFAIL n msg] fails with [msg] as an error message at level [n]
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 38fa2bc73..7fe584ec1 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -19,6 +19,7 @@ Tacsubst
 Taccoerce
 Tacintern
 Tacenv
+TacticMatching
 Tacinterp
 Evar_tactics
 Autorewrite