src/Pure/defs.ML
author wenzelm
Thu Oct 27 13:54:42 2005 +0200 (2005-10-27)
changeset 17994 6a1a49cba5b3
parent 17803 e235a57651a1
child 19025 596fb1eb7856
permissions -rw-r--r--
removed inappropriate monomorphic test;
     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 merge: Pretty.pp -> T * T -> T
    15 end
    16 
    17 structure Defs: DEFS =
    18 struct
    19 
    20 (** datatype T **)
    21 
    22 datatype T = Defs of
    23  {consts: typ Graph.T,                                 (*constant declarations and dependencies*)
    24   specified: (string * typ) Inttab.table Symtab.table}; (*specification name and const type*)
    25 
    26 fun make_defs (consts, specified) = Defs {consts = consts, specified = specified};
    27 fun map_defs f (Defs {consts, specified}) = make_defs (f (consts, specified));
    28 
    29 
    30 (* specified consts *)
    31 
    32 fun disjoint_types T U =
    33   (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
    34     handle Type.TUNIFY => true;
    35 
    36 fun check_specified c (i, (a, T)) = Inttab.forall (fn (j, (b, U)) =>
    37   i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse
    38     error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
    39       " for constant " ^ quote c));
    40 
    41 
    42 (* define consts *)
    43 
    44 fun err_cyclic cycles =
    45   error ("Cyclic dependency of constants:\n" ^
    46     cat_lines (map (space_implode " -> " o map quote o rev) cycles));
    47 
    48 fun define const_type name lhs rhs = map_defs (fn (consts, specified) =>
    49   let
    50     fun declare (a, _) = Graph.default_node (a, const_type a);
    51     fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G
    52       handle Graph.CYCLES cycles => err_cyclic cycles;
    53 
    54     val (c, T) = lhs;
    55     val spec = (serial (), (name, T));
    56     val no_overloading = Type.raw_instance (const_type c, T);
    57 
    58     val consts' =
    59       consts |> declare lhs |> fold declare rhs
    60       |> K no_overloading ? add_deps (c, map #1 rhs);
    61     val specified' = specified
    62       |> Symtab.default (c, Inttab.empty)
    63       |> Symtab.map_entry c (fn specs =>
    64         (check_specified c spec specs; Inttab.update spec specs));
    65   in (consts', specified') end);
    66 
    67 
    68 (* empty and merge *)
    69 
    70 val empty = make_defs (Graph.empty, Symtab.empty);
    71 
    72 fun merge pp
    73    (Defs {consts = consts1, specified = specified1},
    74     Defs {consts = consts2, specified = specified2}) =
    75   let
    76     val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
    77       handle Graph.CYCLES cycles => err_cyclic cycles;
    78     val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
    79       SOME (Inttab.fold (fn spec2 => fn specs1 =>
    80         (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1));
    81   in make_defs (consts', specified') end;
    82 
    83 end;