101 Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U') |
101 Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U') |
102 | _ => |
102 | _ => |
103 let val (env3, V) = mk_tvar (env2, []) |
103 let val (env3, V) = mk_tvar (env2, []) |
104 in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end) |
104 in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end) |
105 end |
105 end |
106 | infer_type thy env Ts vTs (t as Bound i) = (t, List.nth (Ts, i), vTs, env); |
106 | infer_type thy env Ts vTs (t as Bound i) = ((t, List.nth (Ts, i), vTs, env) |
|
107 handle Subscript => error ("infer_type: bad variable index " ^ string_of_int i)); |
107 |
108 |
108 fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^ |
109 fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^ |
109 Sign.string_of_term thy t ^ "\n\n" ^ Sign.string_of_term thy u); |
110 Sign.string_of_term thy t ^ "\n\n" ^ Sign.string_of_term thy u); |
110 |
111 |
111 fun decompose thy Ts (env, p as (t, u)) = |
112 fun decompose thy Ts (env, p as (t, u)) = |
155 in (prop'', change_type (SOME Ts) prf, [], env', vTs) end; |
156 in (prop'', change_type (SOME Ts) prf, [], env', vTs) end; |
156 |
157 |
157 fun head_norm (prop, prf, cnstrts, env, vTs) = |
158 fun head_norm (prop, prf, cnstrts, env, vTs) = |
158 (Envir.head_norm env prop, prf, cnstrts, env, vTs); |
159 (Envir.head_norm env prop, prf, cnstrts, env, vTs); |
159 |
160 |
160 fun mk_cnstrts env _ Hs vTs (PBound i) = (List.nth (Hs, i), PBound i, [], env, vTs) |
161 fun mk_cnstrts env _ Hs vTs (PBound i) = ((List.nth (Hs, i), PBound i, [], env, vTs) |
|
162 handle Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i)) |
161 | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) = |
163 | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) = |
162 let |
164 let |
163 val (env', T) = (case opT of |
165 val (env', T) = (case opT of |
164 NONE => mk_tvar (env, []) | SOME T => (env, T)); |
166 NONE => mk_tvar (env, []) | SOME T => (env, T)); |
165 val (t, prf, cnstrts, env'', vTs') = |
167 val (t, prf, cnstrts, env'', vTs') = |