src/Pure/defs.ML
author wenzelm
Mon May 08 17:40:06 2006 +0200 (2006-05-08)
changeset 19590 12af4942923d
parent 19569 1c23356a8ea8
child 19613 9bf274ec94cf
permissions -rw-r--r--
simple substructure test for typargs (independent type constructors);
     1 (*  Title:      Pure/defs.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Global well-formedness checks for constant definitions -- covers
     6 dependencies of simple sub-structural overloading.
     7 *)
     8 
     9 signature DEFS =
    10 sig
    11   type T
    12   val define: (string * typ -> typ list) ->
    13     bool -> string -> string -> string * typ -> (string * typ) list -> T -> T
    14   val specifications_of: T -> string ->
    15    (serial * {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list}) list
    16   val empty: T
    17   val merge: Pretty.pp -> T * T -> T
    18 end
    19 
    20 structure Defs: DEFS =
    21 struct
    22 
    23 
    24 (** datatype T **)
    25 
    26 type spec = {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list};
    27 
    28 datatype T = Defs of
    29  {consts: unit Graph.T,
    30   specified: spec Inttab.table Symtab.table};
    31 
    32 fun make_defs (consts, specified) = Defs {consts = consts, specified = specified};
    33 fun map_defs f (Defs {consts, specified}) = make_defs (f (consts, specified));
    34 
    35 fun cyclic cycles =
    36   "Cyclic dependency of constants:\n" ^
    37     cat_lines (map (space_implode " -> " o map quote o rev) cycles);
    38 
    39 
    40 (* specified consts *)
    41 
    42 fun disjoint_types T U =
    43   (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
    44     handle Type.TUNIFY => true;
    45 
    46 fun check_specified c (i, {lhs = T, name = a, ...}: spec) =
    47   Inttab.forall (fn (j, {lhs = U, name = b, ...}: spec) =>
    48     i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse
    49       error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
    50         " for constant " ^ quote c));
    51 
    52 
    53 (* substructural type arguments *)
    54 
    55 fun struct_less T (Type (_, Us)) = exists (struct_le T) Us
    56   | struct_less _ _ = false
    57 and struct_le T U = T = U orelse struct_less T U;
    58 
    59 fun structs_le Ts Us = forall (fn U => exists (fn T => struct_le T U) Ts) Us;
    60 fun structs_less Ts Us = Ts <> Us andalso structs_le Ts Us;
    61 
    62 
    63 (* define consts *)
    64 
    65 fun define const_typargs is_def module name lhs rhs = map_defs (fn (consts, specified) =>
    66   let
    67     val (c, T) = lhs;
    68     val args = const_typargs lhs;
    69     val deps = rhs |> map_filter (fn d =>
    70       if structs_less (const_typargs d) args then NONE else SOME (#1 d));
    71     val no_overloading = forall Term.is_TVar args andalso not (has_duplicates (op =) args);
    72 
    73     val consts' = fold (fn (a, _) => Graph.default_node (a, ())) (lhs :: rhs) consts;
    74     val consts'' = Graph.add_deps_acyclic (c, deps) consts' handle Graph.CYCLES cycles =>
    75       if no_overloading then error (cyclic cycles)
    76       else (warning (cyclic cycles ^ "\nUnchecked overloaded specification: " ^ name); consts');
    77 
    78     val spec = (serial (), {is_def = is_def, module = module, name = name, lhs = T, rhs = rhs});
    79     val specified' = specified
    80       |> Symtab.default (c, Inttab.empty)
    81       |> Symtab.map_entry c (fn specs => (check_specified c spec specs; Inttab.update spec specs));
    82   in (consts', specified') end);
    83 
    84 fun specifications_of (Defs {specified, ...}) c =
    85   Inttab.dest (the_default Inttab.empty (Symtab.lookup specified c));
    86 
    87 
    88 (* empty and merge *)
    89 
    90 val empty = make_defs (Graph.empty, Symtab.empty);
    91 
    92 fun merge pp
    93    (Defs {consts = consts1, specified = specified1},
    94     Defs {consts = consts2, specified = specified2}) =
    95   let
    96     val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
    97       handle Graph.CYCLES cycles => error (cyclic cycles);
    98     val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
    99       Inttab.fold (fn spec2 => fn specs1 =>
   100         (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1);
   101   in make_defs (consts', specified') end;
   102 
   103 end;