adamc@623
|
1 (** Row folding *)
|
adamc@623
|
2
|
adamc@623
|
3 con folder = K ==> fn r :: {K} =>
|
adamc@623
|
4 tf :: ({K} -> Type)
|
adamc@653
|
5 -> (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
|
adamc@653
|
6 tf r -> tf ([nm = v] ++ r))
|
adamc@623
|
7 -> tf [] -> tf r
|
adamc@623
|
8
|
adamc@822
|
9 fun fold [K] [tf :: {K} -> Type]
|
adamc@653
|
10 (f : (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
|
adamc@653
|
11 tf r -> tf ([nm = v] ++ r)))
|
adamc@1093
|
12 (i : tf []) [r ::: {K}] (fl : folder r) = fl [tf] f i
|
adamc@653
|
13
|
adamc@627
|
14 structure Folder = struct
|
adamc@822
|
15 fun nil [K] [tf :: {K} -> Type]
|
adamc@653
|
16 (f : nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
|
adamc@653
|
17 tf r -> tf ([nm = v] ++ r))
|
adamc@627
|
18 (i : tf []) = i
|
adamc@627
|
19
|
adamc@822
|
20 fun cons [K] [r ::: {K}] [nm :: Name] [v :: K] [[nm] ~ r] (fold : folder r)
|
adamc@822
|
21 [tf :: {K} -> Type]
|
adamc@653
|
22 (f : nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
|
adamc@653
|
23 tf r -> tf ([nm = v] ++ r))
|
adamc@653
|
24 (i : tf []) = f [nm] [v] [r] ! (fold [tf] f i)
|
adamc@628
|
25
|
adamc@822
|
26 fun concat [K] [r1 ::: {K}] [r2 ::: {K}] [r1 ~ r2]
|
adamc@628
|
27 (f1 : folder r1) (f2 : folder r2)
|
adamc@822
|
28 [tf :: {K} -> Type]
|
adamc@653
|
29 (f : nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
|
adamc@653
|
30 tf r -> tf ([nm = v] ++ r))
|
adamc@628
|
31 (i : tf []) =
|
adamc@629
|
32 f1 [fn r1' => [r1' ~ r2] => tf (r1' ++ r2)]
|
adamc@822
|
33 (fn [nm :: Name] [v :: K] [r1' :: {K}] [[nm] ~ r1']
|
adamc@653
|
34 (acc : [r1' ~ r2] => tf (r1' ++ r2))
|
adamc@653
|
35 [[nm = v] ++ r1' ~ r2] =>
|
adamc@653
|
36 f [nm] [v] [r1' ++ r2] ! acc)
|
adamc@629
|
37 (fn [[] ~ r2] => f2 [tf] f i) !
|
adamc@630
|
38
|
adamc@822
|
39 fun mp [K1] [K2] [f ::: K1 -> K2] [r ::: {K1}]
|
adamc@630
|
40 (fold : folder r)
|
adamc@822
|
41 [tf :: {K2} -> Type]
|
adamc@653
|
42 (f : nm :: Name -> v :: K2 -> r :: {K2} -> [[nm] ~ r] =>
|
adamc@653
|
43 tf r -> tf ([nm = v] ++ r))
|
adamc@630
|
44 (i : tf []) =
|
adamc@630
|
45 fold [fn r => tf (map f r)]
|
adamc@822
|
46 (fn [nm :: Name] [v :: K1] [rest :: {K1}] [[nm] ~ rest] (acc : tf (map f rest)) =>
|
adamc@653
|
47 f [nm] [f v] [map f rest] ! acc)
|
adamc@630
|
48 i
|
adamc@627
|
49 end
|
adamc@627
|
50
|
adamc@623
|
51
|
adamc@422
|
52 fun not b = if b then False else True
|
adamc@422
|
53
|
adamc@898
|
54 con id = K ==> fn t :: K => t
|
adamc@356
|
55 con record (t :: {Type}) = $t
|
adamc@637
|
56 con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1
|
adamc@637
|
57 con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2
|
adamc@637
|
58 con fst3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.1
|
adamc@637
|
59 con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2
|
adamc@637
|
60 con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3
|
adamc@329
|
61
|
adamc@643
|
62 con mapU = K ==> fn f :: K => map (fn _ :: Unit => f)
|
adamc@445
|
63
|
adamc@339
|
64 con ex = fn tf :: (Type -> Type) =>
|
adamc@356
|
65 res ::: Type -> (choice :: Type -> tf choice -> res) -> res
|
adamc@339
|
66
|
adamc@822
|
67 fun ex [tf :: (Type -> Type)] [choice :: Type] (body : tf choice) : ex tf =
|
adamc@822
|
68 fn [res] (f : choice :: Type -> tf choice -> res) =>
|
adamc@356
|
69 f [choice] body
|
adamc@339
|
70
|
adamc@822
|
71 fun compose [t1 ::: Type] [t2 ::: Type] [t3 ::: Type]
|
adamc@356
|
72 (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x)
|
adamc@325
|
73
|
adamc@822
|
74 fun show_option [t ::: Type] (_ : show t) =
|
adamc@777
|
75 mkShow (fn opt : option t =>
|
adamc@777
|
76 case opt of
|
adamc@777
|
77 None => ""
|
adamc@777
|
78 | Some x => show x)
|
adamc@777
|
79
|
adamc@822
|
80 fun read_option [t ::: Type] (_ : read t) =
|
adamc@777
|
81 mkRead (fn s =>
|
adamc@777
|
82 case s of
|
adamc@777
|
83 "" => None
|
adamc@777
|
84 | _ => Some (readError s : t))
|
adamc@777
|
85 (fn s =>
|
adamc@777
|
86 case s of
|
adamc@777
|
87 "" => Some None
|
adamc@777
|
88 | _ => case read s of
|
adamc@777
|
89 None => None
|
adamc@777
|
90 | v => Some v)
|
adamc@777
|
91
|
adam@1360
|
92 fun txt [t] [ctx ::: {Unit}] [use ::: {Type}] (_ : show t) (v : t) : xml ctx use [] =
|
adamc@564
|
93 cdata (show v)
|
adamc@328
|
94
|
adamc@1093
|
95 fun map0 [K] [tf :: K -> Type] (f : t :: K -> tf t) [r ::: {K}] (fl : folder r) =
|
adamc@993
|
96 fl [fn r :: {K} => $(map tf r)]
|
adamc@993
|
97 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc =>
|
adamc@993
|
98 acc ++ {nm = f [t]})
|
adamc@993
|
99 {}
|
adamc@993
|
100
|
adamc@1093
|
101 fun mp [K] [tf1 :: K -> Type] [tf2 :: K -> Type] (f : t ::: K -> tf1 t -> tf2 t) [r ::: {K}] (fl : folder r) =
|
adamc@898
|
102 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r)]
|
adamc@898
|
103 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r =>
|
adamc@898
|
104 acc (r -- nm) ++ {nm = f r.nm})
|
adamc@898
|
105 (fn _ => {})
|
adamc@898
|
106
|
adamc@905
|
107 fun map2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type]
|
adamc@1093
|
108 (f : t ::: K -> tf1 t -> tf2 t -> tf3 t) [r ::: {K}] (fl : folder r) =
|
adamc@905
|
109 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r)]
|
adamc@905
|
110 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 =>
|
adamc@905
|
111 acc (r1 -- nm) (r2 -- nm) ++ {nm = f r1.nm r2.nm})
|
adamc@905
|
112 (fn _ _ => {})
|
adamc@898
|
113
|
adamc@937
|
114 fun map3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tf :: K -> Type]
|
adamc@1093
|
115 (f : t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) [r ::: {K}] (fl : folder r) =
|
adamc@937
|
116 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)]
|
adamc@937
|
117 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 r3 =>
|
adamc@937
|
118 acc (r1 -- nm) (r2 -- nm) (r3 -- nm) ++ {nm = f r1.nm r2.nm r3.nm})
|
adamc@937
|
119 (fn _ _ _ => {})
|
adamc@937
|
120
|
adamc@822
|
121 fun foldUR [tf :: Type] [tr :: {Unit} -> Type]
|
adamc@411
|
122 (f : nm :: Name -> rest :: {Unit}
|
adamc@629
|
123 -> [[nm] ~ rest] =>
|
adamc@411
|
124 tf -> tr rest -> tr ([nm] ++ rest))
|
adamc@1093
|
125 (i : tr []) [r ::: {Unit}] (fl : folder r) =
|
adamc@653
|
126 fl [fn r :: {Unit} => $(mapU tf r) -> tr r]
|
adamc@822
|
127 (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r =>
|
adamc@653
|
128 f [nm] [rest] ! r.nm (acc (r -- nm)))
|
adamc@653
|
129 (fn _ => i)
|
adamc@411
|
130
|
adamc@822
|
131 fun foldUR2 [tf1 :: Type] [tf2 :: Type] [tr :: {Unit} -> Type]
|
adamc@418
|
132 (f : nm :: Name -> rest :: {Unit}
|
adamc@629
|
133 -> [[nm] ~ rest] =>
|
adamc@418
|
134 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
|
adamc@1093
|
135 (i : tr []) [r ::: {Unit}] (fl : folder r) =
|
adamc@653
|
136 fl [fn r :: {Unit} => $(mapU tf1 r) -> $(mapU tf2 r) -> tr r]
|
adamc@822
|
137 (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r1 r2 =>
|
adamc@653
|
138 f [nm] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
|
adamc@653
|
139 (fn _ _ => i)
|
adamc@418
|
140
|
adamc@822
|
141 fun foldR [K] [tf :: K -> Type] [tr :: {K} -> Type]
|
adamc@623
|
142 (f : nm :: Name -> t :: K -> rest :: {K}
|
adamc@629
|
143 -> [[nm] ~ rest] =>
|
adamc@356
|
144 tf t -> tr rest -> tr ([nm = t] ++ rest))
|
adamc@1093
|
145 (i : tr []) [r ::: {K}] (fl : folder r) =
|
adamc@653
|
146 fl [fn r :: {K} => $(map tf r) -> tr r]
|
adamc@822
|
147 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> tr rest) r =>
|
adamc@653
|
148 f [nm] [t] [rest] ! r.nm (acc (r -- nm)))
|
adamc@653
|
149 (fn _ => i)
|
adamc@336
|
150
|
adamc@822
|
151 fun foldR2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type]
|
adamc@623
|
152 (f : nm :: Name -> t :: K -> rest :: {K}
|
adamc@629
|
153 -> [[nm] ~ rest] =>
|
adamc@367
|
154 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
|
adamc@1093
|
155 (i : tr []) [r ::: {K}] (fl : folder r) =
|
adamc@653
|
156 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r]
|
adamc@822
|
157 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
|
adamc@653
|
158 (acc : _ -> _ -> tr rest) r1 r2 =>
|
adamc@653
|
159 f [nm] [t] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
|
adamc@653
|
160 (fn _ _ => i)
|
adamc@332
|
161
|
adamc@910
|
162 fun foldR3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type]
|
adamc@910
|
163 (f : nm :: Name -> t :: K -> rest :: {K}
|
adamc@910
|
164 -> [[nm] ~ rest] =>
|
adamc@910
|
165 tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
|
adamc@1093
|
166 (i : tr []) [r ::: {K}] (fl : folder r) =
|
adamc@910
|
167 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r]
|
adamc@910
|
168 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
|
adamc@910
|
169 (acc : _ -> _ -> _ -> tr rest) r1 r2 r3 =>
|
adamc@910
|
170 f [nm] [t] [rest] ! r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm)))
|
adamc@910
|
171 (fn _ _ _ => i)
|
adamc@910
|
172
|
adamc@1172
|
173 fun mapUX [tf :: Type] [ctx :: {Unit}]
|
adamc@1172
|
174 (f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf -> xml ctx [] []) =
|
adamc@1172
|
175 @@foldR [fn _ => tf] [fn _ => xml ctx [] []]
|
adamc@1172
|
176 (fn [nm :: Name] [u :: Unit] [rest :: {Unit}] [[nm] ~ rest] r acc =>
|
adamc@1172
|
177 <xml>{f [nm] [rest] ! r}{acc}</xml>)
|
adamc@1172
|
178 <xml/>
|
adamc@1172
|
179
|
adamc@1172
|
180 fun mapX [K] [tf :: K -> Type] [ctx :: {Unit}]
|
adamc@623
|
181 (f : nm :: Name -> t :: K -> rest :: {K}
|
adamc@629
|
182 -> [[nm] ~ rest] =>
|
adamc@720
|
183 tf t -> xml ctx [] []) =
|
adamc@1093
|
184 @@foldR [tf] [fn _ => xml ctx [] []]
|
adamc@1093
|
185 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc =>
|
adamc@1093
|
186 <xml>{f [nm] [t] [rest] ! r}{acc}</xml>)
|
adamc@1093
|
187 <xml/>
|
adamc@336
|
188
|
adamc@1173
|
189 fun mapUX2 [tf1 :: Type] [tf2 :: Type] [ctx :: {Unit}]
|
adamc@1173
|
190 (f : nm :: Name -> rest :: {Unit}
|
adamc@1173
|
191 -> [[nm] ~ rest] =>
|
adamc@1173
|
192 tf1 -> tf2 -> xml ctx [] []) =
|
adamc@1173
|
193 @@foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
|
adamc@1173
|
194 (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] v1 v2 acc =>
|
adamc@1173
|
195 <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>)
|
adamc@1173
|
196 <xml/>
|
adamc@1173
|
197
|
adamc@1172
|
198 fun mapX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}]
|
adamc@623
|
199 (f : nm :: Name -> t :: K -> rest :: {K}
|
adamc@629
|
200 -> [[nm] ~ rest] =>
|
adamc@720
|
201 tf1 t -> tf2 t -> xml ctx [] []) =
|
adamc@1093
|
202 @@foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
|
adamc@1093
|
203 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
|
adamc@1093
|
204 r1 r2 acc =>
|
adamc@1093
|
205 <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>)
|
adamc@1093
|
206 <xml/>
|
adamc@445
|
207
|
adamc@1172
|
208 fun mapX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}]
|
adamc@910
|
209 (f : nm :: Name -> t :: K -> rest :: {K}
|
adamc@910
|
210 -> [[nm] ~ rest] =>
|
adamc@910
|
211 tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) =
|
adamc@1093
|
212 @@foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []]
|
adamc@1093
|
213 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
|
adamc@1093
|
214 r1 r2 r3 acc =>
|
adamc@1093
|
215 <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>)
|
adamc@1093
|
216 <xml/>
|
adamc@910
|
217
|
adam@1394
|
218 fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [] [t = fs] [])
|
adamc@1177
|
219 (f : $fs -> state -> transaction state) (i : state) =
|
adamc@1177
|
220 query q (fn r => f r.t) i
|
adamc@1177
|
221
|
adam@1394
|
222 fun query1' [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [] [t = fs] [])
|
adamc@1177
|
223 (f : $fs -> state -> state) (i : state) =
|
adamc@1177
|
224 query q (fn r s => return (f r.t s)) i
|
adamc@1177
|
225
|
adam@1394
|
226 fun queryL [tables] [exps] [tables ~ exps] (q : sql_query [] [] tables exps) =
|
adamc@1081
|
227 query q
|
adamc@1081
|
228 (fn r ls => return (r :: ls))
|
adamc@1081
|
229 []
|
adamc@1081
|
230
|
adam@1394
|
231 fun queryL1 [t ::: Name] [fs ::: {Type}] (q : sql_query [] [] [t = fs] []) =
|
adam@1321
|
232 query q
|
adam@1321
|
233 (fn r ls => return (r.t :: ls))
|
adam@1321
|
234 []
|
adam@1321
|
235
|
adamc@822
|
236 fun queryI [tables ::: {{Type}}] [exps ::: {Type}]
|
adam@1394
|
237 [tables ~ exps] (q : sql_query [] [] tables exps)
|
adamc@682
|
238 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
|
adamc@682
|
239 -> transaction unit) =
|
adamc@682
|
240 query q
|
adamc@682
|
241 (fn fs _ => f fs)
|
adamc@682
|
242 ()
|
adamc@682
|
243
|
adam@1394
|
244 fun queryI1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] [])
|
adam@1363
|
245 (f : $fs -> transaction unit) =
|
adam@1363
|
246 query q
|
adam@1363
|
247 (fn fs _ => f fs.nm)
|
adam@1363
|
248 ()
|
adam@1363
|
249
|
adamc@1004
|
250 fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
|
adam@1394
|
251 [tables ~ exps] (q : sql_query [] [] tables exps)
|
adamc@621
|
252 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
|
adamc@1004
|
253 -> xml ctx inp []) =
|
adamc@356
|
254 query q
|
adamc@356
|
255 (fn fs acc => return <xml>{acc}{f fs}</xml>)
|
adamc@360
|
256 <xml/>
|
adamc@341
|
257
|
adam@1405
|
258 fun rev [a] (ls : list a) : list a =
|
adam@1405
|
259 let
|
adam@1405
|
260 fun rev' ls acc =
|
adam@1405
|
261 case ls of
|
adam@1405
|
262 [] => acc
|
adam@1405
|
263 | x :: ls => rev' ls (x :: acc)
|
adam@1405
|
264 in
|
adam@1405
|
265 rev' ls []
|
adam@1405
|
266 end
|
adam@1405
|
267
|
adam@1405
|
268 fun queryXI [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
|
adam@1405
|
269 [tables ~ exps] (q : sql_query [] [] tables exps)
|
adam@1405
|
270 (f : int -> $(exps ++ map (fn fields :: {Type} => $fields) tables)
|
adam@1405
|
271 -> xml ctx inp []) =
|
adam@1405
|
272 let
|
adam@1405
|
273 fun qxi ls i =
|
adam@1405
|
274 case ls of
|
adam@1405
|
275 [] => <xml/>
|
adam@1405
|
276 | x :: ls => <xml>{f i x}{qxi ls (i+1)}</xml>
|
adam@1405
|
277 in
|
adam@1405
|
278 ls <- queryL q;
|
adam@1405
|
279 return (qxi ls 0)
|
adam@1405
|
280 end
|
adam@1405
|
281
|
adamc@1076
|
282 fun queryX1 [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
|
adam@1394
|
283 (q : sql_query [] [] [nm = fs] [])
|
adamc@1076
|
284 (f : $fs -> xml ctx inp []) =
|
adamc@1076
|
285 query q
|
adamc@1076
|
286 (fn fs acc => return <xml>{acc}{f fs.nm}</xml>)
|
adamc@1076
|
287 <xml/>
|
adamc@1076
|
288
|
adam@1405
|
289 fun queryX1I [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
|
adam@1405
|
290 (q : sql_query [] [] [nm = fs] [])
|
adam@1405
|
291 (f : int -> $fs -> xml ctx inp []) =
|
adam@1405
|
292 let
|
adam@1405
|
293 fun qx1i ls i =
|
adam@1405
|
294 case ls of
|
adam@1405
|
295 [] => <xml/>
|
adam@1405
|
296 | x :: ls => <xml>{f i x.nm}{qx1i ls (i+1)}</xml>
|
adam@1405
|
297 in
|
adam@1405
|
298 ls <- queryL q;
|
adam@1405
|
299 return (qx1i ls 0)
|
adam@1405
|
300 end
|
adam@1405
|
301
|
adamc@1032
|
302 fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
|
adam@1394
|
303 [tables ~ exps] (q : sql_query [] [] tables exps)
|
adamc@621
|
304 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
|
adamc@1032
|
305 -> transaction (xml ctx inp [])) =
|
adamc@469
|
306 query q
|
adamc@469
|
307 (fn fs acc =>
|
adamc@469
|
308 r <- f fs;
|
adamc@469
|
309 return <xml>{acc}{r}</xml>)
|
adamc@469
|
310 <xml/>
|
adamc@469
|
311
|
adamc@1110
|
312 fun queryX1' [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
|
adam@1394
|
313 (q : sql_query [] [] [nm = fs] [])
|
adamc@1110
|
314 (f : $fs -> transaction (xml ctx inp [])) =
|
adamc@1110
|
315 query q
|
adamc@1110
|
316 (fn fs acc =>
|
adamc@1110
|
317 r <- f fs.nm;
|
adamc@1110
|
318 return <xml>{acc}{r}</xml>)
|
adamc@1110
|
319 <xml/>
|
adamc@1110
|
320
|
adamc@1110
|
321 fun queryXE' [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
|
adam@1394
|
322 (q : sql_query [] [] [] exps)
|
adamc@1110
|
323 (f : $exps -> transaction (xml ctx inp [])) =
|
adamc@1110
|
324 query q
|
adamc@1110
|
325 (fn fs acc =>
|
adamc@1110
|
326 r <- f fs;
|
adamc@1110
|
327 return <xml>{acc}{r}</xml>)
|
adamc@1110
|
328 <xml/>
|
adamc@1110
|
329
|
adamc@1072
|
330 fun hasRows [tables ::: {{Type}}] [exps ::: {Type}]
|
adamc@1072
|
331 [tables ~ exps]
|
adam@1394
|
332 (q : sql_query [] [] tables exps) =
|
adamc@1072
|
333 query q
|
adamc@1072
|
334 (fn _ _ => return True)
|
adamc@1072
|
335 False
|
adamc@1072
|
336
|
adamc@822
|
337 fun oneOrNoRows [tables ::: {{Type}}] [exps ::: {Type}]
|
adamc@629
|
338 [tables ~ exps]
|
adam@1394
|
339 (q : sql_query [] [] tables exps) =
|
adamc@356
|
340 query q
|
adamc@356
|
341 (fn fs _ => return (Some fs))
|
adamc@356
|
342 None
|
adamc@440
|
343
|
adam@1394
|
344 fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] []) =
|
adamc@1003
|
345 query q
|
adamc@1003
|
346 (fn fs _ => return (Some fs.nm))
|
adamc@1003
|
347 None
|
adamc@1003
|
348
|
adam@1394
|
349 fun oneOrNoRowsE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] [] (mapU [] tabs) [nm = t]) =
|
adamc@1006
|
350 query q
|
adamc@1006
|
351 (fn fs _ => return (Some fs.nm))
|
adamc@1006
|
352 None
|
adamc@1006
|
353
|
adamc@822
|
354 fun oneRow [tables ::: {{Type}}] [exps ::: {Type}]
|
adam@1394
|
355 [tables ~ exps] (q : sql_query [] [] tables exps) =
|
adamc@440
|
356 o <- oneOrNoRows q;
|
adamc@440
|
357 return (case o of
|
adamc@440
|
358 None => error <xml>Query returned no rows</xml>
|
adamc@440
|
359 | Some r => r)
|
adamc@440
|
360
|
adam@1394
|
361 fun oneRow1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] []) =
|
adamc@1076
|
362 o <- oneOrNoRows q;
|
adamc@1076
|
363 return (case o of
|
adamc@1076
|
364 None => error <xml>Query returned no rows</xml>
|
adamc@1076
|
365 | Some r => r.nm)
|
adamc@1076
|
366
|
adam@1394
|
367 fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] [] (mapU [] tabs) [nm = t]) =
|
adamc@1003
|
368 o <- oneOrNoRows q;
|
adamc@1003
|
369 return (case o of
|
adamc@1003
|
370 None => error <xml>Query returned no rows</xml>
|
adamc@1003
|
371 | Some r => r.nm)
|
adamc@1003
|
372
|
adamc@1074
|
373 fun nonempty [fs] [us] (t : sql_table fs us) =
|
adamc@1074
|
374 oneRowE1 (SELECT COUNT( * ) > 0 AS B FROM t)
|
adamc@1074
|
375
|
adamc@822
|
376 fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
|
adamc@822
|
377 [t ::: Type] (_ : sql_injectable (option t))
|
adamc@470
|
378 (e1 : sql_exp tables agg exps (option t))
|
adamc@470
|
379 (e2 : sql_exp tables agg exps (option t)) =
|
adamc@471
|
380 (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2})
|
adamc@470
|
381
|
adamc@822
|
382 fun eqNullable' [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
|
adamc@822
|
383 [t ::: Type] (_ : sql_injectable (option t))
|
adamc@470
|
384 (e1 : sql_exp tables agg exps (option t))
|
adamc@470
|
385 (e2 : option t) =
|
adamc@470
|
386 case e2 of
|
adamc@471
|
387 None => (SQL {e1} IS NULL)
|
adamc@564
|
388 | Some _ => sql_binary sql_eq e1 (sql_inject e2)
|
adam@1360
|
389
|
adam@1360
|
390 fun mkRead' [t ::: Type] (f : string -> option t) (name : string) : read t =
|
adam@1360
|
391 mkRead (fn s => case f s of
|
adam@1360
|
392 None => error <xml>Invalid {txt name}: {txt s}</xml>
|
adam@1360
|
393 | Some v => v) f
|