diff sql.urs @ 13:d05943db55e8

Sql.joiner
author Adam Chlipala <adam@chlipala.net>
date Mon, 21 Mar 2011 10:16:12 -0400
parents 799f43bce62b
children 6ebc2ca594b7
line wrap: on
line diff
--- 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. *)