src/Pure/pattern.ML
changeset 13642 a3d97348ceb6
parent 13195 98975cc13d28
child 13645 430310b12c5b
     1.1 --- a/src/Pure/pattern.ML	Thu Oct 10 14:26:50 2002 +0200
     1.2 +++ b/src/Pure/pattern.ML	Thu Oct 10 19:02:23 2002 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4    type type_sig
     1.5    type sg
     1.6    type env
     1.7 +  val trace_unify_fail  : bool ref
     1.8    val aeconv            : term * term -> bool
     1.9    val eta_contract      : term -> term
    1.10    val beta_eta_contract : term -> term
    1.11 @@ -49,6 +50,66 @@
    1.12  exception Unif;
    1.13  exception Pattern;
    1.14  
    1.15 +val trace_unify_fail = ref false;
    1.16 +
    1.17 +(* Only for communication between unification and error message printing *)
    1.18 +val sgr = ref Sign.pre_pure
    1.19 +
    1.20 +fun string_of_term env binders t = Sign.string_of_term (!sgr)
    1.21 +  (Envir.norm_term env (subst_bounds(map Free binders,t)));
    1.22 +
    1.23 +fun bname binders i = fst(nth_elem(i,binders));
    1.24 +fun bnames binders is = space_implode " " (map (bname binders) is);
    1.25 +
    1.26 +fun norm_typ tye =
    1.27 +  let fun chase(v,s) =
    1.28 +      (case  Vartab.lookup (tye, v) of
    1.29 +        Some U => norm_typ tye U
    1.30 +      | None => TVar(v,s))
    1.31 +  in map_type_tvar chase end
    1.32 +
    1.33 +fun typ_clash(tye,T,U) =
    1.34 +  if !trace_unify_fail
    1.35 +  then let val t = Sign.string_of_typ (!sgr) (norm_typ tye T)
    1.36 +           and u = Sign.string_of_typ (!sgr) (norm_typ tye U)
    1.37 +       in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
    1.38 +  else ()
    1.39 +
    1.40 +fun clash a b =
    1.41 +  if !trace_unify_fail then tracing("Clash: " ^ a ^ " =/= " ^ b) else ()
    1.42 +
    1.43 +fun boundVar binders i =
    1.44 +  "bound variable " ^ bname binders i ^ " (depth " ^ string_of_int i ^ ")";
    1.45 +
    1.46 +fun clashBB binders i j =
    1.47 +  if !trace_unify_fail then clash (boundVar binders i) (boundVar binders j)
    1.48 +  else ()
    1.49 +
    1.50 +fun clashB binders i s =
    1.51 +  if !trace_unify_fail then clash (boundVar binders i) s
    1.52 +  else ()
    1.53 +
    1.54 +fun proj_fail(env,binders,F,is,t) =
    1.55 +  if !trace_unify_fail
    1.56 +  then let val f = Syntax.string_of_vname F
    1.57 +           val xs = bnames binders is
    1.58 +           val u = string_of_term env binders t
    1.59 +           val ys = bnames binders (loose_bnos t \\ is)
    1.60 +       in tracing("Cannot unify variable " ^ f ^
    1.61 +               " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^
    1.62 +               "\nTerm contains additional bound variable(s) " ^ ys)
    1.63 +       end
    1.64 +  else ()
    1.65 +
    1.66 +fun ocheck_fail(F,t,binders,env) =
    1.67 +  if !trace_unify_fail
    1.68 +  then let val f = Syntax.string_of_vname F
    1.69 +           val u = string_of_term env binders t
    1.70 +       in tracing("Variable " ^ f ^ " occurs in term\n" ^ u ^
    1.71 +                  "\nCannot unify!\n")
    1.72 +       end
    1.73 +  else ()
    1.74 +
    1.75  fun occurs(F,t,env) =
    1.76      let fun occ(Var(G,_))   = (case Envir.lookup(env,G) of
    1.77                                   Some(t) => occ t
    1.78 @@ -188,7 +249,7 @@
    1.79    if T=U then env
    1.80    else let val (iTs',maxidx') = Type.unify (!tsgr) (iTs, maxidx) (U, T)
    1.81         in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    1.82 -       handle Type.TUNIFY => raise Unif;
    1.83 +       handle Type.TUNIFY => (typ_clash(iTs,T,U); raise Unif);
    1.84  
    1.85  fun unif binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of
    1.86        (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
    1.87 @@ -209,21 +270,29 @@
    1.88        | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts)
    1.89        | ((Abs(_),_),_)                => raise Pattern
    1.90        | (_,(Abs(_),_))                => raise Pattern
    1.91 -      | _                             => raise Unif
    1.92 +      | ((Const(c,_),_),(Free(f,_),_)) => (clash c f; raise Unif)
    1.93 +      | ((Const(c,_),_),(Bound i,_))   => (clashB binders i c; raise Unif)
    1.94 +      | ((Free(f,_),_),(Const(c,_),_)) => (clash f c; raise Unif)
    1.95 +      | ((Free(f,_),_),(Bound i,_))    => (clashB binders i f; raise Unif)
    1.96 +      | ((Bound i,_),(Const(c,_),_))   => (clashB binders i c; raise Unif)
    1.97 +      | ((Bound i,_),(Free(f,_),_))    => (clashB binders i f; raise Unif)
    1.98 +
    1.99  
   1.100  and rigidrigid (env,binders,(a,Ta),(b,Tb),ss,ts) =
   1.101 -      if a<>b then raise Unif
   1.102 +      if a<>b then (clash a b; raise Unif)
   1.103        else foldl (unif binders) (unify_types(Ta,Tb,env), ss~~ts)
   1.104  
   1.105  and rigidrigidB (env,binders,i,j,ss,ts) =
   1.106 -     if i <> j then raise Unif else foldl (unif binders) (env ,ss~~ts)
   1.107 +     if i <> j then (clashBB binders i j; raise Unif)
   1.108 +     else foldl (unif binders) (env ,ss~~ts)
   1.109  
   1.110 -and flexrigid (env,binders,F,is,t) =
   1.111 -      if occurs(F,t,env) then raise Unif
   1.112 -      else let val (u,env') = proj(t,env,binders,is)
   1.113 -           in Envir.update((F,mkabs(binders,is,u)),env') end;
   1.114 +and flexrigid (params as (env,binders,F,is,t)) =
   1.115 +      if occurs(F,t,env) then (ocheck_fail(F,t,binders,env); raise Unif)
   1.116 +      else (let val (u,env') = proj(t,env,binders,is)
   1.117 +            in Envir.update((F,mkabs(binders,is,u)),env') end
   1.118 +            handle Unif => (proj_fail params; raise Unif));
   1.119  
   1.120 -fun unify(sg,env,tus) = (tsgr := #tsig(Sign.rep_sg sg);
   1.121 +fun unify(sg,env,tus) = (sgr := sg; tsgr := #tsig(Sign.rep_sg sg);
   1.122                           foldl (unif []) (env,tus));
   1.123  
   1.124  
   1.125 @@ -472,3 +541,5 @@
   1.126    in if_none (rew1 skel0 tm) tm end;
   1.127  
   1.128  end;
   1.129 +
   1.130 +val trace_unify_fail = Pattern.trace_unify_fail;