# HG changeset patch
# User wenzelm
# Date 1167409484 -3600
# Node ID 819ef284720b2dfacd7a55521942b51aee108a4b
# Parent  7d592dc078e37ace7d5344e432856eb8e5d1b8f8
classes: more direct way to achieve topological sorting;
renamed classes to all_classes;
added minimal_classes;
renamed project to subalgebra, tuned;

diff -r 7d592dc078e3 -r 819ef284720b src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Fri Dec 29 17:24:43 2006 +0100
+++ b/src/Pure/sorts.ML	Fri Dec 29 17:24:44 2006 +0100
@@ -28,7 +28,8 @@
   val rep_algebra: algebra ->
    {classes: serial Graph.T,
     arities: (class * (class * sort list)) list Symtab.table}
-  val classes: algebra -> class list
+  val all_classes: algebra -> class list
+  val minimal_classes: algebra -> class list
   val super_classes: algebra -> class -> class list
   val class_less: algebra -> class * class -> bool
   val class_le: algebra -> class * class -> bool
@@ -43,7 +44,7 @@
   val add_arities: Pretty.pp -> string * (class * sort list) list -> algebra -> algebra
   val empty_algebra: algebra
   val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
-  val project_algebra: Pretty.pp -> (class -> bool) -> algebra -> (sort -> sort) * algebra
+  val subalgebra: Pretty.pp -> (class -> bool) -> algebra -> (sort -> sort) * algebra
   type class_error
   val class_error: Pretty.pp -> class_error -> 'a
   exception CLASS_ERROR of class_error
@@ -120,8 +121,9 @@
 
 (* classes *)
 
-val classes = flat o rev o Graph.strong_conn o classes_of;
-  (*order allows for left-to-right traversal*)
+fun all_classes (Algebra {classes, ...}) = Graph.all_preds classes (Graph.maximals classes);
+
+val minimal_classes = Graph.minimals o classes_of;
 val super_classes = Graph.imm_succs o classes_of;
 
 
@@ -280,14 +282,17 @@
       |> add_arities_table pp algebra0 arities2;
   in make_algebra (classes', arities') end;
 
-fun project_algebra pp proj (algebra as Algebra {classes, arities}) =
+
+(* subalgebra *)
+
+fun subalgebra pp P (algebra as Algebra {classes, arities}) =
   let
-    val proj_sort = norm_sort algebra o filter proj o Graph.all_succs classes;
-    fun proj_arity (c, (_, Ss)) =
-      if proj c then SOME (c, (c, map proj_sort Ss)) else NONE;
-    val classes' = classes |> Graph.project proj;
-    val arities' = arities |> (Symtab.map o map_filter) proj_arity;
-  in (proj_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;
+    val restrict_sort = norm_sort algebra o filter P o Graph.all_succs classes;
+    fun restrict_arity (c, (_, Ss)) =
+      if P c then SOME (c, (c, map restrict_sort Ss)) else NONE;
+    val classes' = classes |> Graph.subgraph P;
+    val arities' = arities |> (Symtab.map o map_filter) restrict_arity;
+  in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;