Mercurial > urweb

comparison lib/ur/basis.urs @ 1394:d328983dc5a6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Allow subqueries to reference aggregate-only columns of free tables; treat non-COUNT aggregate functions as possibly returning NULL
author Adam Chlipala <adam@chlipala.net>
date Sat, 15 Jan 2011 14:53:13 -0500
parents 65fbb250b875
children 5f4fee8a4dcd
comparison
equal deleted inserted replaced
1393:802c179dac1f 1394:d328983dc5a6
289 -> sql_constraint fs [] 289 -> sql_constraint fs []
290 290
291 291
292 (*** Queries *) 292 (*** Queries *)
293 293
294 con sql_query :: {{Type}} -> {{Type}} -> {Type} -> Type 294 con sql_query :: {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
295 con sql_query1 :: {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type 295 con sql_query1 :: {{Type}} -> {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
296 296
297 con sql_subset :: {{Type}} -> {{Type}} -> Type 297 con sql_subset :: {{Type}} -> {{Type}} -> Type
298 val sql_subset : keep_drop :: {({Type} * {Type})} 298 val sql_subset : keep_drop :: {({Type} * {Type})}
299 -> sql_subset 299 -> sql_subset
300 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop) 300 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop)
312 val sql_from_nil : free ::: {{Type}} -> sql_from_items free [] 312 val sql_from_nil : free ::: {{Type}} -> sql_from_items free []
313 val sql_from_table : free ::: {{Type}} -> t ::: Type -> fs ::: {Type} 313 val sql_from_table : free ::: {{Type}} -> t ::: Type -> fs ::: {Type}
314 -> fieldsOf t fs -> name :: Name 314 -> fieldsOf t fs -> name :: Name
315 -> t -> sql_from_items free [name = fs] 315 -> t -> sql_from_items free [name = fs]
316 val sql_from_query : free ::: {{Type}} -> fs ::: {Type} -> name :: Name 316 val sql_from_query : free ::: {{Type}} -> fs ::: {Type} -> name :: Name
317 -> sql_query free [] fs 317 -> sql_query free [] [] fs
318 -> sql_from_items free [name = fs] 318 -> sql_from_items free [name = fs]
319 val sql_from_comma : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}} 319 val sql_from_comma : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
320 -> [tabs1 ~ tabs2] 320 -> [tabs1 ~ tabs2]
321 => sql_from_items free tabs1 -> sql_from_items free tabs2 321 => sql_from_items free tabs1 -> sql_from_items free tabs2
322 -> sql_from_items free (tabs1 ++ tabs2) 322 -> sql_from_items free (tabs1 ++ tabs2)
351 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2) 351 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
352 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool 352 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool
353 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2)) 353 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
354 354
355 val sql_query1 : free ::: {{Type}} 355 val sql_query1 : free ::: {{Type}}
356 -> afree ::: {{Type}}
356 -> tables ::: {{Type}} 357 -> tables ::: {{Type}}
357 -> grouped ::: {{Type}} 358 -> grouped ::: {{Type}}
358 -> selectedFields ::: {{Type}} 359 -> selectedFields ::: {{Type}}
359 -> selectedExps ::: {Type} 360 -> selectedExps ::: {Type}
360 -> empties :: {Unit} 361 -> empties :: {Unit}
361 -> [free ~ tables] 362 -> [free ~ tables]
362 => [free ~ grouped] 363 => [free ~ grouped]
364 => [afree ~ tables]
363 => [empties ~ selectedFields] 365 => [empties ~ selectedFields]
364 => {Distinct : bool, 366 => {Distinct : bool,
365 From : sql_from_items free tables, 367 From : sql_from_items free tables,
366 Where : sql_exp (free ++ tables) [] [] bool, 368 Where : sql_exp (free ++ tables) afree [] bool,
367 GroupBy : sql_subset tables grouped, 369 GroupBy : sql_subset tables grouped,
368 Having : sql_exp (free ++ grouped) tables [] bool, 370 Having : sql_exp (free ++ grouped) (afree ++ tables) [] bool,
369 SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields), 371 SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields),
370 SelectExps : $(map (sql_exp (free ++ grouped) tables []) 372 SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) [])
371 selectedExps) } 373 selectedExps) }
372 -> sql_query1 free tables selectedFields selectedExps 374 -> sql_query1 free afree tables selectedFields selectedExps
373 375
374 type sql_relop 376 type sql_relop
375 val sql_union : sql_relop 377 val sql_union : sql_relop
376 val sql_intersect : sql_relop 378 val sql_intersect : sql_relop
377 val sql_except : sql_relop 379 val sql_except : sql_relop
378 val sql_relop : free ::: {{Type}} 380 val sql_relop : free ::: {{Type}}
381 -> afree ::: {{Type}}
379 -> tables1 ::: {{Type}} 382 -> tables1 ::: {{Type}}
380 -> tables2 ::: {{Type}} 383 -> tables2 ::: {{Type}}
381 -> selectedFields ::: {{Type}} 384 -> selectedFields ::: {{Type}}
382 -> selectedExps ::: {Type} 385 -> selectedExps ::: {Type}
383 -> sql_relop 386 -> sql_relop
384 -> sql_query1 free tables1 selectedFields selectedExps 387 -> sql_query1 free afree tables1 selectedFields selectedExps
385 -> sql_query1 free tables2 selectedFields selectedExps 388 -> sql_query1 free afree tables2 selectedFields selectedExps
386 -> sql_query1 free [] selectedFields selectedExps 389 -> sql_query1 free afree [] selectedFields selectedExps
387 val sql_forget_tables : free ::: {{Type}} -> tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type} 390 val sql_forget_tables : free ::: {{Type}} -> afree ::: {{Type}} -> tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type}
388 -> sql_query1 free tables selectedFields selectedExps 391 -> sql_query1 free afree tables selectedFields selectedExps
389 -> sql_query1 free [] selectedFields selectedExps 392 -> sql_query1 free afree [] selectedFields selectedExps
390 393
391 type sql_direction 394 type sql_direction
392 val sql_asc : sql_direction 395 val sql_asc : sql_direction
393 val sql_desc : sql_direction 396 val sql_desc : sql_direction
394 397
406 type sql_offset 409 type sql_offset
407 val sql_no_offset : sql_offset 410 val sql_no_offset : sql_offset
408 val sql_offset : int -> sql_offset 411 val sql_offset : int -> sql_offset
409 412
410 val sql_query : free ::: {{Type}} 413 val sql_query : free ::: {{Type}}
414 -> afree ::: {{Type}}
411 -> tables ::: {{Type}} 415 -> tables ::: {{Type}}
412 -> selectedFields ::: {{Type}} 416 -> selectedFields ::: {{Type}}
413 -> selectedExps ::: {Type} 417 -> selectedExps ::: {Type}
414 -> [free ~ tables] 418 -> [free ~ tables]
415 => {Rows : sql_query1 free tables selectedFields selectedExps, 419 => {Rows : sql_query1 free afree tables selectedFields selectedExps,
416 OrderBy : sql_order_by (free ++ tables) selectedExps, 420 OrderBy : sql_order_by (free ++ tables) selectedExps,
417 Limit : sql_limit, 421 Limit : sql_limit,
418 Offset : sql_offset} 422 Offset : sql_offset}
419 -> sql_query free selectedFields selectedExps 423 -> sql_query free afree selectedFields selectedExps
420 424
421 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} 425 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
422 -> fieldType ::: Type -> agg ::: {{Type}} 426 -> fieldType ::: Type -> agg ::: {{Type}}
423 -> exps ::: {Type} 427 -> exps ::: {Type}
424 -> tab :: Name -> field :: Name 428 -> tab :: Name -> field :: Name
491 495
492 class sql_summable 496 class sql_summable
493 val sql_summable_int : sql_summable int 497 val sql_summable_int : sql_summable int
494 val sql_summable_float : sql_summable float 498 val sql_summable_float : sql_summable float
495 val sql_summable_option : t ::: Type -> sql_summable t -> sql_summable (option t) 499 val sql_summable_option : t ::: Type -> sql_summable t -> sql_summable (option t)
496 val sql_avg : t ::: Type -> sql_summable t -> sql_aggregate t t 500 val sql_avg : t ::: Type -> nt ::: Type -> sql_summable t -> nullify t nt -> sql_aggregate t nt
497 val sql_sum : t ::: Type -> sql_summable t -> sql_aggregate t t 501 val sql_sum : t ::: Type -> nt ::: Type -> sql_summable t -> nullify t nt -> sql_aggregate t nt
498 502
499 class sql_maxable 503 class sql_maxable
500 val sql_maxable_int : sql_maxable int 504 val sql_maxable_int : sql_maxable int
501 val sql_maxable_float : sql_maxable float 505 val sql_maxable_float : sql_maxable float
502 val sql_maxable_string : sql_maxable string 506 val sql_maxable_string : sql_maxable string
503 val sql_maxable_time : sql_maxable time 507 val sql_maxable_time : sql_maxable time
504 val sql_maxable_option : t ::: Type -> sql_maxable t -> sql_maxable (option t) 508 val sql_maxable_option : t ::: Type -> sql_maxable t -> sql_maxable (option t)
505 val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t t 509 val sql_max : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
506 val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t t 510 val sql_min : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
507 511
508 con sql_nfunc :: Type -> Type 512 con sql_nfunc :: Type -> Type
509 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 513 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
510 -> t ::: Type 514 -> t ::: Type
511 -> sql_nfunc t -> sql_exp tables agg exps t 515 -> sql_nfunc t -> sql_exp tables agg exps t
524 -> sql_injectable_prim t 528 -> sql_injectable_prim t
525 -> sql_exp tables agg exps t 529 -> sql_exp tables agg exps t
526 -> sql_exp tables agg exps (option t) 530 -> sql_exp tables agg exps (option t)
527 531
528 val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type 532 val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type
529 -> sql_query tables [] [nm = t] 533 -> sql_query tables agg [] [nm = t]
530 -> sql_exp tables agg exps t 534 -> sql_exp tables agg exps t
531 535
532 (*** Executing queries *) 536 (*** Executing queries *)
533 537
534 val query : tables ::: {{Type}} -> exps ::: {Type} 538 val query : tables ::: {{Type}} -> exps ::: {Type}
535 -> [tables ~ exps] => 539 -> [tables ~ exps] =>
536 state ::: Type 540 state ::: Type
537 -> sql_query [] tables exps 541 -> sql_query [] [] tables exps
538 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) 542 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
539 -> state 543 -> state
540 -> transaction state) 544 -> transaction state)
541 -> state 545 -> state
542 -> transaction state 546 -> transaction state
836 (** Information flow security *) 840 (** Information flow security *)
837 841
838 type sql_policy 842 type sql_policy
839 843
840 val sendClient : tables ::: {{Type}} -> exps ::: {Type} 844 val sendClient : tables ::: {{Type}} -> exps ::: {Type}
841 -> [tables ~ exps] => sql_query [] tables exps 845 -> [tables ~ exps] => sql_query [] [] tables exps
842 -> sql_policy 846 -> sql_policy
843 847
844 val sendOwnIds : sql_sequence -> sql_policy 848 val sendOwnIds : sql_sequence -> sql_policy
845 849
846 val mayInsert : fs ::: {Type} -> tables ::: {{Type}} -> [[New] ~ tables] 850 val mayInsert : fs ::: {Type} -> tables ::: {{Type}} -> [[New] ~ tables]
847 => sql_query [] ([New = fs] ++ tables) [] 851 => sql_query [] [] ([New = fs] ++ tables) []
848 -> sql_policy 852 -> sql_policy
849 853
850 val mayDelete : fs ::: {Type} -> tables ::: {{Type}} -> [[Old] ~ tables] 854 val mayDelete : fs ::: {Type} -> tables ::: {{Type}} -> [[Old] ~ tables]
851 => sql_query [] ([Old = fs] ++ tables) [] 855 => sql_query [] [] ([Old = fs] ++ tables) []
852 -> sql_policy 856 -> sql_policy
853 857
854 val mayUpdate : fs ::: {Type} -> tables ::: {{Type}} -> [[Old, New] ~ tables] 858 val mayUpdate : fs ::: {Type} -> tables ::: {{Type}} -> [[Old, New] ~ tables]
855 => sql_query [] ([Old = fs, New = fs] ++ tables) [] 859 => sql_query [] [] ([Old = fs, New = fs] ++ tables) []
856 -> sql_policy 860 -> sql_policy
857 861
858 val also : sql_policy -> sql_policy -> sql_policy 862 val also : sql_policy -> sql_policy -> sql_policy
859 863
860 val debug : string -> transaction unit 864 val debug : string -> transaction unit