author  berghofe 
Tue, 01 Jun 2010 11:30:57 +0200  
changeset 37236  739d8b9c59da 
parent 37145  01aa36932739 
parent 37235  cafcc42bae77 
child 39286  1f8131a7bcb9 
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 
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 

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 

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 

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

42 
val paramify_vars = 
32146  43 
Same.commit 
44 
(Term_Subst.map_atypsT_same 

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

22771  46 

22698  47 
val paramify_dummies = 
48 
let 

49 
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

50 

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

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

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

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

56 
 paramify T maxidx = (T, maxidx); 

57 
in paramify end; 

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

58 

24764  59 
fun fixate_params name_context ts = 
60 
let 

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

62 
if is_param xi then 

63 
let 

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

67 
else (inst, used); 

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

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

31977  70 
in (map o map_types) (Term_Subst.instantiateT inst) ts end; 
24764  71 

2957
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 

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

74 
(** pretyps and preterms **) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

75 

32141  76 
(*parameters may get instantiated, anything else is rigid*) 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

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

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

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

82 

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

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

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

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

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

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

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

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

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

91 

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

94 

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

97 
NONE => T 

98 
 SOME U => deref tye U) 

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

100 

16195  101 
fun fold_pretyps f (PConst (_, T)) x = f T x 
102 
 fold_pretyps f (PFree (_, T)) x = f T x 

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

104 
 fold_pretyps _ (PBound _) x = x 

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

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

107 
 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

108 

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

109 

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

110 

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

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

112 

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

114 

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

116 
let 
32141  117 
val (params', idx) = fold_atyps 
20668  118 
(fn TVar (xi as (x, _), S) => 
32141  119 
(fn ps_idx as (ps, idx) => 
24504  120 
if is_para xi andalso not (Vartab.defined ps xi) 
32141  121 
then (Vartab.update (xi, Param (idx, S)) ps, idx + 1) else ps_idx) 
122 
 _ => I) typ params_idx; 

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

123 

32141  124 
fun pre_of (TVar (v as (xi, _))) idx = 
20735  125 
(case Vartab.lookup params' xi of 
15531  126 
NONE => PTVar v 
32141  127 
 SOME p => p, idx) 
128 
 pre_of (TFree ("'_dummy_", S)) idx = (Param (idx, S), idx + 1) 

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

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

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

132 
else 

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

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

135 

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

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

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

138 

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

139 

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

141 

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

143 
let 
32141  144 
fun add_vparm xi (ps_idx as (ps, idx)) = 
20735  145 
if not (Vartab.defined ps xi) then 
32141  146 
(Vartab.update (xi, Param (idx, [])) ps, idx + 1) 
147 
else ps_idx; 

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

148 

32141  149 
val (vparams', idx') = fold_aterms 
20668  150 
(fn Var (_, Type ("_polymorphic_", _)) => I 
151 
 Var (xi, _) => add_vparm xi 

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

153 
 _ => I) 

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

156 

24504  157 
val preT_of = pretyp_of is_para; 
32141  158 
fun polyT_of T idx = apsnd snd (pretyp_of (K true) T (Vartab.empty, idx)); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

159 

22698  160 
fun constraint T t ps = 
20668  161 
if T = dummyT then (t, ps) 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

162 
else 
20668  163 
let val (T', ps') = preT_of T ps 
164 
in (Constraint (t, T'), ps') end; 

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

165 

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

167 
(case const_type c of 
32141  168 
SOME U => 
169 
let val (pU, idx') = polyT_of U idx 

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

15531  171 
 NONE => raise TYPE ("No such constant: " ^ quote c, [], [])) 
32141  172 
 pre_of (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) = 
173 
let val (pT, idx') = polyT_of T idx 

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

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

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

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

178 
pre_of t ps_idx > constraint T 

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

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

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

181 
let 
32141  182 
val (T', ps_idx') = preT_of T ps_idx; 
183 
val (t', ps_idx'') = pre_of t ps_idx'; 

184 
in (PAbs (x, T', t'), ps_idx'') end 

185 
 pre_of (t $ u) ps_idx = 

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

186 
let 
32141  187 
val (t', ps_idx') = pre_of t ps_idx; 
188 
val (u', ps_idx'') = pre_of u ps_idx'; 

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

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

190 

32141  191 
val (tm', (params', idx'')) = pre_of tm (params, idx'); 
192 
in (tm', (vparams', params', idx'')) end; 

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

193 

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

194 

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

195 

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

196 
(** pretyps/terms to typs/terms **) 
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_parms *) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

199 

32146  200 
fun add_parmsT tye T = 
201 
(case deref tye T of 

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

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

205 

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

210 

32146  211 
fun add_namesT tye T = 
212 
(case deref tye T of 

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

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

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

217 

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

219 

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

220 

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

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

222 

32146  223 
fun simple_typ_of tye f T = 
224 
(case deref tye T of 

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

227 
 PTVar v => TVar v 

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

229 

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

230 
(*convert types, drop constraints*) 
32141  231 
fun simple_term_of tye f (PConst (c, T)) = Const (c, simple_typ_of tye f T) 
232 
 simple_term_of tye f (PFree (x, T)) = Free (x, simple_typ_of tye f T) 

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

234 
 simple_term_of tye f (PBound i) = Bound i 

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

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

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

238 
simple_term_of tye f t $ simple_term_of tye f u 

239 
 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

240 

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

241 

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

243 

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

245 
let 
32141  246 
val used' = fold (add_names tye) ts (fold (add_namesT tye) Ts used); 
247 
val parms = rev (fold (add_parms tye) ts (fold (add_parmsT tye) Ts [])); 

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

251 
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

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 

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

256 

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

258 

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

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

261 

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

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

263 

19465  264 
fun not_of_sort x S' S = 
14828  265 
"Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^ 
266 
Pretty.string_of_sort pp S; 

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

267 

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

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

271 
else (Inttab.update_new (i, 

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

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

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

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

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

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

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

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

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

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

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

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

284 
 meets _ tye_idx = tye_idx; 

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

285 

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

286 

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

288 

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

32146  291 
else 
292 
(case Inttab.lookup tye i' of 

32141  293 
NONE => () 
294 
 SOME T => occurs_check tye i T) 

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

296 
 occurs_check _ _ _ = (); 

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

297 

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

298 
fun assign i (T as Param (i', _)) S tye_idx = 
32141  299 
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

300 
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

301 
 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

302 
(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

303 

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

304 

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

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

306 

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

32141  309 
(Param (i, S), T) => assign i T S tye_idx 
310 
 (T, Param (i, S)) => assign i T S tye_idx 

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

2979  312 
if a <> b then 
32141  313 
raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b, tye) 
314 
else fold unif (Ts ~~ Us) tye_idx 

32146  315 
 (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

316 

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

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

318 

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

319 

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

320 

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

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

322 

22698  323 
(* appl_error *) 
324 

14828  325 
fun appl_error pp why t T u U = 
8087  326 
["Type error in application: " ^ why, 
327 
"", 

328 
Pretty.string_of (Pretty.block 

14828  329 
[Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t, 
330 
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]), 

8087  331 
Pretty.string_of (Pretty.block 
14828  332 
[Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u, 
333 
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]), 

8087  334 
""]; 
335 

5635  336 

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

338 

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

340 
let 
2979  341 
(* errors *) 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

342 

2979  343 
fun unif_failed msg = 
14828  344 
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n"; 
2979  345 

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

347 
let 
32141  348 
val (Ts_bTs', ts') = typs_terms_of tye Name.context ~1 (Ts @ map snd bs, ts); 
19012  349 
val (Ts', Ts'') = chop (length Ts) Ts_bTs'; 
27263  350 
fun prep t = 
351 
let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) 

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

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

2979  354 

355 
fun err_loose i = 

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

32141  358 
fun err_appl msg tye bs t T u U = 
2979  359 
let 
32141  360 
val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]; 
3510  361 
val why = 
362 
(case T' of 

14828  363 
Type ("fun", _) => "Incompatible operand type" 
364 
 _ => "Operator not of function type"); 

365 
val text = unif_failed msg ^ cat_lines (appl_error pp why t' T' u' U'); 

3784  366 
in raise TYPE (text, [T', U'], [t', u']) end; 
2979  367 

32141  368 
fun err_constraint msg tye bs t T U = 
2979  369 
let 
32141  370 
val ([t'], [T', U']) = prep_output tye bs [t] [T, U]; 
2979  371 
val text = cat_lines 
372 
[unif_failed msg, 

5635  373 
"Cannot meet type constraint:", "", 
14828  374 
Pretty.string_of (Pretty.block 
375 
[Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t', 

376 
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T']), 

377 
Pretty.string_of (Pretty.block 

378 
[Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp U']), ""]; 

3784  379 
in raise TYPE (text, [T', U'], [t']) end; 
2979  380 

381 

382 
(* main *) 

383 

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

385 

32141  386 
fun inf _ (PConst (_, T)) tye_idx = (T, tye_idx) 
387 
 inf _ (PFree (_, T)) tye_idx = (T, tye_idx) 

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

389 
 inf bs (PBound i) tye_idx = 

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

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

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

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

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

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

395 
let 
32141  396 
val (T, tye_idx') = inf bs t tye_idx; 
397 
val (U, (tye, idx)) = inf bs u tye_idx'; 

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

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

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

402 
in (V, tye_idx'') end 

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

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

405 
(T, 

406 
unif (T, U) tye_idx' 

32146  407 
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

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

409 

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

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

411 

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

412 

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

414 

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

416 
let 
22698  417 
(*constrain vars*) 
418 
val get_type = the_default dummyT o var_type; 

419 
val constrain_vars = Term.map_aterms 

24682  420 
(fn Free (x, T) => constrain T (Free (x, get_type (x, ~1))) 
421 
 Var (xi, T) => constrain T (Var (xi, get_type xi)) 

22698  422 
 t => t); 
423 

27263  424 
(*convert to preterms*) 
425 
val ts = burrow_types check_typs raw_ts; 

32141  426 
val (ts', (_, _, idx)) = 
427 
fold_map (preterm_of const_type is_param o constrain_vars) ts 

428 
(Vartab.empty, Vartab.empty, 0); 

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

429 

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

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

433 

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

434 
end; 