author  wenzelm 
Wed, 18 Jun 2008 22:32:02 +0200  
changeset 27263  a6b7f934fbc4 
parent 24848  5dbbd33c3236 
child 29606  fedb8be05f24 
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) > 
27263  20 
(string > typ option) > (indexname > typ option) > Name.context > int > 
21 
term list > term 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 

27263  35 
val constrain = Syntax.type_constraint; 
22698  36 

37 

38 
(* user parameters *) 

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

39 

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

22771  43 
val paramify_vars = Term.map_atyps (fn TVar ((x, i), S) => param i (x, S)  T => T); 
44 

22698  45 
val paramify_dummies = 
46 
let 

47 
fun dummy S maxidx = (param (maxidx + 1) ("'dummy", S), maxidx + 1); 

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

48 

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

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

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

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

54 
 paramify T maxidx = (T, maxidx); 

55 
in paramify end; 

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

56 

24764  57 
fun fixate_params name_context ts = 
58 
let 

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

60 
if is_param xi then 

61 
let 

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

65 
else (inst, used); 

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

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

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

69 

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

70 

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

71 

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

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

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

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

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

78 
PTVar of indexname * sort  
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

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

81 

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

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

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

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

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

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

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

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

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

90 

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

91 

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

92 
(* utils *) 
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 
val mk_param = Link o ref o Param; 
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 
fun deref (T as Link (ref (Param _))) = T 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

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

99 

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

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

103 
 fold_pretyps _ (PBound _) x = x 

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

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

106 
 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

107 

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

111 

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

113 

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

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

118 
(fn ps => 

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

122 

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

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

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

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

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

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

131 
else PType (a, map pre_of Ts); 
20668  132 
in (pre_of typ, params') 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 

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

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

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

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

143 

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

146 
 Var (xi, _) => add_vparm xi 

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

148 
 _ => I) 

149 
tm vparams; 

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 

24504  152 
val preT_of = pretyp_of is_para; 
20735  153 
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

154 

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

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

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

160 

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

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

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

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

172 
let 
20668  173 
val (T', ps') = preT_of T ps; 
174 
val (t', ps'') = pre_of t ps'; 

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

176 
 pre_of (t $ u) ps = 

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

177 
let 
20668  178 
val (t', ps') = pre_of t ps; 
179 
val (u', ps'') = pre_of u ps'; 

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

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

181 

20668  182 
val (tm', params') = pre_of tm params; 
183 
in (tm', (vparams', params')) end; 

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

184 

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

185 

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

190 

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

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

195 

16195  196 
val add_parms = fold_pretyps add_parmsT; 
2957
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 

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

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

200 

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

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

204 
 add_namesT (Link (ref T)) = add_namesT T 

205 
 add_namesT (Param _) = I; 

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

206 

16195  207 
val add_names = fold_pretyps add_namesT; 
2957
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 

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

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

213 
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

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

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

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

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

218 

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

219 
(*convert types, drop constraints*) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

220 
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

221 
 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

222 
 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

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

224 
 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

225 
 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

226 
 simple_term_of (Constraint (t, _)) = simple_term_of t; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

227 

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

228 

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

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

230 

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

232 
let 
27263  233 
fun elim (r as ref (Param S), x) = r := PTVar ((x, maxidx + 1), S) 
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

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

235 

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

27263  238 
val names = Name.invents used' ("?" ^ Name.aT) (length parms); 
239 
val _ = ListPair.app elim (parms, names); 

240 
in (map simple_typ_of Ts, map simple_term_of ts) end; 

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

241 

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

242 

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

243 

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

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

247 

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

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

250 

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

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

252 

19465  253 
fun not_of_sort x S' S = 
14828  254 
"Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^ 
255 
Pretty.string_of_sort pp S; 

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

256 

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

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

258 
 meet (Link (r as (ref (Param S'))), S) = 
19465  259 
if Type.subsort tsig (S', S) then () 
260 
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

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

262 
 meet (PType (a, Ts), S) = 
19465  263 
ListPair.app meet (Ts, Type.arity_sorts pp tsig a S 
264 
handle ERROR msg => raise NO_UNIFIER msg) 

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

265 
 meet (PTFree (x, S'), S) = 
19465  266 
if Type.subsort tsig (S', S) then () 
267 
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

268 
 meet (PTVar (xi, S'), S) = 
19465  269 
if Type.subsort tsig (S', S) then () 
22678  270 
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

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

272 

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

273 

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

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

275 

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

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

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

278 
else occurs_check r T 
15570  279 
 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

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

281 

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

282 
fun assign r T S = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

284 
T' as Link (r' as ref (Param _)) => 
8087  285 
if r = r' then () else (meet (T', S); r := T') 
286 
 T' => (occurs_check r T'; meet (T', S); r := T')); 

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

287 

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

288 

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

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

290 

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

291 
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

292 
 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

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

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

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

299 
 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

300 

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

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

302 

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

306 

22698  307 
(* appl_error *) 
308 

14828  309 
fun appl_error pp why t T u U = 
8087  310 
["Type error in application: " ^ why, 
311 
"", 

312 
Pretty.string_of (Pretty.block 

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

8087  315 
Pretty.string_of (Pretty.block 
14828  316 
[Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u, 
317 
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]), 

8087  318 
""]; 
319 

5635  320 

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

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

322 

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

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

326 

2979  327 
fun unif_failed msg = 
14828  328 
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n"; 
2979  329 

330 
fun prep_output bs ts Ts = 

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

331 
let 
27263  332 
val (Ts_bTs', ts') = typs_terms_of Name.context ~1 (Ts @ map snd bs, ts); 
19012  333 
val (Ts', Ts'') = chop (length Ts) Ts_bTs'; 
27263  334 
fun prep t = 
335 
let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) 

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

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

2979  338 

339 
fun err_loose i = 

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

3510  342 
fun err_appl msg bs t T u U = 
2979  343 
let 
3510  344 
val ([t', u'], [T', U']) = prep_output bs [t, u] [T, U]; 
345 
val why = 

346 
(case T' of 

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

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

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

352 
fun err_constraint msg bs t T U = 

353 
let 

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

355 
val text = cat_lines 

356 
[unif_failed msg, 

5635  357 
"Cannot meet type constraint:", "", 
14828  358 
Pretty.string_of (Pretty.block 
359 
[Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t', 

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

361 
Pretty.string_of (Pretty.block 

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

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

365 

366 
(* main *) 

367 

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

369 

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

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

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

372 
 inf _ (PVar (_, T)) = T 
15570  373 
 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

374 
 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

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

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

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

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

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

380 
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

381 
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

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

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

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

385 
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

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

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

388 

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

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

390 

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

391 

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

393 

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

395 
let 
22698  396 
(*constrain vars*) 
397 
val get_type = the_default dummyT o var_type; 

398 
val constrain_vars = Term.map_aterms 

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

22698  401 
 t => t); 
402 

27263  403 
(*convert to preterms*) 
404 
val ts = burrow_types check_typs raw_ts; 

22698  405 
val (ts', (vps, ps)) = 
27263  406 
fold_map (preterm_of const_type is_param o constrain_vars) ts (Vartab.empty, Vartab.empty); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

407 

27263  408 
(*do type inference*) 
409 
val _ = List.app (ignore o infer pp tsig) ts'; 

410 
in #2 (typs_terms_of used maxidx ([], ts')) end; 

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

411 

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

412 
end; 