Mercurial > urweb

annotate lib/ur/basis.urs @ 1346:faad7d01b200

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Restore behavior of not complaining about undetermined unification variables when there are other errors
author Adam Chlipala <adam@chlipala.net>
date Thu, 16 Dec 2010 18:40:49 -0500
parents acabf3935060
children b106ca8200b1
rev   line source
adamc@56 1 type int
adamc@56 2 type float
adamc@56 3 type string
adamc@821 4 type char
adamc@436 5 type time
adamc@737 6 type blob
adamc@91 7
adamc@119 8 type unit = {}
adamc@119 9
adamc@186 10 datatype bool = False | True
adamc@186 11
adamc@288 12 datatype option t = None | Some of t
adamc@284 13
adamc@757 14 datatype list t = Nil | Cons of t * list t
adamc@757 15
adamc@91 16
adam@1287 17 (** Polymorphic variants *)
adam@1287 18
adam@1287 19 con variant :: {Type} -> Type
adam@1287 20 val make : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => t -> variant ([nm = t] ++ ts)
adam@1287 21 val match : ts ::: {Type} -> t ::: Type -> variant ts -> $(map (fn t' => t' -> t) ts) -> t
adam@1287 22
adam@1287 23
adamc@256 24 (** Basic type classes *)
adamc@256 25
adamc@256 26 class eq
adamc@256 27 val eq : t ::: Type -> eq t -> t -> t -> bool
adamc@257 28 val ne : t ::: Type -> eq t -> t -> t -> bool
adamc@256 29 val eq_int : eq int
adamc@394 30 val eq_float : eq float
adamc@256 31 val eq_string : eq string
adamc@821 32 val eq_char : eq char
adamc@256 33 val eq_bool : eq bool
adamc@437 34 val eq_time : eq time
adamc@422 35 val mkEq : t ::: Type -> (t -> t -> bool) -> eq t
adamc@256 36
adamc@389 37 class num
adamc@417 38 val zero : t ::: Type -> num t -> t
adamc@389 39 val neg : t ::: Type -> num t -> t -> t
adamc@389 40 val plus : t ::: Type -> num t -> t -> t -> t
adamc@389 41 val minus : t ::: Type -> num t -> t -> t -> t
adamc@389 42 val times : t ::: Type -> num t -> t -> t -> t
adamc@775 43 val divide : t ::: Type -> num t -> t -> t -> t
adamc@389 44 val mod : t ::: Type -> num t -> t -> t -> t
adamc@389 45 val num_int : num int
adamc@390 46 val num_float : num float
adamc@389 47
adamc@391 48 class ord
adamc@391 49 val lt : t ::: Type -> ord t -> t -> t -> bool
adamc@391 50 val le : t ::: Type -> ord t -> t -> t -> bool
adamc@391 51 val gt : t ::: Type -> ord t -> t -> t -> bool
adamc@391 52 val ge : t ::: Type -> ord t -> t -> t -> bool
adamc@391 53 val ord_int : ord int
adamc@394 54 val ord_float : ord float
adamc@394 55 val ord_string : ord string
adamc@821 56 val ord_char : ord char
adamc@394 57 val ord_bool : ord bool
adamc@437 58 val ord_time : ord time
adamc@961 59 val mkOrd : t ::: Type -> {Lt : t -> t -> bool, Le : t -> t -> bool} -> ord t
adamc@391 60
adamc@256 61
adamc@1061 62 (** Character operations *)
adamc@1061 63
adamc@1061 64 val isalnum : char -> bool
adamc@1061 65 val isalpha : char -> bool
adamc@1061 66 val isblank : char -> bool
adamc@1061 67 val iscntrl : char -> bool
adamc@1061 68 val isdigit : char -> bool
adamc@1061 69 val isgraph : char -> bool
adamc@1061 70 val islower : char -> bool
adamc@1061 71 val isprint : char -> bool
adamc@1061 72 val ispunct : char -> bool
adamc@1061 73 val isspace : char -> bool
adamc@1061 74 val isupper : char -> bool
adamc@1061 75 val isxdigit : char -> bool
adamc@1061 76 val tolower : char -> char
adamc@1061 77 val toupper : char -> char
adamc@1128 78 val ord : char -> int
adamc@1128 79 val chr : int -> char
adamc@1061 80
adamc@283 81 (** String operations *)
adamc@283 82
adamc@828 83 val strlen : string -> int
adamc@283 84 val strcat : string -> string -> string
adamc@821 85 val strsub : string -> int -> char
adamc@821 86 val strsuffix : string -> int -> string
adamc@829 87 val strchr : string -> char -> option string
adamc@829 88 val strindex : string -> char -> option int
adamc@1272 89 val strcspn : string -> string -> int
adamc@829 90 val substring : string -> int -> int -> string
adamc@1023 91 val str1 : char -> string
adamc@283 92
adamc@286 93 class show
adamc@286 94 val show : t ::: Type -> show t -> t -> string
adamc@286 95 val show_int : show int
adamc@286 96 val show_float : show float
adamc@286 97 val show_string : show string
adamc@821 98 val show_char : show char
adamc@286 99 val show_bool : show bool
adamc@436 100 val show_time : show time
adamc@452 101 val mkShow : t ::: Type -> (t -> string) -> show t
adamc@286 102
adamc@290 103 class read
adamc@290 104 val read : t ::: Type -> read t -> string -> option t
adamc@292 105 val readError : t ::: Type -> read t -> string -> t
adamc@292 106 (* [readError] calls [error] if the input is malformed. *)
adamc@290 107 val read_int : read int
adamc@290 108 val read_float : read float
adamc@290 109 val read_string : read string
adamc@821 110 val read_char : read char
adamc@290 111 val read_bool : read bool
adamc@436 112 val read_time : read time
adamc@777 113 val mkRead : t ::: Type -> (string -> t) -> (string -> option t) -> read t
adamc@288 114
adamc@283 115
adamc@564 116 (** * Monads *)
adamc@564 117
adamc@711 118 class monad :: (Type -> Type) -> Type
adamc@564 119 val return : m ::: (Type -> Type) -> t ::: Type
adamc@564 120 -> monad m
adamc@564 121 -> t -> m t
adamc@564 122 val bind : m ::: (Type -> Type) -> t1 ::: Type -> t2 ::: Type
adamc@564 123 -> monad m
adamc@564 124 -> m t1 -> (t1 -> m t2)
adamc@564 125 -> m t2
adamc@564 126
adamc@456 127 con transaction :: Type -> Type
adamc@564 128 val transaction_monad : monad transaction
adamc@456 129
adamc@565 130 con source :: Type -> Type
adamc@565 131 val source : t ::: Type -> t -> transaction (source t)
adamc@575 132 val set : t ::: Type -> source t -> t -> transaction unit
adamc@601 133 val get : t ::: Type -> source t -> transaction t
adamc@565 134
adamc@565 135 con signal :: Type -> Type
adamc@565 136 val signal_monad : monad signal
adamc@565 137 val signal : t ::: Type -> source t -> signal t
adamc@841 138 val current : t ::: Type -> signal t -> transaction t
adamc@456 139
adamc@456 140
adamc@1006 141 (** * Time *)
adamc@1006 142
adamc@1006 143 val now : transaction time
adamc@1050 144 val minTime : time
adamc@1138 145 val minusSeconds : time -> int -> time
adamc@1006 146
adamc@1006 147
adamc@456 148 (** HTTP operations *)
adamc@456 149
adamc@459 150 con http_cookie :: Type -> Type
adamc@459 151 val getCookie : t ::: Type -> http_cookie t -> transaction (option t)
adamc@1050 152 val setCookie : t ::: Type -> http_cookie t -> {Value : t,
adamc@1050 153 Expires : option time,
adamc@1050 154 Secure : bool} -> transaction unit
adamc@1050 155 val clearCookie : t ::: Type -> http_cookie t -> transaction unit
adamc@459 156
adamc@456 157
adamc@566 158 (** JavaScript-y gadgets *)
adamc@566 159
adamc@566 160 val alert : string -> transaction unit
adam@1290 161 val confirm : string -> transaction bool
adamc@694 162 val spawn : transaction unit -> transaction unit
adamc@695 163 val sleep : int -> transaction unit
adamc@566 164
adamc@908 165 val rpc : t ::: Type -> transaction t -> transaction t
adamc@908 166
adamc@566 167
adamc@678 168 (** Channels *)
adamc@678 169
adamc@678 170 con channel :: Type -> Type
adamc@678 171 val channel : t ::: Type -> transaction (channel t)
adamc@678 172 val send : t ::: Type -> channel t -> t -> transaction unit
adamc@678 173 val recv : t ::: Type -> channel t -> transaction t
adamc@678 174
adamc@682 175 type client
adamc@682 176 val self : transaction client
adamc@682 177
adamc@678 178
adamc@203 179 (** SQL *)
adamc@203 180
adamc@705 181 con sql_table :: {Type} -> {{Unit}} -> Type
adamc@753 182 con sql_view :: {Type} -> Type
adamc@753 183
adamc@753 184 class fieldsOf :: Type -> {Type} -> Type
adamc@753 185 val fieldsOf_table : fs ::: {Type} -> keys ::: {{Unit}}
adamc@753 186 -> fieldsOf (sql_table fs keys) fs
adamc@753 187 val fieldsOf_view : fs ::: {Type}
adamc@753 188 -> fieldsOf (sql_view fs) fs
adamc@203 189
adamc@704 190 (*** Constraints *)
adamc@704 191
adamc@707 192 (**** Primary keys *)
adamc@707 193
adamc@707 194 class sql_injectable_prim
adamc@707 195 val sql_bool : sql_injectable_prim bool
adamc@707 196 val sql_int : sql_injectable_prim int
adamc@707 197 val sql_float : sql_injectable_prim float
adamc@707 198 val sql_string : sql_injectable_prim string
adamc@1011 199 val sql_char : sql_injectable_prim char
adamc@707 200 val sql_time : sql_injectable_prim time
adamc@737 201 val sql_blob : sql_injectable_prim blob
adamc@707 202 val sql_channel : t ::: Type -> sql_injectable_prim (channel t)
adamc@707 203 val sql_client : sql_injectable_prim client
adamc@707 204
adamc@1104 205 con serialized :: Type -> Type
adamc@1104 206 val serialize : t ::: Type -> t -> serialized t
adamc@1104 207 val deserialize : t ::: Type -> serialized t -> t
adamc@1104 208 val sql_serialized : t ::: Type -> sql_injectable_prim (serialized t)
adamc@1104 209
adamc@707 210 con primary_key :: {Type} -> {{Unit}} -> Type
adamc@707 211 val no_primary_key : fs ::: {Type} -> primary_key fs []
adamc@707 212 val primary_key : rest ::: {Type} -> t ::: Type -> key1 :: Name -> keys :: {Type}
adamc@707 213 -> [[key1] ~ keys] => [[key1 = t] ++ keys ~ rest]
adamc@707 214 => $([key1 = sql_injectable_prim t] ++ map sql_injectable_prim keys)
adamc@707 215 -> primary_key ([key1 = t] ++ keys ++ rest)
adamc@707 216 [Pkey = [key1] ++ map (fn _ => ()) keys]
adamc@707 217
adamc@707 218 (**** Other constraints *)
adamc@707 219
adamc@705 220 con sql_constraints :: {Type} -> {{Unit}} -> Type
adamc@705 221 (* Arguments: column types, uniqueness implications of constraints *)
adamc@704 222
adamc@705 223 con sql_constraint :: {Type} -> {Unit} -> Type
adamc@704 224
adamc@705 225 val no_constraint : fs ::: {Type} -> sql_constraints fs []
adamc@705 226 val one_constraint : fs ::: {Type} -> unique ::: {Unit} -> name :: Name
adamc@705 227 -> sql_constraint fs unique
adamc@705 228 -> sql_constraints fs [name = unique]
adamc@705 229 val join_constraints : fs ::: {Type}
adamc@705 230 -> uniques1 ::: {{Unit}} -> uniques2 ::: {{Unit}} -> [uniques1 ~ uniques2]
adamc@705 231 => sql_constraints fs uniques1 -> sql_constraints fs uniques2
adamc@705 232 -> sql_constraints fs (uniques1 ++ uniques2)
adamc@705 233
adamc@709 234
adamc@705 235 val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type}
adamc@705 236 -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest]
adamc@705 237 => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique)
adamc@704 238
adamc@712 239 class linkable :: Type -> Type -> Type
adamc@712 240 val linkable_same : t ::: Type -> linkable t t
adamc@712 241 val linkable_from_nullable : t ::: Type -> linkable (option t) t
adamc@712 242 val linkable_to_nullable : t ::: Type -> linkable t (option t)
adamc@712 243
adamc@709 244 con matching :: {Type} -> {Type} -> Type
adamc@709 245 val mat_nil : matching [] []
adamc@712 246 val mat_cons : t1 ::: Type -> rest1 ::: {Type} -> t2 ::: Type -> rest2 ::: {Type}
adamc@709 247 -> nm1 :: Name -> nm2 :: Name
adamc@709 248 -> [[nm1] ~ rest1] => [[nm2] ~ rest2]
adamc@712 249 => linkable t1 t2
adamc@712 250 -> matching rest1 rest2
adamc@712 251 -> matching ([nm1 = t1] ++ rest1) ([nm2 = t2] ++ rest2)
adamc@709 252
adamc@709 253 con propagation_mode :: {Type} -> Type
adamc@709 254 val restrict : fs ::: {Type} -> propagation_mode fs
adamc@709 255 val cascade : fs ::: {Type} -> propagation_mode fs
adamc@709 256 val no_action : fs ::: {Type} -> propagation_mode fs
adamc@709 257 val set_null : fs ::: {Type} -> propagation_mode (map option fs)
adamc@709 258
adamc@709 259
adamc@709 260 val foreign_key : mine1 ::: Name -> t ::: Type -> mine ::: {Type} -> munused ::: {Type}
adamc@709 261 -> foreign ::: {Type} -> funused ::: {Type}
adamc@709 262 -> nm ::: Name -> uniques ::: {{Unit}}
adamc@709 263 -> [[mine1] ~ mine] => [[mine1 = t] ++ mine ~ munused]
adamc@709 264 => [foreign ~ funused] => [[nm] ~ uniques]
adamc@709 265 => matching ([mine1 = t] ++ mine) foreign
adamc@709 266 -> sql_table (foreign ++ funused) ([nm = map (fn _ => ()) foreign] ++ uniques)
adamc@709 267 -> {OnDelete : propagation_mode ([mine1 = t] ++ mine),
adamc@709 268 OnUpdate : propagation_mode ([mine1 = t] ++ mine)}
adamc@709 269 -> sql_constraint ([mine1 = t] ++ mine ++ munused) []
adamc@709 270
adamc@714 271 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
adamc@1072 272 val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
adamc@1072 273 -> fs' ::: {{Type}} -> agg' ::: {{Type}} -> exps' ::: {Type}
adamc@1072 274 -> [fs ~ fs'] => [agg ~ agg'] => [exps ~ exps'] =>
adamc@1072 275 sql_exp fs agg exps t
adamc@1072 276 -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') t
adamc@714 277
adamc@714 278 val check : fs ::: {Type}
adamc@714 279 -> sql_exp [] [] fs bool
adamc@714 280 -> sql_constraint fs []
adamc@714 281
adamc@714 282
adamc@204 283 (*** Queries *)
adamc@204 284
adamc@1191 285 con sql_query :: {{Type}} -> {{Type}} -> {Type} -> Type
adamc@1191 286 con sql_query1 :: {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
adamc@204 287
adamc@223 288 con sql_subset :: {{Type}} -> {{Type}} -> Type
adamc@223 289 val sql_subset : keep_drop :: {({Type} * {Type})}
adamc@354 290 -> sql_subset
adamc@621 291 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop)
adamc@621 292 (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop)
adamc@354 293 val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables
adamc@1072 294 val sql_subset_concat : big1 ::: {{Type}} -> little1 ::: {{Type}}
adamc@1072 295 -> big2 ::: {{Type}} -> little2 ::: {{Type}}
adamc@1072 296 -> [big1 ~ big2] => [little1 ~ little2] =>
adamc@1072 297 sql_subset big1 little1
adamc@1072 298 -> sql_subset big2 little2
adamc@1072 299 -> sql_subset (big1 ++ big2) (little1 ++ little2)
adamc@223 300
adamc@1191 301 con sql_from_items :: {{Type}} -> {{Type}} -> Type
adamc@748 302
adamc@1195 303 val sql_from_nil : free ::: {{Type}} -> sql_from_items free []
adamc@1191 304 val sql_from_table : free ::: {{Type}} -> t ::: Type -> fs ::: {Type}
adamc@753 305 -> fieldsOf t fs -> name :: Name
adamc@1191 306 -> t -> sql_from_items free [name = fs]
adamc@1192 307 val sql_from_query : free ::: {{Type}} -> fs ::: {Type} -> name :: Name
adamc@1192 308 -> sql_query free [] fs
adamc@1192 309 -> sql_from_items free [name = fs]
adamc@1191 310 val sql_from_comma : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
adamc@748 311 -> [tabs1 ~ tabs2]
adamc@1191 312 => sql_from_items free tabs1 -> sql_from_items free tabs2
adamc@1191 313 -> sql_from_items free (tabs1 ++ tabs2)
adamc@1191 314 val sql_inner_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
adamc@1191 315 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
adamc@1191 316 => sql_from_items free tabs1 -> sql_from_items free tabs2
adamc@1191 317 -> sql_exp (free ++ tabs1 ++ tabs2) [] [] bool
adamc@1191 318 -> sql_from_items free (tabs1 ++ tabs2)
adamc@748 319
adamc@750 320 class nullify :: Type -> Type -> Type
adamc@750 321 val nullify_option : t ::: Type -> nullify (option t) (option t)
adamc@750 322 val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t)
adamc@750 323
adamc@1191 324 val sql_left_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}}
adamc@1191 325 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
adamc@750 326 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2)
adamc@1191 327 -> sql_from_items free tabs1 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
adamc@1191 328 -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool
adamc@1191 329 -> sql_from_items free (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
adamc@750 330
adamc@1191 331 val sql_right_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}}
adamc@1191 332 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
adamc@751 333 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1)
adamc@1191 334 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items free tabs2
adamc@1191 335 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool
adamc@1191 336 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
adamc@751 337
adamc@1191 338 val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
adamc@1191 339 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
adamc@751 340 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2))
adamc@1191 341 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1)
adamc@1191 342 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
adamc@1191 343 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool
adamc@1191 344 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
adamc@751 345
adamc@1191 346 val sql_query1 : free ::: {{Type}}
adamc@1191 347 -> tables ::: {{Type}}
adamc@354 348 -> grouped ::: {{Type}}
adamc@354 349 -> selectedFields ::: {{Type}}
adamc@354 350 -> selectedExps ::: {Type}
adamc@1070 351 -> empties :: {Unit}
adamc@1191 352 -> [free ~ tables]
adamc@1191 353 => [free ~ grouped]
adamc@1191 354 => [empties ~ selectedFields]
adamc@1070 355 => {Distinct : bool,
adamc@1191 356 From : sql_from_items free tables,
adamc@1191 357 Where : sql_exp (free ++ tables) [] [] bool,
adamc@748 358 GroupBy : sql_subset tables grouped,
adamc@1191 359 Having : sql_exp (free ++ grouped) tables [] bool,
adamc@1070 360 SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields),
adamc@1191 361 SelectExps : $(map (sql_exp (free ++ grouped) tables [])
adamc@705 362 selectedExps) }
adamc@1191 363 -> sql_query1 free tables selectedFields selectedExps
adamc@229 364
adamc@229 365 type sql_relop
adamc@229 366 val sql_union : sql_relop
adamc@229 367 val sql_intersect : sql_relop
adamc@229 368 val sql_except : sql_relop
adamc@1191 369 val sql_relop : free ::: {{Type}}
adamc@1191 370 -> tables1 ::: {{Type}}
adamc@354 371 -> tables2 ::: {{Type}}
adamc@354 372 -> selectedFields ::: {{Type}}
adamc@354 373 -> selectedExps ::: {Type}
adamc@354 374 -> sql_relop
adamc@1191 375 -> sql_query1 free tables1 selectedFields selectedExps
adamc@1191 376 -> sql_query1 free tables2 selectedFields selectedExps
adamc@1191 377 -> sql_query1 free [] selectedFields selectedExps
adamc@1191 378 val sql_forget_tables : free ::: {{Type}} -> tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type}
adamc@1191 379 -> sql_query1 free tables selectedFields selectedExps
adamc@1191 380 -> sql_query1 free [] selectedFields selectedExps
adamc@229 381
adamc@230 382 type sql_direction
adamc@230 383 val sql_asc : sql_direction
adamc@230 384 val sql_desc : sql_direction
adamc@230 385
adamc@234 386 con sql_order_by :: {{Type}} -> {Type} -> Type
adamc@234 387 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
adamc@234 388 val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
adamc@354 389 -> sql_exp tables [] exps t -> sql_direction
adamc@354 390 -> sql_order_by tables exps
adamc@354 391 -> sql_order_by tables exps
adamc@230 392
adamc@231 393 type sql_limit
adamc@231 394 val sql_no_limit : sql_limit
adamc@231 395 val sql_limit : int -> sql_limit
adamc@354 396
adamc@232 397 type sql_offset
adamc@232 398 val sql_no_offset : sql_offset
adamc@232 399 val sql_offset : int -> sql_offset
adamc@232 400
adamc@1191 401 val sql_query : free ::: {{Type}}
adamc@1191 402 -> tables ::: {{Type}}
adamc@354 403 -> selectedFields ::: {{Type}}
adamc@354 404 -> selectedExps ::: {Type}
adamc@1191 405 -> [free ~ tables]
adamc@1191 406 => {Rows : sql_query1 free tables selectedFields selectedExps,
adamc@1191 407 OrderBy : sql_order_by (free ++ tables) selectedExps,
adamc@354 408 Limit : sql_limit,
adamc@354 409 Offset : sql_offset}
adamc@1191 410 -> sql_query free selectedFields selectedExps
adamc@204 411
adamc@354 412 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
adamc@354 413 -> fieldType ::: Type -> agg ::: {{Type}}
adamc@354 414 -> exps ::: {Type}
adamc@354 415 -> tab :: Name -> field :: Name
adamc@354 416 -> sql_exp
adamc@354 417 ([tab = [field = fieldType] ++ otherFields] ++ otherTabs)
adamc@354 418 agg exps fieldType
adamc@234 419
adamc@354 420 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type}
adamc@354 421 -> nm :: Name
adamc@354 422 -> sql_exp tabs agg ([nm = t] ++ rest) t
adamc@209 423
adamc@221 424 class sql_injectable
adamc@676 425 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t
adamc@676 426 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)
adamc@676 427
adamc@354 428 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 429 -> t ::: Type
adamc@354 430 -> sql_injectable t -> t -> sql_exp tables agg exps t
adamc@209 431
adamc@470 432 val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 433 -> t ::: Type
adamc@470 434 -> sql_exp tables agg exps (option t)
adamc@470 435 -> sql_exp tables agg exps bool
adamc@470 436
adamc@559 437 class sql_arith
adamc@559 438 val sql_int_arith : sql_arith int
adamc@559 439 val sql_float_arith : sql_arith float
adamc@559 440
adamc@220 441 con sql_unary :: Type -> Type -> Type
adamc@220 442 val sql_not : sql_unary bool bool
adamc@354 443 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 444 -> arg ::: Type -> res ::: Type
adamc@354 445 -> sql_unary arg res -> sql_exp tables agg exps arg
adamc@354 446 -> sql_exp tables agg exps res
adamc@220 447
adamc@559 448 val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t
adamc@559 449
adamc@220 450 con sql_binary :: Type -> Type -> Type -> Type
adamc@220 451 val sql_and : sql_binary bool bool bool
adamc@220 452 val sql_or : sql_binary bool bool bool
adamc@234 453 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 454 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
adamc@354 455 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1
adamc@354 456 -> sql_exp tables agg exps arg2
adamc@354 457 -> sql_exp tables agg exps res
adamc@220 458
adamc@559 459 val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 460 val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 461 val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 462 val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 463 val sql_mod : sql_binary int int int
adamc@559 464
adamc@559 465 val sql_eq : t ::: Type -> sql_binary t t bool
adamc@559 466 val sql_ne : t ::: Type -> sql_binary t t bool
adamc@559 467 val sql_lt : t ::: Type -> sql_binary t t bool
adamc@559 468 val sql_le : t ::: Type -> sql_binary t t bool
adamc@559 469 val sql_gt : t ::: Type -> sql_binary t t bool
adamc@559 470 val sql_ge : t ::: Type -> sql_binary t t bool
adamc@203 471
adamc@235 472 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@544 473 -> sql_exp tables agg exps int
adamc@235 474
adamc@1187 475 con sql_aggregate :: Type -> Type -> Type
adamc@354 476 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@1187 477 -> dom ::: Type -> ran ::: Type
adamc@1187 478 -> sql_aggregate dom ran -> sql_exp agg agg exps dom
adamc@1187 479 -> sql_exp tables agg exps ran
adamc@1187 480
adamc@1187 481 val sql_count_col : t ::: Type -> sql_aggregate (option t) int
adamc@236 482
adamc@236 483 class sql_summable
adamc@236 484 val sql_summable_int : sql_summable int
adamc@236 485 val sql_summable_float : sql_summable float
adamc@1187 486 val sql_avg : t ::: Type -> sql_summable t -> sql_aggregate t t
adamc@1187 487 val sql_sum : t ::: Type -> sql_summable t -> sql_aggregate t t
adamc@236 488
adamc@236 489 class sql_maxable
adamc@236 490 val sql_maxable_int : sql_maxable int
adamc@236 491 val sql_maxable_float : sql_maxable float
adamc@236 492 val sql_maxable_string : sql_maxable string
adamc@437 493 val sql_maxable_time : sql_maxable time
adamc@1187 494 val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t t
adamc@1187 495 val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t t
adamc@236 496
adamc@441 497 con sql_nfunc :: Type -> Type
adamc@441 498 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@441 499 -> t ::: Type
adamc@441 500 -> sql_nfunc t -> sql_exp tables agg exps t
adamc@441 501 val sql_current_timestamp : sql_nfunc time
adamc@441 502
adamc@746 503 con sql_ufunc :: Type -> Type -> Type
adamc@746 504 val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@746 505 -> dom ::: Type -> ran ::: Type
adamc@746 506 -> sql_ufunc dom ran -> sql_exp tables agg exps dom
adamc@746 507 -> sql_exp tables agg exps ran
adamc@746 508 val sql_octet_length : sql_ufunc blob int
adamc@1207 509 val sql_known : t ::: Type -> sql_ufunc t bool
adamc@746 510
adamc@235 511
adamc@1081 512 val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
adamc@1081 513 -> sql_injectable_prim t
adamc@1081 514 -> sql_exp tables agg exps t
adamc@1081 515 -> sql_exp tables agg exps (option t)
adamc@1081 516
adamc@1191 517 val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type
adamc@1191 518 -> sql_query tables [] [nm = t]
adamc@1191 519 -> sql_exp tables agg exps t
adamc@1191 520
adamc@243 521 (*** Executing queries *)
adamc@243 522
adamc@354 523 val query : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 524 -> [tables ~ exps] =>
adamc@354 525 state ::: Type
adamc@1191 526 -> sql_query [] tables exps
adamc@621 527 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@354 528 -> state
adamc@354 529 -> transaction state)
adamc@354 530 -> state
adamc@354 531 -> transaction state
adamc@243 532
adamc@243 533
adamc@299 534 (*** Database mutators *)
adamc@299 535
adamc@299 536 type dml
adamc@299 537 val dml : dml -> transaction unit
adam@1293 538 val tryDml : dml -> transaction (option string)
adam@1293 539 (* Returns an error message on failure. *)
adamc@299 540
adamc@705 541 val insert : fields ::: {Type} -> uniques ::: {{Unit}}
adamc@705 542 -> sql_table fields uniques
adamc@621 543 -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
adamc@354 544 -> dml
adamc@299 545
adamc@705 546 val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} ->
adamc@629 547 [changed ~ unchanged] =>
adamc@621 548 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
adamc@705 549 -> sql_table (changed ++ unchanged) uniques
adamc@354 550 -> sql_exp [T = changed ++ unchanged] [] [] bool
adamc@354 551 -> dml
adamc@299 552
adamc@705 553 val delete : fields ::: {Type} -> uniques ::: {{Unit}}
adamc@705 554 -> sql_table fields uniques
adamc@354 555 -> sql_exp [T = fields] [] [] bool
adamc@354 556 -> dml
adamc@299 557
adamc@338 558 (*** Sequences *)
adamc@338 559
adamc@338 560 type sql_sequence
adamc@338 561 val nextval : sql_sequence -> transaction int
adamc@1073 562 val setval : sql_sequence -> int -> transaction unit
adamc@338 563
adamc@299 564
adamc@203 565 (** XML *)
adamc@203 566
adamc@721 567 type css_class
adam@1292 568 val classes : css_class -> css_class -> css_class
adam@1292 569 (* The equivalent of writing one class after the other, separated by a space, in
adam@1292 570 * an HTML 'class' attribute *)
adamc@718 571
adamc@720 572 con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
adamc@91 573
adamc@720 574 con xml :: {Unit} -> {Type} -> {Type} -> Type
adamc@720 575 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
adamc@354 576 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type}
adamc@354 577 -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
adamc@354 578 -> useOuter ::: {Type} -> useInner ::: {Type}
adamc@354 579 -> bindOuter ::: {Type} -> bindInner ::: {Type}
adamc@629 580 -> [attrsGiven ~ attrsAbsent] =>
adamc@629 581 [useOuter ~ useInner] =>
adamc@629 582 [bindOuter ~ bindInner] =>
adamc@721 583 option css_class
adamc@721 584 -> $attrsGiven
adamc@629 585 -> tag (attrsGiven ++ attrsAbsent)
adamc@720 586 ctxOuter ctxInner useOuter bindOuter
adamc@720 587 -> xml ctxInner useInner bindInner
adamc@720 588 -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
adamc@140 589 val join : ctx ::: {Unit}
adamc@720 590 -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
adamc@720 591 -> [use1 ~ bind1] => [bind1 ~ bind2] =>
adamc@720 592 xml ctx use1 bind1
adamc@720 593 -> xml ctx (use1 ++ bind1) bind2
adamc@720 594 -> xml ctx use1 (bind1 ++ bind2)
adamc@354 595 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type}
adamc@720 596 -> bind ::: {Type}
adamc@629 597 -> [use1 ~ use2] =>
adamc@720 598 xml ctx use1 bind
adamc@720 599 -> xml ctx (use1 ++ use2) bind
adamc@91 600
adamc@110 601 con xhtml = xml [Html]
adamc@139 602 con page = xhtml [] []
adamc@720 603 con xbody = xml [Body] [] []
adamc@1277 604 con xtable = xml [Body, Table] [] []
adamc@720 605 con xtr = xml [Body, Tr] [] []
adamc@720 606 con xform = xml [Body, Form] [] []
adamc@110 607
adamc@718 608
adamc@204 609 (*** HTML details *)
adamc@204 610
adamc@140 611 con html = [Html]
adamc@140 612 con head = [Head]
adamc@140 613 con body = [Body]
adamc@361 614 con form = [Body, Form]
adamc@760 615 con subform = [Body, Subform]
adamc@332 616 con tabl = [Body, Table]
adamc@332 617 con tr = [Body, Tr]
adamc@93 618
adamc@724 619 type url
adamc@1065 620 val show_url : show url
adamc@724 621 val bless : string -> url
adamc@770 622 val checkUrl : string -> option url
adamc@1085 623 val currentUrl : transaction url
adamc@1065 624 val url : transaction page -> url
adamc@1065 625 val redirect : t ::: Type -> url -> transaction t
adamc@724 626
adamc@847 627 val dyn : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> [ctx ~ body] => unit
adamc@847 628 -> tag [Signal = signal (xml (body ++ ctx) use bind)] (body ++ ctx) [] use bind
adamc@568 629
adamc@720 630 val head : unit -> tag [] html head [] []
adamc@720 631 val title : unit -> tag [] head [] [] []
adamc@1047 632 val link : unit -> tag [Id = string, Rel = string, Typ = string, Href = url, Media = string] head [] [] []
adamc@110 633
adamc@892 634 val body : unit -> tag [Onload = transaction unit, Onresize = transaction unit, Onunload = transaction unit]
adamc@892 635 html body [] []
adamc@354 636 con bodyTag = fn (attrs :: {Type}) =>
adamc@354 637 ctx ::: {Unit} ->
adamc@629 638 [[Body] ~ ctx] =>
adamc@720 639 unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
adamc@354 640 con bodyTagStandalone = fn (attrs :: {Type}) =>
adamc@354 641 ctx ::: {Unit}
adamc@629 642 -> [[Body] ~ ctx] =>
adamc@720 643 unit -> tag attrs ([Body] ++ ctx) [] [] []
adamc@141 644
adamc@1047 645 val br : bodyTagStandalone [Id = int]
adamc@119 646
adamc@892 647 con focusEvents = [Onblur = transaction unit, Onfocus = transaction unit]
adamc@892 648 con mouseEvents = [Onclick = transaction unit, Ondblclick = transaction unit,
adamc@892 649 Onmousedown = transaction unit, Onmousemove = transaction unit,
adamc@892 650 Onmouseout = transaction unit, Onmouseover = transaction unit,
adamc@894 651 Onmouseup = transaction unit]
adamc@895 652 con keyEvents = [Onkeydown = int -> transaction unit, Onkeypress = int -> transaction unit,
adamc@895 653 Onkeyup = int -> transaction unit]
adamc@895 654 (* Key arguments are character codes. *)
adamc@892 655 con resizeEvents = [Onresize = transaction unit]
adamc@691 656
adamc@892 657 con boxEvents = focusEvents ++ mouseEvents ++ keyEvents ++ resizeEvents
adamc@892 658 con tableEvents = focusEvents ++ mouseEvents ++ keyEvents
adamc@140 659
adam@1291 660 con boxAttrs = [Id = string, Title = string] ++ boxEvents
adam@1291 661 con tableAttrs = [Id = string, Title = string] ++ tableEvents
adamc@469 662
adamc@1047 663 val span : bodyTag boxAttrs
adamc@1047 664 val div : bodyTag boxAttrs
adamc@140 665
adamc@1047 666 val p : bodyTag boxAttrs
adamc@1047 667 val b : bodyTag boxAttrs
adamc@1047 668 val i : bodyTag boxAttrs
adamc@1047 669 val tt : bodyTag boxAttrs
adamc@410 670
adamc@1047 671 val h1 : bodyTag boxAttrs
adamc@1047 672 val h2 : bodyTag boxAttrs
adamc@1047 673 val h3 : bodyTag boxAttrs
adamc@1047 674 val h4 : bodyTag boxAttrs
adamc@1047 675 val h5 : bodyTag boxAttrs
adamc@1047 676 val h6 : bodyTag boxAttrs
adamc@717 677
adamc@1047 678 val li : bodyTag boxAttrs
adamc@1047 679 val ol : bodyTag boxAttrs
adamc@1047 680 val ul : bodyTag boxAttrs
adamc@140 681
adamc@1047 682 val hr : bodyTag boxAttrs
adamc@1047 683
adamc@1047 684 val a : bodyTag ([Link = transaction page, Href = url] ++ boxAttrs)
adamc@892 685
adamc@1129 686 val img : bodyTag ([Src = url, Width = int, Height = int,
adamc@1129 687 Onabort = transaction unit, Onerror = transaction unit,
adamc@1047 688 Onload = transaction unit] ++ boxAttrs)
adamc@892 689
adamc@720 690 val form : ctx ::: {Unit} -> bind ::: {Type}
adamc@1120 691 -> [[Body, Form, Table] ~ ctx] =>
adamc@1004 692 xml ([Body, Form] ++ ctx) [] bind
adamc@756 693 -> xml ([Body] ++ ctx) [] []
adamc@756 694
adamc@756 695 val subform : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
adamc@756 696 -> [[Form] ~ ctx] =>
adamc@756 697 nm :: Name -> [[nm] ~ use] =>
adamc@1004 698 xml ([Form] ++ ctx) [] bind
adamc@756 699 -> xml ([Form] ++ ctx) use [nm = $bind]
adamc@758 700
adamc@758 701 val subforms : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
adamc@1004 702 -> [[Form, Subform] ~ ctx] =>
adamc@758 703 nm :: Name -> [[nm] ~ use] =>
adamc@1004 704 xml ([Subform] ++ ctx) [Entry = $bind] []
adamc@758 705 -> xml ([Form] ++ ctx) use [nm = list ($bind)]
adamc@758 706
adamc@758 707 val entry : ctx ::: {Unit} -> bind ::: {Type}
adamc@1004 708 -> [[Subform, Form] ~ ctx] =>
adamc@1004 709 xml ([Form] ++ ctx) [] bind
adamc@758 710 -> xml ([Subform] ++ ctx) [Entry = $bind] []
adamc@758 711
adamc@361 712 con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) =>
adamc@354 713 ctx ::: {Unit}
adamc@629 714 -> [[Form] ~ ctx] =>
adamc@354 715 nm :: Name -> unit
adamc@720 716 -> tag attrs ([Form] ++ ctx) inner [] [nm = ty]
adamc@1047 717 val hidden : formTag string [] [Id = string, Value = string]
adamc@892 718 val textbox : formTag string [] ([Value = string, Size = int, Source = source string, Onchange = transaction unit,
adamc@1047 719 Ontext = transaction unit] ++ boxAttrs)
adamc@1047 720 val password : formTag string [] ([Value = string, Size = int] ++ boxAttrs)
adamc@892 721 val textarea : formTag string [] ([Rows = int, Cols = int, Onchange = transaction unit,
adamc@1047 722 Ontext = transaction unit] ++ boxAttrs)
adamc@153 723
adamc@1047 724 val checkbox : formTag bool [] ([Checked = bool] ++ boxAttrs)
adamc@190 725
adamc@737 726 type file
adamc@737 727 val fileName : file -> option string
adamc@740 728 val fileMimeType : file -> string
adamc@737 729 val fileData : file -> blob
adamc@737 730
adamc@1047 731 val upload : formTag file [] ([Value = string, Size = int] ++ boxAttrs)
adamc@737 732
adamc@741 733 type mimeType
adamc@741 734 val blessMime : string -> mimeType
adamc@770 735 val checkMime : string -> option mimeType
adamc@741 736 val returnBlob : t ::: Type -> blob -> mimeType -> transaction t
adamc@745 737 val blobSize : blob -> int
adamc@1119 738 val textBlob : string -> blob
adamc@741 739
adamc@153 740 con radio = [Body, Radio]
adamc@1047 741 val radio : formTag string radio [Id = string]
adamc@1068 742 val radioOption : unit -> tag ([Value = string, Checked = bool] ++ boxAttrs) radio [] [] []
adamc@142 743
adamc@154 744 con select = [Select]
adamc@1047 745 val select : formTag string select ([Onchange = transaction unit] ++ boxAttrs)
adamc@720 746 val option : unit -> tag [Value = string, Selected = bool] select [] [] []
adamc@154 747
adamc@720 748 val submit : ctx ::: {Unit} -> use ::: {Type}
adamc@629 749 -> [[Form] ~ ctx] =>
adamc@354 750 unit
adamc@1047 751 -> tag ([Value = string, Action = $use -> transaction page] ++ boxAttrs)
adamc@720 752 ([Form] ++ ctx) ([Form] ++ ctx) use []
adamc@283 753
adamc@1047 754 val label : bodyTag ([For = string, Accesskey = string] ++ tableAttrs)
adamc@1047 755
adamc@1047 756
adamc@601 757 (*** AJAX-oriented widgets *)
adamc@601 758
adamc@797 759 con cformTag = fn (attrs :: {Type}) (inner :: {Unit}) =>
adamc@601 760 ctx ::: {Unit}
adamc@629 761 -> [[Body] ~ ctx] =>
adamc@797 762 unit -> tag attrs ([Body] ++ ctx) inner [] []
adamc@601 763
adamc@892 764 val ctextbox : cformTag ([Value = string, Size = int, Source = source string, Onchange = transaction unit,
adamc@1047 765 Ontext = transaction unit] ++ boxAttrs) []
adamc@1047 766 val button : cformTag ([Value = string] ++ boxAttrs) []
adamc@797 767
adamc@1047 768 val ccheckbox : cformTag ([Value = bool, Size = int, Source = source bool] ++ boxAttrs) []
adamc@817 769
adamc@797 770 con cselect = [Cselect]
adamc@1047 771 val cselect : cformTag ([Source = source string, Onchange = transaction unit] ++ boxAttrs) cselect
adamc@797 772 val coption : unit -> tag [Value = string, Selected = bool] cselect [] [] []
adamc@601 773
adamc@1099 774 val ctextarea : cformTag ([Value = string, Rows = int, Cols = int, Source = source string, Onchange = transaction unit,
adamc@1099 775 Ontext = transaction unit] ++ boxAttrs) []
adamc@1099 776
adamc@720 777 (*** Tables *)
adamc@720 778
adamc@892 779 val tabl : other ::: {Unit} -> [other ~ [Body, Table]] => unit
adamc@1047 780 -> tag ([Border = int] ++ boxAttrs)
adamc@892 781 ([Body] ++ other) ([Body, Table] ++ other) [] []
adamc@892 782 val tr : other ::: {Unit} -> [other ~ [Body, Table, Tr]] => unit
adamc@1047 783 -> tag tableAttrs
adamc@892 784 ([Body, Table] ++ other) ([Body, Tr] ++ other) [] []
adamc@892 785 val th : other ::: {Unit} -> [other ~ [Body, Tr]] => unit
adamc@1047 786 -> tag ([Colspan = int] ++ tableAttrs)
adamc@892 787 ([Body, Tr] ++ other) ([Body] ++ other) [] []
adamc@892 788 val td : other ::: {Unit} -> [other ~ [Body, Tr]] => unit
adamc@1047 789 -> tag ([Colspan = int] ++ tableAttrs)
adamc@892 790 ([Body, Tr] ++ other) ([Body] ++ other) [] []
adamc@720 791
adamc@283 792
adamc@283 793 (** Aborting *)
adamc@283 794
adamc@726 795 val error : t ::: Type -> xbody -> t
adamc@720 796
adamc@729 797 (* Client-side-only handlers: *)
adamc@726 798 val onError : (xbody -> transaction unit) -> transaction unit
adamc@728 799 val onFail : (string -> transaction unit) -> transaction unit
adamc@729 800 val onConnectFail : transaction unit -> transaction unit
adamc@729 801 val onDisconnect : transaction unit -> transaction unit
adamc@729 802 val onServerError : (string -> transaction unit) -> transaction unit
adamc@727 803
adamc@727 804 val show_xml : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> show (xml ctx use bind)
adamc@1075 805
adamc@1075 806
adamc@1075 807 (** Tasks *)
adamc@1075 808
adamc@1075 809 type task_kind
adamc@1075 810 val initialize : task_kind
adamc@1120 811
adamc@1120 812
adamc@1199 813 (** Information flow security *)
adamc@1199 814
adamc@1199 815 type sql_policy
adamc@1199 816
adamc@1214 817 val sendClient : tables ::: {{Type}} -> exps ::: {Type}
adamc@1214 818 -> [tables ~ exps] => sql_query [] tables exps
adamc@1214 819 -> sql_policy
adamc@1199 820
adamc@1229 821 val sendOwnIds : sql_sequence -> sql_policy
adamc@1229 822
adamc@1220 823 val mayInsert : fs ::: {Type} -> tables ::: {{Type}} -> [[New] ~ tables]
adamc@1220 824 => sql_query [] ([New = fs] ++ tables) []
adamc@1220 825 -> sql_policy
adamc@1220 826
adamc@1221 827 val mayDelete : fs ::: {Type} -> tables ::: {{Type}} -> [[Old] ~ tables]
adamc@1221 828 => sql_query [] ([Old = fs] ++ tables) []
adamc@1221 829 -> sql_policy
adamc@1221 830
adamc@1223 831 val mayUpdate : fs ::: {Type} -> tables ::: {{Type}} -> [[Old, New] ~ tables]
adamc@1223 832 => sql_query [] ([Old = fs, New = fs] ++ tables) []
adamc@1223 833 -> sql_policy
adamc@1223 834
adamc@1240 835 val also : sql_policy -> sql_policy -> sql_policy
adamc@1199 836
adamc@1120 837 val debug : string -> transaction unit
adamc@1250 838
adamc@1250 839 val rand : transaction int