author  wenzelm 
Sun, 12 Sep 2010 19:55:45 +0200  
changeset 39289  92b50c8bb67b 
parent 39288  f1ae2493d93f 
child 39290  44e4d8dfd6bf 
permissions  rwrr 
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 
24504  11 
val is_param: indexname > 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 
24764  15 
val fixate_params: Name.context > term list > term list 
24485
687bbb686ef9
infer_types: general check_typs instead of Type.cert_typ_mode;
wenzelm
parents:
24275
diff
changeset

16 
val infer_types: Pretty.pp > Type.tsig > (typ list > typ list) > 
27263  17 
(string > typ option) > (indexname > typ option) > Name.context > int > 
18 
term list > term list 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

19 
end; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

20 

37145
01aa36932739
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
wenzelm
parents:
35013
diff
changeset

21 
structure Type_Infer: TYPE_INFER = 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

22 
struct 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

23 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

24 

22698  25 
(** type parameters and constraints **) 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

26 

22698  27 
fun anyT S = TFree ("'_dummy_", S); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

28 

22698  29 
(*indicate polymorphic Vars*) 
30 
fun polymorphicT T = Type ("_polymorphic_", [T]); 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

31 

22698  32 

39286  33 
(* type inference parameters  may get instantiated *) 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

34 

24504  35 
fun is_param (x, _: int) = String.isPrefix "?" x; 
22698  36 
fun param i (x, S) = TVar (("?" ^ x, i), S); 
37 

32002
1a35de4112bb
tuned paramify_vars: Term_Subst.map_atypsT_option;
wenzelm
parents:
31977
diff
changeset

38 
val paramify_vars = 
32146  39 
Same.commit 
40 
(Term_Subst.map_atypsT_same 

41 
(fn TVar ((x, i), S) => (param i (x, S))  _ => raise Same.SAME)); 

22771  42 

22698  43 
val paramify_dummies = 
44 
let 

45 
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

46 

22698  47 
fun paramify (TFree ("'_dummy_", S)) maxidx = dummy S maxidx 
48 
 paramify (Type ("dummy", _)) maxidx = dummy [] maxidx 

49 
 paramify (Type (a, Ts)) maxidx = 

50 
let val (Ts', maxidx') = fold_map paramify Ts maxidx 

51 
in (Type (a, Ts'), maxidx') end 

52 
 paramify T maxidx = (T, maxidx); 

53 
in paramify end; 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

54 

24764  55 
fun fixate_params name_context ts = 
56 
let 

57 
fun subst_param (xi, S) (inst, used) = 

58 
if is_param xi then 

59 
let 

24848  60 
val [a] = Name.invents used Name.aT 1; 
24764  61 
val used' = Name.declare a used; 
62 
in (((xi, S), TFree (a, S)) :: inst, used') end 

63 
else (inst, used); 

64 
val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context; 

65 
val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context'); 

31977  66 
in (map o map_types) (Term_Subst.instantiateT inst) ts end; 
24764  67 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

68 

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 
(** pretyps and preterms **) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

71 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

72 
datatype pretyp = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

73 
PType of string * pretyp list  
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

74 
PTFree of string * sort  
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

75 
PTVar of indexname * sort  
32141  76 
Param of int * sort; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

77 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

78 
datatype preterm = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

79 
PConst of string * pretyp  
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

80 
PFree of string * pretyp  
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

81 
PVar of indexname * pretyp  
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

82 
PBound of int  
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

83 
PAbs of string * pretyp * preterm  
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

84 
PAppl of preterm * preterm  
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

85 
Constraint of preterm * pretyp; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

86 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

87 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

88 
(* utils *) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

89 

32146  90 
fun deref tye (T as Param (i, S)) = 
91 
(case Inttab.lookup tye i of 

92 
NONE => T 

93 
 SOME U => deref tye U) 

32141  94 
 deref tye T = T; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

95 

16195  96 
fun fold_pretyps f (PConst (_, T)) x = f T x 
97 
 fold_pretyps f (PFree (_, T)) x = f T x 

98 
 fold_pretyps f (PVar (_, T)) x = f T x 

99 
 fold_pretyps _ (PBound _) x = x 

100 
 fold_pretyps f (PAbs (_, T, t)) x = fold_pretyps f t (f T x) 

101 
 fold_pretyps f (PAppl (t, u)) x = fold_pretyps f u (fold_pretyps f t x) 

102 
 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

103 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

104 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

105 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

106 
(** raw typs/terms to pretyps/preterms **) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

107 

20668  108 
(* pretyp_of *) 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

109 

39287  110 
fun pretyp_of typ params_idx = 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

111 
let 
32141  112 
val (params', idx) = fold_atyps 
20668  113 
(fn TVar (xi as (x, _), S) => 
32141  114 
(fn ps_idx as (ps, idx) => 
39287  115 
if is_param xi andalso not (Vartab.defined ps xi) 
32141  116 
then (Vartab.update (xi, Param (idx, S)) ps, idx + 1) else ps_idx) 
117 
 _ => I) typ params_idx; 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

118 

32141  119 
fun pre_of (TVar (v as (xi, _))) idx = 
20735  120 
(case Vartab.lookup params' xi of 
15531  121 
NONE => PTVar v 
32141  122 
 SOME p => p, idx) 
123 
 pre_of (TFree ("'_dummy_", S)) idx = (Param (idx, S), idx + 1) 

124 
 pre_of (TFree v) idx = (PTFree v, idx) 

125 
 pre_of (T as Type (a, Ts)) idx = 

126 
if T = dummyT then (Param (idx, []), idx + 1) 

127 
else 

128 
let val (Ts', idx') = fold_map pre_of Ts idx 

129 
in (PType (a, Ts'), idx') end; 

130 

131 
val (ptyp, idx') = pre_of typ idx; 

132 
in (ptyp, (params', idx')) end; 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

133 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

134 

20668  135 
(* preterm_of *) 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

136 

39287  137 
fun preterm_of const_type tm (vparams, params, idx) = 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

138 
let 
32141  139 
fun add_vparm xi (ps_idx as (ps, idx)) = 
20735  140 
if not (Vartab.defined ps xi) then 
32141  141 
(Vartab.update (xi, Param (idx, [])) ps, idx + 1) 
142 
else ps_idx; 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

143 

32141  144 
val (vparams', idx') = fold_aterms 
20668  145 
(fn Var (_, Type ("_polymorphic_", _)) => I 
146 
 Var (xi, _) => add_vparm xi 

147 
 Free (x, _) => add_vparm (x, ~1) 

148 
 _ => I) 

32141  149 
tm (vparams, idx); 
20735  150 
fun var_param xi = the (Vartab.lookup vparams' xi); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

151 

39287  152 
fun polyT_of T idx = apsnd snd (pretyp_of (paramify_vars T) (Vartab.empty, idx)); 
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 
39287  157 
let val (T', ps') = pretyp_of T ps 
20668  158 
in (Constraint (t, T'), ps') end; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

159 

32141  160 
fun pre_of (Const (c, T)) (ps, idx) = 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

161 
(case const_type c of 
32141  162 
SOME U => 
163 
let val (pU, idx') = polyT_of U idx 

164 
in constraint T (PConst (c, pU)) (ps, idx') end 

39286  165 
 NONE => raise TYPE ("Undeclared constant: " ^ quote c, [], [])) 
32141  166 
 pre_of (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) = 
167 
let val (pT, idx') = polyT_of T idx 

168 
in (PVar (xi, pT), (ps, idx')) end 

169 
 pre_of (Var (xi, T)) ps_idx = constraint T (PVar (xi, var_param xi)) ps_idx 

170 
 pre_of (Free (x, T)) ps_idx = constraint T (PFree (x, var_param (x, ~1))) ps_idx 

171 
 pre_of (Const ("_type_constraint_", Type ("fun", [T, _])) $ t) ps_idx = 

172 
pre_of t ps_idx > constraint T 

173 
 pre_of (Bound i) ps_idx = (PBound i, ps_idx) 

174 
 pre_of (Abs (x, T, t)) ps_idx = 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

175 
let 
39287  176 
val (T', ps_idx') = pretyp_of T ps_idx; 
32141  177 
val (t', ps_idx'') = pre_of t ps_idx'; 
178 
in (PAbs (x, T', t'), ps_idx'') end 

179 
 pre_of (t $ u) ps_idx = 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

180 
let 
32141  181 
val (t', ps_idx') = pre_of t ps_idx; 
182 
val (u', ps_idx'') = pre_of u ps_idx'; 

183 
in (PAppl (t', u'), ps_idx'') end; 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

184 

32141  185 
val (tm', (params', idx'')) = pre_of tm (params, idx'); 
186 
in (tm', (vparams', params', idx'')) end; 

2957
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 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

189 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

190 
(** pretyps/terms to typs/terms **) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

191 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

192 
(* add_parms *) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

193 

32146  194 
fun add_parmsT tye T = 
195 
(case deref tye T of 

32141  196 
PType (_, Ts) => fold (add_parmsT tye) Ts 
197 
 Param (i, _) => insert (op =) i 

32146  198 
 _ => I); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

199 

32141  200 
fun add_parms tye = fold_pretyps (add_parmsT tye); 
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 
(* add_names *) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

204 

32146  205 
fun add_namesT tye T = 
206 
(case deref tye T of 

32141  207 
PType (_, Ts) => fold (add_namesT tye) Ts 
208 
 PTFree (x, _) => Name.declare x 

209 
 PTVar ((x, _), _) => Name.declare x 

32146  210 
 Param _ => I); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

211 

32141  212 
fun add_names tye = fold_pretyps (add_namesT tye); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

213 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

214 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

215 
(* simple_typ/term_of *) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

216 

32146  217 
fun simple_typ_of tye f T = 
218 
(case deref tye T of 

32141  219 
PType (a, Ts) => Type (a, map (simple_typ_of tye f) Ts) 
220 
 PTFree v => TFree v 

221 
 PTVar v => TVar v 

32146  222 
 Param (i, S) => TVar (f i, S)); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

223 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

224 
(*convert types, drop constraints*) 
32141  225 
fun simple_term_of tye f (PConst (c, T)) = Const (c, simple_typ_of tye f T) 
226 
 simple_term_of tye f (PFree (x, T)) = Free (x, simple_typ_of tye f T) 

227 
 simple_term_of tye f (PVar (xi, T)) = Var (xi, simple_typ_of tye f T) 

228 
 simple_term_of tye f (PBound i) = Bound i 

229 
 simple_term_of tye f (PAbs (x, T, t)) = 

230 
Abs (x, simple_typ_of tye f T, simple_term_of tye f t) 

231 
 simple_term_of tye f (PAppl (t, u)) = 

232 
simple_term_of tye f t $ simple_term_of tye f u 

233 
 simple_term_of tye f (Constraint (t, _)) = simple_term_of tye f t; 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

234 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

235 

32141  236 
(* typs_terms_of *) 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

237 

32141  238 
fun typs_terms_of tye used maxidx (Ts, ts) = 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

239 
let 
32141  240 
val used' = fold (add_names tye) ts (fold (add_namesT tye) Ts used); 
241 
val parms = rev (fold (add_parms tye) ts (fold (add_parmsT tye) Ts [])); 

27263  242 
val names = Name.invents used' ("?" ^ Name.aT) (length parms); 
32141  243 
val tab = Inttab.make (parms ~~ names); 
244 
fun f i = (the (Inttab.lookup tab i), maxidx + 1); 

245 
in (map (simple_typ_of tye f) Ts, map (simple_term_of tye f) ts) end; 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

246 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

247 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

248 

32141  249 
(** ordersorted unification of types **) 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

250 

32141  251 
exception NO_UNIFIER of string * pretyp Inttab.table; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

252 

19465  253 
fun unify pp tsig = 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

254 
let 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

255 
(* adjust sorts of parameters *) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

256 

19465  257 
fun not_of_sort x S' S = 
14828  258 
"Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^ 
259 
Pretty.string_of_sort pp S; 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

260 

32141  261 
fun meet (_, []) tye_idx = tye_idx 
262 
 meet (Param (i, S'), S) (tye_idx as (tye, idx)) = 

263 
if Type.subsort tsig (S', S) then tye_idx 

264 
else (Inttab.update_new (i, 

265 
Param (idx, Type.inter_sort tsig (S', S))) tye, idx + 1) 

266 
 meet (PType (a, Ts), S) (tye_idx as (tye, _)) = 

267 
meets (Ts, Type.arity_sorts pp tsig a S 

268 
handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx 

269 
 meet (PTFree (x, S'), S) (tye_idx as (tye, _)) = 

270 
if Type.subsort tsig (S', S) then tye_idx 

271 
else raise NO_UNIFIER (not_of_sort x S' S, tye) 

272 
 meet (PTVar (xi, S'), S) (tye_idx as (tye, _)) = 

273 
if Type.subsort tsig (S', S) then tye_idx 

274 
else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye) 

275 
and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) = 

276 
meets (Ts, Ss) (meet (deref tye T, S) tye_idx) 

277 
 meets _ tye_idx = tye_idx; 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

278 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

279 

35013  280 
(* occurs check and assignment *) 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

281 

32141  282 
fun occurs_check tye i (Param (i', S)) = 
283 
if i = i' then raise NO_UNIFIER ("Occurs check!", tye) 

32146  284 
else 
285 
(case Inttab.lookup tye i' of 

32141  286 
NONE => () 
287 
 SOME T => occurs_check tye i T) 

288 
 occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts 

289 
 occurs_check _ _ _ = (); 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

290 

37235
cafcc42bae77
assign now applies meet before update_new to avoid misleading error message.
berghofe
parents:
35013
diff
changeset

291 
fun assign i (T as Param (i', _)) S tye_idx = 
32141  292 
if i = i' then tye_idx 
37235
cafcc42bae77
assign now applies meet before update_new to avoid misleading error message.
berghofe
parents:
35013
diff
changeset

293 
else tye_idx > meet (T, S) >> Inttab.update_new (i, T) 
cafcc42bae77
assign now applies meet before update_new to avoid misleading error message.
berghofe
parents:
35013
diff
changeset

294 
 assign i T S (tye_idx as (tye, _)) = 
cafcc42bae77
assign now applies meet before update_new to avoid misleading error message.
berghofe
parents:
35013
diff
changeset

295 
(occurs_check tye i T; tye_idx > meet (T, S) >> Inttab.update_new (i, T)); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

296 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

297 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

298 
(* unification *) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

299 

39286  300 
fun show_tycon (a, Ts) = 
301 
quote (Pretty.string_of_typ pp (Type (a, replicate (length Ts) dummyT))); 

302 

32146  303 
fun unif (T1, T2) (tye_idx as (tye, idx)) = 
304 
(case (deref tye T1, deref tye T2) of 

32141  305 
(Param (i, S), T) => assign i T S tye_idx 
306 
 (T, Param (i, S)) => assign i T S tye_idx 

307 
 (PType (a, Ts), PType (b, Us)) => 

2979  308 
if a <> b then 
39286  309 
raise NO_UNIFIER 
310 
("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye) 

32141  311 
else fold unif (Ts ~~ Us) tye_idx 
32146  312 
 (T, U) => if T = U then tye_idx else raise NO_UNIFIER ("", tye)); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

313 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

314 
in unif end; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

315 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

316 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

317 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

318 
(** type inference **) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

319 

32141  320 
(* infer *) 
2957
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 

32141  326 
fun prep_output tye bs ts Ts = 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

327 
let 
32141  328 
val (Ts_bTs', ts') = typs_terms_of tye Name.context ~1 (Ts @ map snd bs, ts); 
19012  329 
val (Ts', Ts'') = chop (length Ts) Ts_bTs'; 
27263  330 
fun prep t = 
331 
let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) 

332 
in Term.subst_bounds (map Syntax.mark_boundT xs, t) end; 

333 
in (map prep ts', Ts') end; 

2979  334 

335 
fun err_loose i = 

3784  336 
raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []); 
2979  337 

39289
92b50c8bb67b
common Type.appl_error, which also covers explicit constraints;
wenzelm
parents:
39288
diff
changeset

338 
fun unif_failed msg = 
92b50c8bb67b
common Type.appl_error, which also covers explicit constraints;
wenzelm
parents:
39288
diff
changeset

339 
"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

340 

32141  341 
fun err_appl msg tye bs t T u U = 
2979  342 
let 
32141  343 
val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]; 
39289
92b50c8bb67b
common Type.appl_error, which also covers explicit constraints;
wenzelm
parents:
39288
diff
changeset

344 
val text = unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n"; 
3784  345 
in raise TYPE (text, [T', U'], [t', u']) end; 
2979  346 

32141  347 
fun err_constraint msg tye bs t T U = 
2979  348 
let 
32141  349 
val ([t'], [T', U']) = prep_output tye bs [t] [T, U]; 
39289
92b50c8bb67b
common Type.appl_error, which also covers explicit constraints;
wenzelm
parents:
39288
diff
changeset

350 
val text = 
92b50c8bb67b
common Type.appl_error, which also covers explicit constraints;
wenzelm
parents:
39288
diff
changeset

351 
unif_failed msg ^ 
92b50c8bb67b
common Type.appl_error, which also covers explicit constraints;
wenzelm
parents:
39288
diff
changeset

352 
Type.appl_error pp (Const ("_type_constraint_", U' > U')) (U' > U') t' T' ^ "\n"; 
3784  353 
in raise TYPE (text, [T', U'], [t']) end; 
2979  354 

355 

356 
(* main *) 

357 

19465  358 
val unif = unify pp tsig; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

359 

32141  360 
fun inf _ (PConst (_, T)) tye_idx = (T, tye_idx) 
361 
 inf _ (PFree (_, T)) tye_idx = (T, tye_idx) 

362 
 inf _ (PVar (_, T)) tye_idx = (T, tye_idx) 

363 
 inf bs (PBound i) tye_idx = 

364 
(snd (nth bs i handle Subscript => err_loose i), tye_idx) 

365 
 inf bs (PAbs (x, T, t)) tye_idx = 

366 
let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx 

367 
in (PType ("fun", [T, U]), tye_idx') end 

368 
 inf bs (PAppl (t, u)) tye_idx = 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

369 
let 
32141  370 
val (T, tye_idx') = inf bs t tye_idx; 
371 
val (U, (tye, idx)) = inf bs u tye_idx'; 

372 
val V = Param (idx, []); 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

373 
val U_to_V = PType ("fun", [U, V]); 
32141  374 
val tye_idx'' = unif (U_to_V, T) (tye, idx + 1) 
375 
handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U; 

376 
in (V, tye_idx'') end 

377 
 inf bs (Constraint (t, U)) tye_idx = 

378 
let val (T, tye_idx') = inf bs t tye_idx in 

379 
(T, 

380 
unif (T, U) tye_idx' 

32146  381 
handle NO_UNIFIER (msg, tye) => err_constraint msg tye bs t T U) 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

382 
end; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

383 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

384 
in inf [] end; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

385 

d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

386 

22698  387 
(* infer_types *) 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

388 

27263  389 
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

390 
let 
22698  391 
(*constrain vars*) 
392 
val get_type = the_default dummyT o var_type; 

393 
val constrain_vars = Term.map_aterms 

39288  394 
(fn Free (x, T) => Type.constraint T (Free (x, get_type (x, ~1))) 
395 
 Var (xi, T) => Type.constraint T (Var (xi, get_type xi)) 

22698  396 
 t => t); 
397 

27263  398 
(*convert to preterms*) 
399 
val ts = burrow_types check_typs raw_ts; 

32141  400 
val (ts', (_, _, idx)) = 
39287  401 
fold_map (preterm_of const_type o constrain_vars) ts 
32141  402 
(Vartab.empty, Vartab.empty, 0); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

403 

27263  404 
(*do type inference*) 
32141  405 
val (tye, _) = fold (snd oo infer pp tsig) ts' (Inttab.empty, idx); 
406 
in #2 (typs_terms_of tye used maxidx ([], ts')) end; 

14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

407 

2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

408 
end; 