Mercurial > urweb

annotate lib/top.ur @ 597:d49d58a69877

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Injected a non-special-case datatype
author Adam Chlipala <adamc@hcoop.net>
date Thu, 08 Jan 2009 10:30:14 -0500
parents 803b2f3bb86b
children
rev   line source
adamc@422 1 fun not b = if b then False else True
adamc@422 2
adamc@356 3 con idT (t :: Type) = t
adamc@356 4 con record (t :: {Type}) = $t
adamc@356 5 con fstTT (t :: (Type * Type)) = t.1
adamc@356 6 con sndTT (t :: (Type * Type)) = t.2
adamc@445 7 con fstTTT (t :: (Type * Type * Type)) = t.1
adamc@445 8 con sndTTT (t :: (Type * Type * Type)) = t.2
adamc@445 9 con thdTTT (t :: (Type * Type * Type)) = t.3
adamc@329 10
adamc@356 11 con mapTT (f :: Type -> Type) = fold (fn nm t acc [[nm] ~ acc] =>
adamc@356 12 [nm = f t] ++ acc) []
adamc@325 13
adamc@411 14 con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] =>
adamc@411 15 [nm = f] ++ acc) []
adamc@411 16
adamc@356 17 con mapT2T (f :: (Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] =>
adamc@356 18 [nm = f t] ++ acc) []
adamc@339 19
adamc@445 20 con mapT3T (f :: (Type * Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] =>
adamc@445 21 [nm = f t] ++ acc) []
adamc@445 22
adamc@339 23 con ex = fn tf :: (Type -> Type) =>
adamc@356 24 res ::: Type -> (choice :: Type -> tf choice -> res) -> res
adamc@339 25
adamc@339 26 fun ex (tf :: (Type -> Type)) (choice :: Type) (body : tf choice) : ex tf =
adamc@356 27 fn (res ::: Type) (f : choice :: Type -> tf choice -> res) =>
adamc@356 28 f [choice] body
adamc@339 29
adamc@356 30 fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type)
adamc@356 31 (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x)
adamc@325 32
adamc@564 33 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) =
adamc@564 34 cdata (show v)
adamc@328 35
adamc@411 36 fun foldUR (tf :: Type) (tr :: {Unit} -> Type)
adamc@411 37 (f : nm :: Name -> rest :: {Unit}
adamc@411 38 -> fn [[nm] ~ rest] =>
adamc@411 39 tf -> tr rest -> tr ([nm] ++ rest))
adamc@411 40 (i : tr []) =
adamc@411 41 fold [fn r :: {Unit} => $(mapUT tf r) -> tr r]
adamc@412 42 (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
adamc@412 43 [[nm] ~ rest] r =>
adamc@411 44 f [nm] [rest] r.nm (acc (r -- nm)))
adamc@411 45 (fn _ => i)
adamc@411 46
adamc@418 47 fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type)
adamc@418 48 (f : nm :: Name -> rest :: {Unit}
adamc@418 49 -> fn [[nm] ~ rest] =>
adamc@418 50 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
adamc@418 51 (i : tr []) =
adamc@418 52 fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r]
adamc@418 53 (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
adamc@418 54 [[nm] ~ rest] r1 r2 =>
adamc@418 55 f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
adamc@418 56 (fn _ _ => i)
adamc@418 57
adamc@418 58 fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit})
adamc@418 59 (f : nm :: Name -> rest :: {Unit}
adamc@418 60 -> fn [[nm] ~ rest] =>
adamc@418 61 tf1 -> tf2 -> xml ctx [] []) =
adamc@418 62 foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
adamc@418 63 (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] v1 v2 acc =>
adamc@418 64 <xml>{f [nm] [rest] v1 v2}{acc}</xml>)
adamc@418 65 <xml/>
adamc@418 66
adamc@336 67 fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
adamc@356 68 (f : nm :: Name -> t :: Type -> rest :: {Type}
adamc@356 69 -> fn [[nm] ~ rest] =>
adamc@356 70 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@356 71 (i : tr []) =
adamc@356 72 fold [fn r :: {Type} => $(mapTT tf r) -> tr r]
adamc@356 73 (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest)
adamc@356 74 [[nm] ~ rest] r =>
adamc@356 75 f [nm] [t] [rest] r.nm (acc (r -- nm)))
adamc@356 76 (fn _ => i)
adamc@336 77
adamc@339 78 fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
adamc@367 79 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
adamc@367 80 -> fn [[nm] ~ rest] =>
adamc@367 81 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@367 82 (i : tr []) =
adamc@356 83 fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r]
adamc@356 84 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
adamc@356 85 (acc : _ -> tr rest) [[nm] ~ rest] r =>
adamc@356 86 f [nm] [t] [rest] r.nm (acc (r -- nm)))
adamc@356 87 (fn _ => i)
adamc@339 88
adamc@445 89 fun foldT3R (tf :: (Type * Type * Type) -> Type) (tr :: {(Type * Type * Type)} -> Type)
adamc@445 90 (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
adamc@445 91 -> fn [[nm] ~ rest] =>
adamc@445 92 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@445 93 (i : tr []) =
adamc@445 94 fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf r) -> tr r]
adamc@445 95 (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
adamc@445 96 (acc : _ -> tr rest) [[nm] ~ rest] r =>
adamc@445 97 f [nm] [t] [rest] r.nm (acc (r -- nm)))
adamc@445 98 (fn _ => i)
adamc@445 99
adamc@330 100 fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
adamc@367 101 (f : nm :: Name -> t :: Type -> rest :: {Type}
adamc@367 102 -> fn [[nm] ~ rest] =>
adamc@367 103 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@367 104 (i : tr []) =
adamc@356 105 fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r]
adamc@356 106 (fn (nm :: Name) (t :: Type) (rest :: {Type})
adamc@356 107 (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
adamc@356 108 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
adamc@356 109 (fn _ _ => i)
adamc@332 110
adamc@356 111 fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type)
adamc@356 112 (tr :: {(Type * Type)} -> Type)
adamc@356 113 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
adamc@356 114 -> fn [[nm] ~ rest] =>
adamc@356 115 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@356 116 (i : tr []) =
adamc@356 117 fold [fn r :: {(Type * Type)} => $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r]
adamc@356 118 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
adamc@356 119 (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
adamc@356 120 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
adamc@356 121 (fn _ _ => i)
adamc@339 122
adamc@445 123 fun foldT3R2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type)
adamc@445 124 (tr :: {(Type * Type * Type)} -> Type)
adamc@445 125 (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
adamc@445 126 -> fn [[nm] ~ rest] =>
adamc@445 127 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@445 128 (i : tr []) =
adamc@445 129 fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r]
adamc@445 130 (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
adamc@445 131 (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
adamc@445 132 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
adamc@445 133 (fn _ _ => i)
adamc@445 134
adamc@336 135 fun foldTRX (tf :: Type -> Type) (ctx :: {Unit})
adamc@356 136 (f : nm :: Name -> t :: Type -> rest :: {Type}
adamc@356 137 -> fn [[nm] ~ rest] =>
adamc@356 138 tf t -> xml ctx [] []) =
adamc@356 139 foldTR [tf] [fn _ => xml ctx [] []]
adamc@356 140 (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] r acc =>
adamc@356 141 <xml>{f [nm] [t] [rest] r}{acc}</xml>)
adamc@360 142 <xml/>
adamc@336 143
adamc@339 144 fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit})
adamc@356 145 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
adamc@356 146 -> fn [[nm] ~ rest] =>
adamc@356 147 tf t -> xml ctx [] []) =
adamc@356 148 foldT2R [tf] [fn _ => xml ctx [] []]
adamc@356 149 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
adamc@356 150 [[nm] ~ rest] r acc =>
adamc@356 151 <xml>{f [nm] [t] [rest] r}{acc}</xml>)
adamc@360 152 <xml/>
adamc@339 153
adamc@445 154 fun foldT3RX (tf :: (Type * Type * Type) -> Type) (ctx :: {Unit})
adamc@445 155 (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
adamc@445 156 -> fn [[nm] ~ rest] =>
adamc@445 157 tf t -> xml ctx [] []) =
adamc@445 158 foldT3R [tf] [fn _ => xml ctx [] []]
adamc@445 159 (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
adamc@445 160 [[nm] ~ rest] r acc =>
adamc@445 161 <xml>{f [nm] [t] [rest] r}{acc}</xml>)
adamc@445 162 <xml/>
adamc@445 163
adamc@332 164 fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
adamc@356 165 (f : nm :: Name -> t :: Type -> rest :: {Type}
adamc@356 166 -> fn [[nm] ~ rest] =>
adamc@356 167 tf1 t -> tf2 t -> xml ctx [] []) =
adamc@356 168 foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []]
adamc@356 169 (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest]
adamc@356 170 r1 r2 acc =>
adamc@356 171 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
adamc@360 172 <xml/>
adamc@334 173
adamc@356 174 fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type)
adamc@356 175 (ctx :: {Unit})
adamc@356 176 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
adamc@356 177 -> fn [[nm] ~ rest] =>
adamc@356 178 tf1 t -> tf2 t -> xml ctx [] []) =
adamc@356 179 foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []]
adamc@356 180 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
adamc@356 181 [[nm] ~ rest] r1 r2 acc =>
adamc@356 182 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
adamc@360 183 <xml/>
adamc@339 184
adamc@445 185 fun foldT3RX2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type)
adamc@445 186 (ctx :: {Unit})
adamc@445 187 (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
adamc@445 188 -> fn [[nm] ~ rest] =>
adamc@445 189 tf1 t -> tf2 t -> xml ctx [] []) =
adamc@445 190 foldT3R2 [tf1] [tf2] [fn _ => xml ctx [] []]
adamc@445 191 (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
adamc@445 192 [[nm] ~ rest] r1 r2 acc =>
adamc@445 193 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
adamc@445 194 <xml/>
adamc@445 195
adamc@356 196 fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
adamc@356 197 (q : sql_query tables exps) [tables ~ exps]
adamc@356 198 (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
adamc@356 199 [nm = $fields] ++ acc) [] tables)
adamc@356 200 -> xml ctx [] []) =
adamc@356 201 query q
adamc@356 202 (fn fs acc => return <xml>{acc}{f fs}</xml>)
adamc@360 203 <xml/>
adamc@341 204
adamc@469 205 fun queryX' (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
adamc@469 206 (q : sql_query tables exps) [tables ~ exps]
adamc@469 207 (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
adamc@469 208 [nm = $fields] ++ acc) [] tables)
adamc@469 209 -> transaction (xml ctx [] [])) =
adamc@469 210 query q
adamc@469 211 (fn fs acc =>
adamc@469 212 r <- f fs;
adamc@469 213 return <xml>{acc}{r}</xml>)
adamc@469 214 <xml/>
adamc@469 215
adamc@356 216 fun oneOrNoRows (tables ::: {{Type}}) (exps ::: {Type})
adamc@356 217 (q : sql_query tables exps) [tables ~ exps] =
adamc@356 218 query q
adamc@356 219 (fn fs _ => return (Some fs))
adamc@356 220 None
adamc@440 221
adamc@440 222 fun oneRow (tables ::: {{Type}}) (exps ::: {Type})
adamc@440 223 (q : sql_query tables exps) [tables ~ exps] =
adamc@440 224 o <- oneOrNoRows q;
adamc@440 225 return (case o of
adamc@440 226 None => error <xml>Query returned no rows</xml>
adamc@440 227 | Some r => r)
adamc@440 228
adamc@470 229 fun eqNullable (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type})
adamc@470 230 (t ::: Type) (_ : sql_injectable (option t))
adamc@470 231 (e1 : sql_exp tables agg exps (option t))
adamc@470 232 (e2 : sql_exp tables agg exps (option t)) =
adamc@471 233 (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2})
adamc@470 234
adamc@470 235 fun eqNullable' (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type})
adamc@564 236 (t ::: Type) (_ : sql_injectable (option t))
adamc@470 237 (e1 : sql_exp tables agg exps (option t))
adamc@470 238 (e2 : option t) =
adamc@470 239 case e2 of
adamc@471 240 None => (SQL {e1} IS NULL)
adamc@564 241 | Some _ => sql_binary sql_eq e1 (sql_inject e2)