# HG changeset patch
# User wenzelm
# Date 1224189872 -7200
# Node ID de573f2e53896e8a4dd663af2e3cb8f109435390
# Parent  1a0b845855aca3cb00cccceb2400768eb63e7902
added make, minimal_sorts;

diff -r 1a0b845855ac -r de573f2e5389 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Thu Oct 16 22:44:31 2008 +0200
+++ b/src/Pure/sorts.ML	Thu Oct 16 22:44:32 2008 +0200
@@ -15,6 +15,7 @@
 
 signature SORTS =
 sig
+  val make: sort list -> sort OrdList.T
   val subset: sort OrdList.T * sort OrdList.T -> bool
   val union: sort OrdList.T -> sort OrdList.T -> sort OrdList.T
   val subtract: sort OrdList.T -> sort OrdList.T -> sort OrdList.T
@@ -38,6 +39,7 @@
   val inter_sort: algebra -> sort * sort -> sort
   val minimize_sort: algebra -> sort -> sort
   val complete_sort: algebra -> sort -> sort
+  val minimal_sorts: algebra -> sort list -> sort OrdList.T
   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
@@ -68,6 +70,7 @@
 
 (** ordered lists of sorts **)
 
+val make = OrdList.make Term.sort_ord;
 val op subset = OrdList.subset Term.sort_ord;
 val op union = OrdList.union Term.sort_ord;
 val subtract = OrdList.subtract Term.sort_ord;
@@ -174,6 +177,12 @@
 fun complete_sort algebra =
   Graph.all_succs (classes_of algebra) o minimize_sort algebra;
 
+fun minimal_sorts algebra raw_sorts =
+  let
+    fun le S1 S2 = sort_le algebra (S1, S2);
+    val sorts = make (map (minimize_sort algebra) raw_sorts);
+  in sorts |> filter_out (fn S => exists (fn S' => le S' S andalso not (le S S')) sorts) end;
+
 
 (* certify *)