Mercurial > urweb

annotate lib/ur/top.urs @ 2171:7187068f56f5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Return to working version mode
author Adam Chlipala <adam@chlipala.net>
date Wed, 19 Aug 2015 10:53:18 -0400
parents 9029e0e2c67c
children
rev   line source
adamc@623 1 (** Row folding *)
adamc@623 2
adamc@631 3 con folder :: K --> {K} -> Type
adamc@623 4
adamc@653 5 val fold : K --> tf :: ({K} -> Type)
adamc@653 6 -> (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
adamc@653 7 tf r -> tf ([nm = v] ++ r))
adamc@653 8 -> tf []
adamc@1093 9 -> r ::: {K} -> folder r -> tf r
adamc@653 10
adamc@627 11 structure Folder : sig
adamc@627 12 val nil : K --> folder (([]) :: {K})
adamc@627 13 val cons : K --> r ::: {K} -> nm :: Name -> v :: K
adamc@629 14 -> [[nm] ~ r] => folder r -> folder ([nm = v] ++ r)
adamc@628 15 val concat : K --> r1 ::: {K} -> r2 ::: {K}
adamc@629 16 -> [r1 ~ r2] => folder r1 -> folder r2 -> folder (r1 ++ r2)
adamc@630 17 val mp : K1 --> K2 --> f ::: (K1 -> K2) -> r ::: {K1}
adamc@630 18 -> folder r -> folder (map f r)
adamc@627 19 end
adamc@627 20
adamc@623 21
adamc@422 22 val not : bool -> bool
adamc@422 23
greenrd@1480 24 (* Type-level identity function *)
adam@1649 25 con ident = K ==> fn t :: K => t
greenrd@1480 26
greenrd@1480 27 (* Type-level function which yields the value-level record
greenrd@1480 28 described by the given type-level record *)
adamc@329 29 con record = fn t :: {Type} => $t
greenrd@1480 30
adamc@637 31 con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1
adamc@637 32 con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2
adamc@637 33 con fst3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.1
adamc@637 34 con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2
adamc@637 35 con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3
adamc@329 36
greenrd@1480 37 (* Convert a record of n Units into a type-level record where
adam@2159 38 each field has the same value (which describes a uniformly
greenrd@1480 39 typed record) *)
adamc@643 40 con mapU = K ==> fn f :: K => map (fn _ :: Unit => f)
adamc@445 41
greenrd@1480 42 (* Existential type former *)
adam@1434 43 con ex :: K --> (K -> Type) -> Type
adamc@339 44
greenrd@1480 45 (* Introduction of existential type *)
adam@1434 46 val ex_intro : K --> tf :: (K -> Type) -> choice :: K -> tf choice -> ex tf
greenrd@1480 47
greenrd@1480 48 (* Eliminator for existential type *)
adam@1434 49 val ex_elim : K --> tf ::: (K -> Type) -> ex tf -> res ::: Type -> (choice :: K -> tf choice -> res) -> res
adamc@339 50
greenrd@1480 51 (* Composition of ordinary (value-level) functions *)
adamc@325 52 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type
adamc@355 53 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3)
adamc@325 54
adamc@777 55 val show_option : t ::: Type -> show t -> show (option t)
adamc@777 56 val read_option : t ::: Type -> read t -> read (option t)
adamc@777 57
adamc@720 58 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
adamc@720 59 -> xml ctx use []
adamc@329 60
greenrd@1480 61 (* Given a polymorphic type (tf) and a means of constructing
greenrd@1480 62 "default" values of tf applied to arbitrary arguments,
greenrd@1480 63 constructs records consisting of those "default" values *)
adamc@993 64 val map0 : K --> tf :: (K -> Type)
adamc@993 65 -> (t :: K -> tf t)
adamc@1093 66 -> r ::: {K} -> folder r -> $(map tf r)
greenrd@1480 67
greenrd@1480 68 (* Given two polymorphic types (tf1 and tf2) and a means of
greenrd@1480 69 converting from tf1 t to tf2 t for arbitrary t,
greenrd@1480 70 converts records of tf1's to records of tf2's *)
adamc@898 71 val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
adamc@898 72 -> (t ::: K -> tf1 t -> tf2 t)
adamc@1093 73 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r)
greenrd@1480 74
greenrd@1480 75 (* Two-argument conversion form of mp *)
adamc@937 76 val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf :: (K -> Type)
adamc@937 77 -> (t ::: K -> tf1 t -> tf2 t -> tf t)
adamc@1093 78 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r)
greenrd@1480 79
greenrd@1480 80 (* Three-argument conversion form of mp *)
adamc@937 81 val map3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tf :: (K -> Type)
adamc@937 82 -> (t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t)
adamc@1093 83 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)
adamc@898 84
greenrd@1480 85 (* Fold along a uniformly (homogenously) typed record *)
adamc@411 86 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
adamc@411 87 -> (nm :: Name -> rest :: {Unit}
adamc@629 88 -> [[nm] ~ rest] =>
adamc@411 89 tf -> tr rest -> tr ([nm] ++ rest))
adamc@1093 90 -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf r) -> tr r
adamc@411 91
greenrd@1480 92 (* Fold (generalized safe zip) along two equal-length uniformly-typed records *)
adamc@418 93 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
adamc@418 94 -> (nm :: Name -> rest :: {Unit}
adamc@629 95 -> [[nm] ~ rest] =>
adamc@418 96 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
adamc@1093 97 -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r
adamc@418 98
greenrd@1480 99 (* Fold along a heterogenously-typed record *)
adamc@623 100 val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type)
adamc@623 101 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@629 102 -> [[nm] ~ rest] =>
adamc@355 103 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@1093 104 -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r
adamc@336 105
greenrd@1480 106 (* Fold (generalized safe zip) along two heterogenously-typed records *)
adamc@623 107 val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
adamc@623 108 -> tr :: ({K} -> Type)
adamc@623 109 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@629 110 -> [[nm] ~ rest] =>
adamc@623 111 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@623 112 -> tr []
adamc@1093 113 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
adamc@623 114
greenrd@1480 115 (* Fold (generalized safe zip) along three heterogenously-typed records *)
adamc@910 116 val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
adamc@910 117 -> tr :: ({K} -> Type)
adamc@910 118 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@910 119 -> [[nm] ~ rest] =>
adamc@910 120 tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@910 121 -> tr []
adamc@1093 122 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r
adamc@910 123
greenrd@1480 124 (* Generate some XML by mapping over a uniformly-typed record *)
adamc@1172 125 val mapUX : tf :: Type -> ctx :: {Unit}
adamc@1172 126 -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] =>
adamc@1172 127 tf -> xml ctx [] [])
adamc@1172 128 -> r ::: {Unit} -> folder r -> $(mapU tf r) -> xml ctx [] []
adamc@623 129
greenrd@1480 130 (* Generate some XML by mapping over a heterogenously-typed record *)
adamc@1172 131 val mapX : K --> tf :: (K -> Type) -> ctx :: {Unit}
adamc@1172 132 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@1172 133 -> [[nm] ~ rest] =>
adamc@1172 134 tf t -> xml ctx [] [])
adamc@1172 135 -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] []
adamc@445 136
adamc@1173 137 val mapUX2 : tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
adamc@1173 138 -> (nm :: Name -> rest :: {Unit}
adamc@1173 139 -> [[nm] ~ rest] =>
adamc@1173 140 tf1 -> tf2 -> xml ctx [] [])
adamc@1173 141 -> r ::: {Unit} -> folder r
adamc@1173 142 -> $(mapU tf1 r) -> $(mapU tf2 r) -> xml ctx [] []
adamc@1173 143
adamc@1172 144 val mapX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit}
adamc@1172 145 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@1172 146 -> [[nm] ~ rest] =>
adamc@1172 147 tf1 t -> tf2 t -> xml ctx [] [])
adamc@1172 148 -> r ::: {K} -> folder r
adamc@1172 149 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
adamc@1172 150
adamc@1172 151 val mapX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit}
adamc@1172 152 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@1172 153 -> [[nm] ~ rest] =>
adamc@1172 154 tf1 t -> tf2 t -> tf3 t -> xml ctx [] [])
adamc@1172 155 -> r ::: {K} -> folder r
adamc@1172 156 -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] []
adamc@910 157
adam@2011 158 (* Note that the next two functions return elements in the _reverse_ of the natural order!
adam@2011 159 * Such a choice interacts well with the time complexity of standard list operations.
adam@2011 160 * It's easy to regain the natural order by inverting a query's 'ORDER BY' condition. *)
adam@2011 161
adamc@1081 162 val queryL : tables ::: {{Type}} -> exps ::: {Type}
adamc@1081 163 -> [tables ~ exps] =>
adam@1394 164 sql_query [] [] tables exps
adamc@1081 165 -> transaction (list $(exps ++ map (fn fields :: {Type} => $fields) tables))
adamc@1081 166
adam@1321 167 val queryL1 : t ::: Name -> fs ::: {Type}
adam@1394 168 -> sql_query [] [] [t = fs] []
adam@1321 169 -> transaction (list $fs)
adam@1321 170
adamc@1177 171 val query1 : t ::: Name -> fs ::: {Type} -> state ::: Type
adam@1394 172 -> sql_query [] [] [t = fs] []
adamc@1177 173 -> ($fs -> state -> transaction state)
adamc@1177 174 -> state
adamc@1177 175 -> transaction state
adamc@1177 176
adamc@1177 177 val query1' : t ::: Name -> fs ::: {Type} -> state ::: Type
adam@1394 178 -> sql_query [] [] [t = fs] []
adamc@1177 179 -> ($fs -> state -> state)
adamc@1177 180 -> state
adamc@1177 181 -> transaction state
adamc@1177 182
adamc@682 183 val queryI : tables ::: {{Type}} -> exps ::: {Type}
adamc@682 184 -> [tables ~ exps] =>
adam@1394 185 sql_query [] [] tables exps
adamc@682 186 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@682 187 -> transaction unit)
adamc@682 188 -> transaction unit
adamc@682 189
adam@1363 190 val queryI1 : nm ::: Name -> fs ::: {Type}
adam@1394 191 -> sql_query [] [] [nm = fs] []
adam@1363 192 -> ($fs -> transaction unit)
adam@1363 193 -> transaction unit
adam@1363 194
adamc@1004 195 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adamc@629 196 -> [tables ~ exps] =>
adam@1394 197 sql_query [] [] tables exps
adamc@632 198 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@1004 199 -> xml ctx inp [])
adamc@1004 200 -> transaction (xml ctx inp [])
adamc@341 201
adam@1405 202 val queryXI : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1405 203 -> [tables ~ exps] =>
adam@1405 204 sql_query [] [] tables exps
adam@1405 205 -> (int -> $(exps ++ map (fn fields :: {Type} => $fields) tables)
adam@1405 206 -> xml ctx inp [])
adam@1405 207 -> transaction (xml ctx inp [])
adam@1405 208
adamc@1076 209 val queryX1 : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1394 210 -> sql_query [] [] [nm = fs] []
adamc@1076 211 -> ($fs -> xml ctx inp [])
adamc@1076 212 -> transaction (xml ctx inp [])
adamc@1076 213
adam@1405 214 val queryX1I : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1405 215 -> sql_query [] [] [nm = fs] []
adam@1405 216 -> (int -> $fs -> xml ctx inp [])
adam@1405 217 -> transaction (xml ctx inp [])
adam@1405 218
adamc@1032 219 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adamc@629 220 -> [tables ~ exps] =>
adam@1394 221 sql_query [] [] tables exps
adamc@632 222 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@1032 223 -> transaction (xml ctx inp []))
adamc@1032 224 -> transaction (xml ctx inp [])
adamc@1110 225 val queryX1' : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1394 226 -> sql_query [] [] [nm = fs] []
adamc@1110 227 -> ($fs -> transaction (xml ctx inp []))
adamc@1110 228 -> transaction (xml ctx inp [])
adamc@1110 229 val queryXE' : exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1394 230 -> sql_query [] [] [] exps
adamc@1110 231 -> ($exps -> transaction (xml ctx inp []))
adamc@1110 232 -> transaction (xml ctx inp [])
adamc@1110 233
adamc@1072 234 val hasRows : tables ::: {{Type}} -> exps ::: {Type}
adamc@1072 235 -> [tables ~ exps] =>
adam@1394 236 sql_query [] [] tables exps
adamc@1072 237 -> transaction bool
adamc@1072 238
adamc@355 239 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 240 -> [tables ~ exps] =>
adam@1394 241 sql_query [] [] tables exps
adamc@629 242 -> transaction
adamc@629 243 (option
adamc@629 244 $(exps
adamc@629 245 ++ map (fn fields :: {Type} => $fields) tables))
adamc@440 246
adamc@1003 247 val oneOrNoRows1 : nm ::: Name -> fs ::: {Type}
adam@1394 248 -> sql_query [] [] [nm = fs] []
adamc@1003 249 -> transaction (option $fs)
adamc@1003 250
adamc@1076 251 val oneOrNoRowsE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
adamc@1076 252 -> [tabs ~ [nm]] =>
adam@1394 253 sql_query [] [] (mapU [] tabs) [nm = t]
adamc@1006 254 -> transaction (option t)
adamc@1006 255
adamc@440 256 val oneRow : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 257 -> [tables ~ exps] =>
adam@1394 258 sql_query [] [] tables exps
adamc@629 259 -> transaction
adamc@629 260 $(exps
adamc@629 261 ++ map (fn fields :: {Type} => $fields) tables)
adamc@1003 262
adamc@1076 263 val oneRow1 : nm ::: Name -> fs ::: {Type}
adam@1394 264 -> sql_query [] [] [nm = fs] []
adamc@1076 265 -> transaction $fs
adamc@1076 266
adamc@1064 267 val oneRowE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
adamc@1064 268 -> [tabs ~ [nm]] =>
adam@1394 269 sql_query [] [] (mapU [] tabs) [nm = t]
adamc@1003 270 -> transaction t
adamc@1003 271
adamc@1074 272 val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us
adamc@1074 273 -> transaction bool
adamc@1074 274
adamc@470 275 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adam@1778 276 -> t ::: Type -> sql_injectable (option t)
adam@1778 277 -> sql_exp tables agg exps (option t)
adam@1778 278 -> sql_exp tables agg exps (option t)
adam@1778 279 -> sql_exp tables agg exps bool
adamc@470 280
adamc@470 281 val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adam@1778 282 -> t ::: Type -> sql_injectable (option t)
adam@1778 283 -> sql_exp tables agg exps (option t)
adamc@470 284 -> option t
adam@1778 285 -> sql_exp tables agg exps bool
adam@1360 286
adam@1360 287 val mkRead' : t ::: Type -> (string -> option t) -> string -> read t
adam@1787 288
adam@1787 289 val postFields : postBody -> list (string * string)
adam@2035 290
adam@2035 291 val max : t ::: Type -> ord t -> t -> t -> t
adam@2035 292 val min : t ::: Type -> ord t -> t -> t -> t
adam@2152 293
adam@2152 294 val assert : t ::: Type
adam@2152 295 -> bool (* Did we avoid something bad? *)
adam@2152 296 -> string (* Explanation of the bad thing *)
adam@2152 297 -> string (* Source location of the bad thing *)
adam@2152 298 -> t (* Return this value if all went well. *)
adam@2152 299 -> t