Mercurial > urweb

annotate lib/ur/basis.urs @ 1775:6bc2a8cb3a67

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