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