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