Mercurial > urweb

annotate lib/ur/basis.urs @ 1473:d40066b38710

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