author | wenzelm |
Thu, 01 Dec 2011 14:29:14 +0100 | |
changeset 45709 | 87017fcbad83 |
parent 43329 | 84472e198515 |
child 53672 | df8068269e90 |
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 |
|
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
42400
diff
changeset
|
4 |
Basic representation of type-inference problems. |
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 |
24504 | 9 |
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
|
10 |
val is_paramT: typ -> bool |
42400
26c8c9cabb24
more precise treatment of existing type inference parameters;
wenzelm
parents:
42386
diff
changeset
|
11 |
val param_maxidx: term -> int -> int |
26c8c9cabb24
more precise treatment of existing type inference parameters;
wenzelm
parents:
42386
diff
changeset
|
12 |
val param_maxidx_of: term list -> int |
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset
|
13 |
val param: int -> string * sort -> typ |
40286 | 14 |
val mk_param: int -> sort -> typ |
39296 | 15 |
val anyT: sort -> typ |
22771 | 16 |
val paramify_vars: typ -> typ |
18339 | 17 |
val paramify_dummies: typ -> int -> typ * int |
39296 | 18 |
val deref: typ Vartab.table -> typ -> typ |
19 |
val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list |
|
20 |
val fixate: Proof.context -> 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 |
|
22698 | 26 |
(** type parameters and constraints **) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
27 |
|
39286 | 28 |
(* type inference parameters -- may get instantiated *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
29 |
|
24504 | 30 |
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
|
31 |
|
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
32 |
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
|
33 |
| is_paramT _ = false; |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
34 |
|
42400
26c8c9cabb24
more precise treatment of existing type inference parameters;
wenzelm
parents:
42386
diff
changeset
|
35 |
val param_maxidx = |
26c8c9cabb24
more precise treatment of existing type inference parameters;
wenzelm
parents:
42386
diff
changeset
|
36 |
(Term.fold_types o Term.fold_atyps) |
26c8c9cabb24
more precise treatment of existing type inference parameters;
wenzelm
parents:
42386
diff
changeset
|
37 |
(fn (TVar (xi as (_, i), _)) => if is_param xi then Integer.max i else I | _ => I); |
26c8c9cabb24
more precise treatment of existing type inference parameters;
wenzelm
parents:
42386
diff
changeset
|
38 |
|
26c8c9cabb24
more precise treatment of existing type inference parameters;
wenzelm
parents:
42386
diff
changeset
|
39 |
fun param_maxidx_of ts = fold param_maxidx ts ~1; |
26c8c9cabb24
more precise treatment of existing type inference parameters;
wenzelm
parents:
42386
diff
changeset
|
40 |
|
22698 | 41 |
fun param i (x, S) = TVar (("?" ^ x, i), S); |
42 |
||
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
43 |
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
|
44 |
|
39296 | 45 |
|
46 |
(* pre-stage parameters *) |
|
47 |
||
48 |
fun anyT S = TFree ("'_dummy_", S); |
|
49 |
||
32002
1a35de4112bb
tuned paramify_vars: Term_Subst.map_atypsT_option;
wenzelm
parents:
31977
diff
changeset
|
50 |
val paramify_vars = |
32146 | 51 |
Same.commit |
52 |
(Term_Subst.map_atypsT_same |
|
53 |
(fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME)); |
|
22771 | 54 |
|
22698 | 55 |
val paramify_dummies = |
56 |
let |
|
57 |
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
|
58 |
|
22698 | 59 |
fun paramify (TFree ("'_dummy_", S)) maxidx = dummy S maxidx |
60 |
| paramify (Type ("dummy", _)) maxidx = dummy [] maxidx |
|
61 |
| paramify (Type (a, Ts)) maxidx = |
|
62 |
let val (Ts', maxidx') = fold_map paramify Ts maxidx |
|
63 |
in (Type (a, Ts'), maxidx') end |
|
64 |
| paramify T maxidx = (T, maxidx); |
|
65 |
in paramify end; |
|
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
66 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
67 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
68 |
|
39296 | 69 |
(** results **) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
70 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
71 |
(* dereferenced views *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
72 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
73 |
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
|
74 |
(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
|
75 |
NONE => T |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
76 |
| SOME U => deref tye U) |
42400
26c8c9cabb24
more precise treatment of existing type inference parameters;
wenzelm
parents:
42386
diff
changeset
|
77 |
| deref _ T = T; |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
78 |
|
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
79 |
fun add_parms tye T = |
32146 | 80 |
(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
|
81 |
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
|
82 |
| TVar (xi, _) => if is_param xi then insert (op =) xi else I |
32146 | 83 |
| _ => I); |
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 add_names tye T = |
32146 | 86 |
(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
|
87 |
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
|
88 |
| TFree (x, _) => Name.declare x |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
89 |
| 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
|
90 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
91 |
|
39296 | 92 |
(* finish -- standardize remaining parameters *) |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
93 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
94 |
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
|
95 |
let |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
96 |
val used = |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
97 |
(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
|
98 |
val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts [])); |
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
42405
diff
changeset
|
99 |
val names = Name.invent used ("?" ^ Name.aT) (length parms); |
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
100 |
val tab = Vartab.make (parms ~~ names); |
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
101 |
|
39294
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
102 |
fun finish_typ T = |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
103 |
(case deref tye T of |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
104 |
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
|
105 |
| U as TFree _ => U |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
106 |
| U as TVar (xi, S) => |
27fae73fe769
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
wenzelm
parents:
39292
diff
changeset
|
107 |
(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
|
108 |
NONE => U |
39295
6e8b0672c6a2
Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
wenzelm
parents:
39294
diff
changeset
|
109 |
| 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
|
110 |
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
|
111 |
|
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
112 |
|
39296 | 113 |
(* fixate -- introduce fresh type variables *) |
114 |
||
115 |
fun fixate ctxt ts = |
|
116 |
let |
|
117 |
fun subst_param (xi, S) (inst, used) = |
|
118 |
if is_param xi then |
|
119 |
let |
|
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
42405
diff
changeset
|
120 |
val [a] = Name.invent used Name.aT 1; |
39296 | 121 |
val used' = Name.declare a used; |
122 |
in (((xi, S), TFree (a, S)) :: inst, used') end |
|
123 |
else (inst, used); |
|
124 |
val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt); |
|
125 |
val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used); |
|
126 |
in (map o map_types) (Term_Subst.instantiateT inst) ts end; |
|
127 |
||
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset
|
128 |
end; |