src/Pure/theory_data.ML
author wenzelm
Mon, 09 Nov 1998 15:42:08 +0100
changeset 5840 e2d2b896c717
parent 5642 1b3e48bdbb93
child 6546 995a66249a9b
permissions -rw-r--r--
Object logic specific operations.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5003
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/theory_data.ML
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
     4
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
     5
Type-safe interface for theory data.
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
     6
*)
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
     7
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
     8
signature THEORY_DATA_ARGS =
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
     9
sig
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    10
  val name: string
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    11
  type T
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    12
  val empty: T
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    13
  val prep_ext: T -> T
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    14
  val merge: T * T -> T
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    15
  val print: Sign.sg -> T -> unit
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    16
end;
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    17
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    18
signature THEORY_DATA =
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    19
sig
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    20
  type T
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    21
  val init: theory -> theory
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    22
  val print: theory -> unit
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    23
  val get_sg: Sign.sg -> T
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    24
  val get: theory -> T
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    25
  val put: T -> theory -> theory
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    26
end;
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    27
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    28
functor TheoryDataFun(Args: THEORY_DATA_ARGS): THEORY_DATA =
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    29
struct
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    30
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    31
(*object kind kept private!*)
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    32
val kind = Object.kind Args.name;
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    33
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    34
type T = Args.T;
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    35
exception Data of T;
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    36
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    37
val init =
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    38
  Theory.init_data kind
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    39
    (Data Args.empty,
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    40
      fn (Data x) => Data (Args.prep_ext x),
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    41
      fn (Data x1, Data x2) => Data (Args.merge (x1, x2)),
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    42
      fn sg => fn (Data x) => Args.print sg x);
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    43
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    44
val print = Theory.print_data kind;
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    45
val get_sg = Sign.get_data kind (fn Data x => x);
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    46
val get = get_sg o Theory.sign_of;
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    47
val put = Theory.put_data kind Data;
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    48
f73ad32e44d3 Type-safe interface for theory data.
wenzelm
parents:
diff changeset
    49
end;
5642
1b3e48bdbb93 PRIVATE sig parts;
wenzelm
parents: 5003
diff changeset
    50
1b3e48bdbb93 PRIVATE sig parts;
wenzelm
parents: 5003
diff changeset
    51
(* FIXME deactivated due to Provers/classical.ML legacy code
1b3e48bdbb93 PRIVATE sig parts;
wenzelm
parents: 5003
diff changeset
    52
(*hide private data access functions*)
1b3e48bdbb93 PRIVATE sig parts;
wenzelm
parents: 5003
diff changeset
    53
structure Sign: SIGN = Sign;
1b3e48bdbb93 PRIVATE sig parts;
wenzelm
parents: 5003
diff changeset
    54
structure Theory: THEORY = Theory;
1b3e48bdbb93 PRIVATE sig parts;
wenzelm
parents: 5003
diff changeset
    55
*)