Completed first_order_matching (case Tcase remains)

Also, added a debug flag to be raised when matching of apply fail.
To do that, I changed exception NoMatch so that it returns the terms
that cant be matched.
This needs some testing.

src/transform/case.ml

@@ -7,6 +7,8 @@ open Task
 open Args_wrapper
 open Reduction_engine
 
+let debug_matching = Debug.register_info_flag "print_match"
+  ~desc:"Print@ terms@ that@ were@ not@ successfully@ matched@ by@ ITP@ tactic@ apply."
 
 let rec dup n x = if n = 0 then [] else x::(dup (n-1) x)
 
@@ -144,8 +146,13 @@ let apply pr : Task.task Trans.tlist = Trans.store (fun task ->
   let t = term_decl d in
   let (lp, lv, nt) = intros t in
   let (_ty, subst) = try first_order_matching lv [nt] [g] with
-    (* TODO export the exception *)
-  | _ -> failwith "Unable to instantiate variables with possible values" in
+  | Reduction_engine.NoMatch (Some (t1, t2)) ->
+      (if (Debug.test_flag debug_matching) then
+        Format.printf "Term %a and %a can not be matched. Failure in matching@."
+          Pretty.print_term t1 Pretty.print_term t2
+      else ()); failwith "Unable to instantiate variables with possible values@."
+  | Reduction_engine.NoMatch None -> failwith "Tactic apply matching failure. Please report@."
+  in
   let inst_nt = t_subst subst nt in
   if (Term.t_equal_nt_nl inst_nt g) then
     let nlp = List.map (t_subst subst) lp in
@@ -189,7 +196,12 @@ let replace_subst lp lv f1 f2 t =
   | None ->
     begin
       let fom = try Some (first_order_matching lv [f1] [t]) with
-      | _ -> None in
+      | Reduction_engine.NoMatch (Some (t1, t2)) ->
+        (if (Debug.test_flag debug_matching) then
+          Format.printf "Term %a and %a can not be matched. Failure in matching@."
+          Pretty.print_term t1 Pretty.print_term t2
+        else ()); None
+      | Reduction_engine.NoMatch None -> None in
         (match fom with
         | None -> t_map (fun t -> replace lv f1 f2 t) t
         | Some (_ty, subst) ->

src/transform/reduction_engine.ml

@@ -299,7 +299,7 @@ type config = {
 }
 
 
-exception NoMatch
+exception NoMatch of (term * term) option
 
 let first_order_matching (vars : Svs.t) (largs : term list)
     (args : term list) : Ty.ty Ty.Mtv.t * substitution =
@@ -319,12 +319,12 @@ let first_order_matching (vars : Svs.t) (largs : term list)
                     if t_equal t t2 then
                       loop sigma r1 r2
                     else
-                      raise NoMatch
+                      raise (NoMatch (Some (t1, t2)))
                 with Not_found ->
                   try
                     let ts = Ty.ty_match mt vs.vs_ty (t_type t2) in
                     loop (ts,Mvs.add vs t2 mv) r1 r2
-                  with Ty.TypeMismatch _ -> raise NoMatch
+                  with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2)))
               end
             | Tvar vs when Mvs.mem vs mv ->
                 begin
@@ -332,7 +332,7 @@ let first_order_matching (vars : Svs.t) (largs : term list)
                   if t_equal t t2 then
                     loop sigma r1 r2
                   else
-                    raise NoMatch
+                    raise (NoMatch (Some (t1, t2)))
                 end
             | Tapp(ls1,args1) ->
               begin
@@ -342,9 +342,9 @@ let first_order_matching (vars : Svs.t) (largs : term list)
                       (List.rev_append args2 r2) in
                     begin
                       try Ty.oty_match mt t1.t_ty t2.t_ty, mv
-                      with Ty.TypeMismatch _ -> raise NoMatch
+                      with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2)))
                     end
-                  | _ -> raise NoMatch
+                  | _ -> raise (NoMatch (Some (t1, t2)))
               end
             | Tquant (q1, bv1) ->
               begin
@@ -357,20 +357,59 @@ let first_order_matching (vars : Svs.t) (largs : term list)
                       let mt = Ty.ty_match mt e1.vs_ty e2.vs_ty in
                       (mt, Mvs.add e1 (t_var e2) mv)) (mt, mv) vl1 vl2 in
                   loop (mt, mv) (term1 :: r1) (term2 :: r2)
-                | _ -> raise NoMatch
+                | _ -> raise (NoMatch (Some (t1, t2)))
               end
             | Tbinop (b1, t1_l, t1_r) ->
               begin
                 match t2.t_node with
                 | Tbinop (b2, t2_l, t2_r) when b1 = b2 ->
                   loop (mt, mv) (t1_l :: t1_r :: r1) (t2_l :: t2_r :: r2)
-                | _ -> raise NoMatch
+                | _ -> raise (NoMatch (Some (t1, t2)))
+              end
+            | Tif (t11, t12, t13) ->
+              begin
+                match t2.t_node with
+                | Tif (t21, t22, t23) ->
+                  loop (mt, mv) (t11 :: t12 :: t13 :: r1) (t21 :: t22 :: t23 :: r2)
+                | _ -> raise (NoMatch (Some (t1, t2)))
+              end
+            | Tlet (t1, tb1) ->
+              begin
+                match t2.t_node with
+                | Tlet (t2, tb2) ->
+                  let (v1, tl1) = t_open_bound tb1 in
+                  let (v2, tl2) = t_open_bound tb2 in
+                  let mt = Ty.ty_match mt v1.vs_ty v2.vs_ty in
+                  let mv = Mvs.add v1 (t_var v2) mv in
+                  loop (mt, mv) (t1 :: tl1 :: r1) (t2 :: tl2 :: r2)
+                | _ ->
+                  raise (NoMatch (Some (t1, t2)))
+              end
+            (* TODO not supported. How do patterns work ? *)
+            | Tcase _ -> raise (NoMatch (Some (t1, t2)))
+            | Teps tb1 ->
+              begin
+                match t2.t_node with
+                | Teps tb2 ->
+                  let (v1, t1) = t_open_bound tb1 in
+                  let (v2, t2) = t_open_bound tb2 in
+                  let mt = Ty.ty_match mt v1.vs_ty v2.vs_ty in
+                  let mv = Mvs.add v1 (t_var v2) mv in
+                  loop (mt, mv) (t1 :: r1) (t2 :: r2)
+                | _ -> raise (NoMatch (Some (t1, t2)))
+              end
+            | Tnot t1 ->
+              begin
+                match t2.t_node with
+                | Tnot t2 ->
+                  loop sigma (t1 :: r1) (t2 :: r2)
+                | _ -> raise (NoMatch (Some (t1, t2)))
               end
             | (Tconst _ | Ttrue | Tfalse) when t_equal t1 t2 ->
                 loop sigma r1 r2
-            | _ -> raise NoMatch
+            | Tvar _ | Tconst _ | Ttrue | Tfalse -> raise (NoMatch (Some (t1, t2)))
         end
-      | _ -> raise NoMatch
+      | _ -> raise (NoMatch None)
   in
   loop (Ty.Mtv.empty, Mvs.empty) largs args
 
@@ -387,7 +426,7 @@ let one_step_reduce engine ls args =
             try
               let sigma = first_order_matching vars largs args in
               sigma,rhs
-            with NoMatch ->
+            with NoMatch _ ->
               loop rem
           end
     in loop rules
@@ -401,7 +440,7 @@ let rec matching ((mt,mv) as sigma) t p =
   | Por(p1,p2) ->
     begin
       try matching sigma t p1
-      with NoMatch -> matching sigma t p2
+      with NoMatch _ -> matching sigma t p2
     end
   | Pas(p,v) -> matching (mt,Mvs.add v t mv) t p
   | Papp(ls1,pl) ->
@@ -410,7 +449,7 @@ let rec matching ((mt,mv) as sigma) t p =
         if ls_equal ls1 ls2 then
           List.fold_left2 matching sigma tl pl
         else
-          if ls2.ls_constr > 0 then raise NoMatch
+          if ls2.ls_constr > 0 then raise (NoMatch None)
           else raise Undetermined
       | _ -> raise Undetermined
 
@@ -528,7 +567,7 @@ and reduce_match st u ~orig tbl sigma cont =
         { value_stack = st;
           cont_stack = (Keval(t,mv''), t_label_copy orig t) :: cont;
         }
-      with NoMatch -> iter rem
+      with NoMatch _ -> iter rem
   in
   try iter tbl with Undetermined ->
     let dmy = t_var (create_vsymbol (Ident.id_fresh "__dmy") (t_type u)) in

src/transform/reduction_engine.mli

@@ -115,6 +115,8 @@ val normalize : limit:int -> engine -> Term.term -> Term.term
 
 open Term
 
+exception NoMatch of (term * term) option
+
 type substitution = term Mvs.t
 
 val first_order_matching: Svs.t -> term list -> term list -> Ty.ty Ty.Mtv.t * substitution