src/Pure/sign.ML
changeset 24732 08c2dd5378c7
parent 24707 dfeb98f84e93
child 24761 d762ab297a07
     1.1 --- a/src/Pure/sign.ML	Wed Sep 26 20:50:33 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed Sep 26 20:50:34 2007 +0200
     1.3 @@ -75,17 +75,19 @@
     1.4    val classes_of: theory -> Sorts.algebra
     1.5    val all_classes: theory -> class list
     1.6    val super_classes: theory -> class -> class list
     1.7 +  val minimize_sort: theory -> sort -> sort
     1.8 +  val complete_sort: theory -> sort -> sort
     1.9    val defaultS: theory -> sort
    1.10    val subsort: theory -> sort * sort -> bool
    1.11    val of_sort: theory -> typ * sort -> bool
    1.12    val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list
    1.13    val universal_witness: theory -> (typ * sort) option
    1.14    val all_sorts_nonempty: theory -> bool
    1.15 +  val is_logtype: theory -> string -> bool
    1.16    val typ_instance: theory -> typ * typ -> bool
    1.17    val typ_equiv: theory -> typ * typ -> bool
    1.18    val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv
    1.19    val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int
    1.20 -  val is_logtype: theory -> string -> bool
    1.21    val consts_of: theory -> Consts.T
    1.22    val const_constraint: theory -> string -> typ option
    1.23    val the_const_constraint: theory -> string -> typ
    1.24 @@ -243,21 +245,26 @@
    1.25  (* type signature *)
    1.26  
    1.27  val tsig_of = #tsig o rep_sg;
    1.28 +
    1.29  val classes_of = #2 o #classes o Type.rep_tsig o tsig_of;
    1.30  val all_classes = Sorts.all_classes o classes_of;
    1.31  val minimal_classes = Sorts.minimal_classes o classes_of;
    1.32  val super_classes = Sorts.super_classes o classes_of;
    1.33 +val minimize_sort = Sorts.minimize_sort o classes_of;
    1.34 +val complete_sort = Sorts.complete_sort o classes_of;
    1.35 +
    1.36  val defaultS = Type.defaultS o tsig_of;
    1.37  val subsort = Type.subsort o tsig_of;
    1.38  val of_sort = Type.of_sort o tsig_of;
    1.39  val witness_sorts = Type.witness_sorts o tsig_of;
    1.40  val universal_witness = Type.universal_witness o tsig_of;
    1.41  val all_sorts_nonempty = is_some o universal_witness;
    1.42 +val is_logtype = member (op =) o Type.logical_types o tsig_of;
    1.43 +
    1.44  val typ_instance = Type.typ_instance o tsig_of;
    1.45  fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T);
    1.46  val typ_match = Type.typ_match o tsig_of;
    1.47  val typ_unify = Type.unify o tsig_of;
    1.48 -val is_logtype = member (op =) o Type.logical_types o tsig_of;
    1.49  
    1.50  
    1.51  (* polymorphic constants *)