src/Pure/sorts.ML
author paulson
Fri May 30 15:14:59 1997 +0200 (1997-05-30)
changeset 3365 86c0d1988622
parent 2990 271062b8c461
child 3633 1884b433c6a5
permissions -rw-r--r--
flushOut ensures that no recent error message are lost (not certain this is
necessary)
     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 of_sort: classrel -> arities -> typ * sort -> bool
    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 (* mg_domain *)                 (*exception TYPE*)
   138 
   139 fun mg_dom arities a c =
   140   (case assoc2 (arities, (a, c)) of
   141     None => raise_type ("No way to get " ^ a ^ "::" ^ c ^ ".") [] []
   142   | Some Ss => Ss);
   143 
   144 fun mg_domain _ _ _ [] = sys_error "mg_domain"  (*don't know number of args!*)
   145   | mg_domain classrel arities a S =
   146       let val doms = map (mg_dom arities a) S in
   147         foldl (ListPair.map (inter_sort classrel)) (hd doms, tl doms)
   148       end;
   149 
   150 
   151 (* of_sort *)
   152 
   153 fun of_sort classrel arities =
   154   let
   155     fun ofS (_, []) = true
   156       | ofS (TFree (_, S), S') = sort_le classrel (S, S')
   157       | ofS (TVar (_, S), S') = sort_le classrel (S, S')
   158       | ofS (Type (a, Ts), S) =
   159           let val Ss = mg_domain classrel arities a S in
   160             ListPair.all ofS (Ts, Ss)
   161           end handle TYPE _ => false;
   162   in ofS end;
   163 
   164 
   165 
   166 (** nonempty_sort **)
   167 
   168 (* FIXME improve: proper sorts; non-base, non-ground types (vars from hyps) *)
   169 fun nonempty_sort classrel _ _ [] = true
   170   | nonempty_sort classrel arities hyps S =
   171       exists (exists (fn (c, Ss) => [c] = S andalso null Ss) o snd) arities
   172         orelse exists (fn S' => sort_le classrel (S', S)) hyps;
   173 
   174 end;