Mercurial > meta
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)) |