diff options
author | Adam Chlipala <adam@chlipala.net> | 2010-12-23 17:46:40 -0500 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2010-12-23 17:46:40 -0500 |
commit | 38d3bc508b3b882e81599bdb0e1d4a2572c23dd0 (patch) | |
tree | 31bbf2f979aa12d31eb3977bb6c0cdfe2c57bae9 /lib/ur/top.ur | |
parent | 867a11af44827af8974250e6dbb5e96b6268b44f (diff) |
[De]serialization of times in JavaScript; proper integer division in JavaScript; Basis.crypt; Top.mkRead'; more aggressive Mono-level inlining, for values of function-y types
Diffstat (limited to 'lib/ur/top.ur')
-rw-r--r-- | lib/ur/top.ur | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/lib/ur/top.ur b/lib/ur/top.ur index 32d06a43..19259e92 100644 --- a/lib/ur/top.ur +++ b/lib/ur/top.ur @@ -89,7 +89,7 @@ fun read_option [t ::: Type] (_ : read t) = None => None | v => Some v) -fun txt [t] [ctx ::: {Unit}] [use ::: {Type}] (_ : show t) (v : t) = +fun txt [t] [ctx ::: {Unit}] [use ::: {Type}] (_ : show t) (v : t) : xml ctx use [] = cdata (show v) fun map0 [K] [tf :: K -> Type] (f : t :: K -> tf t) [r ::: {K}] (fl : folder r) = @@ -343,3 +343,8 @@ fun eqNullable' [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}] case e2 of None => (SQL {e1} IS NULL) | Some _ => sql_binary sql_eq e1 (sql_inject e2) + +fun mkRead' [t ::: Type] (f : string -> option t) (name : string) : read t = + mkRead (fn s => case f s of + None => error <xml>Invalid {txt name}: {txt s}</xml> + | Some v => v) f |