Mercurial > urweb

annotate lib/ur/top.ur @ 1076:dcf98ae3c48d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Allow same constructor shorthand for 'view' sig items as for 'table'
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Dec 2009 11:11:49 -0500
parents d89f98f0b4bb
children 25d491287358
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@822 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
adamc@822 92 fun txt [t] [ctx ::: {Unit}] [use ::: {Type}] (_ : show t) (v : t) =
adamc@564 93 cdata (show v)
adamc@328 94
adamc@993 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@898 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@905 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@937 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@898 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@822 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 foldURX2 [tf1 :: Type] [tf2 :: Type] [ctx :: {Unit}]
adamc@418 142 (f : nm :: Name -> rest :: {Unit}
adamc@629 143 -> [[nm] ~ rest] =>
adamc@720 144 tf1 -> tf2 -> xml ctx [] []) =
adamc@720 145 foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
adamc@822 146 (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] v1 v2 acc =>
adamc@629 147 <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>)
adamc@418 148 <xml/>
adamc@418 149
adamc@822 150 fun foldR [K] [tf :: K -> Type] [tr :: {K} -> Type]
adamc@623 151 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@629 152 -> [[nm] ~ rest] =>
adamc@356 153 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@822 154 (i : tr []) [r :: {K}] (fl : folder r) =
adamc@653 155 fl [fn r :: {K} => $(map tf r) -> tr r]
adamc@822 156 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> tr rest) r =>
adamc@653 157 f [nm] [t] [rest] ! r.nm (acc (r -- nm)))
adamc@653 158 (fn _ => i)
adamc@336 159
adamc@822 160 fun foldR2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type]
adamc@623 161 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@629 162 -> [[nm] ~ rest] =>
adamc@367 163 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@822 164 (i : tr []) [r :: {K}] (fl : folder r) =
adamc@653 165 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r]
adamc@822 166 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@653 167 (acc : _ -> _ -> tr rest) r1 r2 =>
adamc@653 168 f [nm] [t] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
adamc@653 169 (fn _ _ => i)
adamc@332 170
adamc@910 171 fun foldR3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type]
adamc@910 172 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@910 173 -> [[nm] ~ rest] =>
adamc@910 174 tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@910 175 (i : tr []) [r :: {K}] (fl : folder r) =
adamc@910 176 fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r]
adamc@910 177 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@910 178 (acc : _ -> _ -> _ -> tr rest) r1 r2 r3 =>
adamc@910 179 f [nm] [t] [rest] ! r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm)))
adamc@910 180 (fn _ _ _ => i)
adamc@910 181
adamc@822 182 fun foldRX [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@720 186 foldR [tf] [fn _ => xml ctx [] []]
adamc@822 187 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc =>
adamc@629 188 <xml>{f [nm] [t] [rest] ! r}{acc}</xml>)
adamc@623 189 <xml/>
adamc@336 190
adamc@822 191 fun foldRX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}]
adamc@623 192 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@629 193 -> [[nm] ~ rest] =>
adamc@720 194 tf1 t -> tf2 t -> xml ctx [] []) =
adamc@720 195 foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
adamc@822 196 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@623 197 r1 r2 acc =>
adamc@629 198 <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>)
adamc@623 199 <xml/>
adamc@445 200
adamc@910 201 fun foldRX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}]
adamc@910 202 (f : nm :: Name -> t :: K -> rest :: {K}
adamc@910 203 -> [[nm] ~ rest] =>
adamc@910 204 tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) =
adamc@910 205 foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []]
adamc@910 206 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
adamc@910 207 r1 r2 r3 acc =>
adamc@910 208 <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>)
adamc@910 209 <xml/>
adamc@910 210
adamc@822 211 fun queryI [tables ::: {{Type}}] [exps ::: {Type}]
adamc@682 212 [tables ~ exps] (q : sql_query tables exps)
adamc@682 213 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@682 214 -> transaction unit) =
adamc@682 215 query q
adamc@682 216 (fn fs _ => f fs)
adamc@682 217 ()
adamc@682 218
adamc@1004 219 fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
adamc@632 220 [tables ~ exps] (q : sql_query tables exps)
adamc@621 221 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@1004 222 -> xml ctx inp []) =
adamc@356 223 query q
adamc@356 224 (fn fs acc => return <xml>{acc}{f fs}</xml>)
adamc@360 225 <xml/>
adamc@341 226
adamc@1076 227 fun queryX1 [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
adamc@1076 228 (q : sql_query [nm = fs] [])
adamc@1076 229 (f : $fs -> xml ctx inp []) =
adamc@1076 230 query q
adamc@1076 231 (fn fs acc => return <xml>{acc}{f fs.nm}</xml>)
adamc@1076 232 <xml/>
adamc@1076 233
adamc@1032 234 fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}]
adamc@632 235 [tables ~ exps] (q : sql_query tables exps)
adamc@621 236 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@1032 237 -> transaction (xml ctx inp [])) =
adamc@469 238 query q
adamc@469 239 (fn fs acc =>
adamc@469 240 r <- f fs;
adamc@469 241 return <xml>{acc}{r}</xml>)
adamc@469 242 <xml/>
adamc@469 243
adamc@1072 244 fun hasRows [tables ::: {{Type}}] [exps ::: {Type}]
adamc@1072 245 [tables ~ exps]
adamc@1072 246 (q : sql_query tables exps) =
adamc@1072 247 query q
adamc@1072 248 (fn _ _ => return True)
adamc@1072 249 False
adamc@1072 250
adamc@822 251 fun oneOrNoRows [tables ::: {{Type}}] [exps ::: {Type}]
adamc@629 252 [tables ~ exps]
adamc@1003 253 (q : sql_query tables exps) =
adamc@356 254 query q
adamc@356 255 (fn fs _ => return (Some fs))
adamc@356 256 None
adamc@440 257
adamc@1003 258 fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [nm = fs] []) =
adamc@1003 259 query q
adamc@1003 260 (fn fs _ => return (Some fs.nm))
adamc@1003 261 None
adamc@1003 262
adamc@1076 263 fun oneOrNoRowsE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query (mapU [] tabs) [nm = t]) =
adamc@1006 264 query q
adamc@1006 265 (fn fs _ => return (Some fs.nm))
adamc@1006 266 None
adamc@1006 267
adamc@822 268 fun oneRow [tables ::: {{Type}}] [exps ::: {Type}]
adamc@822 269 [tables ~ exps] (q : sql_query tables exps) =
adamc@440 270 o <- oneOrNoRows q;
adamc@440 271 return (case o of
adamc@440 272 None => error <xml>Query returned no rows</xml>
adamc@440 273 | Some r => r)
adamc@440 274
adamc@1076 275 fun oneRow1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [nm = fs] []) =
adamc@1076 276 o <- oneOrNoRows q;
adamc@1076 277 return (case o of
adamc@1076 278 None => error <xml>Query returned no rows</xml>
adamc@1076 279 | Some r => r.nm)
adamc@1076 280
adamc@1064 281 fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query (mapU [] tabs) [nm = t]) =
adamc@1003 282 o <- oneOrNoRows q;
adamc@1003 283 return (case o of
adamc@1003 284 None => error <xml>Query returned no rows</xml>
adamc@1003 285 | Some r => r.nm)
adamc@1003 286
adamc@1074 287 fun nonempty [fs] [us] (t : sql_table fs us) =
adamc@1074 288 oneRowE1 (SELECT COUNT( * ) > 0 AS B FROM t)
adamc@1074 289
adamc@822 290 fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
adamc@822 291 [t ::: Type] (_ : sql_injectable (option t))
adamc@470 292 (e1 : sql_exp tables agg exps (option t))
adamc@470 293 (e2 : sql_exp tables agg exps (option t)) =
adamc@471 294 (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2})
adamc@470 295
adamc@822 296 fun eqNullable' [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}]
adamc@822 297 [t ::: Type] (_ : sql_injectable (option t))
adamc@470 298 (e1 : sql_exp tables agg exps (option t))
adamc@470 299 (e2 : option t) =
adamc@470 300 case e2 of
adamc@471 301 None => (SQL {e1} IS NULL)
adamc@564 302 | Some _ => sql_binary sql_eq e1 (sql_inject e2)