--- a/src/Pure/sorts.ML Wed Mar 04 10:43:39 2009 +0100
+++ b/src/Pure/sorts.ML Wed Mar 04 10:45:52 2009 +0100
@@ -46,9 +46,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 classrels_of: algebra -> (class * class list) list
- val instances_of: algebra -> (string * class) list
- val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list)
+ val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list option)
-> algebra -> (sort -> sort) * algebra
type class_error
val class_error: Pretty.pp -> class_error -> string
@@ -302,19 +300,14 @@
(* 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
val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
fun restrict_arity tyco (c, (_, Ss)) =
- if P c then
- SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) (sargs (c, tyco))
+ if P c then case sargs (c, tyco)
+ of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts
|> map restrict_sort))
+ | NONE => NONE
else NONE;
val classes' = classes |> Graph.subgraph P;
val arities' = arities |> Symtab.map' (map_filter o restrict_arity);