Mercurial > urweb

annotate lib/ur/basis.urs @ 1242:4ed556678214

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