wenzelm@256: (* Title: Pure/type.ML clasohm@0: ID: $Id$ wenzelm@14790: Author: Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel clasohm@0: wenzelm@14790: Type signatures and certified types, special treatment of type vars, wenzelm@14790: matching and unification of types, extend and merge type signatures. clasohm@0: *) clasohm@0: clasohm@0: signature TYPE = wenzelm@2964: sig wenzelm@14790: (*type signatures and certified types*) wenzelm@14790: datatype decl = wenzelm@14790: LogicalType of int | wenzelm@14989: Abbreviation of string list * typ * bool | wenzelm@14790: Nonterminal wenzelm@14790: type tsig wenzelm@14790: val rep_tsig: tsig -> wenzelm@16370: {classes: NameSpace.T * Sorts.classes, wenzelm@14790: default: sort, wenzelm@16370: types: (decl * stamp) NameSpace.table, wenzelm@14790: arities: Sorts.arities, wenzelm@14790: log_types: string list, wenzelm@14790: witness: (typ * sort) option} wenzelm@14790: val empty_tsig: tsig wenzelm@14790: val classes: tsig -> class list wenzelm@14790: val defaultS: tsig -> sort wenzelm@14790: val logical_types: tsig -> string list wenzelm@14790: val universal_witness: tsig -> (typ * sort) option wenzelm@14790: val eq_sort: tsig -> sort * sort -> bool wenzelm@14790: val subsort: tsig -> sort * sort -> bool wenzelm@14790: val of_sort: tsig -> typ * sort -> bool wenzelm@14790: val cert_class: tsig -> class -> class wenzelm@14790: val cert_sort: tsig -> sort -> sort wenzelm@14790: val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list wenzelm@14993: val cert_typ: tsig -> typ -> typ wenzelm@14993: val cert_typ_syntax: tsig -> typ -> typ wenzelm@16340: val cert_typ_abbrev: tsig -> typ -> typ wenzelm@14790: wenzelm@14790: (*special treatment of type vars*) wenzelm@14790: val strip_sorts: typ -> typ wenzelm@621: val no_tvars: typ -> typ wenzelm@621: val varifyT: typ -> typ wenzelm@621: val unvarifyT: typ -> typ berghofe@15797: val varify: term * (string * sort) list -> term * ((string * sort) * indexname) list wenzelm@16289: val freeze_thaw_type: typ -> typ * (typ -> typ) wenzelm@16289: val freeze_type: typ -> typ wenzelm@16289: val freeze_thaw: term -> term * (term -> term) wenzelm@16289: val freeze: term -> term wenzelm@2964: wenzelm@14790: (*matching and unification*) wenzelm@2964: exception TYPE_MATCH berghofe@15797: type tyenv berghofe@15797: val lookup: tyenv * (indexname * sort) -> typ option wenzelm@16946: val typ_match: tsig -> typ * typ -> tyenv -> tyenv wenzelm@14790: val typ_instance: tsig -> typ * typ -> bool wenzelm@16946: val raw_match: typ * typ -> tyenv -> tyenv wenzelm@16946: val raw_instance: typ * typ -> bool wenzelm@2964: exception TUNIFY wenzelm@16946: val unify: tsig -> typ * typ -> tyenv * int -> tyenv * int wenzelm@16946: val raw_unify: typ * typ -> tyenv -> tyenv wenzelm@17804: val could_unify: typ * typ -> bool berghofe@16650: val eq_type: tyenv -> typ * typ -> bool clasohm@0: wenzelm@14790: (*extend and merge type signatures*) wenzelm@16370: val add_classes: Pretty.pp -> NameSpace.naming -> (bstring * class list) list -> tsig -> tsig wenzelm@16370: val hide_classes: bool -> string list -> tsig -> tsig wenzelm@14830: val add_classrel: Pretty.pp -> (class * class) list -> tsig -> tsig wenzelm@14790: val set_defsort: sort -> tsig -> tsig wenzelm@16370: val add_types: NameSpace.naming -> (bstring * int) list -> tsig -> tsig wenzelm@16370: val add_abbrevs: NameSpace.naming -> (string * string list * typ) list -> tsig -> tsig wenzelm@16370: val add_nonterminals: NameSpace.naming -> string list -> tsig -> tsig wenzelm@16370: val hide_types: bool -> string list -> tsig -> tsig wenzelm@14830: val add_arities: Pretty.pp -> arity list -> tsig -> tsig wenzelm@14830: val merge_tsigs: Pretty.pp -> tsig * tsig -> tsig wenzelm@2964: end; wenzelm@2964: wenzelm@2964: structure Type: TYPE = clasohm@0: struct clasohm@0: wenzelm@14790: (** type signatures and certified types **) wenzelm@2964: wenzelm@14790: (* type declarations *) wenzelm@14790: wenzelm@14790: datatype decl = wenzelm@14790: LogicalType of int | wenzelm@14989: Abbreviation of string list * typ * bool | wenzelm@14790: Nonterminal; wenzelm@14790: wenzelm@14790: fun str_of_decl (LogicalType _) = "logical type constructor" wenzelm@14790: | str_of_decl (Abbreviation _) = "type abbreviation" wenzelm@14790: | str_of_decl Nonterminal = "syntactic type"; wenzelm@14790: wenzelm@14790: wenzelm@14790: (* type tsig *) wenzelm@14790: wenzelm@14790: datatype tsig = wenzelm@14790: TSig of { wenzelm@16370: classes: NameSpace.T * Sorts.classes, (*declared classes with proper subclass relation*) wenzelm@16370: default: sort, (*default sort on input*) wenzelm@16370: types: (decl * stamp) NameSpace.table, (*declared types*) wenzelm@16370: arities: Sorts.arities, (*image specification of types wrt. sorts*) wenzelm@16370: log_types: string list, (*logical types sorted by number of arguments*) wenzelm@16370: witness: (typ * sort) option}; (*witness for non-emptiness of strictest sort*) wenzelm@14790: wenzelm@14790: fun rep_tsig (TSig comps) = comps; wenzelm@14790: wenzelm@14790: fun make_tsig (classes, default, types, arities, log_types, witness) = wenzelm@14790: TSig {classes = classes, default = default, types = types, arities = arities, wenzelm@14790: log_types = log_types, witness = witness}; wenzelm@14790: wenzelm@14790: fun build_tsig (classes, default, types, arities) = wenzelm@14790: let wenzelm@14790: val log_types = wenzelm@17756: Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) [] wenzelm@17756: |> Library.sort (Library.int_ord o pairself snd) |> map fst; wenzelm@14790: val witness = wenzelm@17756: (case Sorts.witness_sorts (snd classes, arities) log_types [] [Graph.keys (snd classes)] of skalberg@15531: [w] => SOME w | _ => NONE); wenzelm@14790: in make_tsig (classes, default, types, arities, log_types, witness) end; wenzelm@14790: wenzelm@16370: fun map_tsig f (TSig {classes, default, types, arities, log_types = _, witness = _}) = wenzelm@14790: build_tsig (f (classes, default, types, arities)); wenzelm@14790: wenzelm@16370: val empty_tsig = wenzelm@16370: build_tsig ((NameSpace.empty, Graph.empty), [], NameSpace.empty_table, Symtab.empty); wenzelm@14790: wenzelm@14790: wenzelm@14790: (* classes and sorts *) wenzelm@14790: wenzelm@16370: fun classes (TSig {classes = (_, C), ...}) = Graph.keys C; wenzelm@14790: fun defaultS (TSig {default, ...}) = default; wenzelm@14790: fun logical_types (TSig {log_types, ...}) = log_types; wenzelm@14790: fun universal_witness (TSig {witness, ...}) = witness; wenzelm@14790: wenzelm@16370: fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq (#2 classes); wenzelm@16370: fun subsort (TSig {classes, ...}) = Sorts.sort_le (#2 classes); wenzelm@16370: fun of_sort (TSig {classes, arities, ...}) = Sorts.of_sort (#2 classes, arities); wenzelm@14790: wenzelm@16370: fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes); wenzelm@16370: fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes); wenzelm@14790: wenzelm@14790: fun witness_sorts (tsig as TSig {classes, arities, log_types, ...}) = wenzelm@16370: Sorts.witness_sorts (#2 classes, arities) log_types; wenzelm@14790: wenzelm@14790: wenzelm@14790: (* certified types *) wenzelm@14790: wenzelm@14790: fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t; wenzelm@14830: fun undecl_type c = "Undeclared type constructor: " ^ quote c; wenzelm@14830: wenzelm@14998: local wenzelm@14998: wenzelm@14998: fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts) wenzelm@18957: | inst_typ env (T as TFree (x, _)) = the_default T (AList.lookup (op =) env x) wenzelm@14998: | inst_typ _ T = T; wenzelm@14998: wenzelm@14790: fun certify_typ normalize syntax tsig ty = wenzelm@14790: let wenzelm@16370: val TSig {classes = (_, classes), types = (_, types), ...} = tsig; wenzelm@14790: fun err msg = raise TYPE (msg, [ty], []); wenzelm@14790: wenzelm@14989: val check_syntax = wenzelm@14989: if syntax then K () wenzelm@14989: else fn c => err ("Illegal occurrence of syntactic type: " ^ quote c); wenzelm@14989: wenzelm@14989: fun cert (T as Type (c, Ts)) = wenzelm@14989: let wenzelm@14989: val Ts' = map cert Ts; wenzelm@14989: fun nargs n = if length Ts <> n then err (bad_nargs c) else (); wenzelm@14989: in wenzelm@17412: (case Symtab.lookup types c of skalberg@15531: SOME (LogicalType n, _) => (nargs n; Type (c, Ts')) skalberg@15531: | SOME (Abbreviation (vs, U, syn), _) => (nargs (length vs); wenzelm@14989: if syn then check_syntax c else (); wenzelm@14993: if normalize then inst_typ (vs ~~ Ts') U wenzelm@14989: else Type (c, Ts')) skalberg@15531: | SOME (Nonterminal, _) => (nargs 0; check_syntax c; T) skalberg@15531: | NONE => err (undecl_type c)) wenzelm@14790: end wenzelm@14989: | cert (TFree (x, S)) = TFree (x, Sorts.certify_sort classes S) wenzelm@14989: | cert (TVar (xi as (_, i), S)) = wenzelm@14993: if i < 0 then wenzelm@14993: err ("Malformed type variable: " ^ quote (Term.string_of_vname xi)) wenzelm@14989: else TVar (xi, Sorts.certify_sort classes S); wenzelm@14790: wenzelm@14989: val ty' = cert ty; wenzelm@14993: in if ty = ty' then ty else ty' end; (*avoid copying of already normal type*) wenzelm@14830: wenzelm@14998: in wenzelm@14998: wenzelm@16340: val cert_typ = certify_typ true false; wenzelm@16340: val cert_typ_syntax = certify_typ true true; wenzelm@16340: val cert_typ_abbrev = certify_typ false true; wenzelm@14790: wenzelm@14998: end; wenzelm@14998: wenzelm@14790: wenzelm@14790: wenzelm@14790: (** special treatment of type vars **) wenzelm@14790: wenzelm@14790: (* strip_sorts *) wenzelm@14790: wenzelm@14790: fun strip_sorts (Type (a, Ts)) = Type (a, map strip_sorts Ts) wenzelm@14790: | strip_sorts (TFree (x, _)) = TFree (x, []) wenzelm@14790: | strip_sorts (TVar (xi, _)) = TVar (xi, []); wenzelm@14790: wenzelm@14790: wenzelm@14790: (* no_tvars *) wenzelm@621: wenzelm@621: fun no_tvars T = wenzelm@12501: (case typ_tvars T of [] => T wenzelm@12501: | vs => raise TYPE ("Illegal schematic type variable(s): " ^ wenzelm@14830: commas_quote (map (Term.string_of_vname o #1) vs), [T], [])); wenzelm@621: wenzelm@7641: wenzelm@2964: (* varify, unvarify *) wenzelm@621: wenzelm@2964: val varifyT = map_type_tfree (fn (a, S) => TVar ((a, 0), S)); wenzelm@16946: val unvarifyT = map_type_tvar (fn ((a, 0), S) => TFree (a, S) | v => TVar v); wenzelm@621: wenzelm@621: fun varify (t, fixed) = wenzelm@621: let berghofe@15797: val fs = add_term_tfrees (t, []) \\ fixed; wenzelm@621: val ixns = add_term_tvar_ixns (t, []); berghofe@15797: val fmap = fs ~~ map (rpair 0) (variantlist (map fst fs, map #1 ixns)) wenzelm@2964: fun thaw (f as (a, S)) = wenzelm@17184: (case AList.lookup (op =) fmap f of skalberg@15531: NONE => TFree f wenzelm@16946: | SOME xi => TVar (xi, S)); wenzelm@12501: in (map_term_types (map_type_tfree thaw) t, fmap) end; wenzelm@2964: wenzelm@2964: wenzelm@7641: (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *) paulson@3411: wenzelm@7641: local wenzelm@7641: wenzelm@16289: fun new_name (ix, (pairs, used)) = wenzelm@16289: let val v = variant used (string_of_indexname ix) wenzelm@16289: in ((ix, v) :: pairs, v :: used) end; wenzelm@621: wenzelm@16289: fun freeze_one alist (ix, sort) = wenzelm@17184: TFree (the (AList.lookup (op =) alist ix), sort) skalberg@15531: handle Option => wenzelm@3790: raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []); wenzelm@2964: wenzelm@17184: fun thaw_one alist (a, sort) = TVar (the (AList.lookup (op =) alist a), sort) wenzelm@16289: handle Option => TFree (a, sort); wenzelm@416: wenzelm@10495: in wenzelm@10495: wenzelm@10495: (*this sort of code could replace unvarifyT*) wenzelm@7641: fun freeze_thaw_type T = wenzelm@7641: let wenzelm@7641: val used = add_typ_tfree_names (T, []) wenzelm@7641: and tvars = map #1 (add_typ_tvars (T, [])); skalberg@15574: val (alist, _) = foldr new_name ([], used) tvars; wenzelm@7641: in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end; wenzelm@7641: wenzelm@16289: val freeze_type = #1 o freeze_thaw_type; wenzelm@16289: paulson@3411: fun freeze_thaw t = wenzelm@7641: let wenzelm@7641: val used = it_term_types add_typ_tfree_names (t, []) wenzelm@7641: and tvars = map #1 (it_term_types add_typ_tvars (t, [])); skalberg@15574: val (alist, _) = foldr new_name ([], used) tvars; wenzelm@7641: in wenzelm@7641: (case alist of wenzelm@7641: [] => (t, fn x => x) (*nothing to do!*) wenzelm@7641: | _ => (map_term_types (map_type_tvar (freeze_one alist)) t, wenzelm@7641: map_term_types (map_type_tfree (thaw_one (map swap alist))))) wenzelm@7641: end; wenzelm@7641: wenzelm@16289: val freeze = #1 o freeze_thaw; wenzelm@16289: wenzelm@7641: end; wenzelm@7641: wenzelm@256: wenzelm@256: wenzelm@14790: (** matching and unification of types **) wenzelm@8899: berghofe@15797: type tyenv = (sort * typ) Vartab.table; wenzelm@256: berghofe@15797: fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^ berghofe@15797: quote (Term.string_of_vname ixn) ^ " has two distinct sorts", berghofe@15797: [TVar (ixn, S), TVar (ixn, S')], []); clasohm@0: wenzelm@16289: fun lookup (tye, (ixn, S)) = wenzelm@17412: (case Vartab.lookup tye ixn of berghofe@15797: NONE => NONE wenzelm@16289: | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S'); wenzelm@16289: clasohm@0: wenzelm@14790: (* matching *) clasohm@0: wenzelm@2964: exception TYPE_MATCH; clasohm@0: wenzelm@16946: fun typ_match tsig = wenzelm@2964: let wenzelm@16340: fun match (TVar (v, S), T) subs = berghofe@15797: (case lookup (subs, (v, S)) of skalberg@15531: NONE => wenzelm@17412: if of_sort tsig (T, S) then Vartab.update_new (v, (S, T)) subs wenzelm@14993: else raise TYPE_MATCH skalberg@15531: | SOME U => if U = T then subs else raise TYPE_MATCH) wenzelm@16340: | match (Type (a, Ts), Type (b, Us)) subs = wenzelm@2964: if a <> b then raise TYPE_MATCH wenzelm@16885: else matches (Ts, Us) subs wenzelm@16340: | match (TFree x, TFree y) subs = wenzelm@2964: if x = y then subs else raise TYPE_MATCH wenzelm@16885: | match _ _ = raise TYPE_MATCH wenzelm@16885: and matches (T :: Ts, U :: Us) subs = matches (Ts, Us) (match (T, U) subs) wenzelm@16885: | matches _ subs = subs; wenzelm@16946: in match end; clasohm@0: wenzelm@14790: fun typ_instance tsig (T, U) = wenzelm@16946: (typ_match tsig (U, T) Vartab.empty; true) handle TYPE_MATCH => false; wenzelm@16946: wenzelm@16946: (*purely structural matching*) wenzelm@16946: fun raw_match (TVar (v, S), T) subs = wenzelm@16946: (case lookup (subs, (v, S)) of wenzelm@17412: NONE => Vartab.update_new (v, (S, T)) subs wenzelm@16946: | SOME U => if U = T then subs else raise TYPE_MATCH) wenzelm@16946: | raw_match (Type (a, Ts), Type (b, Us)) subs = wenzelm@16946: if a <> b then raise TYPE_MATCH wenzelm@16946: else raw_matches (Ts, Us) subs wenzelm@16946: | raw_match (TFree x, TFree y) subs = wenzelm@16946: if x = y then subs else raise TYPE_MATCH wenzelm@16946: | raw_match _ _ = raise TYPE_MATCH wenzelm@16946: and raw_matches (T :: Ts, U :: Us) subs = raw_matches (Ts, Us) (raw_match (T, U) subs) wenzelm@16946: | raw_matches _ subs = subs; wenzelm@16946: wenzelm@16946: fun raw_instance (T, U) = wenzelm@16946: (raw_match (U, T) Vartab.empty; true) handle TYPE_MATCH => false; wenzelm@2964: clasohm@0: wenzelm@14790: (* unification *) wenzelm@2964: clasohm@0: exception TUNIFY; clasohm@0: wenzelm@14790: (*occurs_check*) wenzelm@2964: fun occurs v tye = wenzelm@2964: let wenzelm@2964: fun occ (Type (_, Ts)) = exists occ Ts wenzelm@2964: | occ (TFree _) = false berghofe@15797: | occ (TVar (w, S)) = wenzelm@2964: eq_ix (v, w) orelse berghofe@15797: (case lookup (tye, (w, S)) of skalberg@15531: NONE => false skalberg@15531: | SOME U => occ U); clasohm@0: in occ end; clasohm@0: wenzelm@14790: (*chase variable assignments; if devar returns a type var then it must be unassigned*) wenzelm@16885: fun devar tye (T as TVar v) = wenzelm@16885: (case lookup (tye, v) of wenzelm@16885: SOME U => devar tye U skalberg@15531: | NONE => T) wenzelm@16885: | devar tye T = T; clasohm@0: wenzelm@17804: (*order-sorted unification*) wenzelm@16946: fun unify (tsig as TSig {classes = (_, classes), arities, ...}) TU (tyenv, maxidx) = wenzelm@2964: let wenzelm@2964: val tyvar_count = ref maxidx; wenzelm@2964: fun gen_tyvar S = TVar (("'a", inc tyvar_count), S); wenzelm@2964: wenzelm@2964: fun mg_domain a S = wenzelm@14790: Sorts.mg_domain (classes, arities) a S handle Sorts.DOMAIN _ => raise TUNIFY; wenzelm@2964: wenzelm@16885: fun meet (_, []) tye = tye wenzelm@16885: | meet (TVar (xi, S'), S) tye = wenzelm@14790: if Sorts.sort_le classes (S', S) then tye wenzelm@17412: else Vartab.update_new wenzelm@17221: (xi, (S', gen_tyvar (Sorts.inter_sort classes (S', S)))) tye wenzelm@16885: | meet (TFree (_, S'), S) tye = wenzelm@14790: if Sorts.sort_le classes (S', S) then tye wenzelm@2964: else raise TUNIFY wenzelm@16885: | meet (Type (a, Ts), S) tye = meets (Ts, mg_domain a S) tye wenzelm@16885: and meets (T :: Ts, S :: Ss) tye = meets (Ts, Ss) (meet (devar tye T, S) tye) wenzelm@16885: | meets _ tye = tye; wenzelm@2964: wenzelm@16885: fun unif (ty1, ty2) tye = wenzelm@16885: (case (devar tye ty1, devar tye ty2) of wenzelm@2964: (T as TVar (v, S1), U as TVar (w, S2)) => berghofe@15797: if eq_ix (v, w) then berghofe@15797: if S1 = S2 then tye else tvar_clash v S1 S2 wenzelm@14790: else if Sorts.sort_le classes (S1, S2) then wenzelm@17412: Vartab.update_new (w, (S2, T)) tye wenzelm@14790: else if Sorts.sort_le classes (S2, S1) then wenzelm@17412: Vartab.update_new (v, (S1, U)) tye wenzelm@2964: else wenzelm@14790: let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in wenzelm@17412: Vartab.update_new (v, (S1, S)) (Vartab.update_new (w, (S2, S)) tye) wenzelm@2964: end wenzelm@2964: | (TVar (v, S), T) => wenzelm@2964: if occurs v tye T then raise TUNIFY wenzelm@17412: else meet (T, S) (Vartab.update_new (v, (S, T)) tye) wenzelm@2964: | (T, TVar (v, S)) => wenzelm@2964: if occurs v tye T then raise TUNIFY wenzelm@17412: else meet (T, S) (Vartab.update_new (v, (S, T)) tye) wenzelm@2964: | (Type (a, Ts), Type (b, Us)) => wenzelm@2964: if a <> b then raise TUNIFY wenzelm@16885: else unifs (Ts, Us) tye wenzelm@16885: | (T, U) => if T = U then tye else raise TUNIFY) wenzelm@16885: and unifs (T :: Ts, U :: Us) tye = unifs (Ts, Us) (unif (T, U) tye) wenzelm@16885: | unifs _ tye = tye; wenzelm@16885: in (unif TU tyenv, ! tyvar_count) end; clasohm@0: wenzelm@16946: (*purely structural unification*) wenzelm@16946: fun raw_unify (ty1, ty2) tye = wenzelm@16946: (case (devar tye ty1, devar tye ty2) of wenzelm@16946: (T as TVar (v, S1), U as TVar (w, S2)) => wenzelm@16946: if eq_ix (v, w) then wenzelm@16946: if S1 = S2 then tye else tvar_clash v S1 S2 wenzelm@17412: else Vartab.update_new (w, (S2, T)) tye wenzelm@16946: | (TVar (v, S), T) => wenzelm@16946: if occurs v tye T then raise TUNIFY wenzelm@17412: else Vartab.update_new (v, (S, T)) tye wenzelm@16946: | (T, TVar (v, S)) => wenzelm@16946: if occurs v tye T then raise TUNIFY wenzelm@17412: else Vartab.update_new (v, (S, T)) tye wenzelm@16946: | (Type (a, Ts), Type (b, Us)) => wenzelm@16946: if a <> b then raise TUNIFY wenzelm@16946: else raw_unifys (Ts, Us) tye wenzelm@16946: | (T, U) => if T = U then tye else raise TUNIFY) wenzelm@16946: and raw_unifys (T :: Ts, U :: Us) tye = raw_unifys (Ts, Us) (raw_unify (T, U) tye) wenzelm@16946: | raw_unifys _ tye = tye; wenzelm@16946: wenzelm@17804: (*fast unification filter*) wenzelm@17804: fun could_unify (Type (a, Ts), Type (b, Us)) = a = b andalso could_unifys (Ts, Us) wenzelm@17804: | could_unify (TFree (a, _), TFree (b, _)) = a = b wenzelm@17804: | could_unify (TVar _, _) = true wenzelm@17804: | could_unify (_, TVar _) = true wenzelm@17804: | could_unify _ = false wenzelm@17804: and could_unifys (T :: Ts, U :: Us) = could_unify (T, U) andalso could_unifys (Ts, Us) wenzelm@17804: | could_unifys _ = true; wenzelm@450: wenzelm@17804: wenzelm@17804: (*equality with respect to a type environment*) berghofe@16650: fun eq_type tye (T, T') = wenzelm@16885: (case (devar tye T, devar tye T') of berghofe@16650: (Type (s, Ts), Type (s', Ts')) => berghofe@16650: s = s' andalso ListPair.all (eq_type tye) (Ts, Ts') berghofe@16650: | (U, U') => U = U'); berghofe@16650: wenzelm@450: clasohm@0: wenzelm@14790: (** extend and merge type signatures **) wenzelm@14790: wenzelm@14790: (* arities *) wenzelm@14790: wenzelm@14790: local nipkow@1435: wenzelm@14790: fun err_decl t decl = error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t); wenzelm@14830: skalberg@15531: fun for_classes _ NONE = "" skalberg@15531: | for_classes pp (SOME (c1, c2)) = wenzelm@14830: " for classes " ^ Pretty.string_of_classrel pp [c1, c2]; wenzelm@3790: wenzelm@14830: fun err_conflict pp t cc (c, Ss) (c', Ss') = wenzelm@14830: error ("Conflict of type arities" ^ for_classes pp cc ^ ":\n " ^ wenzelm@14830: Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n " ^ wenzelm@14830: Pretty.string_of_arity pp (t, Ss', [c'])); wenzelm@14790: wenzelm@14830: fun coregular pp C t (c, Ss) ars = wenzelm@3790: let wenzelm@14790: fun conflict (c', Ss') = wenzelm@14790: if Sorts.class_le C (c, c') andalso not (Sorts.sorts_le C (Ss, Ss')) then skalberg@15531: SOME ((c, c'), (c', Ss')) wenzelm@14790: else if Sorts.class_le C (c', c) andalso not (Sorts.sorts_le C (Ss', Ss)) then skalberg@15531: SOME ((c', c), (c', Ss')) skalberg@15531: else NONE; wenzelm@14790: in wenzelm@14790: (case Library.get_first conflict ars of skalberg@15531: SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss') skalberg@15531: | NONE => (c, Ss) :: ars) wenzelm@14790: end; wenzelm@3790: wenzelm@16340: fun insert pp C t (c, Ss) ars = wenzelm@17184: (case AList.lookup (op =) ars c of skalberg@15531: NONE => coregular pp C t (c, Ss) ars skalberg@15531: | SOME Ss' => wenzelm@14790: if Sorts.sorts_le C (Ss, Ss') then ars wenzelm@14790: else if Sorts.sorts_le C (Ss', Ss) wenzelm@14830: then coregular pp C t (c, Ss) (ars \ (c, Ss')) skalberg@15531: else err_conflict pp t NONE (c, Ss) (c, Ss')); wenzelm@2587: wenzelm@14790: fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]); wenzelm@3790: wenzelm@16340: fun insert_arities pp classes (t, ars) arities = wenzelm@14790: let val ars' = wenzelm@18957: Symtab.lookup_list arities t wenzelm@16340: |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars) wenzelm@17412: in Symtab.update (t, ars') arities end; wenzelm@3790: wenzelm@16444: fun insert_table pp classes = Symtab.fold (fn (t, ars) => wenzelm@16444: insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars)); wenzelm@14790: wenzelm@14790: in wenzelm@2587: wenzelm@16370: fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) => wenzelm@14790: let wenzelm@14790: fun prep (t, Ss, S) = wenzelm@17756: (case Symtab.lookup (snd types) t of skalberg@15531: SOME (LogicalType n, _) => wenzelm@14790: if length Ss = n then wenzelm@14790: (t, map (cert_sort tsig) Ss, cert_sort tsig S) wenzelm@14790: handle TYPE (msg, _, _) => error msg wenzelm@14790: else error (bad_nargs t) skalberg@15531: | SOME (decl, _) => err_decl t decl skalberg@15531: | NONE => error (undecl_type t)); wenzelm@4603: wenzelm@14790: val ars = decls |> map ((fn (t, Ss, S) => (t, map (fn c => (c, Ss)) S)) o prep); wenzelm@17756: val arities' = fold (insert_arities pp (snd classes)) ars arities; wenzelm@14790: in (classes, default, types, arities') end); wenzelm@12528: wenzelm@14830: fun rebuild_arities pp classes arities = wenzelm@16444: Symtab.empty wenzelm@16444: |> insert_table pp classes arities; wenzelm@14790: wenzelm@14830: fun merge_arities pp classes (arities1, arities2) = wenzelm@16444: Symtab.empty wenzelm@16444: |> insert_table pp classes arities1 wenzelm@16444: |> insert_table pp classes arities2; wenzelm@14790: wenzelm@14790: end; wenzelm@4603: wenzelm@4603: wenzelm@14790: (* classes *) wenzelm@14790: wenzelm@14790: local clasohm@0: wenzelm@14790: fun err_dup_classes cs = wenzelm@14790: error ("Duplicate declaration of class(es): " ^ commas_quote cs); wenzelm@14790: wenzelm@14830: fun err_cyclic_classes pp css = wenzelm@14790: error (cat_lines (map (fn cs => wenzelm@14830: "Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css)); wenzelm@14790: wenzelm@16370: fun add_class pp naming (c, cs) tsig = wenzelm@16370: tsig |> map_tsig (fn ((space, classes), default, types, arities) => wenzelm@16370: let wenzelm@16370: val c' = NameSpace.full naming c; wenzelm@16370: val cs' = map (cert_class tsig) cs wenzelm@16370: handle TYPE (msg, _, _) => error msg; wenzelm@16370: val space' = space |> NameSpace.declare naming c'; wenzelm@16370: val classes' = classes |> Graph.new_node (c', stamp ()) wenzelm@16370: handle Graph.DUP dup => err_dup_classes [dup]; wenzelm@16370: val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c') cs') wenzelm@16370: handle Graph.CYCLES css => err_cyclic_classes pp css; wenzelm@16370: in ((space', classes''), default, types, arities) end); wenzelm@2964: wenzelm@14790: in clasohm@0: wenzelm@16370: val add_classes = fold oo add_class; wenzelm@14790: wenzelm@16370: fun add_classrel pp ps tsig = wenzelm@16370: tsig |> map_tsig (fn ((space, classes), default, types, arities) => wenzelm@16370: let wenzelm@16370: val ps' = map (pairself (cert_class tsig)) ps wenzelm@16370: handle TYPE (msg, _, _) => error msg; wenzelm@16370: val classes' = classes |> fold Graph.add_edge_trans_acyclic ps' wenzelm@16370: handle Graph.CYCLES css => err_cyclic_classes pp css; wenzelm@16370: val default' = default |> Sorts.norm_sort classes'; wenzelm@16370: val arities' = arities |> rebuild_arities pp classes'; wenzelm@16370: in ((space, classes'), default', types, arities') end); wenzelm@16370: wenzelm@16370: fun merge_classes pp ((space1, classes1), (space2, classes2)) = wenzelm@14790: let wenzelm@16370: val space = NameSpace.merge (space1, space2); wenzelm@16370: val classes = wenzelm@16370: Graph.merge_trans_acyclic (op =) (classes1, classes2) wenzelm@16370: handle Graph.DUPS cs => err_dup_classes cs wenzelm@16370: | Graph.CYCLES css => err_cyclic_classes pp css; wenzelm@16946: in (space, classes) end; wenzelm@14790: wenzelm@14790: end; wenzelm@14790: wenzelm@16370: fun hide_classes fully cs = map_tsig (fn ((space, classes), default, types, arities) => wenzelm@16370: ((fold (NameSpace.hide fully) cs space, classes), default, types, arities)); wenzelm@16370: wenzelm@14790: wenzelm@14790: (* default sort *) wenzelm@14790: wenzelm@16370: fun set_defsort S tsig = tsig |> map_tsig (fn (classes, _, types, arities) => wenzelm@14790: (classes, cert_sort tsig S handle TYPE (msg, _, _) => error msg, types, arities)); clasohm@0: clasohm@0: wenzelm@14790: (* types *) wenzelm@14790: wenzelm@14790: local wenzelm@14790: wenzelm@14790: fun err_neg_args c = wenzelm@14790: error ("Negative number of arguments in type constructor declaration: " ^ quote c); nipkow@949: wenzelm@14790: fun err_in_decls c decl decl' = wenzelm@14906: let val s = str_of_decl decl and s' = str_of_decl decl' in wenzelm@14906: if s = s' then error ("Duplicate declaration of " ^ s ^ ": " ^ quote c) wenzelm@14830: else error ("Conflict of " ^ s ^ " with " ^ s' ^ ": " ^ quote c) wenzelm@14790: end; wenzelm@14790: wenzelm@16370: fun new_decl naming (c, decl) (space, types) = wenzelm@16370: let wenzelm@16370: val c' = NameSpace.full naming c; wenzelm@16370: val space' = NameSpace.declare naming c' space; wenzelm@16370: val types' = wenzelm@17412: (case Symtab.lookup types c' of wenzelm@16370: SOME (decl', _) => err_in_decls c' decl decl' wenzelm@17412: | NONE => Symtab.update (c', (decl, stamp ())) types); wenzelm@16370: in (space', types') end; wenzelm@14790: wenzelm@17412: fun the_decl (_, types) = fst o the o Symtab.lookup types; wenzelm@14790: wenzelm@16370: fun change_types f = map_tsig (fn (classes, default, types, arities) => wenzelm@14790: (classes, default, f types, arities)); wenzelm@2964: wenzelm@14989: fun syntactic types (Type (c, Ts)) = wenzelm@17412: (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false) wenzelm@14989: orelse exists (syntactic types) Ts wenzelm@14989: | syntactic _ _ = false; wenzelm@14989: wenzelm@16370: fun add_abbrev naming (a, vs, rhs) tsig = tsig |> change_types (fn types => wenzelm@14790: let wenzelm@14790: fun err msg = wenzelm@14906: error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a); wenzelm@16946: val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs)) wenzelm@14790: handle TYPE (msg, _, _) => err msg; wenzelm@14790: in wenzelm@18964: (case duplicates (op =) vs of wenzelm@14790: [] => [] wenzelm@14790: | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups)); wenzelm@14790: (case gen_rems (op =) (map (#1 o #1) (typ_tvars rhs'), vs) of wenzelm@14790: [] => [] wenzelm@14790: | extras => err ("Extra variables on rhs: " ^ commas_quote extras)); wenzelm@16370: types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) wenzelm@14790: end); clasohm@0: wenzelm@14790: in wenzelm@14790: wenzelm@16370: fun add_types naming ps = change_types (fold (new_decl naming) (ps |> map (fn (c, n) => wenzelm@14790: if n < 0 then err_neg_args c else (c, LogicalType n)))); wenzelm@14790: wenzelm@16370: val add_abbrevs = fold o add_abbrev; wenzelm@16370: wenzelm@16370: fun add_nonterminals naming = change_types o fold (new_decl naming) o map (rpair Nonterminal); wenzelm@14790: wenzelm@14790: fun merge_types (types1, types2) = haftmann@17496: NameSpace.merge_tables (Library.eq_snd (op =)) (types1, types2) handle Symtab.DUPS (d :: _) => wenzelm@14790: err_in_decls d (the_decl types1 d) (the_decl types2 d); wenzelm@14790: wenzelm@14790: end; clasohm@0: wenzelm@16370: fun hide_types fully cs = map_tsig (fn (classes, default, (space, types), arities) => wenzelm@16370: (classes, default, (fold (NameSpace.hide fully) cs space, types), arities)); wenzelm@16370: wenzelm@3790: wenzelm@14790: (* merge type signatures *) wenzelm@14790: wenzelm@14830: fun merge_tsigs pp (tsig1, tsig2) = wenzelm@14790: let wenzelm@14790: val (TSig {classes = classes1, default = default1, types = types1, arities = arities1, wenzelm@14790: log_types = _, witness = _}) = tsig1; wenzelm@14790: val (TSig {classes = classes2, default = default2, types = types2, arities = arities2, wenzelm@14790: log_types = _, witness = _}) = tsig2; wenzelm@14790: wenzelm@14830: val classes' = merge_classes pp (classes1, classes2); wenzelm@16370: val default' = Sorts.inter_sort (#2 classes') (default1, default2); wenzelm@14790: val types' = merge_types (types1, types2); wenzelm@16370: val arities' = merge_arities pp (#2 classes') (arities1, arities2); wenzelm@14790: in build_tsig (classes', default', types', arities') end; wenzelm@14790: clasohm@0: end;