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