Mercurial > urweb

annotate lib/ur/basis.urs @ 1888:5f478ecf65e4

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