summaryrefslogtreecommitdiff
path: root/lib/ur
diff options
context:
space:
mode:
Diffstat (limited to 'lib/ur')
-rw-r--r--lib/ur/basis.urs1207
-rw-r--r--lib/ur/char.ur19
-rw-r--r--lib/ur/char.urs19
-rw-r--r--lib/ur/datetime.ur135
-rw-r--r--lib/ur/datetime.urs38
-rw-r--r--lib/ur/json.ur387
-rw-r--r--lib/ur/json.urs31
-rw-r--r--lib/ur/list.ur498
-rw-r--r--lib/ur/list.urs116
-rw-r--r--lib/ur/listPair.ur46
-rw-r--r--lib/ur/listPair.urs10
-rw-r--r--lib/ur/monad.ur140
-rw-r--r--lib/ur/monad.urs90
-rw-r--r--lib/ur/option.ur61
-rw-r--r--lib/ur/option.urs16
-rw-r--r--lib/ur/string.ur113
-rw-r--r--lib/ur/string.urs37
-rw-r--r--lib/ur/top.ur430
-rw-r--r--lib/ur/top.urs303
19 files changed, 3696 insertions, 0 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
new file mode 100644
index 0000000..89a48d5
--- /dev/null
+++ b/lib/ur/basis.urs
@@ -0,0 +1,1207 @@
+type int
+type float
+type string
+type char
+type time
+type blob
+
+type unit = {}
+
+datatype bool = False | True
+
+datatype option t = None | Some of t
+
+datatype list t = Nil | Cons of t * list t
+
+
+(** Polymorphic variants *)
+
+con variant :: {Type} -> Type
+val make : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => t -> variant ([nm = t] ++ ts)
+val match : ts ::: {Type} -> t ::: Type -> variant ts -> $(map (fn t' => t' -> t) ts) -> t
+
+
+(** Basic type classes *)
+
+class eq
+val eq : t ::: Type -> eq t -> t -> t -> bool
+val ne : t ::: Type -> eq t -> t -> t -> bool
+val eq_int : eq int
+val eq_float : eq float
+val eq_string : eq string
+val eq_char : eq char
+val eq_bool : eq bool
+val eq_time : eq time
+val mkEq : t ::: Type -> (t -> t -> bool) -> eq t
+
+class num
+val zero : t ::: Type -> num t -> t
+val neg : t ::: Type -> num t -> t -> t
+val plus : t ::: Type -> num t -> t -> t -> t
+val minus : t ::: Type -> num t -> t -> t -> t
+val times : t ::: Type -> num t -> t -> t -> t
+val divide : t ::: Type -> num t -> t -> t -> t
+val mod : t ::: Type -> num t -> t -> t -> t
+val pow : t ::: Type -> num t -> t -> t -> t
+val num_int : num int
+val num_float : num float
+
+class ord
+val lt : t ::: Type -> ord t -> t -> t -> bool
+val le : t ::: Type -> ord t -> t -> t -> bool
+val gt : t ::: Type -> ord t -> t -> t -> bool
+val ge : t ::: Type -> ord t -> t -> t -> bool
+val ord_int : ord int
+val ord_float : ord float
+val ord_string : ord string
+val ord_char : ord char
+val ord_bool : ord bool
+val ord_time : ord time
+val mkOrd : t ::: Type -> {Lt : t -> t -> bool, Le : t -> t -> bool} -> ord t
+
+
+(** Character operations *)
+
+val isalnum : char -> bool
+val isalpha : char -> bool
+val isblank : char -> bool
+val iscntrl : char -> bool
+val isdigit : char -> bool
+val isgraph : char -> bool
+val islower : char -> bool
+val isprint : char -> bool
+val ispunct : char -> bool
+val isspace : char -> bool
+val isupper : char -> bool
+val isxdigit : char -> bool
+val tolower : char -> char
+val toupper : char -> char
+val ord : char -> int
+val chr : int -> char
+
+(** String operations *)
+
+val strlen : string -> int
+val strlenGe : string -> int -> bool
+val strcat : string -> string -> string
+val strsub : string -> int -> char
+val strsuffix : string -> int -> string
+val strchr : string -> char -> option string
+val strindex : string -> char -> option int
+val strsindex : string -> string -> option int
+val strcspn : string -> string -> int
+val substring : string -> int -> int -> string
+val str1 : char -> string
+
+class show
+val show : t ::: Type -> show t -> t -> string
+val show_int : show int
+val show_float : show float
+val show_string : show string
+val show_char : show char
+val show_bool : show bool
+val show_time : show time
+val mkShow : t ::: Type -> (t -> string) -> show t
+
+class read
+val read : t ::: Type -> read t -> string -> option t
+val readError : t ::: Type -> read t -> string -> t
+(* [readError] calls [error] if the input is malformed. *)
+val read_int : read int
+val read_float : read float
+val read_string : read string
+val read_char : read char
+val read_bool : read bool
+val read_time : read time
+val mkRead : t ::: Type -> (string -> t) -> (string -> option t) -> read t
+
+
+(** * Monads *)
+
+class monad :: (Type -> Type) -> Type
+val return : m ::: (Type -> Type) -> t ::: Type
+ -> monad m
+ -> t -> m t
+val bind : m ::: (Type -> Type) -> t1 ::: Type -> t2 ::: Type
+ -> monad m
+ -> m t1 -> (t1 -> m t2)
+ -> m t2
+
+val mkMonad : m ::: (Type -> Type)
+ -> {Return : t ::: Type -> t -> m t,
+ Bind : t1 ::: Type -> t2 ::: Type -> m t1 -> (t1 -> m t2) -> m t2}
+ -> monad m
+
+con transaction :: Type -> Type
+val transaction_monad : monad transaction
+
+con source :: Type -> Type
+val source : t ::: Type -> t -> transaction (source t)
+val set : t ::: Type -> source t -> t -> transaction unit
+val get : t ::: Type -> source t -> transaction t
+
+con signal :: Type -> Type
+val signal_monad : monad signal
+val signal : t ::: Type -> source t -> signal t
+val current : t ::: Type -> signal t -> transaction t
+
+
+(** * Floats *)
+
+val float : int -> float
+val ceil : float -> int
+val trunc : float -> int
+val round : float -> int
+val floor : float -> int
+
+(** * Basic Math *)
+
+val sqrt : float -> float
+val sin : float -> float
+val cos : float -> float
+val log : float -> float
+val exp : float -> float
+val asin : float -> float
+val acos : float -> float
+val atan : float -> float
+val atan2 : float -> float -> float
+val abs: float -> float
+
+(** * Time *)
+
+val now : transaction time
+val minTime : time
+val addSeconds : time -> int -> time
+val toSeconds : time -> int
+val diffInSeconds : time -> time -> int
+(* Earlier time first *)
+val toMilliseconds : time -> int
+val fromMilliseconds : int -> time
+val diffInMilliseconds : time -> time -> int
+val timef : string -> time -> string (* Uses strftime() format string *)
+val readUtc : string -> option time
+
+(* Takes a year, month, day, hour, minute, second. *)
+val fromDatetime : int -> int -> int -> int -> int -> int -> time
+val datetimeYear : time -> int
+val datetimeMonth : time -> int
+val datetimeDay : time -> int
+val datetimeHour : time -> int
+val datetimeMinute: time -> int
+val datetimeSecond : time -> int
+val datetimeDayOfWeek : time -> int
+
+
+(** * Encryption *)
+
+val crypt : string -> string -> string
+
+
+(** HTTP operations *)
+
+con http_cookie :: Type -> Type
+val getCookie : t ::: Type -> http_cookie t -> transaction (option t)
+val setCookie : t ::: Type -> http_cookie t -> {Value : t,
+ Expires : option time,
+ Secure : bool} -> transaction unit
+val clearCookie : t ::: Type -> http_cookie t -> transaction unit
+
+type requestHeader
+val blessRequestHeader : string -> requestHeader
+val checkRequestHeader : string -> option requestHeader
+val getHeader : requestHeader -> transaction (option string)
+
+type responseHeader
+val blessResponseHeader : string -> responseHeader
+val checkResponseHeader : string -> option responseHeader
+val setHeader : responseHeader -> string -> transaction unit
+
+type envVar
+val blessEnvVar : string -> envVar
+val checkEnvVar : string -> option envVar
+val getenv : envVar -> transaction (option string)
+
+type meta
+val blessMeta : string -> meta
+val checkMeta : string -> option meta
+
+
+(** JavaScript-y gadgets *)
+
+val alert : string -> transaction unit
+val confirm : string -> transaction bool
+val spawn : transaction unit -> transaction unit
+val sleep : int -> transaction unit
+
+val rpc : t ::: Type -> transaction t -> transaction t
+val tryRpc : t ::: Type -> transaction t -> transaction (option t)
+(* Returns [None] on error condition. *)
+
+
+(** Channels *)
+
+con channel :: Type -> Type
+val channel : t ::: Type -> transaction (channel t)
+val send : t ::: Type -> channel t -> t -> transaction unit
+val recv : t ::: Type -> channel t -> transaction t
+
+type client
+val self : transaction client
+
+
+(** SQL *)
+
+con sql_table :: {Type} -> {{Unit}} -> Type
+con sql_view :: {Type} -> Type
+
+class fieldsOf :: Type -> {Type} -> Type
+val fieldsOf_table : fs ::: {Type} -> keys ::: {{Unit}}
+ -> fieldsOf (sql_table fs keys) fs
+val fieldsOf_view : fs ::: {Type}
+ -> fieldsOf (sql_view fs) fs
+
+(*** Constraints *)
+
+(**** Primary keys *)
+
+class sql_injectable_prim
+val sql_bool : sql_injectable_prim bool
+val sql_int : sql_injectable_prim int
+val sql_float : sql_injectable_prim float
+val sql_string : sql_injectable_prim string
+val sql_char : sql_injectable_prim char
+val sql_time : sql_injectable_prim time
+val sql_blob : sql_injectable_prim blob
+val sql_channel : t ::: Type -> sql_injectable_prim (channel t)
+val sql_client : sql_injectable_prim client
+
+con serialized :: Type -> Type
+val serialize : t ::: Type -> t -> serialized t
+val deserialize : t ::: Type -> serialized t -> t
+val sql_serialized : t ::: Type -> sql_injectable_prim (serialized t)
+
+con primary_key :: {Type} -> {{Unit}} -> Type
+val no_primary_key : fs ::: {Type} -> primary_key fs []
+val primary_key : rest ::: {Type} -> t ::: Type -> key1 :: Name -> keys :: {Type}
+ -> [[key1] ~ keys] => [[key1 = t] ++ keys ~ rest]
+ => $([key1 = sql_injectable_prim t] ++ map sql_injectable_prim keys)
+ -> primary_key ([key1 = t] ++ keys ++ rest)
+ [Pkey = [key1] ++ map (fn _ => ()) keys]
+
+(**** Other constraints *)
+
+con sql_constraints :: {Type} -> {{Unit}} -> Type
+(* Arguments: column types, uniqueness implications of constraints *)
+
+con sql_constraint :: {Type} -> {Unit} -> Type
+
+val no_constraint : fs ::: {Type} -> sql_constraints fs []
+val one_constraint : fs ::: {Type} -> unique ::: {Unit} -> name :: Name
+ -> sql_constraint fs unique
+ -> sql_constraints fs [name = unique]
+val join_constraints : fs ::: {Type}
+ -> uniques1 ::: {{Unit}} -> uniques2 ::: {{Unit}} -> [uniques1 ~ uniques2]
+ => sql_constraints fs uniques1 -> sql_constraints fs uniques2
+ -> sql_constraints fs (uniques1 ++ uniques2)
+
+
+val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type}
+ -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest]
+ => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique)
+
+class linkable :: Type -> Type -> Type
+val linkable_same : t ::: Type -> linkable t t
+val linkable_from_nullable : t ::: Type -> linkable (option t) t
+val linkable_to_nullable : t ::: Type -> linkable t (option t)
+
+con matching :: {Type} -> {Type} -> Type
+val mat_nil : matching [] []
+val mat_cons : t1 ::: Type -> rest1 ::: {Type} -> t2 ::: Type -> rest2 ::: {Type}
+ -> nm1 :: Name -> nm2 :: Name
+ -> [[nm1] ~ rest1] => [[nm2] ~ rest2]
+ => linkable t1 t2
+ -> matching rest1 rest2
+ -> matching ([nm1 = t1] ++ rest1) ([nm2 = t2] ++ rest2)
+
+con propagation_mode :: {Type} -> Type
+val restrict : fs ::: {Type} -> propagation_mode fs
+val cascade : fs ::: {Type} -> propagation_mode fs
+val no_action : fs ::: {Type} -> propagation_mode fs
+val set_null : fs ::: {Type} -> propagation_mode (map option fs)
+
+
+val foreign_key : mine1 ::: Name -> t ::: Type -> mine ::: {Type} -> munused ::: {Type}
+ -> foreign ::: {Type} -> funused ::: {Type}
+ -> nm ::: Name -> uniques ::: {{Unit}}
+ -> [[mine1] ~ mine] => [[mine1 = t] ++ mine ~ munused]
+ => [foreign ~ funused] => [[nm] ~ uniques]
+ => matching ([mine1 = t] ++ mine) foreign
+ -> sql_table (foreign ++ funused) ([nm = map (fn _ => ()) foreign] ++ uniques)
+ -> {OnDelete : propagation_mode ([mine1 = t] ++ mine),
+ OnUpdate : propagation_mode ([mine1 = t] ++ mine)}
+ -> sql_constraint ([mine1 = t] ++ mine ++ munused) []
+
+con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
+val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
+ -> fs' ::: {{Type}} -> agg' ::: {{Type}} -> exps' ::: {Type}
+ -> [fs ~ fs'] => [agg ~ agg'] => [exps ~ exps'] =>
+ sql_exp fs agg exps t
+ -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') t
+
+val check : fs ::: {Type}
+ -> sql_exp [] [] fs bool
+ -> sql_constraint fs []
+
+
+(*** Queries *)
+
+con sql_query :: {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
+con sql_query1 :: {{Type}} -> {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
+
+con sql_subset :: {{Type}} -> {{Type}} -> Type
+val sql_subset : keep_drop :: {({Type} * {Type})}
+ -> sql_subset
+ (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop)
+ (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop)
+val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables
+val sql_subset_concat : big1 ::: {{Type}} -> little1 ::: {{Type}}
+ -> big2 ::: {{Type}} -> little2 ::: {{Type}}
+ -> [big1 ~ big2] => [little1 ~ little2] =>
+ sql_subset big1 little1
+ -> sql_subset big2 little2
+ -> sql_subset (big1 ++ big2) (little1 ++ little2)
+
+con sql_from_items :: {{Type}} -> {{Type}} -> Type
+
+val sql_from_nil : free ::: {{Type}} -> sql_from_items free []
+val sql_from_table : free ::: {{Type}} -> t ::: Type -> fs ::: {Type}
+ -> fieldsOf t fs -> name :: Name
+ -> t -> sql_from_items free [name = fs]
+val sql_from_query : free ::: {{Type}} -> fs ::: {Type} -> name :: Name
+ -> sql_query free [] [] fs
+ -> sql_from_items free [name = fs]
+val sql_from_comma : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
+ -> [tabs1 ~ tabs2]
+ => sql_from_items free tabs1 -> sql_from_items free tabs2
+ -> sql_from_items free (tabs1 ++ tabs2)
+val sql_inner_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
+ -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
+ => sql_from_items free tabs1 -> sql_from_items free tabs2
+ -> sql_exp (free ++ tabs1 ++ tabs2) [] [] bool
+ -> sql_from_items free (tabs1 ++ tabs2)
+
+class nullify :: Type -> Type -> Type
+val nullify_option : t ::: Type -> nullify (option t) (option t)
+val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t)
+
+val sql_left_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}}
+ -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
+ => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2)
+ -> sql_from_items free tabs1 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
+ -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool
+ -> sql_from_items free (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
+
+val sql_right_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}}
+ -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
+ => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1)
+ -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items free tabs2
+ -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool
+ -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
+
+val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
+ -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
+ => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2))
+ -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1)
+ -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
+ -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool
+ -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
+
+(** [ORDER BY] and [SELECT] expressions may use window functions, so we introduce a type family for such expressions. *)
+con sql_expw :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
+
+val sql_query1 : free ::: {{Type}}
+ -> afree ::: {{Type}}
+ -> tables ::: {{Type}}
+ -> grouped ::: {{Type}}
+ -> selectedFields ::: {{Type}}
+ -> selectedExps ::: {Type}
+ -> empties :: {Unit}
+ -> [free ~ tables]
+ => [free ~ grouped]
+ => [afree ~ tables]
+ => [empties ~ selectedFields]
+ => {Distinct : bool,
+ From : sql_from_items free tables,
+ Where : sql_exp (free ++ tables) afree [] bool,
+ GroupBy : sql_subset tables grouped,
+ Having : sql_exp (free ++ grouped) (afree ++ tables) [] bool,
+ SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields),
+ SelectExps : $(map (sql_expw (free ++ grouped) (afree ++ tables) [])
+ selectedExps) }
+ -> sql_query1 free afree tables selectedFields selectedExps
+
+type sql_relop
+val sql_union : sql_relop
+val sql_intersect : sql_relop
+val sql_except : sql_relop
+val sql_relop : free ::: {{Type}}
+ -> afree ::: {{Type}}
+ -> tables1 ::: {{Type}}
+ -> tables2 ::: {{Type}}
+ -> selectedFields ::: {{Type}}
+ -> selectedExps ::: {Type}
+ -> sql_relop
+ -> bool (* ALL *)
+ -> sql_query1 free afree tables1 selectedFields selectedExps
+ -> sql_query1 free afree tables2 selectedFields selectedExps
+ -> sql_query1 free afree [] selectedFields selectedExps
+val sql_forget_tables : free ::: {{Type}} -> afree ::: {{Type}} -> tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type}
+ -> sql_query1 free afree tables selectedFields selectedExps
+ -> sql_query1 free afree [] selectedFields selectedExps
+
+type sql_direction
+val sql_asc : sql_direction
+val sql_desc : sql_direction
+
+(** This type class supports automatic injection of either regular or window expressions into [sql_expw]. *)
+class sql_window :: ({{Type}} -> {{Type}} -> {Type} -> Type -> Type) -> Type
+val sql_window_normal : sql_window sql_exp
+val sql_window_fancy : sql_window sql_expw
+val sql_window : tf ::: ({{Type}} -> {{Type}} -> {Type} -> Type -> Type)
+ -> tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
+ -> sql_window tf
+ -> tf tables agg exps t
+ -> sql_expw tables agg exps t
+
+con sql_order_by :: {{Type}} -> {Type} -> Type
+val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
+val sql_order_by_Cons : tf ::: ({{Type}} -> {{Type}} -> {Type} -> Type -> Type) -> tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
+ -> sql_window tf
+ -> tf tables [] exps t -> sql_direction
+ -> sql_order_by tables exps
+ -> sql_order_by tables exps
+val sql_order_by_random : tables ::: {{Type}} -> exps ::: {Type}
+ -> sql_order_by tables exps
+
+type sql_limit
+val sql_no_limit : sql_limit
+val sql_limit : int -> sql_limit
+
+type sql_offset
+val sql_no_offset : sql_offset
+val sql_offset : int -> sql_offset
+
+val sql_query : free ::: {{Type}}
+ -> afree ::: {{Type}}
+ -> tables ::: {{Type}}
+ -> selectedFields ::: {{Type}}
+ -> selectedExps ::: {Type}
+ -> [free ~ tables]
+ => {Rows : sql_query1 free afree tables selectedFields selectedExps,
+ OrderBy : sql_order_by (free ++ tables) selectedExps,
+ Limit : sql_limit,
+ Offset : sql_offset}
+ -> sql_query free afree selectedFields selectedExps
+
+val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
+ -> fieldType ::: Type -> agg ::: {{Type}}
+ -> exps ::: {Type}
+ -> tab :: Name -> field :: Name
+ -> sql_exp
+ ([tab = [field = fieldType] ++ otherFields] ++ otherTabs)
+ agg exps fieldType
+
+val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type}
+ -> nm :: Name
+ -> sql_exp tabs agg ([nm = t] ++ rest) t
+
+class sql_injectable
+val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t
+val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)
+
+val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type
+ -> sql_injectable t -> t -> sql_exp tables agg exps t
+
+val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type
+ -> sql_exp tables agg exps (option t)
+ -> sql_exp tables agg exps bool
+
+val sql_coalesce : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type
+ -> sql_exp tables agg exps (option t)
+ -> sql_exp tables agg exps t
+ -> sql_exp tables agg exps t
+
+val sql_if_then_else : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type
+ -> sql_exp tables agg exps bool
+ -> sql_exp tables agg exps t
+ -> sql_exp tables agg exps t
+ -> sql_exp tables agg exps t
+
+class sql_arith
+val sql_arith_int : sql_arith int
+val sql_arith_float : sql_arith float
+val sql_arith_option : t ::: Type -> sql_arith t -> sql_arith (option t)
+
+con sql_unary :: Type -> Type -> Type
+val sql_not : sql_unary bool bool
+val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> arg ::: Type -> res ::: Type
+ -> sql_unary arg res -> sql_exp tables agg exps arg
+ -> sql_exp tables agg exps res
+
+val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t
+
+con sql_binary :: Type -> Type -> Type -> Type
+val sql_and : sql_binary bool bool bool
+val sql_or : sql_binary bool bool bool
+val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
+ -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1
+ -> sql_exp tables agg exps arg2
+ -> sql_exp tables agg exps res
+
+val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t
+val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t
+val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t
+val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t
+val sql_mod : sql_binary int int int
+
+val sql_eq : t ::: Type -> sql_binary t t bool
+(* Note that the semantics of this operator on nullable types are different than for standard SQL!
+ * Instead, we do it the sane way, where [NULL = NULL]. *)
+
+val sql_ne : t ::: Type -> sql_binary t t bool
+val sql_lt : t ::: Type -> sql_binary t t bool
+val sql_le : t ::: Type -> sql_binary t t bool
+val sql_gt : t ::: Type -> sql_binary t t bool
+val sql_ge : t ::: Type -> sql_binary t t bool
+
+val sql_like : sql_binary string string bool
+
+val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> sql_exp tables agg exps int
+
+con sql_aggregate :: Type -> Type -> Type
+val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> dom ::: Type -> ran ::: Type
+ -> sql_aggregate dom ran -> sql_exp agg agg exps dom
+ -> sql_exp tables agg exps ran
+
+val sql_count_col : t ::: Type -> sql_aggregate (option t) int
+
+class sql_summable
+val sql_summable_int : sql_summable int
+val sql_summable_float : sql_summable float
+val sql_summable_option : t ::: Type -> sql_summable t -> sql_summable (option t)
+val sql_avg : t ::: Type -> sql_summable t -> sql_aggregate t (option float)
+val sql_sum : t ::: Type -> nt ::: Type -> sql_summable t -> nullify t nt -> sql_aggregate t nt
+
+class sql_maxable
+val sql_maxable_int : sql_maxable int
+val sql_maxable_float : sql_maxable float
+val sql_maxable_string : sql_maxable string
+val sql_maxable_time : sql_maxable time
+val sql_maxable_option : t ::: Type -> sql_maxable t -> sql_maxable (option t)
+val sql_max : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
+val sql_min : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
+
+con sql_nfunc :: Type -> Type
+val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type
+ -> sql_nfunc t -> sql_exp tables agg exps t
+val sql_current_timestamp : sql_nfunc time
+
+con sql_ufunc :: Type -> Type -> Type
+val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> dom ::: Type -> ran ::: Type
+ -> sql_ufunc dom ran -> sql_exp tables agg exps dom
+ -> sql_exp tables agg exps ran
+val sql_octet_length : sql_ufunc blob int
+val sql_known : t ::: Type -> sql_ufunc t bool
+val sql_lower : sql_ufunc string string
+val sql_upper : sql_ufunc string string
+
+val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
+ -> sql_injectable_prim t
+ -> sql_exp tables agg exps t
+ -> sql_exp tables agg exps (option t)
+
+val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type -> nt ::: Type
+ -> nullify t nt
+ -> sql_query tables agg [] [nm = t]
+ -> sql_exp tables agg exps nt
+
+(** Window function expressions *)
+
+con sql_partition :: {{Type}} -> {{Type}} -> {Type} -> Type
+val sql_no_partition : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> sql_partition tables agg exps
+val sql_partition : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
+ -> sql_exp tables agg exps t
+ -> sql_partition tables agg exps
+
+con sql_window_function :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
+val sql_window_function : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type
+ -> sql_window_function tables agg exps t
+ -> sql_partition tables agg exps
+ -> sql_order_by tables exps
+ -> sql_expw tables agg exps t
+
+val sql_window_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type -> nt ::: Type
+ -> sql_aggregate t nt
+ -> sql_exp tables agg exps t
+ -> sql_window_function tables agg exps nt
+val sql_window_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> sql_window_function tables agg exps int
+val sql_rank : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> sql_window_function tables agg exps int
+
+
+(*** Executing queries *)
+
+val query : tables ::: {{Type}} -> exps ::: {Type}
+ -> [tables ~ exps] =>
+ state ::: Type
+ -> sql_query [] [] tables exps
+ -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
+ -> state
+ -> transaction state)
+ -> state
+ -> transaction state
+
+val show_sql_query : freeTables ::: {{Type}} -> freeAggs ::: {{Type}} -> tables ::: {{Type}} -> exps ::: {Type}
+ -> show (sql_query freeTables freeAggs tables exps)
+
+
+(*** Database mutators *)
+
+type dml
+val dml : dml -> transaction unit
+val tryDml : dml -> transaction (option string)
+(* Returns an error message on failure. *)
+
+val insert : fields ::: {Type} -> uniques ::: {{Unit}}
+ -> sql_table fields uniques
+ -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
+ -> dml
+
+val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} ->
+ [changed ~ unchanged] =>
+ $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
+ -> sql_table (changed ++ unchanged) uniques
+ -> sql_exp [T = changed ++ unchanged] [] [] bool
+ -> dml
+
+val delete : fields ::: {Type} -> uniques ::: {{Unit}}
+ -> sql_table fields uniques
+ -> sql_exp [T = fields] [] [] bool
+ -> dml
+
+(*** Sequences *)
+
+type sql_sequence
+val nextval : sql_sequence -> transaction int
+val setval : sql_sequence -> int -> transaction unit
+
+
+(** XML *)
+
+type css_class
+val show_css_class : show css_class
+val null : css_class
+(* No special formatting *)
+val classes : css_class -> css_class -> css_class
+(* The equivalent of writing one class after the other, separated by a space, in
+ * an HTML 'class' attribute *)
+
+type css_value
+val atom : string -> css_value
+type url
+val css_url : url -> css_value
+val sql_url : sql_injectable_prim url
+type css_property
+val property : string -> css_property
+val value : css_property -> css_value -> css_property
+type css_style
+val noStyle : css_style
+val oneProperty : css_style -> css_property -> css_style
+
+con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
+
+con xml :: {Unit} -> {Type} -> {Type} -> Type
+val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
+val cdataChar : ctx ::: {Unit} -> use ::: {Type} -> char -> xml ctx use []
+val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type}
+ -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
+ -> useOuter ::: {Type} -> useInner ::: {Type}
+ -> bindOuter ::: {Type} -> bindInner ::: {Type}
+ -> [attrsGiven ~ attrsAbsent] =>
+ [useOuter ~ useInner] =>
+ [bindOuter ~ bindInner] =>
+ css_class
+ -> option (signal css_class)
+ -> css_style
+ -> option (signal css_style)
+ -> $attrsGiven
+ -> tag (attrsGiven ++ attrsAbsent)
+ ctxOuter ctxInner useOuter bindOuter
+ -> xml ctxInner useInner bindInner
+ -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
+val join : ctx ::: {Unit}
+ -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
+ -> [use1 ~ bind1] => [bind1 ~ bind2] =>
+ xml ctx use1 bind1
+ -> xml ctx (use1 ++ bind1) bind2
+ -> xml ctx use1 (bind1 ++ bind2)
+val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type}
+ -> bind ::: {Type}
+ -> [use1 ~ use2] =>
+ xml ctx use1 bind
+ -> xml ctx (use1 ++ use2) bind
+
+con html = [Html]
+con head = [Head]
+
+con body' = [MakeForm, Body]
+con form' = [Body, Form]
+con subform' = [Body, Subform]
+con tabl' = [MakeForm, Table]
+con tr' = [MakeForm, Tr]
+
+con body = [Dyn] ++ body'
+con form = [Dyn] ++ form'
+con subform = [Dyn] ++ subform'
+con tabl = [Dyn] ++ tabl'
+con tr = [Dyn] ++ tr'
+
+con xhtml = xml html
+con page = xhtml [] []
+con xbody = xml body [] []
+con xhead = xml head [] []
+con xtable = xml tabl [] []
+con xtr = xml tr [] []
+con xform = xml form [] []
+
+
+(*** HTML details *)
+
+type queryString
+val show_queryString : show queryString
+
+val show_url : show url
+val bless : string -> url
+val checkUrl : string -> option url
+val currentUrl : transaction url
+val currentUrlHasPost : transaction bool
+val currentUrlHasQueryString : transaction bool
+val url : transaction page -> url
+val effectfulUrl : (option queryString -> transaction page) -> url
+val redirect : t ::: Type -> url -> transaction t
+
+type id
+val fresh : transaction id
+val giveFocus : id -> transaction unit
+val show_id : show id
+
+val dyn : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> [ctx ~ [Dyn]] => unit
+ -> tag [Signal = signal (xml ([Dyn] ++ ctx) use bind)] ([Dyn] ++ ctx) [] use bind
+
+val active : unit
+ -> tag [Code = transaction xbody] body [] [] []
+
+val script : unit
+ -> tag [Code = transaction unit] head [] [] []
+
+(* Type for HTML5 "data-*" and "aria-*" attributes. *)
+type data_attr_kind
+val data_kind : data_attr_kind
+val aria_kind : data_attr_kind
+
+type data_attr
+val data_attr : data_attr_kind -> string (* Key *) -> string (* Value *) -> data_attr
+(* This function will fail if the key doesn't meet HTML's lexical rules! *)
+val data_attrs : data_attr -> data_attr -> data_attr
+
+val head : unit -> tag [Data = data_attr] html head [] []
+val title : unit -> tag [Data = data_attr] head [] [] []
+val link : unit -> tag [Data = data_attr, Id = id, Rel = string, Typ = string, Href = url, Media = string, Integrity = string, Crossorigin = string] head [] [] []
+val meta : unit -> tag [Nam = meta, Content = string, Id = id] head [] [] []
+
+datatype mouseButton = Left | Right | Middle
+
+type mouseEvent = { ScreenX : int, ScreenY : int, ClientX : int, ClientY : int,
+ CtrlKey : bool, ShiftKey : bool, AltKey : bool, MetaKey : bool,
+ Button : mouseButton }
+
+con mouseEvents = map (fn _ :: Unit => mouseEvent -> transaction unit)
+ [Onclick, Oncontextmenu, Ondblclick, Onmousedown, Onmouseenter, Onmouseleave, Onmousemove, Onmouseout, Onmouseover, Onmouseup]
+
+type keyEvent = { KeyCode : int,
+ CtrlKey : bool, ShiftKey : bool, AltKey : bool, MetaKey : bool }
+
+con keyEvents = map (fn _ :: Unit => keyEvent -> transaction unit)
+ [Onkeydown, Onkeypress, Onkeyup]
+
+val body : unit -> tag ([Data = data_attr, Onload = transaction unit, Onresize = transaction unit, Onunload = transaction unit, Onhashchange = transaction unit]
+ ++ mouseEvents ++ keyEvents)
+ html body [] []
+
+con bodyTag = fn (attrs :: {Type}) =>
+ ctx ::: {Unit} ->
+ [[Body] ~ ctx] =>
+ unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
+con bodyTagStandalone = fn (attrs :: {Type}) =>
+ ctx ::: {Unit}
+ -> [[Body] ~ ctx] =>
+ unit -> tag attrs ([Body] ++ ctx) [] [] []
+
+val br : bodyTagStandalone [Data = data_attr, Id = id]
+
+con focusEvents = [Onblur = transaction unit, Onfocus = transaction unit]
+
+
+(* Key arguments are character codes. *)
+con resizeEvents = [Onresize = transaction unit]
+con scrollEvents = [Onscroll = transaction unit]
+
+con boxEvents = focusEvents ++ mouseEvents ++ keyEvents ++ resizeEvents ++ scrollEvents
+con tableEvents = focusEvents ++ mouseEvents ++ keyEvents
+
+con boxAttrs = [Data = data_attr, Id = id, Title = string, Role = string, Align = string] ++ boxEvents
+con tableAttrs = [Data = data_attr, Id = id, Title = string, Align = string] ++ tableEvents
+
+val span : bodyTag boxAttrs
+val div : bodyTag boxAttrs
+
+val p : bodyTag boxAttrs
+val strong : bodyTag boxAttrs
+val em : bodyTag boxAttrs
+val b : bodyTag boxAttrs
+val i : bodyTag boxAttrs
+val tt : bodyTag boxAttrs
+val sub : bodyTag boxAttrs
+val sup : bodyTag boxAttrs
+
+val h1 : bodyTag boxAttrs
+val h2 : bodyTag boxAttrs
+val h3 : bodyTag boxAttrs
+val h4 : bodyTag boxAttrs
+val h5 : bodyTag boxAttrs
+val h6 : bodyTag boxAttrs
+
+val li : bodyTag boxAttrs
+val ol : bodyTag boxAttrs
+val ul : bodyTag boxAttrs
+
+val hr : bodyTag boxAttrs
+
+val pre : bodyTag boxAttrs
+
+(** sections **)
+val section : bodyTag boxAttrs
+val article : bodyTag boxAttrs
+val nav : bodyTag boxAttrs
+val aside : bodyTag boxAttrs
+val footer : bodyTag boxAttrs
+val header : bodyTag boxAttrs
+val main : bodyTag boxAttrs
+
+(** forms **)
+val meter : bodyTag boxAttrs
+val progress : bodyTag boxAttrs
+val output : bodyTag boxAttrs
+val keygen : bodyTag boxAttrs
+val datalist : bodyTag boxAttrs
+
+(** Interactive Elements **)
+val details : bodyTag boxAttrs
+val dialog : bodyTag boxAttrs
+val menuitem : bodyTag boxAttrs
+
+(** Grouping Content **)
+val figure : bodyTag boxAttrs
+val figcaption : bodyTag boxAttrs
+
+(** Text Level Semantics **)
+val data : bodyTag boxAttrs
+val mark : bodyTag boxAttrs
+val rp : bodyTag boxAttrs
+val rt : bodyTag boxAttrs
+val ruby : bodyTag boxAttrs
+val summary : bodyTag boxAttrs
+val time : bodyTag boxAttrs
+val wbr : bodyTag boxAttrs
+val bdi : bodyTag boxAttrs
+
+val a : bodyTag ([Link = transaction page, Href = url, Target = string, Rel = string, Download = string] ++ boxAttrs)
+
+val img : bodyTag ([Alt = string, Src = url, Width = int, Height = int,
+ Onabort = transaction unit, Onerror = transaction unit,
+ Onload = transaction unit] ++ boxAttrs)
+
+val form : ctx ::: {Unit} -> bind ::: {Type}
+ -> [[MakeForm, Form] ~ ctx] =>
+ option id
+ -> option css_class
+ -> xml ([Form] ++ ctx) [] bind
+ -> xml ([MakeForm] ++ ctx) [] []
+
+val subform : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
+ -> [[Form] ~ ctx] =>
+ nm :: Name -> [[nm] ~ use] =>
+ xml ([Form] ++ ctx) [] bind
+ -> xml ([Form] ++ ctx) use [nm = $bind]
+
+val subforms : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
+ -> [[Form, Subform] ~ ctx] =>
+ nm :: Name -> [[nm] ~ use] =>
+ xml ([Subform] ++ ctx) [Entry = $bind] []
+ -> xml ([Form] ++ ctx) use [nm = list ($bind)]
+
+val entry : ctx ::: {Unit} -> bind ::: {Type}
+ -> [[Subform, Form] ~ ctx] =>
+ xml ([Form] ++ ctx) [] bind
+ -> xml ([Subform] ++ ctx) [Entry = $bind] []
+
+con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) =>
+ ctx ::: {Unit}
+ -> [[Form] ~ ctx] =>
+ nm :: Name -> unit
+ -> tag attrs ([Form] ++ ctx) inner [] [nm = ty]
+
+con inputAttrs = [Required = bool, Autofocus = bool]
+
+
+val hidden : formTag string [] [Data = data_attr, Id = string, Value = string]
+val textbox : formTag string [] ([Value = string, Size = int, Placeholder = string, Source = source string, Onchange = transaction unit,
+ Ontext = transaction unit] ++ boxAttrs ++ inputAttrs)
+val password : formTag string [] ([Value = string, Size = int, Placeholder = string, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs)
+val textarea : formTag string [] ([Rows = int, Cols = int, Placeholder = string, Onchange = transaction unit,
+ Ontext = transaction unit] ++ boxAttrs ++ inputAttrs)
+
+val checkbox : formTag bool [] ([Checked = bool, Onchange = transaction unit] ++ boxAttrs)
+
+(* HTML5 widgets galore! *)
+
+type textWidget = formTag string [] ([Value = string, Size = int, Placeholder = string, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs)
+
+val email : textWidget
+val search : textWidget
+val url_ : textWidget
+val tel : textWidget
+val color : textWidget
+
+val number : formTag float [] ([Value = float, Min = float, Max = float, Step = float, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs)
+val range : formTag float [] ([Value = float, Min = float, Max = float, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs)
+val date : formTag string [] ([Value = string, Min = string, Max = string, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs)
+val datetime : formTag string [] ([Value = string, Min = string, Max = string, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs)
+val datetime_local : formTag string [] ([Value = string, Min = string, Max = string, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs)
+val month : formTag string [] ([Value = string, Min = string, Max = string, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs)
+val week : formTag string [] ([Value = string, Min = string, Max = string, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs)
+val timeInput : formTag string [] ([Value = string, Min = string, Max = string, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs)
+
+
+
+type file
+val fileName : file -> option string
+val fileMimeType : file -> string
+val fileData : file -> blob
+
+val upload : formTag file [] ([Value = string, Size = int] ++ boxAttrs)
+
+type mimeType
+val blessMime : string -> mimeType
+val checkMime : string -> option mimeType
+val returnBlob : t ::: Type -> blob -> mimeType -> transaction t
+val blobSize : blob -> int
+val textBlob : string -> blob
+
+type postBody
+val postType : postBody -> string
+val postData : postBody -> string
+
+type postField
+val firstFormField : string -> option postField
+val fieldName : postField -> string
+val fieldValue : postField -> string
+val remainingFields : postField -> string
+
+con radio = [Body, Radio]
+val radio : formTag (option string) radio [Data = data_attr, Id = id]
+val radioOption : unit -> tag ([Value = string, Checked = bool, Onchange = transaction unit] ++ boxAttrs) radio [] [] []
+
+con select = [Select]
+val select : formTag string select ([Onchange = transaction unit] ++ boxAttrs)
+val option : unit -> tag [Data = data_attr, Value = string, Selected = bool] select [] [] []
+
+val submit : ctx ::: {Unit} -> use ::: {Type}
+ -> [[Form] ~ ctx] =>
+ unit
+ -> tag ([Value = string, Action = $use -> transaction page] ++ boxAttrs)
+ ([Form] ++ ctx) ([Form] ++ ctx) use []
+
+val image : ctx ::: {Unit} -> use ::: {Type}
+ -> [[Form] ~ ctx] =>
+ unit
+ -> tag ([Src = url, Width = int, Height = int, Alt = string, Action = $use -> transaction page] ++ boxAttrs)
+ ([Form] ++ ctx) ([Form] ++ ctx) use []
+
+val label : bodyTag ([For = id, Accesskey = string] ++ tableAttrs)
+
+val fieldset : bodyTag boxAttrs
+val legend : bodyTag boxAttrs
+
+
+(*** AJAX-oriented widgets *)
+
+con cformTag = fn (attrs :: {Type}) (inner :: {Unit}) =>
+ ctx ::: {Unit}
+ -> [[Body] ~ ctx] => [[Body] ~ inner] =>
+ unit -> tag attrs ([Body] ++ ctx) ([Body] ++ inner) [] []
+
+type ctext = cformTag ([Value = string, Size = int, Source = source string, Placeholder = string,
+ Onchange = transaction unit, Ontext = transaction unit] ++ boxAttrs ++ inputAttrs) []
+
+val ctextbox : ctext
+val cpassword : ctext
+val cemail : ctext
+val csearch : ctext
+val curl : ctext
+val ctel : ctext
+val ccolor : ctext
+
+val cnumber : cformTag ([Source = source (option float), Min = float, Max = float, Step = float, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs) []
+val crange : cformTag ([Source = source (option float), Min = float, Max = float, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs) []
+val cdate : cformTag ([Source = source string, Min = string, Max = string, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs) []
+val cdatetime : cformTag ([Source = source string, Min = string, Max = string, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs) []
+val cdatetime_local : cformTag ([Source = source string, Min = string, Max = string, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs) []
+val cmonth : cformTag ([Source = source string, Min = string, Max = string, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs) []
+val cweek : cformTag ([Source = source string, Min = string, Max = string, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs) []
+val ctime : cformTag ([Source = source string, Min = string, Max = string, Size = int, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs) []
+
+val button : cformTag ([Value = string, Disabled = bool] ++ boxAttrs) []
+
+val ccheckbox : cformTag ([Size = int, Source = source bool, Onchange = transaction unit] ++ boxAttrs ++ inputAttrs) []
+
+val cselect : cformTag ([Source = source string, Onchange = transaction unit] ++ boxAttrs) [Cselect]
+val coption : unit -> tag [Value = string, Selected = bool] [Cselect, Body] [] [] []
+
+val ctextarea : cformTag ([Rows = int, Cols = int, Placeholder = string, Source = source string, Onchange = transaction unit,
+ Ontext = transaction unit] ++ boxAttrs ++ inputAttrs) []
+
+(*** Tables *)
+
+val tabl : other ::: {Unit} -> [other ~ [Body, Table]] => unit
+ -> tag ([Border = int] ++ boxAttrs)
+ ([Body] ++ other) ([Table] ++ other) [] []
+val tr : other ::: {Unit} -> [other ~ [Table, Tr]] => unit
+ -> tag tableAttrs
+ ([Table] ++ other) ([Tr] ++ other) [] []
+val th : other ::: {Unit} -> [other ~ [Body, Tr]] => unit
+ -> tag ([Colspan = int, Rowspan = int] ++ tableAttrs)
+ ([Tr] ++ other) ([Body] ++ other) [] []
+val td : other ::: {Unit} -> [other ~ [Body, Tr]] => unit
+ -> tag ([Colspan = int, Rowspan = int] ++ tableAttrs)
+ ([Tr] ++ other) ([Body] ++ other) [] []
+
+val thead : other ::: {Unit} -> [other ~ [Table]] => unit
+ -> tag tableAttrs
+ ([Table] ++ other) ([Table] ++ other) [] []
+val tbody : other ::: {Unit} -> [other ~ [Table]] => unit
+ -> tag tableAttrs
+ ([Table] ++ other) ([Table] ++ other) [] []
+val tfoot : other ::: {Unit} -> [other ~ [Table]] => unit
+ -> tag tableAttrs
+ ([Table] ++ other) ([Table] ++ other) [] []
+
+(** Definition lists *)
+
+val dl : other ::: {Unit} -> [other ~ [Body,Dl]]
+ => unit
+ -> tag [Data = data_attr] ([Body] ++ other) ([Dl] ++ other) [] []
+
+val dt : other ::: {Unit} -> [other ~ [Body,Dl]]
+ => unit
+ -> tag [Data = data_attr] ([Dl] ++ other) ([Body] ++ other) [] []
+
+val dd : other ::: {Unit} -> [other ~ [Body,Dl]]
+ => unit
+ -> tag [Data = data_attr] ([Dl] ++ other) ([Body] ++ other) [] []
+
+
+(** Aborting *)
+
+val error : t ::: Type -> xbody -> t
+
+(* Client-side-only handlers: *)
+val onError : (xbody -> transaction unit) -> transaction unit
+val onFail : (string -> transaction unit) -> transaction unit
+val onConnectFail : transaction unit -> transaction unit
+val onDisconnect : transaction unit -> transaction unit
+val onServerError : (string -> transaction unit) -> transaction unit
+
+(* More standard document-level JavaScript handlers *)
+val onClick : (mouseEvent -> transaction unit) -> transaction unit
+val onDblclick : (mouseEvent -> transaction unit) -> transaction unit
+val onContextmenu : (mouseEvent -> transaction unit) -> transaction unit
+val onKeydown : (keyEvent -> transaction unit) -> transaction unit
+val onKeypress : (keyEvent -> transaction unit) -> transaction unit
+val onKeyup : (keyEvent -> transaction unit) -> transaction unit
+val onMousedown : (mouseEvent -> transaction unit) -> transaction unit
+val onMouseenter : (mouseEvent -> transaction unit) -> transaction unit
+val onMouseleave : (mouseEvent -> transaction unit) -> transaction unit
+val onMousemove : (mouseEvent -> transaction unit) -> transaction unit
+val onMouseout : (mouseEvent -> transaction unit) -> transaction unit
+val onMouseover : (mouseEvent -> transaction unit) -> transaction unit
+val onMouseup : (mouseEvent -> transaction unit) -> transaction unit
+
+(* Prevents default handling of current event *)
+val preventDefault : transaction unit
+(* Stops propagation of current event *)
+val stopPropagation : transaction unit
+
+val show_xml : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> show (xml ctx use bind)
+
+
+(** Tasks *)
+
+con task_kind :: Type -> Type
+val initialize : task_kind unit
+val clientLeaves : task_kind client
+val periodic : int -> task_kind unit
+
+
+(** Information flow security *)
+
+type sql_policy
+
+val sendClient : tables ::: {{Type}} -> exps ::: {Type}
+ -> [tables ~ exps] => sql_query [] [] tables exps
+ -> sql_policy
+
+val sendOwnIds : sql_sequence -> sql_policy
+
+val mayInsert : fs ::: {Type} -> tables ::: {{Type}} -> [[New] ~ tables]
+ => sql_query [] [] ([New = fs] ++ tables) []
+ -> sql_policy
+
+val mayDelete : fs ::: {Type} -> tables ::: {{Type}} -> [[Old] ~ tables]
+ => sql_query [] [] ([Old = fs] ++ tables) []
+ -> sql_policy
+
+val mayUpdate : fs ::: {Type} -> tables ::: {{Type}} -> [[Old, New] ~ tables]
+ => sql_query [] [] ([Old = fs, New = fs] ++ tables) []
+ -> sql_policy
+
+val also : sql_policy -> sql_policy -> sql_policy
+
+val debug : string -> transaction unit
+val naughtyDebug : string -> int
+
+val rand : transaction int
diff --git a/lib/ur/char.ur b/lib/ur/char.ur
new file mode 100644
index 0000000..d2890be
--- /dev/null
+++ b/lib/ur/char.ur
@@ -0,0 +1,19 @@
+type t = char
+
+val isAlnum = Basis.isalnum
+val isAlpha = Basis.isalpha
+val isBlank = Basis.isblank
+val isCntrl = Basis.iscntrl
+val isDigit = Basis.isdigit
+val isGraph = Basis.isgraph
+val isLower = Basis.islower
+val isPrint = Basis.isprint
+val isPunct = Basis.ispunct
+val isSpace = Basis.isspace
+val isUpper = Basis.isupper
+val isXdigit = Basis.isxdigit
+val toLower = Basis.tolower
+val toUpper = Basis.toupper
+
+val toInt = Basis.ord
+val fromInt = Basis.chr
diff --git a/lib/ur/char.urs b/lib/ur/char.urs
new file mode 100644
index 0000000..c185af9
--- /dev/null
+++ b/lib/ur/char.urs
@@ -0,0 +1,19 @@
+type t = char
+
+val isAlnum : t -> bool
+val isAlpha : t -> bool
+val isBlank : t -> bool
+val isCntrl : t -> bool
+val isDigit : t -> bool
+val isGraph : t -> bool
+val isLower : t -> bool
+val isPrint : t -> bool
+val isPunct : t -> bool
+val isSpace : t -> bool
+val isUpper : t -> bool
+val isXdigit : t -> bool
+val toLower : t -> t
+val toUpper : t -> t
+
+val toInt : t -> int
+val fromInt : int -> t
diff --git a/lib/ur/datetime.ur b/lib/ur/datetime.ur
new file mode 100644
index 0000000..9aeab29
--- /dev/null
+++ b/lib/ur/datetime.ur
@@ -0,0 +1,135 @@
+datatype day_of_week = Sunday | Monday | Tuesday | Wednesday | Thursday |
+ Friday | Saturday
+
+val show_day_of_week = mkShow (fn dow => case dow of
+ Sunday => "Sunday"
+ | Monday => "Monday"
+ | Tuesday => "Tuesday"
+ | Wednesday => "Wednesday"
+ | Thursday => "Thursday"
+ | Friday => "Friday"
+ | Saturday => "Saturday")
+
+fun dayOfWeekToInt dow = case dow of
+ Sunday => 0
+ | Monday => 1
+ | Tuesday => 2
+ | Wednesday => 3
+ | Thursday => 4
+ | Friday => 5
+ | Saturday => 6
+
+fun intToDayOfWeek i = case i of
+ 0 => Sunday
+ | 1 => Monday
+ | 2 => Tuesday
+ | 3 => Wednesday
+ | 4 => Thursday
+ | 5 => Friday
+ | 6 => Saturday
+ | n => error <xml>Invalid day of week {[n]}</xml>
+
+val eq_day_of_week = mkEq (fn a b => dayOfWeekToInt a = dayOfWeekToInt b)
+
+
+datatype month = January | February | March | April | May | June | July |
+ August | September | October | November | December
+
+val show_month = mkShow (fn m => case m of
+ January => "January"
+ | February => "February"
+ | March => "March"
+ | April => "April"
+ | May => "May"
+ | June => "June"
+ | July => "July"
+ | August => "August"
+ | September => "September"
+ | October => "October"
+ | November => "November"
+ | December => "December")
+
+type t = {
+ Year : int,
+ Month : month,
+ Day : int,
+ Hour : int,
+ Minute : int,
+ Second : int
+}
+
+fun monthToInt m = case m of
+ January => 0
+ | February => 1
+ | March => 2
+ | April => 3
+ | May => 4
+ | June => 5
+ | July => 6
+ | August => 7
+ | September => 8
+ | October => 9
+ | November => 10
+ | December => 11
+
+fun intToMonth i = case i of
+ 0 => January
+ | 1 => February
+ | 2 => March
+ | 3 => April
+ | 4 => May
+ | 5 => June
+ | 6 => July
+ | 7 => August
+ | 8 => September
+ | 9 => October
+ | 10 => November
+ | 11 => December
+ | n => error <xml>Invalid month number {[n]}</xml>
+
+val eq_month = mkEq (fn a b => monthToInt a = monthToInt b)
+
+
+fun toTime dt : time = fromDatetime dt.Year (monthToInt dt.Month) dt.Day
+ dt.Hour dt.Minute dt.Second
+
+fun fromTime t : t = {
+ Year = datetimeYear t,
+ Month = intToMonth (datetimeMonth t),
+ Day = datetimeDay t,
+ Hour = datetimeHour t,
+ Minute = datetimeMinute t,
+ Second = datetimeSecond t
+}
+
+val ord_datetime = mkOrd { Lt = fn a b => toTime a < toTime b,
+ Le = fn a b => toTime a <= toTime b }
+
+fun format fmt dt : string = timef fmt (toTime dt)
+
+fun dayOfWeek dt : day_of_week = intToDayOfWeek (datetimeDayOfWeek (toTime dt))
+
+val now : transaction t =
+ n <- now;
+ return (fromTime n)
+
+(* Normalize a datetime. This will convert, e.g., January 32nd into February
+ 1st. *)
+
+fun normalize dt = fromTime (toTime dt)
+fun addToField [nm :: Name] [rest ::: {Type}] [[nm] ~ rest]
+ (delta : int) (r : $([nm = int] ++ rest))
+ : $([nm = int] ++ rest) =
+ (r -- nm) ++ {nm = r.nm + delta}
+
+
+(* Functions for adding to a datetime. There is no addMonths or addYears since
+ it's not clear what should be done; what's 1 month after January 31, or 1
+ year after February 29th?
+
+ These can't all be defined in terms of addSeconds because of leap seconds. *)
+
+fun addSeconds n dt = normalize (addToField [#Second] n dt)
+fun addMinutes n dt = normalize (addToField [#Minute] n dt)
+fun addHours n dt = normalize (addToField [#Hour] n dt)
+fun addDays n dt = normalize (addToField [#Day] n dt)
diff --git a/lib/ur/datetime.urs b/lib/ur/datetime.urs
new file mode 100644
index 0000000..972f86b
--- /dev/null
+++ b/lib/ur/datetime.urs
@@ -0,0 +1,38 @@
+datatype day_of_week = Sunday | Monday | Tuesday | Wednesday | Thursday |
+ Friday | Saturday
+
+datatype month = January | February | March | April | May | June | July |
+ August | September | October | November | December
+
+
+type t = {
+ Year : int,
+ Month : month,
+ Day : int,
+ Hour : int,
+ Minute : int,
+ Second : int
+}
+
+val ord_datetime : ord t
+
+val show_day_of_week : show day_of_week
+val show_month : show month
+val eq_day_of_week : eq day_of_week
+val eq_month : eq month
+val dayOfWeekToInt : day_of_week -> int
+val intToDayOfWeek : int -> day_of_week
+val monthToInt : month -> int
+val intToMonth : int -> month
+
+val toTime : t -> time
+val fromTime : time -> t
+val format : string -> t -> string
+val dayOfWeek : t -> day_of_week
+val now : transaction t
+val normalize : t -> t
+
+val addSeconds : int -> t -> t
+val addMinutes : int -> t -> t
+val addHours : int -> t -> t
+val addDays : int -> t -> t
diff --git a/lib/ur/json.ur b/lib/ur/json.ur
new file mode 100644
index 0000000..9288a6d
--- /dev/null
+++ b/lib/ur/json.ur
@@ -0,0 +1,387 @@
+con json a = {ToJson : a -> string,
+ FromJson : string -> a * string}
+
+fun mkJson [a] (x : {ToJson : a -> string,
+ FromJson : string -> a * string}) = x
+
+fun skipSpaces s =
+ let
+ val len = String.length s
+
+ fun skip i =
+ if i >= len then
+ ""
+ else
+ let
+ val ch = String.sub s i
+ in
+ if Char.isSpace ch then
+ skip (i+1)
+ else
+ String.substring s {Start = i, Len = len-i}
+ end
+ in
+ skip 0
+ end
+
+fun toJson [a] (j : json a) : a -> string = j.ToJson
+fun fromJson' [a] (j : json a) : string -> a * string = j.FromJson
+
+fun fromJson [a] (j : json a) (s : string) : a =
+ let
+ val (v, s') = j.FromJson (skipSpaces s)
+ in
+ if String.all Char.isSpace s' then
+ v
+ else
+ error <xml>Extra content at end of JSON record: {[s']}</xml>
+ end
+
+fun escape s =
+ let
+ fun esc s =
+ case s of
+ "" => "\""
+ | _ =>
+ let
+ val ch = String.sub s 0
+ in
+ (if ch = #"\"" || ch = #"\\" then
+ "\\" ^ String.str ch
+ else
+ String.str ch) ^ esc (String.suffix s 1)
+ end
+ in
+ "\"" ^ esc s
+ end
+
+fun unescape s =
+ let
+ val len = String.length s
+
+ fun findEnd i =
+ if i >= len then
+ error <xml>JSON unescape: string ends before quote: {[s]}</xml>
+ else
+ let
+ val ch = String.sub s i
+ in
+ case ch of
+ #"\"" => i
+ | #"\\" =>
+ if i+1 >= len then
+ error <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
+ else
+ findEnd (i+2)
+ | _ => findEnd (i+1)
+ end
+
+ val last = findEnd 1
+
+ fun unesc i =
+ if i >= last then
+ ""
+ else
+ let
+ val ch = String.sub s i
+ in
+ case ch of
+ #"\\" =>
+ if i+1 >= len then
+ error <xml>JSON unescape: Bad escape sequence: {[s]}</xml>
+ else
+ String.str (String.sub s (i+1)) ^ unesc (i+2)
+ | _ => String.str ch ^ unesc (i+1)
+ end
+ in
+ if len = 0 || String.sub s 0 <> #"\"" then
+ error <xml>JSON unescape: String doesn't start with double quote: {[s]}</xml>
+ else
+ (unesc 1, String.substring s {Start = last+1, Len = len-last-1})
+ end
+
+val json_string = {ToJson = escape,
+ FromJson = unescape}
+
+fun numIn [a] (_ : read a) s : a * string =
+ let
+ val len = String.length s
+
+ fun findEnd i =
+ if i >= len then
+ i
+ else
+ let
+ val ch = String.sub s i
+ in
+ if Char.isDigit ch || ch = #"-" || ch = #"." || ch = #"E" || ch = #"e" then
+ findEnd (i+1)
+ else
+ i
+ end
+
+ val last = findEnd 0
+ in
+ (readError (String.substring s {Start = 0, Len = last}), String.substring s {Start = last, Len = len-last})
+ end
+
+fun json_num [a] (_ : show a) (_ : read a) : json a = {ToJson = show,
+ FromJson = numIn}
+
+val json_int = json_num
+val json_float = json_num
+
+val json_bool = {ToJson = fn b => if b then "true" else "false",
+ FromJson = fn s => if String.isPrefix {Full = s, Prefix = "true"} then
+ (True, String.substring s {Start = 4, Len = String.length s - 4})
+ else if String.isPrefix {Full = s, Prefix = "false"} then
+ (False, String.substring s {Start = 5, Len = String.length s - 5})
+ else
+ error <xml>JSON: bad boolean string: {[s]}</xml>}
+
+fun json_option [a] (j : json a) : json (option a) =
+ {ToJson = fn v => case v of
+ None => "null"
+ | Some v => j.ToJson v,
+ FromJson = fn s => if String.isPrefix {Full = s, Prefix = "null"} then
+ (None, String.substring s {Start = 4, Len = String.length s - 4})
+ else
+ let
+ val (v, s') = j.FromJson s
+ in
+ (Some v, s')
+ end}
+
+fun json_list [a] (j : json a) : json (list a) =
+ let
+ fun toJ' (ls : list a) : string =
+ case ls of
+ [] => ""
+ | x :: ls => "," ^ toJson j x ^ toJ' ls
+
+ fun toJ (x : list a) : string =
+ case x of
+ [] => "[]"
+ | x :: [] => "[" ^ toJson j x ^ "]"
+ | x :: ls => "[" ^ toJson j x ^ toJ' ls ^ "]"
+
+ fun fromJ (s : string) : list a * string =
+ let
+ fun fromJ' (s : string) : list a * string =
+ if String.length s = 0 then
+ error <xml>JSON list doesn't end with ']'</xml>
+ else
+ let
+ val ch = String.sub s 0
+ in
+ case ch of
+ #"]" => ([], String.substring s {Start = 1, Len = String.length s - 1})
+ | _ =>
+ let
+ val (x, s') = j.FromJson s
+ val s' = skipSpaces s'
+ val s' = if String.length s' = 0 then
+ error <xml>JSON list doesn't end with ']'</xml>
+ else if String.sub s' 0 = #"," then
+ skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
+ else
+ s'
+
+ val (ls, s'') = fromJ' s'
+ in
+ (x :: ls, s'')
+ end
+ end
+ in
+ if String.length s = 0 || String.sub s 0 <> #"[" then
+ error <xml>JSON list doesn't start with '[': {[s]}</xml>
+ else
+ fromJ' (skipSpaces (String.substring s {Start = 1, Len = String.length s - 1}))
+ end
+ in
+ {ToJson = toJ,
+ FromJson = fromJ}
+ end
+
+fun skipOne s =
+ let
+ fun skipOne s dquote squote brace bracket =
+ if String.length s = 0 then
+ s
+ else
+ let
+ val ch = String.sub s 0
+ val rest = String.suffix s 1
+ in
+ case ch of
+ #"\"" => skipOne rest (not dquote) squote brace bracket
+ | #"'" => skipOne rest dquote (not squote) brace bracket
+ | #"\\" => if String.length s >= 2 then
+ skipOne (String.suffix s 2) dquote squote brace bracket
+ else
+ ""
+ | #"{" => skipOne rest dquote squote (brace + 1) bracket
+ | #"}" => if brace = 0 then
+ s
+ else
+ skipOne rest dquote squote (brace - 1) bracket
+
+ | #"[" => skipOne rest dquote squote brace (bracket + 1)
+ | #"]" =>
+ if bracket = 0 then
+ s
+ else
+ skipOne rest dquote squote brace (bracket - 1)
+
+ | #"," =>
+ if not dquote && not squote && brace = 0 && bracket = 0 then
+ s
+ else
+ skipOne rest dquote squote brace bracket
+
+ | _ => skipOne rest dquote squote brace bracket
+ end
+ in
+ skipOne s False False 0 0
+ end
+
+fun json_record [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json $ts =
+ {ToJson = fn r => "{" ^ @foldR3 [json] [fn _ => string] [ident] [fn _ => string]
+ (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name v acc =>
+ escape name ^ ":" ^ j.ToJson v ^ (case acc of
+ "" => ""
+ | acc => "," ^ acc))
+ "" fl jss names r ^ "}",
+ FromJson = fn s =>
+ let
+ fun fromJ s (r : $(map option ts)) : $(map option ts) * string =
+ if String.length s = 0 then
+ error <xml>JSON object doesn't end in brace</xml>
+ else if String.sub s 0 = #"}" then
+ (r, String.substring s {Start = 1, Len = String.length s - 1})
+ else let
+ val (name, s') = unescape s
+ val s' = skipSpaces s'
+ val s' = if String.length s' = 0 || String.sub s' 0 <> #":" then
+ error <xml>No colon after JSON object field name</xml>
+ else
+ skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
+
+ val (r, s') = @foldR2 [json] [fn _ => string] [fn ts => $(map option ts) -> $(map option ts) * string]
+ (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name' acc r =>
+ if name = name' then
+ let
+ val (v, s') = j.FromJson s'
+ in
+ (r -- nm ++ {nm = Some v}, s')
+ end
+ else
+ let
+ val (r', s') = acc (r -- nm)
+ in
+ (r' ++ {nm = r.nm}, s')
+ end)
+ (fn r => (r, skipOne s'))
+ fl jss names r
+
+ val s' = skipSpaces s'
+ val s' = if String.length s' <> 0 && String.sub s' 0 = #"," then
+ skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
+ else
+ s'
+ in
+ fromJ s' r
+ end
+ in
+ if String.length s = 0 || String.sub s 0 <> #"{" then
+ error <xml>JSON record doesn't begin with brace</xml>
+ else
+ let
+ val (r, s') = fromJ (skipSpaces (String.substring s {Start = 1, Len = String.length s - 1}))
+ (@map0 [option] (fn [t ::_] => None) fl)
+ in
+ (@map2 [option] [fn _ => string] [ident] (fn [t] (v : option t) name =>
+ case v of
+ None => error <xml>Missing JSON object field {[name]}</xml>
+ | Some v => v) fl r names, s')
+ end
+ end}
+
+fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type]
+ (f : p :: K -> f p -> fr p -> t)
+ [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t =
+ match v
+ (@Top.mp [fr] [fn p => f p -> t]
+ (fn [p] (m : fr p) (v : f p) => f [p] v m)
+ fl r)
+
+fun json_variant [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json (variant ts) =
+ {ToJson = fn r => let val jnames = @map2 [json] [fn _ => string] [fn x => json x * string]
+ (fn [t] (j : json t) (name : string) => (j, name)) fl jss names
+ in @destrR [ident] [fn x => json x * string]
+ (fn [p ::_] (v : p) (j : json p, name : string) =>
+ "{" ^ escape name ^ ":" ^ j.ToJson v ^ "}") fl r jnames
+ end,
+ FromJson = fn s =>
+ if String.length s = 0 || String.sub s 0 <> #"{" then
+ error <xml>JSON variant doesn't begin with brace</xml>
+ else
+ let
+ val (name, s') = unescape (skipSpaces (String.suffix s 1))
+ val s' = skipSpaces s'
+ val s' = if String.length s' = 0 || String.sub s' 0 <> #":" then
+ error <xml>No colon after JSON object field name</xml>
+ else
+ skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
+
+ val (r, s') = (@foldR2 [json] [fn _ => string]
+ [fn ts => ts' :: {Type} -> [ts ~ ts'] => variant (ts ++ ts') * string]
+ (fn [nm ::_] [t ::_] [rest ::_] [[nm] ~ rest] (j : json t) name'
+ (acc : ts' :: {Type} -> [rest ~ ts'] => variant (rest ++ ts') * string) [fwd ::_] [[nm = t] ++ rest ~ fwd] =>
+ if name = name'
+ then
+ let val (v, s') = j.FromJson s'
+ in (make [nm] v, s')
+ end
+ else acc [fwd ++ [nm = t]]
+ )
+ (fn [fwd ::_] [[] ~ fwd] => error <xml>Unknown JSON object variant name {[name]}</xml>)
+ fl jss names) [[]] !
+
+ val s' = skipSpaces s'
+ val s' = if String.length s' <> 0 && String.sub s' 0 = #"," then
+ skipSpaces (String.substring s' {Start = 1, Len = String.length s' - 1})
+ else
+ s'
+ in
+ if String.length s' = 0 then
+ error <xml>JSON object doesn't end in brace</xml>
+ else if String.sub s' 0 = #"}" then
+ (r, String.substring s' {Start = 1, Len = String.length s' - 1})
+ else error <xml>Junk after JSON value in object</xml>
+ end
+ }
+
+val json_unit : json unit = json_record {} {}
+
+functor Recursive (M : sig
+ con t :: Type -> Type
+ val json_t : a ::: Type -> json a -> json (t a)
+ end) = struct
+ open M
+
+ datatype r = Rec of t r
+
+ fun rTo (Rec x) = (json_t {ToJson = rTo,
+ FromJson = fn _ => error <xml>Tried to FromJson in ToJson!</xml>}).ToJson x
+
+ fun rFrom s =
+ let
+ val (x, s') = (json_t {ToJson = fn _ => error <xml>Tried to ToJson in FromJson!</xml>,
+ FromJson = rFrom}).FromJson s
+ in
+ (Rec x, s')
+ end
+
+ val json_r = {ToJson = rTo, FromJson = rFrom}
+end
diff --git a/lib/ur/json.urs b/lib/ur/json.urs
new file mode 100644
index 0000000..b4bd635
--- /dev/null
+++ b/lib/ur/json.urs
@@ -0,0 +1,31 @@
+(** The JSON text-based serialization format *)
+
+class json
+
+val toJson : a ::: Type -> json a -> a -> string
+val fromJson : a ::: Type -> json a -> string -> a
+val fromJson' : a ::: Type -> json a -> string -> a * string
+
+val mkJson : a ::: Type -> {ToJson : a -> string,
+ FromJson : string -> a * string} -> json a
+
+val json_string : json string
+val json_int : json int
+val json_float : json float
+val json_bool : json bool
+val json_option : a ::: Type -> json a -> json (option a)
+val json_list : a ::: Type -> json a -> json (list a)
+
+val json_record : ts ::: {Type} -> folder ts -> $(map json ts) -> $(map (fn _ => string) ts) -> json $ts
+val json_variant : ts ::: {Type} -> folder ts -> $(map json ts) -> $(map (fn _ => string) ts) -> json (variant ts)
+
+val json_unit : json unit
+
+functor Recursive (M : sig
+ con t :: Type -> Type
+ val json_t : a ::: Type -> json a -> json (t a)
+ end) : sig
+ datatype r = Rec of M.t r
+
+ val json_r : json r
+end
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
new file mode 100644
index 0000000..cc53367
--- /dev/null
+++ b/lib/ur/list.ur
@@ -0,0 +1,498 @@
+datatype t = datatype Basis.list
+
+val show = fn [a] (_ : show a) =>
+ let
+ fun show' (ls : list a) =
+ case ls of
+ [] => "[]"
+ | x :: ls => show x ^ " :: " ^ show' ls
+ in
+ mkShow show'
+ end
+
+val eq = fn [a] (_ : eq a) =>
+ let
+ fun eq' (ls1 : list a) ls2 =
+ case (ls1, ls2) of
+ ([], []) => True
+ | (x1 :: ls1, x2 :: ls2) => x1 = x2 && eq' ls1 ls2
+ | _ => False
+ in
+ mkEq eq'
+ end
+
+fun foldl [a] [b] (f : a -> b -> b) =
+ let
+ fun foldl' acc ls =
+ case ls of
+ [] => acc
+ | x :: ls => foldl' (f x acc) ls
+ in
+ foldl'
+ end
+
+val rev = fn [a] =>
+ let
+ fun rev' acc (ls : list a) =
+ case ls of
+ [] => acc
+ | x :: ls => rev' (x :: acc) ls
+ in
+ rev' []
+ end
+
+fun foldr [a] [b] f (acc : b) (ls : list a) = foldl f acc (rev ls)
+
+fun foldlAbort [a] [b] f =
+ let
+ fun foldlAbort' acc ls =
+ case ls of
+ [] => Some acc
+ | x :: ls =>
+ case f x acc of
+ None => None
+ | Some acc' => foldlAbort' acc' ls
+ in
+ foldlAbort'
+ end
+
+val length = fn [a] =>
+ let
+ fun length' acc (ls : list a) =
+ case ls of
+ [] => acc
+ | _ :: ls => length' (acc + 1) ls
+ in
+ length' 0
+ end
+
+fun foldlMapAbort [a] [b] [c] f =
+ let
+ fun foldlMapAbort' ls' acc ls =
+ case ls of
+ [] => Some (rev ls', acc)
+ | x :: ls =>
+ case f x acc of
+ None => None
+ | Some (x', acc') => foldlMapAbort' (x' :: ls') acc' ls
+ in
+ foldlMapAbort' []
+ end
+
+val revAppend = fn [a] =>
+ let
+ fun ra (ls : list a) acc =
+ case ls of
+ [] => acc
+ | x :: ls => ra ls (x :: acc)
+ in
+ ra
+ end
+
+fun append [a] (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2
+
+fun mp [a] [b] f =
+ let
+ fun mp' acc ls =
+ case ls of
+ [] => rev acc
+ | x :: ls => mp' (f x :: acc) ls
+ in
+ mp' []
+ end
+
+fun mapi [a] [b] f =
+ let
+ fun mp' n acc ls =
+ case ls of
+ [] => rev acc
+ | x :: ls => mp' (n + 1) (f n x :: acc) ls
+ in
+ mp' 0 []
+ end
+
+fun mapPartial [a] [b] f =
+ let
+ fun mp' acc ls =
+ case ls of
+ [] => rev acc
+ | x :: ls => mp' (case f x of
+ None => acc
+ | Some y => y :: acc) ls
+ in
+ mp' []
+ end
+
+fun mapX [a] [ctx ::: {Unit}] f =
+ let
+ fun mapX' ls =
+ case ls of
+ [] => <xml/>
+ | x :: ls => <xml>{f x}{mapX' ls}</xml>
+ in
+ mapX'
+ end
+
+fun mapXi [a] [ctx ::: {Unit}] f =
+ let
+ fun mapX' i ls =
+ case ls of
+ [] => <xml/>
+ | x :: ls => <xml>{f i x}{mapX' (i + 1) ls}</xml>
+ in
+ mapX' 0
+ end
+
+fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
+ let
+ fun mapM' acc ls =
+ case ls of
+ [] => return (rev acc)
+ | x :: ls => x' <- f x; mapM' (x' :: acc) ls
+ in
+ mapM' []
+ end
+
+fun mapPartialM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
+ let
+ fun mapPartialM' acc ls =
+ case ls of
+ [] => return (rev acc)
+ | x :: ls =>
+ v <- f x;
+ mapPartialM' (case v of
+ None => acc
+ | Some x' => x' :: acc) ls
+ in
+ mapPartialM' []
+ end
+
+fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f =
+ let
+ fun mapXM' ls =
+ case ls of
+ [] => return <xml/>
+ | x :: ls =>
+ this <- f x;
+ rest <- mapXM' ls;
+ return <xml>{this}{rest}</xml>
+ in
+ mapXM'
+ end
+
+fun filter [a] f =
+ let
+ fun fil acc ls =
+ case ls of
+ [] => rev acc
+ | x :: ls => fil (if f x then x :: acc else acc) ls
+ in
+ fil []
+ end
+
+fun exists [a] f =
+ let
+ fun ex ls =
+ case ls of
+ [] => False
+ | x :: ls =>
+ if f x then
+ True
+ else
+ ex ls
+ in
+ ex
+ end
+
+fun foldlMap [a] [b] [c] f =
+ let
+ fun fold ls' st ls =
+ case ls of
+ [] => (rev ls', st)
+ | x :: ls =>
+ case f x st of
+ (y, st) => fold (y :: ls') st ls
+ in
+ fold []
+ end
+
+fun mem [a] (_ : eq a) (x : a) =
+ let
+ fun mm ls =
+ case ls of
+ [] => False
+ | y :: ls => y = x || mm ls
+ in
+ mm
+ end
+
+fun find [a] f =
+ let
+ fun find' ls =
+ case ls of
+ [] => None
+ | x :: ls =>
+ if f x then
+ Some x
+ else
+ find' ls
+ in
+ find'
+ end
+
+fun search [a] [b] f =
+ let
+ fun search' ls =
+ case ls of
+ [] => None
+ | x :: ls =>
+ case f x of
+ None => search' ls
+ | v => v
+ in
+ search'
+ end
+
+fun foldlM [m] (_ : monad m) [a] [b] f =
+ let
+ fun foldlM' acc ls =
+ case ls of
+ [] => return acc
+ | x :: ls =>
+ acc <- f x acc;
+ foldlM' acc ls
+ in
+ foldlM'
+ end
+
+fun foldlMi [m] (_ : monad m) [a] [b] f =
+ let
+ fun foldlMi' i acc ls =
+ case ls of
+ [] => return acc
+ | x :: ls =>
+ acc <- f i x acc;
+ foldlMi' (i + 1) acc ls
+ in
+ foldlMi' 0
+ end
+
+fun filterM [m] (_ : monad m) [a] (p : a -> m bool) =
+ let
+ fun filterM' (acc : list a) (xs : list a) : m (list a) =
+ case xs of
+ [] => return (rev acc)
+ | x :: xs =>
+ c <- p x;
+ filterM' (if c then x :: acc else acc) xs
+ in
+ filterM' []
+ end
+
+fun all [m] f =
+ let
+ fun all' ls =
+ case ls of
+ [] => True
+ | x :: ls => f x && all' ls
+ in
+ all'
+ end
+
+fun app [m] (_ : monad m) [a] f =
+ let
+ fun app' ls =
+ case ls of
+ [] => return ()
+ | x :: ls =>
+ f x;
+ app' ls
+ in
+ app'
+ end
+
+fun appi [m] (_ : monad m) [a] f =
+ let
+ fun app' i ls =
+ case ls of
+ [] => return ()
+ | x :: ls =>
+ f i x;
+ app' (i + 1) ls
+ in
+ app' 0
+ end
+
+fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
+ [tables ~ exps] (q : sql_query [] [] tables exps)
+ (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> t) =
+ ls <- query q
+ (fn fs acc => return (f fs :: acc))
+ [];
+ return (rev ls)
+
+fun mapQueryM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
+ [tables ~ exps] (q : sql_query [] [] tables exps)
+ (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t) =
+ ls <- query q
+ (fn fs acc => v <- f fs; return (v :: acc))
+ [];
+ return (rev ls)
+
+fun mapQueryPartialM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
+ [tables ~ exps] (q : sql_query [] [] tables exps)
+ (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t)) =
+ ls <- query q
+ (fn fs acc => v <- f fs;
+ return (case v of
+ None => acc
+ | Some v => v :: acc))
+ [];
+ return (rev ls)
+
+fun sort [a] (gt : a -> a -> bool) (ls : t a) : t a =
+ let
+ fun split ls acc1 acc2 =
+ case ls of
+ [] => (rev acc1, rev acc2)
+ | x :: [] => (rev (x :: acc1), rev acc2)
+ | x1 :: x2 :: ls' => split ls' (x1 :: acc1) (x2 :: acc2)
+
+ fun merge ls1 ls2 acc =
+ case (ls1, ls2) of
+ ([], _) => revAppend acc ls2
+ | (_, []) => revAppend acc ls1
+ | (x1 :: ls1', x2 :: ls2') => if gt x1 x2 then merge ls1 ls2' (x2 :: acc) else merge ls1' ls2 (x1 :: acc)
+
+ fun sort' ls =
+ case ls of
+ [] => ls
+ | _ :: [] => ls
+ | _ =>
+ let
+ val (ls1, ls2) = split ls [] []
+ in
+ merge (sort' ls1) (sort' ls2) []
+ end
+ in
+ sort' ls
+ end
+
+val nth [a] =
+ let
+ fun nth (ls : list a) (n : int) : option a =
+ case ls of
+ [] => None
+ | x :: ls' =>
+ if n <= 0 then
+ Some x
+ else
+ nth ls' (n-1)
+ in
+ nth
+ end
+
+fun replaceNth [a] (ls : list a) (n : int) (v : a) : list a =
+ let
+ fun repNth (ls : list a) (n : int) (acc : list a) =
+ case ls of
+ [] => rev acc
+ | x :: ls' => if n <= 0 then
+ revAppend acc (v :: ls')
+ else
+ repNth ls' (n-1) (x :: acc)
+ in
+ repNth ls n []
+ end
+
+fun assoc [a] [b] (_ : eq a) (x : a) =
+ let
+ fun assoc' (ls : list (a * b)) =
+ case ls of
+ [] => None
+ | (y, z) :: ls =>
+ if x = y then
+ Some z
+ else
+ assoc' ls
+ in
+ assoc'
+ end
+
+fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
+ case assoc x ls of
+ None => (x, y) :: ls
+ | Some _ => ls
+
+fun recToList [a ::: Type] [r ::: {Unit}] (fl : folder r)
+ = @foldUR [a] [fn _ => list a] (fn [nm ::_] [rest ::_] [[nm] ~ rest] x xs =>
+ x :: xs) [] fl
+
+fun take [a] (n : int) (xs : list a) : list a =
+ if n <= 0 then
+ []
+ else
+ case xs of
+ [] => []
+ | x :: xs => x :: take (n-1) xs
+
+fun drop [a] (n : int) (xs : list a) : list a =
+ if n <= 0 then
+ xs
+ else
+ case xs of
+ [] => []
+ | x :: xs => drop (n-1) xs
+
+fun splitAt [a] (n : int) (xs : list a) : list a * list a =
+ (take n xs, drop n xs)
+
+fun span [a] (f : a -> bool) (ls : list a) : list a * list a =
+ let
+ fun span' ls acc =
+ case ls of
+ [] => (rev acc, [])
+ | x :: xs => if f x then span' xs (x :: acc) else (rev acc, ls)
+ in
+ span' ls []
+ end
+
+fun groupBy [a] (f : a -> a -> bool) (ls : list a) : list (list a) =
+ let
+ fun groupBy' ls acc =
+ case ls of
+ [] => rev ([] :: acc)
+ | x :: xs =>
+ let
+ val (ys, zs) = span (f x) xs
+ in
+ groupBy' zs ((x :: ys) :: acc)
+ end
+ in
+ groupBy' ls []
+ end
+
+fun mapXiM [m ::: Type -> Type] (_ : monad m) [a] [ctx ::: {Unit}] (f : int -> a -> m (xml ctx [] [])) : t a -> m (xml ctx [] []) =
+ let
+ fun mapXiM' i ls =
+ case ls of
+ [] => return <xml/>
+ | x :: ls =>
+ this <- f i x;
+ rest <- mapXiM' (i+1) ls;
+ return <xml>{this}{rest}</xml>
+ in
+ mapXiM' 0
+ end
+
+fun tabulateM [m] (_ : monad m) [a] (f : int -> m a) n =
+ let
+ fun tabulate' n acc =
+ if n <= 0 then
+ return acc
+ else
+ (v <- f (n-1);
+ tabulate' (n-1) (v :: acc))
+ in
+ tabulate' n []
+ end
diff --git a/lib/ur/list.urs b/lib/ur/list.urs
new file mode 100644
index 0000000..fd56679
--- /dev/null
+++ b/lib/ur/list.urs
@@ -0,0 +1,116 @@
+datatype t = datatype Basis.list
+
+val show : a ::: Type -> show a -> show (t a)
+val eq : a ::: Type -> eq a -> eq (t a)
+
+val foldl : a ::: Type -> b ::: Type -> (a -> b -> b) -> b -> t a -> b
+val foldlAbort : a ::: Type -> b ::: Type -> (a -> b -> option b) -> b -> t a -> option b
+val foldlMapAbort : a ::: Type -> b ::: Type -> c ::: Type
+ -> (a -> b -> option (c * b)) -> b -> t a -> option (t c * b)
+
+val foldr : a ::: Type -> b ::: Type -> (a -> b -> b) -> b -> t a -> b
+
+val length : a ::: Type -> t a -> int
+
+val rev : a ::: Type -> t a -> t a
+
+val revAppend : a ::: Type -> t a -> t a -> t a
+
+val append : a ::: Type -> t a -> t a -> t a
+
+val mp : a ::: Type -> b ::: Type -> (a -> b) -> t a -> t b
+
+val mapPartial : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> t b
+
+val mapi : a ::: Type -> b ::: Type -> (int -> a -> b) -> t a -> t b
+
+val mapX : a ::: Type -> ctx ::: {Unit} -> (a -> xml ctx [] []) -> t a -> xml ctx [] []
+
+val mapXi : a ::: Type -> ctx ::: {Unit} -> (int -> a -> xml ctx [] []) -> t a -> xml ctx [] []
+
+val mapM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type
+ -> (a -> m b) -> t a -> m (t b)
+
+val mapPartialM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> (a -> m (option b)) -> t a -> m (t b)
+
+val mapXM : m ::: (Type -> Type) -> monad m -> a ::: Type -> ctx ::: {Unit}
+ -> (a -> m (xml ctx [] [])) -> t a -> m (xml ctx [] [])
+
+val mapXiM : m ::: (Type -> Type) -> monad m -> a ::: Type -> ctx ::: {Unit} -> (int -> a -> m (xml ctx [] [])) -> t a -> m (xml ctx [] [])
+
+val filter : a ::: Type -> (a -> bool) -> t a -> t a
+
+val exists : a ::: Type -> (a -> bool) -> t a -> bool
+
+val foldlM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type
+ -> (a -> b -> m b) -> b -> t a -> m b
+
+val foldlMi : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type
+ -> (int -> a -> b -> m b) -> b -> t a -> m b
+
+val filterM : m ::: (Type -> Type) -> monad m -> a ::: Type
+ -> (a -> m bool) -> t a -> m (t a)
+
+val foldlMap : a ::: Type -> b ::: Type -> c ::: Type
+ -> (a -> b -> c * b) -> b -> t a -> t c * b
+
+val mem : a ::: Type -> eq a -> a -> t a -> bool
+
+val find : a ::: Type -> (a -> bool) -> t a -> option a
+
+val search : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> option b
+
+val all : a ::: Type -> (a -> bool) -> t a -> bool
+
+val app : m ::: (Type -> Type) -> monad m -> a ::: Type
+ -> (a -> m unit) -> t a -> m unit
+
+val appi : m ::: (Type -> Type) -> monad m -> a ::: Type
+ -> (int -> a -> m unit) -> t a -> m unit
+
+val tabulateM : m ::: (Type -> Type) -> monad m -> a ::: Type
+ -> (int -> m a) -> int -> m (t a)
+
+val mapQuery : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
+ -> [tables ~ exps] =>
+ sql_query [] [] tables exps
+ -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> t)
+ -> transaction (list t)
+
+val mapQueryM : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
+ -> [tables ~ exps] =>
+ sql_query [] [] tables exps
+ -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t)
+ -> transaction (list t)
+
+val mapQueryPartialM : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
+ -> [tables ~ exps] =>
+ sql_query [] [] tables exps
+ -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t))
+ -> transaction (list t)
+
+val sort : a ::: Type -> (a -> a -> bool) (* > predicate *) -> t a -> t a
+
+val nth : a ::: Type -> list a -> int -> option a
+val replaceNth : a ::: Type -> list a -> int -> a -> list a
+
+(** Association lists *)
+
+val assoc : a ::: Type -> b ::: Type -> eq a -> a -> t (a * b) -> option b
+
+val assocAdd : a ::: Type -> b ::: Type -> eq a -> a -> b -> t (a * b) -> t (a * b)
+
+(** Converting records to lists *)
+
+val recToList : a ::: Type -> r ::: {Unit} -> folder r -> $(mapU a r) -> t a
+
+(* Divide a list into two sections at a particular 0-based position, returning the second, first, or both parts, respectively. *)
+val drop : t ::: Type -> int -> list t -> list t
+val take : t ::: Type -> int -> list t -> list t
+val splitAt : t ::: Type -> int -> list t -> list t * list t
+
+(** Longest prefix of elements that satisfy a predicate, returned along with the remaining suffix *)
+val span : a ::: Type -> (a -> bool) -> t a -> t a * t a
+
+(** Group a list into maximal adjacent segments where all elements compare as equal, according to the provided predicate. *)
+val groupBy : a ::: Type -> (a -> a -> bool) -> t a -> t (t a)
diff --git a/lib/ur/listPair.ur b/lib/ur/listPair.ur
new file mode 100644
index 0000000..94b9287
--- /dev/null
+++ b/lib/ur/listPair.ur
@@ -0,0 +1,46 @@
+fun foldlAbort [a] [b] [c] f =
+ let
+ fun foldlAbort' acc ls1 ls2 =
+ case (ls1, ls2) of
+ ([], []) => Some acc
+ | (x1 :: ls1, x2 :: ls2) =>
+ (case f x1 x2 acc of
+ None => None
+ | Some acc' => foldlAbort' acc' ls1 ls2)
+ | _ => None
+ in
+ foldlAbort'
+ end
+
+fun mapX [a] [b] [ctx ::: {Unit}] f =
+ let
+ fun mapX' ls1 ls2 =
+ case (ls1, ls2) of
+ ([], []) => <xml/>
+ | (x1 :: ls1, x2 :: ls2) => <xml>{f x1 x2}{mapX' ls1 ls2}</xml>
+ | _ => error <xml>ListPair.mapX: Unequal list lengths</xml>
+ in
+ mapX'
+ end
+
+fun all [a] [b] f =
+ let
+ fun all' ls1 ls2 =
+ case (ls1, ls2) of
+ ([], []) => True
+ | (x1 :: ls1, x2 :: ls2) => f x1 x2 && all' ls1 ls2
+ | _ => False
+ in
+ all'
+ end
+
+fun mp [a] [b] [c] (f : a -> b -> c) =
+ let
+ fun map' ls1 ls2 =
+ case (ls1, ls2) of
+ ([], []) => []
+ | (x1 :: ls1, x2 :: ls2) => f x1 x2 :: map' ls1 ls2
+ | _ => error <xml>ListPair.map2: Unequal list lengths</xml>
+ in
+ map'
+ end
diff --git a/lib/ur/listPair.urs b/lib/ur/listPair.urs
new file mode 100644
index 0000000..b473e22
--- /dev/null
+++ b/lib/ur/listPair.urs
@@ -0,0 +1,10 @@
+val foldlAbort : a ::: Type -> b ::: Type -> c ::: Type
+ -> (a -> b -> c -> option c) -> c -> list a -> list b -> option c
+
+val mapX : a ::: Type -> b ::: Type -> ctx ::: {Unit}
+ -> (a -> b -> xml ctx [] []) -> list a -> list b -> xml ctx [] []
+
+val all : a ::: Type -> b ::: Type -> (a -> b -> bool) -> list a -> list b -> bool
+
+val mp : a ::: Type -> b ::: Type -> c ::: Type
+ -> (a -> b -> c) -> list a -> list b -> list c
diff --git a/lib/ur/monad.ur b/lib/ur/monad.ur
new file mode 100644
index 0000000..8bff013
--- /dev/null
+++ b/lib/ur/monad.ur
@@ -0,0 +1,140 @@
+fun exec [m ::: Type -> Type] (_ : monad m) [ts ::: {Type}] r (fd : folder ts) =
+ @foldR [m] [fn ts => m $ts]
+ (fn [nm :: Name] [v :: Type] [rest :: {Type}] [[nm] ~ rest] action acc =>
+ this <- action;
+ others <- acc;
+ return ({nm = this} ++ others))
+ (return {}) fd r
+
+fun ignore [m ::: Type -> Type] (_ : monad m) [t] (v : m t) = x <- v; return ()
+
+fun mp [m] (_ : monad m) [a] [b] f m =
+ v <- m;
+ return (f v)
+
+val liftM = @@mp
+
+fun foldR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: {K} -> Type]
+ (f : nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf t -> tr rest -> m (tr ([nm = t] ++ rest)))
+ (i : tr []) [r ::: {K}] (fl : folder r) =
+ @Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ (acc : _ -> m (tr rest)) r =>
+ acc' <- acc (r -- nm);
+ f [nm] [t] [rest] r.nm acc')
+ (fn _ => return i)
+ fl
+
+fun foldR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type]
+ (f : nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest)))
+ (i : tr []) [r ::: {K}] (fl : folder r) =
+ @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ (acc : _ -> _ -> m (tr rest)) r1 r2 =>
+ acc' <- acc (r1 -- nm) (r2 -- nm);
+ f [nm] [t] [rest] r1.nm r2.nm acc')
+ (fn _ _ => return i)
+ fl
+
+fun foldR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type]
+ (f : nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest)))
+ (i : tr []) [r ::: {K}] (fl : folder r) =
+ @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 =>
+ acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
+ f [nm] [t] [rest] r1.nm r2.nm r3.nm acc')
+ (fn _ _ _ => return i)
+ fl
+
+fun mapR0 [K] [m] (_ : monad m) [tr :: K -> Type]
+ (f : nm :: Name -> t :: K -> m (tr t)) [r ::: {K}] (fl : folder r) =
+ @Top.fold [fn r => m ($(map tr r))]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : m ($(map tr rest))) =>
+ v <- f [nm] [t];
+ vs <- acc;
+ return (vs ++ {nm = v}))
+ (return {})
+ fl
+
+fun mapR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: K -> Type]
+ (f : nm :: Name -> t :: K -> tf t -> m (tr t)) =
+ @@foldR [m] _ [tf] [fn r => $(map tr r)]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v : tf t)
+ (acc : $(map tr rest)) =>
+ v' <- f [nm] [t] v;
+ return (acc ++ {nm = v'}))
+ {}
+
+fun mapR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: K -> Type]
+ (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t)) =
+ @@foldR2 [m] _ [tf1] [tf2] [fn r => $(map tr r)]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v1 : tf1 t) (v2 : tf2 t)
+ (acc : $(map tr rest)) =>
+ v' <- f [nm] [t] v1 v2;
+ return (acc ++ {nm = v'}))
+ {}
+
+fun mapR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: K -> Type]
+ (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> tf3 t -> m (tr t)) =
+ @@foldR3 [m] _ [tf1] [tf2] [tf3] [fn r => $(map tr r)]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v1 : tf1 t) (v2 : tf2 t) (v3 : tf3 t)
+ (acc : $(map tr rest)) =>
+ v' <- f [nm] [t] v1 v2 v3;
+ return (acc ++ {nm = v'}))
+ {}
+
+fun foldMapR [K] [m] (_ : monad m) [tf :: K -> Type] [tf' :: K -> Type] [tr :: {K} -> Type]
+ (f : nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf t -> tr rest -> m (tf' t * tr ([nm = t] ++ rest)))
+ (i : tr []) [r ::: {K}] (fl : folder r) =
+ @Top.fold [fn r :: {K} => $(map tf r) -> m ($(map tf' r) * tr r)]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ (acc : _ -> m ($(map tf' rest) * tr rest)) r =>
+ p <- acc (r -- nm);
+ p' <- f [nm] [t] [rest] r.nm p.2;
+ return ({nm = p'.1} ++ p.1, p'.2))
+ (fn _ => return ({}, i))
+ fl
+
+fun appR [K] [m] (_ : monad m) [tf :: K -> Type]
+ (f : nm :: Name -> t :: K -> tf t -> m unit)
+ [r ::: {K}] (fl : folder r) =
+ @Top.fold [fn r :: {K} => $(map tf r) -> m unit]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r =>
+ acc (r -- nm);
+ f [nm] [t] r.nm)
+ (fn _ => return ())
+ fl
+
+fun appR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type]
+ (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> m unit)
+ [r ::: {K}] (fl : folder r) =
+ @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m unit]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 =>
+ acc (r1 -- nm) (r2 -- nm);
+ f [nm] [t] r1.nm r2.nm)
+ (fn _ _ => return ())
+ fl
+
+fun appR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type]
+ (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> tf3 t -> m unit)
+ [r ::: {K}] (fl : folder r) =
+ @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m unit]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 r3 =>
+ acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
+ f [nm] [t] r1.nm r2.nm r3.nm)
+ (fn _ _ _ => return ())
+ fl
+
+fun liftM2 [m ::: Type -> Type] (_ : monad m) [a] [b] [c] (f : a -> b -> c) (mx : m a) (my : m b) : m c =
+ x <- mx;
+ y <- my;
+ return (f x y)
diff --git a/lib/ur/monad.urs b/lib/ur/monad.urs
new file mode 100644
index 0000000..8ca8d0a
--- /dev/null
+++ b/lib/ur/monad.urs
@@ -0,0 +1,90 @@
+val exec : m ::: (Type -> Type) -> monad m -> ts ::: {Type}
+ -> $(map m ts) -> folder ts -> m $ts
+
+val ignore : m ::: (Type -> Type) -> monad m -> t ::: Type
+ -> m t -> m unit
+
+val mp : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type
+ -> (a -> b) -> m a -> m b
+
+val liftM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type
+ -> (a -> b) -> m a -> m b
+(* Haskell-style synonym for [mp] *)
+
+val liftM2 : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> c ::: Type
+ -> (a -> b -> c) -> m a -> m b -> m c
+
+val foldR : K --> m ::: (Type -> Type) -> monad m
+ -> tf :: (K -> Type)
+ -> tr :: ({K} -> Type)
+ -> (nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf t -> tr rest -> m (tr ([nm = t] ++ rest)))
+ -> tr []
+ -> r ::: {K} -> folder r -> $(map tf r) -> m (tr r)
+
+val foldR2 : K --> m ::: (Type -> Type) -> monad m
+ -> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
+ -> tr :: ({K} -> Type)
+ -> (nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest)))
+ -> tr []
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r)
+
+val foldR3 : K --> m ::: (Type -> Type) -> monad m
+ -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
+ -> tr :: ({K} -> Type)
+ -> (nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest)))
+ -> tr []
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)
+
+val mapR0 : K --> m ::: (Type -> Type) -> monad m
+ -> tr :: (K -> Type)
+ -> (nm :: Name -> t :: K -> m (tr t))
+ -> r ::: {K} -> folder r -> m ($(map tr r))
+
+val mapR : K --> m ::: (Type -> Type) -> monad m
+ -> tf :: (K -> Type)
+ -> tr :: (K -> Type)
+ -> (nm :: Name -> t :: K -> tf t -> m (tr t))
+ -> r ::: {K} -> folder r -> $(map tf r) -> m ($(map tr r))
+
+val mapR2 : K --> m ::: (Type -> Type) -> monad m
+ -> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
+ -> tr :: (K -> Type)
+ -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t))
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r))
+
+val mapR3 : K --> m ::: (Type -> Type) -> monad m
+ -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
+ -> tr :: (K -> Type)
+ -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> tf3 t -> m (tr t))
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m ($(map tr r))
+
+val foldMapR : K --> m ::: (Type -> Type) -> monad m
+ -> tf :: (K -> Type)
+ -> tf' :: (K -> Type)
+ -> tr :: ({K} -> Type)
+ -> (nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf t -> tr rest -> m (tf' t * tr ([nm = t] ++ rest)))
+ -> tr []
+ -> r ::: {K} -> folder r -> $(map tf r) -> m ($(map tf' r) * tr r)
+
+val appR : K --> m ::: (Type -> Type) -> monad m
+ -> tf :: (K -> Type)
+ -> (nm :: Name -> t :: K -> tf t -> m unit)
+ -> r ::: {K} -> folder r -> $(map tf r) -> m unit
+
+val appR2 : K --> m ::: (Type -> Type) -> monad m
+ -> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
+ -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m unit)
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m unit
+
+val appR3 : K --> m ::: (Type -> Type) -> monad m
+ -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
+ -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> tf3 t -> m unit)
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m unit
diff --git a/lib/ur/option.ur b/lib/ur/option.ur
new file mode 100644
index 0000000..baa0846
--- /dev/null
+++ b/lib/ur/option.ur
@@ -0,0 +1,61 @@
+datatype t = datatype Basis.option
+
+val monad = mkMonad {Return = @@Some,
+ Bind = fn [a] [b] (m1 : t a) (m2 : a -> t b) =>
+ case m1 of
+ None => None
+ | Some v => m2 v}
+
+fun eq [a] (_ : eq a) =
+ mkEq (fn x y =>
+ case (x, y) of
+ (None, None) => True
+ | (Some x, Some y) => x = y
+ | _ => False)
+
+fun ord [a] (_ : ord a) =
+ mkOrd {Lt = fn x y =>
+ case (x, y) of
+ (None, Some _) => True
+ | (Some x, Some y) => x < y
+ | _ => False,
+ Le = fn x y =>
+ case (x, y) of
+ (None, _) => True
+ | (Some x, Some y) => x <= y
+ | _ => False}
+
+fun isNone [a] x =
+ case x of
+ None => True
+ | Some _ => False
+
+fun isSome [a] x =
+ case x of
+ None => False
+ | Some _ => True
+
+fun mp [a] [b] f x =
+ case x of
+ None => None
+ | Some y => Some (f y)
+
+fun app [m] [a] (_ : monad m) (f : a -> m {}) x =
+ case x of
+ None => return ()
+ | Some y => f y
+
+fun bind [a] [b] f x =
+ case x of
+ None => None
+ | Some y => f y
+
+fun get [a] (x : a) (o : option a) =
+ case o of
+ None => x
+ | Some v => v
+
+fun unsafeGet [a] (o : option a) =
+ case o of
+ None => error <xml>Option.unsafeGet: encountered None</xml>
+ | Some v => v
diff --git a/lib/ur/option.urs b/lib/ur/option.urs
new file mode 100644
index 0000000..c30c40e
--- /dev/null
+++ b/lib/ur/option.urs
@@ -0,0 +1,16 @@
+datatype t = datatype Basis.option
+
+val monad : monad t
+
+val eq : a ::: Type -> eq a -> eq (t a)
+val ord : a ::: Type -> ord a -> ord (t a)
+
+val isNone : a ::: Type -> t a -> bool
+val isSome : a ::: Type -> t a -> bool
+
+val mp : a ::: Type -> b ::: Type -> (a -> b) -> t a -> t b
+val app : m ::: (Type -> Type) -> a ::: Type -> monad m -> (a -> m {}) -> t a -> m {}
+val bind : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> t b
+
+val get : a ::: Type -> a -> option a -> a
+val unsafeGet : a ::: Type -> option a -> a
diff --git a/lib/ur/string.ur b/lib/ur/string.ur
new file mode 100644
index 0000000..da4e7eb
--- /dev/null
+++ b/lib/ur/string.ur
@@ -0,0 +1,113 @@
+type t = Basis.string
+
+val str = Basis.str1
+
+val length = Basis.strlen
+val lengthGe = Basis.strlenGe
+val append = Basis.strcat
+
+val sub = Basis.strsub
+val suffix = Basis.strsuffix
+
+val index = Basis.strindex
+fun sindex r = Basis.strsindex r.Haystack r.Needle
+val atFirst = Basis.strchr
+
+fun mindex {Haystack = s, Needle = chs} =
+ let
+ val n = Basis.strcspn s chs
+ in
+ if n >= length s then
+ None
+ else
+ Some n
+ end
+
+fun substring s {Start = start, Len = len} = Basis.substring s start len
+
+fun seek s ch =
+ case index s ch of
+ None => None
+ | Some i => Some (suffix s (i + 1))
+fun mseek {Haystack = s, Needle = chs} =
+ case mindex {Haystack = s, Needle = chs} of
+ None => None
+ | Some i => Some (sub s i, suffix s (i + 1))
+
+fun split s ch =
+ case index s ch of
+ None => None
+ | Some i => Some (substring s {Start = 0, Len = i},
+ suffix s (i + 1))
+fun split' s ch =
+ case index s ch of
+ None => None
+ | Some i => Some (substring s {Start = 0, Len = i},
+ suffix s i)
+fun msplit {Haystack = s, Needle = chs} =
+ case mindex {Haystack = s, Needle = chs} of
+ None => None
+ | Some i => Some (substring s {Start = 0, Len = i},
+ sub s i,
+ suffix s (i + 1))
+
+fun ssplit r =
+ case sindex r of
+ None => None
+ | Some i => Some (substring r.Haystack {Start = 0, Len = i},
+ suffix r.Haystack (i + length r.Needle))
+
+fun all f s =
+ let
+ val len = length s
+
+ fun al i =
+ i >= len
+ || (f (sub s i) && al (i + 1))
+ in
+ al 0
+ end
+
+fun mp f s =
+ let
+ fun mp' i acc =
+ if i < 0 then
+ acc
+ else
+ mp' (i - 1) (str (f (sub s i)) ^ acc)
+ in
+ mp' (length s - 1) ""
+ end
+
+fun newlines [ctx] [[Body] ~ ctx] (s : string) : xml ([Body] ++ ctx) [] [] =
+ case split s #"\n" of
+ None => cdata s
+ | Some (s1, s2) => <xml>{[s1]}<br/>{newlines s2}</xml>
+
+fun isPrefix {Full = f, Prefix = p} =
+ length f >= length p && substring f {Start = 0, Len = length p} = p
+
+fun trim s =
+ let
+ val len = length s
+
+ fun findStart i =
+ if i < len && isspace (sub s i) then
+ findStart (i+1)
+ else
+ i
+
+ fun findFinish i =
+ if i >= 0 && isspace (sub s i) then
+ findFinish (i-1)
+ else
+ i
+
+ val start = findStart 0
+ val finish = findFinish (len - 1)
+ in
+ if finish >= start then
+ substring s {Start = start, Len = finish - start + 1}
+ else
+ ""
+ end
diff --git a/lib/ur/string.urs b/lib/ur/string.urs
new file mode 100644
index 0000000..1bdca96
--- /dev/null
+++ b/lib/ur/string.urs
@@ -0,0 +1,37 @@
+type t = string
+
+val str : char -> t
+
+val length : t -> int
+val lengthGe : t -> int -> bool
+
+val append : t -> t -> t
+
+val sub : t -> int -> char
+val suffix : t -> int -> string
+
+val index : t -> char -> option int
+val sindex : {Haystack : t, Needle : t} -> option int
+val atFirst : t -> char -> option string
+
+val mindex : {Haystack : t, Needle : t} -> option int
+
+val substring : t -> {Start : int, Len : int} -> string
+
+val seek : t -> char -> option string
+val mseek : {Haystack : t, Needle : t} -> option (char * string)
+
+val split : t -> char -> option (string * string)
+val split' : t -> char -> option (string * string) (* The matched character is kept at the beginning of the suffix. *)
+val msplit : {Haystack : t, Needle : t} -> option (string * char * string)
+
+val ssplit : {Haystack : t, Needle : t} -> option (string * string)
+
+val all : (char -> bool) -> string -> bool
+val mp : (char -> char) -> string -> string
+
+val newlines : ctx ::: {Unit} -> [[Body] ~ ctx] => string -> xml ([Body] ++ ctx) [] []
+
+val isPrefix : {Full : t, Prefix : t} -> bool
+
+val trim : t -> t
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
new file mode 100644
index 0000000..0256791
--- /dev/null
+++ b/lib/ur/top.ur
@@ -0,0 +1,430 @@
+(** Row folding *)
+
+con folder = K ==> fn r :: {K} =>
+ tf :: ({K} -> Type)
+ -> (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
+ tf r -> tf ([nm = v] ++ r))
+ -> tf [] -> tf r
+
+fun fold [K] [tf :: {K} -> Type]
+ (f : (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
+ tf r -> tf ([nm = v] ++ r)))
+ (i : tf []) [r ::: {K}] (fl : folder r) = fl [tf] f i
+
+structure Folder = struct
+ fun nil [K] [tf :: {K} -> Type]
+ (f : nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
+ tf r -> tf ([nm = v] ++ r))
+ (i : tf []) = i
+
+ fun cons [K] [r ::: {K}] [nm :: Name] [v :: K] [[nm] ~ r] (fold : folder r)
+ [tf :: {K} -> Type]
+ (f : nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
+ tf r -> tf ([nm = v] ++ r))
+ (i : tf []) = f [nm] [v] [r] (fold [tf] f i)
+
+ fun concat [K] [r1 ::: {K}] [r2 ::: {K}] [r1 ~ r2]
+ (f1 : folder r1) (f2 : folder r2)
+ [tf :: {K} -> Type]
+ (f : nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
+ tf r -> tf ([nm = v] ++ r))
+ (i : tf []) =
+ f1 [fn r1' => [r1' ~ r2] => tf (r1' ++ r2)]
+ (fn [nm :: Name] [v :: K] [r1' :: {K}] [[nm] ~ r1']
+ (acc : [r1' ~ r2] => tf (r1' ++ r2))
+ [[nm = v] ++ r1' ~ r2] =>
+ f [nm] [v] [r1' ++ r2] acc)
+ (fn [[] ~ r2] => f2 [tf] f i)
+
+ fun mp [K1] [K2] [f ::: K1 -> K2] [r ::: {K1}]
+ (fold : folder r)
+ [tf :: {K2} -> Type]
+ (f : nm :: Name -> v :: K2 -> r :: {K2} -> [[nm] ~ r] =>
+ tf r -> tf ([nm = v] ++ r))
+ (i : tf []) =
+ fold [fn r => tf (map f r)]
+ (fn [nm :: Name] [v :: K1] [rest :: {K1}] [[nm] ~ rest] (acc : tf (map f rest)) =>
+ f [nm] [f v] [map f rest] acc)
+ i
+end
+
+
+fun not b = if b then False else True
+
+con ident = K ==> fn t :: K => t
+con record (t :: {Type}) = $t
+con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1
+con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2
+con fst3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.1
+con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2
+con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3
+
+con mapU = K ==> fn f :: K => map (fn _ :: Unit => f)
+
+con ex = K ==> fn tf :: (K -> Type) =>
+ res ::: Type -> (choice :: K -> tf choice -> res) -> res
+
+fun ex_intro [K] [tf :: K -> Type] [choice :: K] (body : tf choice) : ex tf =
+ fn [res] (f : choice :: K -> tf choice -> res) =>
+ f [choice] body
+
+fun ex_elim [K] [tf ::: K -> Type] (v : ex tf) [res ::: Type] = @@v [res]
+
+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] [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) =
+ fl [fn r :: {K} => $(map tf r)]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc =>
+ acc ++ {nm = f [t]})
+ {}
+
+fun mp [K] [tf1 :: K -> Type] [tf2 :: K -> Type] (f : t ::: K -> tf1 t -> tf2 t) [r ::: {K}] (fl : folder r) =
+ fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r)]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r =>
+ acc (r -- nm) ++ {nm = f r.nm})
+ (fn _ => {})
+
+fun map2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type]
+ (f : t ::: K -> tf1 t -> tf2 t -> tf3 t) [r ::: {K}] (fl : folder r) =
+ fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r)]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 =>
+ acc (r1 -- nm) (r2 -- nm) ++ {nm = f r1.nm r2.nm})
+ (fn _ _ => {})
+
+fun map3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tf :: K -> Type]
+ (f : t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) [r ::: {K}] (fl : folder r) =
+ fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 r3 =>
+ acc (r1 -- nm) (r2 -- nm) (r3 -- nm) ++ {nm = f r1.nm r2.nm r3.nm})
+ (fn _ _ _ => {})
+
+fun foldUR [tf :: Type] [tr :: {Unit} -> Type]
+ (f : nm :: Name -> rest :: {Unit}
+ -> [[nm] ~ rest] =>
+ tf -> tr rest -> tr ([nm] ++ rest))
+ (i : tr []) [r ::: {Unit}] (fl : folder r) =
+ fl [fn r :: {Unit} => $(mapU tf r) -> tr r]
+ (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r =>
+ f [nm] [rest] r.nm (acc (r -- nm)))
+ (fn _ => i)
+
+fun foldUR2 [tf1 :: Type] [tf2 :: Type] [tr :: {Unit} -> Type]
+ (f : nm :: Name -> rest :: {Unit}
+ -> [[nm] ~ rest] =>
+ tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
+ (i : tr []) [r ::: {Unit}] (fl : folder r) =
+ fl [fn r :: {Unit} => $(mapU tf1 r) -> $(mapU tf2 r) -> tr r]
+ (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r1 r2 =>
+ f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+ (fn _ _ => i)
+
+fun foldR [K] [tf :: K -> Type] [tr :: {K} -> Type]
+ (f : nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf t -> tr rest -> tr ([nm = t] ++ rest))
+ (i : tr []) [r ::: {K}] (fl : folder r) =
+ fl [fn r :: {K} => $(map tf r) -> tr r]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> tr rest) r =>
+ f [nm] [t] [rest] r.nm (acc (r -- nm)))
+ (fn _ => i)
+
+fun foldR2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type]
+ (f : nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+ (i : tr []) [r ::: {K}] (fl : folder r) =
+ fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ (acc : _ -> _ -> tr rest) r1 r2 =>
+ f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+ (fn _ _ => i)
+
+fun foldR3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type]
+ (f : nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
+ (i : tr []) [r ::: {K}] (fl : folder r) =
+ fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ (acc : _ -> _ -> _ -> tr rest) r1 r2 r3 =>
+ f [nm] [t] [rest] r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm)))
+ (fn _ _ _ => i)
+
+fun mapUX [tf :: Type] [ctx :: {Unit}]
+ (f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf -> xml ctx [] []) =
+ @@foldR [fn _ => tf] [fn _ => xml ctx [] []]
+ (fn [nm :: Name] [u :: Unit] [rest :: {Unit}] [[nm] ~ rest] r acc =>
+ <xml>{f [nm] [rest] r}{acc}</xml>)
+ <xml/>
+
+fun mapUX_rev [tf :: Type] [ctx :: {Unit}]
+ (f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf -> xml ctx [] []) =
+ @@foldR [fn _ => tf] [fn _ => xml ctx [] []]
+ (fn [nm :: Name] [u :: Unit] [rest :: {Unit}] [[nm] ~ rest] r acc =>
+ <xml>{acc}{f [nm] [rest] r}</xml>)
+ <xml/>
+
+fun mapX [K] [tf :: K -> Type] [ctx :: {Unit}]
+ (f : nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf t -> xml ctx [] []) =
+ @@foldR [tf] [fn _ => xml ctx [] []]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc =>
+ <xml>{f [nm] [t] [rest] r}{acc}</xml>)
+ <xml/>
+
+fun mapUX2 [tf1 :: Type] [tf2 :: Type] [ctx :: {Unit}]
+ (f : nm :: Name -> rest :: {Unit}
+ -> [[nm] ~ rest] =>
+ tf1 -> tf2 -> xml ctx [] []) =
+ @@foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
+ (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] v1 v2 acc =>
+ <xml>{f [nm] [rest] v1 v2}{acc}</xml>)
+ <xml/>
+
+fun mapX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}]
+ (f : nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> xml ctx [] []) =
+ @@foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ r1 r2 acc =>
+ <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
+ <xml/>
+
+fun mapX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}]
+ (f : nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) =
+ @@foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ r1 r2 r3 acc =>
+ <xml>{f [nm] [t] [rest] r1 r2 r3}{acc}</xml>)
+ <xml/>
+
+fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [] [t = fs] [])
+ (f : $fs -> state -> transaction state) (i : state) =
+ query q (fn r => f r.t) i
+
+fun query1' [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [] [t = fs] [])
+ (f : $fs -> state -> state) (i : state) =
+ query q (fn r s => return (f r.t s)) i
+
+val rev = fn [a] =>
+ let
+ fun rev' acc (ls : list a) =
+ case ls of
+ [] => acc
+ | x :: ls => rev' (x :: acc) ls
+ in
+ rev' []
+ end
+
+fun queryL [tables] [exps] [tables ~ exps] (q : sql_query [] [] tables exps) =
+ ls <- query q (fn r ls => return (r :: ls)) [];
+ return (rev ls)
+
+fun queryL1 [t ::: Name] [fs ::: {Type}] (q : sql_query [] [] [t = fs] []) =
+ ls <- query q (fn r ls => return (r.t :: ls)) [];
+ return (rev ls)
+
+fun queryI [tables ::: {{Type}}] [exps ::: {Type}]
+ [tables ~ exps] (q : sql_query [] [] tables exps)
+ (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
+ -> transaction unit) =
+ query q
+ (fn fs _ => f fs)
+ ()
+
+fun queryI1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] [])
+ (f : $fs -> transaction unit) =
+ query q
+ (fn fs _ => f fs.nm)
+ ()
+
+fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
+ [tables ~ exps] (q : sql_query [] [] tables exps)
+ (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
+ -> xml ctx inp []) =
+ query q
+ (fn fs acc => return <xml>{acc}{f fs}</xml>)
+ <xml/>
+
+fun rev [a] (ls : list a) : list a =
+ let
+ fun rev' ls acc =
+ case ls of
+ [] => acc
+ | x :: ls => rev' ls (x :: acc)
+ in
+ rev' ls []
+ end
+
+fun queryXI [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
+ [tables ~ exps] (q : sql_query [] [] tables exps)
+ (f : int -> $(exps ++ map (fn fields :: {Type} => $fields) tables)
+ -> xml ctx inp []) =
+ let
+ fun qxi ls i =
+ case ls of
+ [] => <xml/>
+ | x :: ls => <xml>{f i x}{qxi ls (i+1)}</xml>
+ in
+ ls <- queryL q;
+ return (qxi (rev ls) 0)
+ end
+
+fun queryX1 [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
+ (q : sql_query [] [] [nm = fs] [])
+ (f : $fs -> xml ctx inp []) =
+ query q
+ (fn fs acc => return <xml>{acc}{f fs.nm}</xml>)
+ <xml/>
+
+fun queryX1I [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
+ (q : sql_query [] [] [nm = fs] [])
+ (f : int -> $fs -> xml ctx inp []) =
+ let
+ fun qx1i ls i =
+ case ls of
+ [] => <xml/>
+ | x :: ls => <xml>{f i x.nm}{qx1i ls (i+1)}</xml>
+ in
+ ls <- queryL q;
+ return (qx1i (rev ls) 0)
+ end
+
+fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
+ [tables ~ exps] (q : sql_query [] [] tables exps)
+ (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
+ -> transaction (xml ctx inp [])) =
+ query q
+ (fn fs acc =>
+ r <- f fs;
+ return <xml>{acc}{r}</xml>)
+ <xml/>
+
+fun queryX1' [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
+ (q : sql_query [] [] [nm = fs] [])
+ (f : $fs -> transaction (xml ctx inp [])) =
+ query q
+ (fn fs acc =>
+ r <- f fs.nm;
+ return <xml>{acc}{r}</xml>)
+ <xml/>
+
+fun queryXE' [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
+ (q : sql_query [] [] [] exps)
+ (f : $exps -> transaction (xml ctx inp [])) =
+ query q
+ (fn fs acc =>
+ r <- f fs;
+ return <xml>{acc}{r}</xml>)
+ <xml/>
+
+fun hasRows [tables ::: {{Type}}] [exps ::: {Type}]
+ [tables ~ exps]
+ (q : sql_query [] [] tables exps) =
+ query q
+ (fn _ _ => return True)
+ False
+
+fun oneOrNoRows [tables ::: {{Type}}] [exps ::: {Type}]
+ [tables ~ exps]
+ (q : sql_query [] [] tables exps) =
+ query q
+ (fn fs _ => return (Some fs))
+ None
+
+fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] []) =
+ query q
+ (fn fs _ => return (Some fs.nm))
+ None
+
+fun oneOrNoRowsE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] [] (mapU [] tabs) [nm = t]) =
+ query q
+ (fn fs _ => return (Some fs.nm))
+ None
+
+fun oneRow [tables ::: {{Type}}] [exps ::: {Type}]
+ [tables ~ exps] (q : sql_query [] [] tables exps) =
+ o <- oneOrNoRows q;
+ return (case o of
+ None => error <xml>Query returned no rows</xml>
+ | Some r => r)
+
+fun oneRow1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] []) =
+ o <- oneOrNoRows q;
+ return (case o of
+ None => error <xml>Query returned no rows</xml>
+ | Some r => r.nm)
+
+fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] [] (mapU [] tabs) [nm = t]) =
+ o <- oneOrNoRows q;
+ return (case o of
+ None => error <xml>Query returned no rows</xml>
+ | Some r => r.nm)
+
+fun nonempty [fs] [us] (t : sql_table fs us) =
+ oneRowE1 (SELECT COUNT( * ) > 0 AS B FROM t)
+
+fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
+ [t ::: Type] (_ : sql_injectable (option t))
+ (e1 : sql_exp tables agg exps (option t))
+ (e2 : sql_exp tables agg exps (option t)) =
+ (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2})
+
+fun eqNullable' [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
+ [t ::: Type] (_ : sql_injectable (option t))
+ (e1 : sql_exp tables agg exps (option t))
+ (e2 : option t) =
+ 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
+
+fun postFields pb =
+ let
+ fun postFields' s =
+ case firstFormField s of
+ None => []
+ | Some f => (fieldName f, fieldValue f) :: postFields' (remainingFields f)
+ in
+ case postType pb of
+ "application/x-www-form-urlencoded" => postFields' (postData pb)
+ | _ => error <xml>Tried to get POST fields, but MIME type is not "application/x-www-form-urlencoded"</xml>
+ end
+
+fun max [t] ( _ : ord t) (x : t) (y : t) : t =
+ if x > y then x else y
+fun min [t] ( _ : ord t) (x : t) (y : t) : t =
+ if x < y then x else y
+
+fun assert [a] (cond: bool) (msg: string) (loc: string) (x:a): a =
+ if cond then x else error <xml>{txt msg} at {txt loc}</xml>
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
new file mode 100644
index 0000000..ec09895
--- /dev/null
+++ b/lib/ur/top.urs
@@ -0,0 +1,303 @@
+(** Row folding *)
+
+con folder :: K --> {K} -> Type
+
+val fold : K --> tf :: ({K} -> Type)
+ -> (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
+ tf r -> tf ([nm = v] ++ r))
+ -> tf []
+ -> r ::: {K} -> folder r -> tf r
+
+structure Folder : sig
+ val nil : K --> folder (([]) :: {K})
+ val cons : K --> r ::: {K} -> nm :: Name -> v :: K
+ -> [[nm] ~ r] => folder r -> folder ([nm = v] ++ r)
+ val concat : K --> r1 ::: {K} -> r2 ::: {K}
+ -> [r1 ~ r2] => folder r1 -> folder r2 -> folder (r1 ++ r2)
+ val mp : K1 --> K2 --> f ::: (K1 -> K2) -> r ::: {K1}
+ -> folder r -> folder (map f r)
+end
+
+
+val not : bool -> bool
+
+(* Type-level identity function *)
+con ident = K ==> fn t :: K => t
+
+(* Type-level function which yields the value-level record
+ described by the given type-level record *)
+con record = fn t :: {Type} => $t
+
+con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1
+con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2
+con fst3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.1
+con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2
+con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3
+
+(* Convert a record of n Units into a type-level record where
+ each field has the same value (which describes a uniformly
+ typed record) *)
+con mapU = K ==> fn f :: K => map (fn _ :: Unit => f)
+
+(* Existential type former *)
+con ex :: K --> (K -> Type) -> Type
+
+(* Introduction of existential type *)
+val ex_intro : K --> tf :: (K -> Type) -> choice :: K -> tf choice -> ex tf
+
+(* Eliminator for existential type *)
+val ex_elim : K --> tf ::: (K -> Type) -> ex tf -> res ::: Type -> (choice :: K -> tf choice -> res) -> res
+
+(* Composition of ordinary (value-level) functions *)
+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 []
+
+(* Given a polymorphic type (tf) and a means of constructing
+ "default" values of tf applied to arbitrary arguments,
+ constructs records consisting of those "default" values *)
+val map0 : K --> tf :: (K -> Type)
+ -> (t :: K -> tf t)
+ -> r ::: {K} -> folder r -> $(map tf r)
+
+(* Given two polymorphic types (tf1 and tf2) and a means of
+ converting from tf1 t to tf2 t for arbitrary t,
+ converts records of tf1's to records of tf2's *)
+val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
+ -> (t ::: K -> tf1 t -> tf2 t)
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r)
+
+(* Two-argument conversion form of mp *)
+val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf :: (K -> Type)
+ -> (t ::: K -> tf1 t -> tf2 t -> tf t)
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r)
+
+(* Three-argument conversion form of mp *)
+val map3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tf :: (K -> Type)
+ -> (t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t)
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)
+
+(* Fold along a uniformly (homogenously) typed record *)
+val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
+ -> (nm :: Name -> rest :: {Unit}
+ -> [[nm] ~ rest] =>
+ tf -> tr rest -> tr ([nm] ++ rest))
+ -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf r) -> tr r
+
+(* Fold (generalized safe zip) along two equal-length uniformly-typed records *)
+val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
+ -> (nm :: Name -> rest :: {Unit}
+ -> [[nm] ~ rest] =>
+ tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
+ -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r
+
+(* Fold along a heterogenously-typed record *)
+val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type)
+ -> (nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf t -> tr rest -> tr ([nm = t] ++ rest))
+ -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r
+
+(* Fold (generalized safe zip) along two heterogenously-typed records *)
+val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
+ -> tr :: ({K} -> Type)
+ -> (nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+ -> tr []
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
+
+(* Fold (generalized safe zip) along three heterogenously-typed records *)
+val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
+ -> tr :: ({K} -> Type)
+ -> (nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
+ -> tr []
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r
+
+(* Generate some XML by mapping over a uniformly-typed record *)
+val mapUX : tf :: Type -> ctx :: {Unit}
+ -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] =>
+ tf -> xml ctx [] [])
+ -> r ::: {Unit} -> folder r -> $(mapU tf r) -> xml ctx [] []
+val mapUX_rev : tf :: Type -> ctx :: {Unit}
+ -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] =>
+ tf -> xml ctx [] [])
+ -> r ::: {Unit} -> folder r -> $(mapU tf r) -> xml ctx [] []
+
+(* Generate some XML by mapping over a heterogenously-typed record *)
+val mapX : K --> tf :: (K -> Type) -> ctx :: {Unit}
+ -> (nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf t -> xml ctx [] [])
+ -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] []
+
+val mapUX2 : tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
+ -> (nm :: Name -> rest :: {Unit}
+ -> [[nm] ~ rest] =>
+ tf1 -> tf2 -> xml ctx [] [])
+ -> r ::: {Unit} -> folder r
+ -> $(mapU tf1 r) -> $(mapU tf2 r) -> xml ctx [] []
+
+val mapX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit}
+ -> (nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> xml ctx [] [])
+ -> r ::: {K} -> folder r
+ -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
+
+val mapX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit}
+ -> (nm :: Name -> t :: K -> rest :: {K}
+ -> [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tf3 t -> xml ctx [] [])
+ -> r ::: {K} -> folder r
+ -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] []
+
+(* Note that the next two functions return elements in the _reverse_ of the natural order!
+ * Such a choice interacts well with the time complexity of standard list operations.
+ * It's easy to regain the natural order by inverting a query's 'ORDER BY' condition. *)
+
+val queryL : tables ::: {{Type}} -> exps ::: {Type}
+ -> [tables ~ exps] =>
+ sql_query [] [] tables exps
+ -> transaction (list $(exps ++ map (fn fields :: {Type} => $fields) tables))
+
+val queryL1 : t ::: Name -> fs ::: {Type}
+ -> sql_query [] [] [t = fs] []
+ -> transaction (list $fs)
+
+val query1 : t ::: Name -> fs ::: {Type} -> state ::: Type
+ -> sql_query [] [] [t = fs] []
+ -> ($fs -> state -> transaction state)
+ -> state
+ -> transaction state
+
+val query1' : t ::: Name -> fs ::: {Type} -> state ::: Type
+ -> sql_query [] [] [t = fs] []
+ -> ($fs -> state -> state)
+ -> state
+ -> transaction state
+
+val queryI : tables ::: {{Type}} -> exps ::: {Type}
+ -> [tables ~ exps] =>
+ sql_query [] [] tables exps
+ -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
+ -> transaction unit)
+ -> transaction unit
+
+val queryI1 : nm ::: Name -> fs ::: {Type}
+ -> sql_query [] [] [nm = fs] []
+ -> ($fs -> transaction unit)
+ -> transaction unit
+
+val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
+ -> [tables ~ exps] =>
+ sql_query [] [] tables exps
+ -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
+ -> xml ctx inp [])
+ -> transaction (xml ctx inp [])
+
+val queryXI : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
+ -> [tables ~ exps] =>
+ sql_query [] [] tables exps
+ -> (int -> $(exps ++ map (fn fields :: {Type} => $fields) tables)
+ -> xml ctx inp [])
+ -> transaction (xml ctx inp [])
+
+val queryX1 : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
+ -> sql_query [] [] [nm = fs] []
+ -> ($fs -> xml ctx inp [])
+ -> transaction (xml ctx inp [])
+
+val queryX1I : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
+ -> sql_query [] [] [nm = fs] []
+ -> (int -> $fs -> xml ctx inp [])
+ -> transaction (xml ctx inp [])
+
+val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
+ -> [tables ~ exps] =>
+ sql_query [] [] tables exps
+ -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
+ -> transaction (xml ctx inp []))
+ -> transaction (xml ctx inp [])
+val queryX1' : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
+ -> sql_query [] [] [nm = fs] []
+ -> ($fs -> transaction (xml ctx inp []))
+ -> transaction (xml ctx inp [])
+val queryXE' : exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
+ -> sql_query [] [] [] exps
+ -> ($exps -> transaction (xml ctx inp []))
+ -> transaction (xml ctx inp [])
+
+val hasRows : tables ::: {{Type}} -> exps ::: {Type}
+ -> [tables ~ exps] =>
+ sql_query [] [] tables exps
+ -> transaction bool
+
+val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
+ -> [tables ~ exps] =>
+ sql_query [] [] tables exps
+ -> transaction
+ (option
+ $(exps
+ ++ map (fn fields :: {Type} => $fields) tables))
+
+val oneOrNoRows1 : nm ::: Name -> fs ::: {Type}
+ -> sql_query [] [] [nm = fs] []
+ -> transaction (option $fs)
+
+val oneOrNoRowsE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
+ -> [tabs ~ [nm]] =>
+ sql_query [] [] (mapU [] tabs) [nm = t]
+ -> transaction (option t)
+
+val oneRow : tables ::: {{Type}} -> exps ::: {Type}
+ -> [tables ~ exps] =>
+ sql_query [] [] tables exps
+ -> transaction
+ $(exps
+ ++ map (fn fields :: {Type} => $fields) tables)
+
+val oneRow1 : nm ::: Name -> fs ::: {Type}
+ -> sql_query [] [] [nm = fs] []
+ -> transaction $fs
+
+val oneRowE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
+ -> [tabs ~ [nm]] =>
+ sql_query [] [] (mapU [] tabs) [nm = t]
+ -> transaction t
+
+val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us
+ -> transaction bool
+
+val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type -> sql_injectable (option t)
+ -> sql_exp tables agg exps (option t)
+ -> sql_exp tables agg exps (option t)
+ -> sql_exp tables agg exps bool
+
+val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type -> sql_injectable (option t)
+ -> sql_exp tables agg exps (option t)
+ -> option t
+ -> sql_exp tables agg exps bool
+
+val mkRead' : t ::: Type -> (string -> option t) -> string -> read t
+
+val postFields : postBody -> list (string * string)
+
+val max : t ::: Type -> ord t -> t -> t -> t
+val min : t ::: Type -> ord t -> t -> t -> t
+
+val assert : t ::: Type
+ -> bool (* Did we avoid something bad? *)
+ -> string (* Explanation of the bad thing *)
+ -> string (* Source location of the bad thing *)
+ -> t (* Return this value if all went well. *)
+ -> t
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-22 01:24:26 +0000