--- a/src/HOL/HOL.thy Sun Feb 22 12:48:49 2009 -0800
+++ b/src/HOL/HOL.thy Mon Feb 23 06:51:26 2009 -0800
@@ -29,7 +29,7 @@
"~~/src/Tools/value.ML"
"~~/src/Tools/code/code_name.ML"
"~~/src/Tools/code/code_wellsorted.ML" (* formal dependency *)
- "~~/src/Tools/code/code_funcgr.ML"
+ (*"~~/src/Tools/code/code_funcgr.ML"*)
"~~/src/Tools/code/code_thingol.ML"
"~~/src/Tools/code/code_printer.ML"
"~~/src/Tools/code/code_target.ML"
--- a/src/Pure/sorts.ML Sun Feb 22 12:48:49 2009 -0800
+++ b/src/Pure/sorts.ML Mon Feb 23 06:51:26 2009 -0800
@@ -46,8 +46,6 @@
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 option)
-> algebra -> (sort -> sort) * algebra
type class_error
@@ -302,22 +300,6 @@
(* algebra projections *)
-val sorted_classes = rev o flat o Graph.strong_conn o classes_of;
-
-fun classrels_of algebra =
- map (fn c => (c, Graph.imm_succs (classes_of algebra) c)) (sorted_classes algebra);
-
-fun instances_of algebra =
- let
- val arities = arities_of algebra;
- val all_classes = sorted_classes algebra;
- fun sort_classes cs = filter (member (op = o apsnd fst) cs)
- all_classes;
- in
- Symtab.fold (fn (a, cs) => append ((map (pair a) o sort_classes) cs))
- arities []
- end;
-
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;
--- a/src/Tools/code/code_wellsorted.ML Sun Feb 22 12:48:49 2009 -0800
+++ b/src/Tools/code/code_wellsorted.ML Mon Feb 23 06:51:26 2009 -0800
@@ -210,29 +210,6 @@
(* applying instantiations *)
-fun build_algebra thy arities =
- let
- val pp = Syntax.pp_global thy;
- val thy_algebra = Sign.classes_of thy;
- val is_proper = can (AxClass.get_info thy);
- val classrels = Sorts.classrels_of thy_algebra
- |> filter (is_proper o fst)
- |> (map o apsnd) (filter is_proper);
- val instances = Sorts.instances_of thy_algebra
- |> filter (is_proper o snd)
- |> map swap (*FIXME*)
- fun add_class (class, superclasses) algebra =
- Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra;
- fun add_arity (class, tyco) algebra = case AList.lookup (op =) arities (class, tyco)
- of SOME sorts => Sorts.add_arities pp
- (tyco, [(class, map (Sorts.minimize_sort algebra) sorts)]) algebra
- | NONE => algebra;
- in
- Sorts.empty_algebra
- |> fold add_class classrels
- |> fold add_arity instances
- end;
-
fun dicts_of thy (proj_sort, algebra) (T, sort) =
let
fun class_relation (x, _) _ = x;
@@ -273,8 +250,10 @@
|> fold (assert_fun thy arities eqngr) cs
|> fold (assert_rhs thy arities eqngr) cs_rhss';
val arities' = fold (add_arity thy vardeps) insts arities;
- val algebra = build_algebra thy arities';
- val proj_sort = complete_proper_sort thy #> Sorts.minimize_sort algebra;
+ val pp = Syntax.pp_global thy;
+ val is_proper_class = can (AxClass.get_info thy);
+ val (proj_sort, algebra) = Sorts.subalgebra pp is_proper_class
+ (AList.lookup (op =) arities') (Sign.classes_of thy);
val (rhss, eqngr') = Symtab.fold
(add_eqs thy (proj_sort, algebra) vardeps) eqntab ([], eqngr);
fun deps_of (c, rhs) = c ::