Mercurial > urweb

annotate lib/ur/basis.urs @ 709:0406e9cccb72

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FOREIGN KEY, without ability to link NULL to NOT NULL (and with some lingering problems in row inference)
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 18:47:47 -0400
parents d8217b4cb617
children 7292bcb7c02d
rev   line source
adamc@56 1 type int
adamc@56 2 type float
adamc@56 3 type string
adamc@436 4 type time
adamc@91 5
adamc@119 6 type unit = {}
adamc@119 7
adamc@186 8 datatype bool = False | True
adamc@186 9
adamc@288 10 datatype option t = None | Some of t
adamc@284 11
adamc@91 12
adamc@256 13 (** Basic type classes *)
adamc@256 14
adamc@256 15 class eq
adamc@256 16 val eq : t ::: Type -> eq t -> t -> t -> bool
adamc@257 17 val ne : t ::: Type -> eq t -> t -> t -> bool
adamc@256 18 val eq_int : eq int
adamc@394 19 val eq_float : eq float
adamc@256 20 val eq_string : eq string
adamc@256 21 val eq_bool : eq bool
adamc@437 22 val eq_time : eq time
adamc@422 23 val mkEq : t ::: Type -> (t -> t -> bool) -> eq t
adamc@256 24
adamc@389 25 class num
adamc@417 26 val zero : t ::: Type -> num t -> t
adamc@389 27 val neg : t ::: Type -> num t -> t -> t
adamc@389 28 val plus : t ::: Type -> num t -> t -> t -> t
adamc@389 29 val minus : t ::: Type -> num t -> t -> t -> t
adamc@389 30 val times : t ::: Type -> num t -> t -> t -> t
adamc@389 31 val div : t ::: Type -> num t -> t -> t -> t
adamc@389 32 val mod : t ::: Type -> num t -> t -> t -> t
adamc@389 33 val num_int : num int
adamc@390 34 val num_float : num float
adamc@389 35
adamc@391 36 class ord
adamc@391 37 val lt : t ::: Type -> ord t -> t -> t -> bool
adamc@391 38 val le : t ::: Type -> ord t -> t -> t -> bool
adamc@391 39 val gt : t ::: Type -> ord t -> t -> t -> bool
adamc@391 40 val ge : t ::: Type -> ord t -> t -> t -> bool
adamc@391 41 val ord_int : ord int
adamc@394 42 val ord_float : ord float
adamc@394 43 val ord_string : ord string
adamc@394 44 val ord_bool : ord bool
adamc@437 45 val ord_time : ord time
adamc@391 46
adamc@256 47
adamc@283 48 (** String operations *)
adamc@283 49
adamc@283 50 val strcat : string -> string -> string
adamc@283 51
adamc@286 52 class show
adamc@286 53 val show : t ::: Type -> show t -> t -> string
adamc@286 54 val show_int : show int
adamc@286 55 val show_float : show float
adamc@286 56 val show_string : show string
adamc@286 57 val show_bool : show bool
adamc@436 58 val show_time : show time
adamc@452 59 val mkShow : t ::: Type -> (t -> string) -> show t
adamc@286 60
adamc@290 61 class read
adamc@290 62 val read : t ::: Type -> read t -> string -> option t
adamc@292 63 val readError : t ::: Type -> read t -> string -> t
adamc@292 64 (* [readError] calls [error] if the input is malformed. *)
adamc@290 65 val read_int : read int
adamc@290 66 val read_float : read float
adamc@290 67 val read_string : read string
adamc@290 68 val read_bool : read bool
adamc@436 69 val read_time : read time
adamc@288 70
adamc@283 71
adamc@564 72 (** * Monads *)
adamc@564 73
adamc@564 74 class monad :: Type -> Type
adamc@564 75 val return : m ::: (Type -> Type) -> t ::: Type
adamc@564 76 -> monad m
adamc@564 77 -> t -> m t
adamc@564 78 val bind : m ::: (Type -> Type) -> t1 ::: Type -> t2 ::: Type
adamc@564 79 -> monad m
adamc@564 80 -> m t1 -> (t1 -> m t2)
adamc@564 81 -> m t2
adamc@564 82
adamc@456 83 con transaction :: Type -> Type
adamc@564 84 val transaction_monad : monad transaction
adamc@456 85
adamc@565 86 con source :: Type -> Type
adamc@565 87 val source : t ::: Type -> t -> transaction (source t)
adamc@575 88 val set : t ::: Type -> source t -> t -> transaction unit
adamc@601 89 val get : t ::: Type -> source t -> transaction t
adamc@565 90
adamc@565 91 con signal :: Type -> Type
adamc@565 92 val signal_monad : monad signal
adamc@565 93 val signal : t ::: Type -> source t -> signal t
adamc@456 94
adamc@456 95
adamc@456 96 (** HTTP operations *)
adamc@456 97
adamc@456 98 val requestHeader : string -> transaction (option string)
adamc@456 99
adamc@459 100 con http_cookie :: Type -> Type
adamc@459 101 val getCookie : t ::: Type -> http_cookie t -> transaction (option t)
adamc@459 102 val setCookie : t ::: Type -> http_cookie t -> t -> transaction unit
adamc@459 103
adamc@456 104
adamc@566 105 (** JavaScript-y gadgets *)
adamc@566 106
adamc@566 107 val alert : string -> transaction unit
adamc@694 108 val spawn : transaction unit -> transaction unit
adamc@695 109 val sleep : int -> transaction unit
adamc@566 110
adamc@566 111
adamc@678 112 (** Channels *)
adamc@678 113
adamc@678 114 con channel :: Type -> Type
adamc@678 115 val channel : t ::: Type -> transaction (channel t)
adamc@678 116 val send : t ::: Type -> channel t -> t -> transaction unit
adamc@678 117 val recv : t ::: Type -> channel t -> transaction t
adamc@678 118
adamc@682 119 type client
adamc@682 120 val self : transaction client
adamc@682 121
adamc@678 122
adamc@203 123 (** SQL *)
adamc@203 124
adamc@705 125 con sql_table :: {Type} -> {{Unit}} -> Type
adamc@203 126
adamc@704 127 (*** Constraints *)
adamc@704 128
adamc@707 129 (**** Primary keys *)
adamc@707 130
adamc@707 131 class sql_injectable_prim
adamc@707 132 val sql_bool : sql_injectable_prim bool
adamc@707 133 val sql_int : sql_injectable_prim int
adamc@707 134 val sql_float : sql_injectable_prim float
adamc@707 135 val sql_string : sql_injectable_prim string
adamc@707 136 val sql_time : sql_injectable_prim time
adamc@707 137 val sql_channel : t ::: Type -> sql_injectable_prim (channel t)
adamc@707 138 val sql_client : sql_injectable_prim client
adamc@707 139
adamc@707 140 con primary_key :: {Type} -> {{Unit}} -> Type
adamc@707 141 val no_primary_key : fs ::: {Type} -> primary_key fs []
adamc@707 142 val primary_key : rest ::: {Type} -> t ::: Type -> key1 :: Name -> keys :: {Type}
adamc@707 143 -> [[key1] ~ keys] => [[key1 = t] ++ keys ~ rest]
adamc@707 144 => $([key1 = sql_injectable_prim t] ++ map sql_injectable_prim keys)
adamc@707 145 -> primary_key ([key1 = t] ++ keys ++ rest)
adamc@707 146 [Pkey = [key1] ++ map (fn _ => ()) keys]
adamc@707 147
adamc@707 148 (**** Other constraints *)
adamc@707 149
adamc@705 150 con sql_constraints :: {Type} -> {{Unit}} -> Type
adamc@705 151 (* Arguments: column types, uniqueness implications of constraints *)
adamc@704 152
adamc@705 153 con sql_constraint :: {Type} -> {Unit} -> Type
adamc@704 154
adamc@705 155 val no_constraint : fs ::: {Type} -> sql_constraints fs []
adamc@705 156 val one_constraint : fs ::: {Type} -> unique ::: {Unit} -> name :: Name
adamc@705 157 -> sql_constraint fs unique
adamc@705 158 -> sql_constraints fs [name = unique]
adamc@705 159 val join_constraints : fs ::: {Type}
adamc@705 160 -> uniques1 ::: {{Unit}} -> uniques2 ::: {{Unit}} -> [uniques1 ~ uniques2]
adamc@705 161 => sql_constraints fs uniques1 -> sql_constraints fs uniques2
adamc@705 162 -> sql_constraints fs (uniques1 ++ uniques2)
adamc@705 163
adamc@709 164
adamc@705 165 val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type}
adamc@705 166 -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest]
adamc@705 167 => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique)
adamc@704 168
adamc@709 169 con matching :: {Type} -> {Type} -> Type
adamc@709 170 val mat_nil : matching [] []
adamc@709 171 val mat_cons : t ::: Type -> rest1 ::: {Type} -> rest2 ::: {Type}
adamc@709 172 -> nm1 :: Name -> nm2 :: Name
adamc@709 173 -> [[nm1] ~ rest1] => [[nm2] ~ rest2]
adamc@709 174 => matching rest1 rest2
adamc@709 175 -> matching ([nm1 = t] ++ rest1) ([nm2 = t] ++ rest2)
adamc@709 176
adamc@709 177 con propagation_mode :: {Type} -> Type
adamc@709 178 val restrict : fs ::: {Type} -> propagation_mode fs
adamc@709 179 val cascade : fs ::: {Type} -> propagation_mode fs
adamc@709 180 val no_action : fs ::: {Type} -> propagation_mode fs
adamc@709 181 val set_null : fs ::: {Type} -> propagation_mode (map option fs)
adamc@709 182
adamc@709 183
adamc@709 184 val foreign_key : mine1 ::: Name -> t ::: Type -> mine ::: {Type} -> munused ::: {Type}
adamc@709 185 -> foreign ::: {Type} -> funused ::: {Type}
adamc@709 186 -> nm ::: Name -> uniques ::: {{Unit}}
adamc@709 187 -> [[mine1] ~ mine] => [[mine1 = t] ++ mine ~ munused]
adamc@709 188 => [foreign ~ funused] => [[nm] ~ uniques]
adamc@709 189 => matching ([mine1 = t] ++ mine) foreign
adamc@709 190 -> sql_table (foreign ++ funused) ([nm = map (fn _ => ()) foreign] ++ uniques)
adamc@709 191 -> {OnDelete : propagation_mode ([mine1 = t] ++ mine),
adamc@709 192 OnUpdate : propagation_mode ([mine1 = t] ++ mine)}
adamc@709 193 -> sql_constraint ([mine1 = t] ++ mine ++ munused) []
adamc@709 194
adamc@704 195
adamc@204 196 (*** Queries *)
adamc@204 197
adamc@233 198 con sql_query :: {{Type}} -> {Type} -> Type
adamc@233 199 con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type
adamc@234 200 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
adamc@204 201
adamc@223 202 con sql_subset :: {{Type}} -> {{Type}} -> Type
adamc@223 203 val sql_subset : keep_drop :: {({Type} * {Type})}
adamc@354 204 -> sql_subset
adamc@621 205 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop)
adamc@621 206 (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop)
adamc@354 207 val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables
adamc@223 208
adamc@705 209 val sql_query1 : tables ::: {({Type} * {{Unit}})}
adamc@354 210 -> grouped ::: {{Type}}
adamc@354 211 -> selectedFields ::: {{Type}}
adamc@354 212 -> selectedExps ::: {Type}
adamc@705 213 -> {From : $(map (fn p :: ({Type} * {{Unit}}) => sql_table p.1 p.2) tables),
adamc@705 214 Where : sql_exp (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) [] [] bool,
adamc@705 215 GroupBy : sql_subset (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) grouped,
adamc@705 216 Having : sql_exp grouped (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) [] bool,
adamc@354 217 SelectFields : sql_subset grouped selectedFields,
adamc@705 218 SelectExps : $(map (sql_exp grouped (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) [])
adamc@705 219 selectedExps) }
adamc@705 220 -> sql_query1 (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) selectedFields selectedExps
adamc@229 221
adamc@229 222 type sql_relop
adamc@229 223 val sql_union : sql_relop
adamc@229 224 val sql_intersect : sql_relop
adamc@229 225 val sql_except : sql_relop
adamc@260 226 val sql_relop : tables1 ::: {{Type}}
adamc@354 227 -> tables2 ::: {{Type}}
adamc@354 228 -> selectedFields ::: {{Type}}
adamc@354 229 -> selectedExps ::: {Type}
adamc@354 230 -> sql_relop
adamc@354 231 -> sql_query1 tables1 selectedFields selectedExps
adamc@354 232 -> sql_query1 tables2 selectedFields selectedExps
adamc@354 233 -> sql_query1 selectedFields selectedFields selectedExps
adamc@229 234
adamc@230 235 type sql_direction
adamc@230 236 val sql_asc : sql_direction
adamc@230 237 val sql_desc : sql_direction
adamc@230 238
adamc@234 239 con sql_order_by :: {{Type}} -> {Type} -> Type
adamc@234 240 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
adamc@234 241 val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
adamc@354 242 -> sql_exp tables [] exps t -> sql_direction
adamc@354 243 -> sql_order_by tables exps
adamc@354 244 -> sql_order_by tables exps
adamc@230 245
adamc@231 246 type sql_limit
adamc@231 247 val sql_no_limit : sql_limit
adamc@231 248 val sql_limit : int -> sql_limit
adamc@354 249
adamc@232 250 type sql_offset
adamc@232 251 val sql_no_offset : sql_offset
adamc@232 252 val sql_offset : int -> sql_offset
adamc@232 253
adamc@229 254 val sql_query : tables ::: {{Type}}
adamc@354 255 -> selectedFields ::: {{Type}}
adamc@354 256 -> selectedExps ::: {Type}
adamc@354 257 -> {Rows : sql_query1 tables selectedFields selectedExps,
adamc@354 258 OrderBy : sql_order_by tables selectedExps,
adamc@354 259 Limit : sql_limit,
adamc@354 260 Offset : sql_offset}
adamc@354 261 -> sql_query selectedFields selectedExps
adamc@204 262
adamc@354 263 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
adamc@354 264 -> fieldType ::: Type -> agg ::: {{Type}}
adamc@354 265 -> exps ::: {Type}
adamc@354 266 -> tab :: Name -> field :: Name
adamc@354 267 -> sql_exp
adamc@354 268 ([tab = [field = fieldType] ++ otherFields] ++ otherTabs)
adamc@354 269 agg exps fieldType
adamc@234 270
adamc@354 271 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type}
adamc@354 272 -> nm :: Name
adamc@354 273 -> sql_exp tabs agg ([nm = t] ++ rest) t
adamc@209 274
adamc@221 275 class sql_injectable
adamc@676 276 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t
adamc@676 277 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)
adamc@676 278
adamc@354 279 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 280 -> t ::: Type
adamc@354 281 -> sql_injectable t -> t -> sql_exp tables agg exps t
adamc@209 282
adamc@470 283 val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 284 -> t ::: Type
adamc@470 285 -> sql_exp tables agg exps (option t)
adamc@470 286 -> sql_exp tables agg exps bool
adamc@470 287
adamc@559 288 class sql_arith
adamc@559 289 val sql_int_arith : sql_arith int
adamc@559 290 val sql_float_arith : sql_arith float
adamc@559 291
adamc@220 292 con sql_unary :: Type -> Type -> Type
adamc@220 293 val sql_not : sql_unary bool bool
adamc@354 294 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 295 -> arg ::: Type -> res ::: Type
adamc@354 296 -> sql_unary arg res -> sql_exp tables agg exps arg
adamc@354 297 -> sql_exp tables agg exps res
adamc@220 298
adamc@559 299 val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t
adamc@559 300
adamc@220 301 con sql_binary :: Type -> Type -> Type -> Type
adamc@220 302 val sql_and : sql_binary bool bool bool
adamc@220 303 val sql_or : sql_binary bool bool bool
adamc@234 304 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 305 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
adamc@354 306 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1
adamc@354 307 -> sql_exp tables agg exps arg2
adamc@354 308 -> sql_exp tables agg exps res
adamc@220 309
adamc@559 310 val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 311 val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 312 val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 313 val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t
adamc@559 314 val sql_mod : sql_binary int int int
adamc@559 315
adamc@559 316 val sql_eq : t ::: Type -> sql_binary t t bool
adamc@559 317 val sql_ne : t ::: Type -> sql_binary t t bool
adamc@559 318 val sql_lt : t ::: Type -> sql_binary t t bool
adamc@559 319 val sql_le : t ::: Type -> sql_binary t t bool
adamc@559 320 val sql_gt : t ::: Type -> sql_binary t t bool
adamc@559 321 val sql_ge : t ::: Type -> sql_binary t t bool
adamc@203 322
adamc@235 323 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@544 324 -> sql_exp tables agg exps int
adamc@235 325
adamc@236 326 con sql_aggregate :: Type -> Type
adamc@354 327 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 328 -> t ::: Type
adamc@354 329 -> sql_aggregate t -> sql_exp agg agg exps t
adamc@354 330 -> sql_exp tables agg exps t
adamc@236 331
adamc@236 332 class sql_summable
adamc@236 333 val sql_summable_int : sql_summable int
adamc@236 334 val sql_summable_float : sql_summable float
adamc@236 335 val sql_avg : t ::: Type -> sql_summable t -> sql_aggregate t
adamc@236 336 val sql_sum : t ::: Type -> sql_summable t -> sql_aggregate t
adamc@236 337
adamc@236 338 class sql_maxable
adamc@236 339 val sql_maxable_int : sql_maxable int
adamc@236 340 val sql_maxable_float : sql_maxable float
adamc@236 341 val sql_maxable_string : sql_maxable string
adamc@437 342 val sql_maxable_time : sql_maxable time
adamc@236 343 val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t
adamc@236 344 val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t
adamc@236 345
adamc@441 346 con sql_nfunc :: Type -> Type
adamc@441 347 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@441 348 -> t ::: Type
adamc@441 349 -> sql_nfunc t -> sql_exp tables agg exps t
adamc@441 350 val sql_current_timestamp : sql_nfunc time
adamc@441 351
adamc@235 352
adamc@243 353 (*** Executing queries *)
adamc@243 354
adamc@354 355 val query : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 356 -> [tables ~ exps] =>
adamc@354 357 state ::: Type
adamc@354 358 -> sql_query tables exps
adamc@621 359 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@354 360 -> state
adamc@354 361 -> transaction state)
adamc@354 362 -> state
adamc@354 363 -> transaction state
adamc@243 364
adamc@243 365
adamc@299 366 (*** Database mutators *)
adamc@299 367
adamc@299 368 type dml
adamc@299 369 val dml : dml -> transaction unit
adamc@299 370
adamc@705 371 val insert : fields ::: {Type} -> uniques ::: {{Unit}}
adamc@705 372 -> sql_table fields uniques
adamc@621 373 -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
adamc@354 374 -> dml
adamc@299 375
adamc@705 376 val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} ->
adamc@629 377 [changed ~ unchanged] =>
adamc@621 378 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
adamc@705 379 -> sql_table (changed ++ unchanged) uniques
adamc@354 380 -> sql_exp [T = changed ++ unchanged] [] [] bool
adamc@354 381 -> dml
adamc@299 382
adamc@705 383 val delete : fields ::: {Type} -> uniques ::: {{Unit}}
adamc@705 384 -> sql_table fields uniques
adamc@354 385 -> sql_exp [T = fields] [] [] bool
adamc@354 386 -> dml
adamc@299 387
adamc@338 388 (*** Sequences *)
adamc@338 389
adamc@338 390 type sql_sequence
adamc@338 391 val nextval : sql_sequence -> transaction int
adamc@338 392
adamc@299 393
adamc@203 394 (** XML *)
adamc@203 395
adamc@139 396 con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
adamc@91 397
adamc@91 398
adamc@139 399 con xml :: {Unit} -> {Type} -> {Type} -> Type
adamc@141 400 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
adamc@354 401 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type}
adamc@354 402 -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
adamc@354 403 -> useOuter ::: {Type} -> useInner ::: {Type}
adamc@354 404 -> bindOuter ::: {Type} -> bindInner ::: {Type}
adamc@629 405 -> [attrsGiven ~ attrsAbsent] =>
adamc@629 406 [useOuter ~ useInner] =>
adamc@629 407 [bindOuter ~ bindInner] =>
adamc@629 408 $attrsGiven
adamc@629 409 -> tag (attrsGiven ++ attrsAbsent)
adamc@629 410 ctxOuter ctxInner useOuter bindOuter
adamc@629 411 -> xml ctxInner useInner bindInner
adamc@629 412 -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
adamc@140 413 val join : ctx ::: {Unit}
adamc@139 414 -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
adamc@629 415 -> [use1 ~ bind1] => [bind1 ~ bind2] =>
adamc@354 416 xml ctx use1 bind1
adamc@354 417 -> xml ctx (use1 ++ bind1) bind2
adamc@354 418 -> xml ctx use1 (bind1 ++ bind2)
adamc@354 419 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type}
adamc@354 420 -> bind ::: {Type}
adamc@629 421 -> [use1 ~ use2] =>
adamc@354 422 xml ctx use1 bind
adamc@354 423 -> xml ctx (use1 ++ use2) bind
adamc@91 424
adamc@110 425 con xhtml = xml [Html]
adamc@139 426 con page = xhtml [] []
adamc@325 427 con xbody = xml [Body] [] []
adamc@326 428 con xtr = xml [Body, Tr] [] []
adamc@361 429 con xform = xml [Body, Form] [] []
adamc@110 430
adamc@204 431 (*** HTML details *)
adamc@204 432
adamc@140 433 con html = [Html]
adamc@140 434 con head = [Head]
adamc@140 435 con body = [Body]
adamc@361 436 con form = [Body, Form]
adamc@332 437 con tabl = [Body, Table]
adamc@332 438 con tr = [Body, Tr]
adamc@93 439
adamc@691 440 val dyn : use ::: {Type} -> bind ::: {Type} -> unit
adamc@691 441 -> tag [Signal = signal (xml body use bind)] body [] use bind
adamc@568 442
adamc@140 443 val head : unit -> tag [] html head [] []
adamc@140 444 val title : unit -> tag [] head [] [] []
adamc@110 445
adamc@668 446 val body : unit -> tag [Onload = transaction unit] html body [] []
adamc@354 447 con bodyTag = fn (attrs :: {Type}) =>
adamc@354 448 ctx ::: {Unit} ->
adamc@629 449 [[Body] ~ ctx] =>
adamc@354 450 unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
adamc@354 451 con bodyTagStandalone = fn (attrs :: {Type}) =>
adamc@354 452 ctx ::: {Unit}
adamc@629 453 -> [[Body] ~ ctx] =>
adamc@354 454 unit -> tag attrs ([Body] ++ ctx) [] [] []
adamc@141 455
adamc@141 456 val br : bodyTagStandalone []
adamc@119 457
adamc@691 458 val span : bodyTag []
adamc@691 459
adamc@140 460 val p : bodyTag []
adamc@140 461 val b : bodyTag []
adamc@140 462 val i : bodyTag []
adamc@407 463 val tt : bodyTag []
adamc@140 464 val font : bodyTag [Size = int, Face = string]
adamc@140 465
adamc@140 466 val h1 : bodyTag []
adamc@443 467 val h2 : bodyTag []
adamc@443 468 val h3 : bodyTag []
adamc@443 469 val h4 : bodyTag []
adamc@469 470
adamc@140 471 val li : bodyTag []
adamc@469 472 val ol : bodyTag []
adamc@469 473 val ul : bodyTag []
adamc@140 474
adamc@410 475 val hr : bodyTag []
adamc@410 476
adamc@566 477 val a : bodyTag [Link = transaction page, Onclick = transaction unit]
adamc@140 478
adamc@361 479 val form : ctx ::: {Unit} -> bind ::: {Type}
adamc@629 480 -> [[Body] ~ ctx] =>
adamc@354 481 xml form [] bind
adamc@354 482 -> xml ([Body] ++ ctx) [] []
adamc@361 483 con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) =>
adamc@354 484 ctx ::: {Unit}
adamc@629 485 -> [[Form] ~ ctx] =>
adamc@354 486 nm :: Name -> unit
adamc@361 487 -> tag attrs ([Form] ++ ctx) inner [] [nm = ty]
adamc@598 488 val textbox : formTag string [] [Value = string, Size = int, Source = source string]
adamc@444 489 val password : formTag string [] [Value = string, Size = int]
adamc@444 490 val textarea : formTag string [] [Rows = int, Cols = int]
adamc@153 491
adamc@361 492 val checkbox : formTag bool [] [Checked = bool]
adamc@190 493
adamc@153 494 con radio = [Body, Radio]
adamc@361 495 val radio : formTag string radio []
adamc@153 496 val radioOption : unit -> tag [Value = string] radio [] [] []
adamc@142 497
adamc@154 498 con select = [Select]
adamc@361 499 val select : formTag string select []
adamc@422 500 val option : unit -> tag [Value = string, Selected = bool] select [] [] []
adamc@154 501
adamc@568 502 val submit : ctx ::: {Unit} -> use ::: {Type}
adamc@629 503 -> [[Form] ~ ctx] =>
adamc@354 504 unit
adamc@406 505 -> tag [Value = string, Action = $use -> transaction page]
adamc@361 506 ([Form] ++ ctx) ([Form] ++ ctx) use []
adamc@283 507
adamc@601 508 (*** AJAX-oriented widgets *)
adamc@601 509
adamc@601 510 con cformTag = fn (attrs :: {Type}) =>
adamc@601 511 ctx ::: {Unit}
adamc@629 512 -> [[Body] ~ ctx] =>
adamc@601 513 unit -> tag attrs ([Body] ++ ctx) [] [] []
adamc@601 514
adamc@601 515 val ctextbox : cformTag [Value = string, Size = int, Source = source string]
adamc@601 516 val button : cformTag [Value = string, Onclick = transaction unit]
adamc@601 517
adamc@325 518 (*** Tables *)
adamc@325 519
adamc@629 520 val tabl : other ::: {Unit} -> [other ~ [Body, Table]] =>
adamc@406 521 unit -> tag [Border = int] ([Body] ++ other) ([Body, Table] ++ other) [] []
adamc@629 522 val tr : other ::: {Unit} -> [other ~ [Body, Table, Tr]] =>
adamc@406 523 unit -> tag [] ([Body, Table] ++ other) ([Body, Tr] ++ other) [] []
adamc@629 524 val th : other ::: {Unit} -> [other ~ [Body, Tr]] =>
adamc@406 525 unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] []
adamc@629 526 val td : other ::: {Unit} -> [other ~ [Body, Tr]] =>
adamc@406 527 unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] []
adamc@325 528
adamc@283 529
adamc@283 530 (** Aborting *)
adamc@283 531
adamc@283 532 val error : t ::: Type -> xml [Body] [] [] -> t
adamc@668 533
adamc@668 534