src/Pure/ML-Systems/universal.ML
author wenzelm
Thu Dec 20 21:12:00 2007 +0100 (2007-12-20 ago)
changeset 25733 8722d68471ff
child 28255 6faea8ad8559
permissions -rw-r--r--
Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm@25733
     1
(*  Title:      Pure/ML-Systems/universal.ML
wenzelm@25733
     2
    ID:         $Id$
wenzelm@25733
     3
    Author:     Makarius
wenzelm@25733
     4
wenzelm@25733
     5
Universal values via tagged union.  Emulates structure Universal
wenzelm@25733
     6
in Poly/ML 5.1.
wenzelm@25733
     7
*)
wenzelm@25733
     8
wenzelm@25733
     9
signature UNIVERSAL =
wenzelm@25733
    10
sig
wenzelm@25733
    11
  type universal
wenzelm@25733
    12
  type 'a tag
wenzelm@25733
    13
  val tag: unit -> 'a tag
wenzelm@25733
    14
  val tagIs: 'a tag -> universal -> bool
wenzelm@25733
    15
  val tagInject: 'a tag -> 'a -> universal
wenzelm@25733
    16
  val tagProject: 'a tag -> universal -> 'a
wenzelm@25733
    17
end;
wenzelm@25733
    18
wenzelm@25733
    19
structure Universal: UNIVERSAL =
wenzelm@25733
    20
struct
wenzelm@25733
    21
wenzelm@25733
    22
type universal = exn;
wenzelm@25733
    23
wenzelm@25733
    24
datatype 'a tag = Tag of
wenzelm@25733
    25
 {is: universal -> bool,
wenzelm@25733
    26
  inject: 'a -> universal,
wenzelm@25733
    27
  project: universal -> 'a};
wenzelm@25733
    28
wenzelm@25733
    29
fun tag () =
wenzelm@25733
    30
  let exception Universal of 'a in
wenzelm@25733
    31
   Tag {
wenzelm@25733
    32
    is = fn Universal _ => true | _ => false,
wenzelm@25733
    33
    inject = Universal,
wenzelm@25733
    34
    project = fn Universal x => x}
wenzelm@25733
    35
  end;
wenzelm@25733
    36
wenzelm@25733
    37
fun tagIs (Tag {is, ...}) = is;
wenzelm@25733
    38
fun tagInject (Tag {inject, ...}) = inject;
wenzelm@25733
    39
fun tagProject (Tag {project, ...}) = project;
wenzelm@25733
    40
wenzelm@25733
    41
end;
wenzelm@25733
    42