comparison sql.ur @ 15:6ebc2ca594b7

Sql.insertIfMissing and deleteByKey (partly from Ron de Bruijn)
author Adam Chlipala <adam@chlipala.net>
date Sun, 11 Dec 2011 14:04:34 -0500
parents 744bf911dcc6
children 959583692166
comparison
equal deleted inserted replaced
14:744bf911dcc6 15:6ebc2ca594b7
1 fun sqexps [env] [fields] (fl : folder fields) (inj : $(map sql_injectable fields)) (r : $fields) = 1 fun sqexps [env] [fields] (fl : folder fields) (inj : $(map sql_injectable fields)) (r : $fields) =
2 @map2 [sql_injectable] [id] [sql_exp env [] []] 2 @map2 [sql_injectable] [id] [sql_exp env [] []]
3 (fn [t] => @sql_inject) 3 (fn [t] => @sql_inject)
4 fl inj r 4 fl inj r
5 5
6 fun selector [tn :: Name] [fs] [ofs] [fs ~ ofs] (fl : folder fs) (m : $(map sql_injectable fs)) (r : $fs) = 6 fun selector [tn :: Name] [fs] [ofs] [fs ~ ofs] (fl : folder fs) (m : $(map sql_injectable fs)) (r : $fs)
7 : sql_exp [tn = ofs ++ fs] [] [] bool =
7 @foldR2 [sql_injectable] [id] 8 @foldR2 [sql_injectable] [id]
8 [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool] 9 [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool]
9 (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key] 10 (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
10 (inj : sql_injectable t) (v : t) 11 (inj : sql_injectable t) (v : t)
11 (exp : rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool) 12 (exp : rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool)
13 (WHERE {{tn}}.{nm} = {@sql_inject inj v} AND {exp [[nm = t] ++ rest]})) 14 (WHERE {{tn}}.{nm} = {@sql_inject inj v} AND {exp [[nm = t] ++ rest]}))
14 (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE)) 15 (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE))
15 fl m r [_] ! 16 fl m r [_] !
16 17
17 fun joiner [tn1 :: Name] [tn2 :: Name] [fs] [ofs1] [ofs2] [[tn1] ~ [tn2]] [fs ~ ofs1] [fs ~ ofs2] 18 fun joiner [tn1 :: Name] [tn2 :: Name] [fs] [ofs1] [ofs2] [[tn1] ~ [tn2]] [fs ~ ofs1] [fs ~ ofs2]
18 (fl : folder fs) = 19 (fl : folder fs) : sql_exp [tn1 = ofs1 ++ fs, tn2 = ofs2 ++ fs] [] [] bool =
19 @fold 20 @fold
20 [fn key => rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key] => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool] 21 [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 (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
22 (exp : rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key] 23 (exp : rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key]
23 => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool) 24 => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool)
24 [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ [nm = t] ++ key] [rest2 ~ [nm = t] ++ key] => 25 [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 (WHERE {{tn1}}.{nm} = {{tn2}}.{nm} AND {exp [[nm = t] ++ rest1] [[nm = t] ++ rest2]}))
26 (fn [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ []] [rest2 ~ []] => (WHERE TRUE)) 27 (fn [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ []] [rest2 ~ []] => (WHERE TRUE))
27 fl [_] [_] ! ! 28 fl [_] [_] ! !
29
30 fun insertIfMissing [keyCols ::: {Type}] [otherCols ::: {Type}] [otherKeys ::: {{Unit}}]
31 [keyCols ~ otherCols] [[Pkey] ~ otherKeys]
32 (t : sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys))
33 (vs : $(keyCols ++ otherCols))
34 (kfl : folder keyCols) (kinj : $(map sql_injectable keyCols))
35 (ofl : folder otherCols) (oinj : $(map sql_injectable otherCols))
36 : transaction bool =
37 alreadyThere <- oneRowE1 (SELECT COUNT( * ) > 0
38 FROM t
39 WHERE {@selector [#T] ! kfl kinj (vs --- _)});
40 if alreadyThere then
41 return False
42 else
43 dml (insert t (@sqexps kfl kinj (vs --- _)
44 ++ @sqexps ofl oinj (vs --- _)));
45 return True
46
47 fun deleteByKey [keyCols ::: {Type}] [otherCols ::: {Type}] [otherKeys ::: {{Unit}}]
48 [keyCols ~ otherCols] [[Pkey] ~ otherKeys]
49 (t : sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys))
50 (vs : $keyCols) (kfl : folder keyCols) (kinj : $(map sql_injectable keyCols)) =
51 dml (delete t (@selector [#T] ! kfl kinj vs))