diff lib/ur/top.ur @ 777:87a7702d681d

outer demo
author Adam Chlipala <adamc@hcoop.net>
date Sun, 03 May 2009 14:57:33 -0400
parents acb8537f58f0
children d4e811beb8eb
line wrap: on
line diff
--- a/lib/ur/top.ur	Sun May 03 12:49:47 2009 -0400
+++ b/lib/ur/top.ur	Sun May 03 14:57:33 2009 -0400
@@ -71,6 +71,24 @@
 fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type)
             (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x)
 
+fun show_option (t ::: Type) (_ : show t) =
+    mkShow (fn opt : option t =>
+               case opt of
+                   None => ""
+                 | Some x => show x)
+
+fun read_option (t ::: Type) (_ : read t) =
+    mkRead (fn s =>
+               case s of
+                   "" => None
+                 | _ => Some (readError s : t))
+           (fn s =>
+               case s of
+                   "" => Some None
+                 | _ => case read s of
+                            None => None
+                          | v => Some v)
+
 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) =
     cdata (show v)