Mercurial > meta
changeset 13:d05943db55e8
Sql.joiner
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Mon, 21 Mar 2011 10:16:12 -0400 |
parents | a6730c3cfea7 |
children | 744bf911dcc6 |
files | sql.ur sql.urs |
diffstat | 2 files changed, 18 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- 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 [_] [_] ! !
--- 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. *)