src/Pure/defs.ML
author wenzelm
Fri May 12 18:11:09 2006 +0200 (2006-05-12)
changeset 19624 3b6629701a79
parent 19620 ccd6de95f4a6
child 19628 de019ddcd89e
permissions -rw-r--r--
tuned;
     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, where type
     7 arguments are approximated by the outermost type constructor.
     8 *)
     9 
    10 signature DEFS =
    11 sig
    12   type T
    13   val specifications_of: T -> string ->
    14    (serial * {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list}) list
    15   val empty: T
    16   val merge: T * T -> T
    17   val define: (string * typ -> typ list) ->
    18     bool -> string -> string -> string * typ -> (string * typ) list -> T -> T
    19 end
    20 
    21 structure Defs: DEFS =
    22 struct
    23 
    24 (* dependency items *)
    25 
    26 (*
    27   Constant c covers all instances of c
    28 
    29   Instance (c, a) covers all instances of applications (c, [Type (a, _)])
    30 
    31   Different Constant/Constant or Instance/Instance items represent
    32   disjoint sets of instances.  The set Constant c subsumes any
    33   Instance (c, a) -- dependencies are propagated accordingly.
    34 *)
    35 
    36 datatype item =
    37   Constant of string |
    38   Instance of string * string;
    39 
    40 fun make_item (c, [Type (a, _)]) = Instance (c, a)
    41   | make_item (c, _) = Constant c;
    42 
    43 fun pretty_item (Constant c) = Pretty.str (quote c)
    44   | pretty_item (Instance (c, a)) = Pretty.str (quote c ^ " (type " ^ quote a ^ ")");
    45 
    46 fun item_ord (Constant c, Constant c') = fast_string_ord (c, c')
    47   | item_ord (Instance ca, Instance ca') = prod_ord fast_string_ord fast_string_ord (ca, ca')
    48   | item_ord (Constant _, Instance _) = LESS
    49   | item_ord (Instance _, Constant _) = GREATER;
    50 
    51 structure Items = GraphFun(type key = item val ord = item_ord);
    52 
    53 fun declare_edge (i, j) =
    54   Items.default_node (i, ()) #>
    55   Items.default_node (j, ()) #>
    56   Items.add_edge_acyclic (i, j);
    57 
    58 fun propagate_deps insts deps =
    59   let
    60     fun inst_item (Constant c) = Symtab.lookup_list insts c
    61       | inst_item (Instance _) = [];
    62     fun inst_edge i j =
    63       fold declare_edge (tl (product (i :: inst_item i) (j :: inst_item j)));
    64   in Items.fold (fn (i, (_, (_, js))) => fold (inst_edge i) js) deps deps end;
    65 
    66 
    67 (* specifications *)
    68 
    69 type spec = {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list};
    70 
    71 datatype T = Defs of
    72  {specs: (bool * spec Inttab.table) Symtab.table,
    73   insts: item list Symtab.table,
    74   deps: unit Items.T};
    75 
    76 fun no_overloading_of (Defs {specs, ...}) c =
    77   (case Symtab.lookup specs c of
    78     SOME (b, _) => b
    79   | NONE => false);
    80 
    81 fun specifications_of (Defs {specs, ...}) c =
    82   (case Symtab.lookup specs c of
    83     SOME (_, sps) => Inttab.dest sps
    84   | NONE => []);
    85 
    86 fun make_defs (specs, insts, deps) = Defs {specs = specs, insts = insts, deps = deps};
    87 fun map_defs f (Defs {specs, insts, deps}) = make_defs (f (specs, insts, deps));
    88 
    89 val empty = make_defs (Symtab.empty, Symtab.empty, Items.empty);
    90 
    91 
    92 (* disjoint specs *)
    93 
    94 fun disjoint_types T U =
    95   (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
    96     handle Type.TUNIFY => true;
    97 
    98 fun disjoint_specs c (i, {lhs = T, name = a, ...}: spec) =
    99   Inttab.forall (fn (j, {lhs = U, name = b, ...}: spec) =>
   100     i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse
   101       error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
   102         " for constant " ^ quote c));
   103 
   104 
   105 (* merge *)
   106 
   107 fun cycle_msg css =
   108   let
   109     fun prt_cycle items = Pretty.block (flat
   110       (separate [Pretty.str " ->", Pretty.brk 1] (map (single o pretty_item) items)));
   111   in Pretty.string_of (Pretty.big_list "Cyclic dependency of constants:" (map prt_cycle css)) end;
   112 
   113 fun merge
   114    (Defs {specs = specs1, insts = insts1, deps = deps1},
   115     Defs {specs = specs2, insts = insts2, deps = deps2}) =
   116   let
   117     val specs' = (specs1, specs2) |> Symtab.join (fn c => fn ((b, sps1), (_, sps2)) =>
   118       (b, Inttab.fold (fn sp2 => (disjoint_specs c sp2 sps1; Inttab.update sp2)) sps2 sps1));
   119     val insts' = Symtab.merge_list (op =) (insts1, insts2);
   120     val items' = propagate_deps insts' (Items.merge_acyclic (K true) (deps1, deps2))
   121       handle Items.CYCLES cycles => error (cycle_msg cycles);
   122   in make_defs (specs', insts', items') end;
   123 
   124 
   125 (* define *)
   126 
   127 fun pure_args args = forall Term.is_TVar args andalso not (has_duplicates (op =) args);
   128 
   129 fun define const_typargs is_def module name lhs rhs defs = defs
   130     |> map_defs (fn (specs, insts, deps) =>
   131   let
   132     val (c, T) = lhs;
   133     val args = const_typargs lhs;
   134     val no_overloading = pure_args args;
   135     val rec_args = (case args of [Type (_, Ts)] => if pure_args Ts then Ts else [] | _ => []);
   136 
   137     val spec = (serial (), {is_def = is_def, module = module, name = name, lhs = T, rhs = rhs});
   138     val specs' = specs
   139       |> Symtab.default (c, (false, Inttab.empty))
   140       |> Symtab.map_entry c (fn (_, sps) =>
   141           (disjoint_specs c spec sps; (no_overloading, Inttab.update spec sps)));
   142 
   143     val lhs' = make_item (c, args);
   144     val rhs' = rhs |> map_filter (fn (c', T') =>
   145       let val args' = const_typargs (c', T') in
   146         if gen_subset (op =) (args', rec_args) then NONE
   147         else SOME (make_item (c', if no_overloading_of defs c' then [] else args'))
   148       end);
   149 
   150     val insts' = insts |> fold (fn i as Instance (c, _) =>
   151         Symtab.insert_list (op =) (c, i) | _ => I) (lhs' :: rhs');
   152     val deps' = deps
   153       |> fold (fn r => declare_edge (r, lhs')) rhs'
   154       |> propagate_deps insts'
   155       handle Items.CYCLES cycles =>
   156         if no_overloading then error (cycle_msg cycles)
   157         else (warning (cycle_msg cycles ^ "\nUnchecked overloaded specification: " ^ name); deps);
   158 
   159   in (specs', insts', deps') end);
   160 
   161 end;