author | blanchet |
Wed, 04 Mar 2009 10:45:52 +0100 | |
changeset 30240 | 5b25fee0362c |
parent 29606 | fedb8be05f24 |
child 31977 | e03059ae2d82 |
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 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
23 |
structure TypeInfer: TYPE_INFER = |
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 |
||
37 |
(* user parameters *) |
|
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 |
||
22771 | 42 |
val paramify_vars = Term.map_atyps (fn TVar ((x, i), S) => param i (x, S) | T => T); |
43 |
||
22698 | 44 |
val paramify_dummies = |
45 |
let |
|
46 |
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
|
47 |
|
22698 | 48 |
fun paramify (TFree ("'_dummy_", S)) maxidx = dummy S maxidx |
49 |
| paramify (Type ("dummy", _)) maxidx = dummy [] maxidx |
|
50 |
| paramify (Type (a, Ts)) maxidx = |
|
51 |
let val (Ts', maxidx') = fold_map paramify Ts maxidx |
|
52 |
in (Type (a, Ts'), maxidx') end |
|
53 |
| paramify T maxidx = (T, maxidx); |
|
54 |
in paramify end; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
55 |
|
24764 | 56 |
fun fixate_params name_context ts = |
57 |
let |
|
58 |
fun subst_param (xi, S) (inst, used) = |
|
59 |
if is_param xi then |
|
60 |
let |
|
24848 | 61 |
val [a] = Name.invents used Name.aT 1; |
24764 | 62 |
val used' = Name.declare a used; |
63 |
in (((xi, S), TFree (a, S)) :: inst, used') end |
|
64 |
else (inst, used); |
|
65 |
val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context; |
|
66 |
val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context'); |
|
67 |
in (map o map_types) (TermSubst.instantiateT inst) ts end; |
|
68 |
||
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
69 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
70 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
71 |
(** pretyps and preterms **) |
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 |
(*links to parameters may get instantiated, anything else is rigid*) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
74 |
datatype pretyp = |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
75 |
PType of string * pretyp list | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
76 |
PTFree of string * sort | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
77 |
PTVar of indexname * sort | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
78 |
Param of sort | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
79 |
Link of pretyp ref; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
80 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
81 |
datatype preterm = |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
82 |
PConst of string * pretyp | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
83 |
PFree of string * pretyp | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
84 |
PVar of indexname * pretyp | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
85 |
PBound of int | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
86 |
PAbs of string * pretyp * preterm | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
87 |
PAppl of preterm * preterm | |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
88 |
Constraint of preterm * pretyp; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
89 |
|
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 |
(* utils *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
92 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
93 |
val mk_param = Link o ref o Param; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
94 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
95 |
fun deref (T as Link (ref (Param _))) = T |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
96 |
| deref (Link (ref T)) = deref T |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
97 |
| deref T = T; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
98 |
|
16195 | 99 |
fun fold_pretyps f (PConst (_, T)) x = f T x |
100 |
| fold_pretyps f (PFree (_, T)) x = f T x |
|
101 |
| fold_pretyps f (PVar (_, T)) x = f T x |
|
102 |
| fold_pretyps _ (PBound _) x = x |
|
103 |
| fold_pretyps f (PAbs (_, T, t)) x = fold_pretyps f t (f T x) |
|
104 |
| fold_pretyps f (PAppl (t, u)) x = fold_pretyps f u (fold_pretyps f t x) |
|
105 |
| 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
|
106 |
|
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 |
(** raw typs/terms to pretyps/preterms **) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
110 |
|
20668 | 111 |
(* pretyp_of *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
112 |
|
24504 | 113 |
fun pretyp_of is_para typ params = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
114 |
let |
20668 | 115 |
val params' = fold_atyps |
116 |
(fn TVar (xi as (x, _), S) => |
|
117 |
(fn ps => |
|
24504 | 118 |
if is_para xi andalso not (Vartab.defined ps xi) |
20735 | 119 |
then Vartab.update (xi, mk_param S) ps else ps) |
20668 | 120 |
| _ => I) typ params; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
121 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
122 |
fun pre_of (TVar (v as (xi, _))) = |
20735 | 123 |
(case Vartab.lookup params' xi of |
15531 | 124 |
NONE => PTVar v |
125 |
| SOME p => p) |
|
8087 | 126 |
| pre_of (TFree ("'_dummy_", S)) = mk_param S |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
127 |
| pre_of (TFree v) = PTFree v |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
128 |
| pre_of (T as Type (a, Ts)) = |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
129 |
if T = dummyT then mk_param [] |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
130 |
else PType (a, map pre_of Ts); |
20668 | 131 |
in (pre_of typ, params') end; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
132 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
133 |
|
20668 | 134 |
(* preterm_of *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
135 |
|
24504 | 136 |
fun preterm_of const_type is_para tm (vparams, params) = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
137 |
let |
20668 | 138 |
fun add_vparm xi ps = |
20735 | 139 |
if not (Vartab.defined ps xi) then |
140 |
Vartab.update (xi, mk_param []) ps |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
141 |
else ps; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
142 |
|
20668 | 143 |
val vparams' = fold_aterms |
144 |
(fn Var (_, Type ("_polymorphic_", _)) => I |
|
145 |
| Var (xi, _) => add_vparm xi |
|
146 |
| Free (x, _) => add_vparm (x, ~1) |
|
147 |
| _ => I) |
|
148 |
tm vparams; |
|
20735 | 149 |
fun var_param xi = the (Vartab.lookup vparams' xi); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
150 |
|
24504 | 151 |
val preT_of = pretyp_of is_para; |
20735 | 152 |
fun polyT_of T = fst (pretyp_of (K true) T Vartab.empty); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
153 |
|
22698 | 154 |
fun constraint T t ps = |
20668 | 155 |
if T = dummyT then (t, ps) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
156 |
else |
20668 | 157 |
let val (T', ps') = preT_of T ps |
158 |
in (Constraint (t, T'), ps') end; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
159 |
|
20668 | 160 |
fun pre_of (Const (c, T)) ps = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
161 |
(case const_type c of |
22698 | 162 |
SOME U => constraint T (PConst (c, polyT_of U)) ps |
15531 | 163 |
| NONE => raise TYPE ("No such constant: " ^ quote c, [], [])) |
20735 | 164 |
| pre_of (Var (xi, Type ("_polymorphic_", [T]))) ps = (PVar (xi, polyT_of T), ps) |
22698 | 165 |
| pre_of (Var (xi, T)) ps = constraint T (PVar (xi, var_param xi)) ps |
166 |
| pre_of (Free (x, T)) ps = constraint T (PFree (x, var_param (x, ~1))) ps |
|
20668 | 167 |
| pre_of (Const ("_type_constraint_", Type ("fun", [T, _])) $ t) ps = |
22698 | 168 |
pre_of t ps |-> constraint T |
20668 | 169 |
| pre_of (Bound i) ps = (PBound i, ps) |
170 |
| pre_of (Abs (x, T, t)) ps = |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
171 |
let |
20668 | 172 |
val (T', ps') = preT_of T ps; |
173 |
val (t', ps'') = pre_of t ps'; |
|
174 |
in (PAbs (x, T', t'), ps'') end |
|
175 |
| pre_of (t $ u) ps = |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
176 |
let |
20668 | 177 |
val (t', ps') = pre_of t ps; |
178 |
val (u', ps'') = pre_of u ps'; |
|
179 |
in (PAppl (t', u'), ps'') end; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
180 |
|
20668 | 181 |
val (tm', params') = pre_of tm params; |
182 |
in (tm', (vparams', params')) end; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
183 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
184 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
185 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
186 |
(** pretyps/terms to typs/terms **) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
187 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
188 |
(* add_parms *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
189 |
|
16195 | 190 |
fun add_parmsT (PType (_, Ts)) rs = fold add_parmsT Ts rs |
20854 | 191 |
| add_parmsT (Link (r as ref (Param _))) rs = insert (op =) r rs |
16195 | 192 |
| add_parmsT (Link (ref T)) rs = add_parmsT T rs |
193 |
| add_parmsT _ rs = rs; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
194 |
|
16195 | 195 |
val add_parms = fold_pretyps add_parmsT; |
2957
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 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
198 |
(* add_names *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
199 |
|
20161 | 200 |
fun add_namesT (PType (_, Ts)) = fold add_namesT Ts |
201 |
| add_namesT (PTFree (x, _)) = Name.declare x |
|
202 |
| add_namesT (PTVar ((x, _), _)) = Name.declare x |
|
203 |
| add_namesT (Link (ref T)) = add_namesT T |
|
204 |
| add_namesT (Param _) = I; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
205 |
|
16195 | 206 |
val add_names = fold_pretyps add_namesT; |
2957
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 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
209 |
(* simple_typ/term_of *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
210 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
211 |
(*deref links, fail on params*) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
212 |
fun simple_typ_of (PType (a, Ts)) = Type (a, map simple_typ_of Ts) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
213 |
| simple_typ_of (PTFree v) = TFree v |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
214 |
| simple_typ_of (PTVar v) = TVar v |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
215 |
| simple_typ_of (Link (ref T)) = simple_typ_of T |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
216 |
| simple_typ_of (Param _) = sys_error "simple_typ_of: illegal Param"; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
217 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
218 |
(*convert types, drop constraints*) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
219 |
fun simple_term_of (PConst (c, T)) = Const (c, simple_typ_of T) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
220 |
| simple_term_of (PFree (x, T)) = Free (x, simple_typ_of T) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
221 |
| simple_term_of (PVar (xi, T)) = Var (xi, simple_typ_of T) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
222 |
| simple_term_of (PBound i) = Bound i |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
223 |
| simple_term_of (PAbs (x, T, t)) = Abs (x, simple_typ_of T, simple_term_of t) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
224 |
| simple_term_of (PAppl (t, u)) = simple_term_of t $ simple_term_of u |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
225 |
| simple_term_of (Constraint (t, _)) = simple_term_of t; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
226 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
227 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
228 |
(* typs_terms_of *) (*DESTRUCTIVE*) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
229 |
|
27263 | 230 |
fun typs_terms_of used maxidx (Ts, ts) = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
231 |
let |
27263 | 232 |
fun elim (r as ref (Param S), x) = r := PTVar ((x, maxidx + 1), S) |
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
233 |
| elim _ = (); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
234 |
|
16195 | 235 |
val used' = fold add_names ts (fold add_namesT Ts used); |
236 |
val parms = rev (fold add_parms ts (fold add_parmsT Ts [])); |
|
27263 | 237 |
val names = Name.invents used' ("?" ^ Name.aT) (length parms); |
238 |
val _ = ListPair.app elim (parms, names); |
|
239 |
in (map simple_typ_of Ts, map simple_term_of ts) end; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
240 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
241 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
242 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
243 |
(** order-sorted unification of types **) (*DESTRUCTIVE*) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
244 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
245 |
exception NO_UNIFIER of string; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
246 |
|
19465 | 247 |
fun unify pp tsig = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
248 |
let |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
249 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
250 |
(* adjust sorts of parameters *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
251 |
|
19465 | 252 |
fun not_of_sort x S' S = |
14828 | 253 |
"Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^ |
254 |
Pretty.string_of_sort pp S; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
255 |
|
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
256 |
fun meet (_, []) = () |
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
257 |
| meet (Link (r as (ref (Param S'))), S) = |
19465 | 258 |
if Type.subsort tsig (S', S) then () |
259 |
else r := mk_param (Type.inter_sort tsig (S', S)) |
|
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
260 |
| meet (Link (ref T), S) = meet (T, S) |
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
261 |
| meet (PType (a, Ts), S) = |
19465 | 262 |
ListPair.app meet (Ts, Type.arity_sorts pp tsig a S |
263 |
handle ERROR msg => raise NO_UNIFIER msg) |
|
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
264 |
| meet (PTFree (x, S'), S) = |
19465 | 265 |
if Type.subsort tsig (S', S) then () |
266 |
else raise NO_UNIFIER (not_of_sort x S' S) |
|
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
267 |
| meet (PTVar (xi, S'), S) = |
19465 | 268 |
if Type.subsort tsig (S', S) then () |
22678 | 269 |
else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S) |
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
270 |
| meet (Param _, _) = sys_error "meet"; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
271 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
272 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
273 |
(* occurs check and assigment *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
274 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
275 |
fun occurs_check r (Link (r' as ref T)) = |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
276 |
if r = r' then raise NO_UNIFIER "Occurs check!" |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
277 |
else occurs_check r T |
15570 | 278 |
| occurs_check r (PType (_, Ts)) = List.app (occurs_check r) Ts |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
279 |
| occurs_check _ _ = (); |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
280 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
281 |
fun assign r T S = |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
282 |
(case deref T of |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
283 |
T' as Link (r' as ref (Param _)) => |
8087 | 284 |
if r = r' then () else (meet (T', S); r := T') |
285 |
| T' => (occurs_check r T'; meet (T', S); r := T')); |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
286 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
287 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
288 |
(* unification *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
289 |
|
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
290 |
fun unif (Link (r as ref (Param S)), T) = assign r T S |
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
291 |
| unif (T, Link (r as ref (Param S))) = assign r T S |
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
292 |
| unif (Link (ref T), U) = unif (T, U) |
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
293 |
| unif (T, Link (ref U)) = unif (T, U) |
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
294 |
| unif (PType (a, Ts), PType (b, Us)) = |
2979 | 295 |
if a <> b then |
14828 | 296 |
raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b) |
16195 | 297 |
else ListPair.app unif (Ts, Us) |
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
298 |
| unif (T, U) = if T = U then () else raise NO_UNIFIER ""; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
299 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
300 |
in unif end; |
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 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
304 |
(** type inference **) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
305 |
|
22698 | 306 |
(* appl_error *) |
307 |
||
14828 | 308 |
fun appl_error pp why t T u U = |
8087 | 309 |
["Type error in application: " ^ why, |
310 |
"", |
|
311 |
Pretty.string_of (Pretty.block |
|
14828 | 312 |
[Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t, |
313 |
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]), |
|
8087 | 314 |
Pretty.string_of (Pretty.block |
14828 | 315 |
[Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u, |
316 |
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]), |
|
8087 | 317 |
""]; |
318 |
||
5635 | 319 |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
320 |
(* infer *) (*DESTRUCTIVE*) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
321 |
|
19465 | 322 |
fun infer pp tsig = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
323 |
let |
2979 | 324 |
(* errors *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
325 |
|
2979 | 326 |
fun unif_failed msg = |
14828 | 327 |
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n"; |
2979 | 328 |
|
329 |
fun prep_output bs ts Ts = |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
330 |
let |
27263 | 331 |
val (Ts_bTs', ts') = typs_terms_of Name.context ~1 (Ts @ map snd bs, ts); |
19012 | 332 |
val (Ts', Ts'') = chop (length Ts) Ts_bTs'; |
27263 | 333 |
fun prep t = |
334 |
let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) |
|
335 |
in Term.subst_bounds (map Syntax.mark_boundT xs, t) end; |
|
336 |
in (map prep ts', Ts') end; |
|
2979 | 337 |
|
338 |
fun err_loose i = |
|
3784 | 339 |
raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []); |
2979 | 340 |
|
3510 | 341 |
fun err_appl msg bs t T u U = |
2979 | 342 |
let |
3510 | 343 |
val ([t', u'], [T', U']) = prep_output bs [t, u] [T, U]; |
344 |
val why = |
|
345 |
(case T' of |
|
14828 | 346 |
Type ("fun", _) => "Incompatible operand type" |
347 |
| _ => "Operator not of function type"); |
|
348 |
val text = unif_failed msg ^ cat_lines (appl_error pp why t' T' u' U'); |
|
3784 | 349 |
in raise TYPE (text, [T', U'], [t', u']) end; |
2979 | 350 |
|
351 |
fun err_constraint msg bs t T U = |
|
352 |
let |
|
353 |
val ([t'], [T', U']) = prep_output bs [t] [T, U]; |
|
354 |
val text = cat_lines |
|
355 |
[unif_failed msg, |
|
5635 | 356 |
"Cannot meet type constraint:", "", |
14828 | 357 |
Pretty.string_of (Pretty.block |
358 |
[Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t', |
|
359 |
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T']), |
|
360 |
Pretty.string_of (Pretty.block |
|
361 |
[Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp U']), ""]; |
|
3784 | 362 |
in raise TYPE (text, [T', U'], [t']) end; |
2979 | 363 |
|
364 |
||
365 |
(* main *) |
|
366 |
||
19465 | 367 |
val unif = unify pp tsig; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
368 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
369 |
fun inf _ (PConst (_, T)) = T |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
370 |
| inf _ (PFree (_, T)) = T |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
371 |
| inf _ (PVar (_, T)) = T |
30240 | 372 |
| inf bs (PBound i) = snd (nth bs i handle Subscript => err_loose i) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
373 |
| inf bs (PAbs (x, T, t)) = PType ("fun", [T, inf ((x, T) :: bs) t]) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
374 |
| inf bs (PAppl (t, u)) = |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
375 |
let |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
376 |
val T = inf bs t; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
377 |
val U = inf bs u; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
378 |
val V = mk_param []; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
379 |
val U_to_V = PType ("fun", [U, V]); |
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
380 |
val _ = unif (U_to_V, T) handle NO_UNIFIER msg => err_appl msg bs t T u U; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
381 |
in V end |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
382 |
| inf bs (Constraint (t, U)) = |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
383 |
let val T = inf bs t in |
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset
|
384 |
unif (T, U) handle NO_UNIFIER msg => err_constraint msg bs t T U; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
385 |
T |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
386 |
end; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
387 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
388 |
in inf [] end; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
389 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
390 |
|
22698 | 391 |
(* infer_types *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
392 |
|
27263 | 393 |
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
|
394 |
let |
22698 | 395 |
(*constrain vars*) |
396 |
val get_type = the_default dummyT o var_type; |
|
397 |
val constrain_vars = Term.map_aterms |
|
24682 | 398 |
(fn Free (x, T) => constrain T (Free (x, get_type (x, ~1))) |
399 |
| Var (xi, T) => constrain T (Var (xi, get_type xi)) |
|
22698 | 400 |
| t => t); |
401 |
||
27263 | 402 |
(*convert to preterms*) |
403 |
val ts = burrow_types check_typs raw_ts; |
|
22698 | 404 |
val (ts', (vps, ps)) = |
27263 | 405 |
fold_map (preterm_of const_type is_param o constrain_vars) ts (Vartab.empty, Vartab.empty); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
406 |
|
27263 | 407 |
(*do type inference*) |
408 |
val _ = List.app (ignore o infer pp tsig) ts'; |
|
409 |
in #2 (typs_terms_of used maxidx ([], ts')) end; |
|
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset
|
410 |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
411 |
end; |