From e1618fb012b5926889d80893c9ac4ce08838519d Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Sun, 3 May 2009 14:57:33 -0400
Subject: outer demo

---
 lib/ur/basis.urs |  1 +
 lib/ur/top.ur    | 18 ++++++++++++++++++
 lib/ur/top.urs   |  3 +++
 3 files changed, 22 insertions(+)

(limited to 'lib')

diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index ea4432cd..9736ce1e 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -70,6 +70,7 @@ val read_float : read float
 val read_string : read string
 val read_bool : read bool
 val read_time : read time
+val mkRead : t ::: Type -> (string -> t) -> (string -> option t) -> read t
 
 
 (** * Monads *)
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index b9728158..f9b3d033 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -71,6 +71,24 @@ fun ex (tf :: (Type -> Type)) (choice :: Type) (body : tf choice) : ex tf =
 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)
 
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index 60b6dac2..4ed64075 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -39,6 +39,9 @@ val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf
 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type
               -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3)
 
+val show_option : t ::: Type -> show t -> show (option t)
+val read_option : t ::: Type -> read t -> read (option t)
+
 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
           -> xml ctx use []
 
-- 
cgit v1.2.3