# HG changeset patch
# User wenzelm
# Date 1190832634 -7200
# Node ID 08c2dd5378c7a74f19d247c1193968dd723f091e
# Parent  c25aa6ae64ec409994e91ee9207f1742b3f5c8e7
added minimize_sort, complete_sort;

diff -r c25aa6ae64ec -r 08c2dd5378c7 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Sep 26 20:50:33 2007 +0200
+++ b/src/Pure/sign.ML	Wed Sep 26 20:50:34 2007 +0200
@@ -75,17 +75,19 @@
   val classes_of: theory -> Sorts.algebra
   val all_classes: theory -> class list
   val super_classes: theory -> class -> class list
+  val minimize_sort: theory -> sort -> sort
+  val complete_sort: theory -> sort -> sort
   val defaultS: theory -> sort
   val subsort: theory -> sort * sort -> bool
   val of_sort: theory -> typ * sort -> bool
   val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list
   val universal_witness: theory -> (typ * sort) option
   val all_sorts_nonempty: theory -> bool
+  val is_logtype: theory -> string -> bool
   val typ_instance: theory -> typ * typ -> bool
   val typ_equiv: theory -> typ * typ -> bool
   val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv
   val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int
-  val is_logtype: theory -> string -> bool
   val consts_of: theory -> Consts.T
   val const_constraint: theory -> string -> typ option
   val the_const_constraint: theory -> string -> typ
@@ -243,21 +245,26 @@
 (* type signature *)
 
 val tsig_of = #tsig o rep_sg;
+
 val classes_of = #2 o #classes o Type.rep_tsig o tsig_of;
 val all_classes = Sorts.all_classes o classes_of;
 val minimal_classes = Sorts.minimal_classes o classes_of;
 val super_classes = Sorts.super_classes o classes_of;
+val minimize_sort = Sorts.minimize_sort o classes_of;
+val complete_sort = Sorts.complete_sort o classes_of;
+
 val defaultS = Type.defaultS o tsig_of;
 val subsort = Type.subsort o tsig_of;
 val of_sort = Type.of_sort o tsig_of;
 val witness_sorts = Type.witness_sorts o tsig_of;
 val universal_witness = Type.universal_witness o tsig_of;
 val all_sorts_nonempty = is_some o universal_witness;
+val is_logtype = member (op =) o Type.logical_types o tsig_of;
+
 val typ_instance = Type.typ_instance o tsig_of;
 fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T);
 val typ_match = Type.typ_match o tsig_of;
 val typ_unify = Type.unify o tsig_of;
-val is_logtype = member (op =) o Type.logical_types o tsig_of;
 
 
 (* polymorphic constants *)
diff -r c25aa6ae64ec -r 08c2dd5378c7 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Wed Sep 26 20:50:33 2007 +0200
+++ b/src/Pure/sorts.ML	Wed Sep 26 20:50:34 2007 +0200
@@ -36,6 +36,8 @@
   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
@@ -160,14 +162,17 @@
   sort_strings (fold (inter_class algebra) S1 S2);
 
 
-(* normal form *)
+(* normal forms *)
 
-fun norm_sort _ [] = []
-  | norm_sort _ (S as [_]) = S
-  | norm_sort algebra S =
+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 *)
 
@@ -175,7 +180,7 @@
   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);
 
 
 
@@ -286,7 +291,7 @@
 
 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))