added minimize_sort, complete_sort;
authorwenzelm
Wed Sep 26 20:50:34 2007 +0200 (2007-09-26)
changeset 2473208c2dd5378c7
parent 24731 c25aa6ae64ec
child 24733 59e0b49688fb
added minimize_sort, complete_sort;
src/Pure/sign.ML
src/Pure/sorts.ML
     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 *)
     2.1 --- a/src/Pure/sorts.ML	Wed Sep 26 20:50:33 2007 +0200
     2.2 +++ b/src/Pure/sorts.ML	Wed Sep 26 20:50:34 2007 +0200
     2.3 @@ -36,6 +36,8 @@
     2.4    val sort_le: algebra -> sort * sort -> bool
     2.5    val sorts_le: algebra -> sort list * sort list -> bool
     2.6    val inter_sort: algebra -> sort * sort -> sort
     2.7 +  val minimize_sort: algebra -> sort -> sort
     2.8 +  val complete_sort: algebra -> sort -> sort
     2.9    val certify_class: algebra -> class -> class    (*exception TYPE*)
    2.10    val certify_sort: algebra -> sort -> sort       (*exception TYPE*)
    2.11    val add_class: Pretty.pp -> class * class list -> algebra -> algebra
    2.12 @@ -160,14 +162,17 @@
    2.13    sort_strings (fold (inter_class algebra) S1 S2);
    2.14  
    2.15  
    2.16 -(* normal form *)
    2.17 +(* normal forms *)
    2.18  
    2.19 -fun norm_sort _ [] = []
    2.20 -  | norm_sort _ (S as [_]) = S
    2.21 -  | norm_sort algebra S =
    2.22 +fun minimize_sort _ [] = []
    2.23 +  | minimize_sort _ (S as [_]) = S
    2.24 +  | minimize_sort algebra S =
    2.25        filter (fn c => not (exists (fn c' => class_less algebra (c', c)) S)) S
    2.26        |> sort_distinct string_ord;
    2.27  
    2.28 +fun complete_sort algebra =
    2.29 +  Graph.all_succs (classes_of algebra) o minimize_sort algebra;
    2.30 +
    2.31  
    2.32  (* certify *)
    2.33  
    2.34 @@ -175,7 +180,7 @@
    2.35    if can (Graph.get_node (classes_of algebra)) c then c
    2.36    else raise TYPE ("Undeclared class: " ^ quote c, [], []);
    2.37  
    2.38 -fun certify_sort classes = norm_sort classes o map (certify_class classes);
    2.39 +fun certify_sort classes = minimize_sort classes o map (certify_class classes);
    2.40  
    2.41  
    2.42  
    2.43 @@ -286,7 +291,7 @@
    2.44  
    2.45  fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
    2.46    let
    2.47 -    val restrict_sort = norm_sort algebra o filter P o Graph.all_succs classes;
    2.48 +    val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
    2.49      fun restrict_arity tyco (c, (_, Ss)) =
    2.50        if P c then
    2.51          SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) (sargs (c, tyco))