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;
wenzelm@17707
     1
(*  Title:      Pure/defs.ML
obua@16108
     2
    ID:         $Id$
wenzelm@17707
     3
    Author:     Makarius
obua@16108
     4
wenzelm@17707
     5
Global well-formedness checks for constant definitions.  Dependencies
wenzelm@17707
     6
are only tracked for non-overloaded definitions!
obua@16108
     7
*)
obua@16108
     8
wenzelm@16877
     9
signature DEFS =
wenzelm@16877
    10
sig
wenzelm@17707
    11
  type T
wenzelm@17707
    12
  val monomorphic: T -> string -> bool
wenzelm@17712
    13
  val define: (string -> typ) -> string -> string * typ -> (string * typ) list -> T -> T
wenzelm@17707
    14
  val empty: T
wenzelm@17707
    15
  val merge: Pretty.pp -> T * T -> T
obua@16108
    16
end
obua@16108
    17
wenzelm@17711
    18
structure Defs: DEFS =
wenzelm@17707
    19
struct
obua@16108
    20
wenzelm@17707
    21
(** datatype T **)
wenzelm@16877
    22
wenzelm@17707
    23
datatype T = Defs of
wenzelm@17707
    24
 {consts: typ Graph.T,                                 (*constant declarations and dependencies*)
wenzelm@17707
    25
  specified: (string * typ) Inttab.table Symtab.table, (*specification name and const type*)
wenzelm@17707
    26
  monomorphic: unit Symtab.table};                     (*constants having monomorphic specs*)
obua@16384
    27
wenzelm@17707
    28
fun rep_defs (Defs args) = args;
wenzelm@16877
    29
wenzelm@17707
    30
fun make_defs (consts, specified, monomorphic) =
wenzelm@17707
    31
  Defs {consts = consts, specified = specified, monomorphic = monomorphic};
wenzelm@16877
    32
wenzelm@17707
    33
fun map_defs f (Defs {consts, specified, monomorphic}) =
wenzelm@17707
    34
  make_defs (f (consts, specified, monomorphic));
wenzelm@16877
    35
wenzelm@16877
    36
wenzelm@17707
    37
(* specified consts *)
wenzelm@16877
    38
wenzelm@17707
    39
fun disjoint_types T U =
wenzelm@17707
    40
  (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
wenzelm@17707
    41
    handle Type.TUNIFY => true;
obua@16308
    42
wenzelm@17803
    43
fun check_specified c (i, (a, T)) = Inttab.forall (fn (j, (b, U)) =>
wenzelm@17803
    44
  i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse
wenzelm@17803
    45
    error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
wenzelm@17803
    46
      " for constant " ^ quote c));
wenzelm@16877
    47
wenzelm@16982
    48
wenzelm@17707
    49
(* monomorphic constants *)
wenzelm@16982
    50
wenzelm@17707
    51
val monomorphic = Symtab.defined o #monomorphic o rep_defs;
wenzelm@16877
    52
wenzelm@17707
    53
fun update_monomorphic specified c =
wenzelm@17707
    54
  let
wenzelm@17707
    55
    val specs = the_default Inttab.empty (Symtab.lookup specified c);
wenzelm@17707
    56
    fun is_monoT (Type (_, Ts)) = forall is_monoT Ts
wenzelm@17707
    57
      | is_monoT _ = false;
wenzelm@17707
    58
    val is_mono =
wenzelm@17707
    59
      Inttab.is_empty specs orelse
wenzelm@17707
    60
        Inttab.min_key specs = Inttab.max_key specs andalso
wenzelm@17707
    61
        is_monoT (snd (the (Inttab.lookup specs (the (Inttab.min_key specs)))));
wenzelm@17707
    62
  in if is_mono then Symtab.update (c, ()) else Symtab.remove (K true) (c, ()) end;
wenzelm@16877
    63
wenzelm@16877
    64
wenzelm@17707
    65
(* define consts *)
wenzelm@17707
    66
wenzelm@17707
    67
fun err_cyclic cycles =
wenzelm@17707
    68
  error ("Cyclic dependency of constants:\n" ^
wenzelm@17707
    69
    cat_lines (map (space_implode " -> " o map quote o rev) cycles));
wenzelm@16877
    70
wenzelm@17707
    71
fun define const_type name lhs rhs = map_defs (fn (consts, specified, monomorphic) =>
wenzelm@17707
    72
  let
wenzelm@17707
    73
    fun declare (a, _) = Graph.default_node (a, const_type a);
wenzelm@17707
    74
    fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G
wenzelm@17707
    75
      handle Graph.CYCLES cycles => err_cyclic cycles;
wenzelm@17707
    76
wenzelm@17707
    77
    val (c, T) = lhs;
wenzelm@17803
    78
    val spec = (serial (), (name, T));
wenzelm@17707
    79
    val no_overloading = Type.raw_instance (const_type c, T);
wenzelm@16877
    80
wenzelm@17707
    81
    val consts' =
wenzelm@17707
    82
      consts |> declare lhs |> fold declare rhs
wenzelm@17707
    83
      |> K no_overloading ? add_deps (c, map #1 rhs);
wenzelm@17803
    84
    val specified' = specified
wenzelm@17803
    85
      |> Symtab.default (c, Inttab.empty)
wenzelm@17803
    86
      |> Symtab.map_entry c (fn specs =>
wenzelm@17803
    87
        (check_specified c spec specs; Inttab.update spec specs));
wenzelm@17707
    88
    val monomorphic' = monomorphic |> update_monomorphic specified' c;
wenzelm@17707
    89
  in (consts', specified', monomorphic') end);
wenzelm@17707
    90
wenzelm@17707
    91
wenzelm@17707
    92
(* empty and merge *)
wenzelm@16877
    93
wenzelm@17707
    94
val empty = make_defs (Graph.empty, Symtab.empty, Symtab.empty);
wenzelm@16877
    95
wenzelm@17707
    96
fun merge pp
wenzelm@17707
    97
   (Defs {consts = consts1, specified = specified1, monomorphic},
wenzelm@17707
    98
    Defs {consts = consts2, specified = specified2, ...}) =
wenzelm@17707
    99
  let
wenzelm@17707
   100
    val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
wenzelm@17707
   101
      handle Graph.CYCLES cycles => err_cyclic cycles;
wenzelm@17803
   102
    val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
wenzelm@17803
   103
      SOME (Inttab.fold (fn spec2 => fn specs1 =>
wenzelm@17803
   104
        (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1));
wenzelm@17707
   105
    val monomorphic' = monomorphic
wenzelm@17707
   106
      |> Symtab.fold (update_monomorphic specified' o #1) specified';
wenzelm@17707
   107
  in make_defs (consts', specified', monomorphic') end;
wenzelm@16877
   108
obua@16108
   109
end;