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