Ty.TypeMismatch now carries two type expressions

src/core/decl.ml

@@ -275,7 +275,7 @@ let create_ind_decl idl =
     match f.f_node with
       | Fapp (s, tl) when ls_equal s ps ->
           let mtch sb t ty =
-            try ty_match sb (t.t_ty) ty with TypeMismatch ->
+            try ty_match sb (t.t_ty) ty with TypeMismatch _ ->
               raise (TooSpecificIndDecl (ps, pr, t))
           in
           ignore (List.fold_left2 mtch Mtv.empty tl ps.ls_args);

src/core/term.ml

@@ -142,9 +142,12 @@ let pat_map fn pat = match pat.pat_node with
   | Papp (s, pl) -> pat_app s (List.map fn pl) pat.pat_ty
   | Pas (p, v) -> pat_as (fn p) v
 
+let check_ty_equal ty1 ty2 =
+  if not (ty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))
+
 let protect fn pat =
   let res = fn pat in
-  if not (ty_equal res.pat_ty pat.pat_ty) then raise TypeMismatch;
+  check_ty_equal pat.pat_ty res.pat_ty;
   res
 
 let pat_map fn = pat_map (protect fn)
@@ -184,7 +187,7 @@ let pat_app fs pl ty =
   pat_app fs pl ty
 
 let pat_as p v =
-  if not (ty_equal p.pat_ty v.vs_ty) then raise TypeMismatch;
+  check_ty_equal p.pat_ty v.vs_ty;
   pat_as p v
 
 (* symbol-wise map/fold *)
@@ -558,7 +561,7 @@ let f_map_unsafe fnT fnF lvl f = f_label_copy f (match f.f_node with
 
 let protect fn lvl t =
   let res = fn lvl t in
-  if not (ty_equal res.t_ty t.t_ty) then raise TypeMismatch;
+  check_ty_equal t.t_ty res.t_ty;
   res
 
 let t_map_unsafe fnT = t_map_unsafe (protect fnT)
@@ -649,11 +652,11 @@ let f_app ps tl =
   f_app ps tl
 
 let p_check t p =
-  if not (ty_equal p.pat_ty t.t_ty) then raise TypeMismatch
+  check_ty_equal p.pat_ty t.t_ty
 
 let t_case tl bl ty =
   let t_check_branch (pl,_,tbr) =
-    if not (ty_equal tbr.t_ty ty) then raise TypeMismatch;
+    check_ty_equal ty tbr.t_ty;
     List.iter2 p_check tl pl
   in
   List.iter t_check_branch bl;
@@ -667,15 +670,15 @@ let f_case tl bl =
   f_case tl bl
 
 let t_if f t1 t2 =
-  if not (ty_equal t1.t_ty t2.t_ty) then raise TypeMismatch;
+  check_ty_equal t1.t_ty t2.t_ty;
   t_if f t1 t2
 
 let t_let v t1 t2 =
-  if not (ty_equal v.vs_ty t1.t_ty) then raise TypeMismatch;
+  check_ty_equal v.vs_ty t1.t_ty;
   t_let v t1 t2
 
 let f_let v t1 f2 =
-  if not (ty_equal v.vs_ty t1.t_ty) then raise TypeMismatch;
+  check_ty_equal v.vs_ty t1.t_ty;
   f_let v t1 f2
 
 (* generic map over types, symbols and variables *)
@@ -993,7 +996,7 @@ let f_map fnT fnF f = f_label_copy f (match f.f_node with
 
 let protect fn t =
   let res = fn t in
-  if not (ty_equal res.t_ty t.t_ty) then raise TypeMismatch;
+  check_ty_equal t.t_ty res.t_ty;
   res
 
 let t_map fnT = t_map (protect fnT)
@@ -1175,7 +1178,7 @@ let f_map_cont fnT fnF contF f =
       list_map_cont fnT cont_case tl
 
 let protect_cont t contT e =
-  if not (ty_equal e.t_ty t.t_ty) then raise TypeMismatch;
+  check_ty_equal t.t_ty e.t_ty;
   contT e
 
 let t_map_cont fnT = t_map_cont (fun c t -> fnT (protect_cont t c) t)
@@ -1438,11 +1441,13 @@ let rec t_subst_term t1 t2 lvl t = if t_equal t t1 then t2 else
 and f_subst_term t1 t2 lvl f =
   f_map_unsafe (t_subst_term t1 t2) (f_subst_term t1 t2) lvl f
 
-let t_subst_term t1 t2 t = if ty_equal t1.t_ty t2.t_ty
-  then t_subst_term t1 t2 0 t else raise TypeMismatch
+let t_subst_term t1 t2 t = 
+  check_ty_equal t1.t_ty t2.t_ty;
+  t_subst_term t1 t2 0 t
 
-let f_subst_term t1 t2 f = if ty_equal t1.t_ty t2.t_ty
-  then f_subst_term t1 t2 0 f else raise TypeMismatch
+let f_subst_term t1 t2 f = 
+  check_ty_equal t1.t_ty t2.t_ty;
+  f_subst_term t1 t2 0 f
 
 (* substitutes fmla [f2] for fmla [f1] in term [t] *)
 
@@ -1463,11 +1468,13 @@ let rec t_subst_term_alpha t1 t2 lvl t = if t_equal t t1 then t2 else
 and f_subst_term_alpha t1 t2 lvl f =
   f_map_unsafe (t_subst_term_alpha t1 t2) (f_subst_term_alpha t1 t2) lvl f
 
-let t_subst_term_alpha t1 t2 t = if ty_equal t1.t_ty t2.t_ty
-  then t_subst_term_alpha t1 t2 0 t else raise TypeMismatch
+let t_subst_term_alpha t1 t2 t = 
+  check_ty_equal t1.t_ty t2.t_ty;
+  t_subst_term_alpha t1 t2 0 t
 
-let f_subst_term_alpha t1 t2 f = if ty_equal t1.t_ty t2.t_ty
-  then f_subst_term_alpha t1 t2 0 f else raise TypeMismatch
+let f_subst_term_alpha t1 t2 f =
+  check_ty_equal t1.t_ty t2.t_ty;
+  f_subst_term_alpha t1 t2 0 f
 
 (* substitutes fmla [f2] for fmla [f1] in term [t] modulo alpha *)
 

src/core/theory.ml

@@ -364,7 +364,7 @@ let cl_init_ls cl ls ls' =
   if not (Sid.mem id cl.id_local) then raise (NonLocal id);
   let mtch sb ty ty' =
     try ty_match sb ty' (cl_trans_ty cl ty)
-    with TypeMismatch -> raise (BadInstance (id, ls'.ls_name))
+    with TypeMismatch _ -> raise (BadInstance (id, ls'.ls_name))
   in
   let sb = match ls.ls_value,ls'.ls_value with
     | Some ty, Some ty' -> mtch Mtv.empty ty ty'

src/core/ty.ml

@@ -182,23 +182,27 @@ let ty_s_any pr ty =
 
 (* type matching *)
 
-exception TypeMismatch
+let rec ty_inst s ty = match ty.ty_node with
+  | Tyvar n -> (try Mtv.find n s with Not_found -> ty)
+  | _ -> ty_map (ty_inst s) ty
 
 let rec ty_match s ty1 ty2 =
   if ty_equal ty1 ty2 then s
   else match ty1.ty_node, ty2.ty_node with
     | Tyvar n1, _ ->
         (try if ty_equal (Mtv.find n1 s) ty2
-              then s else raise TypeMismatch
+              then s else raise Exit
          with Not_found -> Mtv.add n1 ty2 s)
     | Tyapp (f1, l1), Tyapp (f2, l2) when ts_equal f1 f2 ->
         List.fold_left2 ty_match s l1 l2
     | _ ->
-        raise TypeMismatch
+        raise Exit
 
-let rec ty_inst s ty = match ty.ty_node with
-  | Tyvar n -> (try Mtv.find n s with Not_found -> ty)
-  | _ -> ty_map (ty_inst s) ty
+exception TypeMismatch of ty * ty
+
+let ty_match s ty1 ty2 =
+  try ty_match s ty1 ty2
+  with Exit -> raise (TypeMismatch (ty_inst s ty1, ty2))
 
 (* built-in symbols *)
 

src/core/ty.mli

@@ -82,7 +82,7 @@ val ty_s_fold : ('a -> tysymbol -> 'a) -> 'a -> ty -> 'a
 val ty_s_all : (tysymbol -> bool) -> ty -> bool
 val ty_s_any : (tysymbol -> bool) -> ty -> bool
 
-exception TypeMismatch
+exception TypeMismatch of ty * ty
 
 val ty_match : ty Mtv.t -> ty -> ty -> ty Mtv.t
 val ty_inst  : ty Mtv.t -> ty -> ty

src/programs/pgm_main.ml

@@ -59,6 +59,12 @@ let rec report fmt = function
       Pgm_typing.report fmt e
   | Denv.Error e ->
       Denv.report fmt e
+(*
+  | Ty.TypeMismatch (ty1, ty2) as e ->
+      eprintf "@[type mismatch: %a, %a@]@." 
+	Pretty.print_ty ty1 Pretty.print_ty ty2;
+      raise e
+*)
   | e ->
       raise e