43 val trace_unify_fail = ref false; |
43 val trace_unify_fail = ref false; |
44 |
44 |
45 fun string_of_term thy env binders t = Sign.string_of_term thy |
45 fun string_of_term thy env binders t = Sign.string_of_term thy |
46 (Envir.norm_term env (subst_bounds(map Free binders,t))); |
46 (Envir.norm_term env (subst_bounds(map Free binders,t))); |
47 |
47 |
48 fun bname binders i = fst(List.nth(binders,i)); |
48 fun bname binders i = fst (nth binders i); |
49 fun bnames binders is = space_implode " " (map (bname binders) is); |
49 fun bnames binders is = space_implode " " (map (bname binders) is); |
50 |
50 |
51 fun typ_clash thy (tye,T,U) = |
51 fun typ_clash thy (tye,T,U) = |
52 if !trace_unify_fail |
52 if !trace_unify_fail |
53 then let val t = Sign.string_of_typ thy (Envir.norm_type tye T) |
53 then let val t = Sign.string_of_typ thy (Envir.norm_type tye T) |
108 in mpb 0 end; |
108 in mpb 0 end; |
109 |
109 |
110 fun idx [] j = raise Unif |
110 fun idx [] j = raise Unif |
111 | idx(i::is) j = if (i:int) =j then length is else idx is j; |
111 | idx(i::is) j = if (i:int) =j then length is else idx is j; |
112 |
112 |
113 fun at xs i = List.nth (xs,i); |
|
114 |
|
115 fun mkabs (binders,is,t) = |
113 fun mkabs (binders,is,t) = |
116 let fun mk(i::is) = let val (x,T) = List.nth(binders,i) |
114 let fun mk(i::is) = let val (x,T) = nth binders i |
117 in Abs(x,T,mk is) end |
115 in Abs(x,T,mk is) end |
118 | mk [] = t |
116 | mk [] = t |
119 in mk is end; |
117 in mk is end; |
120 |
118 |
121 val incr = mapbnd (fn i => i+1); |
119 val incr = mapbnd (fn i => i+1); |
132 fun app (s,(i::is)) = app (s$Bound(i),is) |
130 fun app (s,(i::is)) = app (s$Bound(i),is) |
133 | app (s,[]) = s; |
131 | app (s,[]) = s; |
134 |
132 |
135 fun red (Abs(_,_,s)) (i::is) js = red s is (i::js) |
133 fun red (Abs(_,_,s)) (i::is) js = red s is (i::js) |
136 | red t [] [] = t |
134 | red t [] [] = t |
137 | red t is jn = app (mapbnd (at jn) t,is); |
135 | red t is jn = app (mapbnd (nth jn) t,is); |
138 |
136 |
139 |
137 |
140 (* split_type ([T1,....,Tn]---> T,n,[]) = ([Tn,...,T1],T) *) |
138 (* split_type ([T1,....,Tn]---> T,n,[]) = ([Tn,...,T1],T) *) |
141 fun split_type (T,0,Ts) = (Ts,T) |
139 fun split_type (T,0,Ts) = (Ts,T) |
142 | split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts) |
140 | split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts) |
143 | split_type _ = error("split_type"); |
141 | split_type _ = error("split_type"); |
144 |
142 |
145 fun type_of_G (env as Envir.Envir {iTs, ...}) (T,n,is) = |
143 fun type_of_G (env as Envir.Envir {iTs, ...}) (T,n,is) = |
146 let val (Ts, U) = split_type (Envir.norm_type iTs T, n, []) |
144 let val (Ts, U) = split_type (Envir.norm_type iTs T, n, []) |
147 in map (at Ts) is ---> U end; |
145 in map (nth Ts) is ---> U end; |
148 |
146 |
149 fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js)); |
147 fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js)); |
150 |
148 |
151 fun mknewhnf(env,binders,is,F as (a,_),T,js) = |
149 fun mknewhnf(env,binders,is,F as (a,_),T,js) = |
152 let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js)) |
150 let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js)) |