Type-safe interface for theory data.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/theory_data.ML Mon Jun 08 15:57:30 1998 +0200
@@ -0,0 +1,49 @@
+(* Title: Pure/theory_data.ML
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+
+Type-safe interface for theory data.
+*)
+
+signature THEORY_DATA_ARGS =
+sig
+ val name: string
+ type T
+ val empty: T
+ val prep_ext: T -> T
+ val merge: T * T -> T
+ val print: Sign.sg -> T -> unit
+end;
+
+signature THEORY_DATA =
+sig
+ type T
+ val init: theory -> theory
+ val print: theory -> unit
+ val get_sg: Sign.sg -> T
+ val get: theory -> T
+ val put: T -> theory -> theory
+end;
+
+functor TheoryDataFun(Args: THEORY_DATA_ARGS): THEORY_DATA =
+struct
+
+(*object kind kept private!*)
+val kind = Object.kind Args.name;
+
+type T = Args.T;
+exception Data of T;
+
+val init =
+ Theory.init_data kind
+ (Data Args.empty,
+ fn (Data x) => Data (Args.prep_ext x),
+ fn (Data x1, Data x2) => Data (Args.merge (x1, x2)),
+ fn sg => fn (Data x) => Args.print sg x);
+
+val print = Theory.print_data kind;
+val get_sg = Sign.get_data kind (fn Data x => x);
+val get = get_sg o Theory.sign_of;
+val put = Theory.put_data kind Data;
+
+end;