Mercurial > urweb

annotate lib/ur/basis.urs @ 1642:c3627f317bfd

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