80 let val (T', ps') = prepare_typ T ps |
81 let val (T', ps') = prepare_typ T ps |
81 in (Type.constraint T' t, ps') end; |
82 in (Type.constraint T' t, ps') end; |
82 |
83 |
83 fun prepare (Const ("_type_constraint_", T) $ t) ps_idx = |
84 fun prepare (Const ("_type_constraint_", T) $ t) ps_idx = |
84 let |
85 let |
85 fun err () = |
86 val A = Type.constraint_type ctxt T; |
86 error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T); |
|
87 val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ()); |
|
88 val (A', ps_idx') = prepare_typ A ps_idx; |
87 val (A', ps_idx') = prepare_typ A ps_idx; |
89 val (t', ps_idx'') = prepare t ps_idx'; |
88 val (t', ps_idx'') = prepare t ps_idx'; |
90 in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end |
89 in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end |
91 | prepare (Const (c, T)) (ps, idx) = |
90 | prepare (Const (c, T)) (ps, idx) = |
92 (case const_type ctxt c of |
91 (case const_type ctxt c of |
113 |
112 |
114 val (tm', (params', idx'')) = prepare tm (params, idx'); |
113 val (tm', (params', idx'')) = prepare tm (params, idx'); |
115 in (tm', (vparams', params', idx'')) end; |
114 in (tm', (vparams', params', idx'')) end; |
116 |
115 |
117 |
116 |
|
117 (* prepare_positions *) |
|
118 |
|
119 fun prepare_positions ctxt tms = |
|
120 let |
|
121 val visible = Context_Position.is_visible ctxt; |
|
122 |
|
123 fun prepareT (Type (a, Ts)) ps_idx = |
|
124 let val (Ts', ps_idx') = fold_map prepareT Ts ps_idx |
|
125 in (Type (a, Ts'), ps_idx') end |
|
126 | prepareT T (ps, idx) = |
|
127 (case Term_Position.decode_positionT T of |
|
128 SOME pos => |
|
129 if visible then |
|
130 let val U = Type_Infer.mk_param idx [] |
|
131 in (U, ((pos, U) :: ps, idx + 1)) end |
|
132 else (dummyT, (ps, idx)) |
|
133 | NONE => (T, (ps, idx))); |
|
134 |
|
135 fun prepare (Const ("_type_constraint_", T)) ps_idx = |
|
136 let |
|
137 val A = Type.constraint_type ctxt T; |
|
138 val (A', ps_idx') = prepareT A ps_idx; |
|
139 in (Const ("_type_constraint_", A' --> A'), ps_idx') end |
|
140 | prepare (Const (c, T)) ps_idx = |
|
141 let val (T', ps_idx') = prepareT T ps_idx |
|
142 in (Const (c, T'), ps_idx') end |
|
143 | prepare (Free (x, T)) ps_idx = |
|
144 let val (T', ps_idx') = prepareT T ps_idx |
|
145 in (Free (x, T'), ps_idx') end |
|
146 | prepare (Var (xi, T)) ps_idx = |
|
147 let val (T', ps_idx') = prepareT T ps_idx |
|
148 in (Var (xi, T'), ps_idx') end |
|
149 | prepare (t as Bound _) ps_idx = (t, ps_idx) |
|
150 | prepare (Abs (x, T, t)) ps_idx = |
|
151 let |
|
152 val (T', ps_idx') = prepareT T ps_idx; |
|
153 val (t', ps_idx'') = prepare t ps_idx'; |
|
154 in (Abs (x, T', t'), ps_idx'') end |
|
155 | prepare (t $ u) ps_idx = |
|
156 let |
|
157 val (t', ps_idx') = prepare t ps_idx; |
|
158 val (u', ps_idx'') = prepare u ps_idx'; |
|
159 in (t' $ u', ps_idx'') end; |
|
160 |
|
161 val idx = Type_Infer.param_maxidx_of tms + 1; |
|
162 val (tms', (ps, _)) = fold_map prepare tms ([], idx); |
|
163 in (tms', ps) end; |
|
164 |
|
165 |
118 |
166 |
119 (** order-sorted unification of types **) |
167 (** order-sorted unification of types **) |
120 |
168 |
121 exception NO_UNIFIER of string * typ Vartab.table; |
169 exception NO_UNIFIER of string * typ Vartab.table; |
122 |
170 |