5 Type inference. |
5 Type inference. |
6 *) |
6 *) |
7 |
7 |
8 signature TYPE_INFER = |
8 signature TYPE_INFER = |
9 sig |
9 sig |
|
10 val anyT: sort -> typ |
|
11 val logicT: typ |
10 val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T) |
12 val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T) |
11 -> (string -> typ option) -> Sorts.classrel -> Sorts.arities |
13 -> (string -> typ option) -> Sorts.classrel -> Sorts.arities |
12 -> string list -> bool -> (indexname -> bool) -> term list -> typ list |
14 -> string list -> bool -> (indexname -> bool) -> term list -> typ list |
13 -> term list * typ list * (indexname * typ) list |
15 -> term list * typ list * (indexname * typ) list |
14 val appl_error: (term -> Pretty.T) -> (typ -> Pretty.T) |
16 val appl_error: (term -> Pretty.T) -> (typ -> Pretty.T) |
26 |
28 |
27 parse trees (type term): |
29 parse trees (type term): |
28 A very complicated structure produced by the syntax module's |
30 A very complicated structure produced by the syntax module's |
29 read functions. Encodes types and sorts as terms; may contain |
31 read functions. Encodes types and sorts as terms; may contain |
30 explicit constraints and partial typing information (where |
32 explicit constraints and partial typing information (where |
31 dummyT serves as wildcard). |
33 dummies serve as wildcards). |
32 |
34 |
33 Parse trees are INTERNAL! Users should never encounter them, |
35 Parse trees are INTERNAL! Users should never encounter them, |
34 except in parse / print translation functions. |
36 except in parse / print translation functions. |
35 |
37 |
36 raw terms (type term): |
38 raw terms (type term): |
37 Provide the user interface to type inferences. They may contain |
39 Provide the user interface to type inferences. They may contain |
38 partial type information (dummyT is wildcard) or explicit type |
40 partial type information (dummies are wildcards) or explicit |
39 constraints (introduced via constrain: term -> typ -> term). |
41 type constraints (introduced via constrain: term -> typ -> |
|
42 term). |
40 |
43 |
41 The type inference function also lets users specify a certain |
44 The type inference function also lets users specify a certain |
42 subset of TVars to be treated as non-rigid inference parameters. |
45 subset of TVars to be treated as non-rigid inference parameters. |
43 |
46 |
44 preterms (type preterm): |
47 preterms (type preterm): |
91 |
94 |
92 (** raw typs/terms to pretyps/preterms **) |
95 (** raw typs/terms to pretyps/preterms **) |
93 |
96 |
94 (* pretyp(s)_of *) |
97 (* pretyp(s)_of *) |
95 |
98 |
|
99 fun anyT S = TFree ("'_dummy_", S); |
|
100 val logicT = anyT logicS; |
|
101 |
96 fun pretyp_of is_param (params, typ) = |
102 fun pretyp_of is_param (params, typ) = |
97 let |
103 let |
98 fun add_parms (ps, TVar (xi as (x, _), S)) = |
104 fun add_parms (ps, TVar (xi as (x, _), S)) = |
99 if is_param xi andalso is_none (assoc (ps, xi)) |
105 if is_param xi andalso is_none (assoc (ps, xi)) |
100 then (xi, mk_param S) :: ps else ps |
106 then (xi, mk_param S) :: ps else ps |
105 |
111 |
106 fun pre_of (TVar (v as (xi, _))) = |
112 fun pre_of (TVar (v as (xi, _))) = |
107 (case assoc (params', xi) of |
113 (case assoc (params', xi) of |
108 None => PTVar v |
114 None => PTVar v |
109 | Some p => p) |
115 | Some p => p) |
|
116 | pre_of (TFree ("'_dummy_", S)) = mk_param S |
110 | pre_of (TFree v) = PTFree v |
117 | pre_of (TFree v) = PTFree v |
111 | pre_of (T as Type (a, Ts)) = |
118 | pre_of (T as Type (a, Ts)) = |
112 if T = dummyT then mk_param [] |
119 if T = dummyT then mk_param [] |
113 else PType (a, map pre_of Ts); |
120 else PType (a, map pre_of Ts); |
114 in (params', pre_of typ) end; |
121 in (params', pre_of typ) end; |
138 val preT_of = pretyp_of is_param; |
145 val preT_of = pretyp_of is_param; |
139 |
146 |
140 fun constrain (ps, t) T = |
147 fun constrain (ps, t) T = |
141 if T = dummyT then (ps, t) |
148 if T = dummyT then (ps, t) |
142 else |
149 else |
143 let val (ps', T') = preT_of (ps, T) in |
150 let val (ps', T') = preT_of (ps, T) |
144 (ps', Constraint (t, T')) |
151 in (ps', Constraint (t, T')) end; |
145 end; |
|
146 |
152 |
147 fun pre_of (ps, Const (c, T)) = |
153 fun pre_of (ps, Const (c, T)) = |
148 (case const_type c of |
154 (case const_type c of |
149 Some U => constrain (ps, PConst (c, snd (pretyp_of (K true) ([], U)))) T |
155 Some U => constrain (ps, PConst (c, snd (pretyp_of (K true) ([], U)))) T |
150 | None => raise TYPE ("No such constant: " ^ quote c, [], [])) |
156 | None => raise TYPE ("No such constant: " ^ quote c, [], [])) |
275 | occurs_check _ _ = (); |
281 | occurs_check _ _ = (); |
276 |
282 |
277 fun assign r T S = |
283 fun assign r T S = |
278 (case deref T of |
284 (case deref T of |
279 T' as Link (r' as ref (Param _)) => |
285 T' as Link (r' as ref (Param _)) => |
280 if r = r' then () else (r := T'; meet (T', S)) |
286 if r = r' then () else (meet (T', S); r := T') |
281 | T' => (occurs_check r T'; r := T'; meet (T', S))); |
287 | T' => (occurs_check r T'; meet (T', S); r := T')); |
282 |
288 |
283 |
289 |
284 (* unification *) |
290 (* unification *) |
285 |
291 |
286 fun unif (Link (r as ref (Param S)), T) = assign r T S |
292 fun unif (Link (r as ref (Param S)), T) = assign r T S |
298 |
304 |
299 |
305 |
300 (** type inference **) |
306 (** type inference **) |
301 |
307 |
302 fun appl_error prt prT why t T u U = |
308 fun appl_error prt prT why t T u U = |
303 ["Type error in application: " ^ why, |
309 ["Type error in application: " ^ why, |
304 "", |
310 "", |
305 Pretty.string_of |
311 Pretty.string_of (Pretty.block |
306 (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t, |
312 [Pretty.str "Operator:", Pretty.brk 2, prt t, Pretty.str " ::", Pretty.brk 1, prT T]), |
307 Pretty.str " ::", Pretty.brk 1, prT T]), |
313 Pretty.string_of (Pretty.block |
308 Pretty.string_of |
314 [Pretty.str "Operand:", Pretty.brk 3, prt u, Pretty.str " ::", Pretty.brk 1, prT U]), |
309 (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u, |
315 ""]; |
310 Pretty.str " ::", Pretty.brk 1, prT U]), |
316 |
311 ""]; |
|
312 |
317 |
313 (* infer *) (*DESTRUCTIVE*) |
318 (* infer *) (*DESTRUCTIVE*) |
314 |
319 |
315 fun infer prt prT classrel arities = |
320 fun infer prt prT classrel arities = |
316 let |
321 let |