added inter_sort;
authorwenzelm
Tue Apr 25 22:23:24 2006 +0200 (2006-04-25 ago)
changeset 19464d13309e30aba
parent 19463 6cb10eea48c3
child 19465 e6093a7fa53a
added inter_sort;
added arity_number/sorts;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Tue Apr 25 22:23:17 2006 +0200
     1.2 +++ b/src/Pure/type.ML	Tue Apr 25 22:23:24 2006 +0200
     1.3 @@ -29,12 +29,15 @@
     1.4    val eq_sort: tsig -> sort * sort -> bool
     1.5    val subsort: tsig -> sort * sort -> bool
     1.6    val of_sort: tsig -> typ * sort -> bool
     1.7 +  val inter_sort: tsig -> sort * sort -> sort
     1.8    val cert_class: tsig -> class -> class
     1.9    val cert_sort: tsig -> sort -> sort
    1.10    val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
    1.11    val cert_typ: tsig -> typ -> typ
    1.12    val cert_typ_syntax: tsig -> typ -> typ
    1.13    val cert_typ_abbrev: tsig -> typ -> typ
    1.14 +  val arity_number: tsig -> string -> int
    1.15 +  val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
    1.16  
    1.17    (*special treatment of type vars*)
    1.18    val strip_sorts: typ -> typ
    1.19 @@ -135,6 +138,7 @@
    1.20  fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq (#2 classes);
    1.21  fun subsort (TSig {classes, ...}) = Sorts.sort_le (#2 classes);
    1.22  fun of_sort (TSig {classes, arities, ...}) = Sorts.of_sort (#2 classes, arities);
    1.23 +fun inter_sort (TSig {classes, ...}) = Sorts.inter_sort (#2 classes);
    1.24  
    1.25  fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes);
    1.26  fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes);
    1.27 @@ -195,6 +199,19 @@
    1.28  end;
    1.29  
    1.30  
    1.31 +(* type arities *)
    1.32 +
    1.33 +fun arity_number (TSig {types = (_, types), ...}) a =
    1.34 +  (case Symtab.lookup types a of
    1.35 +    SOME (LogicalType n, _) => n
    1.36 +  | _ => error (undecl_type a));
    1.37 +
    1.38 +fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
    1.39 +  | arity_sorts pp (TSig {classes, arities, ...}) a S =
    1.40 +      Sorts.mg_domain (#2 classes, arities) a S handle Sorts.DOMAIN (a, c) =>
    1.41 +        error ("No way to get " ^ Pretty.string_of_arity pp (a, [], [c]));
    1.42 +
    1.43 +
    1.44  
    1.45  (** special treatment of type vars **)
    1.46