src/Pure/sorts.ML

   val class_le: algebra -> class * class -> bool
   val sort_eq: algebra -> sort * sort -> bool
   val sort_le: algebra -> sort * sort -> bool
   val sorts_le: algebra -> sort list * sort list -> bool
   val inter_sort: algebra -> sort * sort -> sort
+  val minimize_sort: algebra -> sort -> sort
+  val complete_sort: algebra -> sort -> sort
   val certify_class: algebra -> class -> class    (*exception TYPE*)
   val certify_sort: algebra -> sort -> sort       (*exception TYPE*)
   val add_class: Pretty.pp -> class * class list -> algebra -> algebra
   val add_classrel: Pretty.pp -> class * class -> algebra -> algebra
   val add_arities: Pretty.pp -> string * (class * sort list) list -> algebra -> algebra

 
 fun inter_sort algebra (S1, S2) =
   sort_strings (fold (inter_class algebra) S1 S2);
 
 
-(* normal form *)
-
-fun norm_sort _ [] = []
-  | norm_sort _ (S as [_]) = S
-  | norm_sort algebra S =
+(* normal forms *)
+
+fun minimize_sort _ [] = []
+  | minimize_sort _ (S as [_]) = S
+  | minimize_sort algebra S =
       filter (fn c => not (exists (fn c' => class_less algebra (c', c)) S)) S
       |> sort_distinct string_ord;
+
+fun complete_sort algebra =
+  Graph.all_succs (classes_of algebra) o minimize_sort algebra;
 
 
 (* certify *)
 
 fun certify_class algebra c =
   if can (Graph.get_node (classes_of algebra)) c then c
   else raise TYPE ("Undeclared class: " ^ quote c, [], []);
 
-fun certify_sort classes = norm_sort classes o map (certify_class classes);
+fun certify_sort classes = minimize_sort classes o map (certify_class classes);
 
 
 
 (** build algebras **)
 

 
 (* subalgebra *)
 
 fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
   let
-    val restrict_sort = norm_sort algebra o filter P o Graph.all_succs classes;
+    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))
           |> map restrict_sort))
       else NONE;