From 4dcddbb299324d2c21d591600dfba0845d93cbfe Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 23 Dec 2010 17:46:40 -0500 Subject: [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 --- lib/ur/top.ur | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'lib/ur/top.ur') 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 Invalid {txt name}: {txt s} + | Some v => v) f -- cgit v1.2.3