|
adam@6
|
1 fun sqexps [env] [fields] (fl : folder fields) (inj : $(map sql_injectable fields)) (r : $fields) =
|
|
adam@18
|
2 @map2 [sql_injectable] [ident] [sql_exp env [] []]
|
|
adam@6
|
3 (fn [t] => @sql_inject)
|
|
adam@6
|
4 fl inj r
|
|
adam@6
|
5
|
|
adam@15
|
6 fun selector [tn :: Name] [fs] [ofs] [fs ~ ofs] (fl : folder fs) (m : $(map sql_injectable fs)) (r : $fs)
|
|
adam@15
|
7 : sql_exp [tn = ofs ++ fs] [] [] bool =
|
|
adam@18
|
8 @foldR2 [sql_injectable] [ident]
|
|
adam@6
|
9 [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool]
|
|
adam@6
|
10 (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
|
|
adam@6
|
11 (inj : sql_injectable t) (v : t)
|
|
adam@6
|
12 (exp : rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool)
|
|
adam@6
|
13 [rest :: {Type}] [rest ~ [nm = t] ++ key] =>
|
|
adam@14
|
14 (WHERE {{tn}}.{nm} = {@sql_inject inj v} AND {exp [[nm = t] ++ rest]}))
|
|
adam@6
|
15 (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE))
|
|
adam@6
|
16 fl m r [_] !
|
|
adam@13
|
17
|
|
adam@13
|
18 fun joiner [tn1 :: Name] [tn2 :: Name] [fs] [ofs1] [ofs2] [[tn1] ~ [tn2]] [fs ~ ofs1] [fs ~ ofs2]
|
|
adam@15
|
19 (fl : folder fs) : sql_exp [tn1 = ofs1 ++ fs, tn2 = ofs2 ++ fs] [] [] bool =
|
|
adam@13
|
20 @fold
|
|
adam@13
|
21 [fn key => rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key] => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool]
|
|
adam@13
|
22 (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
|
|
adam@13
|
23 (exp : rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key]
|
|
adam@13
|
24 => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool)
|
|
adam@13
|
25 [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ [nm = t] ++ key] [rest2 ~ [nm = t] ++ key] =>
|
|
adam@14
|
26 (WHERE {{tn1}}.{nm} = {{tn2}}.{nm} AND {exp [[nm = t] ++ rest1] [[nm = t] ++ rest2]}))
|
|
adam@13
|
27 (fn [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ []] [rest2 ~ []] => (WHERE TRUE))
|
|
adam@13
|
28 fl [_] [_] ! !
|
|
adam@15
|
29
|
|
adam@15
|
30 fun insertIfMissing [keyCols ::: {Type}] [otherCols ::: {Type}] [otherKeys ::: {{Unit}}]
|
|
adam@15
|
31 [keyCols ~ otherCols] [[Pkey] ~ otherKeys]
|
|
adam@16
|
32 (kfl : folder keyCols) (kinj : $(map sql_injectable keyCols))
|
|
adam@16
|
33 (ofl : folder otherCols) (oinj : $(map sql_injectable otherCols))
|
|
adam@15
|
34 (t : sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys))
|
|
adam@15
|
35 (vs : $(keyCols ++ otherCols))
|
|
adam@15
|
36 : transaction bool =
|
|
adam@15
|
37 alreadyThere <- oneRowE1 (SELECT COUNT( * ) > 0
|
|
adam@15
|
38 FROM t
|
|
adam@15
|
39 WHERE {@selector [#T] ! kfl kinj (vs --- _)});
|
|
adam@15
|
40 if alreadyThere then
|
|
adam@15
|
41 return False
|
|
adam@15
|
42 else
|
|
adam@15
|
43 dml (insert t (@sqexps kfl kinj (vs --- _)
|
|
adam@15
|
44 ++ @sqexps ofl oinj (vs --- _)));
|
|
adam@15
|
45 return True
|
|
adam@15
|
46
|
|
adam@15
|
47 fun deleteByKey [keyCols ::: {Type}] [otherCols ::: {Type}] [otherKeys ::: {{Unit}}]
|
|
adam@15
|
48 [keyCols ~ otherCols] [[Pkey] ~ otherKeys]
|
|
adam@16
|
49 (kfl : folder keyCols) (kinj : $(map sql_injectable keyCols))
|
|
adam@15
|
50 (t : sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys))
|
|
adam@16
|
51 (vs : $keyCols) =
|
|
adam@15
|
52 dml (delete t (@selector [#T] ! kfl kinj vs))
|
|
adam@19
|
53
|
|
adam@19
|
54 fun lookup [keyCols ::: {Type}] [otherCols ::: {Type}] [otherKeys ::: {{Unit}}]
|
|
adam@19
|
55 [keyCols ~ otherCols] [[Pkey] ~ otherKeys]
|
|
adam@19
|
56 (kfl : folder keyCols) (kinj : $(map sql_injectable keyCols))
|
|
adam@19
|
57 (t : sql_table (keyCols ++ otherCols) ([Pkey = map (fn _ => ()) keyCols] ++ otherKeys))
|
|
adam@19
|
58 (vs : $keyCols)
|
|
adam@19
|
59 : transaction (option $otherCols) =
|
|
adam@19
|
60 oneOrNoRows1 (SELECT t.{{otherCols}}
|
|
adam@19
|
61 FROM t
|
|
adam@19
|
62 WHERE {@selector [#T] ! kfl kinj (vs --- _)})
|
|
adam@26
|
63
|
|
adam@26
|
64 fun listify [lead :: Name] [cols ::: {Type}] [rest ::: {{Type}}] [[lead] ~ rest]
|
|
adam@26
|
65 (fl : folder cols) (eqs : $(map eq cols)) (q : sql_query [] [] ([lead = cols] ++ rest) []) =
|
|
adam@26
|
66 query q
|
|
adam@26
|
67 (fn r acc =>
|
|
adam@26
|
68 return (case acc of
|
|
adam@26
|
69 [] => (r.lead, (r -- lead) :: []) :: []
|
|
adam@26
|
70 | (key, ls) :: acc' =>
|
|
adam@26
|
71 if @Record.equal eqs fl r.lead key then
|
|
adam@26
|
72 (key, (r -- lead) :: ls) :: acc'
|
|
adam@26
|
73 else
|
|
adam@26
|
74 (r.lead, (r -- lead) :: []) :: acc))
|
|
adam@26
|
75 []
|
