author | wenzelm |
Sun, 12 Sep 2010 16:06:03 +0200 | |
changeset 39286 | 1f8131a7bcb9 |
parent 37236 | 739d8b9c59da |
child 39287 | d30be6791038 |
permissions | -rw-r--r-- |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/type_infer.ML |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
2 |
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
3 |
|
22698 | 4 |
Simple type inference. |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
5 |
*) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
6 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
7 |
signature TYPE_INFER = |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
8 |
sig |
8087 | 9 |
val anyT: sort -> typ |
8611 | 10 |
val polymorphicT: typ -> typ |
24682 | 11 |
val constrain: typ -> term -> term |
24504 | 12 |
val is_param: indexname -> bool |
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset
|
13 |
val param: int -> string * sort -> typ |
22771 | 14 |
val paramify_vars: typ -> typ |
18339 | 15 |
val paramify_dummies: typ -> int -> typ * int |
24764 | 16 |
val fixate_params: Name.context -> term list -> term list |
22698 | 17 |
val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list |
24485
687bbb686ef9
infer_types: general check_typs instead of Type.cert_typ_mode;
wenzelm
parents:
24275
diff
changeset
|
18 |
val infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) -> |
27263 | 19 |
(string -> typ option) -> (indexname -> typ option) -> Name.context -> int -> |
20 |
term list -> term list |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
21 |
end; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
22 |
|
37145
01aa36932739
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
wenzelm
parents:
35013
diff
changeset
|
23 |
structure Type_Infer: TYPE_INFER = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
24 |
struct |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
25 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
26 |
|
22698 | 27 |
(** type parameters and constraints **) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
28 |
|
22698 | 29 |
fun anyT S = TFree ("'_dummy_", S); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
30 |
|
22698 | 31 |
(*indicate polymorphic Vars*) |
32 |
fun polymorphicT T = Type ("_polymorphic_", [T]); |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
33 |
|
27263 | 34 |
val constrain = Syntax.type_constraint; |
22698 | 35 |
|
36 |
||
39286 | 37 |
(* type inference parameters -- may get instantiated *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
38 |
|
24504 | 39 |
fun is_param (x, _: int) = String.isPrefix "?" x; |
22698 | 40 |
fun param i (x, S) = TVar (("?" ^ x, i), S); |
41 |
||
32002
1a35de4112bb
tuned paramify_vars: Term_Subst.map_atypsT_option;
wenzelm
parents:
31977
diff
changeset
|
42 |
val paramify_vars = |
32146 | 43 |
Same.commit |
44 |
(Term_Subst.map_atypsT_same |
|
45 |
(fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME)); |
|
22771 | 46 |
|
22698 | 47 |
val paramify_dummies = |
48 |
let |
|
49 |
fun dummy S maxidx = (param (maxidx + 1) ("'dummy", S), maxidx + 1); |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
50 |
|
22698 | 51 |
fun paramify (TFree ("'_dummy_", S)) maxidx = dummy S maxidx |
52 |
| paramify (Type ("dummy", _)) maxidx = dummy [] maxidx |
|
53 |
| paramify (Type (a, Ts)) maxidx = |
|
54 |
let val (Ts', maxidx') = fold_map paramify Ts maxidx |
|
55 |
in (Type (a, Ts'), maxidx') end |
|
56 |
| paramify T maxidx = (T, maxidx); |
|
57 |
in paramify end; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
58 |
|
24764 | 59 |
fun fixate_params name_context ts = |
60 |
let |
|
61 |
fun subst_param (xi, S) (inst, used) = |
|
62 |
if is_param xi then |
|
63 |
let |
|
24848 | 64 |
val [a] = Name.invents used Name.aT 1; |
24764 | 65 |
val used' = Name.declare a used; |
66 |
in (((xi, S), TFree (a, S)) :: inst, used') end |
|
67 |
else (inst, used); |
|
68 |
val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context; |
|
69 |
val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context'); |
|
31977 | 70 |
in (map o map_types) (Term_Subst.instantiateT inst) ts end; |
24764 | 71 |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
72 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
73 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
74 |
(** pretyps and preterms **) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
75 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
76 |
datatype pretyp = |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
77 |
PType of string * pretyp list | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
78 |
PTFree of string * sort | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
79 |
PTVar of indexname * sort | |
32141 | 80 |
Param of int * sort; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
81 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
82 |
datatype preterm = |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
83 |
PConst of string * pretyp | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
84 |
PFree of string * pretyp | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
85 |
PVar of indexname * pretyp | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
86 |
PBound of int | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
87 |
PAbs of string * pretyp * preterm | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
88 |
PAppl of preterm * preterm | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
89 |
Constraint of preterm * pretyp; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
90 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
91 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
92 |
(* utils *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
93 |
|
32146 | 94 |
fun deref tye (T as Param (i, S)) = |
95 |
(case Inttab.lookup tye i of |
|
96 |
NONE => T |
|
97 |
| SOME U => deref tye U) |
|
32141 | 98 |
| deref tye T = T; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
99 |
|
16195 | 100 |
fun fold_pretyps f (PConst (_, T)) x = f T x |
101 |
| fold_pretyps f (PFree (_, T)) x = f T x |
|
102 |
| fold_pretyps f (PVar (_, T)) x = f T x |
|
103 |
| fold_pretyps _ (PBound _) x = x |
|
104 |
| fold_pretyps f (PAbs (_, T, t)) x = fold_pretyps f t (f T x) |
|
105 |
| fold_pretyps f (PAppl (t, u)) x = fold_pretyps f u (fold_pretyps f t x) |
|
106 |
| fold_pretyps f (Constraint (t, T)) x = f T (fold_pretyps f t x); |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
107 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
108 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
109 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
110 |
(** raw typs/terms to pretyps/preterms **) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
111 |
|
20668 | 112 |
(* pretyp_of *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
113 |
|
32141 | 114 |
fun pretyp_of is_para typ params_idx = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
115 |
let |
32141 | 116 |
val (params', idx) = fold_atyps |
20668 | 117 |
(fn TVar (xi as (x, _), S) => |
32141 | 118 |
(fn ps_idx as (ps, idx) => |
24504 | 119 |
if is_para xi andalso not (Vartab.defined ps xi) |
32141 | 120 |
then (Vartab.update (xi, Param (idx, S)) ps, idx + 1) else ps_idx) |
121 |
| _ => I) typ params_idx; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
122 |
|
32141 | 123 |
fun pre_of (TVar (v as (xi, _))) idx = |
20735 | 124 |
(case Vartab.lookup params' xi of |
15531 | 125 |
NONE => PTVar v |
32141 | 126 |
| SOME p => p, idx) |
127 |
| pre_of (TFree ("'_dummy_", S)) idx = (Param (idx, S), idx + 1) |
|
128 |
| pre_of (TFree v) idx = (PTFree v, idx) |
|
129 |
| pre_of (T as Type (a, Ts)) idx = |
|
130 |
if T = dummyT then (Param (idx, []), idx + 1) |
|
131 |
else |
|
132 |
let val (Ts', idx') = fold_map pre_of Ts idx |
|
133 |
in (PType (a, Ts'), idx') end; |
|
134 |
||
135 |
val (ptyp, idx') = pre_of typ idx; |
|
136 |
in (ptyp, (params', idx')) end; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
137 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
138 |
|
20668 | 139 |
(* preterm_of *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
140 |
|
32141 | 141 |
fun preterm_of const_type is_para tm (vparams, params, idx) = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
142 |
let |
32141 | 143 |
fun add_vparm xi (ps_idx as (ps, idx)) = |
20735 | 144 |
if not (Vartab.defined ps xi) then |
32141 | 145 |
(Vartab.update (xi, Param (idx, [])) ps, idx + 1) |
146 |
else ps_idx; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
147 |
|
32141 | 148 |
val (vparams', idx') = fold_aterms |
20668 | 149 |
(fn Var (_, Type ("_polymorphic_", _)) => I |
150 |
| Var (xi, _) => add_vparm xi |
|
151 |
| Free (x, _) => add_vparm (x, ~1) |
|
152 |
| _ => I) |
|
32141 | 153 |
tm (vparams, idx); |
20735 | 154 |
fun var_param xi = the (Vartab.lookup vparams' xi); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
155 |
|
24504 | 156 |
val preT_of = pretyp_of is_para; |
32141 | 157 |
fun polyT_of T idx = apsnd snd (pretyp_of (K true) T (Vartab.empty, idx)); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
158 |
|
22698 | 159 |
fun constraint T t ps = |
20668 | 160 |
if T = dummyT then (t, ps) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
161 |
else |
20668 | 162 |
let val (T', ps') = preT_of T ps |
163 |
in (Constraint (t, T'), ps') end; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
164 |
|
32141 | 165 |
fun pre_of (Const (c, T)) (ps, idx) = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
166 |
(case const_type c of |
32141 | 167 |
SOME U => |
168 |
let val (pU, idx') = polyT_of U idx |
|
169 |
in constraint T (PConst (c, pU)) (ps, idx') end |
|
39286 | 170 |
| NONE => raise TYPE ("Undeclared constant: " ^ quote c, [], [])) |
32141 | 171 |
| pre_of (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) = |
172 |
let val (pT, idx') = polyT_of T idx |
|
173 |
in (PVar (xi, pT), (ps, idx')) end |
|
174 |
| pre_of (Var (xi, T)) ps_idx = constraint T (PVar (xi, var_param xi)) ps_idx |
|
175 |
| pre_of (Free (x, T)) ps_idx = constraint T (PFree (x, var_param (x, ~1))) ps_idx |
|
176 |
| pre_of (Const ("_type_constraint_", Type ("fun", [T, _])) $ t) ps_idx = |
|
177 |
pre_of t ps_idx |-> constraint T |
|
178 |
| pre_of (Bound i) ps_idx = (PBound i, ps_idx) |
|
179 |
| pre_of (Abs (x, T, t)) ps_idx = |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
180 |
let |
32141 | 181 |
val (T', ps_idx') = preT_of T ps_idx; |
182 |
val (t', ps_idx'') = pre_of t ps_idx'; |
|
183 |
in (PAbs (x, T', t'), ps_idx'') end |
|
184 |
| pre_of (t $ u) ps_idx = |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
185 |
let |
32141 | 186 |
val (t', ps_idx') = pre_of t ps_idx; |
187 |
val (u', ps_idx'') = pre_of u ps_idx'; |
|
188 |
in (PAppl (t', u'), ps_idx'') end; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
189 |
|
32141 | 190 |
val (tm', (params', idx'')) = pre_of tm (params, idx'); |
191 |
in (tm', (vparams', params', idx'')) end; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
192 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
193 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
194 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
195 |
(** pretyps/terms to typs/terms **) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
196 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
197 |
(* add_parms *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
198 |
|
32146 | 199 |
fun add_parmsT tye T = |
200 |
(case deref tye T of |
|
32141 | 201 |
PType (_, Ts) => fold (add_parmsT tye) Ts |
202 |
| Param (i, _) => insert (op =) i |
|
32146 | 203 |
| _ => I); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
204 |
|
32141 | 205 |
fun add_parms tye = fold_pretyps (add_parmsT tye); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
206 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
207 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
208 |
(* add_names *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
209 |
|
32146 | 210 |
fun add_namesT tye T = |
211 |
(case deref tye T of |
|
32141 | 212 |
PType (_, Ts) => fold (add_namesT tye) Ts |
213 |
| PTFree (x, _) => Name.declare x |
|
214 |
| PTVar ((x, _), _) => Name.declare x |
|
32146 | 215 |
| Param _ => I); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
216 |
|
32141 | 217 |
fun add_names tye = fold_pretyps (add_namesT tye); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
218 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
219 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
220 |
(* simple_typ/term_of *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
221 |
|
32146 | 222 |
fun simple_typ_of tye f T = |
223 |
(case deref tye T of |
|
32141 | 224 |
PType (a, Ts) => Type (a, map (simple_typ_of tye f) Ts) |
225 |
| PTFree v => TFree v |
|
226 |
| PTVar v => TVar v |
|
32146 | 227 |
| Param (i, S) => TVar (f i, S)); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
228 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
229 |
(*convert types, drop constraints*) |
32141 | 230 |
fun simple_term_of tye f (PConst (c, T)) = Const (c, simple_typ_of tye f T) |
231 |
| simple_term_of tye f (PFree (x, T)) = Free (x, simple_typ_of tye f T) |
|
232 |
| simple_term_of tye f (PVar (xi, T)) = Var (xi, simple_typ_of tye f T) |
|
233 |
| simple_term_of tye f (PBound i) = Bound i |
|
234 |
| simple_term_of tye f (PAbs (x, T, t)) = |
|
235 |
Abs (x, simple_typ_of tye f T, simple_term_of tye f t) |
|
236 |
| simple_term_of tye f (PAppl (t, u)) = |
|
237 |
simple_term_of tye f t $ simple_term_of tye f u |
|
238 |
| simple_term_of tye f (Constraint (t, _)) = simple_term_of tye f t; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
239 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
240 |
|
32141 | 241 |
(* typs_terms_of *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
242 |
|
32141 | 243 |
fun typs_terms_of tye used maxidx (Ts, ts) = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
244 |
let |
32141 | 245 |
val used' = fold (add_names tye) ts (fold (add_namesT tye) Ts used); |
246 |
val parms = rev (fold (add_parms tye) ts (fold (add_parmsT tye) Ts [])); |
|
27263 | 247 |
val names = Name.invents used' ("?" ^ Name.aT) (length parms); |
32141 | 248 |
val tab = Inttab.make (parms ~~ names); |
249 |
fun f i = (the (Inttab.lookup tab i), maxidx + 1); |
|
250 |
in (map (simple_typ_of tye f) Ts, map (simple_term_of tye f) ts) end; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
251 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
252 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
253 |
|
32141 | 254 |
(** order-sorted unification of types **) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
255 |
|
32141 | 256 |
exception NO_UNIFIER of string * pretyp Inttab.table; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
257 |
|
19465 | 258 |
fun unify pp tsig = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
259 |
let |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
260 |
(* adjust sorts of parameters *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
261 |
|
19465 | 262 |
fun not_of_sort x S' S = |
14828 | 263 |
"Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^ |
264 |
Pretty.string_of_sort pp S; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
265 |
|
32141 | 266 |
fun meet (_, []) tye_idx = tye_idx |
267 |
| meet (Param (i, S'), S) (tye_idx as (tye, idx)) = |
|
268 |
if Type.subsort tsig (S', S) then tye_idx |
|
269 |
else (Inttab.update_new (i, |
|
270 |
Param (idx, Type.inter_sort tsig (S', S))) tye, idx + 1) |
|
271 |
| meet (PType (a, Ts), S) (tye_idx as (tye, _)) = |
|
272 |
meets (Ts, Type.arity_sorts pp tsig a S |
|
273 |
handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx |
|
274 |
| meet (PTFree (x, S'), S) (tye_idx as (tye, _)) = |
|
275 |
if Type.subsort tsig (S', S) then tye_idx |
|
276 |
else raise NO_UNIFIER (not_of_sort x S' S, tye) |
|
277 |
| meet (PTVar (xi, S'), S) (tye_idx as (tye, _)) = |
|
278 |
if Type.subsort tsig (S', S) then tye_idx |
|
279 |
else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye) |
|
280 |
and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) = |
|
281 |
meets (Ts, Ss) (meet (deref tye T, S) tye_idx) |
|
282 |
| meets _ tye_idx = tye_idx; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
283 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
284 |
|
35013 | 285 |
(* occurs check and assignment *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
286 |
|
32141 | 287 |
fun occurs_check tye i (Param (i', S)) = |
288 |
if i = i' then raise NO_UNIFIER ("Occurs check!", tye) |
|
32146 | 289 |
else |
290 |
(case Inttab.lookup tye i' of |
|
32141 | 291 |
NONE => () |
292 |
| SOME T => occurs_check tye i T) |
|
293 |
| occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts |
|
294 |
| occurs_check _ _ _ = (); |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
295 |
|
37235
cafcc42bae77
assign now applies meet before update_new to avoid misleading error message.
berghofe
parents:
35013
diff
changeset
|
296 |
fun assign i (T as Param (i', _)) S tye_idx = |
32141 | 297 |
if i = i' then tye_idx |
37235
cafcc42bae77
assign now applies meet before update_new to avoid misleading error message.
berghofe
parents:
35013
diff
changeset
|
298 |
else tye_idx |> meet (T, S) |>> Inttab.update_new (i, T) |
cafcc42bae77
assign now applies meet before update_new to avoid misleading error message.
berghofe
parents:
35013
diff
changeset
|
299 |
| assign i T S (tye_idx as (tye, _)) = |
cafcc42bae77
assign now applies meet before update_new to avoid misleading error message.
berghofe
parents:
35013
diff
changeset
|
300 |
(occurs_check tye i T; tye_idx |> meet (T, S) |>> Inttab.update_new (i, T)); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
301 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
302 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
303 |
(* unification *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
304 |
|
39286 | 305 |
fun show_tycon (a, Ts) = |
306 |
quote (Pretty.string_of_typ pp (Type (a, replicate (length Ts) dummyT))); |
|
307 |
||
32146 | 308 |
fun unif (T1, T2) (tye_idx as (tye, idx)) = |
309 |
(case (deref tye T1, deref tye T2) of |
|
32141 | 310 |
(Param (i, S), T) => assign i T S tye_idx |
311 |
| (T, Param (i, S)) => assign i T S tye_idx |
|
312 |
| (PType (a, Ts), PType (b, Us)) => |
|
2979 | 313 |
if a <> b then |
39286 | 314 |
raise NO_UNIFIER |
315 |
("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye) |
|
32141 | 316 |
else fold unif (Ts ~~ Us) tye_idx |
32146 | 317 |
| (T, U) => if T = U then tye_idx else raise NO_UNIFIER ("", tye)); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
318 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
319 |
in unif end; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
320 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
321 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
322 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
323 |
(** type inference **) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
324 |
|
22698 | 325 |
(* appl_error *) |
326 |
||
14828 | 327 |
fun appl_error pp why t T u U = |
8087 | 328 |
["Type error in application: " ^ why, |
329 |
"", |
|
330 |
Pretty.string_of (Pretty.block |
|
14828 | 331 |
[Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t, |
332 |
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]), |
|
8087 | 333 |
Pretty.string_of (Pretty.block |
14828 | 334 |
[Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u, |
335 |
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]), |
|
8087 | 336 |
""]; |
337 |
||
5635 | 338 |
|
32141 | 339 |
(* infer *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
340 |
|
19465 | 341 |
fun infer pp tsig = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
342 |
let |
2979 | 343 |
(* errors *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
344 |
|
2979 | 345 |
fun unif_failed msg = |
14828 | 346 |
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n"; |
2979 | 347 |
|
32141 | 348 |
fun prep_output tye bs ts Ts = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
349 |
let |
32141 | 350 |
val (Ts_bTs', ts') = typs_terms_of tye Name.context ~1 (Ts @ map snd bs, ts); |
19012 | 351 |
val (Ts', Ts'') = chop (length Ts) Ts_bTs'; |
27263 | 352 |
fun prep t = |
353 |
let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) |
|
354 |
in Term.subst_bounds (map Syntax.mark_boundT xs, t) end; |
|
355 |
in (map prep ts', Ts') end; |
|
2979 | 356 |
|
357 |
fun err_loose i = |
|
3784 | 358 |
raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []); |
2979 | 359 |
|
32141 | 360 |
fun err_appl msg tye bs t T u U = |
2979 | 361 |
let |
32141 | 362 |
val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]; |
3510 | 363 |
val why = |
364 |
(case T' of |
|
14828 | 365 |
Type ("fun", _) => "Incompatible operand type" |
366 |
| _ => "Operator not of function type"); |
|
367 |
val text = unif_failed msg ^ cat_lines (appl_error pp why t' T' u' U'); |
|
3784 | 368 |
in raise TYPE (text, [T', U'], [t', u']) end; |
2979 | 369 |
|
32141 | 370 |
fun err_constraint msg tye bs t T U = |
2979 | 371 |
let |
32141 | 372 |
val ([t'], [T', U']) = prep_output tye bs [t] [T, U]; |
2979 | 373 |
val text = cat_lines |
374 |
[unif_failed msg, |
|
5635 | 375 |
"Cannot meet type constraint:", "", |
14828 | 376 |
Pretty.string_of (Pretty.block |
377 |
[Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t', |
|
378 |
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T']), |
|
379 |
Pretty.string_of (Pretty.block |
|
380 |
[Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp U']), ""]; |
|
3784 | 381 |
in raise TYPE (text, [T', U'], [t']) end; |
2979 | 382 |
|
383 |
||
384 |
(* main *) |
|
385 |
||
19465 | 386 |
val unif = unify pp tsig; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
387 |
|
32141 | 388 |
fun inf _ (PConst (_, T)) tye_idx = (T, tye_idx) |
389 |
| inf _ (PFree (_, T)) tye_idx = (T, tye_idx) |
|
390 |
| inf _ (PVar (_, T)) tye_idx = (T, tye_idx) |
|
391 |
| inf bs (PBound i) tye_idx = |
|
392 |
(snd (nth bs i handle Subscript => err_loose i), tye_idx) |
|
393 |
| inf bs (PAbs (x, T, t)) tye_idx = |
|
394 |
let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx |
|
395 |
in (PType ("fun", [T, U]), tye_idx') end |
|
396 |
| inf bs (PAppl (t, u)) tye_idx = |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
397 |
let |
32141 | 398 |
val (T, tye_idx') = inf bs t tye_idx; |
399 |
val (U, (tye, idx)) = inf bs u tye_idx'; |
|
400 |
val V = Param (idx, []); |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
401 |
val U_to_V = PType ("fun", [U, V]); |
32141 | 402 |
val tye_idx'' = unif (U_to_V, T) (tye, idx + 1) |
403 |
handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U; |
|
404 |
in (V, tye_idx'') end |
|
405 |
| inf bs (Constraint (t, U)) tye_idx = |
|
406 |
let val (T, tye_idx') = inf bs t tye_idx in |
|
407 |
(T, |
|
408 |
unif (T, U) tye_idx' |
|
32146 | 409 |
handle NO_UNIFIER (msg, tye) => err_constraint msg tye bs t T U) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
410 |
end; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
411 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
412 |
in inf [] end; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
413 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
414 |
|
22698 | 415 |
(* infer_types *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
416 |
|
27263 | 417 |
fun infer_types pp tsig check_typs const_type var_type used maxidx raw_ts = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
418 |
let |
22698 | 419 |
(*constrain vars*) |
420 |
val get_type = the_default dummyT o var_type; |
|
421 |
val constrain_vars = Term.map_aterms |
|
24682 | 422 |
(fn Free (x, T) => constrain T (Free (x, get_type (x, ~1))) |
423 |
| Var (xi, T) => constrain T (Var (xi, get_type xi)) |
|
22698 | 424 |
| t => t); |
425 |
||
27263 | 426 |
(*convert to preterms*) |
427 |
val ts = burrow_types check_typs raw_ts; |
|
32141 | 428 |
val (ts', (_, _, idx)) = |
429 |
fold_map (preterm_of const_type is_param o constrain_vars) ts |
|
430 |
(Vartab.empty, Vartab.empty, 0); |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
431 |
|
27263 | 432 |
(*do type inference*) |
32141 | 433 |
val (tye, _) = fold (snd oo infer pp tsig) ts' (Inttab.empty, idx); |
434 |
in #2 (typs_terms_of tye used maxidx ([], ts')) end; |
|
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset
|
435 |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
436 |
end; |