165 fun cert (T as Type (c, Ts)) = |
165 fun cert (T as Type (c, Ts)) = |
166 let |
166 let |
167 val Ts' = map cert Ts; |
167 val Ts' = map cert Ts; |
168 fun nargs n = if length Ts <> n then err (bad_nargs c) else (); |
168 fun nargs n = if length Ts <> n then err (bad_nargs c) else (); |
169 in |
169 in |
170 (case Symtab.lookup (types, c) of |
170 (case Symtab.curried_lookup types c of |
171 SOME (LogicalType n, _) => (nargs n; Type (c, Ts')) |
171 SOME (LogicalType n, _) => (nargs n; Type (c, Ts')) |
172 | SOME (Abbreviation (vs, U, syn), _) => (nargs (length vs); |
172 | SOME (Abbreviation (vs, U, syn), _) => (nargs (length vs); |
173 if syn then check_syntax c else (); |
173 if syn then check_syntax c else (); |
174 if normalize then inst_typ (vs ~~ Ts') U |
174 if normalize then inst_typ (vs ~~ Ts') U |
175 else Type (c, Ts')) |
175 else Type (c, Ts')) |
282 fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^ |
282 fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^ |
283 quote (Term.string_of_vname ixn) ^ " has two distinct sorts", |
283 quote (Term.string_of_vname ixn) ^ " has two distinct sorts", |
284 [TVar (ixn, S), TVar (ixn, S')], []); |
284 [TVar (ixn, S), TVar (ixn, S')], []); |
285 |
285 |
286 fun lookup (tye, (ixn, S)) = |
286 fun lookup (tye, (ixn, S)) = |
287 (case Vartab.lookup (tye, ixn) of |
287 (case Vartab.curried_lookup tye ixn of |
288 NONE => NONE |
288 NONE => NONE |
289 | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S'); |
289 | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S'); |
290 |
290 |
291 |
291 |
292 (* matching *) |
292 (* matching *) |
296 fun typ_match tsig = |
296 fun typ_match tsig = |
297 let |
297 let |
298 fun match (TVar (v, S), T) subs = |
298 fun match (TVar (v, S), T) subs = |
299 (case lookup (subs, (v, S)) of |
299 (case lookup (subs, (v, S)) of |
300 NONE => |
300 NONE => |
301 if of_sort tsig (T, S) then Vartab.update_new ((v, (S, T)), subs) |
301 if of_sort tsig (T, S) then Vartab.curried_update_new (v, (S, T)) subs |
302 else raise TYPE_MATCH |
302 else raise TYPE_MATCH |
303 | SOME U => if U = T then subs else raise TYPE_MATCH) |
303 | SOME U => if U = T then subs else raise TYPE_MATCH) |
304 | match (Type (a, Ts), Type (b, Us)) subs = |
304 | match (Type (a, Ts), Type (b, Us)) subs = |
305 if a <> b then raise TYPE_MATCH |
305 if a <> b then raise TYPE_MATCH |
306 else matches (Ts, Us) subs |
306 else matches (Ts, Us) subs |
315 (typ_match tsig (U, T) Vartab.empty; true) handle TYPE_MATCH => false; |
315 (typ_match tsig (U, T) Vartab.empty; true) handle TYPE_MATCH => false; |
316 |
316 |
317 (*purely structural matching*) |
317 (*purely structural matching*) |
318 fun raw_match (TVar (v, S), T) subs = |
318 fun raw_match (TVar (v, S), T) subs = |
319 (case lookup (subs, (v, S)) of |
319 (case lookup (subs, (v, S)) of |
320 NONE => Vartab.update_new ((v, (S, T)), subs) |
320 NONE => Vartab.curried_update_new (v, (S, T)) subs |
321 | SOME U => if U = T then subs else raise TYPE_MATCH) |
321 | SOME U => if U = T then subs else raise TYPE_MATCH) |
322 | raw_match (Type (a, Ts), Type (b, Us)) subs = |
322 | raw_match (Type (a, Ts), Type (b, Us)) subs = |
323 if a <> b then raise TYPE_MATCH |
323 if a <> b then raise TYPE_MATCH |
324 else raw_matches (Ts, Us) subs |
324 else raw_matches (Ts, Us) subs |
325 | raw_match (TFree x, TFree y) subs = |
325 | raw_match (TFree x, TFree y) subs = |
364 Sorts.mg_domain (classes, arities) a S handle Sorts.DOMAIN _ => raise TUNIFY; |
364 Sorts.mg_domain (classes, arities) a S handle Sorts.DOMAIN _ => raise TUNIFY; |
365 |
365 |
366 fun meet (_, []) tye = tye |
366 fun meet (_, []) tye = tye |
367 | meet (TVar (xi, S'), S) tye = |
367 | meet (TVar (xi, S'), S) tye = |
368 if Sorts.sort_le classes (S', S) then tye |
368 if Sorts.sort_le classes (S', S) then tye |
369 else Vartab.update_new ((xi, (S', |
369 else Vartab.curried_update_new |
370 gen_tyvar (Sorts.inter_sort classes (S', S)))), tye) |
370 (xi, (S', gen_tyvar (Sorts.inter_sort classes (S', S)))) tye |
371 | meet (TFree (_, S'), S) tye = |
371 | meet (TFree (_, S'), S) tye = |
372 if Sorts.sort_le classes (S', S) then tye |
372 if Sorts.sort_le classes (S', S) then tye |
373 else raise TUNIFY |
373 else raise TUNIFY |
374 | meet (Type (a, Ts), S) tye = meets (Ts, mg_domain a S) tye |
374 | meet (Type (a, Ts), S) tye = meets (Ts, mg_domain a S) tye |
375 and meets (T :: Ts, S :: Ss) tye = meets (Ts, Ss) (meet (devar tye T, S) tye) |
375 and meets (T :: Ts, S :: Ss) tye = meets (Ts, Ss) (meet (devar tye T, S) tye) |
379 (case (devar tye ty1, devar tye ty2) of |
379 (case (devar tye ty1, devar tye ty2) of |
380 (T as TVar (v, S1), U as TVar (w, S2)) => |
380 (T as TVar (v, S1), U as TVar (w, S2)) => |
381 if eq_ix (v, w) then |
381 if eq_ix (v, w) then |
382 if S1 = S2 then tye else tvar_clash v S1 S2 |
382 if S1 = S2 then tye else tvar_clash v S1 S2 |
383 else if Sorts.sort_le classes (S1, S2) then |
383 else if Sorts.sort_le classes (S1, S2) then |
384 Vartab.update_new ((w, (S2, T)), tye) |
384 Vartab.curried_update_new (w, (S2, T)) tye |
385 else if Sorts.sort_le classes (S2, S1) then |
385 else if Sorts.sort_le classes (S2, S1) then |
386 Vartab.update_new ((v, (S1, U)), tye) |
386 Vartab.curried_update_new (v, (S1, U)) tye |
387 else |
387 else |
388 let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in |
388 let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in |
389 Vartab.update_new ((v, (S1, S)), Vartab.update_new ((w, (S2, S)), tye)) |
389 Vartab.curried_update_new (v, (S1, S)) (Vartab.curried_update_new (w, (S2, S)) tye) |
390 end |
390 end |
391 | (TVar (v, S), T) => |
391 | (TVar (v, S), T) => |
392 if occurs v tye T then raise TUNIFY |
392 if occurs v tye T then raise TUNIFY |
393 else meet (T, S) (Vartab.update_new ((v, (S, T)), tye)) |
393 else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye) |
394 | (T, TVar (v, S)) => |
394 | (T, TVar (v, S)) => |
395 if occurs v tye T then raise TUNIFY |
395 if occurs v tye T then raise TUNIFY |
396 else meet (T, S) (Vartab.update_new ((v, (S, T)), tye)) |
396 else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye) |
397 | (Type (a, Ts), Type (b, Us)) => |
397 | (Type (a, Ts), Type (b, Us)) => |
398 if a <> b then raise TUNIFY |
398 if a <> b then raise TUNIFY |
399 else unifs (Ts, Us) tye |
399 else unifs (Ts, Us) tye |
400 | (T, U) => if T = U then tye else raise TUNIFY) |
400 | (T, U) => if T = U then tye else raise TUNIFY) |
401 and unifs (T :: Ts, U :: Us) tye = unifs (Ts, Us) (unif (T, U) tye) |
401 and unifs (T :: Ts, U :: Us) tye = unifs (Ts, Us) (unif (T, U) tye) |
406 fun raw_unify (ty1, ty2) tye = |
406 fun raw_unify (ty1, ty2) tye = |
407 (case (devar tye ty1, devar tye ty2) of |
407 (case (devar tye ty1, devar tye ty2) of |
408 (T as TVar (v, S1), U as TVar (w, S2)) => |
408 (T as TVar (v, S1), U as TVar (w, S2)) => |
409 if eq_ix (v, w) then |
409 if eq_ix (v, w) then |
410 if S1 = S2 then tye else tvar_clash v S1 S2 |
410 if S1 = S2 then tye else tvar_clash v S1 S2 |
411 else Vartab.update_new ((w, (S2, T)), tye) |
411 else Vartab.curried_update_new (w, (S2, T)) tye |
412 | (TVar (v, S), T) => |
412 | (TVar (v, S), T) => |
413 if occurs v tye T then raise TUNIFY |
413 if occurs v tye T then raise TUNIFY |
414 else Vartab.update_new ((v, (S, T)), tye) |
414 else Vartab.curried_update_new (v, (S, T)) tye |
415 | (T, TVar (v, S)) => |
415 | (T, TVar (v, S)) => |
416 if occurs v tye T then raise TUNIFY |
416 if occurs v tye T then raise TUNIFY |
417 else Vartab.update_new ((v, (S, T)), tye) |
417 else Vartab.curried_update_new (v, (S, T)) tye |
418 | (Type (a, Ts), Type (b, Us)) => |
418 | (Type (a, Ts), Type (b, Us)) => |
419 if a <> b then raise TUNIFY |
419 if a <> b then raise TUNIFY |
420 else raw_unifys (Ts, Us) tye |
420 else raw_unifys (Ts, Us) tye |
421 | (T, U) => if T = U then tye else raise TUNIFY) |
421 | (T, U) => if T = U then tye else raise TUNIFY) |
422 and raw_unifys (T :: Ts, U :: Us) tye = raw_unifys (Ts, Us) (raw_unify (T, U) tye) |
422 and raw_unifys (T :: Ts, U :: Us) tye = raw_unifys (Ts, Us) (raw_unify (T, U) tye) |
474 |
474 |
475 fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]); |
475 fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]); |
476 |
476 |
477 fun insert_arities pp classes (t, ars) arities = |
477 fun insert_arities pp classes (t, ars) arities = |
478 let val ars' = |
478 let val ars' = |
479 Symtab.lookup_multi (arities, t) |
479 Symtab.curried_lookup_multi arities t |
480 |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars) |
480 |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars) |
481 in Symtab.update ((t, ars'), arities) end; |
481 in Symtab.curried_update (t, ars') arities end; |
482 |
482 |
483 fun insert_table pp classes = Symtab.fold (fn (t, ars) => |
483 fun insert_table pp classes = Symtab.fold (fn (t, ars) => |
484 insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars)); |
484 insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars)); |
485 |
485 |
486 in |
486 in |
487 |
487 |
488 fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) => |
488 fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) => |
489 let |
489 let |
490 fun prep (t, Ss, S) = |
490 fun prep (t, Ss, S) = |
491 (case Symtab.lookup (#2 types, t) of |
491 (case Symtab.curried_lookup (#2 types) t of |
492 SOME (LogicalType n, _) => |
492 SOME (LogicalType n, _) => |
493 if length Ss = n then |
493 if length Ss = n then |
494 (t, map (cert_sort tsig) Ss, cert_sort tsig S) |
494 (t, map (cert_sort tsig) Ss, cert_sort tsig S) |
495 handle TYPE (msg, _, _) => error msg |
495 handle TYPE (msg, _, _) => error msg |
496 else error (bad_nargs t) |
496 else error (bad_nargs t) |
589 fun new_decl naming (c, decl) (space, types) = |
589 fun new_decl naming (c, decl) (space, types) = |
590 let |
590 let |
591 val c' = NameSpace.full naming c; |
591 val c' = NameSpace.full naming c; |
592 val space' = NameSpace.declare naming c' space; |
592 val space' = NameSpace.declare naming c' space; |
593 val types' = |
593 val types' = |
594 (case Symtab.lookup (types, c') of |
594 (case Symtab.curried_lookup types c' of |
595 SOME (decl', _) => err_in_decls c' decl decl' |
595 SOME (decl', _) => err_in_decls c' decl decl' |
596 | NONE => Symtab.update ((c', (decl, stamp ())), types)); |
596 | NONE => Symtab.curried_update (c', (decl, stamp ())) types); |
597 in (space', types') end; |
597 in (space', types') end; |
598 |
598 |
599 fun the_decl (_, types) c = fst (the (Symtab.lookup (types, c))); |
599 fun the_decl (_, types) = fst o the o Symtab.curried_lookup types; |
600 |
600 |
601 fun change_types f = map_tsig (fn (classes, default, types, arities) => |
601 fun change_types f = map_tsig (fn (classes, default, types, arities) => |
602 (classes, default, f types, arities)); |
602 (classes, default, f types, arities)); |
603 |
603 |
604 fun syntactic types (Type (c, Ts)) = |
604 fun syntactic types (Type (c, Ts)) = |
605 (case Symtab.lookup (types, c) of SOME (Nonterminal, _) => true | _ => false) |
605 (case Symtab.curried_lookup types c of SOME (Nonterminal, _) => true | _ => false) |
606 orelse exists (syntactic types) Ts |
606 orelse exists (syntactic types) Ts |
607 | syntactic _ _ = false; |
607 | syntactic _ _ = false; |
608 |
608 |
609 fun add_abbrev naming (a, vs, rhs) tsig = tsig |> change_types (fn types => |
609 fun add_abbrev naming (a, vs, rhs) tsig = tsig |> change_types (fn types => |
610 let |
610 let |