diff options
author | Adam Chlipala <adamc@hcoop.net> | 2009-05-03 14:57:33 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2009-05-03 14:57:33 -0400 |
commit | e1618fb012b5926889d80893c9ac4ce08838519d (patch) | |
tree | 46b157b5c6fb6967e1ab4809f94a6d6505de7411 /lib | |
parent | ddac92a3d792b7e7342e4003862cd5ff5c1f0ab8 (diff) |
outer demo
Diffstat (limited to 'lib')
-rw-r--r-- | lib/ur/basis.urs | 1 | ||||
-rw-r--r-- | lib/ur/top.ur | 18 | ||||
-rw-r--r-- | lib/ur/top.urs | 3 |
3 files changed, 22 insertions, 0 deletions
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 [] |