author  wenzelm 
Wed, 19 Jul 2006 12:12:04 +0200  
changeset 20161  b8b1d4a380aa 
parent 20076  def4ad161528 
child 20668  00521d5e1838 
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 

18339  12 
val mixfixT: Syntax.mixfix > typ 
8611  13 
val polymorphicT: typ > typ 
14828  14 
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

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

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

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

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

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

22 
> (indexname > sort option) > (string > string) > (typ > typ) 
20161  23 
> (sort > sort) > Name.context > bool > typ list > term list 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

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

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

28 
struct 
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 

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

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

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

35 

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

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

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

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

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

41 

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

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

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

44 

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

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

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

49 
term). 

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

50 

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

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

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

53 

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

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

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

56 

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

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

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

59 
certification functions. 
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 

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

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

65 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

85 

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

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

87 

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

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

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

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

91 

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

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

95 
 fold_pretyps _ (PBound _) x = x 

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

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

98 
 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

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 

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

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

103 

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

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

105 

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

18339  109 
fun mixfixT (Binder _) = (logicT > logicT) > logicT 
110 
 mixfixT mx = replicate (Syntax.mixfix_args mx) logicT > logicT; 

111 

112 

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

115 

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

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

117 
let 
16195  118 
fun add_parms (TVar (xi as (x, _), S)) ps = 
17282  119 
if is_param xi andalso not (AList.defined (op =) ps xi) 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

120 
then (xi, mk_param S) :: ps else ps 
16195  121 
 add_parms (TFree _) ps = ps 
122 
 add_parms (Type (_, Ts)) ps = fold add_parms Ts ps; 

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

123 

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

125 

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

126 
fun pre_of (TVar (v as (xi, _))) = 
17271  127 
(case AList.lookup (op =) params' xi of 
15531  128 
NONE => PTVar v 
129 
 SOME p => p) 

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

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

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

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

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

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

136 

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

137 
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

138 

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

139 

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

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

141 

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

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

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

144 
fun add_vparm (ps, xi) = 
17282  145 
if not (AList.defined (op =) ps xi) then 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

146 
(xi, mk_param []) :: ps 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

148 

8611  149 
fun add_vparms (ps, Var (xi, Type ("_polymorphic_", _))) = ps 
150 
 add_vparms (ps, Var (xi, _)) = add_vparm (ps, xi) 

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

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

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

153 
 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

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

155 

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

156 
val vparams' = add_vparms (vparams, tm); 
17271  157 
fun var_param xi = (the o AList.lookup (op =) vparams') xi; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

158 

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

159 

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

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

161 

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

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

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

164 
else 
8087  165 
let val (ps', T') = preT_of (ps, T) 
166 
in (ps', Constraint (t, T')) end; 

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

167 

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

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

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

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

174 
 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

175 
 pre_of (ps, Free (x, T)) = constrain (ps, PFree (x, var_param (x, ~1))) T 
19577  176 
 pre_of (ps, Const ("_type_constraint_", Type ("fun", [T, _])) $ t) = 
177 
constrain (pre_of (ps, t)) T 

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

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

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

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

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

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

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

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

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

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

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

188 
in (ps'', PAppl (t', u')) end; 
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 
val (params', tm') = pre_of (params, tm); 
8611  191 
in ((vparams', params'), tm') end; 
2957
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

192 

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

193 
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

194 

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

195 

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

196 

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

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

200 

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

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

204 
 add_parmsT _ rs = rs; 

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

205 

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

207 

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

208 

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

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

210 

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

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

214 
 add_namesT (Link (ref T)) = add_namesT T 

215 
 add_namesT (Param _) = I; 

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

216 

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

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

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

221 

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

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

223 
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

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

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

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

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

230 
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

231 
 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

232 
 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

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

234 
 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

235 
 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

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

237 

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

238 

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

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

240 

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

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

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

243 
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

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

245 

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

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

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

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

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

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

255 

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

256 
(** ordersorted unification of types **) (*DESTRUCTIVE*) 
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 
exception NO_UNIFIER of string; 
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 

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

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

263 

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

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

265 

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

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

269 

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

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

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

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

275 
 meet (PType (a, Ts), S) = 
19465  276 
ListPair.app meet (Ts, Type.arity_sorts pp tsig a S 
277 
handle ERROR msg => raise NO_UNIFIER msg) 

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

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

281 
 meet (PTVar (xi, S'), S) = 
19465  282 
if Type.subsort tsig (S', S) then () 
283 
else raise NO_UNIFIER (not_of_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

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

285 

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

286 

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

287 
(* occurs check and assigment *) 
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 
fun occurs_check r (Link (r' as ref T)) = 
d35fca99b3be
Type inference (isolated from type.ML, completely reimplemented).
wenzelm
parents:
diff
changeset

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

291 
else occurs_check r T 
15570  292 
 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

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

294 

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

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

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

297 
T' as Link (r' as ref (Param _)) => 
8087  298 
if r = r' then () else (meet (T', S); r := T') 
299 
 T' => (occurs_check r T'; meet (T', S); r := T')); 

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 

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

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

303 

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

304 
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

305 
 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

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

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

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

312 
 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

313 

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

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

315 

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

316 

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

317 

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

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

319 

14828  320 
fun appl_error pp why t T u U = 
8087  321 
["Type error in application: " ^ why, 
322 
"", 

323 
Pretty.string_of (Pretty.block 

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

8087  326 
Pretty.string_of (Pretty.block 
14828  327 
[Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u, 
328 
Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]), 

8087  329 
""]; 
330 

5635  331 

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

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

333 

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

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

337 

2979  338 
fun unif_failed msg = 
14828  339 
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n"; 
2979  340 

341 
fun prep_output bs ts Ts = 

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

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

346 
val ts'' = map (fn t => subst_bounds (xs, t)) ts'; 
2979  347 
in (ts'', Ts') end; 
348 

349 
fun err_loose i = 

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

3510  352 
fun err_appl msg bs t T u U = 
2979  353 
let 
3510  354 
val ([t', u'], [T', U']) = prep_output bs [t, u] [T, U]; 
355 
val why = 

356 
(case T' of 

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

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

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

362 
fun err_constraint msg bs t T U = 

363 
let 

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

365 
val text = cat_lines 

366 
[unif_failed msg, 

5635  367 
"Cannot meet type constraint:", "", 
14828  368 
Pretty.string_of (Pretty.block 
369 
[Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t', 

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

371 
Pretty.string_of (Pretty.block 

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

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

375 

376 
(* main *) 

377 

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

379 

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

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

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

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

384 
 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

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

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

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

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

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

390 
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

391 
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

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

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

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

395 
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

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

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

398 

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

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

400 

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

401 

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

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

403 

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

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

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

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

408 
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

409 

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

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

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

413 

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

414 
(*collect result unifier*) 
15531  415 
fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); NONE) 
416 
 ch_var xi_T = SOME xi_T; 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19465
diff
changeset

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

418 

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

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

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

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

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

423 
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

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

425 
in (final_ts, final_Ts, final_env) end; 
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 

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 
(** type inference **) 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

430 

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

431 
(* user constraints *) 
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 
fun constrain t T = 
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

434 
if T = dummyT then t 
19577  435 
else Const ("_type_constraint_", T > T) $ t; 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

436 

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

437 

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

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

439 

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

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

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

442 

18339  443 
val paramify_dummies = 
444 
let 

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

446 

447 
fun paramify (TFree ("'_dummy_", S)) maxidx = dummy S maxidx 

448 
 paramify (Type ("dummy", _)) maxidx = dummy [] maxidx 

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

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

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

452 
 paramify T maxidx = (T, maxidx); 

453 
in paramify end; 

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

454 

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

455 

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

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

457 

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

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

459 
let 
16668  460 
fun eq ((xi: indexname, S), (xi', S')) = 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

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

462 

19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
19012
diff
changeset

463 
val env = distinct eq (map (apsnd map_sort) raw_env); 
18964  464 
val _ = (case duplicates (eq_fst (op =)) env of [] => () 
14828  465 
 dups => error ("Inconsistent sort constraints for type variable(s) " 
466 
^ commas_quote (map (Syntax.string_of_vname' o fst) dups))); 

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

467 

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

468 
fun get xi = 
17271  469 
(case (AList.lookup (op =) env xi, def_sort xi) of 
15531  470 
(NONE, NONE) => Type.defaultS tsig 
471 
 (NONE, SOME S) => S 

472 
 (SOME S, NONE) => S 

473 
 (SOME S, SOME S') => 

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

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

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

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

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

478 

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

479 

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

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

481 

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

482 
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

483 
let 
18939  484 
fun get_type xi = the_default dummyT (def_type xi); 
16195  485 
fun is_free x = is_some (def_type (x, ~1)); 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

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

487 
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

488 

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

490 
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

491 

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

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

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

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

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

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

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

498 
 decode (t $ u) = decode t $ decode u 
18996  499 
 decode (Const (x, T)) = 
500 
let val c = (case try (unprefix Syntax.constN) x of SOME c => c  NONE => map_const x) 

501 
in Const (c, certT T) end 

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

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

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

504 
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

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

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

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

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

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

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

511 
else constrain (Var (xi, certT T)) (get_type xi) 
18996  512 
 decode (t as Bound _) = t; 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

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

514 

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

515 

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

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

517 

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

518 
(*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

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

520 

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

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

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

20161  525 
used: context of already used type variables 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

526 
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

527 

14828  528 
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

529 
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

530 
let 
14993  531 
val pat_Ts' = map (Type.cert_typ tsig) pat_Ts; 
16195  532 
val is_const = is_some o const_type; 
14788
9776f0c747c8
incorporate type inference interface from type.ML;
wenzelm
parents:
14695
diff
changeset

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

534 
map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts; 
19465  535 
val (ts, Ts, unifier) = 
536 
basic_infer_types pp tsig const_type used freeze is_param raw_ts' pat_Ts'; 

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

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

538 

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

539 
end; 