src/Pure/ML-Systems/universal.ML
author wenzelm
Tue Mar 25 13:18:10 2014 +0100 (2014-03-25 ago)
changeset 56275 600f432ab556
parent 29564 f8b933a62151
permissions -rw-r--r--
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm@25733
     1
(*  Title:      Pure/ML-Systems/universal.ML
wenzelm@25733
     2
    Author:     Makarius
wenzelm@25733
     3
wenzelm@25733
     4
Universal values via tagged union.  Emulates structure Universal
wenzelm@28255
     5
from Poly/ML 5.1.
wenzelm@25733
     6
*)
wenzelm@25733
     7
wenzelm@25733
     8
signature UNIVERSAL =
wenzelm@25733
     9
sig
wenzelm@25733
    10
  type universal
wenzelm@25733
    11
  type 'a tag
wenzelm@25733
    12
  val tag: unit -> 'a tag
wenzelm@25733
    13
  val tagIs: 'a tag -> universal -> bool
wenzelm@25733
    14
  val tagInject: 'a tag -> 'a -> universal
wenzelm@25733
    15
  val tagProject: 'a tag -> universal -> 'a
wenzelm@25733
    16
end;
wenzelm@25733
    17
wenzelm@25733
    18
structure Universal: UNIVERSAL =
wenzelm@25733
    19
struct
wenzelm@25733
    20
wenzelm@25733
    21
type universal = exn;
wenzelm@25733
    22
wenzelm@25733
    23
datatype 'a tag = Tag of
wenzelm@25733
    24
 {is: universal -> bool,
wenzelm@25733
    25
  inject: 'a -> universal,
wenzelm@25733
    26
  project: universal -> 'a};
wenzelm@25733
    27
wenzelm@25733
    28
fun tag () =
wenzelm@25733
    29
  let exception Universal of 'a in
wenzelm@25733
    30
   Tag {
wenzelm@25733
    31
    is = fn Universal _ => true | _ => false,
wenzelm@25733
    32
    inject = Universal,
wenzelm@25733
    33
    project = fn Universal x => x}
wenzelm@25733
    34
  end;
wenzelm@25733
    35
wenzelm@25733
    36
fun tagIs (Tag {is, ...}) = is;
wenzelm@25733
    37
fun tagInject (Tag {inject, ...}) = inject;
wenzelm@25733
    38
fun tagProject (Tag {project, ...}) = project;
wenzelm@25733
    39
wenzelm@25733
    40
end;
wenzelm@25733
    41