src/Pure/defs.ML
author haftmann
Sat Feb 25 15:11:35 2006 +0100 (2006-02-25)
changeset 19135 2de31ba562d7
parent 19050 527bc006f2b6
child 19339 59f08f67ed3f
permissions -rw-r--r--
added more detailed data to consts
     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) -> (bool * string) * string
    13     -> string * typ -> (string * typ) list -> T -> T
    14   val empty: T
    15   val specifications_of: T -> string -> (typ * string) list
    16   val merge: Pretty.pp -> T * T -> T
    17 end
    18 
    19 structure Defs: DEFS =
    20 struct
    21 
    22 (** datatype T **)
    23 
    24 datatype T = Defs of
    25  {consts: typ Graph.T,
    26     (*constant declarations and dependencies*)
    27   specified: (bool * string * string * typ) Inttab.table Symtab.table};
    28     (*is proper definition?, theory name, specification name and const type*)
    29 
    30 fun make_defs (consts, specified) = Defs {consts = consts, specified = specified};
    31 fun map_defs f (Defs {consts, specified}) = make_defs (f (consts, specified));
    32 
    33 
    34 (* specified consts *)
    35 
    36 fun disjoint_types T U =
    37   (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
    38     handle Type.TUNIFY => true;
    39 
    40 fun check_specified c (i, (_, a, _, T)) = Inttab.forall (fn (j, (_, b, _, U)) =>
    41   i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse
    42     error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
    43       " for constant " ^ quote c));
    44 
    45 
    46 (* define consts *)
    47 
    48 fun err_cyclic cycles =
    49   error ("Cyclic dependency of constants:\n" ^
    50     cat_lines (map (space_implode " -> " o map quote o rev) cycles));
    51 
    52 fun define const_type ((is_def, thyname), name) lhs rhs = map_defs (fn (consts, specified) =>
    53   let
    54     fun declare (a, _) = Graph.default_node (a, const_type a);
    55     fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G
    56       handle Graph.CYCLES cycles => err_cyclic cycles;
    57 
    58     val (c, T) = lhs;
    59     val spec = (serial (), (is_def, name, thyname, T));
    60     val no_overloading = Type.raw_instance (const_type c, T);
    61 
    62     val consts' =
    63       consts |> declare lhs |> fold declare rhs
    64       |> K no_overloading ? add_deps (c, map #1 rhs);
    65     val specified' = specified
    66       |> Symtab.default (c, Inttab.empty)
    67       |> Symtab.map_entry c (fn specs =>
    68         (check_specified c spec specs; Inttab.update spec specs));
    69   in (consts', specified') end);
    70 
    71 fun specifications_of (Defs {specified, ...}) c =
    72   (List.mapPartial
    73     (fn (_, (false, _, _, _)) => NONE
    74       | (_, (true, _, thyname, ty)) => SOME (ty, thyname)) o Inttab.dest
    75     o the_default Inttab.empty o Symtab.lookup specified) c;
    76 
    77 
    78 (* empty and merge *)
    79 
    80 val empty = make_defs (Graph.empty, Symtab.empty);
    81 
    82 fun merge pp
    83    (Defs {consts = consts1, specified = specified1},
    84     Defs {consts = consts2, specified = specified2}) =
    85   let
    86     val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
    87       handle Graph.CYCLES cycles => err_cyclic cycles;
    88     val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
    89       Inttab.fold (fn spec2 => fn specs1 =>
    90         (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1);
    91   in make_defs (consts', specified') end;
    92 
    93 end;