author  wenzelm 
Sat, 11 Jun 2005 22:15:51 +0200  
changeset 16366  6ff17d08c3d5 
parent 16195  0eb3c15298cd 
child 16668  fdb4992cf1d2 
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 

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

5 
Type inference. 
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 
11 
val logicT: typ 

8611  12 
val polymorphicT: typ > typ 
14828  13 
val appl_error: Pretty.pp > string > term > typ > term > typ > string list 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

14 
val constrain: term > typ > term 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

15 
val param: int > string * sort > typ 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

16 
val paramify_dummies: int * typ > int * typ 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

17 
val get_sort: Type.tsig > (indexname > sort option) > (sort > sort) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

18 
> (indexname * sort) list > indexname > sort 
14828  19 
val infer_types: Pretty.pp 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

20 
> Type.tsig > (string > typ option) > (indexname > typ option) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

21 
> (indexname > sort option) > (string > string) > (typ > typ) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

22 
> (sort > sort) > string list > bool > typ list > term list 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

23 
> term list * (indexname * typ) list 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

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

28 

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

29 

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

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

31 

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

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

33 
Flavours of term encodings: 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

34 

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

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

36 
A very complicated structure produced by the syntax module's 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

37 
read functions. Encodes types and sorts as terms; may contain 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

38 
explicit constraints and partial typing information (where 
8087  39 
dummies serve as wildcards). 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

40 

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

41 
Parse trees are INTERNAL! Users should never encounter them, 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

42 
except in parse / print translation functions. 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

43 

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

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

45 
Provide the user interface to type inferences. They may contain 
8087  46 
partial type information (dummies are wildcards) or explicit 
47 
type constraints (introduced via constrain: term > typ > 

48 
term). 

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

49 

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

50 
The type inference function also lets users specify a certain 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

51 
subset of TVars to be treated as nonrigid inference parameters. 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

52 

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

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

54 
The internal representation for type inference. 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

55 

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

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

57 
Fully typed lambda terms to be accepted by appropriate 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

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

60 

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

61 

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

62 

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

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

64 

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

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

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

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

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

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

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

71 
Link of pretyp ref; 
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 
datatype preterm = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

84 

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

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

86 

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

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

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

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

90 

16195  91 
fun fold_pretyps f (PConst (_, T)) x = f T x 
92 
 fold_pretyps f (PFree (_, T)) x = f T x 

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

94 
 fold_pretyps _ (PBound _) x = x 

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

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

97 
 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

98 

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

99 

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

100 

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

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

102 

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

103 
(* pretyp(s)_of *) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

104 

8087  105 
fun anyT S = TFree ("'_dummy_", S); 
14854  106 
val logicT = anyT []; 
8087  107 

8611  108 
(*indicate polymorphic Vars*) 
109 
fun polymorphicT T = Type ("_polymorphic_", [T]); 

110 

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

111 
fun pretyp_of is_param (params, typ) = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

112 
let 
16195  113 
fun add_parms (TVar (xi as (x, _), S)) ps = 
114 
if is_param xi andalso is_none (assoc_string_int (ps, xi)) 

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

115 
then (xi, mk_param S) :: ps else ps 
16195  116 
 add_parms (TFree _) ps = ps 
117 
 add_parms (Type (_, Ts)) ps = fold add_parms Ts ps; 

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

118 

16195  119 
val params' = add_parms typ params; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

120 

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

121 
fun pre_of (TVar (v as (xi, _))) = 
16195  122 
(case assoc_string_int (params', xi) of 
15531  123 
NONE => PTVar v 
124 
 SOME p => p) 

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

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

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

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

129 
else PType (a, map pre_of Ts); 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

130 
in (params', pre_of typ) end; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

131 

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

132 
fun pretyps_of is_param = foldl_map (pretyp_of is_param); 
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 

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

135 
(* preterm(s)_of *) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

136 

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

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

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

139 
fun add_vparm (ps, xi) = 
16195  140 
if is_none (assoc_string_int (ps, xi)) then 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

141 
(xi, mk_param []) :: ps 
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 

8611  144 
fun add_vparms (ps, Var (xi, Type ("_polymorphic_", _))) = ps 
145 
 add_vparms (ps, Var (xi, _)) = add_vparm (ps, xi) 

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

146 
 add_vparms (ps, Free (x, _)) = add_vparm (ps, (x, ~1)) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

147 
 add_vparms (ps, Abs (_, _, t)) = add_vparms (ps, t) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

148 
 add_vparms (ps, t $ u) = add_vparms (add_vparms (ps, t), u) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

150 

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

151 
val vparams' = add_vparms (vparams, tm); 
16195  152 
fun var_param xi = the (assoc_string_int (vparams', xi)); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

153 

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

154 

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

155 
val preT_of = pretyp_of is_param; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

156 

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

157 
fun constrain (ps, t) T = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

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

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

162 

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

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

164 
(case const_type c of 
15531  165 
SOME U => constrain (ps, PConst (c, snd (pretyp_of (K true) ([], U)))) T 
166 
 NONE => raise TYPE ("No such constant: " ^ quote c, [], [])) 

8611  167 
 pre_of (ps, Var (xi, Type ("_polymorphic_", [T]))) = 
168 
(ps, PVar (xi, snd (pretyp_of (K true) ([], T)))) 

169 
 pre_of (ps, Var (xi, T)) = constrain (ps, PVar (xi, var_param xi)) T 

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

170 
 pre_of (ps, Free (x, T)) = constrain (ps, PFree (x, var_param (x, ~1))) T 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

171 
 pre_of (ps, Const ("_type_constraint_", T) $ t) = constrain (pre_of (ps, t)) T 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

173 
 pre_of (ps, Abs (x, T, t)) = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

175 
val (ps', T') = preT_of (ps, T); 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

176 
val (ps'', t') = pre_of (ps', t); 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

177 
in (ps'', PAbs (x, T', t')) end 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

178 
 pre_of (ps, t $ u) = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

180 
val (ps', t') = pre_of (ps, t); 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

181 
val (ps'', u') = pre_of (ps', u); 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

182 
in (ps'', PAppl (t', u')) end; 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

183 

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

184 
val (params', tm') = pre_of (params, tm); 
8611  185 
in ((vparams', params'), tm') end; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

186 

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

187 
fun preterms_of const_type is_param = foldl_map (preterm_of const_type is_param); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

188 

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

189 

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

190 

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

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

192 

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

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

194 

16195  195 
fun add_parmsT (PType (_, Ts)) rs = fold add_parmsT Ts rs 
196 
 add_parmsT (Link (r as ref (Param _))) rs = r ins rs 

197 
 add_parmsT (Link (ref T)) rs = add_parmsT T rs 

198 
 add_parmsT _ rs = rs; 

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

199 

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

201 

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

202 

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

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

204 

16195  205 
fun add_namesT (PType (_, Ts)) xs = fold add_namesT Ts xs 
206 
 add_namesT (PTFree (x, _)) xs = x ins_string xs 

207 
 add_namesT (PTVar ((x, _), _)) xs = x ins_string xs 

208 
 add_namesT (Link (ref T)) xs = add_namesT T xs 

209 
 add_namesT (Param _) xs = xs; 

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

210 

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

212 

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

215 

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

216 
(*deref links, fail on params*) 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

217 
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

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

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

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

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

222 

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

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

224 
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

225 
 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

226 
 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

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

228 
 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

229 
 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

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

231 

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

234 

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

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

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

237 
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

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

239 

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

14695  242 
val names = Term.invent_names used' (prfx ^ "'a") (length parms); 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

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

246 
end; 
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 

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

251 

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

252 
exception NO_UNIFIER of string; 
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 

14828  255 
fun unify pp classes arities = 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

257 

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

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

259 

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

260 
fun not_in_sort x S' S = 
14828  261 
"Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^ 
262 
Pretty.string_of_sort pp S; 

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

263 

14828  264 
fun no_domain (a, c) = "No way to get " ^ Pretty.string_of_arity pp (a, [], [c]); 
7639  265 

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

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

267 
 meet (Link (r as (ref (Param S'))), S) = 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

268 
if Sorts.sort_le classes (S', S) then () 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

269 
else r := mk_param (Sorts.inter_sort classes (S', S)) 
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

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

271 
 meet (PType (a, Ts), S) = 
16195  272 
ListPair.app meet (Ts, Sorts.mg_domain (classes, arities) a S 
7639  273 
handle Sorts.DOMAIN ac => raise NO_UNIFIER (no_domain ac)) 
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

274 
 meet (PTFree (x, S'), S) = 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

275 
if Sorts.sort_le classes (S', S) then () 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

276 
else raise NO_UNIFIER (not_in_sort x S' S) 
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

277 
 meet (PTVar (xi, S'), S) = 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

278 
if Sorts.sort_le classes (S', S) then () 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

279 
else raise NO_UNIFIER (not_in_sort (Syntax.string_of_vname xi) S' S) 
4957
30c49821e61f
remove seq2, scan (use seq2, foldl_map from library.ML);
wenzelm
parents:
3784
diff
changeset

280 
 meet (Param _, _) = sys_error "meet"; 
2957
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 

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

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

284 

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

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

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

287 
else occurs_check r T 
15570  288 
 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

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

290 

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

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

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

293 
T' as Link (r' as ref (Param _)) => 
8087  294 
if r = r' then () else (meet (T', S); r := T') 
295 
 T' => (occurs_check r T'; meet (T', S); r := T')); 

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

296 

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

297 

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

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

299 

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

300 
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

301 
 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

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

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

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

308 
 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

309 

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

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

311 

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

312 

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

313 

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

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

315 

14828  316 
fun appl_error pp why t T u U = 
8087  317 
["Type error in application: " ^ why, 
318 
"", 

319 
Pretty.string_of (Pretty.block 

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

8087  322 
Pretty.string_of (Pretty.block 
14828  323 
[Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u, 
324 
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]), 

8087  325 
""]; 
326 

5635  327 

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

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

329 

14828  330 
fun infer pp classes arities = 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

333 

2979  334 
fun unif_failed msg = 
14828  335 
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n"; 
2979  336 

337 
fun prep_output bs ts Ts = 

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

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

339 
val (Ts_bTs', ts') = typs_terms_of [] PTFree "??" (Ts @ map snd bs, ts); 
13629  340 
val (Ts',Ts'') = Library.splitAt(length Ts, Ts_bTs'); 
341 
val xs = map Free (map fst bs ~~ Ts''); 

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

342 
val ts'' = map (fn t => subst_bounds (xs, t)) ts'; 
2979  343 
in (ts'', Ts') end; 
344 

345 
fun err_loose i = 

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

3510  348 
fun err_appl msg bs t T u U = 
2979  349 
let 
3510  350 
val ([t', u'], [T', U']) = prep_output bs [t, u] [T, U]; 
351 
val why = 

352 
(case T' of 

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

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

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

358 
fun err_constraint msg bs t T U = 

359 
let 

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

361 
val text = cat_lines 

362 
[unif_failed msg, 

5635  363 
"Cannot meet type constraint:", "", 
14828  364 
Pretty.string_of (Pretty.block 
365 
[Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t', 

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

367 
Pretty.string_of (Pretty.block 

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

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

371 

372 
(* main *) 

373 

14828  374 
val unif = unify pp classes arities; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

375 

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

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

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

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

380 
 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

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

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

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

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

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

386 
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

387 
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

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

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

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

391 
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

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

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

394 

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

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

396 

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

397 

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

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

399 

14828  400 
fun basic_infer_types pp const_type classes arities used freeze is_param ts Ts = 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

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

403 
val (Tps, Ts') = pretyps_of (K true) ([], Ts); 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

404 
val ((vps, ps), ts') = preterms_of const_type is_param (([], Tps), ts); 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

405 

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

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

407 
val tTs' = ListPair.map Constraint (ts', Ts'); 
15570  408 
val _ = List.app (fn t => (infer pp classes arities t; ())) tTs'; 
2957
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 
(*collect result unifier*) 
15531  411 
fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); NONE) 
412 
 ch_var xi_T = SOME xi_T; 

15570  413 
val env = List.mapPartial ch_var Tps; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

414 

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

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

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

417 
if freeze then PTFree 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

418 
else (fn (x, S) => PTVar ((x, 0), S)); 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

419 
val (final_Ts, final_ts) = typs_terms_of used mk_var "" (Ts', ts'); 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

420 
val final_env = map (apsnd simple_typ_of) env; 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

421 
in (final_ts, final_Ts, final_env) end; 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

422 

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

423 

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

424 

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

425 
(** type inference **) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

426 

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

427 
(* user constraints *) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

428 

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

429 
fun constrain t T = 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

430 
if T = dummyT then t 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

431 
else Const ("_type_constraint_", T) $ t; 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

432 

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

433 

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

434 
(* user parameters *) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

435 

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

436 
fun is_param (x, _) = size x > 0 andalso ord x = ord "?"; 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

437 
fun param i (x, S) = TVar (("?" ^ x, i), S); 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

438 

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

439 
fun paramify_dummies (maxidx, TFree ("'_dummy_", S)) = 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

440 
(maxidx + 1, param (maxidx + 1) ("'dummy", S)) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

441 
 paramify_dummies (maxidx, Type (a, Ts)) = 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

442 
let val (maxidx', Ts') = foldl_map paramify_dummies (maxidx, Ts) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

443 
in (maxidx', Type (a, Ts')) end 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

444 
 paramify_dummies arg = arg; 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

445 

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

446 

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

447 
(* decode sort constraints *) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

448 

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

449 
fun get_sort tsig def_sort map_sort raw_env = 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

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

451 
fun eq ((xi, S), (xi', S')) = 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

452 
xi = xi' andalso Type.eq_sort tsig (S, S'); 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

453 

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

454 
val env = gen_distinct eq (map (apsnd map_sort) raw_env); 
14828  455 
val _ = (case gen_duplicates eq_fst env of [] => () 
456 
 dups => error ("Inconsistent sort constraints for type variable(s) " 

457 
^ commas_quote (map (Syntax.string_of_vname' o fst) dups))); 

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

458 

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

459 
fun get xi = 
16195  460 
(case (assoc_string_int (env, xi), def_sort xi) of 
15531  461 
(NONE, NONE) => Type.defaultS tsig 
462 
 (NONE, SOME S) => S 

463 
 (SOME S, NONE) => S 

464 
 (SOME S, SOME S') => 

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

465 
if Type.eq_sort tsig (S, S') then S' 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

466 
else error ("Sort constraint inconsistent with default for type variable " ^ 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

467 
quote (Syntax.string_of_vname' xi))); 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

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

469 

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

470 

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

471 
(* decode_types  transform parse tree into raw term *) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

472 

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

473 
fun decode_types tsig is_const def_type def_sort map_const map_type map_sort tm = 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

474 
let 
16195  475 
fun get_type xi = if_none (def_type xi) dummyT; 
476 
fun is_free x = is_some (def_type (x, ~1)); 

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

477 
val raw_env = Syntax.raw_term_sorts tm; 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

478 
val sort_of = get_sort tsig def_sort map_sort raw_env; 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

479 

14993  480 
val certT = Type.cert_typ tsig o map_type; 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

481 
fun decodeT t = certT (Syntax.typ_of_term sort_of map_sort t); 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

482 

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

483 
fun decode (Const ("_constrain", _) $ t $ typ) = 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

484 
constrain (decode t) (decodeT typ) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

485 
 decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) = 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

486 
if T = dummyT then Abs (x, decodeT typ, decode t) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

487 
else constrain (Abs (x, certT T, decode t)) (decodeT typ > dummyT) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

488 
 decode (Abs (x, T, t)) = Abs (x, certT T, decode t) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

489 
 decode (t $ u) = decode t $ decode u 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

490 
 decode (Free (x, T)) = 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

491 
let val c = map_const x in 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

492 
if not (is_free x) andalso (is_const c orelse NameSpace.is_qualified c) then 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

493 
Const (c, certT T) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

494 
else if T = dummyT then Free (x, get_type (x, ~1)) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

495 
else constrain (Free (x, certT T)) (get_type (x, ~1)) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

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

497 
 decode (Var (xi, T)) = 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

498 
if T = dummyT then Var (xi, get_type xi) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

499 
else constrain (Var (xi, certT T)) (get_type xi) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

500 
 decode (t as Bound _) = t 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

501 
 decode (Const (c, T)) = Const (map_const c, certT T); 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

502 
in decode tm end; 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

503 

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

504 

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

505 
(* infer_types *) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

506 

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

507 
(*Given [T1,...,Tn] and [t1,...,tn], ensure that the type of ti 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

508 
unifies with Ti (for i=1,...,n). 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

509 

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

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

511 
const_type: name mapping and signature lookup 
16195  512 
def_type: partial map from indexnames to types (constrains Frees and Vars) 
513 
def_sort: partial map from indexnames to sorts (constrains TFrees and TVars) 

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

514 
used: list of already used type variables 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

515 
freeze: if true then generated parameters are turned into TFrees, else TVars*) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

516 

14828  517 
fun infer_types pp tsig const_type def_type def_sort 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

518 
map_const map_type map_sort used freeze pat_Ts raw_ts = 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

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

520 
val {classes, arities, ...} = Type.rep_tsig tsig; 
14993  521 
val pat_Ts' = map (Type.cert_typ tsig) pat_Ts; 
16195  522 
val is_const = is_some o const_type; 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

523 
val raw_ts' = 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

524 
map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts; 
14828  525 
val (ts, Ts, unifier) = basic_infer_types pp const_type 
16366  526 
(#2 classes) arities used freeze is_param raw_ts' pat_Ts'; 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

527 
in (ts, unifier) end; 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

528 

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

529 
end; 