annotate sql.ur @ 6:799f43bce62b
Import some code from iwl
| author |
Adam Chlipala <adam@chlipala.net> |
| date |
Tue, 14 Dec 2010 10:33:24 -0500 |
| parents |
|
| children |
d05943db55e8 |
| rev |
line source |
|
adam@6
|
1 fun sqexps [env] [fields] (fl : folder fields) (inj : $(map sql_injectable fields)) (r : $fields) =
|
|
adam@6
|
2 @map2 [sql_injectable] [id] [sql_exp env [] []]
|
|
adam@6
|
3 (fn [t] => @sql_inject)
|
|
adam@6
|
4 fl inj r
|
|
adam@6
|
5
|
|
adam@6
|
6 fun selector [tn :: Name] [fs] [ofs] [fs ~ ofs] (fl : folder fs) (m : $(map sql_injectable fs)) (r : $fs) =
|
|
adam@6
|
7 @foldR2 [sql_injectable] [id]
|
|
adam@6
|
8 [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool]
|
|
adam@6
|
9 (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
|
|
adam@6
|
10 (inj : sql_injectable t) (v : t)
|
|
adam@6
|
11 (exp : rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool)
|
|
adam@6
|
12 [rest :: {Type}] [rest ~ [nm = t] ++ key] =>
|
|
adam@6
|
13 (WHERE {{tn}}.{nm} = {@sql_inject inj v} AND {exp [[nm = t] ++ rest] !}))
|
|
adam@6
|
14 (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE))
|
|
adam@6
|
15 fl m r [_] !
|
