src/Pure/General/object.ML
author wenzelm
Fri Dec 14 11:52:54 2001 +0100 (2001-12-14)
changeset 12498 3b0091bf06e8
parent 8806 a202293db3f6
child 14981 e73f8140af78
permissions -rw-r--r--
changed Thm.varifyT';
wenzelm@6118
     1
(*  Title:      Pure/General/object.ML
wenzelm@5016
     2
    ID:         $Id$
wenzelm@5016
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8806
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@5016
     5
wenzelm@5016
     6
Generic objects of arbitrary type -- fool the ML type system via
wenzelm@5016
     7
exception constructors.
wenzelm@5016
     8
*)
wenzelm@5016
     9
wenzelm@5016
    10
signature OBJECT =
wenzelm@5016
    11
sig
wenzelm@5016
    12
  type T
wenzelm@5016
    13
  type kind
wenzelm@5016
    14
  val kind: string -> kind
wenzelm@5016
    15
  val name_of_kind: kind -> string
wenzelm@5016
    16
  val eq_kind: kind * kind -> bool
wenzelm@5016
    17
  val kind_error: kind -> 'a
wenzelm@5016
    18
end;
wenzelm@5016
    19
wenzelm@5016
    20
structure Object: OBJECT =
wenzelm@5016
    21
struct
wenzelm@5016
    22
wenzelm@5016
    23
wenzelm@5016
    24
(* anytype values *)
wenzelm@5016
    25
wenzelm@5016
    26
type T = exn;
wenzelm@5016
    27
wenzelm@5016
    28
wenzelm@5016
    29
(* kinds *)
wenzelm@5016
    30
wenzelm@5016
    31
datatype kind = Kind of string * stamp;
wenzelm@5016
    32
wenzelm@5016
    33
fun kind name = Kind (name, stamp ());
wenzelm@5016
    34
wenzelm@5016
    35
fun name_of_kind (Kind (name, _)) = name;
wenzelm@5016
    36
wenzelm@5016
    37
fun eq_kind (Kind (_, s1), Kind (_, s2)) = s1 = s2;
wenzelm@5016
    38
wenzelm@5016
    39
fun kind_error k =
wenzelm@5016
    40
  error ("## RUNTIME TYPE ERROR ##\nFailed to access " ^ quote (name_of_kind k) ^ " object");
wenzelm@5016
    41
wenzelm@5016
    42
wenzelm@5016
    43
end;