author | wenzelm |
Mon, 13 Sep 2010 12:42:08 +0200 | |
changeset 39295 | 6e8b0672c6a2 |
parent 39294 | 27fae73fe769 |
child 39296 | e275d581a218 |
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 |
24504 | 10 |
val is_param: indexname -> bool |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
11 |
val is_paramT: typ -> bool |
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset
|
12 |
val param: int -> string * sort -> typ |
22771 | 13 |
val paramify_vars: typ -> typ |
18339 | 14 |
val paramify_dummies: typ -> int -> typ * int |
39295
6e8b0672c6a2
Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
wenzelm
parents:
39294
diff
changeset
|
15 |
val fixate_params: Proof.context -> term list -> term list |
39290
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
16 |
val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) -> |
27263 | 17 |
term list -> term list |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
18 |
end; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
19 |
|
37145
01aa36932739
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
wenzelm
parents:
35013
diff
changeset
|
20 |
structure Type_Infer: TYPE_INFER = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
21 |
struct |
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 |
|
22698 | 24 |
(** type parameters and constraints **) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
25 |
|
22698 | 26 |
fun anyT S = TFree ("'_dummy_", S); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
27 |
|
22698 | 28 |
|
39286 | 29 |
(* type inference parameters -- may get instantiated *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
30 |
|
24504 | 31 |
fun is_param (x, _: int) = String.isPrefix "?" x; |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
32 |
|
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
33 |
fun is_paramT (TVar (xi, _)) = is_param xi |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
34 |
| is_paramT _ = false; |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
35 |
|
22698 | 36 |
fun param i (x, S) = TVar (("?" ^ x, i), S); |
37 |
||
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
38 |
fun mk_param i S = TVar (("?'a", i), S); |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
39 |
|
32002
1a35de4112bb
tuned paramify_vars: Term_Subst.map_atypsT_option;
wenzelm
parents:
31977
diff
changeset
|
40 |
val paramify_vars = |
32146 | 41 |
Same.commit |
42 |
(Term_Subst.map_atypsT_same |
|
43 |
(fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME)); |
|
22771 | 44 |
|
22698 | 45 |
val paramify_dummies = |
46 |
let |
|
47 |
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
|
48 |
|
22698 | 49 |
fun paramify (TFree ("'_dummy_", S)) maxidx = dummy S maxidx |
50 |
| paramify (Type ("dummy", _)) maxidx = dummy [] maxidx |
|
51 |
| paramify (Type (a, Ts)) maxidx = |
|
52 |
let val (Ts', maxidx') = fold_map paramify Ts maxidx |
|
53 |
in (Type (a, Ts'), maxidx') end |
|
54 |
| paramify T maxidx = (T, maxidx); |
|
55 |
in paramify end; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
56 |
|
39295
6e8b0672c6a2
Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
wenzelm
parents:
39294
diff
changeset
|
57 |
fun fixate_params ctxt ts = |
24764 | 58 |
let |
59 |
fun subst_param (xi, S) (inst, used) = |
|
60 |
if is_param xi then |
|
61 |
let |
|
24848 | 62 |
val [a] = Name.invents used Name.aT 1; |
24764 | 63 |
val used' = Name.declare a used; |
64 |
in (((xi, S), TFree (a, S)) :: inst, used') end |
|
65 |
else (inst, used); |
|
39295
6e8b0672c6a2
Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
wenzelm
parents:
39294
diff
changeset
|
66 |
val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt); |
6e8b0672c6a2
Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
wenzelm
parents:
39294
diff
changeset
|
67 |
val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used); |
31977 | 68 |
in (map o map_types) (Term_Subst.instantiateT inst) ts end; |
24764 | 69 |
|
2957
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 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
72 |
(** prepare types/terms: create inference parameters **) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
73 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
74 |
(* prepare_typ *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
75 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
76 |
fun prepare_typ typ params_idx = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
77 |
let |
32141 | 78 |
val (params', idx) = fold_atyps |
20668 | 79 |
(fn TVar (xi as (x, _), S) => |
32141 | 80 |
(fn ps_idx as (ps, idx) => |
39287 | 81 |
if is_param xi andalso not (Vartab.defined ps xi) |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
82 |
then (Vartab.update (xi, mk_param idx S) ps, idx + 1) else ps_idx) |
32141 | 83 |
| _ => I) typ params_idx; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
84 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
85 |
fun prepare (T as Type (a, Ts)) idx = |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
86 |
if T = dummyT then (mk_param idx [], idx + 1) |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
87 |
else |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
88 |
let val (Ts', idx') = fold_map prepare Ts idx |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
89 |
in (Type (a, Ts'), idx') end |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
90 |
| prepare (T as TVar (xi, _)) idx = |
20735 | 91 |
(case Vartab.lookup params' xi of |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
92 |
NONE => T |
32141 | 93 |
| SOME p => p, idx) |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
94 |
| prepare (TFree ("'_dummy_", S)) idx = (mk_param idx S, idx + 1) |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
95 |
| prepare (T as TFree _) idx = (T, idx); |
32141 | 96 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
97 |
val (typ', idx') = prepare typ idx; |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
98 |
in (typ', (params', idx')) end; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
99 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
100 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
101 |
(* prepare_term *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
102 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
103 |
fun prepare_term const_type tm (vparams, params, idx) = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
104 |
let |
32141 | 105 |
fun add_vparm xi (ps_idx as (ps, idx)) = |
20735 | 106 |
if not (Vartab.defined ps xi) then |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
107 |
(Vartab.update (xi, mk_param idx []) ps, idx + 1) |
32141 | 108 |
else ps_idx; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
109 |
|
32141 | 110 |
val (vparams', idx') = fold_aterms |
20668 | 111 |
(fn Var (_, Type ("_polymorphic_", _)) => I |
112 |
| Var (xi, _) => add_vparm xi |
|
113 |
| Free (x, _) => add_vparm (x, ~1) |
|
114 |
| _ => I) |
|
32141 | 115 |
tm (vparams, idx); |
20735 | 116 |
fun var_param xi = the (Vartab.lookup vparams' xi); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
117 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
118 |
fun polyT_of T idx = apsnd snd (prepare_typ (paramify_vars T) (Vartab.empty, idx)); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
119 |
|
22698 | 120 |
fun constraint T t ps = |
20668 | 121 |
if T = dummyT then (t, ps) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
122 |
else |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
123 |
let val (T', ps') = prepare_typ T ps |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
124 |
in (Type.constraint T' t, ps') end; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
125 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
126 |
fun prepare (Const ("_type_constraint_", T) $ t) ps_idx = |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
127 |
let |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
128 |
val (T', ps_idx') = prepare_typ T ps_idx; |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
129 |
val (t', ps_idx'') = prepare t ps_idx'; |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
130 |
in (Const ("_type_constraint_", T') $ t', ps_idx'') end |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
131 |
| prepare (Const (c, T)) (ps, idx) = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
132 |
(case const_type c of |
32141 | 133 |
SOME U => |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
134 |
let val (U', idx') = polyT_of U idx |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
135 |
in constraint T (Const (c, U')) (ps, idx') end |
39291
4b632bb847a8
Type_Infer.infer_types: plain error instead of kernel exception TYPE;
wenzelm
parents:
39290
diff
changeset
|
136 |
| NONE => error ("Undeclared constant: " ^ quote c)) |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
137 |
| prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) = |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
138 |
let val (T', idx') = polyT_of T idx |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
139 |
in (Var (xi, T'), (ps, idx')) end |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
140 |
| prepare (Var (xi, T)) ps_idx = constraint T (Var (xi, var_param xi)) ps_idx |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
141 |
| prepare (Free (x, T)) ps_idx = constraint T (Free (x, var_param (x, ~1))) ps_idx |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
142 |
| prepare (Bound i) ps_idx = (Bound i, ps_idx) |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
143 |
| prepare (Abs (x, T, t)) ps_idx = |
39292
6f085332c7d3
Type_Infer.preterm: eliminated separate Constraint;
wenzelm
parents:
39291
diff
changeset
|
144 |
let |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
145 |
val (T', ps_idx') = prepare_typ T ps_idx; |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
146 |
val (t', ps_idx'') = prepare t ps_idx'; |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
147 |
in (Abs (x, T', t'), ps_idx'') end |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
148 |
| prepare (t $ u) ps_idx = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
149 |
let |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
150 |
val (t', ps_idx') = prepare t ps_idx; |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
151 |
val (u', ps_idx'') = prepare u ps_idx'; |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
152 |
in (t' $ u', ps_idx'') end; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
153 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
154 |
val (tm', (params', idx'')) = prepare tm (params, idx'); |
32141 | 155 |
in (tm', (vparams', params', idx'')) end; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
156 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
157 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
158 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
159 |
(** finish types/terms: standardize remaining parameters **) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
160 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
161 |
(* dereferenced views *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
162 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
163 |
fun deref tye (T as TVar (xi, _)) = |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
164 |
(case Vartab.lookup tye xi of |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
165 |
NONE => T |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
166 |
| SOME U => deref tye U) |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
167 |
| deref tye T = T; |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
168 |
|
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
169 |
fun add_parms tye T = |
32146 | 170 |
(case deref tye T of |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
171 |
Type (_, Ts) => fold (add_parms tye) Ts |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
172 |
| TVar (xi, _) => if is_param xi then insert (op =) xi else I |
32146 | 173 |
| _ => I); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
174 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
175 |
fun add_names tye T = |
32146 | 176 |
(case deref tye T of |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
177 |
Type (_, Ts) => fold (add_names tye) Ts |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
178 |
| TFree (x, _) => Name.declare x |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
179 |
| TVar ((x, i), _) => if is_param (x, i) then I else Name.declare x); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
180 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
181 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
182 |
(* finish *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
183 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
184 |
fun finish ctxt tye (Ts, ts) = |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
185 |
let |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
186 |
val used = |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
187 |
(fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt)); |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
188 |
val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts [])); |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
189 |
val names = Name.invents used ("?" ^ Name.aT) (length parms); |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
190 |
val tab = Vartab.make (parms ~~ names); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
191 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
192 |
fun finish_typ T = |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
193 |
(case deref tye T of |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
194 |
Type (a, Ts) => Type (a, map finish_typ Ts) |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
195 |
| U as TFree _ => U |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
196 |
| U as TVar (xi, S) => |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
197 |
(case Vartab.lookup tab xi of |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
198 |
NONE => U |
39295
6e8b0672c6a2
Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
wenzelm
parents:
39294
diff
changeset
|
199 |
| SOME a => TVar ((a, 0), S))); |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
200 |
in (map finish_typ Ts, map (Type.strip_constraints o Term.map_types finish_typ) ts) end; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
201 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
202 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
203 |
|
32141 | 204 |
(** order-sorted unification of types **) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
205 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
206 |
exception NO_UNIFIER of string * typ Vartab.table; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
207 |
|
39290
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
208 |
fun unify ctxt pp = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
209 |
let |
39290
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
210 |
val thy = ProofContext.theory_of ctxt; |
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
211 |
val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy); |
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
212 |
|
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
213 |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
214 |
(* adjust sorts of parameters *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
215 |
|
19465 | 216 |
fun not_of_sort x S' S = |
39290
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
217 |
"Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^ |
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
218 |
Syntax.string_of_sort ctxt S; |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
219 |
|
32141 | 220 |
fun meet (_, []) tye_idx = tye_idx |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
221 |
| meet (Type (a, Ts), S) (tye_idx as (tye, _)) = |
39291
4b632bb847a8
Type_Infer.infer_types: plain error instead of kernel exception TYPE;
wenzelm
parents:
39290
diff
changeset
|
222 |
meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
223 |
| meet (TFree (x, S'), S) (tye_idx as (tye, _)) = |
39290
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
224 |
if Sign.subsort thy (S', S) then tye_idx |
32141 | 225 |
else raise NO_UNIFIER (not_of_sort x S' S, tye) |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
226 |
| meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) = |
39290
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
227 |
if Sign.subsort thy (S', S) then tye_idx |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
228 |
else if is_param xi then |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
229 |
(Vartab.update_new (xi, mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1) |
32141 | 230 |
else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye) |
231 |
and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) = |
|
232 |
meets (Ts, Ss) (meet (deref tye T, S) tye_idx) |
|
233 |
| meets _ tye_idx = tye_idx; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
234 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
235 |
|
35013 | 236 |
(* occurs check and assignment *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
237 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
238 |
fun occurs_check tye xi (TVar (xi', S)) = |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
239 |
if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye) |
32146 | 240 |
else |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
241 |
(case Vartab.lookup tye xi' of |
32141 | 242 |
NONE => () |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
243 |
| SOME T => occurs_check tye xi T) |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
244 |
| occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts |
32141 | 245 |
| occurs_check _ _ _ = (); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
246 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
247 |
fun assign xi (T as TVar (xi', _)) S env = |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
248 |
if xi = xi' then env |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
249 |
else env |> meet (T, S) |>> Vartab.update_new (xi, T) |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
250 |
| assign xi T S (env as (tye, _)) = |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
251 |
(occurs_check tye xi T; env |> meet (T, S) |>> Vartab.update_new (xi, T)); |
2957
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 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
254 |
(* unification *) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
255 |
|
39286 | 256 |
fun show_tycon (a, Ts) = |
39290
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
257 |
quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT))); |
39286 | 258 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
259 |
fun unif (T1, T2) (env as (tye, _)) = |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
260 |
(case pairself (`is_paramT o deref tye) (T1, T2) of |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
261 |
((true, TVar (xi, S)), (_, T)) => assign xi T S env |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
262 |
| ((_, T), (true, TVar (xi, S))) => assign xi T S env |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
263 |
| ((_, Type (a, Ts)), (_, Type (b, Us))) => |
2979 | 264 |
if a <> b then |
39286 | 265 |
raise NO_UNIFIER |
266 |
("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye) |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
267 |
else fold unif (Ts ~~ Us) env |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
268 |
| ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye)); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
269 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
270 |
in unif end; |
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 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
274 |
(** type inference **) |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
275 |
|
32141 | 276 |
(* infer *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
277 |
|
39290
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
278 |
fun infer ctxt = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
279 |
let |
39290
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
280 |
val pp = Syntax.pp ctxt; |
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
281 |
|
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
282 |
|
2979 | 283 |
(* errors *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
284 |
|
32141 | 285 |
fun prep_output tye bs ts Ts = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
286 |
let |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
287 |
val (Ts_bTs', ts') = finish ctxt tye (Ts @ map snd bs, ts); |
19012 | 288 |
val (Ts', Ts'') = chop (length Ts) Ts_bTs'; |
27263 | 289 |
fun prep t = |
290 |
let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) |
|
291 |
in Term.subst_bounds (map Syntax.mark_boundT xs, t) end; |
|
292 |
in (map prep ts', Ts') end; |
|
2979 | 293 |
|
39291
4b632bb847a8
Type_Infer.infer_types: plain error instead of kernel exception TYPE;
wenzelm
parents:
39290
diff
changeset
|
294 |
fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i); |
2979 | 295 |
|
39289
92b50c8bb67b
common Type.appl_error, which also covers explicit constraints;
wenzelm
parents:
39288
diff
changeset
|
296 |
fun unif_failed msg = |
92b50c8bb67b
common Type.appl_error, which also covers explicit constraints;
wenzelm
parents:
39288
diff
changeset
|
297 |
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n"; |
92b50c8bb67b
common Type.appl_error, which also covers explicit constraints;
wenzelm
parents:
39288
diff
changeset
|
298 |
|
32141 | 299 |
fun err_appl msg tye bs t T u U = |
39291
4b632bb847a8
Type_Infer.infer_types: plain error instead of kernel exception TYPE;
wenzelm
parents:
39290
diff
changeset
|
300 |
let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U] |
4b632bb847a8
Type_Infer.infer_types: plain error instead of kernel exception TYPE;
wenzelm
parents:
39290
diff
changeset
|
301 |
in error (unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n") end; |
2979 | 302 |
|
303 |
||
304 |
(* main *) |
|
305 |
||
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
306 |
fun inf _ (Const (_, T)) tye_idx = (T, tye_idx) |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
307 |
| inf _ (Free (_, T)) tye_idx = (T, tye_idx) |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
308 |
| inf _ (Var (_, T)) tye_idx = (T, tye_idx) |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
309 |
| inf bs (Bound i) tye_idx = |
32141 | 310 |
(snd (nth bs i handle Subscript => err_loose i), tye_idx) |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
311 |
| inf bs (Abs (x, T, t)) tye_idx = |
32141 | 312 |
let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
313 |
in (T --> U, tye_idx') end |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
314 |
| inf bs (t $ u) tye_idx = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
315 |
let |
32141 | 316 |
val (T, tye_idx') = inf bs t tye_idx; |
317 |
val (U, (tye, idx)) = inf bs u tye_idx'; |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
318 |
val V = mk_param idx []; |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
319 |
val tye_idx'' = unify ctxt pp (U --> V, T) (tye, idx + 1) |
32141 | 320 |
handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U; |
39292
6f085332c7d3
Type_Infer.preterm: eliminated separate Constraint;
wenzelm
parents:
39291
diff
changeset
|
321 |
in (V, tye_idx'') end; |
2957
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 |
in inf [] end; |
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
324 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
325 |
|
22698 | 326 |
(* infer_types *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
327 |
|
39290
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
328 |
fun infer_types ctxt const_type var_type raw_ts = |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
329 |
let |
22698 | 330 |
(*constrain vars*) |
331 |
val get_type = the_default dummyT o var_type; |
|
332 |
val constrain_vars = Term.map_aterms |
|
39288 | 333 |
(fn Free (x, T) => Type.constraint T (Free (x, get_type (x, ~1))) |
334 |
| Var (xi, T) => Type.constraint T (Var (xi, get_type xi)) |
|
22698 | 335 |
| t => t); |
336 |
||
27263 | 337 |
(*convert to preterms*) |
39290
44e4d8dfd6bf
load type_infer.ML later -- proper context for Type_Infer.infer_types;
wenzelm
parents:
39289
diff
changeset
|
338 |
val ts = burrow_types (Syntax.check_typs ctxt) raw_ts; |
32141 | 339 |
val (ts', (_, _, idx)) = |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
340 |
fold_map (prepare_term const_type o constrain_vars) ts |
32141 | 341 |
(Vartab.empty, Vartab.empty, 0); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
342 |
|
27263 | 343 |
(*do type inference*) |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
344 |
val (tye, _) = fold (snd oo infer ctxt) ts' (Vartab.empty, idx); |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
345 |
in #2 (finish ctxt tye ([], ts')) end; |
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset
|
346 |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
347 |
end; |