src/Pure/theory_data.ML
author wenzelm
Sat Nov 24 16:55:56 2001 +0100 (2001-11-24)
changeset 12284 131e743d168a
parent 12123 739eba13e2cd
child 12311 ce5f9e61c037
permissions -rw-r--r--
added gen_merge_lists(') and merge_lists(');
removed obsolete generic_extend, generic_merge, extend_list;
     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 finish: T -> T
    15   val prep_ext: T -> T
    16   val merge: T * T -> T
    17   val print: Sign.sg -> T -> unit
    18 end;
    19 
    20 signature THEORY_DATA =
    21 sig
    22   type T
    23   val init: theory -> theory
    24   val print: theory -> unit
    25   val get_sg: Sign.sg -> T
    26   val get: theory -> T
    27   val put: T -> theory -> theory
    28   val map: (T -> T) -> theory -> theory
    29 end;
    30 
    31 functor TheoryDataFun(Args: THEORY_DATA_ARGS): THEORY_DATA =
    32 struct
    33 
    34 (*object kind kept private!*)
    35 val kind = Object.kind Args.name;
    36 
    37 type T = Args.T;
    38 exception Data of T;
    39 
    40 val init =
    41   Theory.init_data kind
    42     (Data Args.empty,
    43       fn (Data x) => Data (Args.copy x),
    44       fn (Data x) => Data (Args.finish x),
    45       fn (Data x) => Data (Args.prep_ext x),
    46       fn (Data x1, Data x2) => Data (Args.merge (x1, x2)),
    47       fn sg => fn (Data x) => Args.print sg x);
    48 
    49 val print = Theory.print_data kind;
    50 val get_sg = Sign.get_data kind (fn Data x => x);
    51 val get = get_sg o Theory.sign_of;
    52 val put = Theory.put_data kind Data;
    53 fun map f thy = put (f (get thy)) thy;
    54 
    55 end;
    56 
    57 (*hide private data access functions*)
    58 structure Sign: SIGN = Sign;
    59 structure Theory: THEORY = Theory;