Commit c8605766 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'issue_221' into 'master'

Better error when matching fails for apply

See merge request !69
parents 04ece33a b1574a30
......@@ -744,7 +744,7 @@ let schedule_transformation c id name args ~callback ~notification =
(* if result is same as input task, consider it as a failure *)
callback (TSfailed (id, NoProgress))
| (Arg_trans _ | Arg_trans_decl _ | Arg_trans_missing _
| Arg_trans_term _ | Arg_trans_term2 _
| Arg_trans_term _ | Arg_trans_term2 _ | Arg_trans_term3 _
| Arg_trans_pattern _ | Arg_trans_type _ | Arg_bad_hypothesis _
| Cannot_infer_type _ | Unnecessary_terms _ | Parse_error _
| Arg_expected _ | Arg_theory_not_found _ | Arg_expected_none _
......
......@@ -212,6 +212,12 @@ let get_exception_message ses id e =
P.print_term t1 (print_opt_type ~print_type:P.print_ty) t1.Term.t_ty
P.print_term t2 (print_opt_type ~print_type:P.print_ty) t2.Term.t_ty,
Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_term3 (s, t1, t2, t3) ->
Pp.sprintf "Error in transformation %s during unification of following two terms:\n %a : %a \n %a : %a\n\n%a is already matched with %a" s
P.print_term t1 (print_opt_type ~print_type:P.print_ty) t1.Term.t_ty
P.print_term t2 (print_opt_type ~print_type:P.print_ty) t2.Term.t_ty
P.print_term t1 P.print_term t3,
Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_pattern (s, pa1, pa2) ->
Pp.sprintf "Error in transformation %s during unification of the following terms:\n %a \n %a"
s P.print_pat pa1 P.print_pat pa2, Loc.dummy_position, ""
......
......@@ -96,12 +96,20 @@ let with_terms ~trans_name subst_ty subst lv withed_terms =
is probably possible to use a simplified version. But don't forget
to unify type variables. (Same comment as at top of this function) *)
try first_order_matching slv lv withed_terms with
| Reduction_engine.NoMatch (Some (t1, t2)) ->
Debug.dprintf debug_matching "Term %a and %a can not be matched. Failure in matching@."
| Reduction_engine.NoMatch (Some (t1, t2, None)) ->
Debug.dprintf debug_matching
"Term %a and %a can not be matched. Failure in matching@."
Pretty.print_term t1 Pretty.print_term t2;
raise (Arg_trans_term2 (trans_name^":matching", t1, t2))
| Reduction_engine.NoMatch (Some (t1, t2, Some t3)) ->
Debug.dprintf debug_matching
"Term %a and %a can not be matched. %a already matched with %a@."
Pretty.print_term t1 Pretty.print_term t2 Pretty.print_term t1
Pretty.print_term t3;
raise (Arg_trans_term3 (trans_name^":matching", t1, t2, t3))
| Reduction_engine.NoMatchpat (Some (p1, p2)) ->
Debug.dprintf debug_matching "Term %a and %a can not be matched. Failure in matching@."
Debug.dprintf debug_matching
"Term %a and %a can not be matched. Failure in matching@."
Pretty.print_pat p1 Pretty.print_pat p2;
raise (Arg_trans_pattern (trans_name, p1, p2))
| Reduction_engine.NoMatch None ->
......@@ -131,18 +139,21 @@ let with_terms ~trans_name subst_ty subst lv withed_terms =
trans_name is used for nice error messages. Errors are returned when the size
of withed_terms is incorrect.
*)
(* TODO Having both slv and lv is redundant but we need both an Svs and the
order of elements: to be improved.
*)
let matching_with_terms ~trans_name lv llet_vs left_term right_term withed_terms =
let slv = List.fold_left (fun acc v -> Svs.add v acc) llet_vs lv in
let (subst_ty, subst) =
try first_order_matching slv [left_term] [right_term] with
| Reduction_engine.NoMatch (Some (t1, t2)) ->
| Reduction_engine.NoMatch (Some (t1, t2, None)) ->
Debug.dprintf debug_matching
"Term %a and %a can not be matched. Failure in matching@."
Pretty.print_term t1 Pretty.print_term t2;
raise (Arg_trans_term2 (trans_name^":no_match", t1, t2))
| Reduction_engine.NoMatch (Some (t1, t2, Some t3)) ->
Debug.dprintf debug_matching
"Term %a and %a can not be matched. %a already matched with %a@."
Pretty.print_term t1 Pretty.print_term t2 Pretty.print_term t1
Pretty.print_term t3;
raise (Arg_trans_term3 (trans_name^":no_match", t1, t2, t3))
| Reduction_engine.NoMatchpat (Some (p1, p2)) ->
Debug.dprintf debug_matching
"Term %a and %a can not be matched. Failure in matching@."
......
......@@ -17,6 +17,7 @@ exception Arg_trans of string
exception Arg_trans_decl of (string * tdecl list)
exception Arg_trans_term of (string * term)
exception Arg_trans_term2 of (string * term * term)
exception Arg_trans_term3 of (string * term * term * term)
exception Arg_trans_pattern of (string * pattern * pattern)
exception Arg_trans_type of (string * Ty.ty * Ty.ty)
exception Arg_trans_missing of (string * Svs.t)
......
......@@ -15,6 +15,7 @@ exception Arg_trans of string
exception Arg_trans_decl of (string * Theory.tdecl list)
exception Arg_trans_term of (string * term)
exception Arg_trans_term2 of (string * term * term)
exception Arg_trans_term3 of (string * term * term * term)
exception Arg_trans_pattern of (string * pattern * pattern)
exception Arg_trans_type of (string * Ty.ty * Ty.ty)
exception Arg_trans_missing of (string * Svs.t)
......
......@@ -296,7 +296,7 @@ type config = {
transformation step. *)
let rec_step_limit = ref 0
exception NoMatch of (term * term) option
exception NoMatch of (term * term * term option) option
exception NoMatchpat of (pattern * pattern) option
let rec pattern_renaming (bound_vars, mt) p1 p2 =
......@@ -349,7 +349,7 @@ let first_order_matching (vars : Svs.t) (largs : term list)
if t_equal t t2 then
loop bound_vars sigma r1 r2
else
raise (NoMatch (Some (t1, t2)))
raise (NoMatch (Some (t1, t2, Some t)))
with Not_found ->
try
let ts = Ty.ty_match mt vs.vs_ty (t_type t2) in
......@@ -357,8 +357,9 @@ let first_order_matching (vars : Svs.t) (largs : term list)
if Mvs.is_empty (Mvs.set_inter bound_vars fv2) then
loop bound_vars (ts,Mvs.add vs t2 mv) r1 r2
else
raise (NoMatch (Some (t1, t2)))
with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2)))
raise (NoMatch (Some (t1, t2, None)))
with Ty.TypeMismatch _ ->
raise (NoMatch (Some (t1, t2, None)))
end
| Tapp(ls1,args1) ->
begin
......@@ -369,9 +370,10 @@ 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 (Some (t1, t2)))
with Ty.TypeMismatch _ ->
raise (NoMatch (Some (t1, t2, None)))
end
| _ -> raise (NoMatch (Some (t1, t2)))
| _ -> raise (NoMatch (Some (t1, t2, None)))
end
| Tquant (q1, bv1) ->
begin
......@@ -385,17 +387,17 @@ let first_order_matching (vars : Svs.t) (largs : term list)
let bound_vars = Mvs.add e2 e1 bound_vars in
(bound_vars,term1, mt)) (bound_vars,term1, mt) vl1 vl2
with Invalid_argument _ | Ty.TypeMismatch _ ->
raise (NoMatch (Some (t1,t2)))
raise (NoMatch (Some (t1,t2,None)))
in
loop bound_vars (mt, mv) (term1 :: r1) (term2 :: r2)
| _ -> raise (NoMatch (Some (t1, t2)))
| _ -> raise (NoMatch (Some (t1, t2, None)))
end
| Tbinop (b1, t1_l, t1_r) ->
begin
match t2.t_node with
| Tbinop (b2, t2_l, t2_r) when b1 = b2 ->
loop bound_vars (mt, mv) (t1_l :: t1_r :: r1) (t2_l :: t2_r :: r2)
| _ -> raise (NoMatch (Some (t1, t2)))
| _ -> raise (NoMatch (Some (t1, t2, None)))
end
| Tif (t11, t12, t13) ->
begin
......@@ -403,7 +405,7 @@ let first_order_matching (vars : Svs.t) (largs : term list)
| Tif (t21, t22, t23) ->
loop bound_vars (mt, mv) (t11 :: t12 :: t13 :: r1)
(t21 :: t22 :: t23 :: r2)
| _ -> raise (NoMatch (Some (t1, t2)))
| _ -> raise (NoMatch (Some (t1, t2, None)))
end
| Tlet (td1, tb1) ->
begin
......@@ -412,11 +414,12 @@ let first_order_matching (vars : Svs.t) (largs : term list)
let (v1, tl1) = t_open_bound tb1 in
let (v2, tl2) = t_open_bound tb2 in
let mt = try Ty.ty_match mt v1.vs_ty v2.vs_ty
with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1,t2))) in
with Ty.TypeMismatch _ ->
raise (NoMatch (Some (t1,t2, None))) in
let bound_vars = Mvs.add v2 v1 bound_vars in
loop bound_vars (mt, mv) (td1 :: tl1 :: r1) (td2 :: tl2 :: r2)
| _ ->
raise (NoMatch (Some (t1, t2)))
raise (NoMatch (Some (t1, t2, None)))
end
| Tcase (ts1, tbl1) ->
begin
......@@ -432,9 +435,9 @@ let first_order_matching (vars : Svs.t) (largs : term list)
) (bound_vars,mt, ts1 :: r1, ts2 :: r2) tbl1 tbl2 in
loop bound_vars (mt,mv) l1 l2
with Invalid_argument _ ->
raise (NoMatch (Some (t1, t2)))
raise (NoMatch (Some (t1, t2, None)))
end
| _ -> raise (NoMatch (Some (t1, t2)))
| _ -> raise (NoMatch (Some (t1, t2, None)))
end
| Teps tb1 ->
begin
......@@ -443,10 +446,11 @@ let first_order_matching (vars : Svs.t) (largs : term list)
let (v1, td1) = t_open_bound tb1 in
let (v2, td2) = t_open_bound tb2 in
let mt = try Ty.ty_match mt v1.vs_ty v2.vs_ty
with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1,t2))) in
with Ty.TypeMismatch _ ->
raise (NoMatch (Some (t1,t2,None))) in
let bound_vars = Mvs.add v2 v1 bound_vars in
loop bound_vars (mt, mv) (td1 :: r1) (td2 :: r2)
| _ -> raise (NoMatch (Some (t1, t2)))
| _ -> raise (NoMatch (Some (t1, t2, None)))
end
| Tnot t1 ->
......@@ -454,7 +458,7 @@ let first_order_matching (vars : Svs.t) (largs : term list)
match t2.t_node with
| Tnot t2 ->
loop bound_vars sigma (t1 :: r1) (t2 :: r2)
| _ -> raise (NoMatch (Some (t1, t2)))
| _ -> raise (NoMatch (Some (t1, t2, None)))
end
| Tvar v1 ->
begin match t2.t_node with
......@@ -463,15 +467,15 @@ let first_order_matching (vars : Svs.t) (largs : term list)
if vs_equal v1 (Mvs.find v2 bound_vars) then
loop bound_vars sigma r1 r2
else
raise (NoMatch (Some (t1, t2)))
raise (NoMatch (Some (t1, t2, None)))
with
Not_found -> assert false
end
| _ -> raise (NoMatch (Some (t1, t2)))
| _ -> raise (NoMatch (Some (t1, t2, None)))
end
| (Tconst _ | Ttrue | Tfalse) when t_equal t1 t2 ->
loop bound_vars sigma r1 r2
| Tconst _ | Ttrue | Tfalse -> raise (NoMatch (Some (t1, t2)))
| Tconst _ | Ttrue | Tfalse -> raise (NoMatch (Some (t1, t2, None)))
end
| _ -> raise (NoMatch None)
in
......
......@@ -118,7 +118,9 @@ val normalize : ?step_limit:int -> limit:int -> engine -> Term.term -> Term.term
open Term
exception NoMatch of (term * term) option
exception NoMatch of (term * term * term option) option
(** [NoMatch (t1, t2, t3)] Cannot match [t1] with [t2]. If [t3] exists then [t1]
is already matched with [t3]. *)
exception NoMatchpat of (pattern * pattern) option
type substitution = term Mvs.t
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment