# HG changeset patch
# User wenzelm
# Date 1145996604 -7200
# Node ID d13309e30aba21287a87525a8cae9e0be1f4ba4c
# Parent  6cb10eea48c37d14b8d0402ed056d345136c2609
added inter_sort;
added arity_number/sorts;

diff -r 6cb10eea48c3 -r d13309e30aba src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Apr 25 22:23:17 2006 +0200
+++ b/src/Pure/type.ML	Tue Apr 25 22:23:24 2006 +0200
@@ -29,12 +29,15 @@
   val eq_sort: tsig -> sort * sort -> bool
   val subsort: tsig -> sort * sort -> bool
   val of_sort: tsig -> typ * sort -> bool
+  val inter_sort: tsig -> sort * sort -> sort
   val cert_class: tsig -> class -> class
   val cert_sort: tsig -> sort -> sort
   val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
   val cert_typ: tsig -> typ -> typ
   val cert_typ_syntax: tsig -> typ -> typ
   val cert_typ_abbrev: tsig -> typ -> typ
+  val arity_number: tsig -> string -> int
+  val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
 
   (*special treatment of type vars*)
   val strip_sorts: typ -> typ
@@ -135,6 +138,7 @@
 fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq (#2 classes);
 fun subsort (TSig {classes, ...}) = Sorts.sort_le (#2 classes);
 fun of_sort (TSig {classes, arities, ...}) = Sorts.of_sort (#2 classes, arities);
+fun inter_sort (TSig {classes, ...}) = Sorts.inter_sort (#2 classes);
 
 fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes);
 fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes);
@@ -195,6 +199,19 @@
 end;
 
 
+(* type arities *)
+
+fun arity_number (TSig {types = (_, types), ...}) a =
+  (case Symtab.lookup types a of
+    SOME (LogicalType n, _) => n
+  | _ => error (undecl_type a));
+
+fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
+  | arity_sorts pp (TSig {classes, arities, ...}) a S =
+      Sorts.mg_domain (#2 classes, arities) a S handle Sorts.DOMAIN (a, c) =>
+        error ("No way to get " ^ Pretty.string_of_arity pp (a, [], [c]));
+
+
 
 (** special treatment of type vars **)