# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1300716972 14400
# Node ID d05943db55e89588d32561db89268ce717b03664
# Parent  a6730c3cfea7f66ea870f58f8bc3fda4ca056041
Sql.joiner

diff -r a6730c3cfea7 -r d05943db55e8 sql.ur
--- a/sql.ur	Tue Feb 08 16:52:41 2011 -0500
+++ b/sql.ur	Mon Mar 21 10:16:12 2011 -0400
@@ -13,3 +13,15 @@
          (WHERE {{tn}}.{nm} = {@sql_inject inj v} AND {exp [[nm = t] ++ rest] !}))
      (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE))
      fl m r [_] !
+
+fun joiner [tn1 :: Name] [tn2 :: Name] [fs] [ofs1] [ofs2] [[tn1] ~ [tn2]] [fs ~ ofs1] [fs ~ ofs2]
+           (fl : folder fs) =
+    @fold
+     [fn key => rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key] => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool]
+     (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
+                      (exp : rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key]
+                       => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool)
+                      [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ [nm = t] ++ key] [rest2 ~ [nm = t] ++ key] =>
+         (WHERE {{tn1}}.{nm} = {{tn2}}.{nm} AND {exp [[nm = t] ++ rest1] [[nm = t] ++ rest2] ! !}))
+     (fn [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ []] [rest2 ~ []] => (WHERE TRUE))
+     fl [_] [_] ! !
diff -r a6730c3cfea7 -r d05943db55e8 sql.urs
--- a/sql.urs	Tue Feb 08 16:52:41 2011 -0500
+++ b/sql.urs	Mon Mar 21 10:16:12 2011 -0400
@@ -9,3 +9,9 @@
                -> sql_exp [tn = ofs ++ fs] [] [] bool
 (* Build a boolean SQL expression expressing equality of some fields of a table
  * row with a record of Ur values *)
+
+val joiner : tn1 :: Name -> tn2 :: Name -> fs ::: {Type} -> ofs1 ::: {Type} -> ofs2 ::: {Type}
+             -> [[tn1] ~ [tn2]] => [fs ~ ofs1] => [fs ~ ofs2]
+               => folder fs
+               -> sql_exp [tn1 = ofs1 ++ fs, tn2 = ofs2 ++ fs] [] [] bool
+(* Declare equality of same-named columns from two tables. *)