Mercurial > urweb

comparison lib/ur/basis.urs @ 1778:818d4097e2ed

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Lighter-weight encoding of window function use
author Adam Chlipala <adam@chlipala.net>
date Sun, 03 Jun 2012 11:29:31 -0400
parents 59b07fdae1ff
children 5bc4fbf9c0fe
comparison
equal deleted inserted replaced
1777:59b07fdae1ff 1778:818d4097e2ed
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 allow_window :: {Unit} 308 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
309 con disallow_window :: {Unit} 309 val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
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
318 -> fs' ::: {{Type}} -> agg' ::: {{Type}} -> exps' ::: {Type} 310 -> fs' ::: {{Type}} -> agg' ::: {{Type}} -> exps' ::: {Type}
319 -> [fs ~ fs'] => [agg ~ agg'] => [exps ~ exps'] => 311 -> [fs ~ fs'] => [agg ~ agg'] => [exps ~ exps'] =>
320 sql_exp fs agg exps aw t 312 sql_exp fs agg exps t
321 -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') aw t 313 -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') t
322 314
323 val check : fs ::: {Type} 315 val check : fs ::: {Type}
324 -> sql_exp [] [] fs disallow_window bool 316 -> sql_exp [] [] fs bool
325 -> sql_constraint fs [] 317 -> sql_constraint fs []
326 318
327 319
328 (*** Queries *) 320 (*** Queries *)
329 321
357 => sql_from_items free tabs1 -> sql_from_items free tabs2 349 => sql_from_items free tabs1 -> sql_from_items free tabs2
358 -> sql_from_items free (tabs1 ++ tabs2) 350 -> sql_from_items free (tabs1 ++ tabs2)
359 val sql_inner_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}} 351 val sql_inner_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
360 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2] 352 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
361 => sql_from_items free tabs1 -> sql_from_items free tabs2 353 => sql_from_items free tabs1 -> sql_from_items free tabs2
362 -> sql_exp (free ++ tabs1 ++ tabs2) [] [] disallow_window bool 354 -> sql_exp (free ++ tabs1 ++ tabs2) [] [] bool
363 -> sql_from_items free (tabs1 ++ tabs2) 355 -> sql_from_items free (tabs1 ++ tabs2)
364 356
365 class nullify :: Type -> Type -> Type 357 class nullify :: Type -> Type -> Type
366 val nullify_option : t ::: Type -> nullify (option t) (option t) 358 val nullify_option : t ::: Type -> nullify (option t) (option t)
367 val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t) 359 val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t)
368 360
369 val sql_left_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}} 361 val sql_left_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}}
370 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2] 362 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
371 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2) 363 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2)
372 -> sql_from_items free tabs1 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2) 364 -> sql_from_items free tabs1 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
373 -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] disallow_window bool 365 -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool
374 -> sql_from_items free (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2) 366 -> sql_from_items free (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
375 367
376 val sql_right_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}} 368 val sql_right_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}}
377 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2] 369 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
378 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1) 370 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1)
379 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items free tabs2 371 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items free tabs2
380 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] disallow_window bool 372 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool
381 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2) 373 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
382 374
383 val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}} 375 val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
384 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2] 376 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
385 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2)) 377 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2))
386 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) 378 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1)
387 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2) 379 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
388 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] disallow_window bool 380 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool
389 -> 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))
382
383 (** [ORDER BY] and [SELECT] expressions may use window functions, so we introduce a type family for such expressions. *)
384 con sql_expw :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
390 385
391 val sql_query1 : free ::: {{Type}} 386 val sql_query1 : free ::: {{Type}}
392 -> afree ::: {{Type}} 387 -> afree ::: {{Type}}
393 -> tables ::: {{Type}} 388 -> tables ::: {{Type}}
394 -> grouped ::: {{Type}} 389 -> grouped ::: {{Type}}
399 => [free ~ grouped] 394 => [free ~ grouped]
400 => [afree ~ tables] 395 => [afree ~ tables]
401 => [empties ~ selectedFields] 396 => [empties ~ selectedFields]
402 => {Distinct : bool, 397 => {Distinct : bool,
403 From : sql_from_items free tables, 398 From : sql_from_items free tables,
404 Where : sql_exp (free ++ tables) afree [] disallow_window bool, 399 Where : sql_exp (free ++ tables) afree [] bool,
405 GroupBy : sql_subset tables grouped, 400 GroupBy : sql_subset tables grouped,
406 Having : sql_exp (free ++ grouped) (afree ++ tables) [] disallow_window bool, 401 Having : sql_exp (free ++ grouped) (afree ++ tables) [] bool,
407 SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields), 402 SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields),
408 SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) [] allow_window) 403 SelectExps : $(map (sql_expw (free ++ grouped) (afree ++ tables) [])
409 selectedExps) } 404 selectedExps) }
410 -> sql_query1 free afree tables selectedFields selectedExps 405 -> sql_query1 free afree tables selectedFields selectedExps
411 406
412 type sql_relop 407 type sql_relop
413 val sql_union : sql_relop 408 val sql_union : sql_relop
430 425
431 type sql_direction 426 type sql_direction
432 val sql_asc : sql_direction 427 val sql_asc : sql_direction
433 val sql_desc : sql_direction 428 val sql_desc : sql_direction
434 429
430 (** This type class supports automatic injection of either regular or window expressions into [sql_expw]. *)
431 class sql_window :: ({{Type}} -> {{Type}} -> {Type} -> Type -> Type) -> Type
432 val sql_window_normal : sql_window sql_exp
433 val sql_window_fancy : sql_window sql_expw
434 val sql_window : tf ::: ({{Type}} -> {{Type}} -> {Type} -> Type -> Type)
435 -> tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
436 -> sql_window tf
437 -> tf tables agg exps t
438 -> sql_expw tables agg exps t
439
435 con sql_order_by :: {{Type}} -> {Type} -> Type 440 con sql_order_by :: {{Type}} -> {Type} -> Type
436 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps 441 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
437 val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type 442 val sql_order_by_Cons : tf ::: ({{Type}} -> {{Type}} -> {Type} -> Type -> Type) -> tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
438 -> sql_exp tables [] exps allow_window t -> sql_direction 443 -> sql_window tf
444 -> tf tables [] exps t -> sql_direction
439 -> sql_order_by tables exps 445 -> sql_order_by tables exps
440 -> sql_order_by tables exps 446 -> sql_order_by tables exps
441 val sql_order_by_random : tables ::: {{Type}} -> exps ::: {Type} 447 val sql_order_by_random : tables ::: {{Type}} -> exps ::: {Type}
442 -> sql_order_by tables exps 448 -> sql_order_by tables exps
443 449
460 Limit : sql_limit, 466 Limit : sql_limit,
461 Offset : sql_offset} 467 Offset : sql_offset}
462 -> sql_query free afree selectedFields selectedExps 468 -> sql_query free afree selectedFields selectedExps
463 469
464 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} 470 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
465 -> aw ::: {Unit} -> fieldType ::: Type -> agg ::: {{Type}} 471 -> fieldType ::: Type -> agg ::: {{Type}}
466 -> exps ::: {Type} 472 -> exps ::: {Type}
467 -> tab :: Name -> field :: Name 473 -> tab :: Name -> field :: Name
468 -> sql_exp 474 -> sql_exp
469 ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) 475 ([tab = [field = fieldType] ++ otherFields] ++ otherTabs)
470 agg exps aw fieldType 476 agg exps fieldType
471 477
472 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> aw ::: {Unit} -> t ::: Type -> rest ::: {Type} 478 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type}
473 -> nm :: Name 479 -> nm :: Name
474 -> sql_exp tabs agg ([nm = t] ++ rest) aw t 480 -> sql_exp tabs agg ([nm = t] ++ rest) t
475 481
476 class sql_injectable 482 class sql_injectable
477 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t 483 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t
478 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t) 484 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)
479 485
480 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 486 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
481 -> aw ::: {Unit} -> t ::: Type 487 -> t ::: Type
482 -> sql_injectable t -> t -> sql_exp tables agg exps aw t 488 -> sql_injectable t -> t -> sql_exp tables agg exps t
483 489
484 val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 490 val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
485 -> aw ::: {Unit} -> t ::: Type 491 -> t ::: Type
486 -> sql_exp tables agg exps aw (option t) 492 -> sql_exp tables agg exps (option t)
487 -> sql_exp tables agg exps aw bool 493 -> sql_exp tables agg exps bool
488 494
489 val sql_coalesce : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 495 val sql_coalesce : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
490 -> aw ::: {Unit} -> t ::: Type 496 -> t ::: Type
491 -> sql_exp tables agg exps aw (option t) 497 -> sql_exp tables agg exps (option t)
492 -> sql_exp tables agg exps aw t 498 -> sql_exp tables agg exps t
493 -> sql_exp tables agg exps aw t 499 -> sql_exp tables agg exps t
494 500
495 val sql_if_then_else : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 501 val sql_if_then_else : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
496 -> aw ::: {Unit} -> t ::: Type 502 -> t ::: Type
497 -> sql_exp tables agg exps aw bool 503 -> sql_exp tables agg exps bool
498 -> sql_exp tables agg exps aw t 504 -> sql_exp tables agg exps t
499 -> sql_exp tables agg exps aw t 505 -> sql_exp tables agg exps t
500 -> sql_exp tables agg exps aw t 506 -> sql_exp tables agg exps t
501 507
502 class sql_arith 508 class sql_arith
503 val sql_arith_int : sql_arith int 509 val sql_arith_int : sql_arith int
504 val sql_arith_float : sql_arith float 510 val sql_arith_float : sql_arith float
505 val sql_arith_option : t ::: Type -> sql_arith t -> sql_arith (option t) 511 val sql_arith_option : t ::: Type -> sql_arith t -> sql_arith (option t)
506 512
507 con sql_unary :: Type -> Type -> Type 513 con sql_unary :: Type -> Type -> Type
508 val sql_not : sql_unary bool bool 514 val sql_not : sql_unary bool bool
509 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 515 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
510 -> aw ::: {Unit} -> arg ::: Type -> res ::: Type 516 -> arg ::: Type -> res ::: Type
511 -> sql_unary arg res -> sql_exp tables agg exps aw arg 517 -> sql_unary arg res -> sql_exp tables agg exps arg
512 -> sql_exp tables agg exps aw res 518 -> sql_exp tables agg exps res
513 519
514 val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t 520 val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t
515 521
516 con sql_binary :: Type -> Type -> Type -> Type 522 con sql_binary :: Type -> Type -> Type -> Type
517 val sql_and : sql_binary bool bool bool 523 val sql_and : sql_binary bool bool bool
518 val sql_or : sql_binary bool bool bool 524 val sql_or : sql_binary bool bool bool
519 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 525 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
520 -> aw ::: {Unit} -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type 526 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
521 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps aw arg1 527 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1
522 -> sql_exp tables agg exps aw arg2 528 -> sql_exp tables agg exps arg2
523 -> sql_exp tables agg exps aw res 529 -> sql_exp tables agg exps res
524 530
525 val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t 531 val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t
526 val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t 532 val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t
527 val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t 533 val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t
528 val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t 534 val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t
535 val sql_gt : t ::: Type -> sql_binary t t bool 541 val sql_gt : t ::: Type -> sql_binary t t bool
536 val sql_ge : t ::: Type -> sql_binary t t bool 542 val sql_ge : t ::: Type -> sql_binary t t bool
537 543
538 val sql_like : sql_binary string string bool 544 val sql_like : sql_binary string string bool
539 545
540 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} 546 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
541 -> sql_exp tables agg exps aw int 547 -> sql_exp tables agg exps int
542 548
543 con sql_aggregate :: Type -> Type -> Type 549 con sql_aggregate :: Type -> Type -> Type
544 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 550 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
545 -> aw ::: {Unit} -> dom ::: Type -> ran ::: Type 551 -> dom ::: Type -> ran ::: Type
546 -> sql_aggregate dom ran -> sql_exp agg agg exps aw dom 552 -> sql_aggregate dom ran -> sql_exp agg agg exps dom
547 -> sql_exp tables agg exps aw ran 553 -> sql_exp tables agg exps ran
548 554
549 val sql_count_col : t ::: Type -> sql_aggregate (option t) int 555 val sql_count_col : t ::: Type -> sql_aggregate (option t) int
550 556
551 class sql_summable 557 class sql_summable
552 val sql_summable_int : sql_summable int 558 val sql_summable_int : sql_summable int
562 val sql_maxable_time : sql_maxable time 568 val sql_maxable_time : sql_maxable time
563 val sql_maxable_option : t ::: Type -> sql_maxable t -> sql_maxable (option t) 569 val sql_maxable_option : t ::: Type -> sql_maxable t -> sql_maxable (option t)
564 val sql_max : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt 570 val sql_max : 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 571 val sql_min : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
566 572
573 con sql_nfunc :: Type -> Type
574 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
575 -> t ::: Type
576 -> sql_nfunc t -> sql_exp tables agg exps t
577 val sql_current_timestamp : sql_nfunc time
578
579 con sql_ufunc :: Type -> Type -> Type
580 val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
581 -> dom ::: Type -> ran ::: Type
582 -> sql_ufunc dom ran -> sql_exp tables agg exps dom
583 -> sql_exp tables agg exps ran
584 val sql_octet_length : sql_ufunc blob int
585 val sql_known : t ::: Type -> sql_ufunc t bool
586 val sql_lower : sql_ufunc string string
587 val sql_upper : sql_ufunc string string
588
589 val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
590 -> sql_injectable_prim t
591 -> sql_exp tables agg exps t
592 -> sql_exp tables agg exps (option t)
593
594 val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type -> nt ::: Type
595 -> nullify t nt
596 -> sql_query tables agg [] [nm = t]
597 -> sql_exp tables agg exps nt
598
599 (** Window function expressions *)
600
567 con sql_partition :: {{Type}} -> {{Type}} -> {Type} -> Type 601 con sql_partition :: {{Type}} -> {{Type}} -> {Type} -> Type
568 val sql_no_partition : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 602 val sql_no_partition : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
569 -> sql_partition tables agg exps 603 -> sql_partition tables agg exps
570 val sql_partition : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type 604 val sql_partition : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
571 -> sql_exp tables agg exps disallow_window t 605 -> sql_exp tables agg exps t
572 -> sql_partition tables agg exps 606 -> sql_partition tables agg exps
573 607
574 con sql_window :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type 608 con sql_window_function :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
575 val sql_window : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 609 val sql_window_function : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
576 -> t ::: Type 610 -> t ::: Type
577 -> sql_window tables agg exps t 611 -> sql_window_function tables agg exps t
578 -> sql_partition tables agg exps 612 -> sql_partition tables agg exps
579 -> sql_order_by tables exps 613 -> sql_order_by tables exps
580 -> sql_exp tables agg exps allow_window t 614 -> sql_expw tables agg exps t
581 615
582 val sql_window_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 616 val sql_window_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
583 -> t ::: Type -> nt ::: Type 617 -> t ::: Type -> nt ::: Type
584 -> sql_aggregate t nt 618 -> sql_aggregate t nt
585 -> sql_exp tables agg exps disallow_window t 619 -> sql_exp tables agg exps t
586 -> sql_window tables agg exps nt 620 -> sql_window_function tables agg exps nt
587 val sql_window_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 621 val sql_window_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
588 -> sql_window tables agg exps int 622 -> sql_window_function tables agg exps int
589 val sql_window_rank : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 623 val sql_rank : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
590 -> sql_window tables agg exps int 624 -> sql_window_function tables agg exps int
591 625
592 con sql_nfunc :: Type -> Type
593 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
594 -> aw ::: {Unit} -> t ::: Type
595 -> sql_nfunc t -> sql_exp tables agg exps aw t
596 val sql_current_timestamp : sql_nfunc time
597
598 con sql_ufunc :: Type -> Type -> Type
599 val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
600 -> aw ::: {Unit} -> dom ::: Type -> ran ::: Type
601 -> sql_ufunc dom ran -> sql_exp tables agg exps aw dom
602 -> sql_exp tables agg exps aw ran
603 val sql_octet_length : sql_ufunc blob int
604 val sql_known : t ::: Type -> sql_ufunc t bool
605 val sql_lower : sql_ufunc string string
606 val sql_upper : sql_ufunc string string
607
608 val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} -> t ::: Type
609 -> sql_injectable_prim t
610 -> sql_exp tables agg exps aw t
611 -> sql_exp tables agg exps aw (option t)
612
613 val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> aw ::: {Unit} -> t ::: Type -> nt ::: Type
614 -> nullify t nt
615 -> sql_query tables agg [] [nm = t]
616 -> sql_exp tables agg exps aw nt
617 626
618 (*** Executing queries *) 627 (*** Executing queries *)
619 628
620 val query : tables ::: {{Type}} -> exps ::: {Type} 629 val query : tables ::: {{Type}} -> exps ::: {Type}
621 -> [tables ~ exps] => 630 -> [tables ~ exps] =>
635 val tryDml : dml -> transaction (option string) 644 val tryDml : dml -> transaction (option string)
636 (* Returns an error message on failure. *) 645 (* Returns an error message on failure. *)
637 646
638 val insert : fields ::: {Type} -> uniques ::: {{Unit}} 647 val insert : fields ::: {Type} -> uniques ::: {{Unit}}
639 -> sql_table fields uniques 648 -> sql_table fields uniques
640 -> $(map (fn t :: Type => sql_exp [] [] [] disallow_window t) fields) 649 -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
641 -> dml 650 -> dml
642 651
643 val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} -> 652 val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} ->
644 [changed ~ unchanged] => 653 [changed ~ unchanged] =>
645 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] disallow_window t) changed) 654 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
646 -> sql_table (changed ++ unchanged) uniques 655 -> sql_table (changed ++ unchanged) uniques
647 -> sql_exp [T = changed ++ unchanged] [] [] disallow_window bool 656 -> sql_exp [T = changed ++ unchanged] [] [] bool
648 -> dml 657 -> dml
649 658
650 val delete : fields ::: {Type} -> uniques ::: {{Unit}} 659 val delete : fields ::: {Type} -> uniques ::: {{Unit}}
651 -> sql_table fields uniques 660 -> sql_table fields uniques
652 -> sql_exp [T = fields] [] [] disallow_window bool 661 -> sql_exp [T = fields] [] [] bool
653 -> dml 662 -> dml
654 663
655 (*** Sequences *) 664 (*** Sequences *)
656 665
657 type sql_sequence 666 type sql_sequence