src/Pure/General/object.ML
author wenzelm
Wed, 13 Jan 1999 15:18:02 +0100
changeset 6118 caa439435666
parent 5016 67c5966611c6
child 8806 a202293db3f6
permissions -rw-r--r--
fixed titles;

(*  Title:      Pure/General/object.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Generic objects of arbitrary type -- fool the ML type system via
exception constructors.
*)

signature OBJECT =
sig
  type T
  type kind
  val kind: string -> kind
  val name_of_kind: kind -> string
  val eq_kind: kind * kind -> bool
  val kind_error: kind -> 'a
end;

structure Object: OBJECT =
struct


(* anytype values *)

type T = exn;


(* kinds *)

datatype kind = Kind of string * stamp;

fun kind name = Kind (name, stamp ());

fun name_of_kind (Kind (name, _)) = name;

fun eq_kind (Kind (_, s1), Kind (_, s2)) = s1 = s2;

fun kind_error k =
  error ("## RUNTIME TYPE ERROR ##\nFailed to access " ^ quote (name_of_kind k) ^ " object");


end;