src/Pure/ML-Systems/universal.ML
author wenzelm
Sun Jan 30 13:02:18 2011 +0100 (2011-01-30)
changeset 41648 6d736d983d5c
parent 28255 6faea8ad8559
permissions -rw-r--r--
clarified example settings for Proof General;
     1 (*  Title:      Pure/ML-Systems/universal.ML
     2     Author:     Makarius
     3 
     4 Universal values via tagged union.  Emulates structure Universal
     5 from Poly/ML 5.1.
     6 *)
     7 
     8 signature UNIVERSAL =
     9 sig
    10   type universal
    11   type 'a tag
    12   val tag: unit -> 'a tag
    13   val tagIs: 'a tag -> universal -> bool
    14   val tagInject: 'a tag -> 'a -> universal
    15   val tagProject: 'a tag -> universal -> 'a
    16 end;
    17 
    18 structure Universal: UNIVERSAL =
    19 struct
    20 
    21 type universal = exn;
    22 
    23 datatype 'a tag = Tag of
    24  {is: universal -> bool,
    25   inject: 'a -> universal,
    26   project: universal -> 'a};
    27 
    28 fun tag () =
    29   let exception Universal of 'a in
    30    Tag {
    31     is = fn Universal _ => true | _ => false,
    32     inject = Universal,
    33     project = fn Universal x => x}
    34   end;
    35 
    36 fun tagIs (Tag {is, ...}) = is;
    37 fun tagInject (Tag {inject, ...}) = inject;
    38 fun tagProject (Tag {project, ...}) = project;
    39 
    40 end;
    41