Mercurial > urweb

annotate lib/ur/basis.urs @ 925:552c989c1601

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Change string URLification to avoid using the empty string, which confuses Apache no2slash()
author Adam Chlipala <adamc@hcoop.net>
date Sat, 12 Sep 2009 09:31:50 -0400
parents ed06e25c70ef
children b8d7a47b8e0c
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@908 128 val rpc : t ::: Type -> transaction t -> transaction t
adamc@908 129
adamc@566 130
adamc@678 131 (** Channels *)
adamc@678 132
adamc@678 133 con channel :: Type -> Type
adamc@678 134 val channel : t ::: Type -> transaction (channel t)
adamc@678 135 val send : t ::: Type -> channel t -> t -> transaction unit
adamc@678 136 val recv : t ::: Type -> channel t -> transaction t
adamc@678 137
adamc@682 138 type client
adamc@682 139 val self : transaction client
adamc@682 140
adamc@678 141
adamc@203 142 (** SQL *)
adamc@203 143
adamc@705 144 con sql_table :: {Type} -> {{Unit}} -> Type
adamc@753 145 con sql_view :: {Type} -> Type
adamc@753 146
adamc@753 147 class fieldsOf :: Type -> {Type} -> Type
adamc@753 148 val fieldsOf_table : fs ::: {Type} -> keys ::: {{Unit}}
adamc@753 149 -> fieldsOf (sql_table fs keys) fs
adamc@753 150 val fieldsOf_view : fs ::: {Type}
adamc@753 151 -> fieldsOf (sql_view fs) fs
adamc@203 152
adamc@704 153 (*** Constraints *)
adamc@704 154
adamc@707 155 (**** Primary keys *)
adamc@707 156
adamc@707 157 class sql_injectable_prim
adamc@707 158 val sql_bool : sql_injectable_prim bool
adamc@707 159 val sql_int : sql_injectable_prim int
adamc@707 160 val sql_float : sql_injectable_prim float
adamc@707 161 val sql_string : sql_injectable_prim string
adamc@707 162 val sql_time : sql_injectable_prim time
adamc@737 163 val sql_blob : sql_injectable_prim blob
adamc@707 164 val sql_channel : t ::: Type -> sql_injectable_prim (channel t)
adamc@707 165 val sql_client : sql_injectable_prim client
adamc@707 166
adamc@707 167 con primary_key :: {Type} -> {{Unit}} -> Type
adamc@707 168 val no_primary_key : fs ::: {Type} -> primary_key fs []
adamc@707 169 val primary_key : rest ::: {Type} -> t ::: Type -> key1 :: Name -> keys :: {Type}
adamc@707 170 -> [[key1] ~ keys] => [[key1 = t] ++ keys ~ rest]
adamc@707 171 => $([key1 = sql_injectable_prim t] ++ map sql_injectable_prim keys)
adamc@707 172 -> primary_key ([key1 = t] ++ keys ++ rest)
adamc@707 173 [Pkey = [key1] ++ map (fn _ => ()) keys]
adamc@707 174
adamc@707 175 (**** Other constraints *)
adamc@707 176
adamc@705 177 con sql_constraints :: {Type} -> {{Unit}} -> Type
adamc@705 178 (* Arguments: column types, uniqueness implications of constraints *)
adamc@704 179
adamc@705 180 con sql_constraint :: {Type} -> {Unit} -> Type
adamc@704 181
adamc@705 182 val no_constraint : fs ::: {Type} -> sql_constraints fs []
adamc@705 183 val one_constraint : fs ::: {Type} -> unique ::: {Unit} -> name :: Name
adamc@705 184 -> sql_constraint fs unique
adamc@705 185 -> sql_constraints fs [name = unique]
adamc@705 186 val join_constraints : fs ::: {Type}
adamc@705 187 -> uniques1 ::: {{Unit}} -> uniques2 ::: {{Unit}} -> [uniques1 ~ uniques2]
adamc@705 188 => sql_constraints fs uniques1 -> sql_constraints fs uniques2
adamc@705 189 -> sql_constraints fs (uniques1 ++ uniques2)
adamc@705 190
adamc@709 191
adamc@705 192 val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type}
adamc@705 193 -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest]
adamc@705 194 => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique)
adamc@704 195
adamc@712 196 class linkable :: Type -> Type -> Type
adamc@712 197 val linkable_same : t ::: Type -> linkable t t
adamc@712 198 val linkable_from_nullable : t ::: Type -> linkable (option t) t
adamc@712 199 val linkable_to_nullable : t ::: Type -> linkable t (option t)
adamc@712 200
adamc@709 201 con matching :: {Type} -> {Type} -> Type
adamc@709 202 val mat_nil : matching [] []
adamc@712 203 val mat_cons : t1 ::: Type -> rest1 ::: {Type} -> t2 ::: Type -> rest2 ::: {Type}
adamc@709 204 -> nm1 :: Name -> nm2 :: Name
adamc@709 205 -> [[nm1] ~ rest1] => [[nm2] ~ rest2]
adamc@712 206 => linkable t1 t2
adamc@712 207 -> matching rest1 rest2
adamc@712 208 -> matching ([nm1 = t1] ++ rest1) ([nm2 = t2] ++ rest2)
adamc@709 209
adamc@709 210 con propagation_mode :: {Type} -> Type
adamc@709 211 val restrict : fs ::: {Type} -> propagation_mode fs
adamc@709 212 val cascade : fs ::: {Type} -> propagation_mode fs
adamc@709 213 val no_action : fs ::: {Type} -> propagation_mode fs
adamc@709 214 val set_null : fs ::: {Type} -> propagation_mode (map option fs)
adamc@709 215
adamc@709 216
adamc@709 217 val foreign_key : mine1 ::: Name -> t ::: Type -> mine ::: {Type} -> munused ::: {Type}
adamc@709 218 -> foreign ::: {Type} -> funused ::: {Type}
adamc@709 219 -> nm ::: Name -> uniques ::: {{Unit}}
adamc@709 220 -> [[mine1] ~ mine] => [[mine1 = t] ++ mine ~ munused]
adamc@709 221 => [foreign ~ funused] => [[nm] ~ uniques]
adamc@709 222 => matching ([mine1 = t] ++ mine) foreign
adamc@709 223 -> sql_table (foreign ++ funused) ([nm = map (fn _ => ()) foreign] ++ uniques)
adamc@709 224 -> {OnDelete : propagation_mode ([mine1 = t] ++ mine),
adamc@709 225 OnUpdate : propagation_mode ([mine1 = t] ++ mine)}
adamc@709 226 -> sql_constraint ([mine1 = t] ++ mine ++ munused) []
adamc@709 227
adamc@714 228 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
adamc@714 229
adamc@714 230 val check : fs ::: {Type}
adamc@714 231 -> sql_exp [] [] fs bool
adamc@714 232 -> sql_constraint fs []
adamc@714 233
adamc@714 234
adamc@704 235
adamc@204 236 (*** Queries *)
adamc@204 237
adamc@233 238 con sql_query :: {{Type}} -> {Type} -> Type
adamc@233 239 con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type
adamc@204 240
adamc@223 241 con sql_subset :: {{Type}} -> {{Type}} -> Type
adamc@223 242 val sql_subset : keep_drop :: {({Type} * {Type})}
adamc@354 243 -> sql_subset
adamc@621 244 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop)
adamc@621 245 (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop)
adamc@354 246 val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables
adamc@223 247
adamc@748 248 con sql_from_items :: {{Type}} -> Type
adamc@748 249
adamc@753 250 val sql_from_table : t ::: Type -> fs ::: {Type}
adamc@753 251 -> fieldsOf t fs -> name :: Name
adamc@753 252 -> t -> sql_from_items [name = fs]
adamc@748 253 val sql_from_comma : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
adamc@748 254 -> [tabs1 ~ tabs2]
adamc@748 255 => sql_from_items tabs1 -> sql_from_items tabs2
adamc@748 256 -> sql_from_items (tabs1 ++ tabs2)
adamc@749 257 val sql_inner_join : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
adamc@749 258 -> [tabs1 ~ tabs2]
adamc@749 259 => sql_from_items tabs1 -> sql_from_items tabs2
adamc@749 260 -> sql_exp (tabs1 ++ tabs2) [] [] bool
adamc@749 261 -> sql_from_items (tabs1 ++ tabs2)
adamc@748 262
adamc@750 263 class nullify :: Type -> Type -> Type
adamc@750 264 val nullify_option : t ::: Type -> nullify (option t) (option t)
adamc@750 265 val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t)
adamc@750 266
adamc@750 267 val sql_left_join : tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}}
adamc@750 268 -> [tabs1 ~ tabs2]
adamc@750 269 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2)
adamc@750 270 -> sql_from_items tabs1 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs2)
adamc@750 271 -> sql_exp (tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool
adamc@750 272 -> sql_from_items (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
adamc@750 273
adamc@751 274 val sql_right_join : tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}}
adamc@751 275 -> [tabs1 ~ tabs2]
adamc@751 276 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1)
adamc@751 277 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items tabs2
adamc@751 278 -> sql_exp (map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool
adamc@751 279 -> sql_from_items (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
adamc@751 280
adamc@751 281 val sql_full_join : tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
adamc@751 282 -> [tabs1 ~ tabs2]
adamc@751 283 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2))
adamc@751 284 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs1)
adamc@751 285 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs2)
adamc@751 286 -> sql_exp (map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool
adamc@751 287 -> sql_from_items (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
adamc@751 288
adamc@748 289 val sql_query1 : tables ::: {{Type}}
adamc@354 290 -> grouped ::: {{Type}}
adamc@354 291 -> selectedFields ::: {{Type}}
adamc@354 292 -> selectedExps ::: {Type}
adamc@748 293 -> {From : sql_from_items tables,
adamc@748 294 Where : sql_exp tables [] [] bool,
adamc@748 295 GroupBy : sql_subset tables grouped,
adamc@748 296 Having : sql_exp grouped tables [] bool,
adamc@354 297 SelectFields : sql_subset grouped selectedFields,
adamc@748 298 SelectExps : $(map (sql_exp grouped tables [])
adamc@705 299 selectedExps) }
adamc@748 300 -> sql_query1 tables selectedFields selectedExps
adamc@229 301
adamc@229 302 type sql_relop
adamc@229 303 val sql_union : sql_relop
adamc@229 304 val sql_intersect : sql_relop
adamc@229 305 val sql_except : sql_relop
adamc@260 306 val sql_relop : tables1 ::: {{Type}}
adamc@354 307 -> tables2 ::: {{Type}}
adamc@354 308 -> selectedFields ::: {{Type}}
adamc@354 309 -> selectedExps ::: {Type}
adamc@354 310 -> sql_relop
adamc@354 311 -> sql_query1 tables1 selectedFields selectedExps
adamc@354 312 -> sql_query1 tables2 selectedFields selectedExps
adamc@354 313 -> sql_query1 selectedFields selectedFields selectedExps
adamc@229 314
adamc@230 315 type sql_direction
adamc@230 316 val sql_asc : sql_direction
adamc@230 317 val sql_desc : sql_direction
adamc@230 318
adamc@234 319 con sql_order_by :: {{Type}} -> {Type} -> Type
adamc@234 320 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
adamc@234 321 val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
adamc@354 322 -> sql_exp tables [] exps t -> sql_direction
adamc@354 323 -> sql_order_by tables exps
adamc@354 324 -> sql_order_by tables exps
adamc@230 325
adamc@231 326 type sql_limit
adamc@231 327 val sql_no_limit : sql_limit
adamc@231 328 val sql_limit : int -> sql_limit
adamc@354 329
adamc@232 330 type sql_offset
adamc@232 331 val sql_no_offset : sql_offset
adamc@232 332 val sql_offset : int -> sql_offset
adamc@232 333
adamc@229 334 val sql_query : tables ::: {{Type}}
adamc@354 335 -> selectedFields ::: {{Type}}
adamc@354 336 -> selectedExps ::: {Type}
adamc@354 337 -> {Rows : sql_query1 tables selectedFields selectedExps,
adamc@354 338 OrderBy : sql_order_by tables selectedExps,
adamc@354 339 Limit : sql_limit,
adamc@354 340 Offset : sql_offset}
adamc@354 341 -> sql_query selectedFields selectedExps
adamc@204 342
adamc@354 343 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
adamc@354 344 -> fieldType ::: Type -> agg ::: {{Type}}
adamc@354 345 -> exps ::: {Type}
adamc@354 346 -> tab :: Name -> field :: Name
adamc@354 347 -> sql_exp
adamc@354 348 ([tab = [field = fieldType] ++ otherFields] ++ otherTabs)
adamc@354 349 agg exps fieldType
adamc@234 350
adamc@354 351 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type}
adamc@354 352 -> nm :: Name
adamc@354 353 -> sql_exp tabs agg ([nm = t] ++ rest) t
adamc@209 354
adamc@221 355 class sql_injectable
adamc@676 356 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t
adamc@676 357 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)
adamc@676 358
adamc@354 359 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 360 -> t ::: Type
adamc@354 361 -> sql_injectable t -> t -> sql_exp tables agg exps t
adamc@209 362
adamc@470 363 val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 364 -> t ::: Type
adamc@470 365 -> sql_exp tables agg exps (option t)
adamc@470 366 -> sql_exp tables agg exps bool
adamc@470 367
adamc@559 368 class sql_arith
adamc@559 369 val sql_int_arith : sql_arith int
adamc@559 370 val sql_float_arith : sql_arith float
adamc@559 371
adamc@220 372 con sql_unary :: Type -> Type -> Type
adamc@220 373 val sql_not : sql_unary bool bool
adamc@354 374 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 375 -> arg ::: Type -> res ::: Type
adamc@354 376 -> sql_unary arg res -> sql_exp tables agg exps arg
adamc@354 377 -> sql_exp tables agg exps res
adamc@220 378
adamc@559 379 val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t
adamc@559 380
adamc@220 381 con sql_binary :: Type -> Type -> Type -> Type
adamc@220 382 val sql_and : sql_binary bool bool bool
adamc@220 383 val sql_or : sql_binary bool bool bool
adamc@234 384 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 385 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
adamc@354 386 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1
adamc@354 387 -> sql_exp tables agg exps arg2
adamc@354 388 -> sql_exp tables agg exps res
adamc@220 389
adamc@559 390 val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 391 val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 392 val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 393 val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 394 val sql_mod : sql_binary int int int
adamc@559 395
adamc@559 396 val sql_eq : t ::: Type -> sql_binary t t bool
adamc@559 397 val sql_ne : t ::: Type -> sql_binary t t bool
adamc@559 398 val sql_lt : t ::: Type -> sql_binary t t bool
adamc@559 399 val sql_le : t ::: Type -> sql_binary t t bool
adamc@559 400 val sql_gt : t ::: Type -> sql_binary t t bool
adamc@559 401 val sql_ge : t ::: Type -> sql_binary t t bool
adamc@203 402
adamc@235 403 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@544 404 -> sql_exp tables agg exps int
adamc@235 405
adamc@236 406 con sql_aggregate :: Type -> Type
adamc@354 407 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 408 -> t ::: Type
adamc@354 409 -> sql_aggregate t -> sql_exp agg agg exps t
adamc@354 410 -> sql_exp tables agg exps t
adamc@236 411
adamc@236 412 class sql_summable
adamc@236 413 val sql_summable_int : sql_summable int
adamc@236 414 val sql_summable_float : sql_summable float
adamc@236 415 val sql_avg : t ::: Type -> sql_summable t -> sql_aggregate t
adamc@236 416 val sql_sum : t ::: Type -> sql_summable t -> sql_aggregate t
adamc@236 417
adamc@236 418 class sql_maxable
adamc@236 419 val sql_maxable_int : sql_maxable int
adamc@236 420 val sql_maxable_float : sql_maxable float
adamc@236 421 val sql_maxable_string : sql_maxable string
adamc@437 422 val sql_maxable_time : sql_maxable time
adamc@236 423 val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t
adamc@236 424 val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t
adamc@236 425
adamc@441 426 con sql_nfunc :: Type -> Type
adamc@441 427 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@441 428 -> t ::: Type
adamc@441 429 -> sql_nfunc t -> sql_exp tables agg exps t
adamc@441 430 val sql_current_timestamp : sql_nfunc time
adamc@441 431
adamc@746 432 con sql_ufunc :: Type -> Type -> Type
adamc@746 433 val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@746 434 -> dom ::: Type -> ran ::: Type
adamc@746 435 -> sql_ufunc dom ran -> sql_exp tables agg exps dom
adamc@746 436 -> sql_exp tables agg exps ran
adamc@746 437 val sql_octet_length : sql_ufunc blob int
adamc@746 438
adamc@235 439
adamc@243 440 (*** Executing queries *)
adamc@243 441
adamc@354 442 val query : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 443 -> [tables ~ exps] =>
adamc@354 444 state ::: Type
adamc@354 445 -> sql_query tables exps
adamc@621 446 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@354 447 -> state
adamc@354 448 -> transaction state)
adamc@354 449 -> state
adamc@354 450 -> transaction state
adamc@243 451
adamc@243 452
adamc@299 453 (*** Database mutators *)
adamc@299 454
adamc@299 455 type dml
adamc@299 456 val dml : dml -> transaction unit
adamc@299 457
adamc@705 458 val insert : fields ::: {Type} -> uniques ::: {{Unit}}
adamc@705 459 -> sql_table fields uniques
adamc@621 460 -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
adamc@354 461 -> dml
adamc@299 462
adamc@705 463 val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} ->
adamc@629 464 [changed ~ unchanged] =>
adamc@621 465 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
adamc@705 466 -> sql_table (changed ++ unchanged) uniques
adamc@354 467 -> sql_exp [T = changed ++ unchanged] [] [] bool
adamc@354 468 -> dml
adamc@299 469
adamc@705 470 val delete : fields ::: {Type} -> uniques ::: {{Unit}}
adamc@705 471 -> sql_table fields uniques
adamc@354 472 -> sql_exp [T = fields] [] [] bool
adamc@354 473 -> dml
adamc@299 474
adamc@338 475 (*** Sequences *)
adamc@338 476
adamc@338 477 type sql_sequence
adamc@338 478 val nextval : sql_sequence -> transaction int
adamc@338 479
adamc@299 480
adamc@203 481 (** XML *)
adamc@203 482
adamc@721 483 type css_class
adamc@718 484
adamc@720 485 con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
adamc@91 486
adamc@720 487 con xml :: {Unit} -> {Type} -> {Type} -> Type
adamc@720 488 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
adamc@354 489 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type}
adamc@354 490 -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
adamc@354 491 -> useOuter ::: {Type} -> useInner ::: {Type}
adamc@354 492 -> bindOuter ::: {Type} -> bindInner ::: {Type}
adamc@629 493 -> [attrsGiven ~ attrsAbsent] =>
adamc@629 494 [useOuter ~ useInner] =>
adamc@629 495 [bindOuter ~ bindInner] =>
adamc@721 496 option css_class
adamc@721 497 -> $attrsGiven
adamc@629 498 -> tag (attrsGiven ++ attrsAbsent)
adamc@720 499 ctxOuter ctxInner useOuter bindOuter
adamc@720 500 -> xml ctxInner useInner bindInner
adamc@720 501 -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
adamc@140 502 val join : ctx ::: {Unit}
adamc@720 503 -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
adamc@720 504 -> [use1 ~ bind1] => [bind1 ~ bind2] =>
adamc@720 505 xml ctx use1 bind1
adamc@720 506 -> xml ctx (use1 ++ bind1) bind2
adamc@720 507 -> xml ctx use1 (bind1 ++ bind2)
adamc@354 508 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type}
adamc@720 509 -> bind ::: {Type}
adamc@629 510 -> [use1 ~ use2] =>
adamc@720 511 xml ctx use1 bind
adamc@720 512 -> xml ctx (use1 ++ use2) bind
adamc@91 513
adamc@110 514 con xhtml = xml [Html]
adamc@139 515 con page = xhtml [] []
adamc@720 516 con xbody = xml [Body] [] []
adamc@720 517 con xtr = xml [Body, Tr] [] []
adamc@720 518 con xform = xml [Body, Form] [] []
adamc@110 519
adamc@718 520
adamc@204 521 (*** HTML details *)
adamc@204 522
adamc@140 523 con html = [Html]
adamc@140 524 con head = [Head]
adamc@140 525 con body = [Body]
adamc@361 526 con form = [Body, Form]
adamc@760 527 con subform = [Body, Subform]
adamc@332 528 con tabl = [Body, Table]
adamc@332 529 con tr = [Body, Tr]
adamc@93 530
adamc@724 531 type url
adamc@724 532 val bless : string -> url
adamc@770 533 val checkUrl : string -> option url
adamc@724 534
adamc@847 535 val dyn : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> [ctx ~ body] => unit
adamc@847 536 -> tag [Signal = signal (xml (body ++ ctx) use bind)] (body ++ ctx) [] use bind
adamc@568 537
adamc@720 538 val head : unit -> tag [] html head [] []
adamc@720 539 val title : unit -> tag [] head [] [] []
adamc@724 540 val link : unit -> tag [Rel = string, Typ = string, Href = url, Media = string] head [] [] []
adamc@110 541
adamc@892 542 val body : unit -> tag [Onload = transaction unit, Onresize = transaction unit, Onunload = transaction unit]
adamc@892 543 html body [] []
adamc@354 544 con bodyTag = fn (attrs :: {Type}) =>
adamc@354 545 ctx ::: {Unit} ->
adamc@629 546 [[Body] ~ ctx] =>
adamc@720 547 unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
adamc@354 548 con bodyTagStandalone = fn (attrs :: {Type}) =>
adamc@354 549 ctx ::: {Unit}
adamc@629 550 -> [[Body] ~ ctx] =>
adamc@720 551 unit -> tag attrs ([Body] ++ ctx) [] [] []
adamc@141 552
adamc@141 553 val br : bodyTagStandalone []
adamc@119 554
adamc@892 555 con focusEvents = [Onblur = transaction unit, Onfocus = transaction unit]
adamc@892 556 con mouseEvents = [Onclick = transaction unit, Ondblclick = transaction unit,
adamc@892 557 Onmousedown = transaction unit, Onmousemove = transaction unit,
adamc@892 558 Onmouseout = transaction unit, Onmouseover = transaction unit,
adamc@894 559 Onmouseup = transaction unit]
adamc@895 560 con keyEvents = [Onkeydown = int -> transaction unit, Onkeypress = int -> transaction unit,
adamc@895 561 Onkeyup = int -> transaction unit]
adamc@895 562 (* Key arguments are character codes. *)
adamc@892 563 con resizeEvents = [Onresize = transaction unit]
adamc@691 564
adamc@892 565 con boxEvents = focusEvents ++ mouseEvents ++ keyEvents ++ resizeEvents
adamc@892 566 con tableEvents = focusEvents ++ mouseEvents ++ keyEvents
adamc@140 567
adamc@892 568 val span : bodyTag boxEvents
adamc@892 569 val div : bodyTag boxEvents
adamc@469 570
adamc@892 571 val p : bodyTag boxEvents
adamc@892 572 val b : bodyTag boxEvents
adamc@892 573 val i : bodyTag boxEvents
adamc@892 574 val tt : bodyTag boxEvents
adamc@140 575
adamc@892 576 val h1 : bodyTag boxEvents
adamc@892 577 val h2 : bodyTag boxEvents
adamc@892 578 val h3 : bodyTag boxEvents
adamc@892 579 val h4 : bodyTag boxEvents
adamc@893 580 val h5 : bodyTag boxEvents
adamc@893 581 val h6 : bodyTag boxEvents
adamc@410 582
adamc@892 583 val li : bodyTag boxEvents
adamc@892 584 val ol : bodyTag boxEvents
adamc@892 585 val ul : bodyTag boxEvents
adamc@717 586
adamc@892 587 val hr : bodyTag boxEvents
adamc@140 588
adamc@892 589 val a : bodyTag ([Link = transaction page, Href = url] ++ boxEvents)
adamc@892 590
adamc@892 591 val img : bodyTag ([Src = url, Onabort = transaction unit, Onerror = transaction unit,
adamc@892 592 Onload = transaction unit] ++ boxEvents)
adamc@892 593
adamc@720 594 val form : ctx ::: {Unit} -> bind ::: {Type}
adamc@756 595 -> [[Body] ~ ctx] =>
adamc@756 596 xml form [] bind
adamc@756 597 -> xml ([Body] ++ ctx) [] []
adamc@756 598
adamc@756 599 val subform : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
adamc@756 600 -> [[Form] ~ ctx] =>
adamc@756 601 nm :: Name -> [[nm] ~ use] =>
adamc@756 602 xml form [] bind
adamc@756 603 -> xml ([Form] ++ ctx) use [nm = $bind]
adamc@758 604
adamc@758 605 val subforms : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
adamc@758 606 -> [[Form] ~ ctx] =>
adamc@758 607 nm :: Name -> [[nm] ~ use] =>
adamc@760 608 xml subform [Entry = $bind] []
adamc@758 609 -> xml ([Form] ++ ctx) use [nm = list ($bind)]
adamc@758 610
adamc@758 611 val entry : ctx ::: {Unit} -> bind ::: {Type}
adamc@758 612 -> [[Subform] ~ ctx] =>
adamc@758 613 xml form [] bind
adamc@758 614 -> xml ([Subform] ++ ctx) [Entry = $bind] []
adamc@758 615
adamc@361 616 con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) =>
adamc@354 617 ctx ::: {Unit}
adamc@629 618 -> [[Form] ~ ctx] =>
adamc@354 619 nm :: Name -> unit
adamc@720 620 -> tag attrs ([Form] ++ ctx) inner [] [nm = ty]
adamc@761 621 val hidden : formTag string [] [Value = string]
adamc@892 622 val textbox : formTag string [] ([Value = string, Size = int, Source = source string, Onchange = transaction unit,
adamc@892 623 Ontext = transaction unit] ++ boxEvents)
adamc@892 624 val password : formTag string [] ([Value = string, Size = int] ++ boxEvents)
adamc@892 625 val textarea : formTag string [] ([Rows = int, Cols = int, Onchange = transaction unit,
adamc@892 626 Ontext = transaction unit] ++ boxEvents)
adamc@153 627
adamc@892 628 val checkbox : formTag bool [] ([Checked = bool] ++ boxEvents)
adamc@190 629
adamc@737 630 type file
adamc@737 631 val fileName : file -> option string
adamc@740 632 val fileMimeType : file -> string
adamc@737 633 val fileData : file -> blob
adamc@737 634
adamc@892 635 val upload : formTag file [] ([Value = string, Size = int] ++ boxEvents)
adamc@737 636
adamc@741 637 type mimeType
adamc@741 638 val blessMime : string -> mimeType
adamc@770 639 val checkMime : string -> option mimeType
adamc@741 640 val returnBlob : t ::: Type -> blob -> mimeType -> transaction t
adamc@745 641 val blobSize : blob -> int
adamc@741 642
adamc@153 643 con radio = [Body, Radio]
adamc@361 644 val radio : formTag string radio []
adamc@892 645 val radioOption : unit -> tag ([Value = string] ++ boxEvents) radio [] [] []
adamc@142 646
adamc@154 647 con select = [Select]
adamc@892 648 val select : formTag string select ([Onchange = transaction unit] ++ boxEvents)
adamc@720 649 val option : unit -> tag [Value = string, Selected = bool] select [] [] []
adamc@154 650
adamc@720 651 val submit : ctx ::: {Unit} -> use ::: {Type}
adamc@629 652 -> [[Form] ~ ctx] =>
adamc@354 653 unit
adamc@892 654 -> tag ([Value = string, Action = $use -> transaction page] ++ boxEvents)
adamc@720 655 ([Form] ++ ctx) ([Form] ++ ctx) use []
adamc@283 656
adamc@601 657 (*** AJAX-oriented widgets *)
adamc@601 658
adamc@797 659 con cformTag = fn (attrs :: {Type}) (inner :: {Unit}) =>
adamc@601 660 ctx ::: {Unit}
adamc@629 661 -> [[Body] ~ ctx] =>
adamc@797 662 unit -> tag attrs ([Body] ++ ctx) inner [] []
adamc@601 663
adamc@892 664 val ctextbox : cformTag ([Value = string, Size = int, Source = source string, Onchange = transaction unit,
adamc@892 665 Ontext = transaction unit] ++ boxEvents) []
adamc@892 666 val button : cformTag ([Value = string] ++ boxEvents) []
adamc@797 667
adamc@892 668 val ccheckbox : cformTag ([Value = bool, Size = int, Source = source bool] ++ boxEvents) []
adamc@817 669
adamc@797 670 con cselect = [Cselect]
adamc@892 671 val cselect : cformTag ([Source = source string, Onchange = transaction unit] ++ boxEvents) cselect
adamc@797 672 val coption : unit -> tag [Value = string, Selected = bool] cselect [] [] []
adamc@601 673
adamc@720 674 (*** Tables *)
adamc@720 675
adamc@892 676 val tabl : other ::: {Unit} -> [other ~ [Body, Table]] => unit
adamc@892 677 -> tag ([Border = int] ++ boxEvents)
adamc@892 678 ([Body] ++ other) ([Body, Table] ++ other) [] []
adamc@892 679 val tr : other ::: {Unit} -> [other ~ [Body, Table, Tr]] => unit
adamc@892 680 -> tag tableEvents
adamc@892 681 ([Body, Table] ++ other) ([Body, Tr] ++ other) [] []
adamc@892 682 val th : other ::: {Unit} -> [other ~ [Body, Tr]] => unit
adamc@892 683 -> tag tableEvents
adamc@892 684 ([Body, Tr] ++ other) ([Body] ++ other) [] []
adamc@892 685 val td : other ::: {Unit} -> [other ~ [Body, Tr]] => unit
adamc@892 686 -> tag tableEvents
adamc@892 687 ([Body, Tr] ++ other) ([Body] ++ other) [] []
adamc@720 688
adamc@283 689
adamc@283 690 (** Aborting *)
adamc@283 691
adamc@726 692 val error : t ::: Type -> xbody -> t
adamc@720 693
adamc@729 694 (* Client-side-only handlers: *)
adamc@726 695 val onError : (xbody -> transaction unit) -> transaction unit
adamc@728 696 val onFail : (string -> transaction unit) -> transaction unit
adamc@729 697 val onConnectFail : transaction unit -> transaction unit
adamc@729 698 val onDisconnect : transaction unit -> transaction unit
adamc@729 699 val onServerError : (string -> transaction unit) -> transaction unit
adamc@727 700
adamc@727 701 val show_xml : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> show (xml ctx use bind)