Mercurial > meta
comparison sql.ur @ 13:d05943db55e8
Sql.joiner
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Mon, 21 Mar 2011 10:16:12 -0400 |
parents | 799f43bce62b |
children | 744bf911dcc6 |
comparison
equal
deleted
inserted
replaced
12:a6730c3cfea7 | 13:d05943db55e8 |
---|---|
11 (exp : rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool) | 11 (exp : rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool) |
12 [rest :: {Type}] [rest ~ [nm = t] ++ key] => | 12 [rest :: {Type}] [rest ~ [nm = t] ++ key] => |
13 (WHERE {{tn}}.{nm} = {@sql_inject inj v} AND {exp [[nm = t] ++ rest] !})) | 13 (WHERE {{tn}}.{nm} = {@sql_inject inj v} AND {exp [[nm = t] ++ rest] !})) |
14 (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE)) | 14 (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE)) |
15 fl m r [_] ! | 15 fl m r [_] ! |
16 | |
17 fun joiner [tn1 :: Name] [tn2 :: Name] [fs] [ofs1] [ofs2] [[tn1] ~ [tn2]] [fs ~ ofs1] [fs ~ ofs2] | |
18 (fl : folder fs) = | |
19 @fold | |
20 [fn key => rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key] => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool] | |
21 (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key] | |
22 (exp : rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key] | |
23 => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool) | |
24 [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ [nm = t] ++ key] [rest2 ~ [nm = t] ++ key] => | |
25 (WHERE {{tn1}}.{nm} = {{tn2}}.{nm} AND {exp [[nm = t] ++ rest1] [[nm = t] ++ rest2] ! !})) | |
26 (fn [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ []] [rest2 ~ []] => (WHERE TRUE)) | |
27 fl [_] [_] ! ! |