# HG changeset patch # User wenzelm # Date 1146430209 -7200 # Node ID 9f650083da65729483142627648ea35f158ac937 # Parent 1f0218dab84965ea9828d4ad0899d0e7733ab210 build classes/arities: refer to operations in sorts.ML; simplified add_class/classrel/arity; tuned; diff -r 1f0218dab849 -r 9f650083da65 src/Pure/type.ML --- a/src/Pure/type.ML Sun Apr 30 22:50:08 2006 +0200 +++ b/src/Pure/type.ML Sun Apr 30 22:50:09 2006 +0200 @@ -65,15 +65,15 @@ val eq_type: tyenv -> typ * typ -> bool (*extend and merge type signatures*) - val add_classes: Pretty.pp -> NameSpace.naming -> (bstring * class list) list -> tsig -> tsig + val add_class: Pretty.pp -> NameSpace.naming -> bstring * class list -> tsig -> tsig val hide_classes: bool -> string list -> tsig -> tsig - val add_classrel: Pretty.pp -> (class * class) list -> tsig -> tsig val set_defsort: sort -> tsig -> tsig val add_types: NameSpace.naming -> (bstring * int) list -> tsig -> tsig val add_abbrevs: NameSpace.naming -> (string * string list * typ) list -> tsig -> tsig val add_nonterminals: NameSpace.naming -> string list -> tsig -> tsig val hide_types: bool -> string list -> tsig -> tsig - val add_arities: Pretty.pp -> arity list -> tsig -> tsig + val add_arity: Pretty.pp -> arity -> tsig -> tsig + val add_classrel: Pretty.pp -> class * class -> tsig -> tsig val merge_tsigs: Pretty.pp -> tsig * tsig -> tsig end; @@ -140,8 +140,12 @@ fun of_sort (TSig {classes, arities, ...}) = Sorts.of_sort (#2 classes, arities); fun inter_sort (TSig {classes, ...}) = Sorts.inter_sort (#2 classes); -fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes); -fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes); +fun cert_class (TSig {classes, ...}) c = + if can (Graph.get_node (#2 classes)) c then c + else raise TYPE ("Undeclared class: " ^ quote c, [], []); + +fun cert_sort (tsig as TSig {classes, ...}) = + Sorts.norm_sort (#2 classes) o map (cert_class tsig); fun witness_sorts (tsig as TSig {classes, arities, log_types, ...}) = Sorts.witness_sorts (#2 classes, arities) log_types; @@ -160,7 +164,7 @@ fun certify_typ normalize syntax tsig ty = let - val TSig {classes = (_, classes), types = (_, types), ...} = tsig; + val TSig {types = (_, types), ...} = tsig; fun err msg = raise TYPE (msg, [ty], []); val check_syntax = @@ -181,11 +185,11 @@ | SOME (Nonterminal, _) => (nargs 0; check_syntax c; T) | NONE => err (undecl_type c)) end - | cert (TFree (x, S)) = TFree (x, Sorts.certify_sort classes S) + | cert (TFree (x, S)) = TFree (x, cert_sort tsig S) | cert (TVar (xi as (_, i), S)) = if i < 0 then err ("Malformed type variable: " ^ quote (Term.string_of_vname xi)) - else TVar (xi, Sorts.certify_sort classes S); + else TVar (xi, cert_sort tsig S); val ty' = cert ty; in if ty = ty' then ty else ty' end; (*avoid copying of already normal type*) @@ -463,96 +467,8 @@ (** extend and merge type signatures **) -(* arities *) - -local - -fun err_decl t decl = error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t); - -fun for_classes _ NONE = "" - | for_classes pp (SOME (c1, c2)) = - " for classes " ^ Pretty.string_of_classrel pp [c1, c2]; - -fun err_conflict pp t cc (c, Ss) (c', Ss') = - error ("Conflict of type arities" ^ for_classes pp cc ^ ":\n " ^ - Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n " ^ - Pretty.string_of_arity pp (t, Ss', [c'])); - -fun coregular pp C t (c, Ss) ars = - let - fun conflict (c', Ss') = - if Sorts.class_le C (c, c') andalso not (Sorts.sorts_le C (Ss, Ss')) then - SOME ((c, c'), (c', Ss')) - else if Sorts.class_le C (c', c) andalso not (Sorts.sorts_le C (Ss', Ss)) then - SOME ((c', c), (c', Ss')) - else NONE; - in - (case Library.get_first conflict ars of - SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss') - | NONE => (c, Ss) :: ars) - end; - -fun insert pp C t (c, Ss) ars = - (case AList.lookup (op =) ars c of - NONE => coregular pp C t (c, Ss) ars - | SOME Ss' => - if Sorts.sorts_le C (Ss, Ss') then ars - else if Sorts.sorts_le C (Ss', Ss) - then coregular pp C t (c, Ss) (remove (op =) (c, Ss') ars) - else err_conflict pp t NONE (c, Ss) (c, Ss')); - -fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]); - -fun insert_arities pp classes (t, ars) arities = - let val ars' = - Symtab.lookup_list arities t - |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars) - in Symtab.update (t, ars') arities end; - -fun insert_table pp classes = Symtab.fold (fn (t, ars) => - insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars)); - -in - -fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) => - let - fun prep (t, Ss, S) = - (case Symtab.lookup (snd types) t of - SOME (LogicalType n, _) => - if length Ss = n then - (t, map (cert_sort tsig) Ss, cert_sort tsig S) - handle TYPE (msg, _, _) => error msg - else error (bad_nargs t) - | SOME (decl, _) => err_decl t decl - | NONE => error (undecl_type t)); - - val ars = decls |> map ((fn (t, Ss, S) => (t, map (fn c => (c, Ss)) S)) o prep); - val arities' = fold (insert_arities pp (snd classes)) ars arities; - in (classes, default, types, arities') end); - -fun rebuild_arities pp classes arities = - Symtab.empty - |> insert_table pp classes arities; - -fun merge_arities pp classes (arities1, arities2) = - Symtab.empty - |> insert_table pp classes arities1 - |> insert_table pp classes arities2; - -end; - - (* classes *) -local - -fun err_dup_classes cs = - error ("Duplicate declaration of class(es): " ^ commas_quote cs); - -fun err_cyclic_classes pp css = - error (cat_lines (map (fn cs => - "Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css)); - fun add_class pp naming (c, cs) tsig = tsig |> map_tsig (fn ((space, classes), default, types, arities) => let @@ -560,42 +476,41 @@ val cs' = map (cert_class tsig) cs handle TYPE (msg, _, _) => error msg; val space' = space |> NameSpace.declare naming c'; - val classes' = classes |> Graph.new_node (c', stamp ()) - handle Graph.DUP dup => err_dup_classes [dup]; - val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c') cs') - handle Graph.CYCLES css => err_cyclic_classes pp css; - in ((space', classes''), default, types, arities) end); - -in - -val add_classes = fold oo add_class; - -fun add_classrel pp ps tsig = - tsig |> map_tsig (fn ((space, classes), default, types, arities) => - let - val ps' = map (pairself (cert_class tsig)) ps - handle TYPE (msg, _, _) => error msg; - val classes' = classes |> fold Graph.add_edge_trans_acyclic ps' - handle Graph.CYCLES css => err_cyclic_classes pp css; - val default' = default |> Sorts.norm_sort classes'; - val arities' = arities |> rebuild_arities pp classes'; - in ((space, classes'), default', types, arities') end); - -fun merge_classes pp ((space1, classes1), (space2, classes2)) = - let - val space = NameSpace.merge (space1, space2); - val classes = - Graph.merge_trans_acyclic (op =) (classes1, classes2) - handle Graph.DUPS cs => err_dup_classes cs - | Graph.CYCLES css => err_cyclic_classes pp css; - in (space, classes) end; - -end; + val classes' = classes |> Sorts.add_class pp (c', cs'); + in ((space', classes'), default, types, arities) end); fun hide_classes fully cs = map_tsig (fn ((space, classes), default, types, arities) => ((fold (NameSpace.hide fully) cs space, classes), default, types, arities)); +(* arities *) + +fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn (classes, default, types, arities) => + let + val _ = + (case Symtab.lookup (#2 types) t of + SOME (LogicalType n, _) => if length Ss <> n then error (bad_nargs t) else () + | SOME (decl, _) => error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t) + | NONE => error (undecl_type t)); + val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S) + handle TYPE (msg, _, _) => error msg; + val arities' = arities |> Sorts.add_arities pp (#2 classes) ((t, map (fn c' => (c', Ss')) S')); + in (classes, default, types, arities') end); + + +(* classrel *) + +fun add_classrel pp rel tsig = + tsig |> map_tsig (fn ((space, classes), default, types, arities) => + let + val rel' = pairself (cert_class tsig) rel + handle TYPE (msg, _, _) => error msg; + val classes' = classes |> Sorts.add_classrel pp rel; + val default' = default |> Sorts.norm_sort classes'; + val arities' = arities |> Sorts.rebuild_arities pp classes'; + in ((space, classes'), default', types, arities') end); + + (* default sort *) fun set_defsort S tsig = tsig |> map_tsig (fn (classes, _, types, arities) => @@ -673,15 +588,16 @@ fun merge_tsigs pp (tsig1, tsig2) = let - val (TSig {classes = classes1, default = default1, types = types1, arities = arities1, - log_types = _, witness = _}) = tsig1; - val (TSig {classes = classes2, default = default2, types = types2, arities = arities2, - log_types = _, witness = _}) = tsig2; + val (TSig {classes = (space1, classes1), default = default1, types = types1, + arities = arities1, log_types = _, witness = _}) = tsig1; + val (TSig {classes = (space2, classes2), default = default2, types = types2, + arities = arities2, log_types = _, witness = _}) = tsig2; - val classes' = merge_classes pp (classes1, classes2); - val default' = Sorts.inter_sort (#2 classes') (default1, default2); + val space' = NameSpace.merge (space1, space2); + val classes' = Sorts.merge_classes pp (classes1, classes2); + val default' = Sorts.inter_sort classes' (default1, default2); val types' = merge_types (types1, types2); - val arities' = merge_arities pp (#2 classes') (arities1, arities2); - in build_tsig (classes', default', types', arities') end; + val arities' = Sorts.merge_arities pp classes' (arities1, arities2); + in build_tsig ((space', classes'), default', types', arities') end; end;