diff lib/ur/basis.urs @ 751:f95d652086cd

RIGHT and FULL JOIN
author Adam Chlipala <adamc@hcoop.net>
date Tue, 28 Apr 2009 11:14:24 -0400
parents 059074c8d2fc
children d484df4e841a
line wrap: on
line diff
--- a/lib/ur/basis.urs	Tue Apr 28 11:05:28 2009 -0400
+++ b/lib/ur/basis.urs	Tue Apr 28 11:14:24 2009 -0400
@@ -246,6 +246,21 @@
        -> sql_exp (tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool
        -> sql_from_items (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
 
+val sql_right_join : tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}}
+                     -> [tabs1 ~ tabs2]
+    => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1)
+       -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items tabs2
+       -> sql_exp (map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool
+       -> sql_from_items (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
+
+val sql_full_join : tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
+                     -> [tabs1 ~ tabs2]
+    => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2))
+       -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs1)
+       -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs2)
+       -> sql_exp (map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool
+       -> sql_from_items (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
+
 val sql_query1 : tables ::: {{Type}}
                  -> grouped ::: {{Type}}
                  -> selectedFields ::: {{Type}}