src/Pure/ML-Systems/universal.ML
author wenzelm
Mon, 19 Jan 2009 19:38:03 +0100
changeset 29564 f8b933a62151
parent 28255 6faea8ad8559
permissions -rw-r--r--
removed Ids;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
25733
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/universal.ML
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
     3
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
     4
Universal values via tagged union.  Emulates structure Universal
28255
6faea8ad8559 tuned comments;
wenzelm
parents: 25733
diff changeset
     5
from Poly/ML 5.1.
25733
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
     6
*)
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
     7
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
     8
signature UNIVERSAL =
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
     9
sig
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    10
  type universal
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    11
  type 'a tag
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    12
  val tag: unit -> 'a tag
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    13
  val tagIs: 'a tag -> universal -> bool
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    14
  val tagInject: 'a tag -> 'a -> universal
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    15
  val tagProject: 'a tag -> universal -> 'a
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    16
end;
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    17
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    18
structure Universal: UNIVERSAL =
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    19
struct
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    20
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    21
type universal = exn;
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    22
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    23
datatype 'a tag = Tag of
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    24
 {is: universal -> bool,
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    25
  inject: 'a -> universal,
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    26
  project: universal -> 'a};
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    27
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    28
fun tag () =
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    29
  let exception Universal of 'a in
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    30
   Tag {
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    31
    is = fn Universal _ => true | _ => false,
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    32
    inject = Universal,
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    33
    project = fn Universal x => x}
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    34
  end;
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    35
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    36
fun tagIs (Tag {is, ...}) = is;
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    37
fun tagInject (Tag {inject, ...}) = inject;
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    38
fun tagProject (Tag {project, ...}) = project;
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    39
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    40
end;
8722d68471ff Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
wenzelm
parents:
diff changeset
    41