# HG changeset patch
# User nipkow
# Date 1034269343 -7200
# Node ID a3d97348ceb68ceb3ad669ef64bdb675c0e59e3c
# Parent  63d1790a43edceccce89ecc35808cae725085a86
added failure trace information to pattern unification

diff -r 63d1790a43ed -r a3d97348ceb6 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Thu Oct 10 14:26:50 2002 +0200
+++ b/src/Pure/pattern.ML	Thu Oct 10 19:02:23 2002 +0200
@@ -19,6 +19,7 @@
   type type_sig
   type sg
   type env
+  val trace_unify_fail  : bool ref
   val aeconv            : term * term -> bool
   val eta_contract      : term -> term
   val beta_eta_contract : term -> term
@@ -49,6 +50,66 @@
 exception Unif;
 exception Pattern;
 
+val trace_unify_fail = ref false;
+
+(* Only for communication between unification and error message printing *)
+val sgr = ref Sign.pre_pure
+
+fun string_of_term env binders t = Sign.string_of_term (!sgr)
+  (Envir.norm_term env (subst_bounds(map Free binders,t)));
+
+fun bname binders i = fst(nth_elem(i,binders));
+fun bnames binders is = space_implode " " (map (bname binders) is);
+
+fun norm_typ tye =
+  let fun chase(v,s) =
+      (case  Vartab.lookup (tye, v) of
+        Some U => norm_typ tye U
+      | None => TVar(v,s))
+  in map_type_tvar chase end
+
+fun typ_clash(tye,T,U) =
+  if !trace_unify_fail
+  then let val t = Sign.string_of_typ (!sgr) (norm_typ tye T)
+           and u = Sign.string_of_typ (!sgr) (norm_typ tye U)
+       in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
+  else ()
+
+fun clash a b =
+  if !trace_unify_fail then tracing("Clash: " ^ a ^ " =/= " ^ b) else ()
+
+fun boundVar binders i =
+  "bound variable " ^ bname binders i ^ " (depth " ^ string_of_int i ^ ")";
+
+fun clashBB binders i j =
+  if !trace_unify_fail then clash (boundVar binders i) (boundVar binders j)
+  else ()
+
+fun clashB binders i s =
+  if !trace_unify_fail then clash (boundVar binders i) s
+  else ()
+
+fun proj_fail(env,binders,F,is,t) =
+  if !trace_unify_fail
+  then let val f = Syntax.string_of_vname F
+           val xs = bnames binders is
+           val u = string_of_term env binders t
+           val ys = bnames binders (loose_bnos t \\ is)
+       in tracing("Cannot unify variable " ^ f ^
+               " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^
+               "\nTerm contains additional bound variable(s) " ^ ys)
+       end
+  else ()
+
+fun ocheck_fail(F,t,binders,env) =
+  if !trace_unify_fail
+  then let val f = Syntax.string_of_vname F
+           val u = string_of_term env binders t
+       in tracing("Variable " ^ f ^ " occurs in term\n" ^ u ^
+                  "\nCannot unify!\n")
+       end
+  else ()
+
 fun occurs(F,t,env) =
     let fun occ(Var(G,_))   = (case Envir.lookup(env,G) of
                                  Some(t) => occ t
@@ -188,7 +249,7 @@
   if T=U then env
   else let val (iTs',maxidx') = Type.unify (!tsgr) (iTs, maxidx) (U, T)
        in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
-       handle Type.TUNIFY => raise Unif;
+       handle Type.TUNIFY => (typ_clash(iTs,T,U); raise Unif);
 
 fun unif binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of
       (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
@@ -209,21 +270,29 @@
       | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts)
       | ((Abs(_),_),_)                => raise Pattern
       | (_,(Abs(_),_))                => raise Pattern
-      | _                             => raise Unif
+      | ((Const(c,_),_),(Free(f,_),_)) => (clash c f; raise Unif)
+      | ((Const(c,_),_),(Bound i,_))   => (clashB binders i c; raise Unif)
+      | ((Free(f,_),_),(Const(c,_),_)) => (clash f c; raise Unif)
+      | ((Free(f,_),_),(Bound i,_))    => (clashB binders i f; raise Unif)
+      | ((Bound i,_),(Const(c,_),_))   => (clashB binders i c; raise Unif)
+      | ((Bound i,_),(Free(f,_),_))    => (clashB binders i f; raise Unif)
+
 
 and rigidrigid (env,binders,(a,Ta),(b,Tb),ss,ts) =
-      if a<>b then raise Unif
+      if a<>b then (clash a b; raise Unif)
       else foldl (unif binders) (unify_types(Ta,Tb,env), ss~~ts)
 
 and rigidrigidB (env,binders,i,j,ss,ts) =
-     if i <> j then raise Unif else foldl (unif binders) (env ,ss~~ts)
+     if i <> j then (clashBB binders i j; raise Unif)
+     else foldl (unif binders) (env ,ss~~ts)
 
-and flexrigid (env,binders,F,is,t) =
-      if occurs(F,t,env) then raise Unif
-      else let val (u,env') = proj(t,env,binders,is)
-           in Envir.update((F,mkabs(binders,is,u)),env') end;
+and flexrigid (params as (env,binders,F,is,t)) =
+      if occurs(F,t,env) then (ocheck_fail(F,t,binders,env); raise Unif)
+      else (let val (u,env') = proj(t,env,binders,is)
+            in Envir.update((F,mkabs(binders,is,u)),env') end
+            handle Unif => (proj_fail params; raise Unif));
 
-fun unify(sg,env,tus) = (tsgr := #tsig(Sign.rep_sg sg);
+fun unify(sg,env,tus) = (sgr := sg; tsgr := #tsig(Sign.rep_sg sg);
                          foldl (unif []) (env,tus));
 
 
@@ -472,3 +541,5 @@
   in if_none (rew1 skel0 tm) tm end;
 
 end;
+
+val trace_unify_fail = Pattern.trace_unify_fail;
diff -r 63d1790a43ed -r a3d97348ceb6 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Oct 10 14:26:50 2002 +0200
+++ b/src/Pure/thm.ML	Thu Oct 10 19:02:23 2002 +0200
@@ -1386,7 +1386,8 @@
         val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);
         fun res [] = Seq.empty
           | res ((eres_flg, rule)::brules) =
-              if could_bires (Hs, B, eres_flg, rule)
+              if !Pattern.trace_unify_fail orelse
+                 could_bires (Hs, B, eres_flg, rule)
               then Seq.make (*delay processing remainder till needed*)
                   (fn()=> Some(comp (eres_flg, lift rule, nprems_of rule),
                                res brules))