1 files changed, 47 insertions, 0 deletions
diff --git a/rewrite.ml4 b/rewrite.ml4
index 6229262..383d706 100644
--- a/rewrite.ml4
+++ b/rewrite.ml4
@@ -32,6 +32,10 @@ let push_anomaly msg = function
   | Util.Anomaly _ as e -> raise e
   | _ -> Coq.anomaly msg
 
+
+
+
+
 module M = Matcher
 
 open Term
@@ -435,6 +439,41 @@ let aac_rewrite  ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict
     ) goal
 
 
+(** [aac_match eq (fun x1 ... xn => p) t H] match the term [t] against
+    the pattern, and introduces an hypothesis H of type p = t.  (Note
+    that we have performed the substitution in p).
+*)
+
+let aac_match ~eq pattern term h = fun gl ->
+  let env = Tacmach.pf_env gl in
+  let evar_map = Tacmach.project gl in
+  let carrier = Typing.type_of env evar_map term in   
+  let rel = Coq.Relation.make carrier eq in
+  let equiv,gl = Coq.Equivalence.from_relation gl rel in 
+  (* first, we decompose the pattern as an arity. *)
+  let x_args, pat = Term.decompose_lam pattern in 
+  (* then, we reify the pattern and the term, using the provided equality *)
+  let envs = Theory.Trans.empty_envs () in
+  let left, right,gl = Theory.Trans.t_of_constr gl rel envs (pat,term) in 
+  let gl,ir = Theory.Trans.ir_of_envs gl rel envs in 
+  let solutions = Matcher.matcher (Theory.Trans.ir_to_units ir) left right in 
+  (* then, we pick the first solution   to the matching problem *)
+  let sigma = match Search_monad.choose solutions with
+    | None -> Coq.user_error "no solution to the matching problem"
+    | Some sigma -> sigma
+  in
+  let p_sigma = Matcher.Subst.instantiate sigma left in 
+  let args = List.map (fun (x,t) -> x,Theory.Trans.raw_constr_of_t ir rel [] t) (Matcher.Subst.to_list sigma) in 
+  (* Then, we have to assert the fact that p_sigma is equal to term *)
+  let equation = mkApp (eq, [| Theory.Trans.raw_constr_of_t ir rel [] p_sigma ; term |]) in 
+  let evar_map = Tacmach.project gl in
+  Tacticals.tclTHENLIST 
+    [      
+      Refiner.tclEVARS evar_map;
+      Tactics.assert_by h  equation (by_aac_reflexivity term equiv ir p_sigma right);
+    ] gl
+  
+
 open Coq.Rewrite
 open Tacmach
 open Tacticals
@@ -522,3 +561,11 @@ TACTIC EXTEND _aacu_instances_
 | [ "aacu_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
   [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl ]
 END
+
+TACTIC EXTEND _aac_match_
+| [ "aac_match" constr(p) constr(t) ident(h)] ->
+  [ fun gl ->
+    let ty = Tacmach.pf_type_of gl t in 
+    let eq = Coq.Leibniz.eq ty in 
+    aac_match ~eq p t (Names.Name h) gl]
+END