author | wenzelm |
Sun, 19 May 2024 18:43:45 +0200 | |
changeset 80181 | aa92c0f96036 |
parent 79433 | 88341f610b33 |
permissions | -rw-r--r-- |
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 |
Type-inference 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 |
47291
6a641856a0e9
better drop background syntax if entity depends on parameters;
wenzelm
parents:
46873
diff
changeset
|
10 |
val const_type: Proof.context -> string -> typ option |
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset
|
11 |
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
|
12 |
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
|
13 |
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
|
14 |
end; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
15 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
16 |
structure Type_Infer_Context: TYPE_INFER_CONTEXT = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
17 |
struct |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
18 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
19 |
(** prepare types/terms: create inference parameters **) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
20 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
21 |
(* constraints *) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
22 |
|
69575 | 23 |
val const_sorts = Config.declare_bool ("const_sorts", \<^here>) (K true); |
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
24 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
25 |
fun const_type ctxt = |
79411 | 26 |
try ((not (Config.get ctxt const_sorts) ? Term.strip_sortsT) o |
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
27 |
Consts.the_constraint (Proof_Context.consts_of ctxt)); |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
28 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
29 |
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
|
30 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
31 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
32 |
(* prepare_typ *) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
33 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
34 |
fun prepare_typ typ params_idx = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
35 |
let |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
36 |
val (params', idx) = fold_atyps |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
37 |
(fn TVar (xi, S) => |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
38 |
(fn ps_idx as (ps, idx) => |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
39 |
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
|
40 |
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
|
41 |
| _ => I) typ params_idx; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
42 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
43 |
fun prepare (T as Type (a, Ts)) idx = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
44 |
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
|
45 |
else |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
46 |
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
|
47 |
in (Type (a, Ts'), idx') end |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
48 |
| prepare (T as TVar (xi, _)) idx = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
49 |
(case Vartab.lookup params' xi of |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
50 |
NONE => T |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
51 |
| SOME p => p, idx) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
52 |
| 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
|
53 |
| prepare (T as TFree _) idx = (T, idx); |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
54 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
55 |
val (typ', idx') = prepare typ idx; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
56 |
in (typ', (params', idx')) end; |
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 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
59 |
(* prepare_term *) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
60 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
61 |
fun prepare_term ctxt tm (vparams, params, idx) = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
62 |
let |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
63 |
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
|
64 |
if not (Vartab.defined ps xi) then |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
65 |
(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
|
66 |
else ps_idx; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
67 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
68 |
val (vparams', idx') = fold_aterms |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
69 |
(fn Var (_, Type ("_polymorphic_", _)) => I |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
70 |
| Var (xi, _) => add_vparm xi |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
71 |
| Free (x, _) => add_vparm (x, ~1) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
72 |
| _ => I) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
73 |
tm (vparams, idx); |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
74 |
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
|
75 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
76 |
fun polyT_of T idx = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
77 |
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
|
78 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
79 |
fun constraint T t ps = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
80 |
if T = dummyT then (t, ps) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
81 |
else |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
82 |
let val (T', ps') = prepare_typ T ps |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
83 |
in (Type.constraint T' t, ps') end; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
84 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
85 |
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
|
86 |
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
|
87 |
val A = Type.constraint_type ctxt T; |
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
88 |
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
|
89 |
val (t', ps_idx'') = prepare t ps_idx'; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
90 |
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
|
91 |
| prepare (Const (c, T)) (ps, idx) = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
92 |
(case const_type ctxt c of |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
93 |
SOME U => |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
94 |
let val (U', idx') = polyT_of U idx |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
95 |
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
|
96 |
| NONE => error ("Undeclared constant: " ^ quote c)) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
97 |
| prepare (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
98 |
let val (T', idx') = polyT_of T idx |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
99 |
in (Var (xi, T'), (ps, idx')) end |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
100 |
| 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
|
101 |
| 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
|
102 |
| 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
|
103 |
| prepare (Abs (x, T, t)) ps_idx = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
104 |
let |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
105 |
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
|
106 |
val (t', ps_idx'') = prepare t ps_idx'; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
107 |
in (Abs (x, T', t'), ps_idx'') end |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
108 |
| prepare (t $ u) ps_idx = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
109 |
let |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
110 |
val (t', ps_idx') = prepare t ps_idx; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
111 |
val (u', ps_idx'') = prepare u ps_idx'; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
112 |
in (t' $ u', ps_idx'') end; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
113 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
114 |
val (tm', (params', idx'')) = prepare tm (params, idx'); |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
115 |
in (tm', (vparams', params', idx'')) end; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
116 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
117 |
|
45445
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset
|
118 |
(* 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
|
119 |
|
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset
|
120 |
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
|
121 |
let |
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset
|
122 |
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
|
123 |
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
|
124 |
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
|
125 |
| 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
|
126 |
(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
|
127 |
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
|
128 |
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
|
129 |
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
|
130 |
| 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
|
131 |
|
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset
|
132 |
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
|
133 |
let |
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 = 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
|
135 |
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
|
136 |
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
|
137 |
| 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
|
138 |
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
|
139 |
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
|
140 |
| 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
|
141 |
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
|
142 |
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
|
143 |
| 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
|
144 |
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
|
145 |
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
|
146 |
| 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
|
147 |
| 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
|
148 |
let |
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') = 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
|
150 |
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
|
151 |
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
|
152 |
| 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
|
153 |
let |
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 (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
|
155 |
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
|
156 |
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
|
157 |
|
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 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
|
159 |
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
|
160 |
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
|
161 |
|
41e641a870de
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents:
45429
diff
changeset
|
162 |
|
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
163 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
164 |
(** order-sorted unification of types **) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
165 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
166 |
exception NO_UNIFIER of string * typ Vartab.table; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
167 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
168 |
fun unify ctxt = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
169 |
let |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
170 |
val thy = Proof_Context.theory_of ctxt; |
59840 | 171 |
val arity_sorts = Proof_Context.arity_sorts ctxt; |
42405
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 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
174 |
(* adjust sorts of parameters *) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
175 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
176 |
fun not_of_sort x S' S = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
177 |
"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
|
178 |
Syntax.string_of_sort ctxt S; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
179 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
180 |
fun meet (_, []) tye_idx = tye_idx |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
181 |
| 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
|
182 |
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
|
183 |
| 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
|
184 |
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
|
185 |
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
|
186 |
| 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
|
187 |
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
|
188 |
else if Type_Infer.is_param xi then |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
189 |
(Vartab.update_new |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
190 |
(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
|
191 |
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
|
192 |
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
|
193 |
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
|
194 |
| meets _ tye_idx = tye_idx; |
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 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
197 |
(* occurs check and assignment *) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
198 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
199 |
fun occurs_check tye xi (TVar (xi', _)) = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
200 |
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
|
201 |
else |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
202 |
(case Vartab.lookup tye xi' of |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
203 |
NONE => () |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
204 |
| SOME T => occurs_check tye xi T) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
205 |
| 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
|
206 |
| occurs_check _ _ _ = (); |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
207 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
208 |
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
|
209 |
if xi = xi' then env |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
210 |
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
|
211 |
| assign xi T S (env as (tye, _)) = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
212 |
(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
|
213 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
214 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
215 |
(* unification *) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
216 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
217 |
fun show_tycon (a, Ts) = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
218 |
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
|
219 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
220 |
fun unif (T1, T2) (env as (tye, _)) = |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
56438
diff
changeset
|
221 |
(case apply2 (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of |
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
222 |
((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
|
223 |
| ((_, 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
|
224 |
| ((_, Type (a, Ts)), (_, Type (b, Us))) => |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
225 |
if a <> b then |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
226 |
raise NO_UNIFIER |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
227 |
("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
|
228 |
else fold unif (Ts ~~ Us) env |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
229 |
| ((_, 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
|
230 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
231 |
in unif end; |
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 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
235 |
(** simple type inference **) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
236 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
237 |
(* infer *) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
238 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
239 |
fun infer ctxt = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
240 |
let |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
241 |
(* errors *) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
242 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
243 |
fun prep_output tye bs ts Ts = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
244 |
let |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
245 |
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
|
246 |
val (Ts', Ts'') = chop (length Ts) Ts_bTs'; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
247 |
fun prep t = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
248 |
let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) |
49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
47291
diff
changeset
|
249 |
in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end; |
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
250 |
in (map prep ts', Ts') end; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
251 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
252 |
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
|
253 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
254 |
fun unif_failed msg = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
255 |
"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
|
256 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
257 |
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
|
258 |
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
|
259 |
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
|
260 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
261 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
262 |
(* main *) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
263 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
264 |
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
|
265 |
| inf _ (Free (_, T)) tye_idx = (T, tye_idx) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
266 |
| inf _ (Var (_, T)) tye_idx = (T, tye_idx) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
267 |
| inf bs (Bound i) tye_idx = |
43278 | 268 |
(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
|
269 |
| inf bs (Abs (x, T, t)) tye_idx = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
270 |
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
|
271 |
in (T --> U, tye_idx') end |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
272 |
| inf bs (t $ u) tye_idx = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
273 |
let |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
274 |
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
|
275 |
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
|
276 |
val V = Type_Infer.mk_param idx []; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
277 |
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
|
278 |
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
|
279 |
in (V, tye_idx'') end; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
280 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
281 |
in inf [] end; |
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 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
284 |
(* main interfaces *) |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
285 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
286 |
fun prepare ctxt raw_ts = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
287 |
let |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
288 |
val constrain_vars = Term.map_aterms |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
289 |
(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
|
290 |
| Var (xi, T) => Type.constraint T (Var (xi, var_type ctxt xi)) |
79433 | 291 |
| _ => raise Same.SAME); |
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
292 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
293 |
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
|
294 |
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
|
295 |
val (ts', (_, _, idx')) = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
296 |
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
|
297 |
(Vartab.empty, Vartab.empty, idx); |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
298 |
in (idx', ts') end; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
299 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
300 |
fun infer_types ctxt raw_ts = |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
301 |
let |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
302 |
val (idx, ts) = prepare ctxt raw_ts; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
303 |
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
|
304 |
val (_, ts') = Type_Infer.finish ctxt tye ([], ts); |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
305 |
in ts' end; |
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
306 |
|
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
diff
changeset
|
307 |
end; |