summaryrefslogtreecommitdiff
path: root/lib/ur/top.ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-03 14:57:33 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-03 14:57:33 -0400
commite1618fb012b5926889d80893c9ac4ce08838519d (patch)
tree46b157b5c6fb6967e1ab4809f94a6d6505de7411 /lib/ur/top.ur
parentddac92a3d792b7e7342e4003862cd5ff5c1f0ab8 (diff)
outer demo
Diffstat (limited to 'lib/ur/top.ur')
-rw-r--r--lib/ur/top.ur18
1 files changed, 18 insertions, 0 deletions
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)