Mercurial > urweb

comparison lib/ur/basis.urs @ 1191:61c3139eab12

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Subquery expressions
author Adam Chlipala <adamc@hcoop.net>
date Thu, 25 Mar 2010 15:44:24 -0400
parents ad9829c3c12c
children 9c82548c97e9
comparison
equal deleted inserted replaced
1190:899875315bde 1191:61c3139eab12
272 -> sql_constraint fs [] 272 -> sql_constraint fs []
273 273
274 274
275 (*** Queries *) 275 (*** Queries *)
276 276
277 con sql_query :: {{Type}} -> {Type} -> Type 277 con sql_query :: {{Type}} -> {{Type}} -> {Type} -> Type
278 con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type 278 con sql_query1 :: {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
279 279
280 con sql_subset :: {{Type}} -> {{Type}} -> Type 280 con sql_subset :: {{Type}} -> {{Type}} -> Type
281 val sql_subset : keep_drop :: {({Type} * {Type})} 281 val sql_subset : keep_drop :: {({Type} * {Type})}
282 -> sql_subset 282 -> sql_subset
283 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop) 283 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop)
288 -> [big1 ~ big2] => [little1 ~ little2] => 288 -> [big1 ~ big2] => [little1 ~ little2] =>
289 sql_subset big1 little1 289 sql_subset big1 little1
290 -> sql_subset big2 little2 290 -> sql_subset big2 little2
291 -> sql_subset (big1 ++ big2) (little1 ++ little2) 291 -> sql_subset (big1 ++ big2) (little1 ++ little2)
292 292
293 con sql_from_items :: {{Type}} -> Type 293 con sql_from_items :: {{Type}} -> {{Type}} -> Type
294 294
295 val sql_from_table : t ::: Type -> fs ::: {Type} 295 val sql_from_table : free ::: {{Type}} -> t ::: Type -> fs ::: {Type}
296 -> fieldsOf t fs -> name :: Name 296 -> fieldsOf t fs -> name :: Name
297 -> t -> sql_from_items [name = fs] 297 -> t -> sql_from_items free [name = fs]
298 val sql_from_comma : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}} 298 val sql_from_comma : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
299 -> [tabs1 ~ tabs2] 299 -> [tabs1 ~ tabs2]
300 => sql_from_items tabs1 -> sql_from_items tabs2 300 => sql_from_items free tabs1 -> sql_from_items free tabs2
301 -> sql_from_items (tabs1 ++ tabs2) 301 -> sql_from_items free (tabs1 ++ tabs2)
302 val sql_inner_join : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}} 302 val sql_inner_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
303 -> [tabs1 ~ tabs2] 303 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
304 => sql_from_items tabs1 -> sql_from_items tabs2 304 => sql_from_items free tabs1 -> sql_from_items free tabs2
305 -> sql_exp (tabs1 ++ tabs2) [] [] bool 305 -> sql_exp (free ++ tabs1 ++ tabs2) [] [] bool
306 -> sql_from_items (tabs1 ++ tabs2) 306 -> sql_from_items free (tabs1 ++ tabs2)
307 307
308 class nullify :: Type -> Type -> Type 308 class nullify :: Type -> Type -> Type
309 val nullify_option : t ::: Type -> nullify (option t) (option t) 309 val nullify_option : t ::: Type -> nullify (option t) (option t)
310 val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t) 310 val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t)
311 311
312 val sql_left_join : tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}} 312 val sql_left_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}}
313 -> [tabs1 ~ tabs2] 313 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
314 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2) 314 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2)
315 -> sql_from_items tabs1 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs2) 315 -> sql_from_items free tabs1 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
316 -> sql_exp (tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool 316 -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool
317 -> sql_from_items (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2) 317 -> sql_from_items free (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
318 318
319 val sql_right_join : tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}} 319 val sql_right_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}}
320 -> [tabs1 ~ tabs2] 320 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
321 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1) 321 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1)
322 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items tabs2 322 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items free tabs2
323 -> sql_exp (map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool 323 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool
324 -> sql_from_items (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2) 324 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
325 325
326 val sql_full_join : tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}} 326 val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
327 -> [tabs1 ~ tabs2] 327 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
328 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2)) 328 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2))
329 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs1) 329 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1)
330 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs2) 330 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
331 -> sql_exp (map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool 331 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool
332 -> sql_from_items (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2)) 332 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
333 333
334 val sql_query1 : tables ::: {{Type}} 334 val sql_query1 : free ::: {{Type}}
335 -> tables ::: {{Type}}
335 -> grouped ::: {{Type}} 336 -> grouped ::: {{Type}}
336 -> selectedFields ::: {{Type}} 337 -> selectedFields ::: {{Type}}
337 -> selectedExps ::: {Type} 338 -> selectedExps ::: {Type}
338 -> empties :: {Unit} 339 -> empties :: {Unit}
339 -> [empties ~ selectedFields] 340 -> [free ~ tables]
341 => [free ~ grouped]
342 => [empties ~ selectedFields]
340 => {Distinct : bool, 343 => {Distinct : bool,
341 From : sql_from_items tables, 344 From : sql_from_items free tables,
342 Where : sql_exp tables [] [] bool, 345 Where : sql_exp (free ++ tables) [] [] bool,
343 GroupBy : sql_subset tables grouped, 346 GroupBy : sql_subset tables grouped,
344 Having : sql_exp grouped tables [] bool, 347 Having : sql_exp (free ++ grouped) tables [] bool,
345 SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields), 348 SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields),
346 SelectExps : $(map (sql_exp grouped tables []) 349 SelectExps : $(map (sql_exp (free ++ grouped) tables [])
347 selectedExps) } 350 selectedExps) }
348 -> sql_query1 tables selectedFields selectedExps 351 -> sql_query1 free tables selectedFields selectedExps
349 352
350 type sql_relop 353 type sql_relop
351 val sql_union : sql_relop 354 val sql_union : sql_relop
352 val sql_intersect : sql_relop 355 val sql_intersect : sql_relop
353 val sql_except : sql_relop 356 val sql_except : sql_relop
354 val sql_relop : tables1 ::: {{Type}} 357 val sql_relop : free ::: {{Type}}
358 -> tables1 ::: {{Type}}
355 -> tables2 ::: {{Type}} 359 -> tables2 ::: {{Type}}
356 -> selectedFields ::: {{Type}} 360 -> selectedFields ::: {{Type}}
357 -> selectedExps ::: {Type} 361 -> selectedExps ::: {Type}
358 -> sql_relop 362 -> sql_relop
359 -> sql_query1 tables1 selectedFields selectedExps 363 -> sql_query1 free tables1 selectedFields selectedExps
360 -> sql_query1 tables2 selectedFields selectedExps 364 -> sql_query1 free tables2 selectedFields selectedExps
361 -> sql_query1 [] selectedFields selectedExps 365 -> sql_query1 free [] selectedFields selectedExps
362 val sql_forget_tables : tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type} 366 val sql_forget_tables : free ::: {{Type}} -> tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type}
363 -> sql_query1 tables selectedFields selectedExps 367 -> sql_query1 free tables selectedFields selectedExps
364 -> sql_query1 [] selectedFields selectedExps 368 -> sql_query1 free [] selectedFields selectedExps
365 369
366 type sql_direction 370 type sql_direction
367 val sql_asc : sql_direction 371 val sql_asc : sql_direction
368 val sql_desc : sql_direction 372 val sql_desc : sql_direction
369 373
380 384
381 type sql_offset 385 type sql_offset
382 val sql_no_offset : sql_offset 386 val sql_no_offset : sql_offset
383 val sql_offset : int -> sql_offset 387 val sql_offset : int -> sql_offset
384 388
385 val sql_query : tables ::: {{Type}} 389 val sql_query : free ::: {{Type}}
390 -> tables ::: {{Type}}
386 -> selectedFields ::: {{Type}} 391 -> selectedFields ::: {{Type}}
387 -> selectedExps ::: {Type} 392 -> selectedExps ::: {Type}
388 -> {Rows : sql_query1 tables selectedFields selectedExps, 393 -> [free ~ tables]
389 OrderBy : sql_order_by tables selectedExps, 394 => {Rows : sql_query1 free tables selectedFields selectedExps,
395 OrderBy : sql_order_by (free ++ tables) selectedExps,
390 Limit : sql_limit, 396 Limit : sql_limit,
391 Offset : sql_offset} 397 Offset : sql_offset}
392 -> sql_query selectedFields selectedExps 398 -> sql_query free selectedFields selectedExps
393 399
394 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} 400 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
395 -> fieldType ::: Type -> agg ::: {{Type}} 401 -> fieldType ::: Type -> agg ::: {{Type}}
396 -> exps ::: {Type} 402 -> exps ::: {Type}
397 -> tab :: Name -> field :: Name 403 -> tab :: Name -> field :: Name
493 val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type 499 val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
494 -> sql_injectable_prim t 500 -> sql_injectable_prim t
495 -> sql_exp tables agg exps t 501 -> sql_exp tables agg exps t
496 -> sql_exp tables agg exps (option t) 502 -> sql_exp tables agg exps (option t)
497 503
504 val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type
505 -> sql_query tables [] [nm = t]
506 -> sql_exp tables agg exps t
507
498 (*** Executing queries *) 508 (*** Executing queries *)
499 509
500 val query : tables ::: {{Type}} -> exps ::: {Type} 510 val query : tables ::: {{Type}} -> exps ::: {Type}
501 -> [tables ~ exps] => 511 -> [tables ~ exps] =>
502 state ::: Type 512 state ::: Type
503 -> sql_query tables exps 513 -> sql_query [] tables exps
504 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) 514 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
505 -> state 515 -> state
506 -> transaction state) 516 -> transaction state)
507 -> state 517 -> state
508 -> transaction state 518 -> transaction state