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;
     1 (*  Title:      Pure/theory_data.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Type-safe interface for theory data.
     6 *)
     7 
     8 signature THEORY_DATA_ARGS =
     9 sig
    10   val name: string
    11   type T
    12   val empty: T
    13   val prep_ext: T -> T
    14   val merge: T * T -> T
    15   val print: Sign.sg -> T -> unit
    16 end;
    17 
    18 signature THEORY_DATA =
    19 sig
    20   type T
    21   val init: theory -> theory
    22   val print: theory -> unit
    23   val get_sg: Sign.sg -> T
    24   val get: theory -> T
    25   val put: T -> theory -> theory
    26 end;
    27 
    28 functor TheoryDataFun(Args: THEORY_DATA_ARGS): THEORY_DATA =
    29 struct
    30 
    31 (*object kind kept private!*)
    32 val kind = Object.kind Args.name;
    33 
    34 type T = Args.T;
    35 exception Data of T;
    36 
    37 val init =
    38   Theory.init_data kind
    39     (Data Args.empty,
    40       fn (Data x) => Data (Args.prep_ext x),
    41       fn (Data x1, Data x2) => Data (Args.merge (x1, x2)),
    42       fn sg => fn (Data x) => Args.print sg x);
    43 
    44 val print = Theory.print_data kind;
    45 val get_sg = Sign.get_data kind (fn Data x => x);
    46 val get = get_sg o Theory.sign_of;
    47 val put = Theory.put_data kind Data;
    48 
    49 end;
    50 
    51 (* FIXME deactivated due to Provers/classical.ML legacy code
    52 (*hide private data access functions*)
    53 structure Sign: SIGN = Sign;
    54 structure Theory: THEORY = Theory;
    55 *)