# HG changeset patch # User wenzelm # Date 1146430208 -7200 # Node ID 1f0218dab84965ea9828d4ad0899d0e7733ab210 # Parent 77ff7cd602d7d76a7a88c5792540fdf00cd7ca3d moved certify_class/sort to type.ML; added operations to build sort algebras (from type.ML); tuned; diff -r 77ff7cd602d7 -r 1f0218dab849 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Sun Apr 30 22:50:07 2006 +0200 +++ b/src/Pure/sorts.ML Sun Apr 30 22:50:08 2006 +0200 @@ -2,12 +2,11 @@ ID: $Id$ Author: Markus Wenzel and Stefan Berghofer, TU Muenchen -Type classes and sorts. +The order-sorted algebra of type classes. *) signature SORTS = sig - (*operations on ordered lists*) val eq_set: sort list * sort list -> bool val union: sort list -> sort list -> sort list val subtract: sort list -> sort list -> sort list @@ -17,7 +16,6 @@ val insert_typs: typ list -> sort list -> sort list val insert_term: term -> sort list -> sort list val insert_terms: term list -> sort list -> sort list - (*signature information*) type classes type arities val class_eq: classes -> class * class -> bool @@ -28,18 +26,23 @@ val sorts_le: classes -> sort list * sort list -> bool val inter_sort: classes -> sort * sort -> sort val norm_sort: classes -> sort -> sort - val certify_class: classes -> class -> class - val certify_sort: classes -> sort -> sort val of_sort: classes * arities -> typ * sort -> bool exception DOMAIN of string * class val mg_domain: classes * arities -> string -> sort -> sort list (*exception DOMAIN*) val witness_sorts: classes * arities -> string list -> sort list -> sort list -> (typ * sort) list + val add_arities: Pretty.pp -> classes -> string * (class * sort list) list -> arities -> arities + val rebuild_arities: Pretty.pp -> classes -> arities -> arities + val merge_arities: Pretty.pp -> classes -> arities * arities -> arities + val add_class: Pretty.pp -> class * class list -> classes -> classes + val add_classrel: Pretty.pp -> class * class -> classes -> classes + val merge_classes: Pretty.pp -> classes * classes -> classes end; structure Sorts: SORTS = struct + (** type classes and sorts **) (* @@ -50,8 +53,6 @@ Sorts are intersections of finitely many classes. They are represented by lists of classes. Normal forms of sorts are sorted lists of minimal classes (wrt. current class inclusion). - - (types already defined in Pure/term.ML) *) @@ -130,19 +131,9 @@ | norm_sort classes S = sort_distinct string_ord (filter (minimal_class classes S) S); -(* certify *) - -fun certify_class classes c = - if can (Graph.get_node classes) c then c - else raise TYPE ("Undeclared class: " ^ quote c, [], []); -fun certify_sort classes = norm_sort classes o map (certify_class classes); - - +(** intersection -- preserving minimality **) -(** intersection **) - -(*intersect class with sort (preserves minimality)*) fun inter_class classes c S = let fun intr [] = [c] @@ -152,7 +143,6 @@ else c' :: intr c's in intr S end; -(*instersect sorts (preserves minimality)*) fun inter_sort classes (S1, S2) = sort_strings (fold (inter_class classes) S1 S2); @@ -252,4 +242,101 @@ end; + + +(** build sort algebras **) + +(* 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)); + +in + +fun add_class pp (c, cs) classes = + let + 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 classes'' end; + +fun add_classrel pp rel classes = + classes |> Graph.add_edge_trans_acyclic rel + handle Graph.CYCLES css => err_cyclic_classes pp css; + +fun merge_classes pp args : classes = + Graph.merge_trans_acyclic (op =) args + handle Graph.DUPS cs => err_dup_classes cs + | Graph.CYCLES css => err_cyclic_classes pp css; + end; + + +(* arities *) + +local + +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 class_le C (c, c') andalso not (sorts_le C (Ss, Ss')) then + SOME ((c, c'), (c', Ss')) + else if class_le C (c', c) andalso not (sorts_le C (Ss', Ss)) then + SOME ((c', c), (c', Ss')) + else NONE; + in + (case 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_le C (Ss, Ss') then ars + else if 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]); + +in + +fun add_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 add_arities_table pp classes = Symtab.fold (fn (t, ars) => + add_arities pp classes (t, map (apsnd (map (norm_sort classes))) ars)); + +fun rebuild_arities pp classes arities = + Symtab.empty + |> add_arities_table pp classes arities; + +fun merge_arities pp classes (arities1, arities2) = + Symtab.empty + |> add_arities_table pp classes arities1 + |> add_arities_table pp classes arities2; + +end; + +end;