src/Pure/theory_data.ML
changeset 5003 f73ad32e44d3
child 5642 1b3e48bdbb93
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/theory_data.ML	Mon Jun 08 15:57:30 1998 +0200
     1.3 @@ -0,0 +1,49 @@
     1.4 +(*  Title:      Pure/theory_data.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Type-safe interface for theory data.
     1.9 +*)
    1.10 +
    1.11 +signature THEORY_DATA_ARGS =
    1.12 +sig
    1.13 +  val name: string
    1.14 +  type T
    1.15 +  val empty: T
    1.16 +  val prep_ext: T -> T
    1.17 +  val merge: T * T -> T
    1.18 +  val print: Sign.sg -> T -> unit
    1.19 +end;
    1.20 +
    1.21 +signature THEORY_DATA =
    1.22 +sig
    1.23 +  type T
    1.24 +  val init: theory -> theory
    1.25 +  val print: theory -> unit
    1.26 +  val get_sg: Sign.sg -> T
    1.27 +  val get: theory -> T
    1.28 +  val put: T -> theory -> theory
    1.29 +end;
    1.30 +
    1.31 +functor TheoryDataFun(Args: THEORY_DATA_ARGS): THEORY_DATA =
    1.32 +struct
    1.33 +
    1.34 +(*object kind kept private!*)
    1.35 +val kind = Object.kind Args.name;
    1.36 +
    1.37 +type T = Args.T;
    1.38 +exception Data of T;
    1.39 +
    1.40 +val init =
    1.41 +  Theory.init_data kind
    1.42 +    (Data Args.empty,
    1.43 +      fn (Data x) => Data (Args.prep_ext x),
    1.44 +      fn (Data x1, Data x2) => Data (Args.merge (x1, x2)),
    1.45 +      fn sg => fn (Data x) => Args.print sg x);
    1.46 +
    1.47 +val print = Theory.print_data kind;
    1.48 +val get_sg = Sign.get_data kind (fn Data x => x);
    1.49 +val get = get_sg o Theory.sign_of;
    1.50 +val put = Theory.put_data kind Data;
    1.51 +
    1.52 +end;