Mercurial > urweb

comparison lib/ur/basis.urs @ 1775:6bc2a8cb3a67

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Track whether SQL expressions may use window functions, in preparation for actual window function support
author Adam Chlipala <adam@chlipala.net>
date Sat, 02 Jun 2012 15:35:58 -0400
parents acadf9d1214a
children 8f28c3295148
comparison
equal deleted inserted replaced
1774:27fdd78bd2f5 1775:6bc2a8cb3a67
303 -> sql_table (foreign ++ funused) ([nm = map (fn _ => ()) foreign] ++ uniques) 303 -> sql_table (foreign ++ funused) ([nm = map (fn _ => ()) foreign] ++ uniques)
304 -> {OnDelete : propagation_mode ([mine1 = t] ++ mine), 304 -> {OnDelete : propagation_mode ([mine1 = t] ++ mine),
305 OnUpdate : propagation_mode ([mine1 = t] ++ mine)} 305 OnUpdate : propagation_mode ([mine1 = t] ++ mine)}
306 -> sql_constraint ([mine1 = t] ++ mine ++ munused) [] 306 -> sql_constraint ([mine1 = t] ++ mine ++ munused) []
307 307
308 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type 308 con allow_window :: {Unit}
309 val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type 309 con disallow_window :: {Unit}
310
311 con sql_exp :: {{Type}} (* Free tables, for normal use *)
312 -> {{Type}} (* Free tables, for use in arguments to aggregate functions *)
313 -> {Type} (* Free ad-hoc variables *)
314 -> {Unit} (* Allow window functions here? ([allow_window] indicates yes.) *)
315 -> Type (* SQL type of this expression *)
316 -> Type
317 val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} -> t ::: Type
310 -> fs' ::: {{Type}} -> agg' ::: {{Type}} -> exps' ::: {Type} 318 -> fs' ::: {{Type}} -> agg' ::: {{Type}} -> exps' ::: {Type}
311 -> [fs ~ fs'] => [agg ~ agg'] => [exps ~ exps'] => 319 -> [fs ~ fs'] => [agg ~ agg'] => [exps ~ exps'] =>
312 sql_exp fs agg exps t 320 sql_exp fs agg exps aw t
313 -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') t 321 -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') aw t
314 322
315 val check : fs ::: {Type} 323 val check : fs ::: {Type}
316 -> sql_exp [] [] fs bool 324 -> sql_exp [] [] fs disallow_window bool
317 -> sql_constraint fs [] 325 -> sql_constraint fs []
318 326
319 327
320 (*** Queries *) 328 (*** Queries *)
321 329
349 => sql_from_items free tabs1 -> sql_from_items free tabs2 357 => sql_from_items free tabs1 -> sql_from_items free tabs2
350 -> sql_from_items free (tabs1 ++ tabs2) 358 -> sql_from_items free (tabs1 ++ tabs2)
351 val sql_inner_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}} 359 val sql_inner_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
352 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2] 360 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
353 => sql_from_items free tabs1 -> sql_from_items free tabs2 361 => sql_from_items free tabs1 -> sql_from_items free tabs2
354 -> sql_exp (free ++ tabs1 ++ tabs2) [] [] bool 362 -> sql_exp (free ++ tabs1 ++ tabs2) [] [] disallow_window bool
355 -> sql_from_items free (tabs1 ++ tabs2) 363 -> sql_from_items free (tabs1 ++ tabs2)
356 364
357 class nullify :: Type -> Type -> Type 365 class nullify :: Type -> Type -> Type
358 val nullify_option : t ::: Type -> nullify (option t) (option t) 366 val nullify_option : t ::: Type -> nullify (option t) (option t)
359 val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t) 367 val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t)
360 368
361 val sql_left_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}} 369 val sql_left_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}}
362 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2] 370 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
363 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2) 371 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2)
364 -> sql_from_items free tabs1 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2) 372 -> sql_from_items free tabs1 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
365 -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool 373 -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] disallow_window bool
366 -> sql_from_items free (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2) 374 -> sql_from_items free (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
367 375
368 val sql_right_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}} 376 val sql_right_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}}
369 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2] 377 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
370 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1) 378 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1)
371 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items free tabs2 379 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items free tabs2
372 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool 380 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] disallow_window bool
373 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2) 381 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
374 382
375 val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}} 383 val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
376 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2] 384 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
377 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2)) 385 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2))
378 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) 386 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1)
379 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2) 387 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
380 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool 388 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] disallow_window bool
381 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2)) 389 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
382 390
383 val sql_query1 : free ::: {{Type}} 391 val sql_query1 : free ::: {{Type}}
384 -> afree ::: {{Type}} 392 -> afree ::: {{Type}}
385 -> tables ::: {{Type}} 393 -> tables ::: {{Type}}
391 => [free ~ grouped] 399 => [free ~ grouped]
392 => [afree ~ tables] 400 => [afree ~ tables]
393 => [empties ~ selectedFields] 401 => [empties ~ selectedFields]
394 => {Distinct : bool, 402 => {Distinct : bool,
395 From : sql_from_items free tables, 403 From : sql_from_items free tables,
396 Where : sql_exp (free ++ tables) afree [] bool, 404 Where : sql_exp (free ++ tables) afree [] disallow_window bool,
397 GroupBy : sql_subset tables grouped, 405 GroupBy : sql_subset tables grouped,
398 Having : sql_exp (free ++ grouped) (afree ++ tables) [] bool, 406 Having : sql_exp (free ++ grouped) (afree ++ tables) [] disallow_window bool,
399 SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields), 407 SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields),
400 SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) []) 408 SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) [] allow_window)
401 selectedExps) } 409 selectedExps) }
402 -> sql_query1 free afree tables selectedFields selectedExps 410 -> sql_query1 free afree tables selectedFields selectedExps
403 411
404 type sql_relop 412 type sql_relop
405 val sql_union : sql_relop 413 val sql_union : sql_relop
425 val sql_desc : sql_direction 433 val sql_desc : sql_direction
426 434
427 con sql_order_by :: {{Type}} -> {Type} -> Type 435 con sql_order_by :: {{Type}} -> {Type} -> Type
428 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps 436 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
429 val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type 437 val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
430 -> sql_exp tables [] exps t -> sql_direction 438 -> sql_exp tables [] exps allow_window t -> sql_direction
431 -> sql_order_by tables exps 439 -> sql_order_by tables exps
432 -> sql_order_by tables exps 440 -> sql_order_by tables exps
433 val sql_order_by_random : tables ::: {{Type}} -> exps ::: {Type} 441 val sql_order_by_random : tables ::: {{Type}} -> exps ::: {Type}
434 -> sql_order_by tables exps 442 -> sql_order_by tables exps
435 443
452 Limit : sql_limit, 460 Limit : sql_limit,
453 Offset : sql_offset} 461 Offset : sql_offset}
454 -> sql_query free afree selectedFields selectedExps 462 -> sql_query free afree selectedFields selectedExps
455 463
456 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} 464 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
457 -> fieldType ::: Type -> agg ::: {{Type}} 465 -> aw ::: {Unit} -> fieldType ::: Type -> agg ::: {{Type}}
458 -> exps ::: {Type} 466 -> exps ::: {Type}
459 -> tab :: Name -> field :: Name 467 -> tab :: Name -> field :: Name
460 -> sql_exp 468 -> sql_exp
461 ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) 469 ([tab = [field = fieldType] ++ otherFields] ++ otherTabs)
462 agg exps fieldType 470 agg exps aw fieldType
463 471
464 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type} 472 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> aw ::: {Unit} -> t ::: Type -> rest ::: {Type}
465 -> nm :: Name 473 -> nm :: Name
466 -> sql_exp tabs agg ([nm = t] ++ rest) t 474 -> sql_exp tabs agg ([nm = t] ++ rest) aw t
467 475
468 class sql_injectable 476 class sql_injectable
469 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t 477 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t
470 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t) 478 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)
471 479
472 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 480 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
473 -> t ::: Type 481 -> aw ::: {Unit} -> t ::: Type
474 -> sql_injectable t -> t -> sql_exp tables agg exps t 482 -> sql_injectable t -> t -> sql_exp tables agg exps aw t
475 483
476 val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 484 val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
477 -> t ::: Type 485 -> aw ::: {Unit} -> t ::: Type
478 -> sql_exp tables agg exps (option t) 486 -> sql_exp tables agg exps aw (option t)
479 -> sql_exp tables agg exps bool 487 -> sql_exp tables agg exps aw bool
480 488
481 val sql_coalesce : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 489 val sql_coalesce : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
482 -> t ::: Type 490 -> aw ::: {Unit} -> t ::: Type
483 -> sql_exp tables agg exps (option t) 491 -> sql_exp tables agg exps aw (option t)
484 -> sql_exp tables agg exps t 492 -> sql_exp tables agg exps aw t
485 -> sql_exp tables agg exps t 493 -> sql_exp tables agg exps aw t
486 494
487 val sql_if_then_else : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 495 val sql_if_then_else : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
488 -> t ::: Type 496 -> aw ::: {Unit} -> t ::: Type
489 -> sql_exp tables agg exps bool 497 -> sql_exp tables agg exps aw bool
490 -> sql_exp tables agg exps t 498 -> sql_exp tables agg exps aw t
491 -> sql_exp tables agg exps t 499 -> sql_exp tables agg exps aw t
492 -> sql_exp tables agg exps t 500 -> sql_exp tables agg exps aw t
493 501
494 class sql_arith 502 class sql_arith
495 val sql_arith_int : sql_arith int 503 val sql_arith_int : sql_arith int
496 val sql_arith_float : sql_arith float 504 val sql_arith_float : sql_arith float
497 val sql_arith_option : t ::: Type -> sql_arith t -> sql_arith (option t) 505 val sql_arith_option : t ::: Type -> sql_arith t -> sql_arith (option t)
498 506
499 con sql_unary :: Type -> Type -> Type 507 con sql_unary :: Type -> Type -> Type
500 val sql_not : sql_unary bool bool 508 val sql_not : sql_unary bool bool
501 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 509 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
502 -> arg ::: Type -> res ::: Type 510 -> aw ::: {Unit} -> arg ::: Type -> res ::: Type
503 -> sql_unary arg res -> sql_exp tables agg exps arg 511 -> sql_unary arg res -> sql_exp tables agg exps aw arg
504 -> sql_exp tables agg exps res 512 -> sql_exp tables agg exps aw res
505 513
506 val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t 514 val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t
507 515
508 con sql_binary :: Type -> Type -> Type -> Type 516 con sql_binary :: Type -> Type -> Type -> Type
509 val sql_and : sql_binary bool bool bool 517 val sql_and : sql_binary bool bool bool
510 val sql_or : sql_binary bool bool bool 518 val sql_or : sql_binary bool bool bool
511 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 519 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
512 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type 520 -> aw ::: {Unit} -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
513 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1 521 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps aw arg1
514 -> sql_exp tables agg exps arg2 522 -> sql_exp tables agg exps aw arg2
515 -> sql_exp tables agg exps res 523 -> sql_exp tables agg exps aw res
516 524
517 val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t 525 val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t
518 val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t 526 val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t
519 val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t 527 val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t
520 val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t 528 val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t
527 val sql_gt : t ::: Type -> sql_binary t t bool 535 val sql_gt : t ::: Type -> sql_binary t t bool
528 val sql_ge : t ::: Type -> sql_binary t t bool 536 val sql_ge : t ::: Type -> sql_binary t t bool
529 537
530 val sql_like : sql_binary string string bool 538 val sql_like : sql_binary string string bool
531 539
532 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 540 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit}
533 -> sql_exp tables agg exps int 541 -> sql_exp tables agg exps aw int
534 542
535 con sql_aggregate :: Type -> Type -> Type 543 con sql_aggregate :: Type -> Type -> Type
536 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 544 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
537 -> dom ::: Type -> ran ::: Type 545 -> aw ::: {Unit} -> dom ::: Type -> ran ::: Type
538 -> sql_aggregate dom ran -> sql_exp agg agg exps dom 546 -> sql_aggregate dom ran -> sql_exp agg agg exps aw dom
539 -> sql_exp tables agg exps ran 547 -> sql_exp tables agg exps aw ran
540 548
541 val sql_count_col : t ::: Type -> sql_aggregate (option t) int 549 val sql_count_col : t ::: Type -> sql_aggregate (option t) int
542 550
543 class sql_summable 551 class sql_summable
544 val sql_summable_int : sql_summable int 552 val sql_summable_int : sql_summable int
556 val sql_max : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt 564 val sql_max : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
557 val sql_min : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt 565 val sql_min : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
558 566
559 con sql_nfunc :: Type -> Type 567 con sql_nfunc :: Type -> Type
560 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 568 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
561 -> t ::: Type 569 -> aw ::: {Unit} -> t ::: Type
562 -> sql_nfunc t -> sql_exp tables agg exps t 570 -> sql_nfunc t -> sql_exp tables agg exps aw t
563 val sql_current_timestamp : sql_nfunc time 571 val sql_current_timestamp : sql_nfunc time
564 572
565 con sql_ufunc :: Type -> Type -> Type 573 con sql_ufunc :: Type -> Type -> Type
566 val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 574 val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
567 -> dom ::: Type -> ran ::: Type 575 -> aw ::: {Unit} -> dom ::: Type -> ran ::: Type
568 -> sql_ufunc dom ran -> sql_exp tables agg exps dom 576 -> sql_ufunc dom ran -> sql_exp tables agg exps aw dom
569 -> sql_exp tables agg exps ran 577 -> sql_exp tables agg exps aw ran
570 val sql_octet_length : sql_ufunc blob int 578 val sql_octet_length : sql_ufunc blob int
571 val sql_known : t ::: Type -> sql_ufunc t bool 579 val sql_known : t ::: Type -> sql_ufunc t bool
572 val sql_lower : sql_ufunc string string 580 val sql_lower : sql_ufunc string string
573 val sql_upper : sql_ufunc string string 581 val sql_upper : sql_ufunc string string
574 582
575 val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type 583 val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} -> t ::: Type
576 -> sql_injectable_prim t 584 -> sql_injectable_prim t
577 -> sql_exp tables agg exps t 585 -> sql_exp tables agg exps aw t
578 -> sql_exp tables agg exps (option t) 586 -> sql_exp tables agg exps aw (option t)
579 587
580 val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type -> nt ::: Type 588 val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> aw ::: {Unit} -> t ::: Type -> nt ::: Type
581 -> nullify t nt 589 -> nullify t nt
582 -> sql_query tables agg [] [nm = t] 590 -> sql_query tables agg [] [nm = t]
583 -> sql_exp tables agg exps nt 591 -> sql_exp tables agg exps aw nt
584 592
585 (*** Executing queries *) 593 (*** Executing queries *)
586 594
587 val query : tables ::: {{Type}} -> exps ::: {Type} 595 val query : tables ::: {{Type}} -> exps ::: {Type}
588 -> [tables ~ exps] => 596 -> [tables ~ exps] =>
602 val tryDml : dml -> transaction (option string) 610 val tryDml : dml -> transaction (option string)
603 (* Returns an error message on failure. *) 611 (* Returns an error message on failure. *)
604 612
605 val insert : fields ::: {Type} -> uniques ::: {{Unit}} 613 val insert : fields ::: {Type} -> uniques ::: {{Unit}}
606 -> sql_table fields uniques 614 -> sql_table fields uniques
607 -> $(map (fn t :: Type => sql_exp [] [] [] t) fields) 615 -> $(map (fn t :: Type => sql_exp [] [] [] disallow_window t) fields)
608 -> dml 616 -> dml
609 617
610 val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} -> 618 val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} ->
611 [changed ~ unchanged] => 619 [changed ~ unchanged] =>
612 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed) 620 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] disallow_window t) changed)
613 -> sql_table (changed ++ unchanged) uniques 621 -> sql_table (changed ++ unchanged) uniques
614 -> sql_exp [T = changed ++ unchanged] [] [] bool 622 -> sql_exp [T = changed ++ unchanged] [] [] disallow_window bool
615 -> dml 623 -> dml
616 624
617 val delete : fields ::: {Type} -> uniques ::: {{Unit}} 625 val delete : fields ::: {Type} -> uniques ::: {{Unit}}
618 -> sql_table fields uniques 626 -> sql_table fields uniques
619 -> sql_exp [T = fields] [] [] bool 627 -> sql_exp [T = fields] [] [] disallow_window bool
620 -> dml 628 -> dml
621 629
622 (*** Sequences *) 630 (*** Sequences *)
623 631
624 type sql_sequence 632 type sql_sequence