src/Pure/defs.ML
author wenzelm
Thu Sep 29 01:09:39 2005 +0200 (2005-09-29)
changeset 17711 c16cbe73798c
parent 17707 bc0270e9d27f
child 17712 46c2091e5187
permissions -rw-r--r--
activate signature constraints;
     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 -> 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 specified =
    44   specified |> Inttab.forall (fn (i, (a, T)) =>
    45     specified |> Inttab.forall (fn (j, (b, U)) =>
    46       i = j orelse disjoint_types T U orelse
    47         error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
    48           " for constant " ^ quote c)));
    49 
    50 
    51 (* monomorphic constants *)
    52 
    53 val monomorphic = Symtab.defined o #monomorphic o rep_defs;
    54 
    55 fun update_monomorphic specified c =
    56   let
    57     val specs = the_default Inttab.empty (Symtab.lookup specified c);
    58     fun is_monoT (Type (_, Ts)) = forall is_monoT Ts
    59       | is_monoT _ = false;
    60     val is_mono =
    61       Inttab.is_empty specs orelse
    62         Inttab.min_key specs = Inttab.max_key specs andalso
    63         is_monoT (snd (the (Inttab.lookup specs (the (Inttab.min_key specs)))));
    64   in if is_mono then Symtab.update (c, ()) else Symtab.remove (K true) (c, ()) end;
    65 
    66 
    67 (* define consts *)
    68 
    69 fun err_cyclic cycles =
    70   error ("Cyclic dependency of constants:\n" ^
    71     cat_lines (map (space_implode " -> " o map quote o rev) cycles));
    72 
    73 fun define const_type name lhs rhs = map_defs (fn (consts, specified, monomorphic) =>
    74   let
    75     fun declare (a, _) = Graph.default_node (a, const_type a);
    76     fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G
    77       handle Graph.CYCLES cycles => err_cyclic cycles;
    78 
    79     val (c, T) = lhs;
    80     val no_overloading = Type.raw_instance (const_type c, T);
    81 
    82     val consts' =
    83       consts |> declare lhs |> fold declare rhs
    84       |> K no_overloading ? add_deps (c, map #1 rhs);
    85     val specified' =
    86       specified |> Symtab.default (c, Inttab.empty)
    87       |> Symtab.map_entry c (Inttab.update (serial (), (name, T)) #> tap (check_specified c));
    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)
   103       |> Symtab.join (fn c => Inttab.merge (K true) #> tap (check_specified c) #> SOME);
   104     val monomorphic' = monomorphic
   105       |> Symtab.fold (update_monomorphic specified' o #1) specified';
   106   in make_defs (consts', specified', monomorphic') end;
   107 
   108 end;