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