Mercurial > urweb

annotate lib/ur/basis.urs @ 853:19fdeef40ada

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Factor out common request functionality, in preparation for supporting different protocols
author Adam Chlipala <adamc@hcoop.net>
date Tue, 23 Jun 2009 14:05:12 -0400
parents 0f7e2cca6d9b
children e04af9641067
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
adamc@256 17 (** Basic type classes *)
adamc@256 18
adamc@256 19 class eq
adamc@256 20 val eq : t ::: Type -> eq t -> t -> t -> bool
adamc@257 21 val ne : t ::: Type -> eq t -> t -> t -> bool
adamc@256 22 val eq_int : eq int
adamc@394 23 val eq_float : eq float
adamc@256 24 val eq_string : eq string
adamc@821 25 val eq_char : eq char
adamc@256 26 val eq_bool : eq bool
adamc@437 27 val eq_time : eq time
adamc@422 28 val mkEq : t ::: Type -> (t -> t -> bool) -> eq t
adamc@256 29
adamc@389 30 class num
adamc@417 31 val zero : t ::: Type -> num t -> t
adamc@389 32 val neg : t ::: Type -> num t -> t -> t
adamc@389 33 val plus : t ::: Type -> num t -> t -> t -> t
adamc@389 34 val minus : t ::: Type -> num t -> t -> t -> t
adamc@389 35 val times : t ::: Type -> num t -> t -> t -> t
adamc@775 36 val divide : t ::: Type -> num t -> t -> t -> t
adamc@389 37 val mod : t ::: Type -> num t -> t -> t -> t
adamc@389 38 val num_int : num int
adamc@390 39 val num_float : num float
adamc@389 40
adamc@391 41 class ord
adamc@391 42 val lt : t ::: Type -> ord t -> t -> t -> bool
adamc@391 43 val le : t ::: Type -> ord t -> t -> t -> bool
adamc@391 44 val gt : t ::: Type -> ord t -> t -> t -> bool
adamc@391 45 val ge : t ::: Type -> ord t -> t -> t -> bool
adamc@391 46 val ord_int : ord int
adamc@394 47 val ord_float : ord float
adamc@394 48 val ord_string : ord string
adamc@821 49 val ord_char : ord char
adamc@394 50 val ord_bool : ord bool
adamc@437 51 val ord_time : ord time
adamc@391 52
adamc@256 53
adamc@283 54 (** String operations *)
adamc@283 55
adamc@828 56 val strlen : string -> int
adamc@283 57 val strcat : string -> string -> string
adamc@821 58 val strsub : string -> int -> char
adamc@821 59 val strsuffix : string -> int -> string
adamc@829 60 val strchr : string -> char -> option string
adamc@829 61 val strindex : string -> char -> option int
adamc@831 62 val strcspn : string -> string -> option int
adamc@829 63 val substring : string -> int -> int -> string
adamc@283 64
adamc@286 65 class show
adamc@286 66 val show : t ::: Type -> show t -> t -> string
adamc@286 67 val show_int : show int
adamc@286 68 val show_float : show float
adamc@286 69 val show_string : show string
adamc@821 70 val show_char : show char
adamc@286 71 val show_bool : show bool
adamc@436 72 val show_time : show time
adamc@452 73 val mkShow : t ::: Type -> (t -> string) -> show t
adamc@286 74
adamc@290 75 class read
adamc@290 76 val read : t ::: Type -> read t -> string -> option t
adamc@292 77 val readError : t ::: Type -> read t -> string -> t
adamc@292 78 (* [readError] calls [error] if the input is malformed. *)
adamc@290 79 val read_int : read int
adamc@290 80 val read_float : read float
adamc@290 81 val read_string : read string
adamc@821 82 val read_char : read char
adamc@290 83 val read_bool : read bool
adamc@436 84 val read_time : read time
adamc@777 85 val mkRead : t ::: Type -> (string -> t) -> (string -> option t) -> read t
adamc@288 86
adamc@283 87
adamc@564 88 (** * Monads *)
adamc@564 89
adamc@711 90 class monad :: (Type -> Type) -> Type
adamc@564 91 val return : m ::: (Type -> Type) -> t ::: Type
adamc@564 92 -> monad m
adamc@564 93 -> t -> m t
adamc@564 94 val bind : m ::: (Type -> Type) -> t1 ::: Type -> t2 ::: Type
adamc@564 95 -> monad m
adamc@564 96 -> m t1 -> (t1 -> m t2)
adamc@564 97 -> m t2
adamc@564 98
adamc@456 99 con transaction :: Type -> Type
adamc@564 100 val transaction_monad : monad transaction
adamc@456 101
adamc@565 102 con source :: Type -> Type
adamc@565 103 val source : t ::: Type -> t -> transaction (source t)
adamc@575 104 val set : t ::: Type -> source t -> t -> transaction unit
adamc@601 105 val get : t ::: Type -> source t -> transaction t
adamc@565 106
adamc@565 107 con signal :: Type -> Type
adamc@565 108 val signal_monad : monad signal
adamc@565 109 val signal : t ::: Type -> source t -> signal t
adamc@841 110 val current : t ::: Type -> signal t -> transaction t
adamc@456 111
adamc@456 112
adamc@456 113 (** HTTP operations *)
adamc@456 114
adamc@456 115 val requestHeader : string -> transaction (option string)
adamc@456 116
adamc@459 117 con http_cookie :: Type -> Type
adamc@459 118 val getCookie : t ::: Type -> http_cookie t -> transaction (option t)
adamc@459 119 val setCookie : t ::: Type -> http_cookie t -> t -> transaction unit
adamc@459 120
adamc@456 121
adamc@566 122 (** JavaScript-y gadgets *)
adamc@566 123
adamc@566 124 val alert : string -> transaction unit
adamc@694 125 val spawn : transaction unit -> transaction unit
adamc@695 126 val sleep : int -> transaction unit
adamc@566 127
adamc@566 128
adamc@678 129 (** Channels *)
adamc@678 130
adamc@678 131 con channel :: Type -> Type
adamc@678 132 val channel : t ::: Type -> transaction (channel t)
adamc@678 133 val send : t ::: Type -> channel t -> t -> transaction unit
adamc@678 134 val recv : t ::: Type -> channel t -> transaction t
adamc@678 135
adamc@682 136 type client
adamc@682 137 val self : transaction client
adamc@682 138
adamc@678 139
adamc@203 140 (** SQL *)
adamc@203 141
adamc@705 142 con sql_table :: {Type} -> {{Unit}} -> Type
adamc@753 143 con sql_view :: {Type} -> Type
adamc@753 144
adamc@753 145 class fieldsOf :: Type -> {Type} -> Type
adamc@753 146 val fieldsOf_table : fs ::: {Type} -> keys ::: {{Unit}}
adamc@753 147 -> fieldsOf (sql_table fs keys) fs
adamc@753 148 val fieldsOf_view : fs ::: {Type}
adamc@753 149 -> fieldsOf (sql_view fs) fs
adamc@203 150
adamc@704 151 (*** Constraints *)
adamc@704 152
adamc@707 153 (**** Primary keys *)
adamc@707 154
adamc@707 155 class sql_injectable_prim
adamc@707 156 val sql_bool : sql_injectable_prim bool
adamc@707 157 val sql_int : sql_injectable_prim int
adamc@707 158 val sql_float : sql_injectable_prim float
adamc@707 159 val sql_string : sql_injectable_prim string
adamc@707 160 val sql_time : sql_injectable_prim time
adamc@737 161 val sql_blob : sql_injectable_prim blob
adamc@707 162 val sql_channel : t ::: Type -> sql_injectable_prim (channel t)
adamc@707 163 val sql_client : sql_injectable_prim client
adamc@707 164
adamc@707 165 con primary_key :: {Type} -> {{Unit}} -> Type
adamc@707 166 val no_primary_key : fs ::: {Type} -> primary_key fs []
adamc@707 167 val primary_key : rest ::: {Type} -> t ::: Type -> key1 :: Name -> keys :: {Type}
adamc@707 168 -> [[key1] ~ keys] => [[key1 = t] ++ keys ~ rest]
adamc@707 169 => $([key1 = sql_injectable_prim t] ++ map sql_injectable_prim keys)
adamc@707 170 -> primary_key ([key1 = t] ++ keys ++ rest)
adamc@707 171 [Pkey = [key1] ++ map (fn _ => ()) keys]
adamc@707 172
adamc@707 173 (**** Other constraints *)
adamc@707 174
adamc@705 175 con sql_constraints :: {Type} -> {{Unit}} -> Type
adamc@705 176 (* Arguments: column types, uniqueness implications of constraints *)
adamc@704 177
adamc@705 178 con sql_constraint :: {Type} -> {Unit} -> Type
adamc@704 179
adamc@705 180 val no_constraint : fs ::: {Type} -> sql_constraints fs []
adamc@705 181 val one_constraint : fs ::: {Type} -> unique ::: {Unit} -> name :: Name
adamc@705 182 -> sql_constraint fs unique
adamc@705 183 -> sql_constraints fs [name = unique]
adamc@705 184 val join_constraints : fs ::: {Type}
adamc@705 185 -> uniques1 ::: {{Unit}} -> uniques2 ::: {{Unit}} -> [uniques1 ~ uniques2]
adamc@705 186 => sql_constraints fs uniques1 -> sql_constraints fs uniques2
adamc@705 187 -> sql_constraints fs (uniques1 ++ uniques2)
adamc@705 188
adamc@709 189
adamc@705 190 val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type}
adamc@705 191 -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest]
adamc@705 192 => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique)
adamc@704 193
adamc@712 194 class linkable :: Type -> Type -> Type
adamc@712 195 val linkable_same : t ::: Type -> linkable t t
adamc@712 196 val linkable_from_nullable : t ::: Type -> linkable (option t) t
adamc@712 197 val linkable_to_nullable : t ::: Type -> linkable t (option t)
adamc@712 198
adamc@709 199 con matching :: {Type} -> {Type} -> Type
adamc@709 200 val mat_nil : matching [] []
adamc@712 201 val mat_cons : t1 ::: Type -> rest1 ::: {Type} -> t2 ::: Type -> rest2 ::: {Type}
adamc@709 202 -> nm1 :: Name -> nm2 :: Name
adamc@709 203 -> [[nm1] ~ rest1] => [[nm2] ~ rest2]
adamc@712 204 => linkable t1 t2
adamc@712 205 -> matching rest1 rest2
adamc@712 206 -> matching ([nm1 = t1] ++ rest1) ([nm2 = t2] ++ rest2)
adamc@709 207
adamc@709 208 con propagation_mode :: {Type} -> Type
adamc@709 209 val restrict : fs ::: {Type} -> propagation_mode fs
adamc@709 210 val cascade : fs ::: {Type} -> propagation_mode fs
adamc@709 211 val no_action : fs ::: {Type} -> propagation_mode fs
adamc@709 212 val set_null : fs ::: {Type} -> propagation_mode (map option fs)
adamc@709 213
adamc@709 214
adamc@709 215 val foreign_key : mine1 ::: Name -> t ::: Type -> mine ::: {Type} -> munused ::: {Type}
adamc@709 216 -> foreign ::: {Type} -> funused ::: {Type}
adamc@709 217 -> nm ::: Name -> uniques ::: {{Unit}}
adamc@709 218 -> [[mine1] ~ mine] => [[mine1 = t] ++ mine ~ munused]
adamc@709 219 => [foreign ~ funused] => [[nm] ~ uniques]
adamc@709 220 => matching ([mine1 = t] ++ mine) foreign
adamc@709 221 -> sql_table (foreign ++ funused) ([nm = map (fn _ => ()) foreign] ++ uniques)
adamc@709 222 -> {OnDelete : propagation_mode ([mine1 = t] ++ mine),
adamc@709 223 OnUpdate : propagation_mode ([mine1 = t] ++ mine)}
adamc@709 224 -> sql_constraint ([mine1 = t] ++ mine ++ munused) []
adamc@709 225
adamc@714 226 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
adamc@714 227
adamc@714 228 val check : fs ::: {Type}
adamc@714 229 -> sql_exp [] [] fs bool
adamc@714 230 -> sql_constraint fs []
adamc@714 231
adamc@714 232
adamc@704 233
adamc@204 234 (*** Queries *)
adamc@204 235
adamc@233 236 con sql_query :: {{Type}} -> {Type} -> Type
adamc@233 237 con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type
adamc@204 238
adamc@223 239 con sql_subset :: {{Type}} -> {{Type}} -> Type
adamc@223 240 val sql_subset : keep_drop :: {({Type} * {Type})}
adamc@354 241 -> sql_subset
adamc@621 242 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop)
adamc@621 243 (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop)
adamc@354 244 val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables
adamc@223 245
adamc@748 246 con sql_from_items :: {{Type}} -> Type
adamc@748 247
adamc@753 248 val sql_from_table : t ::: Type -> fs ::: {Type}
adamc@753 249 -> fieldsOf t fs -> name :: Name
adamc@753 250 -> t -> sql_from_items [name = fs]
adamc@748 251 val sql_from_comma : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
adamc@748 252 -> [tabs1 ~ tabs2]
adamc@748 253 => sql_from_items tabs1 -> sql_from_items tabs2
adamc@748 254 -> sql_from_items (tabs1 ++ tabs2)
adamc@749 255 val sql_inner_join : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
adamc@749 256 -> [tabs1 ~ tabs2]
adamc@749 257 => sql_from_items tabs1 -> sql_from_items tabs2
adamc@749 258 -> sql_exp (tabs1 ++ tabs2) [] [] bool
adamc@749 259 -> sql_from_items (tabs1 ++ tabs2)
adamc@748 260
adamc@750 261 class nullify :: Type -> Type -> Type
adamc@750 262 val nullify_option : t ::: Type -> nullify (option t) (option t)
adamc@750 263 val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t)
adamc@750 264
adamc@750 265 val sql_left_join : tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}}
adamc@750 266 -> [tabs1 ~ tabs2]
adamc@750 267 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2)
adamc@750 268 -> sql_from_items tabs1 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs2)
adamc@750 269 -> sql_exp (tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool
adamc@750 270 -> sql_from_items (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
adamc@750 271
adamc@751 272 val sql_right_join : tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}}
adamc@751 273 -> [tabs1 ~ tabs2]
adamc@751 274 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1)
adamc@751 275 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items tabs2
adamc@751 276 -> sql_exp (map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool
adamc@751 277 -> sql_from_items (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
adamc@751 278
adamc@751 279 val sql_full_join : tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
adamc@751 280 -> [tabs1 ~ tabs2]
adamc@751 281 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2))
adamc@751 282 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs1)
adamc@751 283 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs2)
adamc@751 284 -> sql_exp (map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool
adamc@751 285 -> sql_from_items (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
adamc@751 286
adamc@748 287 val sql_query1 : tables ::: {{Type}}
adamc@354 288 -> grouped ::: {{Type}}
adamc@354 289 -> selectedFields ::: {{Type}}
adamc@354 290 -> selectedExps ::: {Type}
adamc@748 291 -> {From : sql_from_items tables,
adamc@748 292 Where : sql_exp tables [] [] bool,
adamc@748 293 GroupBy : sql_subset tables grouped,
adamc@748 294 Having : sql_exp grouped tables [] bool,
adamc@354 295 SelectFields : sql_subset grouped selectedFields,
adamc@748 296 SelectExps : $(map (sql_exp grouped tables [])
adamc@705 297 selectedExps) }
adamc@748 298 -> sql_query1 tables selectedFields selectedExps
adamc@229 299
adamc@229 300 type sql_relop
adamc@229 301 val sql_union : sql_relop
adamc@229 302 val sql_intersect : sql_relop
adamc@229 303 val sql_except : sql_relop
adamc@260 304 val sql_relop : tables1 ::: {{Type}}
adamc@354 305 -> tables2 ::: {{Type}}
adamc@354 306 -> selectedFields ::: {{Type}}
adamc@354 307 -> selectedExps ::: {Type}
adamc@354 308 -> sql_relop
adamc@354 309 -> sql_query1 tables1 selectedFields selectedExps
adamc@354 310 -> sql_query1 tables2 selectedFields selectedExps
adamc@354 311 -> sql_query1 selectedFields selectedFields selectedExps
adamc@229 312
adamc@230 313 type sql_direction
adamc@230 314 val sql_asc : sql_direction
adamc@230 315 val sql_desc : sql_direction
adamc@230 316
adamc@234 317 con sql_order_by :: {{Type}} -> {Type} -> Type
adamc@234 318 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
adamc@234 319 val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
adamc@354 320 -> sql_exp tables [] exps t -> sql_direction
adamc@354 321 -> sql_order_by tables exps
adamc@354 322 -> sql_order_by tables exps
adamc@230 323
adamc@231 324 type sql_limit
adamc@231 325 val sql_no_limit : sql_limit
adamc@231 326 val sql_limit : int -> sql_limit
adamc@354 327
adamc@232 328 type sql_offset
adamc@232 329 val sql_no_offset : sql_offset
adamc@232 330 val sql_offset : int -> sql_offset
adamc@232 331
adamc@229 332 val sql_query : tables ::: {{Type}}
adamc@354 333 -> selectedFields ::: {{Type}}
adamc@354 334 -> selectedExps ::: {Type}
adamc@354 335 -> {Rows : sql_query1 tables selectedFields selectedExps,
adamc@354 336 OrderBy : sql_order_by tables selectedExps,
adamc@354 337 Limit : sql_limit,
adamc@354 338 Offset : sql_offset}
adamc@354 339 -> sql_query selectedFields selectedExps
adamc@204 340
adamc@354 341 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
adamc@354 342 -> fieldType ::: Type -> agg ::: {{Type}}
adamc@354 343 -> exps ::: {Type}
adamc@354 344 -> tab :: Name -> field :: Name
adamc@354 345 -> sql_exp
adamc@354 346 ([tab = [field = fieldType] ++ otherFields] ++ otherTabs)
adamc@354 347 agg exps fieldType
adamc@234 348
adamc@354 349 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type}
adamc@354 350 -> nm :: Name
adamc@354 351 -> sql_exp tabs agg ([nm = t] ++ rest) t
adamc@209 352
adamc@221 353 class sql_injectable
adamc@676 354 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t
adamc@676 355 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)
adamc@676 356
adamc@354 357 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 358 -> t ::: Type
adamc@354 359 -> sql_injectable t -> t -> sql_exp tables agg exps t
adamc@209 360
adamc@470 361 val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 362 -> t ::: Type
adamc@470 363 -> sql_exp tables agg exps (option t)
adamc@470 364 -> sql_exp tables agg exps bool
adamc@470 365
adamc@559 366 class sql_arith
adamc@559 367 val sql_int_arith : sql_arith int
adamc@559 368 val sql_float_arith : sql_arith float
adamc@559 369
adamc@220 370 con sql_unary :: Type -> Type -> Type
adamc@220 371 val sql_not : sql_unary bool bool
adamc@354 372 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 373 -> arg ::: Type -> res ::: Type
adamc@354 374 -> sql_unary arg res -> sql_exp tables agg exps arg
adamc@354 375 -> sql_exp tables agg exps res
adamc@220 376
adamc@559 377 val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t
adamc@559 378
adamc@220 379 con sql_binary :: Type -> Type -> Type -> Type
adamc@220 380 val sql_and : sql_binary bool bool bool
adamc@220 381 val sql_or : sql_binary bool bool bool
adamc@234 382 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 383 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
adamc@354 384 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1
adamc@354 385 -> sql_exp tables agg exps arg2
adamc@354 386 -> sql_exp tables agg exps res
adamc@220 387
adamc@559 388 val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 389 val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 390 val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 391 val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 392 val sql_mod : sql_binary int int int
adamc@559 393
adamc@559 394 val sql_eq : t ::: Type -> sql_binary t t bool
adamc@559 395 val sql_ne : t ::: Type -> sql_binary t t bool
adamc@559 396 val sql_lt : t ::: Type -> sql_binary t t bool
adamc@559 397 val sql_le : t ::: Type -> sql_binary t t bool
adamc@559 398 val sql_gt : t ::: Type -> sql_binary t t bool
adamc@559 399 val sql_ge : t ::: Type -> sql_binary t t bool
adamc@203 400
adamc@235 401 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@544 402 -> sql_exp tables agg exps int
adamc@235 403
adamc@236 404 con sql_aggregate :: Type -> Type
adamc@354 405 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 406 -> t ::: Type
adamc@354 407 -> sql_aggregate t -> sql_exp agg agg exps t
adamc@354 408 -> sql_exp tables agg exps t
adamc@236 409
adamc@236 410 class sql_summable
adamc@236 411 val sql_summable_int : sql_summable int
adamc@236 412 val sql_summable_float : sql_summable float
adamc@236 413 val sql_avg : t ::: Type -> sql_summable t -> sql_aggregate t
adamc@236 414 val sql_sum : t ::: Type -> sql_summable t -> sql_aggregate t
adamc@236 415
adamc@236 416 class sql_maxable
adamc@236 417 val sql_maxable_int : sql_maxable int
adamc@236 418 val sql_maxable_float : sql_maxable float
adamc@236 419 val sql_maxable_string : sql_maxable string
adamc@437 420 val sql_maxable_time : sql_maxable time
adamc@236 421 val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t
adamc@236 422 val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t
adamc@236 423
adamc@441 424 con sql_nfunc :: Type -> Type
adamc@441 425 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@441 426 -> t ::: Type
adamc@441 427 -> sql_nfunc t -> sql_exp tables agg exps t
adamc@441 428 val sql_current_timestamp : sql_nfunc time
adamc@441 429
adamc@746 430 con sql_ufunc :: Type -> Type -> Type
adamc@746 431 val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@746 432 -> dom ::: Type -> ran ::: Type
adamc@746 433 -> sql_ufunc dom ran -> sql_exp tables agg exps dom
adamc@746 434 -> sql_exp tables agg exps ran
adamc@746 435 val sql_octet_length : sql_ufunc blob int
adamc@746 436
adamc@235 437
adamc@243 438 (*** Executing queries *)
adamc@243 439
adamc@354 440 val query : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 441 -> [tables ~ exps] =>
adamc@354 442 state ::: Type
adamc@354 443 -> sql_query tables exps
adamc@621 444 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@354 445 -> state
adamc@354 446 -> transaction state)
adamc@354 447 -> state
adamc@354 448 -> transaction state
adamc@243 449
adamc@243 450
adamc@299 451 (*** Database mutators *)
adamc@299 452
adamc@299 453 type dml
adamc@299 454 val dml : dml -> transaction unit
adamc@299 455
adamc@705 456 val insert : fields ::: {Type} -> uniques ::: {{Unit}}
adamc@705 457 -> sql_table fields uniques
adamc@621 458 -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
adamc@354 459 -> dml
adamc@299 460
adamc@705 461 val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} ->
adamc@629 462 [changed ~ unchanged] =>
adamc@621 463 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
adamc@705 464 -> sql_table (changed ++ unchanged) uniques
adamc@354 465 -> sql_exp [T = changed ++ unchanged] [] [] bool
adamc@354 466 -> dml
adamc@299 467
adamc@705 468 val delete : fields ::: {Type} -> uniques ::: {{Unit}}
adamc@705 469 -> sql_table fields uniques
adamc@354 470 -> sql_exp [T = fields] [] [] bool
adamc@354 471 -> dml
adamc@299 472
adamc@338 473 (*** Sequences *)
adamc@338 474
adamc@338 475 type sql_sequence
adamc@338 476 val nextval : sql_sequence -> transaction int
adamc@338 477
adamc@299 478
adamc@203 479 (** XML *)
adamc@203 480
adamc@721 481 type css_class
adamc@718 482
adamc@720 483 con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
adamc@91 484
adamc@720 485 con xml :: {Unit} -> {Type} -> {Type} -> Type
adamc@720 486 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
adamc@354 487 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type}
adamc@354 488 -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
adamc@354 489 -> useOuter ::: {Type} -> useInner ::: {Type}
adamc@354 490 -> bindOuter ::: {Type} -> bindInner ::: {Type}
adamc@629 491 -> [attrsGiven ~ attrsAbsent] =>
adamc@629 492 [useOuter ~ useInner] =>
adamc@629 493 [bindOuter ~ bindInner] =>
adamc@721 494 option css_class
adamc@721 495 -> $attrsGiven
adamc@629 496 -> tag (attrsGiven ++ attrsAbsent)
adamc@720 497 ctxOuter ctxInner useOuter bindOuter
adamc@720 498 -> xml ctxInner useInner bindInner
adamc@720 499 -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
adamc@140 500 val join : ctx ::: {Unit}
adamc@720 501 -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
adamc@720 502 -> [use1 ~ bind1] => [bind1 ~ bind2] =>
adamc@720 503 xml ctx use1 bind1
adamc@720 504 -> xml ctx (use1 ++ bind1) bind2
adamc@720 505 -> xml ctx use1 (bind1 ++ bind2)
adamc@354 506 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type}
adamc@720 507 -> bind ::: {Type}
adamc@629 508 -> [use1 ~ use2] =>
adamc@720 509 xml ctx use1 bind
adamc@720 510 -> xml ctx (use1 ++ use2) bind
adamc@91 511
adamc@110 512 con xhtml = xml [Html]
adamc@139 513 con page = xhtml [] []
adamc@720 514 con xbody = xml [Body] [] []
adamc@720 515 con xtr = xml [Body, Tr] [] []
adamc@720 516 con xform = xml [Body, Form] [] []
adamc@110 517
adamc@718 518
adamc@204 519 (*** HTML details *)
adamc@204 520
adamc@140 521 con html = [Html]
adamc@140 522 con head = [Head]
adamc@140 523 con body = [Body]
adamc@361 524 con form = [Body, Form]
adamc@760 525 con subform = [Body, Subform]
adamc@332 526 con tabl = [Body, Table]
adamc@332 527 con tr = [Body, Tr]
adamc@93 528
adamc@724 529 type url
adamc@724 530 val bless : string -> url
adamc@770 531 val checkUrl : string -> option url
adamc@724 532
adamc@847 533 val dyn : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> [ctx ~ body] => unit
adamc@847 534 -> tag [Signal = signal (xml (body ++ ctx) use bind)] (body ++ ctx) [] use bind
adamc@568 535
adamc@720 536 val head : unit -> tag [] html head [] []
adamc@720 537 val title : unit -> tag [] head [] [] []
adamc@724 538 val link : unit -> tag [Rel = string, Typ = string, Href = url, Media = string] head [] [] []
adamc@110 539
adamc@720 540 val body : unit -> tag [Onload = transaction unit] html body [] []
adamc@354 541 con bodyTag = fn (attrs :: {Type}) =>
adamc@354 542 ctx ::: {Unit} ->
adamc@629 543 [[Body] ~ ctx] =>
adamc@720 544 unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
adamc@354 545 con bodyTagStandalone = fn (attrs :: {Type}) =>
adamc@354 546 ctx ::: {Unit}
adamc@629 547 -> [[Body] ~ ctx] =>
adamc@720 548 unit -> tag attrs ([Body] ++ ctx) [] [] []
adamc@141 549
adamc@141 550 val br : bodyTagStandalone []
adamc@119 551
adamc@691 552 val span : bodyTag []
adamc@775 553 val div : bodyTag []
adamc@691 554
adamc@140 555 val p : bodyTag []
adamc@140 556 val b : bodyTag []
adamc@140 557 val i : bodyTag []
adamc@407 558 val tt : bodyTag []
adamc@140 559 val font : bodyTag [Size = int, Face = string]
adamc@140 560
adamc@140 561 val h1 : bodyTag []
adamc@443 562 val h2 : bodyTag []
adamc@443 563 val h3 : bodyTag []
adamc@443 564 val h4 : bodyTag []
adamc@469 565
adamc@140 566 val li : bodyTag []
adamc@469 567 val ol : bodyTag []
adamc@469 568 val ul : bodyTag []
adamc@140 569
adamc@410 570 val hr : bodyTag []
adamc@410 571
adamc@720 572 val a : bodyTag [Link = transaction page, Href = url, Onclick = transaction unit]
adamc@717 573
adamc@717 574 val img : bodyTag [Src = url]
adamc@140 575
adamc@720 576 val form : ctx ::: {Unit} -> bind ::: {Type}
adamc@756 577 -> [[Body] ~ ctx] =>
adamc@756 578 xml form [] bind
adamc@756 579 -> xml ([Body] ++ ctx) [] []
adamc@756 580
adamc@756 581 val subform : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
adamc@756 582 -> [[Form] ~ ctx] =>
adamc@756 583 nm :: Name -> [[nm] ~ use] =>
adamc@756 584 xml form [] bind
adamc@756 585 -> xml ([Form] ++ ctx) use [nm = $bind]
adamc@758 586
adamc@758 587 val subforms : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
adamc@758 588 -> [[Form] ~ ctx] =>
adamc@758 589 nm :: Name -> [[nm] ~ use] =>
adamc@760 590 xml subform [Entry = $bind] []
adamc@758 591 -> xml ([Form] ++ ctx) use [nm = list ($bind)]
adamc@758 592
adamc@758 593 val entry : ctx ::: {Unit} -> bind ::: {Type}
adamc@758 594 -> [[Subform] ~ ctx] =>
adamc@758 595 xml form [] bind
adamc@758 596 -> xml ([Subform] ++ ctx) [Entry = $bind] []
adamc@758 597
adamc@361 598 con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) =>
adamc@354 599 ctx ::: {Unit}
adamc@629 600 -> [[Form] ~ ctx] =>
adamc@354 601 nm :: Name -> unit
adamc@720 602 -> tag attrs ([Form] ++ ctx) inner [] [nm = ty]
adamc@761 603 val hidden : formTag string [] [Value = string]
adamc@598 604 val textbox : formTag string [] [Value = string, Size = int, Source = source string]
adamc@444 605 val password : formTag string [] [Value = string, Size = int]
adamc@444 606 val textarea : formTag string [] [Rows = int, Cols = int]
adamc@153 607
adamc@361 608 val checkbox : formTag bool [] [Checked = bool]
adamc@190 609
adamc@737 610 type file
adamc@737 611 val fileName : file -> option string
adamc@740 612 val fileMimeType : file -> string
adamc@737 613 val fileData : file -> blob
adamc@737 614
adamc@739 615 val upload : formTag file [] [Value = string, Size = int]
adamc@737 616
adamc@741 617 type mimeType
adamc@741 618 val blessMime : string -> mimeType
adamc@770 619 val checkMime : string -> option mimeType
adamc@741 620 val returnBlob : t ::: Type -> blob -> mimeType -> transaction t
adamc@745 621 val blobSize : blob -> int
adamc@741 622
adamc@153 623 con radio = [Body, Radio]
adamc@361 624 val radio : formTag string radio []
adamc@720 625 val radioOption : unit -> tag [Value = string] radio [] [] []
adamc@142 626
adamc@154 627 con select = [Select]
adamc@361 628 val select : formTag string select []
adamc@720 629 val option : unit -> tag [Value = string, Selected = bool] select [] [] []
adamc@154 630
adamc@720 631 val submit : ctx ::: {Unit} -> use ::: {Type}
adamc@629 632 -> [[Form] ~ ctx] =>
adamc@354 633 unit
adamc@720 634 -> tag [Value = string, Action = $use -> transaction page]
adamc@720 635 ([Form] ++ ctx) ([Form] ++ ctx) use []
adamc@283 636
adamc@601 637 (*** AJAX-oriented widgets *)
adamc@601 638
adamc@797 639 con cformTag = fn (attrs :: {Type}) (inner :: {Unit}) =>
adamc@601 640 ctx ::: {Unit}
adamc@629 641 -> [[Body] ~ ctx] =>
adamc@797 642 unit -> tag attrs ([Body] ++ ctx) inner [] []
adamc@601 643
adamc@797 644 val ctextbox : cformTag [Value = string, Size = int, Source = source string] []
adamc@797 645 val button : cformTag [Value = string, Onclick = transaction unit] []
adamc@797 646
adamc@817 647 val ccheckbox : cformTag [Value = bool, Size = int, Source = source bool] []
adamc@817 648
adamc@797 649 con cselect = [Cselect]
adamc@799 650 val cselect : cformTag [Source = source string,
adamc@799 651 Onchange = transaction unit] cselect
adamc@797 652 val coption : unit -> tag [Value = string, Selected = bool] cselect [] [] []
adamc@601 653
adamc@720 654 (*** Tables *)
adamc@720 655
adamc@720 656 val tabl : other ::: {Unit} -> [other ~ [Body, Table]] =>
adamc@720 657 unit -> tag [Border = int] ([Body] ++ other) ([Body, Table] ++ other) [] []
adamc@720 658 val tr : other ::: {Unit} -> [other ~ [Body, Table, Tr]] =>
adamc@720 659 unit -> tag [] ([Body, Table] ++ other) ([Body, Tr] ++ other) [] []
adamc@720 660 val th : other ::: {Unit} -> [other ~ [Body, Tr]] =>
adamc@720 661 unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] []
adamc@720 662 val td : other ::: {Unit} -> [other ~ [Body, Tr]] =>
adamc@720 663 unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] []
adamc@720 664
adamc@283 665
adamc@283 666 (** Aborting *)
adamc@283 667
adamc@726 668 val error : t ::: Type -> xbody -> t
adamc@720 669
adamc@729 670 (* Client-side-only handlers: *)
adamc@726 671 val onError : (xbody -> transaction unit) -> transaction unit
adamc@728 672 val onFail : (string -> transaction unit) -> transaction unit
adamc@729 673 val onConnectFail : transaction unit -> transaction unit
adamc@729 674 val onDisconnect : transaction unit -> transaction unit
adamc@729 675 val onServerError : (string -> transaction unit) -> transaction unit
adamc@727 676
adamc@727 677 val show_xml : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> show (xml ctx use bind)