src/Pure/sorts.ML
author berghofe
Wed Oct 31 19:37:04 2001 +0100 (2001-10-31)
changeset 11998 b14e7686ce84
parent 9281 a48818595670
child 14782 d6ce35a1c386
permissions -rw-r--r--
- enter_thmx -> enter_thms
- improved naming of theorems: enter_thms now takes functions pre_name and post_name
as arguments
     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   exception DOMAIN of string * class
    27   val mg_domain: classrel * arities -> string -> sort -> sort list
    28   val witness_sorts: classrel * arities * string list
    29     -> sort list -> sort list -> (typ * sort) list
    30 end;
    31 
    32 structure Sorts: SORTS =
    33 struct
    34 
    35 
    36 (** type classes and sorts **)
    37 
    38 (*
    39   Classes denote (possibly empty) collections of types that are
    40   partially ordered by class inclusion. They are represented
    41   symbolically by strings.
    42 
    43   Sorts are intersections of finitely many classes. They are
    44   represented by lists of classes.  Normal forms of sorts are sorted
    45   lists of minimal classes (wrt. current class inclusion).
    46 
    47   (already defined in Pure/term.ML)
    48 *)
    49 
    50 
    51 (* sort signature information *)
    52 
    53 (*
    54   classrel:
    55     table representing the proper subclass relation; entries (c, cs)
    56     represent the superclasses cs of c;
    57 
    58   arities:
    59     table of association lists of all type arities; (t, ars) means
    60     that type constructor t has the arities ars; an element (c, Ss) of
    61     ars represents the arity t::(Ss)c;
    62 *)
    63 
    64 type classrel = (class list) Symtab.table;
    65 type arities = ((class * sort list) list) Symtab.table;
    66 
    67 
    68 (* print sorts and arities *)
    69 
    70 val str_of_sort = Syntax.simple_str_of_sort;
    71 fun str_of_classrel (c1, c2) = str_of_sort [c1] ^ " < " ^ str_of_sort [c2];
    72 fun str_of_dom Ss = enclose "(" ")" (commas (map str_of_sort Ss));
    73 
    74 fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
    75   | str_of_arity (t, Ss, S) =
    76       t ^ " :: " ^ str_of_dom Ss ^ " " ^ str_of_sort S;
    77 
    78 
    79 
    80 (** equality and inclusion **)
    81 
    82 (* classes *)
    83 
    84 fun class_eq _ (c1, c2:class) = c1 = c2;
    85 
    86 fun class_less classrel (c1, c2) =
    87   (case Symtab.lookup (classrel, c1) of
    88      Some cs => c2 mem_string cs
    89    | None => false);
    90 
    91 fun class_le classrel (c1, c2) =
    92    c1 = c2 orelse class_less classrel (c1, c2);
    93 
    94 
    95 (* sorts *)
    96 
    97 fun sort_le classrel (S1, S2) =
    98   forall (fn c2 => exists  (fn c1 => class_le classrel (c1, c2)) S1) S2;
    99 
   100 fun sorts_le classrel (Ss1, Ss2) =
   101   ListPair.all (sort_le classrel) (Ss1, Ss2);
   102 
   103 fun sort_eq classrel (S1, S2) =
   104   sort_le classrel (S1, S2) andalso sort_le classrel (S2, S1);
   105 
   106 fun sort_less classrel (S1, S2) =
   107   sort_le classrel (S1, S2) andalso not (sort_le classrel (S2, S1));
   108 
   109 
   110 (* normal forms of sorts *)
   111 
   112 fun minimal_class classrel S c =
   113   not (exists (fn c' => class_less classrel (c', c)) S);
   114 
   115 fun norm_sort classrel S =
   116   sort_strings (distinct (filter (minimal_class classrel S) S));
   117 
   118 
   119 
   120 (** intersection **)
   121 
   122 (*intersect class with sort (preserves minimality)*)
   123 fun inter_class classrel (c, S) =
   124   let
   125     fun intr [] = [c]
   126       | intr (S' as c' :: c's) =
   127           if class_le classrel (c', c) then S'
   128           else if class_le classrel (c, c') then intr c's
   129           else c' :: intr c's
   130   in intr S end;
   131 
   132 (*instersect sorts (preserves minimality)*)
   133 fun inter_sort classrel = sort_strings o foldr (inter_class classrel);
   134 
   135 
   136 
   137 (** sorts of types **)
   138 
   139 (* mg_domain *)
   140 
   141 exception DOMAIN of string * class;
   142 
   143 fun mg_dom arities a c =
   144   (case Symtab.lookup (arities, a) of
   145     None => raise DOMAIN (a, c)
   146   | Some ars => (case assoc (ars, c) of None => raise DOMAIN (a, c) | Some Ss => Ss));
   147 
   148 fun mg_domain _ _ [] = sys_error "mg_domain"  (*don't know number of args!*)
   149   | mg_domain (classrel, arities) a S =
   150       let val doms = map (mg_dom arities a) S in
   151         foldl (ListPair.map (inter_sort classrel)) (hd doms, tl doms)
   152       end;
   153 
   154 
   155 (* of_sort *)
   156 
   157 fun of_sort (classrel, arities) =
   158   let
   159     fun ofS (_, []) = true
   160       | ofS (TFree (_, S), S') = sort_le classrel (S, S')
   161       | ofS (TVar (_, S), S') = sort_le classrel (S, S')
   162       | ofS (Type (a, Ts), S) =
   163           let val Ss = mg_domain (classrel, arities) a S in
   164             ListPair.all ofS (Ts, Ss)
   165           end handle DOMAIN _ => false;
   166   in ofS end;
   167 
   168 
   169 
   170 (** witness_sorts **)
   171 
   172 fun witness_sorts_aux (classrel, arities, log_types) hyps sorts =
   173   let
   174     val top_witn = (propT, []);
   175     fun le S1 S2 = sort_le classrel (S1, S2);
   176     fun get_solved S2 (T, S1) = if le S1 S2 then Some (T, S2) else None;
   177     fun get_hyp S2 S1 = if le S1 S2 then Some (TFree ("'hyp", S1), S2) else None;
   178     fun mg_dom t S = Some (mg_domain (classrel, arities) t S) handle DOMAIN _ => None;
   179 
   180     fun witn_sort _ (solved_failed, []) = (solved_failed, Some top_witn)
   181       | witn_sort path ((solved, failed), S) =
   182           if exists (le S) failed then ((solved, failed), None)
   183           else
   184             (case get_first (get_solved S) solved of
   185               Some w => ((solved, failed), Some w)
   186             | None =>
   187                 (case get_first (get_hyp S) hyps of
   188                   Some w => ((w :: solved, failed), Some w)
   189                 | None => witn_types path log_types ((solved, failed), S)))
   190 
   191     and witn_sorts path x = foldl_map (witn_sort path) x
   192 
   193     and witn_types _ [] ((solved, failed), S) = ((solved, S :: failed), None)
   194       | witn_types path (t :: ts) (solved_failed, S) =
   195           (case mg_dom t S of
   196             Some SS =>
   197               (*do not descend into stronger args (achieving termination)*)
   198               if exists (fn D => le D S orelse exists (le D) path) SS then
   199                 witn_types path ts (solved_failed, S)
   200               else
   201                 let val ((solved', failed'), ws) = witn_sorts (S :: path) (solved_failed, SS) in
   202                   if forall is_some ws then
   203                     let val w = (Type (t, map (#1 o the) ws), S)
   204                     in ((w :: solved', failed'), Some w) end
   205                   else witn_types path ts ((solved', failed'), S)
   206                 end
   207           | None => witn_types path ts (solved_failed, S));
   208 
   209   in witn_sorts [] (([], []), sorts) end;
   210 
   211 
   212 fun witness_sorts (classrel, arities, log_types) hyps sorts =
   213   let
   214     fun check_result None = None
   215       | check_result (Some (T, S)) =
   216           if of_sort (classrel, arities) (T, S) then Some (T, S)
   217           else (warning ("witness_sorts: rejected bad witness for " ^ str_of_sort S); None);
   218   in mapfilter check_result (#2 (witness_sorts_aux (classrel, arities, log_types) hyps sorts)) end;
   219 
   220 
   221 end;