src/Pure/defs.ML
author wenzelm
Fri May 05 19:32:33 2006 +0200 (2006-05-05)
changeset 19569 1c23356a8ea8
parent 19482 9f11af8f7ef9
child 19590 12af4942923d
permissions -rw-r--r--
specifications_of: more detailed information;
tuned;
wenzelm@17707
     1
(*  Title:      Pure/defs.ML
obua@16108
     2
    ID:         $Id$
wenzelm@17707
     3
    Author:     Makarius
obua@16108
     4
wenzelm@17707
     5
Global well-formedness checks for constant definitions.  Dependencies
wenzelm@17707
     6
are only tracked for non-overloaded definitions!
obua@16108
     7
*)
obua@16108
     8
wenzelm@16877
     9
signature DEFS =
wenzelm@16877
    10
sig
wenzelm@17707
    11
  type T
wenzelm@19569
    12
  val define: (string -> typ) -> bool -> string -> string ->
wenzelm@19569
    13
    string * typ -> (string * typ) list -> T -> T
wenzelm@17707
    14
  val empty: T
wenzelm@19569
    15
  val specifications_of: T -> string ->
wenzelm@19569
    16
   (serial * {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list}) list
wenzelm@17707
    17
  val merge: Pretty.pp -> T * T -> T
obua@16108
    18
end
obua@16108
    19
wenzelm@17711
    20
structure Defs: DEFS =
wenzelm@17707
    21
struct
obua@16108
    22
wenzelm@19569
    23
wenzelm@17707
    24
(** datatype T **)
wenzelm@16877
    25
wenzelm@19569
    26
type spec = {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list};
wenzelm@19569
    27
wenzelm@17707
    28
datatype T = Defs of
haftmann@19135
    29
 {consts: typ Graph.T,
haftmann@19135
    30
    (*constant declarations and dependencies*)
wenzelm@19569
    31
  specified: spec Inttab.table Symtab.table};
wenzelm@16877
    32
wenzelm@17994
    33
fun make_defs (consts, specified) = Defs {consts = consts, specified = specified};
wenzelm@17994
    34
fun map_defs f (Defs {consts, specified}) = make_defs (f (consts, specified));
wenzelm@16877
    35
wenzelm@16877
    36
wenzelm@17707
    37
(* specified consts *)
wenzelm@16877
    38
wenzelm@17707
    39
fun disjoint_types T U =
wenzelm@17707
    40
  (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
wenzelm@17707
    41
    handle Type.TUNIFY => true;
obua@16308
    42
wenzelm@19569
    43
fun check_specified c (i, {lhs = T, name = a, ...}: spec) =
wenzelm@19569
    44
  Inttab.forall (fn (j, {lhs = U, name = b, ...}: spec) =>
wenzelm@19569
    45
    i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse
wenzelm@19569
    46
      error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
wenzelm@19569
    47
        " for constant " ^ quote c));
wenzelm@16877
    48
wenzelm@16982
    49
wenzelm@17707
    50
(* define consts *)
wenzelm@17707
    51
wenzelm@17707
    52
fun err_cyclic cycles =
wenzelm@17707
    53
  error ("Cyclic dependency of constants:\n" ^
wenzelm@17707
    54
    cat_lines (map (space_implode " -> " o map quote o rev) cycles));
wenzelm@16877
    55
wenzelm@19569
    56
fun define const_type is_def module name lhs rhs = map_defs (fn (consts, specified) =>
wenzelm@17707
    57
  let
wenzelm@17707
    58
    fun declare (a, _) = Graph.default_node (a, const_type a);
wenzelm@17707
    59
    fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G
wenzelm@17707
    60
      handle Graph.CYCLES cycles => err_cyclic cycles;
wenzelm@17707
    61
wenzelm@17707
    62
    val (c, T) = lhs;
wenzelm@19569
    63
    val spec = (serial (), {is_def = is_def, module = module, name = name, lhs = T, rhs = rhs});
wenzelm@17707
    64
    val no_overloading = Type.raw_instance (const_type c, T);
wenzelm@16877
    65
wenzelm@17707
    66
    val consts' =
wenzelm@17707
    67
      consts |> declare lhs |> fold declare rhs
wenzelm@17707
    68
      |> K no_overloading ? add_deps (c, map #1 rhs);
wenzelm@17803
    69
    val specified' = specified
wenzelm@17803
    70
      |> Symtab.default (c, Inttab.empty)
wenzelm@17803
    71
      |> Symtab.map_entry c (fn specs =>
wenzelm@17803
    72
        (check_specified c spec specs; Inttab.update spec specs));
wenzelm@17994
    73
  in (consts', specified') end);
wenzelm@17707
    74
wenzelm@19050
    75
fun specifications_of (Defs {specified, ...}) c =
wenzelm@19569
    76
  Inttab.dest (the_default Inttab.empty (Symtab.lookup specified c));
wenzelm@19050
    77
wenzelm@17707
    78
wenzelm@17707
    79
(* empty and merge *)
wenzelm@16877
    80
wenzelm@17994
    81
val empty = make_defs (Graph.empty, Symtab.empty);
wenzelm@16877
    82
wenzelm@17707
    83
fun merge pp
wenzelm@17994
    84
   (Defs {consts = consts1, specified = specified1},
wenzelm@17994
    85
    Defs {consts = consts2, specified = specified2}) =
wenzelm@17707
    86
  let
wenzelm@17707
    87
    val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
wenzelm@17707
    88
      handle Graph.CYCLES cycles => err_cyclic cycles;
wenzelm@17803
    89
    val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
wenzelm@19025
    90
      Inttab.fold (fn spec2 => fn specs1 =>
wenzelm@19025
    91
        (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1);
wenzelm@17994
    92
  in make_defs (consts', specified') end;
wenzelm@16877
    93
obua@16108
    94
end;