Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
authorwenzelm
Thu Dec 20 21:12:00 2007 +0100 (2007-12-20 ago)
changeset 257338722d68471ff
parent 25732 308315ee2b6d
child 25734 b00b903ae8ae
Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.
src/Pure/ML-Systems/universal.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/universal.ML	Thu Dec 20 21:12:00 2007 +0100
     1.3 @@ -0,0 +1,42 @@
     1.4 +(*  Title:      Pure/ML-Systems/universal.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Universal values via tagged union.  Emulates structure Universal
     1.9 +in Poly/ML 5.1.
    1.10 +*)
    1.11 +
    1.12 +signature UNIVERSAL =
    1.13 +sig
    1.14 +  type universal
    1.15 +  type 'a tag
    1.16 +  val tag: unit -> 'a tag
    1.17 +  val tagIs: 'a tag -> universal -> bool
    1.18 +  val tagInject: 'a tag -> 'a -> universal
    1.19 +  val tagProject: 'a tag -> universal -> 'a
    1.20 +end;
    1.21 +
    1.22 +structure Universal: UNIVERSAL =
    1.23 +struct
    1.24 +
    1.25 +type universal = exn;
    1.26 +
    1.27 +datatype 'a tag = Tag of
    1.28 + {is: universal -> bool,
    1.29 +  inject: 'a -> universal,
    1.30 +  project: universal -> 'a};
    1.31 +
    1.32 +fun tag () =
    1.33 +  let exception Universal of 'a in
    1.34 +   Tag {
    1.35 +    is = fn Universal _ => true | _ => false,
    1.36 +    inject = Universal,
    1.37 +    project = fn Universal x => x}
    1.38 +  end;
    1.39 +
    1.40 +fun tagIs (Tag {is, ...}) = is;
    1.41 +fun tagInject (Tag {inject, ...}) = inject;
    1.42 +fun tagProject (Tag {project, ...}) = project;
    1.43 +
    1.44 +end;
    1.45 +