# HG changeset patch
# User wenzelm
# Date 1198181520 -3600
# Node ID 8722d68471ff0a6e1ace5d71e1fd7e61a59d2e62
# Parent  308315ee2b6d4030c1a4f579c66815e33f1949d7
Universal values via tagged union.  Emulates structure Universal in Poly/ML 5.1.

diff -r 308315ee2b6d -r 8722d68471ff src/Pure/ML-Systems/universal.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/universal.ML	Thu Dec 20 21:12:00 2007 +0100
@@ -0,0 +1,42 @@
+(*  Title:      Pure/ML-Systems/universal.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Universal values via tagged union.  Emulates structure Universal
+in Poly/ML 5.1.
+*)
+
+signature UNIVERSAL =
+sig
+  type universal
+  type 'a tag
+  val tag: unit -> 'a tag
+  val tagIs: 'a tag -> universal -> bool
+  val tagInject: 'a tag -> 'a -> universal
+  val tagProject: 'a tag -> universal -> 'a
+end;
+
+structure Universal: UNIVERSAL =
+struct
+
+type universal = exn;
+
+datatype 'a tag = Tag of
+ {is: universal -> bool,
+  inject: 'a -> universal,
+  project: universal -> 'a};
+
+fun tag () =
+  let exception Universal of 'a in
+   Tag {
+    is = fn Universal _ => true | _ => false,
+    inject = Universal,
+    project = fn Universal x => x}
+  end;
+
+fun tagIs (Tag {is, ...}) = is;
+fun tagInject (Tag {inject, ...}) = inject;
+fun tagProject (Tag {project, ...}) = project;
+
+end;
+