src/Pure/sorts.ML
author haftmann
Sun Aug 28 09:36:18 2005 +0200 (2005-08-28)
changeset 17155 e904580c3ee0
parent 16881 570592642670
child 17184 3d80209e9a53
permissions -rw-r--r--
added superclasses, class_le_path
     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   (*operations on ordered lists*)
    11   val eq_set: sort list * sort list -> bool
    12   val union: sort list -> sort list -> sort list
    13   val subtract: sort list -> sort list -> sort list
    14   val insert_sort: sort -> sort list -> sort list
    15   val insert_typ: typ -> sort list -> sort list
    16   val insert_typs: typ list -> sort list -> sort list
    17   val insert_term: term -> sort list -> sort list
    18   val insert_terms: term list -> sort list -> sort list
    19   (*signature information*)
    20   type classes
    21   type arities
    22   val class_eq: classes -> class * class -> bool
    23   val class_less: classes -> class * class -> bool
    24   val class_le: classes -> class * class -> bool
    25   val class_le_path: classes -> class * class -> class list option
    26   val superclasses: classes -> class -> class list
    27   val sort_eq: classes -> sort * sort -> bool
    28   val sort_less: classes -> sort * sort -> bool
    29   val sort_le: classes -> sort * sort -> bool
    30   val sorts_le: classes -> sort list * sort list -> bool
    31   val inter_sort: classes -> sort * sort -> sort
    32   val norm_sort: classes -> sort -> sort
    33   val certify_class: classes -> class -> class
    34   val certify_sort: classes -> sort -> sort
    35   val of_sort: classes * arities -> typ * sort -> bool
    36   exception DOMAIN of string * class
    37   val mg_domain: classes * arities -> string -> sort -> sort list  (*exception DOMAIN*)
    38   val witness_sorts: classes * arities -> string list ->
    39     sort list -> sort list -> (typ * sort) list
    40 end;
    41 
    42 structure Sorts: SORTS =
    43 struct
    44 
    45 (** type classes and sorts **)
    46 
    47 (*
    48   Classes denote (possibly empty) collections of types that are
    49   partially ordered by class inclusion. They are represented
    50   symbolically by strings.
    51 
    52   Sorts are intersections of finitely many classes. They are
    53   represented by lists of classes.  Normal forms of sorts are sorted
    54   lists of minimal classes (wrt. current class inclusion).
    55 
    56   (types already defined in Pure/term.ML)
    57 *)
    58 
    59 
    60 (* ordered lists of sorts *)
    61 
    62 val eq_set = OrdList.eq_set Term.sort_ord;
    63 val op union = OrdList.union Term.sort_ord;
    64 val subtract = OrdList.subtract Term.sort_ord;
    65 
    66 val insert_sort = OrdList.insert Term.sort_ord;
    67 
    68 fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss
    69   | insert_typ (TVar (_, S)) Ss = insert_sort S Ss
    70   | insert_typ (Type (_, Ts)) Ss = insert_typs Ts Ss
    71 and insert_typs [] Ss = Ss
    72   | insert_typs (T :: Ts) Ss = insert_typs Ts (insert_typ T Ss);
    73 
    74 fun insert_term (Const (_, T)) Ss = insert_typ T Ss
    75   | insert_term (Free (_, T)) Ss = insert_typ T Ss
    76   | insert_term (Var (_, T)) Ss = insert_typ T Ss
    77   | insert_term (Bound _) Ss = Ss
    78   | insert_term (Abs (_, T, t)) Ss = insert_term t (insert_typ T Ss)
    79   | insert_term (t $ u) Ss = insert_term t (insert_term u Ss);
    80 
    81 fun insert_terms [] Ss = Ss
    82   | insert_terms (t :: ts) Ss = insert_terms ts (insert_term t Ss);
    83 
    84 
    85 (* sort signature information *)
    86 
    87 (*
    88   classes: graph representing class declarations together with proper
    89     subclass relation, which needs to be transitive and acyclic.
    90 
    91   arities: table of association lists of all type arities; (t, ars)
    92     means that type constructor t has the arities ars; an element (c,
    93     Ss) of ars represents the arity t::(Ss)c.  "Coregularity" of the
    94     arities structure requires that for any two declarations
    95     t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2 holds Ss1 <= Ss2.
    96 *)
    97 
    98 type classes = stamp Graph.T;
    99 type arities = (class * sort list) list Symtab.table;
   100 
   101 
   102 
   103 (** equality and inclusion **)
   104 
   105 (* classes *)
   106 
   107 fun class_eq (_: classes) (c1, c2:class) = c1 = c2;
   108 val class_less: classes -> class * class -> bool = Graph.is_edge;
   109 fun class_le classes (c1, c2) = c1 = c2 orelse class_less classes (c1, c2);
   110 
   111 fun class_le_path classes (subclass, superclass) =
   112   if class_eq classes (subclass, superclass)
   113   then SOME [subclass]
   114   else case Graph.find_paths classes (subclass, superclass)
   115     of [] => NONE
   116      | (p::_) => SOME p
   117 
   118 val superclasses = Graph.imm_succs
   119 
   120 
   121 (* sorts *)
   122 
   123 fun sort_le classes (S1, S2) =
   124   forall (fn c2 => exists (fn c1 => class_le classes (c1, c2)) S1) S2;
   125 
   126 fun sorts_le classes (Ss1, Ss2) =
   127   ListPair.all (sort_le classes) (Ss1, Ss2);
   128 
   129 fun sort_eq classes (S1, S2) =
   130   sort_le classes (S1, S2) andalso sort_le classes (S2, S1);
   131 
   132 fun sort_less classes (S1, S2) =
   133   sort_le classes (S1, S2) andalso not (sort_le classes (S2, S1));
   134 
   135 
   136 (* normal forms of sorts *)
   137 
   138 fun minimal_class classes S c =
   139   not (exists (fn c' => class_less classes (c', c)) S);
   140 
   141 fun norm_sort _ [] = []
   142   | norm_sort _ (S as [_]) = S
   143   | norm_sort classes S = unique_strings (sort_strings (filter (minimal_class classes S) S));
   144 
   145 
   146 (* certify *)
   147 
   148 fun certify_class classes c =
   149   if can (Graph.get_node classes) c then c
   150   else raise TYPE ("Undeclared class: " ^ quote c, [], []);
   151 
   152 fun certify_sort classes = norm_sort classes o map (certify_class classes);
   153 
   154 
   155 
   156 (** intersection **)
   157 
   158 (*intersect class with sort (preserves minimality)*)
   159 fun inter_class classes c S =
   160   let
   161     fun intr [] = [c]
   162       | intr (S' as c' :: c's) =
   163           if class_le classes (c', c) then S'
   164           else if class_le classes (c, c') then intr c's
   165           else c' :: intr c's
   166   in intr S end;
   167 
   168 (*instersect sorts (preserves minimality)*)
   169 fun inter_sort classes (S1, S2) =
   170   sort_strings (fold (inter_class classes) S1 S2);
   171 
   172 
   173 
   174 (** sorts of types **)
   175 
   176 (* mg_domain *)
   177 
   178 exception DOMAIN of string * class;
   179 
   180 fun mg_domain (classes, arities) a S =
   181   let
   182     fun dom c =
   183       (case Library.assoc_string (Symtab.lookup_multi (arities, a), c) of
   184         NONE => raise DOMAIN (a, c)
   185       | SOME Ss => Ss);
   186     fun dom_inter c Ss = ListPair.map (inter_sort classes) (dom c, Ss);
   187   in
   188     (case S of
   189       [] => sys_error "mg_domain"  (*don't know number of args!*)
   190     | c :: cs => fold dom_inter cs (dom c))
   191   end;
   192 
   193 
   194 (* of_sort *)
   195 
   196 fun of_sort (classes, arities) =
   197   let
   198     fun ofS (_, []) = true
   199       | ofS (TFree (_, S), S') = sort_le classes (S, S')
   200       | ofS (TVar (_, S), S') = sort_le classes (S, S')
   201       | ofS (Type (a, Ts), S) =
   202           let val Ss = mg_domain (classes, arities) a S in
   203             ListPair.all ofS (Ts, Ss)
   204           end handle DOMAIN _ => false;
   205   in ofS end;
   206 
   207 
   208 
   209 (** witness_sorts **)
   210 
   211 local
   212 
   213 fun witness_aux (classes, arities) log_types hyps sorts =
   214   let
   215     val top_witn = (propT, []);
   216     fun le S1 S2 = sort_le classes (S1, S2);
   217     fun get_solved S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE;
   218     fun get_hyp S2 S1 = if le S1 S2 then SOME (TFree ("'hyp", S1), S2) else NONE;
   219     fun mg_dom t S = SOME (mg_domain (classes, arities) t S) handle DOMAIN _ => NONE;
   220 
   221     fun witn_sort _ (solved_failed, []) = (solved_failed, SOME top_witn)
   222       | witn_sort path ((solved, failed), S) =
   223           if exists (le S) failed then ((solved, failed), NONE)
   224           else
   225             (case get_first (get_solved S) solved of
   226               SOME w => ((solved, failed), SOME w)
   227             | NONE =>
   228                 (case get_first (get_hyp S) hyps of
   229                   SOME w => ((w :: solved, failed), SOME w)
   230                 | NONE => witn_types path log_types ((solved, failed), S)))
   231 
   232     and witn_sorts path x = foldl_map (witn_sort path) x
   233 
   234     and witn_types _ [] ((solved, failed), S) = ((solved, S :: failed), NONE)
   235       | witn_types path (t :: ts) (solved_failed, S) =
   236           (case mg_dom t S of
   237             SOME SS =>
   238               (*do not descend into stronger args (achieving termination)*)
   239               if exists (fn D => le D S orelse exists (le D) path) SS then
   240                 witn_types path ts (solved_failed, S)
   241               else
   242                 let val ((solved', failed'), ws) = witn_sorts (S :: path) (solved_failed, SS) in
   243                   if forall isSome ws then
   244                     let val w = (Type (t, map (#1 o valOf) ws), S)
   245                     in ((w :: solved', failed'), SOME w) end
   246                   else witn_types path ts ((solved', failed'), S)
   247                 end
   248           | NONE => witn_types path ts (solved_failed, S));
   249 
   250   in witn_sorts [] (([], []), sorts) end;
   251 
   252 fun str_of_sort [c] = c
   253   | str_of_sort cs = enclose "{" "}" (commas cs);
   254 
   255 in
   256 
   257 fun witness_sorts (classes, arities) log_types hyps sorts =
   258   let
   259     (*double check result of witness construction*)
   260     fun check_result NONE = NONE
   261       | check_result (SOME (T, S)) =
   262           if of_sort (classes, arities) (T, S) then SOME (T, S)
   263           else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S);
   264   in List.mapPartial check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end;
   265 
   266 end;
   267 
   268 end;