Mercurial > urweb

annotate lib/ur/basis.urs @ 1651:dfc854e478bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Error messages about applying 'dynClass' to tags that don't like it
author Adam Chlipala <adam@chlipala.net>
date Sat, 31 Dec 2011 13:31:00 -0500
parents b0720700c36e
children ac141fbb313a
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
adam@1388 84 val strlenGe : string -> int -> bool
adamc@283 85 val strcat : string -> string -> string
adamc@821 86 val strsub : string -> int -> char
adamc@821 87 val strsuffix : string -> int -> string
adamc@829 88 val strchr : string -> char -> option string
adamc@829 89 val strindex : string -> char -> option int
adam@1390 90 val strsindex : string -> string -> option int
adamc@1272 91 val strcspn : string -> string -> int
adamc@829 92 val substring : string -> int -> int -> string
adamc@1023 93 val str1 : char -> string
adamc@283 94
adamc@286 95 class show
adamc@286 96 val show : t ::: Type -> show t -> t -> string
adamc@286 97 val show_int : show int
adamc@286 98 val show_float : show float
adamc@286 99 val show_string : show string
adamc@821 100 val show_char : show char
adamc@286 101 val show_bool : show bool
adamc@436 102 val show_time : show time
adamc@452 103 val mkShow : t ::: Type -> (t -> string) -> show t
adamc@286 104
adamc@290 105 class read
adamc@290 106 val read : t ::: Type -> read t -> string -> option t
adamc@292 107 val readError : t ::: Type -> read t -> string -> t
adamc@292 108 (* [readError] calls [error] if the input is malformed. *)
adamc@290 109 val read_int : read int
adamc@290 110 val read_float : read float
adamc@290 111 val read_string : read string
adamc@821 112 val read_char : read char
adamc@290 113 val read_bool : read bool
adamc@436 114 val read_time : read time
adamc@777 115 val mkRead : t ::: Type -> (string -> t) -> (string -> option t) -> read t
adamc@288 116
adamc@283 117
adamc@564 118 (** * Monads *)
adamc@564 119
adamc@711 120 class monad :: (Type -> Type) -> Type
adamc@564 121 val return : m ::: (Type -> Type) -> t ::: Type
adamc@564 122 -> monad m
adamc@564 123 -> t -> m t
adamc@564 124 val bind : m ::: (Type -> Type) -> t1 ::: Type -> t2 ::: Type
adamc@564 125 -> monad m
adamc@564 126 -> m t1 -> (t1 -> m t2)
adamc@564 127 -> m t2
adamc@564 128
adam@1544 129 val mkMonad : m ::: (Type -> Type)
adam@1544 130 -> {Return : t ::: Type -> t -> m t,
adam@1544 131 Bind : t1 ::: Type -> t2 ::: Type -> m t1 -> (t1 -> m t2) -> m t2}
adam@1544 132 -> monad m
adam@1544 133
adamc@456 134 con transaction :: Type -> Type
adamc@564 135 val transaction_monad : monad transaction
adamc@456 136
adamc@565 137 con source :: Type -> Type
adamc@565 138 val source : t ::: Type -> t -> transaction (source t)
adamc@575 139 val set : t ::: Type -> source t -> t -> transaction unit
adamc@601 140 val get : t ::: Type -> source t -> transaction t
adamc@565 141
adamc@565 142 con signal :: Type -> Type
adamc@565 143 val signal_monad : monad signal
adamc@565 144 val signal : t ::: Type -> source t -> signal t
adamc@841 145 val current : t ::: Type -> signal t -> transaction t
adamc@456 146
adamc@456 147
adam@1571 148 (** * Floats *)
adam@1571 149
adam@1571 150 val float : int -> float
adam@1571 151 val ceil : float -> int
adam@1571 152 val trunc : float -> int
adam@1571 153 val round : float -> int
adam@1571 154
adam@1571 155
adamc@1006 156 (** * Time *)
adamc@1006 157
adamc@1006 158 val now : transaction time
adamc@1050 159 val minTime : time
adam@1369 160 val addSeconds : time -> int -> time
adam@1514 161 val toSeconds : time -> int
adam@1514 162 val diffInSeconds : time -> time -> int
adam@1514 163 (* Earlier time first *)
adam@1359 164 val timef : string -> time -> string (* Uses strftime() format string *)
adam@1372 165 val readUtc : string -> option time
adamc@1006 166
adamc@1006 167
adam@1360 168 (** * Encryption *)
adam@1360 169
adam@1360 170 val crypt : string -> string -> string
adam@1360 171
adam@1360 172
adamc@456 173 (** HTTP operations *)
adamc@456 174
adamc@459 175 con http_cookie :: Type -> Type
adamc@459 176 val getCookie : t ::: Type -> http_cookie t -> transaction (option t)
adamc@1050 177 val setCookie : t ::: Type -> http_cookie t -> {Value : t,
adamc@1050 178 Expires : option time,
adamc@1050 179 Secure : bool} -> transaction unit
adamc@1050 180 val clearCookie : t ::: Type -> http_cookie t -> transaction unit
adamc@459 181
adam@1465 182 type requestHeader
adam@1465 183 val blessRequestHeader : string -> requestHeader
adam@1465 184 val checkRequestHeader : string -> option requestHeader
adam@1465 185 val getHeader : requestHeader -> transaction (option string)
adam@1465 186
adam@1465 187 type responseHeader
adam@1465 188 val blessResponseHeader : string -> responseHeader
adam@1465 189 val checkResponseHeader : string -> option responseHeader
adam@1465 190 val setHeader : responseHeader -> string -> transaction unit
adam@1465 191
adamc@456 192
adamc@566 193 (** JavaScript-y gadgets *)
adamc@566 194
adamc@566 195 val alert : string -> transaction unit
adam@1290 196 val confirm : string -> transaction bool
adamc@694 197 val spawn : transaction unit -> transaction unit
adamc@695 198 val sleep : int -> transaction unit
adamc@566 199
adamc@908 200 val rpc : t ::: Type -> transaction t -> transaction t
adamc@908 201
adamc@566 202
adamc@678 203 (** Channels *)
adamc@678 204
adamc@678 205 con channel :: Type -> Type
adamc@678 206 val channel : t ::: Type -> transaction (channel t)
adamc@678 207 val send : t ::: Type -> channel t -> t -> transaction unit
adamc@678 208 val recv : t ::: Type -> channel t -> transaction t
adamc@678 209
adamc@682 210 type client
adamc@682 211 val self : transaction client
adamc@682 212
adamc@678 213
adamc@203 214 (** SQL *)
adamc@203 215
adamc@705 216 con sql_table :: {Type} -> {{Unit}} -> Type
adamc@753 217 con sql_view :: {Type} -> Type
adamc@753 218
adamc@753 219 class fieldsOf :: Type -> {Type} -> Type
adamc@753 220 val fieldsOf_table : fs ::: {Type} -> keys ::: {{Unit}}
adamc@753 221 -> fieldsOf (sql_table fs keys) fs
adamc@753 222 val fieldsOf_view : fs ::: {Type}
adamc@753 223 -> fieldsOf (sql_view fs) fs
adamc@203 224
adamc@704 225 (*** Constraints *)
adamc@704 226
adamc@707 227 (**** Primary keys *)
adamc@707 228
adamc@707 229 class sql_injectable_prim
adamc@707 230 val sql_bool : sql_injectable_prim bool
adamc@707 231 val sql_int : sql_injectable_prim int
adamc@707 232 val sql_float : sql_injectable_prim float
adamc@707 233 val sql_string : sql_injectable_prim string
adamc@1011 234 val sql_char : sql_injectable_prim char
adamc@707 235 val sql_time : sql_injectable_prim time
adamc@737 236 val sql_blob : sql_injectable_prim blob
adamc@707 237 val sql_channel : t ::: Type -> sql_injectable_prim (channel t)
adamc@707 238 val sql_client : sql_injectable_prim client
adamc@707 239
adamc@1104 240 con serialized :: Type -> Type
adamc@1104 241 val serialize : t ::: Type -> t -> serialized t
adamc@1104 242 val deserialize : t ::: Type -> serialized t -> t
adamc@1104 243 val sql_serialized : t ::: Type -> sql_injectable_prim (serialized t)
adamc@1104 244
adamc@707 245 con primary_key :: {Type} -> {{Unit}} -> Type
adamc@707 246 val no_primary_key : fs ::: {Type} -> primary_key fs []
adamc@707 247 val primary_key : rest ::: {Type} -> t ::: Type -> key1 :: Name -> keys :: {Type}
adamc@707 248 -> [[key1] ~ keys] => [[key1 = t] ++ keys ~ rest]
adamc@707 249 => $([key1 = sql_injectable_prim t] ++ map sql_injectable_prim keys)
adamc@707 250 -> primary_key ([key1 = t] ++ keys ++ rest)
adamc@707 251 [Pkey = [key1] ++ map (fn _ => ()) keys]
adamc@707 252
adamc@707 253 (**** Other constraints *)
adamc@707 254
adamc@705 255 con sql_constraints :: {Type} -> {{Unit}} -> Type
adamc@705 256 (* Arguments: column types, uniqueness implications of constraints *)
adamc@704 257
adamc@705 258 con sql_constraint :: {Type} -> {Unit} -> Type
adamc@704 259
adamc@705 260 val no_constraint : fs ::: {Type} -> sql_constraints fs []
adamc@705 261 val one_constraint : fs ::: {Type} -> unique ::: {Unit} -> name :: Name
adamc@705 262 -> sql_constraint fs unique
adamc@705 263 -> sql_constraints fs [name = unique]
adamc@705 264 val join_constraints : fs ::: {Type}
adamc@705 265 -> uniques1 ::: {{Unit}} -> uniques2 ::: {{Unit}} -> [uniques1 ~ uniques2]
adamc@705 266 => sql_constraints fs uniques1 -> sql_constraints fs uniques2
adamc@705 267 -> sql_constraints fs (uniques1 ++ uniques2)
adamc@705 268
adamc@709 269
adamc@705 270 val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type}
adamc@705 271 -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest]
adamc@705 272 => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique)
adamc@704 273
adamc@712 274 class linkable :: Type -> Type -> Type
adamc@712 275 val linkable_same : t ::: Type -> linkable t t
adamc@712 276 val linkable_from_nullable : t ::: Type -> linkable (option t) t
adamc@712 277 val linkable_to_nullable : t ::: Type -> linkable t (option t)
adamc@712 278
adamc@709 279 con matching :: {Type} -> {Type} -> Type
adamc@709 280 val mat_nil : matching [] []
adamc@712 281 val mat_cons : t1 ::: Type -> rest1 ::: {Type} -> t2 ::: Type -> rest2 ::: {Type}
adamc@709 282 -> nm1 :: Name -> nm2 :: Name
adamc@709 283 -> [[nm1] ~ rest1] => [[nm2] ~ rest2]
adamc@712 284 => linkable t1 t2
adamc@712 285 -> matching rest1 rest2
adamc@712 286 -> matching ([nm1 = t1] ++ rest1) ([nm2 = t2] ++ rest2)
adamc@709 287
adamc@709 288 con propagation_mode :: {Type} -> Type
adamc@709 289 val restrict : fs ::: {Type} -> propagation_mode fs
adamc@709 290 val cascade : fs ::: {Type} -> propagation_mode fs
adamc@709 291 val no_action : fs ::: {Type} -> propagation_mode fs
adamc@709 292 val set_null : fs ::: {Type} -> propagation_mode (map option fs)
adamc@709 293
adamc@709 294
adamc@709 295 val foreign_key : mine1 ::: Name -> t ::: Type -> mine ::: {Type} -> munused ::: {Type}
adamc@709 296 -> foreign ::: {Type} -> funused ::: {Type}
adamc@709 297 -> nm ::: Name -> uniques ::: {{Unit}}
adamc@709 298 -> [[mine1] ~ mine] => [[mine1 = t] ++ mine ~ munused]
adamc@709 299 => [foreign ~ funused] => [[nm] ~ uniques]
adamc@709 300 => matching ([mine1 = t] ++ mine) foreign
adamc@709 301 -> sql_table (foreign ++ funused) ([nm = map (fn _ => ()) foreign] ++ uniques)
adamc@709 302 -> {OnDelete : propagation_mode ([mine1 = t] ++ mine),
adamc@709 303 OnUpdate : propagation_mode ([mine1 = t] ++ mine)}
adamc@709 304 -> sql_constraint ([mine1 = t] ++ mine ++ munused) []
adamc@709 305
adamc@714 306 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
adamc@1072 307 val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
adamc@1072 308 -> fs' ::: {{Type}} -> agg' ::: {{Type}} -> exps' ::: {Type}
adamc@1072 309 -> [fs ~ fs'] => [agg ~ agg'] => [exps ~ exps'] =>
adamc@1072 310 sql_exp fs agg exps t
adamc@1072 311 -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') t
adamc@714 312
adamc@714 313 val check : fs ::: {Type}
adamc@714 314 -> sql_exp [] [] fs bool
adamc@714 315 -> sql_constraint fs []
adamc@714 316
adamc@714 317
adamc@204 318 (*** Queries *)
adamc@204 319
adam@1394 320 con sql_query :: {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
adam@1394 321 con sql_query1 :: {{Type}} -> {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
adamc@204 322
adamc@223 323 con sql_subset :: {{Type}} -> {{Type}} -> Type
adamc@223 324 val sql_subset : keep_drop :: {({Type} * {Type})}
adamc@354 325 -> sql_subset
adamc@621 326 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop)
adamc@621 327 (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop)
adamc@354 328 val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables
adamc@1072 329 val sql_subset_concat : big1 ::: {{Type}} -> little1 ::: {{Type}}
adamc@1072 330 -> big2 ::: {{Type}} -> little2 ::: {{Type}}
adamc@1072 331 -> [big1 ~ big2] => [little1 ~ little2] =>
adamc@1072 332 sql_subset big1 little1
adamc@1072 333 -> sql_subset big2 little2
adamc@1072 334 -> sql_subset (big1 ++ big2) (little1 ++ little2)
adamc@223 335
adamc@1191 336 con sql_from_items :: {{Type}} -> {{Type}} -> Type
adamc@748 337
adamc@1195 338 val sql_from_nil : free ::: {{Type}} -> sql_from_items free []
adamc@1191 339 val sql_from_table : free ::: {{Type}} -> t ::: Type -> fs ::: {Type}
adamc@753 340 -> fieldsOf t fs -> name :: Name
adamc@1191 341 -> t -> sql_from_items free [name = fs]
adamc@1192 342 val sql_from_query : free ::: {{Type}} -> fs ::: {Type} -> name :: Name
adam@1394 343 -> sql_query free [] [] fs
adamc@1192 344 -> sql_from_items free [name = fs]
adamc@1191 345 val sql_from_comma : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
adamc@748 346 -> [tabs1 ~ tabs2]
adamc@1191 347 => sql_from_items free tabs1 -> sql_from_items free tabs2
adamc@1191 348 -> sql_from_items free (tabs1 ++ tabs2)
adamc@1191 349 val sql_inner_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
adamc@1191 350 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
adamc@1191 351 => sql_from_items free tabs1 -> sql_from_items free tabs2
adamc@1191 352 -> sql_exp (free ++ tabs1 ++ tabs2) [] [] bool
adamc@1191 353 -> sql_from_items free (tabs1 ++ tabs2)
adamc@748 354
adamc@750 355 class nullify :: Type -> Type -> Type
adamc@750 356 val nullify_option : t ::: Type -> nullify (option t) (option t)
adamc@750 357 val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t)
adamc@750 358
adamc@1191 359 val sql_left_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}}
adamc@1191 360 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
adamc@750 361 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2)
adamc@1191 362 -> sql_from_items free tabs1 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
adamc@1191 363 -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool
adamc@1191 364 -> sql_from_items free (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
adamc@750 365
adamc@1191 366 val sql_right_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}}
adamc@1191 367 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
adamc@751 368 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1)
adamc@1191 369 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items free tabs2
adamc@1191 370 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool
adamc@1191 371 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
adamc@751 372
adamc@1191 373 val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
adamc@1191 374 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
adamc@751 375 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2))
adamc@1191 376 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1)
adamc@1191 377 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
adamc@1191 378 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool
adamc@1191 379 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
adamc@751 380
adamc@1191 381 val sql_query1 : free ::: {{Type}}
adam@1394 382 -> afree ::: {{Type}}
adamc@1191 383 -> tables ::: {{Type}}
adamc@354 384 -> grouped ::: {{Type}}
adamc@354 385 -> selectedFields ::: {{Type}}
adamc@354 386 -> selectedExps ::: {Type}
adamc@1070 387 -> empties :: {Unit}
adamc@1191 388 -> [free ~ tables]
adamc@1191 389 => [free ~ grouped]
adam@1394 390 => [afree ~ tables]
adamc@1191 391 => [empties ~ selectedFields]
adamc@1070 392 => {Distinct : bool,
adamc@1191 393 From : sql_from_items free tables,
adam@1394 394 Where : sql_exp (free ++ tables) afree [] bool,
adamc@748 395 GroupBy : sql_subset tables grouped,
adam@1394 396 Having : sql_exp (free ++ grouped) (afree ++ tables) [] bool,
adamc@1070 397 SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields),
adam@1394 398 SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) [])
adamc@705 399 selectedExps) }
adam@1394 400 -> sql_query1 free afree tables selectedFields selectedExps
adamc@229 401
adamc@229 402 type sql_relop
adamc@229 403 val sql_union : sql_relop
adamc@229 404 val sql_intersect : sql_relop
adamc@229 405 val sql_except : sql_relop
adamc@1191 406 val sql_relop : free ::: {{Type}}
adam@1394 407 -> afree ::: {{Type}}
adamc@1191 408 -> tables1 ::: {{Type}}
adamc@354 409 -> tables2 ::: {{Type}}
adamc@354 410 -> selectedFields ::: {{Type}}
adamc@354 411 -> selectedExps ::: {Type}
adamc@354 412 -> sql_relop
adam@1427 413 -> bool (* ALL *)
adam@1394 414 -> sql_query1 free afree tables1 selectedFields selectedExps
adam@1394 415 -> sql_query1 free afree tables2 selectedFields selectedExps
adam@1394 416 -> sql_query1 free afree [] selectedFields selectedExps
adam@1394 417 val sql_forget_tables : free ::: {{Type}} -> afree ::: {{Type}} -> tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type}
adam@1394 418 -> sql_query1 free afree tables selectedFields selectedExps
adam@1394 419 -> sql_query1 free afree [] selectedFields selectedExps
adamc@229 420
adamc@230 421 type sql_direction
adamc@230 422 val sql_asc : sql_direction
adamc@230 423 val sql_desc : sql_direction
adamc@230 424
adamc@234 425 con sql_order_by :: {{Type}} -> {Type} -> Type
adamc@234 426 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
adamc@234 427 val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
adamc@354 428 -> sql_exp tables [] exps t -> sql_direction
adamc@354 429 -> sql_order_by tables exps
adamc@354 430 -> sql_order_by tables exps
adamc@230 431
adamc@231 432 type sql_limit
adamc@231 433 val sql_no_limit : sql_limit
adamc@231 434 val sql_limit : int -> sql_limit
adamc@354 435
adamc@232 436 type sql_offset
adamc@232 437 val sql_no_offset : sql_offset
adamc@232 438 val sql_offset : int -> sql_offset
adamc@232 439
adamc@1191 440 val sql_query : free ::: {{Type}}
adam@1394 441 -> afree ::: {{Type}}
adamc@1191 442 -> tables ::: {{Type}}
adamc@354 443 -> selectedFields ::: {{Type}}
adamc@354 444 -> selectedExps ::: {Type}
adamc@1191 445 -> [free ~ tables]
adam@1394 446 => {Rows : sql_query1 free afree tables selectedFields selectedExps,
adamc@1191 447 OrderBy : sql_order_by (free ++ tables) selectedExps,
adamc@354 448 Limit : sql_limit,
adamc@354 449 Offset : sql_offset}
adam@1394 450 -> sql_query free afree selectedFields selectedExps
adamc@204 451
adamc@354 452 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
adamc@354 453 -> fieldType ::: Type -> agg ::: {{Type}}
adamc@354 454 -> exps ::: {Type}
adamc@354 455 -> tab :: Name -> field :: Name
adamc@354 456 -> sql_exp
adamc@354 457 ([tab = [field = fieldType] ++ otherFields] ++ otherTabs)
adamc@354 458 agg exps fieldType
adamc@234 459
adamc@354 460 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type}
adamc@354 461 -> nm :: Name
adamc@354 462 -> sql_exp tabs agg ([nm = t] ++ rest) t
adamc@209 463
adamc@221 464 class sql_injectable
adamc@676 465 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t
adamc@676 466 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)
adamc@676 467
adamc@354 468 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 469 -> t ::: Type
adamc@354 470 -> sql_injectable t -> t -> sql_exp tables agg exps t
adamc@209 471
adamc@470 472 val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 473 -> t ::: Type
adamc@470 474 -> sql_exp tables agg exps (option t)
adamc@470 475 -> sql_exp tables agg exps bool
adamc@470 476
adam@1602 477 val sql_coalesce : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adam@1602 478 -> t ::: Type
adam@1602 479 -> sql_exp tables agg exps (option t)
adam@1602 480 -> sql_exp tables agg exps t
adam@1602 481 -> sql_exp tables agg exps t
adam@1602 482
kkallio@1572 483 val sql_if_then_else : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
kkallio@1572 484 -> t ::: Type
kkallio@1572 485 -> sql_exp tables agg exps bool
kkallio@1572 486 -> sql_exp tables agg exps t
kkallio@1572 487 -> sql_exp tables agg exps t
kkallio@1572 488 -> sql_exp tables agg exps t
kkallio@1572 489
adamc@559 490 class sql_arith
adam@1427 491 val sql_arith_int : sql_arith int
adam@1427 492 val sql_arith_float : sql_arith float
adam@1427 493 val sql_arith_option : t ::: Type -> sql_arith t -> sql_arith (option t)
adamc@559 494
adamc@220 495 con sql_unary :: Type -> Type -> Type
adamc@220 496 val sql_not : sql_unary bool bool
adamc@354 497 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 498 -> arg ::: Type -> res ::: Type
adamc@354 499 -> sql_unary arg res -> sql_exp tables agg exps arg
adamc@354 500 -> sql_exp tables agg exps res
adamc@220 501
adamc@559 502 val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t
adamc@559 503
adamc@220 504 con sql_binary :: Type -> Type -> Type -> Type
adamc@220 505 val sql_and : sql_binary bool bool bool
adamc@220 506 val sql_or : sql_binary bool bool bool
adamc@234 507 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 508 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
adamc@354 509 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1
adamc@354 510 -> sql_exp tables agg exps arg2
adamc@354 511 -> sql_exp tables agg exps res
adamc@220 512
adamc@559 513 val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 514 val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 515 val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 516 val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 517 val sql_mod : sql_binary int int int
adamc@559 518
adamc@559 519 val sql_eq : t ::: Type -> sql_binary t t bool
adamc@559 520 val sql_ne : t ::: Type -> sql_binary t t bool
adamc@559 521 val sql_lt : t ::: Type -> sql_binary t t bool
adamc@559 522 val sql_le : t ::: Type -> sql_binary t t bool
adamc@559 523 val sql_gt : t ::: Type -> sql_binary t t bool
adamc@559 524 val sql_ge : t ::: Type -> sql_binary t t bool
adamc@203 525
kkallio@1607 526 val sql_like : sql_binary string string bool
kkallio@1607 527
adamc@235 528 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@544 529 -> sql_exp tables agg exps int
adamc@235 530
adamc@1187 531 con sql_aggregate :: Type -> Type -> Type
adamc@354 532 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@1187 533 -> dom ::: Type -> ran ::: Type
adamc@1187 534 -> sql_aggregate dom ran -> sql_exp agg agg exps dom
adamc@1187 535 -> sql_exp tables agg exps ran
adamc@1187 536
adamc@1187 537 val sql_count_col : t ::: Type -> sql_aggregate (option t) int
adamc@236 538
adamc@236 539 class sql_summable
adamc@236 540 val sql_summable_int : sql_summable int
adamc@236 541 val sql_summable_float : sql_summable float
adam@1357 542 val sql_summable_option : t ::: Type -> sql_summable t -> sql_summable (option t)
adam@1394 543 val sql_avg : t ::: Type -> nt ::: Type -> sql_summable t -> nullify t nt -> sql_aggregate t nt
adam@1394 544 val sql_sum : t ::: Type -> nt ::: Type -> sql_summable t -> nullify t nt -> sql_aggregate t nt
adamc@236 545
adamc@236 546 class sql_maxable
adamc@236 547 val sql_maxable_int : sql_maxable int
adamc@236 548 val sql_maxable_float : sql_maxable float
adamc@236 549 val sql_maxable_string : sql_maxable string
adamc@437 550 val sql_maxable_time : sql_maxable time
adam@1357 551 val sql_maxable_option : t ::: Type -> sql_maxable t -> sql_maxable (option t)
adam@1394 552 val sql_max : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
adam@1394 553 val sql_min : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
adamc@236 554
adamc@441 555 con sql_nfunc :: Type -> Type
adamc@441 556 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@441 557 -> t ::: Type
adamc@441 558 -> sql_nfunc t -> sql_exp tables agg exps t
adamc@441 559 val sql_current_timestamp : sql_nfunc time
adamc@441 560
adamc@746 561 con sql_ufunc :: Type -> Type -> Type
adamc@746 562 val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@746 563 -> dom ::: Type -> ran ::: Type
adamc@746 564 -> sql_ufunc dom ran -> sql_exp tables agg exps dom
adamc@746 565 -> sql_exp tables agg exps ran
adamc@746 566 val sql_octet_length : sql_ufunc blob int
adamc@1207 567 val sql_known : t ::: Type -> sql_ufunc t bool
adam@1636 568 val sql_lower : sql_ufunc string string
adam@1636 569 val sql_upper : sql_ufunc string string
adamc@235 570
adamc@1081 571 val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
adamc@1081 572 -> sql_injectable_prim t
adamc@1081 573 -> sql_exp tables agg exps t
adamc@1081 574 -> sql_exp tables agg exps (option t)
adamc@1081 575
adam@1421 576 val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type -> nt ::: Type
adam@1421 577 -> nullify t nt
adam@1394 578 -> sql_query tables agg [] [nm = t]
adam@1421 579 -> sql_exp tables agg exps nt
adamc@1191 580
adamc@243 581 (*** Executing queries *)
adamc@243 582
adamc@354 583 val query : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 584 -> [tables ~ exps] =>
adamc@354 585 state ::: Type
adam@1394 586 -> sql_query [] [] tables exps
adamc@621 587 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@354 588 -> state
adamc@354 589 -> transaction state)
adamc@354 590 -> state
adamc@354 591 -> transaction state
adamc@243 592
adamc@243 593
adamc@299 594 (*** Database mutators *)
adamc@299 595
adamc@299 596 type dml
adamc@299 597 val dml : dml -> transaction unit
adam@1293 598 val tryDml : dml -> transaction (option string)
adam@1293 599 (* Returns an error message on failure. *)
adamc@299 600
adamc@705 601 val insert : fields ::: {Type} -> uniques ::: {{Unit}}
adamc@705 602 -> sql_table fields uniques
adamc@621 603 -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
adamc@354 604 -> dml
adamc@299 605
adamc@705 606 val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} ->
adamc@629 607 [changed ~ unchanged] =>
adamc@621 608 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
adamc@705 609 -> sql_table (changed ++ unchanged) uniques
adamc@354 610 -> sql_exp [T = changed ++ unchanged] [] [] bool
adamc@354 611 -> dml
adamc@299 612
adamc@705 613 val delete : fields ::: {Type} -> uniques ::: {{Unit}}
adamc@705 614 -> sql_table fields uniques
adamc@354 615 -> sql_exp [T = fields] [] [] bool
adamc@354 616 -> dml
adamc@299 617
adamc@338 618 (*** Sequences *)
adamc@338 619
adamc@338 620 type sql_sequence
adamc@338 621 val nextval : sql_sequence -> transaction int
adamc@1073 622 val setval : sql_sequence -> int -> transaction unit
adamc@338 623
adamc@299 624
adamc@203 625 (** XML *)
adamc@203 626
adamc@721 627 type css_class
adam@1477 628 val show_css_class : show css_class
adam@1567 629 val null : css_class
adam@1567 630 (* No special formatting *)
adam@1292 631 val classes : css_class -> css_class -> css_class
adam@1292 632 (* The equivalent of writing one class after the other, separated by a space, in
adam@1292 633 * an HTML 'class' attribute *)
adamc@718 634
adamc@720 635 con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
adamc@91 636
adamc@720 637 con xml :: {Unit} -> {Type} -> {Type} -> Type
adamc@720 638 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
adam@1358 639 val cdataChar : ctx ::: {Unit} -> use ::: {Type} -> char -> xml ctx use []
adamc@354 640 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type}
adamc@354 641 -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
adamc@354 642 -> useOuter ::: {Type} -> useInner ::: {Type}
adamc@354 643 -> bindOuter ::: {Type} -> bindInner ::: {Type}
adamc@629 644 -> [attrsGiven ~ attrsAbsent] =>
adamc@629 645 [useOuter ~ useInner] =>
adamc@629 646 [bindOuter ~ bindInner] =>
adamc@721 647 option css_class
adam@1643 648 -> option (signal css_class)
adamc@721 649 -> $attrsGiven
adamc@629 650 -> tag (attrsGiven ++ attrsAbsent)
adamc@720 651 ctxOuter ctxInner useOuter bindOuter
adamc@720 652 -> xml ctxInner useInner bindInner
adamc@720 653 -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
adamc@140 654 val join : ctx ::: {Unit}
adamc@720 655 -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
adamc@720 656 -> [use1 ~ bind1] => [bind1 ~ bind2] =>
adamc@720 657 xml ctx use1 bind1
adamc@720 658 -> xml ctx (use1 ++ bind1) bind2
adamc@720 659 -> xml ctx use1 (bind1 ++ bind2)
adamc@354 660 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type}
adamc@720 661 -> bind ::: {Type}
adamc@629 662 -> [use1 ~ use2] =>
adamc@720 663 xml ctx use1 bind
adamc@720 664 -> xml ctx (use1 ++ use2) bind
adamc@91 665
adam@1641 666 con html = [Html]
adam@1641 667 con head = [Head]
adam@1642 668
adam@1642 669 con body' = [MakeForm, Body]
adam@1642 670 con form' = [Body, Form]
adam@1642 671 con subform' = [Body, Subform]
adam@1642 672 con tabl' = [MakeForm, Table]
adam@1642 673 con tr' = [MakeForm, Tr]
adam@1642 674
adam@1642 675 con body = [Dyn] ++ body'
adam@1642 676 con form = [Dyn] ++ form'
adam@1642 677 con subform = [Dyn] ++ subform'
adam@1642 678 con tabl = [Dyn] ++ tabl'
adam@1642 679 con tr = [Dyn] ++ tr'
adam@1641 680
adam@1641 681 con xhtml = xml html
adamc@139 682 con page = xhtml [] []
adam@1641 683 con xbody = xml body [] []
adam@1641 684 con xtable = xml tabl [] []
adam@1641 685 con xtr = xml tr [] []
adam@1641 686 con xform = xml form [] []
adamc@110 687
adamc@718 688
adamc@204 689 (*** HTML details *)
adamc@204 690
adam@1370 691 type queryString
adam@1370 692 val show_queryString : show queryString
adam@1370 693
adamc@724 694 type url
adamc@1065 695 val show_url : show url
adamc@724 696 val bless : string -> url
adamc@770 697 val checkUrl : string -> option url
adamc@1085 698 val currentUrl : transaction url
adam@1386 699 val currentUrlHasPost : transaction bool
adam@1485 700 val currentUrlHasQueryString : transaction bool
adamc@1065 701 val url : transaction page -> url
adam@1370 702 val effectfulUrl : (option queryString -> transaction page) -> url
adamc@1065 703 val redirect : t ::: Type -> url -> transaction t
adamc@724 704
adam@1556 705 type id
adam@1556 706 val fresh : transaction id
adam@1556 707
adam@1641 708 val dyn : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> [ctx ~ [Dyn]] => unit
adam@1641 709 -> tag [Signal = signal (xml ([Dyn] ++ ctx) use bind)] ([Dyn] ++ ctx) [] use bind
adamc@568 710
adamc@720 711 val head : unit -> tag [] html head [] []
adamc@720 712 val title : unit -> tag [] head [] [] []
adam@1556 713 val link : unit -> tag [Id = id, Rel = string, Typ = string, Href = url, Media = string] head [] [] []
adamc@110 714
adamc@892 715 val body : unit -> tag [Onload = transaction unit, Onresize = transaction unit, Onunload = transaction unit]
adamc@892 716 html body [] []
adamc@354 717 con bodyTag = fn (attrs :: {Type}) =>
adamc@354 718 ctx ::: {Unit} ->
adamc@629 719 [[Body] ~ ctx] =>
adamc@720 720 unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
adamc@354 721 con bodyTagStandalone = fn (attrs :: {Type}) =>
adamc@354 722 ctx ::: {Unit}
adamc@629 723 -> [[Body] ~ ctx] =>
adamc@720 724 unit -> tag attrs ([Body] ++ ctx) [] [] []
adamc@141 725
adam@1556 726 val br : bodyTagStandalone [Id = id]
adamc@119 727
adamc@892 728 con focusEvents = [Onblur = transaction unit, Onfocus = transaction unit]
adamc@892 729 con mouseEvents = [Onclick = transaction unit, Ondblclick = transaction unit,
adamc@892 730 Onmousedown = transaction unit, Onmousemove = transaction unit,
adamc@892 731 Onmouseout = transaction unit, Onmouseover = transaction unit,
adamc@894 732 Onmouseup = transaction unit]
adamc@895 733 con keyEvents = [Onkeydown = int -> transaction unit, Onkeypress = int -> transaction unit,
adamc@895 734 Onkeyup = int -> transaction unit]
adamc@895 735 (* Key arguments are character codes. *)
adamc@892 736 con resizeEvents = [Onresize = transaction unit]
adamc@691 737
adamc@892 738 con boxEvents = focusEvents ++ mouseEvents ++ keyEvents ++ resizeEvents
adamc@892 739 con tableEvents = focusEvents ++ mouseEvents ++ keyEvents
adamc@140 740
adam@1556 741 con boxAttrs = [Id = id, Title = string] ++ boxEvents
adam@1556 742 con tableAttrs = [Id = id, Title = string] ++ tableEvents
adamc@469 743
adamc@1047 744 val span : bodyTag boxAttrs
adamc@1047 745 val div : bodyTag boxAttrs
adamc@140 746
adamc@1047 747 val p : bodyTag boxAttrs
adamc@1047 748 val b : bodyTag boxAttrs
adamc@1047 749 val i : bodyTag boxAttrs
adamc@1047 750 val tt : bodyTag boxAttrs
kkallio@1452 751 val sub : bodyTag boxAttrs
kkallio@1452 752 val sup : bodyTag boxAttrs
adamc@410 753
adamc@1047 754 val h1 : bodyTag boxAttrs
adamc@1047 755 val h2 : bodyTag boxAttrs
adamc@1047 756 val h3 : bodyTag boxAttrs
adamc@1047 757 val h4 : bodyTag boxAttrs
adamc@1047 758 val h5 : bodyTag boxAttrs
adamc@1047 759 val h6 : bodyTag boxAttrs
adamc@717 760
adamc@1047 761 val li : bodyTag boxAttrs
adamc@1047 762 val ol : bodyTag boxAttrs
adamc@1047 763 val ul : bodyTag boxAttrs
adamc@140 764
adamc@1047 765 val hr : bodyTag boxAttrs
adamc@1047 766
vshabanoff@1560 767 val a : bodyTag ([Link = transaction page, Href = url, Target = string] ++ boxAttrs)
adamc@892 768
adam@1419 769 val img : bodyTag ([Alt = string, Src = url, Width = int, Height = int,
adamc@1129 770 Onabort = transaction unit, Onerror = transaction unit,
adamc@1047 771 Onload = transaction unit] ++ boxAttrs)
adamc@892 772
adamc@720 773 val form : ctx ::: {Unit} -> bind ::: {Type}
adam@1642 774 -> [[MakeForm, Form] ~ ctx] =>
adam@1412 775 option css_class
adam@1642 776 -> xml ([Form] ++ ctx) [] bind
adam@1642 777 -> xml ([MakeForm] ++ ctx) [] []
adamc@756 778
adamc@756 779 val subform : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
adamc@756 780 -> [[Form] ~ ctx] =>
adamc@756 781 nm :: Name -> [[nm] ~ use] =>
adamc@1004 782 xml ([Form] ++ ctx) [] bind
adamc@756 783 -> xml ([Form] ++ ctx) use [nm = $bind]
adamc@758 784
adamc@758 785 val subforms : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
adamc@1004 786 -> [[Form, Subform] ~ ctx] =>
adamc@758 787 nm :: Name -> [[nm] ~ use] =>
adamc@1004 788 xml ([Subform] ++ ctx) [Entry = $bind] []
adamc@758 789 -> xml ([Form] ++ ctx) use [nm = list ($bind)]
adamc@758 790
adamc@758 791 val entry : ctx ::: {Unit} -> bind ::: {Type}
adamc@1004 792 -> [[Subform, Form] ~ ctx] =>
adamc@1004 793 xml ([Form] ++ ctx) [] bind
adamc@758 794 -> xml ([Subform] ++ ctx) [Entry = $bind] []
adamc@758 795
adamc@361 796 con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) =>
adamc@354 797 ctx ::: {Unit}
adamc@629 798 -> [[Form] ~ ctx] =>
adamc@354 799 nm :: Name -> unit
adamc@720 800 -> tag attrs ([Form] ++ ctx) inner [] [nm = ty]
adamc@1047 801 val hidden : formTag string [] [Id = string, Value = string]
adamc@892 802 val textbox : formTag string [] ([Value = string, Size = int, Source = source string, Onchange = transaction unit,
adamc@1047 803 Ontext = transaction unit] ++ boxAttrs)
adamc@1047 804 val password : formTag string [] ([Value = string, Size = int] ++ boxAttrs)
adamc@892 805 val textarea : formTag string [] ([Rows = int, Cols = int, Onchange = transaction unit,
adamc@1047 806 Ontext = transaction unit] ++ boxAttrs)
adamc@153 807
adamc@1047 808 val checkbox : formTag bool [] ([Checked = bool] ++ boxAttrs)
adamc@190 809
adamc@737 810 type file
adamc@737 811 val fileName : file -> option string
adamc@740 812 val fileMimeType : file -> string
adamc@737 813 val fileData : file -> blob
adamc@737 814
adamc@1047 815 val upload : formTag file [] ([Value = string, Size = int] ++ boxAttrs)
adamc@737 816
adamc@741 817 type mimeType
adamc@741 818 val blessMime : string -> mimeType
adamc@770 819 val checkMime : string -> option mimeType
adamc@741 820 val returnBlob : t ::: Type -> blob -> mimeType -> transaction t
adamc@745 821 val blobSize : blob -> int
adamc@1119 822 val textBlob : string -> blob
adamc@741 823
adam@1347 824 type postBody
adam@1347 825 val postType : postBody -> string
adam@1347 826 val postData : postBody -> string
adam@1347 827
adamc@153 828 con radio = [Body, Radio]
adam@1556 829 val radio : formTag string radio [Id = id]
adamc@1068 830 val radioOption : unit -> tag ([Value = string, Checked = bool] ++ boxAttrs) radio [] [] []
adamc@142 831
adamc@154 832 con select = [Select]
adamc@1047 833 val select : formTag string select ([Onchange = transaction unit] ++ boxAttrs)
adamc@720 834 val option : unit -> tag [Value = string, Selected = bool] select [] [] []
adamc@154 835
adamc@720 836 val submit : ctx ::: {Unit} -> use ::: {Type}
adamc@629 837 -> [[Form] ~ ctx] =>
adamc@354 838 unit
adamc@1047 839 -> tag ([Value = string, Action = $use -> transaction page] ++ boxAttrs)
adamc@720 840 ([Form] ++ ctx) ([Form] ++ ctx) use []
adamc@283 841
adam@1517 842 val image : ctx ::: {Unit} -> use ::: {Type}
adam@1517 843 -> [[Form] ~ ctx] =>
adam@1517 844 unit
adam@1517 845 -> tag ([Src = url, Width = int, Height = int, Alt = string, Action = $use -> transaction page] ++ boxAttrs)
adam@1517 846 ([Form] ++ ctx) ([Form] ++ ctx) use []
adam@1517 847
adam@1557 848 val label : bodyTag ([For = id, Accesskey = string] ++ tableAttrs)
adamc@1047 849
adamc@1047 850
adamc@601 851 (*** AJAX-oriented widgets *)
adamc@601 852
adamc@797 853 con cformTag = fn (attrs :: {Type}) (inner :: {Unit}) =>
adamc@601 854 ctx ::: {Unit}
adamc@629 855 -> [[Body] ~ ctx] =>
adamc@797 856 unit -> tag attrs ([Body] ++ ctx) inner [] []
adamc@601 857
adamc@892 858 val ctextbox : cformTag ([Value = string, Size = int, Source = source string, Onchange = transaction unit,
adamc@1047 859 Ontext = transaction unit] ++ boxAttrs) []
adamc@1047 860 val button : cformTag ([Value = string] ++ boxAttrs) []
adamc@797 861
adamc@1047 862 val ccheckbox : cformTag ([Value = bool, Size = int, Source = source bool] ++ boxAttrs) []
adamc@817 863
adamc@797 864 con cselect = [Cselect]
adamc@1047 865 val cselect : cformTag ([Source = source string, Onchange = transaction unit] ++ boxAttrs) cselect
adamc@797 866 val coption : unit -> tag [Value = string, Selected = bool] cselect [] [] []
adamc@601 867
adamc@1099 868 val ctextarea : cformTag ([Value = string, Rows = int, Cols = int, Source = source string, Onchange = transaction unit,
adamc@1099 869 Ontext = transaction unit] ++ boxAttrs) []
adamc@1099 870
adamc@720 871 (*** Tables *)
adamc@720 872
adamc@892 873 val tabl : other ::: {Unit} -> [other ~ [Body, Table]] => unit
adamc@1047 874 -> tag ([Border = int] ++ boxAttrs)
adam@1641 875 ([Body] ++ other) ([Table] ++ other) [] []
adam@1641 876 val tr : other ::: {Unit} -> [other ~ [Table, Tr]] => unit
adamc@1047 877 -> tag tableAttrs
adam@1641 878 ([Table] ++ other) ([Tr] ++ other) [] []
adamc@892 879 val th : other ::: {Unit} -> [other ~ [Body, Tr]] => unit
kkallio@1476 880 -> tag ([Colspan = int, Rowspan = int] ++ tableAttrs)
adam@1641 881 ([Tr] ++ other) ([Body] ++ other) [] []
adamc@892 882 val td : other ::: {Unit} -> [other ~ [Body, Tr]] => unit
kkallio@1476 883 -> tag ([Colspan = int, Rowspan = int] ++ tableAttrs)
adam@1641 884 ([Tr] ++ other) ([Body] ++ other) [] []
adamc@720 885
adamc@283 886
adamc@283 887 (** Aborting *)
adamc@283 888
adamc@726 889 val error : t ::: Type -> xbody -> t
adamc@720 890
adamc@729 891 (* Client-side-only handlers: *)
adamc@726 892 val onError : (xbody -> transaction unit) -> transaction unit
adamc@728 893 val onFail : (string -> transaction unit) -> transaction unit
adamc@729 894 val onConnectFail : transaction unit -> transaction unit
adamc@729 895 val onDisconnect : transaction unit -> transaction unit
adamc@729 896 val onServerError : (string -> transaction unit) -> transaction unit
adamc@727 897
adam@1555 898 (* More standard document-level JavaScript handlers *)
adam@1555 899 val onClick : transaction unit -> transaction unit
adam@1555 900 val onDblclick : transaction unit -> transaction unit
adam@1555 901 val onKeydown : (int -> transaction unit) -> transaction unit
adam@1555 902 val onKeypress : (int -> transaction unit) -> transaction unit
adam@1555 903 val onKeyup : (int -> transaction unit) -> transaction unit
adam@1555 904 val onMousedown : transaction unit -> transaction unit
adam@1555 905 val onMouseup : transaction unit -> transaction unit
adam@1555 906
adam@1559 907 (* Prevents default handling of current event *)
adam@1559 908 val preventDefault : transaction unit
adam@1559 909 (* Stops propagation of current event *)
adam@1559 910 val stopPropagation : transaction unit
adam@1559 911
adamc@727 912 val show_xml : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> show (xml ctx use bind)
adamc@1075 913
adamc@1075 914
adamc@1075 915 (** Tasks *)
adamc@1075 916
adam@1348 917 con task_kind :: Type -> Type
adam@1348 918 val initialize : task_kind unit
adam@1348 919 val clientLeaves : task_kind client
adam@1349 920 val periodic : int -> task_kind unit
adamc@1120 921
adamc@1120 922
adamc@1199 923 (** Information flow security *)
adamc@1199 924
adamc@1199 925 type sql_policy
adamc@1199 926
adamc@1214 927 val sendClient : tables ::: {{Type}} -> exps ::: {Type}
adam@1394 928 -> [tables ~ exps] => sql_query [] [] tables exps
adamc@1214 929 -> sql_policy
adamc@1199 930
adamc@1229 931 val sendOwnIds : sql_sequence -> sql_policy
adamc@1229 932
adamc@1220 933 val mayInsert : fs ::: {Type} -> tables ::: {{Type}} -> [[New] ~ tables]
adam@1394 934 => sql_query [] [] ([New = fs] ++ tables) []
adamc@1220 935 -> sql_policy
adamc@1220 936
adamc@1221 937 val mayDelete : fs ::: {Type} -> tables ::: {{Type}} -> [[Old] ~ tables]
adam@1394 938 => sql_query [] [] ([Old = fs] ++ tables) []
adamc@1221 939 -> sql_policy
adamc@1221 940
adamc@1223 941 val mayUpdate : fs ::: {Type} -> tables ::: {{Type}} -> [[Old, New] ~ tables]
adam@1394 942 => sql_query [] [] ([Old = fs, New = fs] ++ tables) []
adamc@1223 943 -> sql_policy
adamc@1223 944
adamc@1240 945 val also : sql_policy -> sql_policy -> sql_policy
adamc@1199 946
adamc@1120 947 val debug : string -> transaction unit
adam@1389 948 val naughtyDebug : string -> int
adamc@1250 949
adamc@1250 950 val rand : transaction int