# HG changeset patch
# User haftmann
# Date 1228130220 -3600
# Node ID ac2c34cad840b953a4791ee36de0bafa5d725b02
# Parent  e60a41c217688b55c3b2fd91d4dc553be0468b59
more means for algebra projection

diff -r e60a41c21768 -r ac2c34cad840 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Mon Dec 01 12:16:59 2008 +0100
+++ b/src/Pure/sorts.ML	Mon Dec 01 12:17:00 2008 +0100
@@ -47,6 +47,8 @@
   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 classrels_of: algebra -> (class * class list) list
+  val instances_of: algebra -> (string * class) list
   val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list)
     -> algebra -> (sort -> sort) * algebra
   type class_error
@@ -299,7 +301,13 @@
   in make_algebra (classes', arities') end;
 
 
-(* subalgebra *)
+(* algebra projections *)
+
+fun classrels_of (Algebra {classes, ...}) =
+  map (fn [c] => (c, Graph.imm_succs classes c)) (rev (Graph.strong_conn classes));
+
+fun instances_of (Algebra {arities, ...}) =
+  Symtab.fold (fn (a, cs) => append (map (pair a o fst) cs)) arities [];
 
 fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
   let