Mercurial > urweb

annotate lib/ur/basis.urs @ 1451:b6ce8ef0ea88

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