109 |
107 |
110 (** raw typs/terms to pretyps/preterms **) |
108 (** raw typs/terms to pretyps/preterms **) |
111 |
109 |
112 (* pretyp_of *) |
110 (* pretyp_of *) |
113 |
111 |
114 fun pretyp_of is_para typ params = |
112 fun pretyp_of is_para typ params_idx = |
115 let |
113 let |
116 val params' = fold_atyps |
114 val (params', idx) = fold_atyps |
117 (fn TVar (xi as (x, _), S) => |
115 (fn TVar (xi as (x, _), S) => |
118 (fn ps => |
116 (fn ps_idx as (ps, idx) => |
119 if is_para xi andalso not (Vartab.defined ps xi) |
117 if is_para xi andalso not (Vartab.defined ps xi) |
120 then Vartab.update (xi, mk_param S) ps else ps) |
118 then (Vartab.update (xi, Param (idx, S)) ps, idx + 1) else ps_idx) |
121 | _ => I) typ params; |
119 | _ => I) typ params_idx; |
122 |
120 |
123 fun pre_of (TVar (v as (xi, _))) = |
121 fun pre_of (TVar (v as (xi, _))) idx = |
124 (case Vartab.lookup params' xi of |
122 (case Vartab.lookup params' xi of |
125 NONE => PTVar v |
123 NONE => PTVar v |
126 | SOME p => p) |
124 | SOME p => p, idx) |
127 | pre_of (TFree ("'_dummy_", S)) = mk_param S |
125 | pre_of (TFree ("'_dummy_", S)) idx = (Param (idx, S), idx + 1) |
128 | pre_of (TFree v) = PTFree v |
126 | pre_of (TFree v) idx = (PTFree v, idx) |
129 | pre_of (T as Type (a, Ts)) = |
127 | pre_of (T as Type (a, Ts)) idx = |
130 if T = dummyT then mk_param [] |
128 if T = dummyT then (Param (idx, []), idx + 1) |
131 else PType (a, map pre_of Ts); |
129 else |
132 in (pre_of typ, params') end; |
130 let val (Ts', idx') = fold_map pre_of Ts idx |
|
131 in (PType (a, Ts'), idx') end; |
|
132 |
|
133 val (ptyp, idx') = pre_of typ idx; |
|
134 in (ptyp, (params', idx')) end; |
133 |
135 |
134 |
136 |
135 (* preterm_of *) |
137 (* preterm_of *) |
136 |
138 |
137 fun preterm_of const_type is_para tm (vparams, params) = |
139 fun preterm_of const_type is_para tm (vparams, params, idx) = |
138 let |
140 let |
139 fun add_vparm xi ps = |
141 fun add_vparm xi (ps_idx as (ps, idx)) = |
140 if not (Vartab.defined ps xi) then |
142 if not (Vartab.defined ps xi) then |
141 Vartab.update (xi, mk_param []) ps |
143 (Vartab.update (xi, Param (idx, [])) ps, idx + 1) |
142 else ps; |
144 else ps_idx; |
143 |
145 |
144 val vparams' = fold_aterms |
146 val (vparams', idx') = fold_aterms |
145 (fn Var (_, Type ("_polymorphic_", _)) => I |
147 (fn Var (_, Type ("_polymorphic_", _)) => I |
146 | Var (xi, _) => add_vparm xi |
148 | Var (xi, _) => add_vparm xi |
147 | Free (x, _) => add_vparm (x, ~1) |
149 | Free (x, _) => add_vparm (x, ~1) |
148 | _ => I) |
150 | _ => I) |
149 tm vparams; |
151 tm (vparams, idx); |
150 fun var_param xi = the (Vartab.lookup vparams' xi); |
152 fun var_param xi = the (Vartab.lookup vparams' xi); |
151 |
153 |
152 val preT_of = pretyp_of is_para; |
154 val preT_of = pretyp_of is_para; |
153 fun polyT_of T = fst (pretyp_of (K true) T Vartab.empty); |
155 fun polyT_of T idx = apsnd snd (pretyp_of (K true) T (Vartab.empty, idx)); |
154 |
156 |
155 fun constraint T t ps = |
157 fun constraint T t ps = |
156 if T = dummyT then (t, ps) |
158 if T = dummyT then (t, ps) |
157 else |
159 else |
158 let val (T', ps') = preT_of T ps |
160 let val (T', ps') = preT_of T ps |
159 in (Constraint (t, T'), ps') end; |
161 in (Constraint (t, T'), ps') end; |
160 |
162 |
161 fun pre_of (Const (c, T)) ps = |
163 fun pre_of (Const (c, T)) (ps, idx) = |
162 (case const_type c of |
164 (case const_type c of |
163 SOME U => constraint T (PConst (c, polyT_of U)) ps |
165 SOME U => |
|
166 let val (pU, idx') = polyT_of U idx |
|
167 in constraint T (PConst (c, pU)) (ps, idx') end |
164 | NONE => raise TYPE ("No such constant: " ^ quote c, [], [])) |
168 | NONE => raise TYPE ("No such constant: " ^ quote c, [], [])) |
165 | pre_of (Var (xi, Type ("_polymorphic_", [T]))) ps = (PVar (xi, polyT_of T), ps) |
169 | pre_of (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) = |
166 | pre_of (Var (xi, T)) ps = constraint T (PVar (xi, var_param xi)) ps |
170 let val (pT, idx') = polyT_of T idx |
167 | pre_of (Free (x, T)) ps = constraint T (PFree (x, var_param (x, ~1))) ps |
171 in (PVar (xi, pT), (ps, idx')) end |
168 | pre_of (Const ("_type_constraint_", Type ("fun", [T, _])) $ t) ps = |
172 | pre_of (Var (xi, T)) ps_idx = constraint T (PVar (xi, var_param xi)) ps_idx |
169 pre_of t ps |-> constraint T |
173 | pre_of (Free (x, T)) ps_idx = constraint T (PFree (x, var_param (x, ~1))) ps_idx |
170 | pre_of (Bound i) ps = (PBound i, ps) |
174 | pre_of (Const ("_type_constraint_", Type ("fun", [T, _])) $ t) ps_idx = |
171 | pre_of (Abs (x, T, t)) ps = |
175 pre_of t ps_idx |-> constraint T |
|
176 | pre_of (Bound i) ps_idx = (PBound i, ps_idx) |
|
177 | pre_of (Abs (x, T, t)) ps_idx = |
172 let |
178 let |
173 val (T', ps') = preT_of T ps; |
179 val (T', ps_idx') = preT_of T ps_idx; |
174 val (t', ps'') = pre_of t ps'; |
180 val (t', ps_idx'') = pre_of t ps_idx'; |
175 in (PAbs (x, T', t'), ps'') end |
181 in (PAbs (x, T', t'), ps_idx'') end |
176 | pre_of (t $ u) ps = |
182 | pre_of (t $ u) ps_idx = |
177 let |
183 let |
178 val (t', ps') = pre_of t ps; |
184 val (t', ps_idx') = pre_of t ps_idx; |
179 val (u', ps'') = pre_of u ps'; |
185 val (u', ps_idx'') = pre_of u ps_idx'; |
180 in (PAppl (t', u'), ps'') end; |
186 in (PAppl (t', u'), ps_idx'') end; |
181 |
187 |
182 val (tm', params') = pre_of tm params; |
188 val (tm', (params', idx'')) = pre_of tm (params, idx'); |
183 in (tm', (vparams', params')) end; |
189 in (tm', (vparams', params', idx'')) end; |
184 |
190 |
185 |
191 |
186 |
192 |
187 (** pretyps/terms to typs/terms **) |
193 (** pretyps/terms to typs/terms **) |
188 |
194 |
189 (* add_parms *) |
195 (* add_parms *) |
190 |
196 |
191 fun add_parmsT (PType (_, Ts)) rs = fold add_parmsT Ts rs |
197 fun add_parmsT tye T = case deref tye T of |
192 | add_parmsT (Link (r as ref (Param _))) rs = insert (op =) r rs |
198 PType (_, Ts) => fold (add_parmsT tye) Ts |
193 | add_parmsT (Link (ref T)) rs = add_parmsT T rs |
199 | Param (i, _) => insert (op =) i |
194 | add_parmsT _ rs = rs; |
200 | _ => I; |
195 |
201 |
196 val add_parms = fold_pretyps add_parmsT; |
202 fun add_parms tye = fold_pretyps (add_parmsT tye); |
197 |
203 |
198 |
204 |
199 (* add_names *) |
205 (* add_names *) |
200 |
206 |
201 fun add_namesT (PType (_, Ts)) = fold add_namesT Ts |
207 fun add_namesT tye T = case deref tye T of |
202 | add_namesT (PTFree (x, _)) = Name.declare x |
208 PType (_, Ts) => fold (add_namesT tye) Ts |
203 | add_namesT (PTVar ((x, _), _)) = Name.declare x |
209 | PTFree (x, _) => Name.declare x |
204 | add_namesT (Link (ref T)) = add_namesT T |
210 | PTVar ((x, _), _) => Name.declare x |
205 | add_namesT (Param _) = I; |
211 | Param _ => I; |
206 |
212 |
207 val add_names = fold_pretyps add_namesT; |
213 fun add_names tye = fold_pretyps (add_namesT tye); |
208 |
214 |
209 |
215 |
210 (* simple_typ/term_of *) |
216 (* simple_typ/term_of *) |
211 |
217 |
212 (*deref links, fail on params*) |
218 fun simple_typ_of tye f T = case deref tye T of |
213 fun simple_typ_of (PType (a, Ts)) = Type (a, map simple_typ_of Ts) |
219 PType (a, Ts) => Type (a, map (simple_typ_of tye f) Ts) |
214 | simple_typ_of (PTFree v) = TFree v |
220 | PTFree v => TFree v |
215 | simple_typ_of (PTVar v) = TVar v |
221 | PTVar v => TVar v |
216 | simple_typ_of (Link (ref T)) = simple_typ_of T |
222 | Param (i, S) => TVar (f i, S); |
217 | simple_typ_of (Param _) = sys_error "simple_typ_of: illegal Param"; |
|
218 |
223 |
219 (*convert types, drop constraints*) |
224 (*convert types, drop constraints*) |
220 fun simple_term_of (PConst (c, T)) = Const (c, simple_typ_of T) |
225 fun simple_term_of tye f (PConst (c, T)) = Const (c, simple_typ_of tye f T) |
221 | simple_term_of (PFree (x, T)) = Free (x, simple_typ_of T) |
226 | simple_term_of tye f (PFree (x, T)) = Free (x, simple_typ_of tye f T) |
222 | simple_term_of (PVar (xi, T)) = Var (xi, simple_typ_of T) |
227 | simple_term_of tye f (PVar (xi, T)) = Var (xi, simple_typ_of tye f T) |
223 | simple_term_of (PBound i) = Bound i |
228 | simple_term_of tye f (PBound i) = Bound i |
224 | simple_term_of (PAbs (x, T, t)) = Abs (x, simple_typ_of T, simple_term_of t) |
229 | simple_term_of tye f (PAbs (x, T, t)) = |
225 | simple_term_of (PAppl (t, u)) = simple_term_of t $ simple_term_of u |
230 Abs (x, simple_typ_of tye f T, simple_term_of tye f t) |
226 | simple_term_of (Constraint (t, _)) = simple_term_of t; |
231 | simple_term_of tye f (PAppl (t, u)) = |
227 |
232 simple_term_of tye f t $ simple_term_of tye f u |
228 |
233 | simple_term_of tye f (Constraint (t, _)) = simple_term_of tye f t; |
229 (* typs_terms_of *) (*DESTRUCTIVE*) |
234 |
230 |
235 |
231 fun typs_terms_of used maxidx (Ts, ts) = |
236 (* typs_terms_of *) |
232 let |
237 |
233 fun elim (r as ref (Param S), x) = r := PTVar ((x, maxidx + 1), S) |
238 fun typs_terms_of tye used maxidx (Ts, ts) = |
234 | elim _ = (); |
239 let |
235 |
240 val used' = fold (add_names tye) ts (fold (add_namesT tye) Ts used); |
236 val used' = fold add_names ts (fold add_namesT Ts used); |
241 val parms = rev (fold (add_parms tye) ts (fold (add_parmsT tye) Ts [])); |
237 val parms = rev (fold add_parms ts (fold add_parmsT Ts [])); |
|
238 val names = Name.invents used' ("?" ^ Name.aT) (length parms); |
242 val names = Name.invents used' ("?" ^ Name.aT) (length parms); |
239 val _ = ListPair.app elim (parms, names); |
243 val tab = Inttab.make (parms ~~ names); |
240 in (map simple_typ_of Ts, map simple_term_of ts) end; |
244 fun f i = (the (Inttab.lookup tab i), maxidx + 1); |
241 |
245 in (map (simple_typ_of tye f) Ts, map (simple_term_of tye f) ts) end; |
242 |
246 |
243 |
247 |
244 (** order-sorted unification of types **) (*DESTRUCTIVE*) |
248 |
245 |
249 (** order-sorted unification of types **) |
246 exception NO_UNIFIER of string; |
250 |
|
251 exception NO_UNIFIER of string * pretyp Inttab.table; |
247 |
252 |
248 fun unify pp tsig = |
253 fun unify pp tsig = |
249 let |
254 let |
250 |
255 |
251 (* adjust sorts of parameters *) |
256 (* adjust sorts of parameters *) |
252 |
257 |
253 fun not_of_sort x S' S = |
258 fun not_of_sort x S' S = |
254 "Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^ |
259 "Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^ |
255 Pretty.string_of_sort pp S; |
260 Pretty.string_of_sort pp S; |
256 |
261 |
257 fun meet (_, []) = () |
262 fun meet (_, []) tye_idx = tye_idx |
258 | meet (Link (r as (ref (Param S'))), S) = |
263 | meet (Param (i, S'), S) (tye_idx as (tye, idx)) = |
259 if Type.subsort tsig (S', S) then () |
264 if Type.subsort tsig (S', S) then tye_idx |
260 else r := mk_param (Type.inter_sort tsig (S', S)) |
265 else (Inttab.update_new (i, |
261 | meet (Link (ref T), S) = meet (T, S) |
266 Param (idx, Type.inter_sort tsig (S', S))) tye, idx + 1) |
262 | meet (PType (a, Ts), S) = |
267 | meet (PType (a, Ts), S) (tye_idx as (tye, _)) = |
263 ListPair.app meet (Ts, Type.arity_sorts pp tsig a S |
268 meets (Ts, Type.arity_sorts pp tsig a S |
264 handle ERROR msg => raise NO_UNIFIER msg) |
269 handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx |
265 | meet (PTFree (x, S'), S) = |
270 | meet (PTFree (x, S'), S) (tye_idx as (tye, _)) = |
266 if Type.subsort tsig (S', S) then () |
271 if Type.subsort tsig (S', S) then tye_idx |
267 else raise NO_UNIFIER (not_of_sort x S' S) |
272 else raise NO_UNIFIER (not_of_sort x S' S, tye) |
268 | meet (PTVar (xi, S'), S) = |
273 | meet (PTVar (xi, S'), S) (tye_idx as (tye, _)) = |
269 if Type.subsort tsig (S', S) then () |
274 if Type.subsort tsig (S', S) then tye_idx |
270 else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S) |
275 else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye) |
271 | meet (Param _, _) = sys_error "meet"; |
276 and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) = |
|
277 meets (Ts, Ss) (meet (deref tye T, S) tye_idx) |
|
278 | meets _ tye_idx = tye_idx; |
272 |
279 |
273 |
280 |
274 (* occurs check and assigment *) |
281 (* occurs check and assigment *) |
275 |
282 |
276 fun occurs_check r (Link (r' as ref T)) = |
283 fun occurs_check tye i (Param (i', S)) = |
277 if r = r' then raise NO_UNIFIER "Occurs check!" |
284 if i = i' then raise NO_UNIFIER ("Occurs check!", tye) |
278 else occurs_check r T |
285 else (case Inttab.lookup tye i' of |
279 | occurs_check r (PType (_, Ts)) = List.app (occurs_check r) Ts |
286 NONE => () |
280 | occurs_check _ _ = (); |
287 | SOME T => occurs_check tye i T) |
281 |
288 | occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts |
282 fun assign r T S = |
289 | occurs_check _ _ _ = (); |
283 (case deref T of |
290 |
284 T' as Link (r' as ref (Param _)) => |
291 fun assign i (T as Param (i', _)) S (tye_idx as (tye, idx)) = |
285 if r = r' then () else (meet (T', S); r := T') |
292 if i = i' then tye_idx |
286 | T' => (occurs_check r T'; meet (T', S); r := T')); |
293 else meet (T, S) (Inttab.update_new (i, T) tye, idx) |
|
294 | assign i T S (tye, idx) = |
|
295 (occurs_check tye i T; meet (T, S) (Inttab.update_new (i, T) tye, idx)); |
287 |
296 |
288 |
297 |
289 (* unification *) |
298 (* unification *) |
290 |
299 |
291 fun unif (Link (r as ref (Param S)), T) = assign r T S |
300 fun unif (T1, T2) (tye_idx as (tye, idx)) = case (deref tye T1, deref tye T2) of |
292 | unif (T, Link (r as ref (Param S))) = assign r T S |
301 (Param (i, S), T) => assign i T S tye_idx |
293 | unif (Link (ref T), U) = unif (T, U) |
302 | (T, Param (i, S)) => assign i T S tye_idx |
294 | unif (T, Link (ref U)) = unif (T, U) |
303 | (PType (a, Ts), PType (b, Us)) => |
295 | unif (PType (a, Ts), PType (b, Us)) = |
|
296 if a <> b then |
304 if a <> b then |
297 raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b) |
305 raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b, tye) |
298 else ListPair.app unif (Ts, Us) |
306 else fold unif (Ts ~~ Us) tye_idx |
299 | unif (T, U) = if T = U then () else raise NO_UNIFIER ""; |
307 | (T, U) => if T = U then tye_idx else raise NO_UNIFIER ("", tye); |
300 |
308 |
301 in unif end; |
309 in unif end; |
302 |
310 |
303 |
311 |
304 |
312 |