[MLton-commit] r7215

[Vesa Karvonen]

Added phantom booleans for expressing arbitrary finite relations at the
type level.

----------------------------------------------------------------------

U   mltonlib/trunk/com/ssh/extended-basis/unstable/detail/typing/phantom.sml
U   mltonlib/trunk/com/ssh/extended-basis/unstable/public/export/top-level.sml
U   mltonlib/trunk/com/ssh/extended-basis/unstable/public/typing/phantom.sig

----------------------------------------------------------------------

Modified: mltonlib/trunk/com/ssh/extended-basis/unstable/detail/typing/phantom.sml
===================================================================
--- mltonlib/trunk/com/ssh/extended-basis/unstable/detail/typing/phantom.sml	2009-07-11 16:49:39 UTC (rev 7214)
+++ mltonlib/trunk/com/ssh/extended-basis/unstable/detail/typing/phantom.sml	2009-07-11 19:41:36 UTC (rev 7215)
@@ -1,4 +1,4 @@
-(* Copyright (C) 2007 Vesa Karvonen
+(* Copyright (C) 2007-2009 Vesa Karvonen
  *
  * This code is released under the MLton license, a BSD-style license.
  * See the LICENSE file or http://mlton.org/License for details.
@@ -7,4 +7,18 @@
 structure Phantom :> PHANTOM = struct
    type yes = unit
    type no  = unit
+
+   structure Bool = struct
+      type ('f, 't, 'r) t = unit
+      type ('f, 't) T = unit
+      type ('f, 't) F = unit
+      val t = ()
+      val f = ()
+      fun split () = ((), ())
+      val generalize = ignore
+      fun iff _ = raise Fail "Phantom.Bool.iff"
+      val notb = ignore
+      val op andb = ignore
+      val op orb = ignore
+   end
 end

Modified: mltonlib/trunk/com/ssh/extended-basis/unstable/public/export/top-level.sml
===================================================================
--- mltonlib/trunk/com/ssh/extended-basis/unstable/public/export/top-level.sml	2009-07-11 16:49:39 UTC (rev 7214)
+++ mltonlib/trunk/com/ssh/extended-basis/unstable/public/export/top-level.sml	2009-07-11 19:41:36 UTC (rev 7215)
@@ -94,6 +94,10 @@
    type yes = Phantom.yes
    type no = Phantom.no
 
+   type ('f, 't, 'r) B = ('f, 't, 'r) Phantom.Bool.t
+   type ('f, 't) T = ('f, 't) Phantom.Bool.T
+   type ('f, 't) F = ('f, 't) Phantom.Bool.F
+
    (** == Product == *)
 
    datatype product = datatype Product.product

Modified: mltonlib/trunk/com/ssh/extended-basis/unstable/public/typing/phantom.sig
===================================================================
--- mltonlib/trunk/com/ssh/extended-basis/unstable/public/typing/phantom.sig	2009-07-11 16:49:39 UTC (rev 7214)
+++ mltonlib/trunk/com/ssh/extended-basis/unstable/public/typing/phantom.sig	2009-07-11 19:41:36 UTC (rev 7215)
@@ -1,4 +1,4 @@
-(* Copyright (C) 2007 Vesa Karvonen
+(* Copyright (C) 2007-2009 Vesa Karvonen
  *
  * This code is released under the MLton license, a BSD-style license.
  * See the LICENSE file or http://mlton.org/License for details.
@@ -10,5 +10,46 @@
  *)
 signature PHANTOM = sig
    type yes
-   type no 
+   type no
+
+   (** Substructure for phantom booleans and type-level conditionals. *)
+   structure Bool : sig
+      type ('f, 't, 'r) t
+      (**
+       * Type constructor for phantom booleans.
+       *)
+
+      type ('f, 't) T = ('f, 't, 't) t (** {true} *)
+      type ('f, 't) F = ('f, 't, 'f) t (** {false} *)
+
+      (** == Term Level Operations ==
+       *
+       * These are not normally used in actual programs.  However, these
+       * can be used to exploit the SML type checker to compute type
+       * expressions involving phantom booleans.
+       *)
+
+      val t : ('f, 't) T
+      val f : ('f, 't) F
+
+      val split : (('f1, 't1) F * ('f2, 't2) F,
+                   ('f3, 't3) T * ('f4, 't4) T,
+                   ('f5, 't5, 'r5) t * ('f6, 't6, 'r6) t) t ->
+                  ('f5, 't5, 'r5) t * ('f6, 't6, 'r6) t
+
+      val generalize :
+          (('f1, 't1) F, ('f2, 't2) T, ('f, 't, 'r) t) t -> ('f, 't, 'r) t
+
+      val iff : ('f, 't, 'r) t -> 't -> 'f -> 'r
+      (** Does not return. *)
+
+      val notb : (('f1, 't1) T, ('f2, 't2) F, ('f, 't, 'r) t) t
+                 -> ('f, 't, 'r) t
+      val andb : (('f1, 't1) F * ('f2, 't2) F, ('f3, 't3) F * ('f4, 't4) T,
+                  'a * 'b) t * ('a, 'b, ('f, 't, 'r) t) t
+                 -> ('f, 't, 'r) t
+      val orb : (('f1, 't1) F * ('f2, 't2) T, ('f3, 't3) T * ('f4, 't4) T,
+                 'a * 'b) t * ('a, 'b, ('f, 't, 'r) t) t
+                -> ('f, 't, 'r) t
+   end
 end