sort instances wrt. to class hierarchy
authorhaftmann
Wed Feb 18 19:18:33 2009 +0100 (2009-02-18)
changeset 29972aee7610106fd
parent 29971 68331b62c873
child 29973 0b5a8957aff2
sort instances wrt. to class hierarchy
src/Pure/sorts.ML
src/Tools/code/code_funcgr_new.ML
     1.1 --- a/src/Pure/sorts.ML	Wed Feb 18 19:18:33 2009 +0100
     1.2 +++ b/src/Pure/sorts.ML	Wed Feb 18 19:18:33 2009 +0100
     1.3 @@ -302,11 +302,21 @@
     1.4  
     1.5  (* algebra projections *)
     1.6  
     1.7 -fun classrels_of (Algebra {classes, ...}) =
     1.8 -  map (fn [c] => (c, Graph.imm_succs classes c)) (rev (Graph.strong_conn classes));
     1.9 +val sorted_classes = rev o flat o Graph.strong_conn o classes_of;
    1.10 +
    1.11 +fun classrels_of algebra = 
    1.12 +  map (fn c => (c, Graph.imm_succs (classes_of algebra) c)) (sorted_classes algebra);
    1.13  
    1.14 -fun instances_of (Algebra {arities, ...}) =
    1.15 -  Symtab.fold (fn (a, cs) => append (map (pair a o fst) cs)) arities [];
    1.16 +fun instances_of algebra =
    1.17 +  let
    1.18 +    val arities = arities_of algebra;
    1.19 +    val all_classes = sorted_classes algebra;
    1.20 +    fun sort_classes cs = filter (member (op = o apsnd fst) cs)
    1.21 +      all_classes;
    1.22 +  in
    1.23 +    Symtab.fold (fn (a, cs) => append ((map (pair a) o sort_classes) cs))
    1.24 +      arities []
    1.25 +  end;
    1.26  
    1.27  fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
    1.28    let
     2.1 --- a/src/Tools/code/code_funcgr_new.ML	Wed Feb 18 19:18:33 2009 +0100
     2.2 +++ b/src/Tools/code/code_funcgr_new.ML	Wed Feb 18 19:18:33 2009 +0100
     2.3 @@ -205,16 +205,6 @@
     2.4         handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
     2.5    end;
     2.6  
     2.7 -fun instances_of (*FIXME move to sorts.ML*) algebra =
     2.8 -  let
     2.9 -    val { classes, arities } = Sorts.rep_algebra algebra;
    2.10 -    val sort_classes = fn cs => filter (member (op = o apsnd fst) cs)
    2.11 -      (flat (rev (Graph.strong_conn classes)));
    2.12 -  in
    2.13 -    Symtab.fold (fn (a, cs) => append ((map (pair a) o sort_classes) cs))
    2.14 -      arities []
    2.15 -  end;
    2.16 -
    2.17  fun algebra_of thy vardeps =
    2.18    let
    2.19      val pp = Syntax.pp_global thy;
    2.20 @@ -223,7 +213,7 @@
    2.21      val classrels = Sorts.classrels_of thy_algebra
    2.22        |> filter (is_proper o fst)
    2.23        |> (map o apsnd) (filter is_proper);
    2.24 -    val instances = instances_of thy_algebra
    2.25 +    val instances = Sorts.instances_of thy_algebra
    2.26        |> filter (is_proper o snd);
    2.27      fun add_class (class, superclasses) algebra =
    2.28        Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra;