Mercurial > urweb

annotate lib/ur/basis.urs @ 1839:d8c260bcc1f9

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