Mercurial > urweb

annotate lib/ur/basis.urs @ 1591:20f898c29525

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweaks to choices of source positions to use in error messages, including for subSgn
author Adam Chlipala <adam@chlipala.net>
date Sat, 05 Nov 2011 13:12:07 -0400
parents 5530a8075b62
children e44be6ece475
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
kkallio@1572 477 val sql_if_then_else : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
kkallio@1572 478 -> t ::: Type
kkallio@1572 479 -> sql_exp tables agg exps bool
kkallio@1572 480 -> sql_exp tables agg exps t
kkallio@1572 481 -> sql_exp tables agg exps t
kkallio@1572 482 -> sql_exp tables agg exps t
kkallio@1572 483
adamc@559 484 class sql_arith
adam@1427 485 val sql_arith_int : sql_arith int
adam@1427 486 val sql_arith_float : sql_arith float
adam@1427 487 val sql_arith_option : t ::: Type -> sql_arith t -> sql_arith (option t)
adamc@559 488
adamc@220 489 con sql_unary :: Type -> Type -> Type
adamc@220 490 val sql_not : sql_unary bool bool
adamc@354 491 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 492 -> arg ::: Type -> res ::: Type
adamc@354 493 -> sql_unary arg res -> sql_exp tables agg exps arg
adamc@354 494 -> sql_exp tables agg exps res
adamc@220 495
adamc@559 496 val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t
adamc@559 497
adamc@220 498 con sql_binary :: Type -> Type -> Type -> Type
adamc@220 499 val sql_and : sql_binary bool bool bool
adamc@220 500 val sql_or : sql_binary bool bool bool
adamc@234 501 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 502 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
adamc@354 503 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1
adamc@354 504 -> sql_exp tables agg exps arg2
adamc@354 505 -> sql_exp tables agg exps res
adamc@220 506
adamc@559 507 val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 508 val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 509 val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 510 val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 511 val sql_mod : sql_binary int int int
adamc@559 512
adamc@559 513 val sql_eq : t ::: Type -> sql_binary t t bool
adamc@559 514 val sql_ne : t ::: Type -> sql_binary t t bool
adamc@559 515 val sql_lt : t ::: Type -> sql_binary t t bool
adamc@559 516 val sql_le : t ::: Type -> sql_binary t t bool
adamc@559 517 val sql_gt : t ::: Type -> sql_binary t t bool
adamc@559 518 val sql_ge : t ::: Type -> sql_binary t t bool
adamc@203 519
adamc@235 520 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@544 521 -> sql_exp tables agg exps int
adamc@235 522
adamc@1187 523 con sql_aggregate :: Type -> Type -> Type
adamc@354 524 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@1187 525 -> dom ::: Type -> ran ::: Type
adamc@1187 526 -> sql_aggregate dom ran -> sql_exp agg agg exps dom
adamc@1187 527 -> sql_exp tables agg exps ran
adamc@1187 528
adamc@1187 529 val sql_count_col : t ::: Type -> sql_aggregate (option t) int
adamc@236 530
adamc@236 531 class sql_summable
adamc@236 532 val sql_summable_int : sql_summable int
adamc@236 533 val sql_summable_float : sql_summable float
adam@1357 534 val sql_summable_option : t ::: Type -> sql_summable t -> sql_summable (option t)
adam@1394 535 val sql_avg : t ::: Type -> nt ::: Type -> sql_summable t -> nullify t nt -> sql_aggregate t nt
adam@1394 536 val sql_sum : t ::: Type -> nt ::: Type -> sql_summable t -> nullify t nt -> sql_aggregate t nt
adamc@236 537
adamc@236 538 class sql_maxable
adamc@236 539 val sql_maxable_int : sql_maxable int
adamc@236 540 val sql_maxable_float : sql_maxable float
adamc@236 541 val sql_maxable_string : sql_maxable string
adamc@437 542 val sql_maxable_time : sql_maxable time
adam@1357 543 val sql_maxable_option : t ::: Type -> sql_maxable t -> sql_maxable (option t)
adam@1394 544 val sql_max : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
adam@1394 545 val sql_min : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
adamc@236 546
adamc@441 547 con sql_nfunc :: Type -> Type
adamc@441 548 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@441 549 -> t ::: Type
adamc@441 550 -> sql_nfunc t -> sql_exp tables agg exps t
adamc@441 551 val sql_current_timestamp : sql_nfunc time
adamc@441 552
adamc@746 553 con sql_ufunc :: Type -> Type -> Type
adamc@746 554 val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@746 555 -> dom ::: Type -> ran ::: Type
adamc@746 556 -> sql_ufunc dom ran -> sql_exp tables agg exps dom
adamc@746 557 -> sql_exp tables agg exps ran
adamc@746 558 val sql_octet_length : sql_ufunc blob int
adamc@1207 559 val sql_known : t ::: Type -> sql_ufunc t bool
adamc@746 560
adamc@235 561
adamc@1081 562 val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
adamc@1081 563 -> sql_injectable_prim t
adamc@1081 564 -> sql_exp tables agg exps t
adamc@1081 565 -> sql_exp tables agg exps (option t)
adamc@1081 566
adam@1421 567 val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type -> nt ::: Type
adam@1421 568 -> nullify t nt
adam@1394 569 -> sql_query tables agg [] [nm = t]
adam@1421 570 -> sql_exp tables agg exps nt
adamc@1191 571
adamc@243 572 (*** Executing queries *)
adamc@243 573
adamc@354 574 val query : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 575 -> [tables ~ exps] =>
adamc@354 576 state ::: Type
adam@1394 577 -> sql_query [] [] tables exps
adamc@621 578 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@354 579 -> state
adamc@354 580 -> transaction state)
adamc@354 581 -> state
adamc@354 582 -> transaction state
adamc@243 583
adamc@243 584
adamc@299 585 (*** Database mutators *)
adamc@299 586
adamc@299 587 type dml
adamc@299 588 val dml : dml -> transaction unit
adam@1293 589 val tryDml : dml -> transaction (option string)
adam@1293 590 (* Returns an error message on failure. *)
adamc@299 591
adamc@705 592 val insert : fields ::: {Type} -> uniques ::: {{Unit}}
adamc@705 593 -> sql_table fields uniques
adamc@621 594 -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
adamc@354 595 -> dml
adamc@299 596
adamc@705 597 val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} ->
adamc@629 598 [changed ~ unchanged] =>
adamc@621 599 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
adamc@705 600 -> sql_table (changed ++ unchanged) uniques
adamc@354 601 -> sql_exp [T = changed ++ unchanged] [] [] bool
adamc@354 602 -> dml
adamc@299 603
adamc@705 604 val delete : fields ::: {Type} -> uniques ::: {{Unit}}
adamc@705 605 -> sql_table fields uniques
adamc@354 606 -> sql_exp [T = fields] [] [] bool
adamc@354 607 -> dml
adamc@299 608
adamc@338 609 (*** Sequences *)
adamc@338 610
adamc@338 611 type sql_sequence
adamc@338 612 val nextval : sql_sequence -> transaction int
adamc@1073 613 val setval : sql_sequence -> int -> transaction unit
adamc@338 614
adamc@299 615
adamc@203 616 (** XML *)
adamc@203 617
adamc@721 618 type css_class
adam@1477 619 val show_css_class : show css_class
adam@1567 620 val null : css_class
adam@1567 621 (* No special formatting *)
adam@1292 622 val classes : css_class -> css_class -> css_class
adam@1292 623 (* The equivalent of writing one class after the other, separated by a space, in
adam@1292 624 * an HTML 'class' attribute *)
adamc@718 625
adamc@720 626 con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
adamc@91 627
adamc@720 628 con xml :: {Unit} -> {Type} -> {Type} -> Type
adamc@720 629 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
adam@1358 630 val cdataChar : ctx ::: {Unit} -> use ::: {Type} -> char -> xml ctx use []
adamc@354 631 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type}
adamc@354 632 -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
adamc@354 633 -> useOuter ::: {Type} -> useInner ::: {Type}
adamc@354 634 -> bindOuter ::: {Type} -> bindInner ::: {Type}
adamc@629 635 -> [attrsGiven ~ attrsAbsent] =>
adamc@629 636 [useOuter ~ useInner] =>
adamc@629 637 [bindOuter ~ bindInner] =>
adamc@721 638 option css_class
adamc@721 639 -> $attrsGiven
adamc@629 640 -> tag (attrsGiven ++ attrsAbsent)
adamc@720 641 ctxOuter ctxInner useOuter bindOuter
adamc@720 642 -> xml ctxInner useInner bindInner
adamc@720 643 -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
adamc@140 644 val join : ctx ::: {Unit}
adamc@720 645 -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
adamc@720 646 -> [use1 ~ bind1] => [bind1 ~ bind2] =>
adamc@720 647 xml ctx use1 bind1
adamc@720 648 -> xml ctx (use1 ++ bind1) bind2
adamc@720 649 -> xml ctx use1 (bind1 ++ bind2)
adamc@354 650 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type}
adamc@720 651 -> bind ::: {Type}
adamc@629 652 -> [use1 ~ use2] =>
adamc@720 653 xml ctx use1 bind
adamc@720 654 -> xml ctx (use1 ++ use2) bind
adamc@91 655
adamc@110 656 con xhtml = xml [Html]
adamc@139 657 con page = xhtml [] []
adamc@720 658 con xbody = xml [Body] [] []
adamc@1277 659 con xtable = xml [Body, Table] [] []
adamc@720 660 con xtr = xml [Body, Tr] [] []
adamc@720 661 con xform = xml [Body, Form] [] []
adamc@110 662
adamc@718 663
adamc@204 664 (*** HTML details *)
adamc@204 665
adamc@140 666 con html = [Html]
adamc@140 667 con head = [Head]
adamc@140 668 con body = [Body]
adamc@361 669 con form = [Body, Form]
adamc@760 670 con subform = [Body, Subform]
adamc@332 671 con tabl = [Body, Table]
adamc@332 672 con tr = [Body, Tr]
adamc@93 673
adam@1370 674 type queryString
adam@1370 675 val show_queryString : show queryString
adam@1370 676
adamc@724 677 type url
adamc@1065 678 val show_url : show url
adamc@724 679 val bless : string -> url
adamc@770 680 val checkUrl : string -> option url
adamc@1085 681 val currentUrl : transaction url
adam@1386 682 val currentUrlHasPost : transaction bool
adam@1485 683 val currentUrlHasQueryString : transaction bool
adamc@1065 684 val url : transaction page -> url
adam@1370 685 val effectfulUrl : (option queryString -> transaction page) -> url
adamc@1065 686 val redirect : t ::: Type -> url -> transaction t
adamc@724 687
adam@1556 688 type id
adam@1556 689 val fresh : transaction id
adam@1556 690
adamc@847 691 val dyn : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> [ctx ~ body] => unit
adamc@847 692 -> tag [Signal = signal (xml (body ++ ctx) use bind)] (body ++ ctx) [] use bind
adamc@568 693
adamc@720 694 val head : unit -> tag [] html head [] []
adamc@720 695 val title : unit -> tag [] head [] [] []
adam@1556 696 val link : unit -> tag [Id = id, Rel = string, Typ = string, Href = url, Media = string] head [] [] []
adamc@110 697
adamc@892 698 val body : unit -> tag [Onload = transaction unit, Onresize = transaction unit, Onunload = transaction unit]
adamc@892 699 html body [] []
adamc@354 700 con bodyTag = fn (attrs :: {Type}) =>
adamc@354 701 ctx ::: {Unit} ->
adamc@629 702 [[Body] ~ ctx] =>
adamc@720 703 unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
adamc@354 704 con bodyTagStandalone = fn (attrs :: {Type}) =>
adamc@354 705 ctx ::: {Unit}
adamc@629 706 -> [[Body] ~ ctx] =>
adamc@720 707 unit -> tag attrs ([Body] ++ ctx) [] [] []
adamc@141 708
adam@1556 709 val br : bodyTagStandalone [Id = id]
adamc@119 710
adamc@892 711 con focusEvents = [Onblur = transaction unit, Onfocus = transaction unit]
adamc@892 712 con mouseEvents = [Onclick = transaction unit, Ondblclick = transaction unit,
adamc@892 713 Onmousedown = transaction unit, Onmousemove = transaction unit,
adamc@892 714 Onmouseout = transaction unit, Onmouseover = transaction unit,
adamc@894 715 Onmouseup = transaction unit]
adamc@895 716 con keyEvents = [Onkeydown = int -> transaction unit, Onkeypress = int -> transaction unit,
adamc@895 717 Onkeyup = int -> transaction unit]
adamc@895 718 (* Key arguments are character codes. *)
adamc@892 719 con resizeEvents = [Onresize = transaction unit]
adamc@691 720
adamc@892 721 con boxEvents = focusEvents ++ mouseEvents ++ keyEvents ++ resizeEvents
adamc@892 722 con tableEvents = focusEvents ++ mouseEvents ++ keyEvents
adamc@140 723
adam@1556 724 con boxAttrs = [Id = id, Title = string] ++ boxEvents
adam@1556 725 con tableAttrs = [Id = id, Title = string] ++ tableEvents
adamc@469 726
adamc@1047 727 val span : bodyTag boxAttrs
adamc@1047 728 val div : bodyTag boxAttrs
adamc@140 729
adamc@1047 730 val p : bodyTag boxAttrs
adamc@1047 731 val b : bodyTag boxAttrs
adamc@1047 732 val i : bodyTag boxAttrs
adamc@1047 733 val tt : bodyTag boxAttrs
kkallio@1452 734 val sub : bodyTag boxAttrs
kkallio@1452 735 val sup : bodyTag boxAttrs
adamc@410 736
adamc@1047 737 val h1 : bodyTag boxAttrs
adamc@1047 738 val h2 : bodyTag boxAttrs
adamc@1047 739 val h3 : bodyTag boxAttrs
adamc@1047 740 val h4 : bodyTag boxAttrs
adamc@1047 741 val h5 : bodyTag boxAttrs
adamc@1047 742 val h6 : bodyTag boxAttrs
adamc@717 743
adamc@1047 744 val li : bodyTag boxAttrs
adamc@1047 745 val ol : bodyTag boxAttrs
adamc@1047 746 val ul : bodyTag boxAttrs
adamc@140 747
adamc@1047 748 val hr : bodyTag boxAttrs
adamc@1047 749
vshabanoff@1560 750 val a : bodyTag ([Link = transaction page, Href = url, Target = string] ++ boxAttrs)
adamc@892 751
adam@1419 752 val img : bodyTag ([Alt = string, Src = url, Width = int, Height = int,
adamc@1129 753 Onabort = transaction unit, Onerror = transaction unit,
adamc@1047 754 Onload = transaction unit] ++ boxAttrs)
adamc@892 755
adamc@720 756 val form : ctx ::: {Unit} -> bind ::: {Type}
adamc@1120 757 -> [[Body, Form, Table] ~ ctx] =>
adam@1412 758 option css_class
adam@1412 759 -> xml ([Body, Form] ++ ctx) [] bind
adamc@756 760 -> xml ([Body] ++ ctx) [] []
adamc@756 761
adamc@756 762 val subform : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
adamc@756 763 -> [[Form] ~ ctx] =>
adamc@756 764 nm :: Name -> [[nm] ~ use] =>
adamc@1004 765 xml ([Form] ++ ctx) [] bind
adamc@756 766 -> xml ([Form] ++ ctx) use [nm = $bind]
adamc@758 767
adamc@758 768 val subforms : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
adamc@1004 769 -> [[Form, Subform] ~ ctx] =>
adamc@758 770 nm :: Name -> [[nm] ~ use] =>
adamc@1004 771 xml ([Subform] ++ ctx) [Entry = $bind] []
adamc@758 772 -> xml ([Form] ++ ctx) use [nm = list ($bind)]
adamc@758 773
adamc@758 774 val entry : ctx ::: {Unit} -> bind ::: {Type}
adamc@1004 775 -> [[Subform, Form] ~ ctx] =>
adamc@1004 776 xml ([Form] ++ ctx) [] bind
adamc@758 777 -> xml ([Subform] ++ ctx) [Entry = $bind] []
adamc@758 778
adamc@361 779 con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) =>
adamc@354 780 ctx ::: {Unit}
adamc@629 781 -> [[Form] ~ ctx] =>
adamc@354 782 nm :: Name -> unit
adamc@720 783 -> tag attrs ([Form] ++ ctx) inner [] [nm = ty]
adamc@1047 784 val hidden : formTag string [] [Id = string, Value = string]
adamc@892 785 val textbox : formTag string [] ([Value = string, Size = int, Source = source string, Onchange = transaction unit,
adamc@1047 786 Ontext = transaction unit] ++ boxAttrs)
adamc@1047 787 val password : formTag string [] ([Value = string, Size = int] ++ boxAttrs)
adamc@892 788 val textarea : formTag string [] ([Rows = int, Cols = int, Onchange = transaction unit,
adamc@1047 789 Ontext = transaction unit] ++ boxAttrs)
adamc@153 790
adamc@1047 791 val checkbox : formTag bool [] ([Checked = bool] ++ boxAttrs)
adamc@190 792
adamc@737 793 type file
adamc@737 794 val fileName : file -> option string
adamc@740 795 val fileMimeType : file -> string
adamc@737 796 val fileData : file -> blob
adamc@737 797
adamc@1047 798 val upload : formTag file [] ([Value = string, Size = int] ++ boxAttrs)
adamc@737 799
adamc@741 800 type mimeType
adamc@741 801 val blessMime : string -> mimeType
adamc@770 802 val checkMime : string -> option mimeType
adamc@741 803 val returnBlob : t ::: Type -> blob -> mimeType -> transaction t
adamc@745 804 val blobSize : blob -> int
adamc@1119 805 val textBlob : string -> blob
adamc@741 806
adam@1347 807 type postBody
adam@1347 808 val postType : postBody -> string
adam@1347 809 val postData : postBody -> string
adam@1347 810
adamc@153 811 con radio = [Body, Radio]
adam@1556 812 val radio : formTag string radio [Id = id]
adamc@1068 813 val radioOption : unit -> tag ([Value = string, Checked = bool] ++ boxAttrs) radio [] [] []
adamc@142 814
adamc@154 815 con select = [Select]
adamc@1047 816 val select : formTag string select ([Onchange = transaction unit] ++ boxAttrs)
adamc@720 817 val option : unit -> tag [Value = string, Selected = bool] select [] [] []
adamc@154 818
adamc@720 819 val submit : ctx ::: {Unit} -> use ::: {Type}
adamc@629 820 -> [[Form] ~ ctx] =>
adamc@354 821 unit
adamc@1047 822 -> tag ([Value = string, Action = $use -> transaction page] ++ boxAttrs)
adamc@720 823 ([Form] ++ ctx) ([Form] ++ ctx) use []
adamc@283 824
adam@1517 825 val image : ctx ::: {Unit} -> use ::: {Type}
adam@1517 826 -> [[Form] ~ ctx] =>
adam@1517 827 unit
adam@1517 828 -> tag ([Src = url, Width = int, Height = int, Alt = string, Action = $use -> transaction page] ++ boxAttrs)
adam@1517 829 ([Form] ++ ctx) ([Form] ++ ctx) use []
adam@1517 830
adam@1557 831 val label : bodyTag ([For = id, Accesskey = string] ++ tableAttrs)
adamc@1047 832
adamc@1047 833
adamc@601 834 (*** AJAX-oriented widgets *)
adamc@601 835
adamc@797 836 con cformTag = fn (attrs :: {Type}) (inner :: {Unit}) =>
adamc@601 837 ctx ::: {Unit}
adamc@629 838 -> [[Body] ~ ctx] =>
adamc@797 839 unit -> tag attrs ([Body] ++ ctx) inner [] []
adamc@601 840
adamc@892 841 val ctextbox : cformTag ([Value = string, Size = int, Source = source string, Onchange = transaction unit,
adamc@1047 842 Ontext = transaction unit] ++ boxAttrs) []
adamc@1047 843 val button : cformTag ([Value = string] ++ boxAttrs) []
adamc@797 844
adamc@1047 845 val ccheckbox : cformTag ([Value = bool, Size = int, Source = source bool] ++ boxAttrs) []
adamc@817 846
adamc@797 847 con cselect = [Cselect]
adamc@1047 848 val cselect : cformTag ([Source = source string, Onchange = transaction unit] ++ boxAttrs) cselect
adamc@797 849 val coption : unit -> tag [Value = string, Selected = bool] cselect [] [] []
adamc@601 850
adamc@1099 851 val ctextarea : cformTag ([Value = string, Rows = int, Cols = int, Source = source string, Onchange = transaction unit,
adamc@1099 852 Ontext = transaction unit] ++ boxAttrs) []
adamc@1099 853
adamc@720 854 (*** Tables *)
adamc@720 855
adamc@892 856 val tabl : other ::: {Unit} -> [other ~ [Body, Table]] => unit
adamc@1047 857 -> tag ([Border = int] ++ boxAttrs)
adamc@892 858 ([Body] ++ other) ([Body, Table] ++ other) [] []
adamc@892 859 val tr : other ::: {Unit} -> [other ~ [Body, Table, Tr]] => unit
adamc@1047 860 -> tag tableAttrs
adamc@892 861 ([Body, Table] ++ other) ([Body, Tr] ++ other) [] []
adamc@892 862 val th : other ::: {Unit} -> [other ~ [Body, Tr]] => unit
kkallio@1476 863 -> tag ([Colspan = int, Rowspan = int] ++ tableAttrs)
adamc@892 864 ([Body, Tr] ++ other) ([Body] ++ other) [] []
adamc@892 865 val td : other ::: {Unit} -> [other ~ [Body, Tr]] => unit
kkallio@1476 866 -> tag ([Colspan = int, Rowspan = int] ++ tableAttrs)
adamc@892 867 ([Body, Tr] ++ other) ([Body] ++ other) [] []
adamc@720 868
adamc@283 869
adamc@283 870 (** Aborting *)
adamc@283 871
adamc@726 872 val error : t ::: Type -> xbody -> t
adamc@720 873
adamc@729 874 (* Client-side-only handlers: *)
adamc@726 875 val onError : (xbody -> transaction unit) -> transaction unit
adamc@728 876 val onFail : (string -> transaction unit) -> transaction unit
adamc@729 877 val onConnectFail : transaction unit -> transaction unit
adamc@729 878 val onDisconnect : transaction unit -> transaction unit
adamc@729 879 val onServerError : (string -> transaction unit) -> transaction unit
adamc@727 880
adam@1555 881 (* More standard document-level JavaScript handlers *)
adam@1555 882 val onClick : transaction unit -> transaction unit
adam@1555 883 val onDblclick : transaction unit -> transaction unit
adam@1555 884 val onKeydown : (int -> transaction unit) -> transaction unit
adam@1555 885 val onKeypress : (int -> transaction unit) -> transaction unit
adam@1555 886 val onKeyup : (int -> transaction unit) -> transaction unit
adam@1555 887 val onMousedown : transaction unit -> transaction unit
adam@1555 888 val onMouseup : transaction unit -> transaction unit
adam@1555 889
adam@1559 890 (* Prevents default handling of current event *)
adam@1559 891 val preventDefault : transaction unit
adam@1559 892 (* Stops propagation of current event *)
adam@1559 893 val stopPropagation : transaction unit
adam@1559 894
adamc@727 895 val show_xml : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> show (xml ctx use bind)
adamc@1075 896
adamc@1075 897
adamc@1075 898 (** Tasks *)
adamc@1075 899
adam@1348 900 con task_kind :: Type -> Type
adam@1348 901 val initialize : task_kind unit
adam@1348 902 val clientLeaves : task_kind client
adam@1349 903 val periodic : int -> task_kind unit
adamc@1120 904
adamc@1120 905
adamc@1199 906 (** Information flow security *)
adamc@1199 907
adamc@1199 908 type sql_policy
adamc@1199 909
adamc@1214 910 val sendClient : tables ::: {{Type}} -> exps ::: {Type}
adam@1394 911 -> [tables ~ exps] => sql_query [] [] tables exps
adamc@1214 912 -> sql_policy
adamc@1199 913
adamc@1229 914 val sendOwnIds : sql_sequence -> sql_policy
adamc@1229 915
adamc@1220 916 val mayInsert : fs ::: {Type} -> tables ::: {{Type}} -> [[New] ~ tables]
adam@1394 917 => sql_query [] [] ([New = fs] ++ tables) []
adamc@1220 918 -> sql_policy
adamc@1220 919
adamc@1221 920 val mayDelete : fs ::: {Type} -> tables ::: {{Type}} -> [[Old] ~ tables]
adam@1394 921 => sql_query [] [] ([Old = fs] ++ tables) []
adamc@1221 922 -> sql_policy
adamc@1221 923
adamc@1223 924 val mayUpdate : fs ::: {Type} -> tables ::: {{Type}} -> [[Old, New] ~ tables]
adam@1394 925 => sql_query [] [] ([Old = fs, New = fs] ++ tables) []
adamc@1223 926 -> sql_policy
adamc@1223 927
adamc@1240 928 val also : sql_policy -> sql_policy -> sql_policy
adamc@1199 929
adamc@1120 930 val debug : string -> transaction unit
adam@1389 931 val naughtyDebug : string -> int
adamc@1250 932
adamc@1250 933 val rand : transaction int