Mercurial > urweb

annotate lib/ur/top.ur @ 1775:6bc2a8cb3a67

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Track whether SQL expressions may use window functions, in preparation for actual window function support
author Adam Chlipala <adam@chlipala.net>
date Sat, 02 Jun 2012 15:35:58 -0400
parents 9253765d7724
children 818d4097e2ed
rev   line source
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))
adam@1472 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] =>
adam@1472 36 f [nm] [v] [r1' ++ r2] acc)
adam@1472 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)) =>
adam@1472 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
adam@1649 54 con ident = 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
adam@1434 64 con ex = K ==> fn tf :: (K -> Type) =>
adam@1434 65 res ::: Type -> (choice :: K -> tf choice -> res) -> res
adamc@339 66
adam@1434 67 fun ex_intro [K] [tf :: K -> Type] [choice :: K] (body : tf choice) : ex tf =
adam@1434 68 fn [res] (f : choice :: K -> tf choice -> res) =>
adamc@356 69 f [choice] body
adamc@339 70
adam@1434 71 fun ex_elim [K] [tf ::: K -> Type] (v : ex tf) [res ::: Type] = @@v [res]
adam@1434 72
adamc@822 73 fun compose [t1 ::: Type] [t2 ::: Type] [t3 ::: Type]
adamc@356 74 (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x)
adamc@325 75
adamc@822 76 fun show_option [t ::: Type] (_ : show t) =
adamc@777 77 mkShow (fn opt : option t =>
adamc@777 78 case opt of
adamc@777 79 None => ""
adamc@777 80 | Some x => show x)
adamc@777 81
adamc@822 82 fun read_option [t ::: Type] (_ : read t) =
adamc@777 83 mkRead (fn s =>
adamc@777 84 case s of
adamc@777 85 "" => None
adamc@777 86 | _ => Some (readError s : t))
adamc@777 87 (fn s =>
adamc@777 88 case s of
adamc@777 89 "" => Some None
adamc@777 90 | _ => case read s of
adamc@777 91 None => None
adamc@777 92 | v => Some v)
adamc@777 93
adam@1360 94 fun txt [t] [ctx ::: {Unit}] [use ::: {Type}] (_ : show t) (v : t) : xml ctx use [] =
adamc@564 95 cdata (show v)
adamc@328 96
adamc@1093 97 fun map0 [K] [tf :: K -> Type] (f : t :: K -> tf t) [r ::: {K}] (fl : folder r) =
adamc@993 98 fl [fn r :: {K} => $(map tf r)]
adamc@993 99 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc =>
adamc@993 100 acc ++ {nm = f [t]})
adamc@993 101 {}
adamc@993 102
adamc@1093 103 fun mp [K] [tf1 :: K -> Type] [tf2 :: K -> Type] (f : t ::: K -> tf1 t -> tf2 t) [r ::: {K}] (fl : folder r) =
adamc@898 104 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r)]
adamc@898 105 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r =>
adamc@898 106 acc (r -- nm) ++ {nm = f r.nm})
adamc@898 107 (fn _ => {})
adamc@898 108
adamc@905 109 fun map2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type]
adamc@1093 110 (f : t ::: K -> tf1 t -> tf2 t -> tf3 t) [r ::: {K}] (fl : folder r) =
adamc@905 111 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r)]
adamc@905 112 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 =>
adamc@905 113 acc (r1 -- nm) (r2 -- nm) ++ {nm = f r1.nm r2.nm})
adamc@905 114 (fn _ _ => {})
adamc@898 115
adamc@937 116 fun map3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tf :: K -> Type]
adamc@1093 117 (f : t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) [r ::: {K}] (fl : folder r) =
adamc@937 118 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)]
adamc@937 119 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 r3 =>
adamc@937 120 acc (r1 -- nm) (r2 -- nm) (r3 -- nm) ++ {nm = f r1.nm r2.nm r3.nm})
adamc@937 121 (fn _ _ _ => {})
adamc@937 122
adamc@822 123 fun foldUR [tf :: Type] [tr :: {Unit} -> Type]
adamc@411 124 (f : nm :: Name -> rest :: {Unit}
adamc@629 125 -> [[nm] ~ rest] =>
adamc@411 126 tf -> tr rest -> tr ([nm] ++ rest))
adamc@1093 127 (i : tr []) [r ::: {Unit}] (fl : folder r) =
adamc@653 128 fl [fn r :: {Unit} => $(mapU tf r) -> tr r]
adamc@822 129 (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r =>
adam@1472 130 f [nm] [rest] r.nm (acc (r -- nm)))
adamc@653 131 (fn _ => i)
adamc@411 132
adamc@822 133 fun foldUR2 [tf1 :: Type] [tf2 :: Type] [tr :: {Unit} -> Type]
adamc@418 134 (f : nm :: Name -> rest :: {Unit}
adamc@629 135 -> [[nm] ~ rest] =>
adamc@418 136 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
adamc@1093 137 (i : tr []) [r ::: {Unit}] (fl : folder r) =
adamc@653 138 fl [fn r :: {Unit} => $(mapU tf1 r) -> $(mapU tf2 r) -> tr r]
adamc@822 139 (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r1 r2 =>
adam@1472 140 f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
adamc@653 141 (fn _ _ => i)
adamc@418 142
adamc@822 143 fun foldR [K] [tf :: K -> Type] [tr :: {K} -> Type]
adamc@623 144 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@629 145 -> [[nm] ~ rest] =>
adamc@356 146 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@1093 147 (i : tr []) [r ::: {K}] (fl : folder r) =
adamc@653 148 fl [fn r :: {K} => $(map tf r) -> tr r]
adamc@822 149 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> tr rest) r =>
adam@1472 150 f [nm] [t] [rest] r.nm (acc (r -- nm)))
adamc@653 151 (fn _ => i)
adamc@336 152
adamc@822 153 fun foldR2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type]
adamc@623 154 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@629 155 -> [[nm] ~ rest] =>
adamc@367 156 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@1093 157 (i : tr []) [r ::: {K}] (fl : folder r) =
adamc@653 158 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r]
adamc@822 159 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@653 160 (acc : _ -> _ -> tr rest) r1 r2 =>
adam@1472 161 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
adamc@653 162 (fn _ _ => i)
adamc@332 163
adamc@910 164 fun foldR3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type]
adamc@910 165 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@910 166 -> [[nm] ~ rest] =>
adamc@910 167 tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@1093 168 (i : tr []) [r ::: {K}] (fl : folder r) =
adamc@910 169 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r]
adamc@910 170 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@910 171 (acc : _ -> _ -> _ -> tr rest) r1 r2 r3 =>
adam@1472 172 f [nm] [t] [rest] r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm)))
adamc@910 173 (fn _ _ _ => i)
adamc@910 174
adamc@1172 175 fun mapUX [tf :: Type] [ctx :: {Unit}]
adamc@1172 176 (f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf -> xml ctx [] []) =
adamc@1172 177 @@foldR [fn _ => tf] [fn _ => xml ctx [] []]
adamc@1172 178 (fn [nm :: Name] [u :: Unit] [rest :: {Unit}] [[nm] ~ rest] r acc =>
adam@1472 179 <xml>{f [nm] [rest] r}{acc}</xml>)
adamc@1172 180 <xml/>
adamc@1172 181
adamc@1172 182 fun mapX [K] [tf :: K -> Type] [ctx :: {Unit}]
adamc@623 183 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@629 184 -> [[nm] ~ rest] =>
adamc@720 185 tf t -> xml ctx [] []) =
adamc@1093 186 @@foldR [tf] [fn _ => xml ctx [] []]
adamc@1093 187 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc =>
adam@1472 188 <xml>{f [nm] [t] [rest] r}{acc}</xml>)
adamc@1093 189 <xml/>
adamc@336 190
adamc@1173 191 fun mapUX2 [tf1 :: Type] [tf2 :: Type] [ctx :: {Unit}]
adamc@1173 192 (f : nm :: Name -> rest :: {Unit}
adamc@1173 193 -> [[nm] ~ rest] =>
adamc@1173 194 tf1 -> tf2 -> xml ctx [] []) =
adamc@1173 195 @@foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
adamc@1173 196 (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] v1 v2 acc =>
adam@1472 197 <xml>{f [nm] [rest] v1 v2}{acc}</xml>)
adamc@1173 198 <xml/>
adamc@1173 199
adamc@1172 200 fun mapX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}]
adamc@623 201 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@629 202 -> [[nm] ~ rest] =>
adamc@720 203 tf1 t -> tf2 t -> xml ctx [] []) =
adamc@1093 204 @@foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
adamc@1093 205 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@1093 206 r1 r2 acc =>
adam@1472 207 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
adamc@1093 208 <xml/>
adamc@445 209
adamc@1172 210 fun mapX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}]
adamc@910 211 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@910 212 -> [[nm] ~ rest] =>
adamc@910 213 tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) =
adamc@1093 214 @@foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []]
adamc@1093 215 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@1093 216 r1 r2 r3 acc =>
adam@1472 217 <xml>{f [nm] [t] [rest] r1 r2 r3}{acc}</xml>)
adamc@1093 218 <xml/>
adamc@910 219
adam@1394 220 fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [] [t = fs] [])
adamc@1177 221 (f : $fs -> state -> transaction state) (i : state) =
adamc@1177 222 query q (fn r => f r.t) i
adamc@1177 223
adam@1394 224 fun query1' [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [] [t = fs] [])
adamc@1177 225 (f : $fs -> state -> state) (i : state) =
adamc@1177 226 query q (fn r s => return (f r.t s)) i
adamc@1177 227
adam@1394 228 fun queryL [tables] [exps] [tables ~ exps] (q : sql_query [] [] tables exps) =
adamc@1081 229 query q
adamc@1081 230 (fn r ls => return (r :: ls))
adamc@1081 231 []
adamc@1081 232
adam@1394 233 fun queryL1 [t ::: Name] [fs ::: {Type}] (q : sql_query [] [] [t = fs] []) =
adam@1321 234 query q
adam@1321 235 (fn r ls => return (r.t :: ls))
adam@1321 236 []
adam@1321 237
adamc@822 238 fun queryI [tables ::: {{Type}}] [exps ::: {Type}]
adam@1394 239 [tables ~ exps] (q : sql_query [] [] tables exps)
adamc@682 240 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@682 241 -> transaction unit) =
adamc@682 242 query q
adamc@682 243 (fn fs _ => f fs)
adamc@682 244 ()
adamc@682 245
adam@1394 246 fun queryI1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] [])
adam@1363 247 (f : $fs -> transaction unit) =
adam@1363 248 query q
adam@1363 249 (fn fs _ => f fs.nm)
adam@1363 250 ()
adam@1363 251
adamc@1004 252 fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
adam@1394 253 [tables ~ exps] (q : sql_query [] [] tables exps)
adamc@621 254 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@1004 255 -> xml ctx inp []) =
adamc@356 256 query q
adamc@356 257 (fn fs acc => return <xml>{acc}{f fs}</xml>)
adamc@360 258 <xml/>
adamc@341 259
adam@1405 260 fun rev [a] (ls : list a) : list a =
adam@1405 261 let
adam@1405 262 fun rev' ls acc =
adam@1405 263 case ls of
adam@1405 264 [] => acc
adam@1405 265 | x :: ls => rev' ls (x :: acc)
adam@1405 266 in
adam@1405 267 rev' ls []
adam@1405 268 end
adam@1405 269
adam@1405 270 fun queryXI [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
adam@1405 271 [tables ~ exps] (q : sql_query [] [] tables exps)
adam@1405 272 (f : int -> $(exps ++ map (fn fields :: {Type} => $fields) tables)
adam@1405 273 -> xml ctx inp []) =
adam@1405 274 let
adam@1405 275 fun qxi ls i =
adam@1405 276 case ls of
adam@1405 277 [] => <xml/>
adam@1405 278 | x :: ls => <xml>{f i x}{qxi ls (i+1)}</xml>
adam@1405 279 in
adam@1405 280 ls <- queryL q;
adam@1406 281 return (qxi (rev ls) 0)
adam@1405 282 end
adam@1405 283
adamc@1076 284 fun queryX1 [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
adam@1394 285 (q : sql_query [] [] [nm = fs] [])
adamc@1076 286 (f : $fs -> xml ctx inp []) =
adamc@1076 287 query q
adamc@1076 288 (fn fs acc => return <xml>{acc}{f fs.nm}</xml>)
adamc@1076 289 <xml/>
adamc@1076 290
adam@1405 291 fun queryX1I [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
adam@1405 292 (q : sql_query [] [] [nm = fs] [])
adam@1405 293 (f : int -> $fs -> xml ctx inp []) =
adam@1405 294 let
adam@1405 295 fun qx1i ls i =
adam@1405 296 case ls of
adam@1405 297 [] => <xml/>
adam@1405 298 | x :: ls => <xml>{f i x.nm}{qx1i ls (i+1)}</xml>
adam@1405 299 in
adam@1405 300 ls <- queryL q;
adam@1406 301 return (qx1i (rev ls) 0)
adam@1405 302 end
adam@1405 303
adamc@1032 304 fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
adam@1394 305 [tables ~ exps] (q : sql_query [] [] tables exps)
adamc@621 306 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@1032 307 -> transaction (xml ctx inp [])) =
adamc@469 308 query q
adamc@469 309 (fn fs acc =>
adamc@469 310 r <- f fs;
adamc@469 311 return <xml>{acc}{r}</xml>)
adamc@469 312 <xml/>
adamc@469 313
adamc@1110 314 fun queryX1' [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
adam@1394 315 (q : sql_query [] [] [nm = fs] [])
adamc@1110 316 (f : $fs -> transaction (xml ctx inp [])) =
adamc@1110 317 query q
adamc@1110 318 (fn fs acc =>
adamc@1110 319 r <- f fs.nm;
adamc@1110 320 return <xml>{acc}{r}</xml>)
adamc@1110 321 <xml/>
adamc@1110 322
adamc@1110 323 fun queryXE' [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
adam@1394 324 (q : sql_query [] [] [] exps)
adamc@1110 325 (f : $exps -> transaction (xml ctx inp [])) =
adamc@1110 326 query q
adamc@1110 327 (fn fs acc =>
adamc@1110 328 r <- f fs;
adamc@1110 329 return <xml>{acc}{r}</xml>)
adamc@1110 330 <xml/>
adamc@1110 331
adamc@1072 332 fun hasRows [tables ::: {{Type}}] [exps ::: {Type}]
adamc@1072 333 [tables ~ exps]
adam@1394 334 (q : sql_query [] [] tables exps) =
adamc@1072 335 query q
adamc@1072 336 (fn _ _ => return True)
adamc@1072 337 False
adamc@1072 338
adamc@822 339 fun oneOrNoRows [tables ::: {{Type}}] [exps ::: {Type}]
adamc@629 340 [tables ~ exps]
adam@1394 341 (q : sql_query [] [] tables exps) =
adamc@356 342 query q
adamc@356 343 (fn fs _ => return (Some fs))
adamc@356 344 None
adamc@440 345
adam@1394 346 fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] []) =
adamc@1003 347 query q
adamc@1003 348 (fn fs _ => return (Some fs.nm))
adamc@1003 349 None
adamc@1003 350
adam@1394 351 fun oneOrNoRowsE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] [] (mapU [] tabs) [nm = t]) =
adamc@1006 352 query q
adamc@1006 353 (fn fs _ => return (Some fs.nm))
adamc@1006 354 None
adamc@1006 355
adamc@822 356 fun oneRow [tables ::: {{Type}}] [exps ::: {Type}]
adam@1394 357 [tables ~ exps] (q : sql_query [] [] tables exps) =
adamc@440 358 o <- oneOrNoRows q;
adamc@440 359 return (case o of
adamc@440 360 None => error <xml>Query returned no rows</xml>
adamc@440 361 | Some r => r)
adamc@440 362
adam@1394 363 fun oneRow1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] []) =
adamc@1076 364 o <- oneOrNoRows q;
adamc@1076 365 return (case o of
adamc@1076 366 None => error <xml>Query returned no rows</xml>
adamc@1076 367 | Some r => r.nm)
adamc@1076 368
adam@1394 369 fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] [] (mapU [] tabs) [nm = t]) =
adamc@1003 370 o <- oneOrNoRows q;
adamc@1003 371 return (case o of
adamc@1003 372 None => error <xml>Query returned no rows</xml>
adamc@1003 373 | Some r => r.nm)
adamc@1003 374
adamc@1074 375 fun nonempty [fs] [us] (t : sql_table fs us) =
adamc@1074 376 oneRowE1 (SELECT COUNT( * ) > 0 AS B FROM t)
adamc@1074 377
adamc@822 378 fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
adam@1775 379 [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t))
adam@1775 380 (e1 : sql_exp tables agg exps aw (option t))
adam@1775 381 (e2 : sql_exp tables agg exps aw (option t)) =
adamc@471 382 (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2})
adamc@470 383
adamc@822 384 fun eqNullable' [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
adam@1775 385 [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t))
adam@1775 386 (e1 : sql_exp tables agg exps aw (option t))
adamc@470 387 (e2 : option t) =
adamc@470 388 case e2 of
adamc@471 389 None => (SQL {e1} IS NULL)
adamc@564 390 | Some _ => sql_binary sql_eq e1 (sql_inject e2)
adam@1360 391
adam@1360 392 fun mkRead' [t ::: Type] (f : string -> option t) (name : string) : read t =
adam@1360 393 mkRead (fn s => case f s of
adam@1360 394 None => error <xml>Invalid {txt name}: {txt s}</xml>
adam@1360 395 | Some v => v) f