1.1 --- a/src/Pure/pattern.ML Sat Jun 05 13:07:31 2004 +0200
1.2 +++ b/src/Pure/pattern.ML Sat Jun 05 13:07:49 2004 +0200
1.3 @@ -46,19 +46,16 @@
1.4
1.5 val trace_unify_fail = ref false;
1.6
1.7 -(* Only for communication between unification and error message printing *)
1.8 -val sgr = ref Sign.pre_pure
1.9 -
1.10 -fun string_of_term env binders t = Sign.string_of_term (!sgr)
1.11 +fun string_of_term sg env binders t = Sign.string_of_term sg
1.12 (Envir.norm_term env (subst_bounds(map Free binders,t)));
1.13
1.14 fun bname binders i = fst(nth_elem(i,binders));
1.15 fun bnames binders is = space_implode " " (map (bname binders) is);
1.16
1.17 -fun typ_clash(tye,T,U) =
1.18 +fun typ_clash sg (tye,T,U) =
1.19 if !trace_unify_fail
1.20 - then let val t = Sign.string_of_typ (!sgr) (Envir.norm_type tye T)
1.21 - and u = Sign.string_of_typ (!sgr) (Envir.norm_type tye U)
1.22 + then let val t = Sign.string_of_typ sg (Envir.norm_type tye T)
1.23 + and u = Sign.string_of_typ sg (Envir.norm_type tye U)
1.24 in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
1.25 else ()
1.26
1.27 @@ -76,11 +73,11 @@
1.28 if !trace_unify_fail then clash (boundVar binders i) s
1.29 else ()
1.30
1.31 -fun proj_fail(env,binders,F,is,t) =
1.32 +fun proj_fail sg (env,binders,F,is,t) =
1.33 if !trace_unify_fail
1.34 then let val f = Syntax.string_of_vname F
1.35 val xs = bnames binders is
1.36 - val u = string_of_term env binders t
1.37 + val u = string_of_term sg env binders t
1.38 val ys = bnames binders (loose_bnos t \\ is)
1.39 in tracing("Cannot unify variable " ^ f ^
1.40 " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^
1.41 @@ -88,10 +85,10 @@
1.42 end
1.43 else ()
1.44
1.45 -fun ocheck_fail(F,t,binders,env) =
1.46 +fun ocheck_fail sg (F,t,binders,env) =
1.47 if !trace_unify_fail
1.48 then let val f = Syntax.string_of_vname F
1.49 - val u = string_of_term env binders t
1.50 + val u = string_of_term sg env binders t
1.51 in tracing("Variable " ^ f ^ " occurs in term\n" ^ u ^
1.52 "\nCannot unify!\n")
1.53 end
1.54 @@ -229,31 +226,29 @@
1.55 end;
1.56 in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
1.57
1.58 -val tsgr = ref(Type.empty_tsig);
1.59 +fun unify_types sg (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
1.60 + if T=U then env
1.61 + else let val (iTs',maxidx') = Type.unify (Sign.tsig_of sg) (iTs, maxidx) (U, T)
1.62 + in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
1.63 + handle Type.TUNIFY => (typ_clash sg (iTs,T,U); raise Unif);
1.64
1.65 -fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
1.66 - if T=U then env
1.67 - else let val (iTs',maxidx') = Type.unify (!tsgr) (iTs, maxidx) (U, T)
1.68 - in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
1.69 - handle Type.TUNIFY => (typ_clash(iTs,T,U); raise Unif);
1.70 -
1.71 -fun unif binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of
1.72 +fun unif sg binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of
1.73 (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
1.74 let val name = if ns = "" then nt else ns
1.75 - in unif ((name,Ts)::binders) (env,(ts,tt)) end
1.76 - | (Abs(ns,Ts,ts),t) => unif ((ns,Ts)::binders) (env,(ts,(incr t)$Bound(0)))
1.77 - | (t,Abs(nt,Tt,tt)) => unif ((nt,Tt)::binders) (env,((incr t)$Bound(0),tt))
1.78 - | p => cases(binders,env,p)
1.79 + in unif sg ((name,Ts)::binders) (env,(ts,tt)) end
1.80 + | (Abs(ns,Ts,ts),t) => unif sg ((ns,Ts)::binders) (env,(ts,(incr t)$Bound(0)))
1.81 + | (t,Abs(nt,Tt,tt)) => unif sg ((nt,Tt)::binders) (env,((incr t)$Bound(0),tt))
1.82 + | p => cases sg (binders,env,p)
1.83
1.84 -and cases(binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
1.85 +and cases sg (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
1.86 ((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
1.87 if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
1.88 else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
1.89 - | ((Var(F,_),ss),_) => flexrigid(env,binders,F,ints_of' env ss,t)
1.90 - | (_,(Var(F,_),ts)) => flexrigid(env,binders,F,ints_of' env ts,s)
1.91 - | ((Const c,ss),(Const d,ts)) => rigidrigid(env,binders,c,d,ss,ts)
1.92 - | ((Free(f),ss),(Free(g),ts)) => rigidrigid(env,binders,f,g,ss,ts)
1.93 - | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts)
1.94 + | ((Var(F,_),ss),_) => flexrigid sg (env,binders,F,ints_of' env ss,t)
1.95 + | (_,(Var(F,_),ts)) => flexrigid sg (env,binders,F,ints_of' env ts,s)
1.96 + | ((Const c,ss),(Const d,ts)) => rigidrigid sg (env,binders,c,d,ss,ts)
1.97 + | ((Free(f),ss),(Free(g),ts)) => rigidrigid sg (env,binders,f,g,ss,ts)
1.98 + | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB sg (env,binders,i,j,ss,ts)
1.99 | ((Abs(_),_),_) => raise Pattern
1.100 | (_,(Abs(_),_)) => raise Pattern
1.101 | ((Const(c,_),_),(Free(f,_),_)) => (clash c f; raise Unif)
1.102 @@ -264,22 +259,21 @@
1.103 | ((Bound i,_),(Free(f,_),_)) => (clashB binders i f; raise Unif)
1.104
1.105
1.106 -and rigidrigid (env,binders,(a,Ta),(b,Tb),ss,ts) =
1.107 +and rigidrigid sg (env,binders,(a,Ta),(b,Tb),ss,ts) =
1.108 if a<>b then (clash a b; raise Unif)
1.109 - else foldl (unif binders) (unify_types(Ta,Tb,env), ss~~ts)
1.110 + else foldl (unif sg binders) (unify_types sg (Ta,Tb,env), ss~~ts)
1.111
1.112 -and rigidrigidB (env,binders,i,j,ss,ts) =
1.113 +and rigidrigidB sg (env,binders,i,j,ss,ts) =
1.114 if i <> j then (clashBB binders i j; raise Unif)
1.115 - else foldl (unif binders) (env ,ss~~ts)
1.116 + else foldl (unif sg binders) (env ,ss~~ts)
1.117
1.118 -and flexrigid (params as (env,binders,F,is,t)) =
1.119 - if occurs(F,t,env) then (ocheck_fail(F,t,binders,env); raise Unif)
1.120 +and flexrigid sg (params as (env,binders,F,is,t)) =
1.121 + if occurs(F,t,env) then (ocheck_fail sg (F,t,binders,env); raise Unif)
1.122 else (let val (u,env') = proj(t,env,binders,is)
1.123 in Envir.update((F,mkabs(binders,is,u)),env') end
1.124 - handle Unif => (proj_fail params; raise Unif));
1.125 + handle Unif => (proj_fail sg params; raise Unif));
1.126
1.127 -fun unify(sg,env,tus) = (sgr := sg; tsgr := Sign.tsig_of sg;
1.128 - foldl (unif []) (env,tus));
1.129 +fun unify(sg,env,tus) = foldl (unif sg []) (env,tus);
1.130
1.131
1.132 (*Eta-contract a term (fully)*)