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