src/Pure/sorts.ML
changeset 24732 08c2dd5378c7
parent 23655 d2d1138e0ddc
child 26326 a68045977f60
     1.1 --- a/src/Pure/sorts.ML	Wed Sep 26 20:50:33 2007 +0200
     1.2 +++ b/src/Pure/sorts.ML	Wed Sep 26 20:50:34 2007 +0200
     1.3 @@ -36,6 +36,8 @@
     1.4    val sort_le: algebra -> sort * sort -> bool
     1.5    val sorts_le: algebra -> sort list * sort list -> bool
     1.6    val inter_sort: algebra -> sort * sort -> sort
     1.7 +  val minimize_sort: algebra -> sort -> sort
     1.8 +  val complete_sort: algebra -> sort -> sort
     1.9    val certify_class: algebra -> class -> class    (*exception TYPE*)
    1.10    val certify_sort: algebra -> sort -> sort       (*exception TYPE*)
    1.11    val add_class: Pretty.pp -> class * class list -> algebra -> algebra
    1.12 @@ -160,14 +162,17 @@
    1.13    sort_strings (fold (inter_class algebra) S1 S2);
    1.14  
    1.15  
    1.16 -(* normal form *)
    1.17 +(* normal forms *)
    1.18  
    1.19 -fun norm_sort _ [] = []
    1.20 -  | norm_sort _ (S as [_]) = S
    1.21 -  | norm_sort algebra S =
    1.22 +fun minimize_sort _ [] = []
    1.23 +  | minimize_sort _ (S as [_]) = S
    1.24 +  | minimize_sort algebra S =
    1.25        filter (fn c => not (exists (fn c' => class_less algebra (c', c)) S)) S
    1.26        |> sort_distinct string_ord;
    1.27  
    1.28 +fun complete_sort algebra =
    1.29 +  Graph.all_succs (classes_of algebra) o minimize_sort algebra;
    1.30 +
    1.31  
    1.32  (* certify *)
    1.33  
    1.34 @@ -175,7 +180,7 @@
    1.35    if can (Graph.get_node (classes_of algebra)) c then c
    1.36    else raise TYPE ("Undeclared class: " ^ quote c, [], []);
    1.37  
    1.38 -fun certify_sort classes = norm_sort classes o map (certify_class classes);
    1.39 +fun certify_sort classes = minimize_sort classes o map (certify_class classes);
    1.40  
    1.41  
    1.42  
    1.43 @@ -286,7 +291,7 @@
    1.44  
    1.45  fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
    1.46    let
    1.47 -    val restrict_sort = norm_sort algebra o filter P o Graph.all_succs classes;
    1.48 +    val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
    1.49      fun restrict_arity tyco (c, (_, Ss)) =
    1.50        if P c then
    1.51          SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) (sargs (c, tyco))