author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24848  5dbbd33c3236 
child 27263  a6b7f934fbc4 
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 
ID: $Id$ 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

3 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

4 

22698  5 
Simple type inference. 
2957
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 

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

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

9 
sig 
8087  10 
val anyT: sort > typ 
8611  11 
val polymorphicT: typ > typ 
24682  12 
val constrain: typ > term > term 
24504  13 
val is_param: indexname > bool 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

14 
val param: int > string * sort > typ 
22771  15 
val paramify_vars: typ > typ 
18339  16 
val paramify_dummies: typ > int > typ * int 
24764  17 
val fixate_params: Name.context > term list > term list 
22698  18 
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

19 
val infer_types: Pretty.pp > Type.tsig > (typ list > typ list) > 
24764  20 
(string > typ option) > (indexname > typ option) > Name.context > int > bool option > 
21 
(term * typ) list > (term * typ) list * (indexname * typ) list 

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

22 
end; 
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 
structure TypeInfer: TYPE_INFER = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

26 

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

27 

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

29 

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

31 

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

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

34 

24682  35 
fun constrain T t = 
22698  36 
if T = dummyT then t 
37 
else Const ("_type_constraint_", T > T) $ t; 

38 

39 

40 
(* user parameters *) 

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

41 

24504  42 
fun is_param (x, _: int) = String.isPrefix "?" x; 
22698  43 
fun param i (x, S) = TVar (("?" ^ x, i), S); 
44 

22771  45 
val paramify_vars = Term.map_atyps (fn TVar ((x, i), S) => param i (x, S)  T => T); 
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'); 

70 
in (map o map_types) (TermSubst.instantiateT inst) ts end; 

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 

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

76 
(*links to parameters may get instantiated, anything else is rigid*) 
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  
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

82 
Link of pretyp ref; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

83 

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

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

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

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

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

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

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

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

91 
Constraint of preterm * pretyp; 
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 

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

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

95 

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

96 
val mk_param = Link o ref o Param; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

97 

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

98 
fun deref (T as Link (ref (Param _))) = T 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

99 
 deref (Link (ref T)) = deref T 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

101 

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

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

105 
 fold_pretyps _ (PBound _) x = x 

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

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

108 
 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

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 

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

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

113 

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

115 

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

117 
let 
20668  118 
val params' = fold_atyps 
119 
(fn TVar (xi as (x, _), S) => 

120 
(fn ps => 

24504  121 
if is_para xi andalso not (Vartab.defined ps xi) 
20735  122 
then Vartab.update (xi, mk_param S) ps else ps) 
20668  123 
 _ => I) typ params; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

124 

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

125 
fun pre_of (TVar (v as (xi, _))) = 
20735  126 
(case Vartab.lookup params' xi of 
15531  127 
NONE => PTVar v 
128 
 SOME p => p) 

8087  129 
 pre_of (TFree ("'_dummy_", S)) = mk_param S 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

130 
 pre_of (TFree v) = PTFree v 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

131 
 pre_of (T as Type (a, Ts)) = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

132 
if T = dummyT then mk_param [] 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

133 
else PType (a, map pre_of Ts); 
20668  134 
in (pre_of typ, params') end; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

135 

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

136 

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

138 

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

140 
let 
20668  141 
fun add_vparm xi ps = 
20735  142 
if not (Vartab.defined ps xi) then 
143 
Vartab.update (xi, mk_param []) ps 

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

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

145 

20668  146 
val vparams' = fold_aterms 
147 
(fn Var (_, Type ("_polymorphic_", _)) => I 

148 
 Var (xi, _) => add_vparm xi 

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

150 
 _ => I) 

151 
tm vparams; 

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

153 

24504  154 
val preT_of = pretyp_of is_para; 
20735  155 
fun polyT_of T = fst (pretyp_of (K true) T Vartab.empty); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

156 

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

159 
else 
20668  160 
let val (T', ps') = preT_of T ps 
161 
in (Constraint (t, T'), ps') end; 

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

162 

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

164 
(case const_type c of 
22698  165 
SOME U => constraint T (PConst (c, polyT_of U)) ps 
15531  166 
 NONE => raise TYPE ("No such constant: " ^ quote c, [], [])) 
20735  167 
 pre_of (Var (xi, Type ("_polymorphic_", [T]))) ps = (PVar (xi, polyT_of T), ps) 
22698  168 
 pre_of (Var (xi, T)) ps = constraint T (PVar (xi, var_param xi)) ps 
169 
 pre_of (Free (x, T)) ps = constraint T (PFree (x, var_param (x, ~1))) ps 

20668  170 
 pre_of (Const ("_type_constraint_", Type ("fun", [T, _])) $ t) ps = 
22698  171 
pre_of t ps > constraint T 
20668  172 
 pre_of (Bound i) ps = (PBound i, ps) 
173 
 pre_of (Abs (x, T, t)) ps = 

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

174 
let 
20668  175 
val (T', ps') = preT_of T ps; 
176 
val (t', ps'') = pre_of t ps'; 

177 
in (PAbs (x, T', t'), ps'') end 

178 
 pre_of (t $ u) ps = 

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

179 
let 
20668  180 
val (t', ps') = pre_of t ps; 
181 
val (u', ps'') = pre_of u ps'; 

182 
in (PAppl (t', u'), ps'') end; 

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

183 

20668  184 
val (tm', params') = pre_of tm params; 
185 
in (tm', (vparams', params')) end; 

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

186 

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

190 

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

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

192 

16195  193 
fun add_parmsT (PType (_, Ts)) rs = fold add_parmsT Ts rs 
20854  194 
 add_parmsT (Link (r as ref (Param _))) rs = insert (op =) r rs 
16195  195 
 add_parmsT (Link (ref T)) rs = add_parmsT T rs 
196 
 add_parmsT _ rs = rs; 

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

197 

16195  198 
val add_parms = fold_pretyps add_parmsT; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

199 

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

200 

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

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

202 

20161  203 
fun add_namesT (PType (_, Ts)) = fold add_namesT Ts 
204 
 add_namesT (PTFree (x, _)) = Name.declare x 

205 
 add_namesT (PTVar ((x, _), _)) = Name.declare x 

206 
 add_namesT (Link (ref T)) = add_namesT T 

207 
 add_namesT (Param _) = I; 

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

208 

16195  209 
val add_names = fold_pretyps add_namesT; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

210 

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

211 

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

212 
(* simple_typ/term_of *) 
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 
(*deref links, fail on params*) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

215 
fun simple_typ_of (PType (a, Ts)) = Type (a, map simple_typ_of Ts) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

216 
 simple_typ_of (PTFree v) = TFree v 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

217 
 simple_typ_of (PTVar v) = TVar v 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

218 
 simple_typ_of (Link (ref T)) = simple_typ_of T 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

219 
 simple_typ_of (Param _) = sys_error "simple_typ_of: illegal Param"; 
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 
(*convert types, drop constraints*) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

222 
fun simple_term_of (PConst (c, T)) = Const (c, simple_typ_of T) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

223 
 simple_term_of (PFree (x, T)) = Free (x, simple_typ_of T) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

224 
 simple_term_of (PVar (xi, T)) = Var (xi, simple_typ_of T) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

225 
 simple_term_of (PBound i) = Bound i 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

226 
 simple_term_of (PAbs (x, T, t)) = Abs (x, simple_typ_of T, simple_term_of t) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

227 
 simple_term_of (PAppl (t, u)) = simple_term_of t $ simple_term_of u 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

228 
 simple_term_of (Constraint (t, _)) = simple_term_of t; 
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 

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

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

232 

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

233 
fun typs_terms_of used mk_var prfx (Ts, ts) = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

234 
let 
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

235 
fun elim (r as ref (Param S), x) = r := mk_var (x, S) 
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

236 
 elim _ = (); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

237 

16195  238 
val used' = fold add_names ts (fold add_namesT Ts used); 
239 
val parms = rev (fold add_parms ts (fold add_parmsT Ts [])); 

24848  240 
val names = Name.invents used' (prfx ^ Name.aT) (length parms); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

241 
in 
16195  242 
ListPair.app elim (parms, names); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

243 
(map simple_typ_of Ts, map simple_term_of ts) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

245 

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

249 

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

250 
exception NO_UNIFIER of string; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

251 

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

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

254 

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 

4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

261 
fun meet (_, []) = () 
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

262 
 meet (Link (r as (ref (Param S'))), S) = 
19465  263 
if Type.subsort tsig (S', S) then () 
264 
else r := mk_param (Type.inter_sort tsig (S', S)) 

4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

265 
 meet (Link (ref T), S) = meet (T, S) 
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

266 
 meet (PType (a, Ts), S) = 
19465  267 
ListPair.app meet (Ts, Type.arity_sorts pp tsig a S 
268 
handle ERROR msg => raise NO_UNIFIER msg) 

4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

269 
 meet (PTFree (x, S'), S) = 
19465  270 
if Type.subsort tsig (S', S) then () 
271 
else raise NO_UNIFIER (not_of_sort x S' S) 

4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

272 
 meet (PTVar (xi, S'), S) = 
19465  273 
if Type.subsort tsig (S', S) then () 
22678  274 
else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S) 
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

275 
 meet (Param _, _) = sys_error "meet"; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

276 

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

277 

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

278 
(* occurs check and assigment *) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

279 

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

280 
fun occurs_check r (Link (r' as ref T)) = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

281 
if r = r' then raise NO_UNIFIER "Occurs check!" 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

282 
else occurs_check r T 
15570  283 
 occurs_check r (PType (_, Ts)) = List.app (occurs_check r) Ts 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

284 
 occurs_check _ _ = (); 
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 
fun assign r T S = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

287 
(case deref T of 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

288 
T' as Link (r' as ref (Param _)) => 
8087  289 
if r = r' then () else (meet (T', S); r := T') 
290 
 T' => (occurs_check r T'; meet (T', S); r := T')); 

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

291 

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

292 

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

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

294 

4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

295 
fun unif (Link (r as ref (Param S)), T) = assign r T S 
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

296 
 unif (T, Link (r as ref (Param S))) = assign r T S 
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

297 
 unif (Link (ref T), U) = unif (T, U) 
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

298 
 unif (T, Link (ref U)) = unif (T, U) 
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

299 
 unif (PType (a, Ts), PType (b, Us)) = 
2979  300 
if a <> b then 
14828  301 
raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b) 
16195  302 
else ListPair.app unif (Ts, Us) 
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

303 
 unif (T, U) = if T = U then () else raise NO_UNIFIER ""; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

304 

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

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

306 

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

307 

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

308 

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

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

310 

22698  311 
(* appl_error *) 
312 

14828  313 
fun appl_error pp why t T u U = 
8087  314 
["Type error in application: " ^ why, 
315 
"", 

316 
Pretty.string_of (Pretty.block 

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

8087  319 
Pretty.string_of (Pretty.block 
14828  320 
[Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u, 
321 
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]), 

8087  322 
""]; 
323 

5635  324 

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

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

326 

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

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

330 

2979  331 
fun unif_failed msg = 
14828  332 
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n"; 
2979  333 

334 
fun prep_output bs ts Ts = 

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

335 
let 
20161  336 
val (Ts_bTs', ts') = typs_terms_of Name.context PTFree "??" (Ts @ map snd bs, ts); 
19012  337 
val (Ts', Ts'') = chop (length Ts) Ts_bTs'; 
13629  338 
val xs = map Free (map fst bs ~~ Ts''); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

339 
val ts'' = map (fn t => subst_bounds (xs, t)) ts'; 
2979  340 
in (ts'', Ts') end; 
341 

342 
fun err_loose i = 

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

3510  345 
fun err_appl msg bs t T u U = 
2979  346 
let 
3510  347 
val ([t', u'], [T', U']) = prep_output bs [t, u] [T, U]; 
348 
val why = 

349 
(case T' of 

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

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

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

355 
fun err_constraint msg bs t T U = 

356 
let 

357 
val ([t'], [T', U']) = prep_output bs [t] [T, U]; 

358 
val text = cat_lines 

359 
[unif_failed msg, 

5635  360 
"Cannot meet type constraint:", "", 
14828  361 
Pretty.string_of (Pretty.block 
362 
[Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t', 

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

364 
Pretty.string_of (Pretty.block 

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

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

368 

369 
(* main *) 

370 

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

372 

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

373 
fun inf _ (PConst (_, T)) = T 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

374 
 inf _ (PFree (_, T)) = T 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

375 
 inf _ (PVar (_, T)) = T 
15570  376 
 inf bs (PBound i) = snd (List.nth (bs, i) handle Subscript => err_loose i) 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

377 
 inf bs (PAbs (x, T, t)) = PType ("fun", [T, inf ((x, T) :: bs) t]) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

378 
 inf bs (PAppl (t, u)) = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

380 
val T = inf bs t; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

381 
val U = inf bs u; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

382 
val V = mk_param []; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

383 
val U_to_V = PType ("fun", [U, V]); 
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

384 
val _ = unif (U_to_V, T) handle NO_UNIFIER msg => err_appl msg bs t T u U; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

386 
 inf bs (Constraint (t, U)) = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

387 
let val T = inf bs t in 
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

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

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

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

391 

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

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

393 

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

394 

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

396 

24764  397 
fun infer_types pp tsig check_typs const_type var_type used maxidx freeze_mode args = 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

398 
let 
24485
687bbb686ef9
infer_types: general check_typs instead of Type.cert_typ_mode;
wenzelm
parents:
24275
diff
changeset

399 
(*check types*) 
22698  400 
val (raw_ts, raw_Ts) = split_list args; 
24485
687bbb686ef9
infer_types: general check_typs instead of Type.cert_typ_mode;
wenzelm
parents:
24275
diff
changeset

401 
val ts = burrow_types check_typs raw_ts; 
687bbb686ef9
infer_types: general check_typs instead of Type.cert_typ_mode;
wenzelm
parents:
24275
diff
changeset

402 
val Ts = check_typs raw_Ts; 
22698  403 

404 
(*constrain vars*) 

405 
val get_type = the_default dummyT o var_type; 

406 
val constrain_vars = Term.map_aterms 

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

22698  409 
 t => t); 
410 

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

411 
(*convert to preterms/typs*) 
20735  412 
val (Ts', Tps) = fold_map (pretyp_of (K true)) Ts Vartab.empty; 
22698  413 
val (ts', (vps, ps)) = 
24504  414 
fold_map (preterm_of const_type is_param o constrain_vars) ts (Vartab.empty, Tps); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

415 

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

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

417 
val tTs' = ListPair.map Constraint (ts', Ts'); 
19465  418 
val _ = List.app (fn t => (infer pp tsig t; ())) tTs'; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

419 

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

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

421 
val mk_var = 
24764  422 
if the_default false freeze_mode then PTFree 
423 
else (fn (x, S) => PTVar ((x, maxidx + 1), S)); 

424 
val prfx = if is_some freeze_mode then "" else "?"; 

425 
val (final_Ts, final_ts) = typs_terms_of used mk_var prfx (Ts', ts'); 

22771  426 

427 
(*collect result unifier*) 

428 
val redundant = fn (xi, TVar (yi, _)) => xi = yi  _ => false; 

429 
val env = filter_out redundant (map (apsnd simple_typ_of) (Vartab.dest Tps)); 

430 

431 
in (final_ts ~~ final_Ts, env) end; 

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

432 

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

433 
end; 