src/Pure/sorts.ML
author wenzelm
Thu Jul 08 18:31:04 1999 +0200 (1999-07-08)
changeset 6930 4b40fb299f9f
parent 3783 37fb4f64eb9d
child 7067 601f930d3739
permissions -rw-r--r--
improved error msgs of cterm_instantiate;
fixed incr_indexes;
     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 val str_of_sort = Syntax.simple_str_of_sort;
    69 fun str_of_classrel (c1, c2) = str_of_sort [c1] ^ " < " ^ str_of_sort [c2];
    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;