# HG changeset patch
# User haftmann
# Date 1151395788 -7200
# Node ID eaf2c25654d3cd9cf80fb8d99731c272aa704596
# Parent  d58e2c564100e7c37daab78990b95866ff5596ca
added class projection

diff -r d58e2c564100 -r eaf2c25654d3 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Tue Jun 27 10:09:44 2006 +0200
+++ b/src/Pure/sorts.ML	Tue Jun 27 10:09:48 2006 +0200
@@ -43,6 +43,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 -> algebra
   type class_error
   val class_error: Pretty.pp -> class_error -> 'a
   exception CLASS_ERROR of class_error
@@ -278,6 +279,23 @@
       |> add_arities_table pp algebra0 arities2;
   in make_algebra (classes', arities') end;
 
+fun project_algebra pp proj (Algebra {classes, arities}) =
+  let
+    fun proj_sort S =
+      maps (fn c => if proj c then [c]
+        else proj_sort (Graph.imm_succs classes c)) S;
+  in
+    make_algebra (
+      classes
+      |> Graph.project proj,
+      arities
+      |> (Symtab.map o map_filter) (fn (c, (c0, Ss)) =>
+          if proj c
+          then SOME (c, (c, map proj_sort Ss))
+          else NONE)
+    ) |> rebuild_arities pp
+  end;
+
 
 
 (** sorts of types **)
@@ -330,7 +348,8 @@
 fun of_sort_derivation pp algebra {classrel, constructor, variable} =
   let
     val {classes, arities} = rep_algebra algebra;
-    fun weaken_path (x, c1 :: c2 :: cs) = weaken_path (classrel (x, c1) c2, c2 :: cs)
+    fun weaken_path (x, c1 :: c2 :: cs) =
+          weaken_path (classrel (x, c1) c2, c2 :: cs)
       | weaken_path (x, _) = x;
     fun weaken (x, c1) c2 =
       (case Graph.irreducible_paths classes (c1, c2) of