comparison lib/ur/basis.urs @ 629:e68de2a5506b

Top.Fold.concat elaborates
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 13:46:08 -0500
parents 8998114760c1
children 81c5c2674215
comparison
equal deleted inserted replaced
628:12b73f3c108e 629:e68de2a5506b
275 275
276 276
277 (*** Executing queries *) 277 (*** Executing queries *)
278 278
279 val query : tables ::: {{Type}} -> exps ::: {Type} 279 val query : tables ::: {{Type}} -> exps ::: {Type}
280 -> fn [tables ~ exps] => 280 -> [tables ~ exps] =>
281 state ::: Type 281 state ::: Type
282 -> sql_query tables exps 282 -> sql_query tables exps
283 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) 283 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
284 -> state 284 -> state
285 -> transaction state) 285 -> transaction state)
296 -> sql_table fields 296 -> sql_table fields
297 -> $(map (fn t :: Type => sql_exp [] [] [] t) fields) 297 -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
298 -> dml 298 -> dml
299 299
300 val update : unchanged ::: {Type} -> changed :: {Type} -> 300 val update : unchanged ::: {Type} -> changed :: {Type} ->
301 fn [changed ~ unchanged] => 301 [changed ~ unchanged] =>
302 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed) 302 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
303 -> sql_table (changed ++ unchanged) 303 -> sql_table (changed ++ unchanged)
304 -> sql_exp [T = changed ++ unchanged] [] [] bool 304 -> sql_exp [T = changed ++ unchanged] [] [] bool
305 -> dml 305 -> dml
306 306
324 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use [] 324 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
325 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type} 325 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type}
326 -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit} 326 -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
327 -> useOuter ::: {Type} -> useInner ::: {Type} 327 -> useOuter ::: {Type} -> useInner ::: {Type}
328 -> bindOuter ::: {Type} -> bindInner ::: {Type} 328 -> bindOuter ::: {Type} -> bindInner ::: {Type}
329 -> fn [attrsGiven ~ attrsAbsent] 329 -> [attrsGiven ~ attrsAbsent] =>
330 [useOuter ~ useInner] 330 [useOuter ~ useInner] =>
331 [bindOuter ~ bindInner] => 331 [bindOuter ~ bindInner] =>
332 $attrsGiven 332 $attrsGiven
333 -> tag (attrsGiven ++ attrsAbsent) 333 -> tag (attrsGiven ++ attrsAbsent)
334 ctxOuter ctxInner useOuter bindOuter 334 ctxOuter ctxInner useOuter bindOuter
335 -> xml ctxInner useInner bindInner 335 -> xml ctxInner useInner bindInner
336 -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner) 336 -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
337 val join : ctx ::: {Unit} 337 val join : ctx ::: {Unit}
338 -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type} 338 -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
339 -> fn [use1 ~ bind1] [bind1 ~ bind2] => 339 -> [use1 ~ bind1] => [bind1 ~ bind2] =>
340 xml ctx use1 bind1 340 xml ctx use1 bind1
341 -> xml ctx (use1 ++ bind1) bind2 341 -> xml ctx (use1 ++ bind1) bind2
342 -> xml ctx use1 (bind1 ++ bind2) 342 -> xml ctx use1 (bind1 ++ bind2)
343 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type} 343 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type}
344 -> bind ::: {Type} 344 -> bind ::: {Type}
345 -> fn [use1 ~ use2] => 345 -> [use1 ~ use2] =>
346 xml ctx use1 bind 346 xml ctx use1 bind
347 -> xml ctx (use1 ++ use2) bind 347 -> xml ctx (use1 ++ use2) bind
348 348
349 con xhtml = xml [Html] 349 con xhtml = xml [Html]
350 con page = xhtml [] [] 350 con page = xhtml [] []
368 val title : unit -> tag [] head [] [] [] 368 val title : unit -> tag [] head [] [] []
369 369
370 val body : unit -> tag [] html body [] [] 370 val body : unit -> tag [] html body [] []
371 con bodyTag = fn (attrs :: {Type}) => 371 con bodyTag = fn (attrs :: {Type}) =>
372 ctx ::: {Unit} -> 372 ctx ::: {Unit} ->
373 fn [[Body] ~ ctx] => 373 [[Body] ~ ctx] =>
374 unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] [] 374 unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
375 con bodyTagStandalone = fn (attrs :: {Type}) => 375 con bodyTagStandalone = fn (attrs :: {Type}) =>
376 ctx ::: {Unit} 376 ctx ::: {Unit}
377 -> fn [[Body] ~ ctx] => 377 -> [[Body] ~ ctx] =>
378 unit -> tag attrs ([Body] ++ ctx) [] [] [] 378 unit -> tag attrs ([Body] ++ ctx) [] [] []
379 379
380 val br : bodyTagStandalone [] 380 val br : bodyTagStandalone []
381 381
382 val p : bodyTag [] 382 val p : bodyTag []
397 val hr : bodyTag [] 397 val hr : bodyTag []
398 398
399 val a : bodyTag [Link = transaction page, Onclick = transaction unit] 399 val a : bodyTag [Link = transaction page, Onclick = transaction unit]
400 400
401 val form : ctx ::: {Unit} -> bind ::: {Type} 401 val form : ctx ::: {Unit} -> bind ::: {Type}
402 -> fn [[Body] ~ ctx] => 402 -> [[Body] ~ ctx] =>
403 xml form [] bind 403 xml form [] bind
404 -> xml ([Body] ++ ctx) [] [] 404 -> xml ([Body] ++ ctx) [] []
405 con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) => 405 con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) =>
406 ctx ::: {Unit} 406 ctx ::: {Unit}
407 -> fn [[Form] ~ ctx] => 407 -> [[Form] ~ ctx] =>
408 nm :: Name -> unit 408 nm :: Name -> unit
409 -> tag attrs ([Form] ++ ctx) inner [] [nm = ty] 409 -> tag attrs ([Form] ++ ctx) inner [] [nm = ty]
410 val textbox : formTag string [] [Value = string, Size = int, Source = source string] 410 val textbox : formTag string [] [Value = string, Size = int, Source = source string]
411 val password : formTag string [] [Value = string, Size = int] 411 val password : formTag string [] [Value = string, Size = int]
412 val textarea : formTag string [] [Rows = int, Cols = int] 412 val textarea : formTag string [] [Rows = int, Cols = int]
420 con select = [Select] 420 con select = [Select]
421 val select : formTag string select [] 421 val select : formTag string select []
422 val option : unit -> tag [Value = string, Selected = bool] select [] [] [] 422 val option : unit -> tag [Value = string, Selected = bool] select [] [] []
423 423
424 val submit : ctx ::: {Unit} -> use ::: {Type} 424 val submit : ctx ::: {Unit} -> use ::: {Type}
425 -> fn [[Form] ~ ctx] => 425 -> [[Form] ~ ctx] =>
426 unit 426 unit
427 -> tag [Value = string, Action = $use -> transaction page] 427 -> tag [Value = string, Action = $use -> transaction page]
428 ([Form] ++ ctx) ([Form] ++ ctx) use [] 428 ([Form] ++ ctx) ([Form] ++ ctx) use []
429 429
430 (*** AJAX-oriented widgets *) 430 (*** AJAX-oriented widgets *)
431 431
432 con cformTag = fn (attrs :: {Type}) => 432 con cformTag = fn (attrs :: {Type}) =>
433 ctx ::: {Unit} 433 ctx ::: {Unit}
434 -> fn [[Body] ~ ctx] => 434 -> [[Body] ~ ctx] =>
435 unit -> tag attrs ([Body] ++ ctx) [] [] [] 435 unit -> tag attrs ([Body] ++ ctx) [] [] []
436 436
437 val ctextbox : cformTag [Value = string, Size = int, Source = source string] 437 val ctextbox : cformTag [Value = string, Size = int, Source = source string]
438 val button : cformTag [Value = string, Onclick = transaction unit] 438 val button : cformTag [Value = string, Onclick = transaction unit]
439 439
440 (*** Tables *) 440 (*** Tables *)
441 441
442 val tabl : other ::: {Unit} -> fn [other ~ [Body, Table]] => 442 val tabl : other ::: {Unit} -> [other ~ [Body, Table]] =>
443 unit -> tag [Border = int] ([Body] ++ other) ([Body, Table] ++ other) [] [] 443 unit -> tag [Border = int] ([Body] ++ other) ([Body, Table] ++ other) [] []
444 val tr : other ::: {Unit} -> fn [other ~ [Body, Table, Tr]] => 444 val tr : other ::: {Unit} -> [other ~ [Body, Table, Tr]] =>
445 unit -> tag [] ([Body, Table] ++ other) ([Body, Tr] ++ other) [] [] 445 unit -> tag [] ([Body, Table] ++ other) ([Body, Tr] ++ other) [] []
446 val th : other ::: {Unit} -> fn [other ~ [Body, Tr]] => 446 val th : other ::: {Unit} -> [other ~ [Body, Tr]] =>
447 unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] [] 447 unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] []
448 val td : other ::: {Unit} -> fn [other ~ [Body, Tr]] => 448 val td : other ::: {Unit} -> [other ~ [Body, Tr]] =>
449 unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] [] 449 unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] []
450 450
451 451
452 (** Aborting *) 452 (** Aborting *)
453 453