src/Pure/sorts.ML
author wenzelm
Wed Apr 16 18:14:43 1997 +0200 (1997-04-16)
changeset 2956 d128ae3e7421
child 2990 271062b8c461
permissions -rw-r--r--
Type classes and sorts (isolated from type.ML).
     1 (*  Title:      Pure/sorts.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     4 
     5 Type classes and sorts.
     6 *)
     7 
     8 signature SORTS =
     9 sig
    10   type classrel
    11   type arities
    12   val str_of_sort: sort -> string
    13   val str_of_arity: string * sort list * sort -> string
    14   val class_eq: classrel -> class * class -> bool
    15   val class_less: classrel -> class * class -> bool
    16   val class_le: classrel -> class * class -> bool
    17   val sort_eq: classrel -> sort * sort -> bool
    18   val sort_less: classrel -> sort * sort -> bool
    19   val sort_le: classrel -> sort * sort -> bool
    20   val sorts_le: classrel -> sort list * sort list -> bool
    21   val inter_class: classrel -> class * sort -> sort
    22   val inter_sort: classrel -> sort * sort -> sort
    23   val norm_sort: classrel -> sort -> sort
    24   val least_sort: classrel -> arities -> typ -> sort
    25   val mg_domain: classrel -> arities -> string -> sort -> sort list
    26   val nonempty_sort: classrel -> arities -> sort list -> sort -> bool
    27 end;
    28 
    29 structure Sorts: SORTS =
    30 struct
    31 
    32 
    33 (** type classes and sorts **)
    34 
    35 (*
    36   Classes denote (possibly empty) collections of types that are
    37   partially ordered by class inclusion. They are represented
    38   symbolically by strings.
    39 
    40   Sorts are intersections of finitely many classes. They are
    41   represented by lists of classes.  Normal forms of sorts are sorted
    42   lists of minimal classes (wrt. current class inclusion).
    43 
    44   (already defined in Pure/term.ML)
    45 *)
    46 
    47 
    48 (* sort signature information *)
    49 
    50 (*
    51   classrel:
    52     association list representing the proper subclass relation;
    53     pairs (c, cs) represent the superclasses cs of c;
    54 
    55   arities:
    56     two-fold association list of all type arities; (t, ars) means
    57     that type constructor t has the arities ars; an element (c, Ss) of
    58     ars represents the arity t::(Ss)c.
    59 *)
    60 
    61 type classrel = (class * class list) list;
    62 type arities = (string * (class * sort list) list) list;
    63 
    64 
    65 (* print sorts and arities *)
    66 
    67 fun str_of_sort [c] = c
    68   | str_of_sort cs = enclose "{" "}" (commas cs);
    69 
    70 fun str_of_dom Ss = enclose "(" ")" (commas (map str_of_sort Ss));
    71 
    72 fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
    73   | str_of_arity (t, Ss, S) =
    74       t ^ " :: " ^ str_of_dom Ss ^ " " ^ str_of_sort S;
    75 
    76 
    77 
    78 (** equality and inclusion **)
    79 
    80 (* classes *)
    81 
    82 fun class_eq _ (c1, c2:class) = c1 = c2;
    83 
    84 fun class_less classrel (c1, c2) =
    85   (case assoc (classrel, c1) of
    86      Some cs => c2 mem_string cs
    87    | None => false);
    88 
    89 fun class_le classrel (c1, c2) =
    90    c1 = c2 orelse class_less classrel (c1, c2);
    91 
    92 
    93 (* sorts *)
    94 
    95 fun sort_le classrel (S1, S2) =
    96   forall (fn c2 => exists  (fn c1 => class_le classrel (c1, c2)) S1) S2;
    97 
    98 fun sorts_le classrel (Ss1, Ss2) =
    99   ListPair.all (sort_le classrel) (Ss1, Ss2);
   100 
   101 fun sort_eq classrel (S1, S2) =
   102   sort_le classrel (S1, S2) andalso sort_le classrel (S2, S1);
   103 
   104 fun sort_less classrel (S1, S2) =
   105   sort_le classrel (S1, S2) andalso not (sort_le classrel (S2, S1));
   106 
   107 
   108 (* normal forms of sorts *)
   109 
   110 fun minimal_class classrel S c =
   111   not (exists (fn c' => class_less classrel (c', c)) S);
   112 
   113 fun norm_sort classrel S =
   114   sort_strings (distinct (filter (minimal_class classrel S) S));
   115 
   116 
   117 
   118 (** intersection **)
   119 
   120 (*intersect class with sort (preserves minimality)*)    (* FIXME tune? *)
   121 fun inter_class classrel (c, S) =
   122   let
   123     fun intr [] = [c]
   124       | intr (S' as c' :: c's) =
   125           if class_le classrel (c', c) then S'
   126           else if class_le classrel (c, c') then intr c's
   127           else c' :: intr c's
   128   in intr S end;
   129 
   130 (*instersect sorts (preserves minimality)*)
   131 fun inter_sort classrel = foldr (inter_class classrel);
   132 
   133 
   134 
   135 (** sorts of types **)
   136 
   137 (* least_sort *)
   138 
   139 fun least_sort classrel arities T =
   140   let
   141     fun match_dom Ss (c, Ss') =
   142       if sorts_le classrel (Ss, Ss') then Some c
   143       else None;
   144 
   145     fun leastS (Type (a, Ts)) =
   146           norm_sort classrel
   147             (mapfilter (match_dom (map leastS Ts)) (assocs arities a))
   148       | leastS (TFree (_, S)) = S
   149       | leastS (TVar (_, S)) = S
   150   in leastS T end;
   151 
   152 
   153 (* mg_domain *)                 (*exception TYPE*)
   154 
   155 fun mg_dom arities a c =
   156   (case assoc2 (arities, (a, c)) of
   157     None => raise_type ("No way to get " ^ a ^ "::" ^ c ^ ".") [] []
   158   | Some Ss => Ss);
   159 
   160 fun mg_domain _ _ _ [] = sys_error "mg_domain"  (*don't know number of args!*)
   161   | mg_domain classrel arities a S =
   162       let val doms = map (mg_dom arities a) S in
   163         foldl (ListPair.map (inter_sort classrel)) (hd doms, tl doms)
   164       end;
   165 
   166 
   167 
   168 (** nonempty_sort **)
   169 
   170 (* FIXME improve: proper sorts; non-base, non-ground types (vars from hyps) *)
   171 fun nonempty_sort classrel _ _ [] = true
   172   | nonempty_sort classrel arities hyps S =
   173       exists (exists (fn (c, Ss) => [c] = S andalso null Ss) o snd) arities
   174         orelse exists (fn S' => sort_le classrel (S', S)) hyps;
   175 
   176 end;