src/Pure/defs.ML
author wenzelm
Sat Oct 08 22:39:41 2005 +0200 (2005-10-08)
changeset 17803 e235a57651a1
parent 17712 46c2091e5187
child 17994 6a1a49cba5b3
permissions -rw-r--r--
more efficient check_specified, much less invocations;
Type.could_unify filter;
     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 monomorphic: T -> string -> bool
    13   val define: (string -> typ) -> string -> string * typ -> (string * typ) list -> T -> T
    14   val empty: T
    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   monomorphic: unit Symtab.table};                     (*constants having monomorphic specs*)
    27 
    28 fun rep_defs (Defs args) = args;
    29 
    30 fun make_defs (consts, specified, monomorphic) =
    31   Defs {consts = consts, specified = specified, monomorphic = monomorphic};
    32 
    33 fun map_defs f (Defs {consts, specified, monomorphic}) =
    34   make_defs (f (consts, specified, monomorphic));
    35 
    36 
    37 (* specified consts *)
    38 
    39 fun disjoint_types T U =
    40   (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
    41     handle Type.TUNIFY => true;
    42 
    43 fun check_specified c (i, (a, T)) = Inttab.forall (fn (j, (b, U)) =>
    44   i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse
    45     error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
    46       " for constant " ^ quote c));
    47 
    48 
    49 (* monomorphic constants *)
    50 
    51 val monomorphic = Symtab.defined o #monomorphic o rep_defs;
    52 
    53 fun update_monomorphic specified c =
    54   let
    55     val specs = the_default Inttab.empty (Symtab.lookup specified c);
    56     fun is_monoT (Type (_, Ts)) = forall is_monoT Ts
    57       | is_monoT _ = false;
    58     val is_mono =
    59       Inttab.is_empty specs orelse
    60         Inttab.min_key specs = Inttab.max_key specs andalso
    61         is_monoT (snd (the (Inttab.lookup specs (the (Inttab.min_key specs)))));
    62   in if is_mono then Symtab.update (c, ()) else Symtab.remove (K true) (c, ()) end;
    63 
    64 
    65 (* define consts *)
    66 
    67 fun err_cyclic cycles =
    68   error ("Cyclic dependency of constants:\n" ^
    69     cat_lines (map (space_implode " -> " o map quote o rev) cycles));
    70 
    71 fun define const_type name lhs rhs = map_defs (fn (consts, specified, monomorphic) =>
    72   let
    73     fun declare (a, _) = Graph.default_node (a, const_type a);
    74     fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G
    75       handle Graph.CYCLES cycles => err_cyclic cycles;
    76 
    77     val (c, T) = lhs;
    78     val spec = (serial (), (name, T));
    79     val no_overloading = Type.raw_instance (const_type c, T);
    80 
    81     val consts' =
    82       consts |> declare lhs |> fold declare rhs
    83       |> K no_overloading ? add_deps (c, map #1 rhs);
    84     val specified' = specified
    85       |> Symtab.default (c, Inttab.empty)
    86       |> Symtab.map_entry c (fn specs =>
    87         (check_specified c spec specs; Inttab.update spec specs));
    88     val monomorphic' = monomorphic |> update_monomorphic specified' c;
    89   in (consts', specified', monomorphic') end);
    90 
    91 
    92 (* empty and merge *)
    93 
    94 val empty = make_defs (Graph.empty, Symtab.empty, Symtab.empty);
    95 
    96 fun merge pp
    97    (Defs {consts = consts1, specified = specified1, monomorphic},
    98     Defs {consts = consts2, specified = specified2, ...}) =
    99   let
   100     val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
   101       handle Graph.CYCLES cycles => err_cyclic cycles;
   102     val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
   103       SOME (Inttab.fold (fn spec2 => fn specs1 =>
   104         (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1));
   105     val monomorphic' = monomorphic
   106       |> Symtab.fold (update_monomorphic specified' o #1) specified';
   107   in make_defs (consts', specified', monomorphic') end;
   108 
   109 end;