src/Pure/theory_data.ML
author wenzelm
Tue Oct 13 14:24:35 1998 +0200 (1998-10-13)
changeset 5642 1b3e48bdbb93
parent 5003 f73ad32e44d3
child 6546 995a66249a9b
permissions -rw-r--r--
PRIVATE sig parts;
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@5003
    13
  val prep_ext: T -> T
wenzelm@5003
    14
  val merge: T * T -> T
wenzelm@5003
    15
  val print: Sign.sg -> T -> unit
wenzelm@5003
    16
end;
wenzelm@5003
    17
wenzelm@5003
    18
signature THEORY_DATA =
wenzelm@5003
    19
sig
wenzelm@5003
    20
  type T
wenzelm@5003
    21
  val init: theory -> theory
wenzelm@5003
    22
  val print: theory -> unit
wenzelm@5003
    23
  val get_sg: Sign.sg -> T
wenzelm@5003
    24
  val get: theory -> T
wenzelm@5003
    25
  val put: T -> theory -> theory
wenzelm@5003
    26
end;
wenzelm@5003
    27
wenzelm@5003
    28
functor TheoryDataFun(Args: THEORY_DATA_ARGS): THEORY_DATA =
wenzelm@5003
    29
struct
wenzelm@5003
    30
wenzelm@5003
    31
(*object kind kept private!*)
wenzelm@5003
    32
val kind = Object.kind Args.name;
wenzelm@5003
    33
wenzelm@5003
    34
type T = Args.T;
wenzelm@5003
    35
exception Data of T;
wenzelm@5003
    36
wenzelm@5003
    37
val init =
wenzelm@5003
    38
  Theory.init_data kind
wenzelm@5003
    39
    (Data Args.empty,
wenzelm@5003
    40
      fn (Data x) => Data (Args.prep_ext x),
wenzelm@5003
    41
      fn (Data x1, Data x2) => Data (Args.merge (x1, x2)),
wenzelm@5003
    42
      fn sg => fn (Data x) => Args.print sg x);
wenzelm@5003
    43
wenzelm@5003
    44
val print = Theory.print_data kind;
wenzelm@5003
    45
val get_sg = Sign.get_data kind (fn Data x => x);
wenzelm@5003
    46
val get = get_sg o Theory.sign_of;
wenzelm@5003
    47
val put = Theory.put_data kind Data;
wenzelm@5003
    48
wenzelm@5003
    49
end;
wenzelm@5642
    50
wenzelm@5642
    51
(* FIXME deactivated due to Provers/classical.ML legacy code
wenzelm@5642
    52
(*hide private data access functions*)
wenzelm@5642
    53
structure Sign: SIGN = Sign;
wenzelm@5642
    54
structure Theory: THEORY = Theory;
wenzelm@5642
    55
*)