src/Pure/theory_data.ML
author obua
Sun May 29 12:39:12 2005 +0200 (2005-05-29)
changeset 16108 cf468b93a02e
parent 14981 e73f8140af78
permissions -rw-r--r--
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
wenzelm@5003
     1
(*  Title:      Pure/theory_data.ML
wenzelm@5003
     2
    ID:         $Id$
wenzelm@5003
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5003
     4
wenzelm@5003
     5
Type-safe interface for theory data.
wenzelm@5003
     6
*)
wenzelm@5003
     7
wenzelm@5003
     8
signature THEORY_DATA_ARGS =
wenzelm@5003
     9
sig
wenzelm@5003
    10
  val name: string
wenzelm@5003
    11
  type T
wenzelm@5003
    12
  val empty: T
wenzelm@6546
    13
  val copy: T -> T
wenzelm@5003
    14
  val prep_ext: T -> T
wenzelm@5003
    15
  val merge: T * T -> T
wenzelm@5003
    16
  val print: Sign.sg -> T -> unit
wenzelm@5003
    17
end;
wenzelm@5003
    18
wenzelm@5003
    19
signature THEORY_DATA =
wenzelm@5003
    20
sig
wenzelm@5003
    21
  type T
wenzelm@5003
    22
  val init: theory -> theory
wenzelm@5003
    23
  val print: theory -> unit
wenzelm@5003
    24
  val get_sg: Sign.sg -> T
wenzelm@5003
    25
  val get: theory -> T
wenzelm@5003
    26
  val put: T -> theory -> theory
wenzelm@8142
    27
  val map: (T -> T) -> theory -> theory
wenzelm@5003
    28
end;
wenzelm@5003
    29
wenzelm@5003
    30
functor TheoryDataFun(Args: THEORY_DATA_ARGS): THEORY_DATA =
wenzelm@5003
    31
struct
wenzelm@5003
    32
wenzelm@5003
    33
(*object kind kept private!*)
wenzelm@5003
    34
val kind = Object.kind Args.name;
wenzelm@5003
    35
wenzelm@5003
    36
type T = Args.T;
wenzelm@5003
    37
exception Data of T;
wenzelm@5003
    38
wenzelm@5003
    39
val init =
wenzelm@5003
    40
  Theory.init_data kind
wenzelm@5003
    41
    (Data Args.empty,
wenzelm@6546
    42
      fn (Data x) => Data (Args.copy x),
wenzelm@5003
    43
      fn (Data x) => Data (Args.prep_ext x),
wenzelm@5003
    44
      fn (Data x1, Data x2) => Data (Args.merge (x1, x2)),
wenzelm@5003
    45
      fn sg => fn (Data x) => Args.print sg x);
wenzelm@5003
    46
wenzelm@5003
    47
val print = Theory.print_data kind;
wenzelm@5003
    48
val get_sg = Sign.get_data kind (fn Data x => x);
wenzelm@5003
    49
val get = get_sg o Theory.sign_of;
wenzelm@5003
    50
val put = Theory.put_data kind Data;
wenzelm@8142
    51
fun map f thy = put (f (get thy)) thy;
wenzelm@5003
    52
wenzelm@5003
    53
end;
wenzelm@5642
    54
wenzelm@5642
    55
(*hide private data access functions*)
wenzelm@5642
    56
structure Sign: SIGN = Sign;
wenzelm@5642
    57
structure Theory: THEORY = Theory;