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