author  wenzelm 
Mon, 12 Mar 2012 13:53:26 +0100  
changeset 46873  7a73f181cbcf 
parent 45445  41e641a870de 
child 47291  6a641856a0e9 
permissions  rwrr 
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/type_infer_context.ML 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

2 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

3 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

4 
Typeinference preparation and standard type inference. 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

5 
*) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

6 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

7 
signature TYPE_INFER_CONTEXT = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

8 
sig 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

9 
val const_sorts: bool Config.T 
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

10 
val prepare_positions: Proof.context > term list > term list * (Position.T * typ) list 
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

11 
val prepare: Proof.context > term list > int * term list 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

12 
val infer_types: Proof.context > term list > term list 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

13 
end; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

14 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

15 
structure Type_Infer_Context: TYPE_INFER_CONTEXT = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

16 
struct 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

17 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

18 
(** prepare types/terms: create inference parameters **) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

19 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

20 
(* constraints *) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

21 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

22 
val const_sorts = Config.bool (Config.declare "const_sorts" (K (Config.Bool true))); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

23 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

24 
fun const_type ctxt = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

25 
try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

26 
Consts.the_constraint (Proof_Context.consts_of ctxt)); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

27 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

28 
fun var_type ctxt = the_default dummyT o Proof_Context.def_type ctxt; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

29 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

30 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

31 
(* prepare_typ *) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

32 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

33 
fun prepare_typ typ params_idx = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

34 
let 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

35 
val (params', idx) = fold_atyps 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

36 
(fn TVar (xi, S) => 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

37 
(fn ps_idx as (ps, idx) => 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

38 
if Type_Infer.is_param xi andalso not (Vartab.defined ps xi) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

39 
then (Vartab.update (xi, Type_Infer.mk_param idx S) ps, idx + 1) else ps_idx) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

40 
 _ => I) typ params_idx; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

41 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

42 
fun prepare (T as Type (a, Ts)) idx = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

43 
if T = dummyT then (Type_Infer.mk_param idx [], idx + 1) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

44 
else 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

45 
let val (Ts', idx') = fold_map prepare Ts idx 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

46 
in (Type (a, Ts'), idx') end 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

47 
 prepare (T as TVar (xi, _)) idx = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

48 
(case Vartab.lookup params' xi of 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

49 
NONE => T 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

50 
 SOME p => p, idx) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

51 
 prepare (TFree ("'_dummy_", S)) idx = (Type_Infer.mk_param idx S, idx + 1) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

52 
 prepare (T as TFree _) idx = (T, idx); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

53 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

54 
val (typ', idx') = prepare typ idx; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

55 
in (typ', (params', idx')) end; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

56 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

57 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

58 
(* prepare_term *) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

59 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

60 
fun prepare_term ctxt tm (vparams, params, idx) = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

61 
let 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

62 
fun add_vparm xi (ps_idx as (ps, idx)) = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

63 
if not (Vartab.defined ps xi) then 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

64 
(Vartab.update (xi, Type_Infer.mk_param idx []) ps, idx + 1) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

65 
else ps_idx; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

66 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

67 
val (vparams', idx') = fold_aterms 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

68 
(fn Var (_, Type ("_polymorphic_", _)) => I 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

69 
 Var (xi, _) => add_vparm xi 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

70 
 Free (x, _) => add_vparm (x, ~1) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

71 
 _ => I) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

72 
tm (vparams, idx); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

73 
fun var_param xi = the (Vartab.lookup vparams' xi); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

74 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

75 
fun polyT_of T idx = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

76 
apsnd snd (prepare_typ (Type_Infer.paramify_vars T) (Vartab.empty, idx)); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

77 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

78 
fun constraint T t ps = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

79 
if T = dummyT then (t, ps) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

80 
else 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

81 
let val (T', ps') = prepare_typ T ps 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

82 
in (Type.constraint T' t, ps') end; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

83 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

84 
fun prepare (Const ("_type_constraint_", T) $ t) ps_idx = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

85 
let 
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

86 
val A = Type.constraint_type ctxt T; 
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

87 
val (A', ps_idx') = prepare_typ A ps_idx; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

88 
val (t', ps_idx'') = prepare t ps_idx'; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

89 
in (Const ("_type_constraint_", A' > A') $ t', ps_idx'') end 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

90 
 prepare (Const (c, T)) (ps, idx) = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

91 
(case const_type ctxt c of 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

92 
SOME U => 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

93 
let val (U', idx') = polyT_of U idx 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

94 
in constraint T (Const (c, U')) (ps, idx') end 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

95 
 NONE => error ("Undeclared constant: " ^ quote c)) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

96 
 prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

97 
let val (T', idx') = polyT_of T idx 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

98 
in (Var (xi, T'), (ps, idx')) end 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

99 
 prepare (Var (xi, T)) ps_idx = constraint T (Var (xi, var_param xi)) ps_idx 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

100 
 prepare (Free (x, T)) ps_idx = constraint T (Free (x, var_param (x, ~1))) ps_idx 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

101 
 prepare (Bound i) ps_idx = (Bound i, ps_idx) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

102 
 prepare (Abs (x, T, t)) ps_idx = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

103 
let 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

104 
val (T', ps_idx') = prepare_typ T ps_idx; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

105 
val (t', ps_idx'') = prepare t ps_idx'; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

106 
in (Abs (x, T', t'), ps_idx'') end 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

107 
 prepare (t $ u) ps_idx = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

108 
let 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

109 
val (t', ps_idx') = prepare t ps_idx; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

110 
val (u', ps_idx'') = prepare u ps_idx'; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

111 
in (t' $ u', ps_idx'') end; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

112 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

113 
val (tm', (params', idx'')) = prepare tm (params, idx'); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

114 
in (tm', (vparams', params', idx'')) end; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

115 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

116 

45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

117 
(* prepare_positions *) 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

118 

41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

119 
fun prepare_positions ctxt tms = 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

120 
let 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

121 
fun prepareT (Type (a, Ts)) ps_idx = 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

122 
let val (Ts', ps_idx') = fold_map prepareT Ts ps_idx 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

123 
in (Type (a, Ts'), ps_idx') end 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

124 
 prepareT T (ps, idx) = 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

125 
(case Term_Position.decode_positionT T of 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

126 
SOME pos => 
46873
7a73f181cbcf
clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;
wenzelm
parents:
45445
diff
changeset

127 
let val U = Type_Infer.mk_param idx [] 
7a73f181cbcf
clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;
wenzelm
parents:
45445
diff
changeset

128 
in (U, ((pos, U) :: ps, idx + 1)) end 
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

129 
 NONE => (T, (ps, idx))); 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

130 

41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

131 
fun prepare (Const ("_type_constraint_", T)) ps_idx = 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

132 
let 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

133 
val A = Type.constraint_type ctxt T; 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

134 
val (A', ps_idx') = prepareT A ps_idx; 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

135 
in (Const ("_type_constraint_", A' > A'), ps_idx') end 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

136 
 prepare (Const (c, T)) ps_idx = 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

137 
let val (T', ps_idx') = prepareT T ps_idx 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

138 
in (Const (c, T'), ps_idx') end 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

139 
 prepare (Free (x, T)) ps_idx = 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

140 
let val (T', ps_idx') = prepareT T ps_idx 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

141 
in (Free (x, T'), ps_idx') end 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

142 
 prepare (Var (xi, T)) ps_idx = 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

143 
let val (T', ps_idx') = prepareT T ps_idx 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

144 
in (Var (xi, T'), ps_idx') end 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

145 
 prepare (t as Bound _) ps_idx = (t, ps_idx) 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

146 
 prepare (Abs (x, T, t)) ps_idx = 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

147 
let 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

148 
val (T', ps_idx') = prepareT T ps_idx; 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

149 
val (t', ps_idx'') = prepare t ps_idx'; 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

150 
in (Abs (x, T', t'), ps_idx'') end 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

151 
 prepare (t $ u) ps_idx = 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

152 
let 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

153 
val (t', ps_idx') = prepare t ps_idx; 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

154 
val (u', ps_idx'') = prepare u ps_idx'; 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

155 
in (t' $ u', ps_idx'') end; 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

156 

41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

157 
val idx = Type_Infer.param_maxidx_of tms + 1; 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

158 
val (tms', (ps, _)) = fold_map prepare tms ([], idx); 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

159 
in (tms', ps) end; 
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

160 

41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset

161 

42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

162 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

163 
(** ordersorted unification of types **) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

164 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

165 
exception NO_UNIFIER of string * typ Vartab.table; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

166 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

167 
fun unify ctxt = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

168 
let 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

169 
val thy = Proof_Context.theory_of ctxt; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

170 
val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

171 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

172 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

173 
(* adjust sorts of parameters *) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

174 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

175 
fun not_of_sort x S' S = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

176 
"Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^ 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

177 
Syntax.string_of_sort ctxt S; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

178 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

179 
fun meet (_, []) tye_idx = tye_idx 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

180 
 meet (Type (a, Ts), S) (tye_idx as (tye, _)) = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

181 
meets (Ts, arity_sorts a S handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

182 
 meet (TFree (x, S'), S) (tye_idx as (tye, _)) = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

183 
if Sign.subsort thy (S', S) then tye_idx 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

184 
else raise NO_UNIFIER (not_of_sort x S' S, tye) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

185 
 meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

186 
if Sign.subsort thy (S', S) then tye_idx 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

187 
else if Type_Infer.is_param xi then 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

188 
(Vartab.update_new 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

189 
(xi, Type_Infer.mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

190 
else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

191 
and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

192 
meets (Ts, Ss) (meet (Type_Infer.deref tye T, S) tye_idx) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

193 
 meets _ tye_idx = tye_idx; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

194 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

195 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

196 
(* occurs check and assignment *) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

197 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

198 
fun occurs_check tye xi (TVar (xi', _)) = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

199 
if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

200 
else 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

201 
(case Vartab.lookup tye xi' of 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

202 
NONE => () 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

203 
 SOME T => occurs_check tye xi T) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

204 
 occurs_check tye xi (Type (_, Ts)) = List.app (occurs_check tye xi) Ts 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

205 
 occurs_check _ _ _ = (); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

206 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

207 
fun assign xi (T as TVar (xi', _)) S env = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

208 
if xi = xi' then env 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

209 
else env > meet (T, S) >> Vartab.update_new (xi, T) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

210 
 assign xi T S (env as (tye, _)) = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

211 
(occurs_check tye xi T; env > meet (T, S) >> Vartab.update_new (xi, T)); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

212 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

213 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

214 
(* unification *) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

215 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

216 
fun show_tycon (a, Ts) = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

217 
quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT))); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

218 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

219 
fun unif (T1, T2) (env as (tye, _)) = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

220 
(case pairself (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

221 
((true, TVar (xi, S)), (_, T)) => assign xi T S env 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

222 
 ((_, T), (true, TVar (xi, S))) => assign xi T S env 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

223 
 ((_, Type (a, Ts)), (_, Type (b, Us))) => 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

224 
if a <> b then 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

225 
raise NO_UNIFIER 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

226 
("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

227 
else fold unif (Ts ~~ Us) env 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

228 
 ((_, T), (_, U)) => if T = U then env else raise NO_UNIFIER ("", tye)); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

229 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

230 
in unif end; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

231 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

232 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

233 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

234 
(** simple type inference **) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

235 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

236 
(* infer *) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

237 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

238 
fun infer ctxt = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

239 
let 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

240 
(* errors *) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

241 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

242 
fun prep_output tye bs ts Ts = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

243 
let 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

244 
val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

245 
val (Ts', Ts'') = chop (length Ts) Ts_bTs'; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

246 
fun prep t = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

247 
let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

248 
in Term.subst_bounds (map Syntax_Trans.mark_boundT xs, t) end; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

249 
in (map prep ts', Ts') end; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

250 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

251 
fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

252 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

253 
fun unif_failed msg = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

254 
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n"; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

255 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

256 
fun err_appl msg tye bs t T u U = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

257 
let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U] 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

258 
in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

259 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

260 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

261 
(* main *) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

262 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

263 
fun inf _ (Const (_, T)) tye_idx = (T, tye_idx) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

264 
 inf _ (Free (_, T)) tye_idx = (T, tye_idx) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

265 
 inf _ (Var (_, T)) tye_idx = (T, tye_idx) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

266 
 inf bs (Bound i) tye_idx = 
43278  267 
(snd (nth bs i handle General.Subscript => err_loose i), tye_idx) 
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

268 
 inf bs (Abs (x, T, t)) tye_idx = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

269 
let val (U, tye_idx') = inf ((x, T) :: bs) t tye_idx 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

270 
in (T > U, tye_idx') end 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

271 
 inf bs (t $ u) tye_idx = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

272 
let 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

273 
val (T, tye_idx') = inf bs t tye_idx; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

274 
val (U, (tye, idx)) = inf bs u tye_idx'; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

275 
val V = Type_Infer.mk_param idx []; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

276 
val tye_idx'' = unify ctxt (U > V, T) (tye, idx + 1) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

277 
handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

278 
in (V, tye_idx'') end; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

279 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

280 
in inf [] end; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

281 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

282 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

283 
(* main interfaces *) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

284 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

285 
fun prepare ctxt raw_ts = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

286 
let 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

287 
val constrain_vars = Term.map_aterms 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

288 
(fn Free (x, T) => Type.constraint T (Free (x, var_type ctxt (x, ~1))) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

289 
 Var (xi, T) => Type.constraint T (Var (xi, var_type ctxt xi)) 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

290 
 t => t); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

291 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

292 
val ts = burrow_types (Syntax.check_typs ctxt) raw_ts; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

293 
val idx = Type_Infer.param_maxidx_of ts + 1; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

294 
val (ts', (_, _, idx')) = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

295 
fold_map (prepare_term ctxt o constrain_vars) ts 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

296 
(Vartab.empty, Vartab.empty, idx); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

297 
in (idx', ts') end; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

298 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

299 
fun infer_types ctxt raw_ts = 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

300 
let 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

301 
val (idx, ts) = prepare ctxt raw_ts; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

302 
val (tye, _) = fold (snd oo infer ctxt) ts (Vartab.empty, idx); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

303 
val (_, ts') = Type_Infer.finish ctxt tye ([], ts); 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

304 
in ts' end; 
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

305 

13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset

306 
end; 