139 (* split_type ([T1,....,Tn]---> T,n,[]) = ([Tn,...,T1],T) *) |
139 (* split_type ([T1,....,Tn]---> T,n,[]) = ([Tn,...,T1],T) *) |
140 fun split_type (T,0,Ts) = (Ts,T) |
140 fun split_type (T,0,Ts) = (Ts,T) |
141 | split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts) |
141 | split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts) |
142 | split_type _ = error("split_type"); |
142 | split_type _ = error("split_type"); |
143 |
143 |
144 fun type_of_G (env as Envir.Envir {iTs, ...}) (T,n,is) = |
144 fun type_of_G env (T, n, is) = |
145 let val (Ts, U) = split_type (Envir.norm_type iTs T, n, []) |
145 let |
|
146 val tyenv = Envir.type_env env; |
|
147 val (Ts, U) = split_type (Envir.norm_type tyenv T, n, []); |
146 in map (nth Ts) is ---> U end; |
148 in map (nth Ts) is ---> U end; |
147 |
149 |
148 fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js)); |
150 fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js)); |
149 |
151 |
150 fun mknewhnf(env,binders,is,F as (a,_),T,js) = |
152 fun mknewhnf(env,binders,is,F as (a,_),T,js) = |
223 fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks)); |
225 fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks)); |
224 in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env')) |
226 in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env')) |
225 end; |
227 end; |
226 in if TermOrd.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end |
228 in if TermOrd.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end |
227 |
229 |
228 fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) = |
230 fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) = |
229 if T=U then env |
231 if T = U then env |
230 else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx) |
232 else |
231 in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end |
233 let val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx) |
232 handle Type.TUNIFY => (typ_clash thy (iTs,T,U); raise Unif); |
234 in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end |
|
235 handle Type.TUNIFY => (typ_clash thy (tyenv, T, U); raise Unif); |
233 |
236 |
234 fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of |
237 fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of |
235 (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) => |
238 (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) => |
236 let val name = if ns = "" then nt else ns |
239 let val name = if ns = "" then nt else ns |
237 in unif thy ((name,Ts)::binders) (ts,tt) env end |
240 in unif thy ((name,Ts)::binders) (ts,tt) env end |