removed least_sort;
authorwenzelm
Fri Apr 18 11:57:51 1997 +0200 (1997-04-18)
changeset 2990271062b8c461
parent 2989 8189a4870d19
child 2991 d9f6299dbf9f
removed least_sort;
added of_sort;
src/Pure/sorts.ML
     1.1 --- a/src/Pure/sorts.ML	Fri Apr 18 11:55:14 1997 +0200
     1.2 +++ b/src/Pure/sorts.ML	Fri Apr 18 11:57:51 1997 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    val inter_class: classrel -> class * sort -> sort
     1.5    val inter_sort: classrel -> sort * sort -> sort
     1.6    val norm_sort: classrel -> sort -> sort
     1.7 -  val least_sort: classrel -> arities -> typ -> sort
     1.8 +  val of_sort: classrel -> arities -> typ * sort -> bool
     1.9    val mg_domain: classrel -> arities -> string -> sort -> sort list
    1.10    val nonempty_sort: classrel -> arities -> sort list -> sort -> bool
    1.11  end;
    1.12 @@ -134,22 +134,6 @@
    1.13  
    1.14  (** sorts of types **)
    1.15  
    1.16 -(* least_sort *)
    1.17 -
    1.18 -fun least_sort classrel arities T =
    1.19 -  let
    1.20 -    fun match_dom Ss (c, Ss') =
    1.21 -      if sorts_le classrel (Ss, Ss') then Some c
    1.22 -      else None;
    1.23 -
    1.24 -    fun leastS (Type (a, Ts)) =
    1.25 -          norm_sort classrel
    1.26 -            (mapfilter (match_dom (map leastS Ts)) (assocs arities a))
    1.27 -      | leastS (TFree (_, S)) = S
    1.28 -      | leastS (TVar (_, S)) = S
    1.29 -  in leastS T end;
    1.30 -
    1.31 -
    1.32  (* mg_domain *)                 (*exception TYPE*)
    1.33  
    1.34  fun mg_dom arities a c =
    1.35 @@ -164,6 +148,20 @@
    1.36        end;
    1.37  
    1.38  
    1.39 +(* of_sort *)
    1.40 +
    1.41 +fun of_sort classrel arities =
    1.42 +  let
    1.43 +    fun ofS (_, []) = true
    1.44 +      | ofS (TFree (_, S), S') = sort_le classrel (S, S')
    1.45 +      | ofS (TVar (_, S), S') = sort_le classrel (S, S')
    1.46 +      | ofS (Type (a, Ts), S) =
    1.47 +          let val Ss = mg_domain classrel arities a S in
    1.48 +            ListPair.all ofS (Ts, Ss)
    1.49 +          end handle TYPE _ => false;
    1.50 +  in ofS end;
    1.51 +
    1.52 +
    1.53  
    1.54  (** nonempty_sort **)
    1.55