src/Pure/theory_data.ML
author berghofe
Wed Oct 31 19:37:04 2001 +0100 (2001-10-31)
changeset 11998 b14e7686ce84
parent 8142 37d3b5a4ebae
child 12123 739eba13e2cd
permissions -rw-r--r--
- enter_thmx -> enter_thms
- improved naming of theorems: enter_thms now takes functions pre_name and post_name
as arguments
     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   val map: (T -> T) -> theory -> theory
    28 end;
    29 
    30 functor TheoryDataFun(Args: THEORY_DATA_ARGS): THEORY_DATA =
    31 struct
    32 
    33 (*object kind kept private!*)
    34 val kind = Object.kind Args.name;
    35 
    36 type T = Args.T;
    37 exception Data of T;
    38 
    39 val init =
    40   Theory.init_data kind
    41     (Data Args.empty,
    42       fn (Data x) => Data (Args.copy x),
    43       fn (Data x) => Data (Args.prep_ext x),
    44       fn (Data x1, Data x2) => Data (Args.merge (x1, x2)),
    45       fn sg => fn (Data x) => Args.print sg x);
    46 
    47 val print = Theory.print_data kind;
    48 val get_sg = Sign.get_data kind (fn Data x => x);
    49 val get = get_sg o Theory.sign_of;
    50 val put = Theory.put_data kind Data;
    51 fun map f thy = put (f (get thy)) thy;
    52 
    53 end;
    54 
    55 (*hide private data access functions*)
    56 structure Sign: SIGN = Sign;
    57 structure Theory: THEORY = Theory;