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