Mercurial > urweb

annotate lib/ur/top.urs @ 1882:77cde56d41b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Change Pthread thread creation logic to avoid Cygwin limitations with setting stack size
author Adam Chlipala <adam@chlipala.net>
date Mon, 14 Oct 2013 08:08:57 -0400
parents 69daa6d70299
children cfd604842006
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
greenrd@1480 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
adamc@1081 158 val queryL : tables ::: {{Type}} -> exps ::: {Type}
adamc@1081 159 -> [tables ~ exps] =>
adam@1394 160 sql_query [] [] tables exps
adamc@1081 161 -> transaction (list $(exps ++ map (fn fields :: {Type} => $fields) tables))
adamc@1081 162
adam@1321 163 val queryL1 : t ::: Name -> fs ::: {Type}
adam@1394 164 -> sql_query [] [] [t = fs] []
adam@1321 165 -> transaction (list $fs)
adam@1321 166
adamc@1177 167 val query1 : t ::: Name -> fs ::: {Type} -> state ::: Type
adam@1394 168 -> sql_query [] [] [t = fs] []
adamc@1177 169 -> ($fs -> state -> transaction state)
adamc@1177 170 -> state
adamc@1177 171 -> transaction state
adamc@1177 172
adamc@1177 173 val query1' : t ::: Name -> fs ::: {Type} -> state ::: Type
adam@1394 174 -> sql_query [] [] [t = fs] []
adamc@1177 175 -> ($fs -> state -> state)
adamc@1177 176 -> state
adamc@1177 177 -> transaction state
adamc@1177 178
adamc@682 179 val queryI : tables ::: {{Type}} -> exps ::: {Type}
adamc@682 180 -> [tables ~ exps] =>
adam@1394 181 sql_query [] [] tables exps
adamc@682 182 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@682 183 -> transaction unit)
adamc@682 184 -> transaction unit
adamc@682 185
adam@1363 186 val queryI1 : nm ::: Name -> fs ::: {Type}
adam@1394 187 -> sql_query [] [] [nm = fs] []
adam@1363 188 -> ($fs -> transaction unit)
adam@1363 189 -> transaction unit
adam@1363 190
adamc@1004 191 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adamc@629 192 -> [tables ~ exps] =>
adam@1394 193 sql_query [] [] tables exps
adamc@632 194 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@1004 195 -> xml ctx inp [])
adamc@1004 196 -> transaction (xml ctx inp [])
adamc@341 197
adam@1405 198 val queryXI : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1405 199 -> [tables ~ exps] =>
adam@1405 200 sql_query [] [] tables exps
adam@1405 201 -> (int -> $(exps ++ map (fn fields :: {Type} => $fields) tables)
adam@1405 202 -> xml ctx inp [])
adam@1405 203 -> transaction (xml ctx inp [])
adam@1405 204
adamc@1076 205 val queryX1 : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1394 206 -> sql_query [] [] [nm = fs] []
adamc@1076 207 -> ($fs -> xml ctx inp [])
adamc@1076 208 -> transaction (xml ctx inp [])
adamc@1076 209
adam@1405 210 val queryX1I : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1405 211 -> sql_query [] [] [nm = fs] []
adam@1405 212 -> (int -> $fs -> xml ctx inp [])
adam@1405 213 -> transaction (xml ctx inp [])
adam@1405 214
adamc@1032 215 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adamc@629 216 -> [tables ~ exps] =>
adam@1394 217 sql_query [] [] tables exps
adamc@632 218 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@1032 219 -> transaction (xml ctx inp []))
adamc@1032 220 -> transaction (xml ctx inp [])
adamc@1110 221 val queryX1' : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1394 222 -> sql_query [] [] [nm = fs] []
adamc@1110 223 -> ($fs -> transaction (xml ctx inp []))
adamc@1110 224 -> transaction (xml ctx inp [])
adamc@1110 225 val queryXE' : exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1394 226 -> sql_query [] [] [] exps
adamc@1110 227 -> ($exps -> transaction (xml ctx inp []))
adamc@1110 228 -> transaction (xml ctx inp [])
adamc@1110 229
adamc@1072 230 val hasRows : tables ::: {{Type}} -> exps ::: {Type}
adamc@1072 231 -> [tables ~ exps] =>
adam@1394 232 sql_query [] [] tables exps
adamc@1072 233 -> transaction bool
adamc@1072 234
adamc@355 235 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 236 -> [tables ~ exps] =>
adam@1394 237 sql_query [] [] tables exps
adamc@629 238 -> transaction
adamc@629 239 (option
adamc@629 240 $(exps
adamc@629 241 ++ map (fn fields :: {Type} => $fields) tables))
adamc@440 242
adamc@1003 243 val oneOrNoRows1 : nm ::: Name -> fs ::: {Type}
adam@1394 244 -> sql_query [] [] [nm = fs] []
adamc@1003 245 -> transaction (option $fs)
adamc@1003 246
adamc@1076 247 val oneOrNoRowsE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
adamc@1076 248 -> [tabs ~ [nm]] =>
adam@1394 249 sql_query [] [] (mapU [] tabs) [nm = t]
adamc@1006 250 -> transaction (option t)
adamc@1006 251
adamc@440 252 val oneRow : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 253 -> [tables ~ exps] =>
adam@1394 254 sql_query [] [] tables exps
adamc@629 255 -> transaction
adamc@629 256 $(exps
adamc@629 257 ++ map (fn fields :: {Type} => $fields) tables)
adamc@1003 258
adamc@1076 259 val oneRow1 : nm ::: Name -> fs ::: {Type}
adam@1394 260 -> sql_query [] [] [nm = fs] []
adamc@1076 261 -> transaction $fs
adamc@1076 262
adamc@1064 263 val oneRowE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
adamc@1064 264 -> [tabs ~ [nm]] =>
adam@1394 265 sql_query [] [] (mapU [] tabs) [nm = t]
adamc@1003 266 -> transaction t
adamc@1003 267
adamc@1074 268 val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us
adamc@1074 269 -> transaction bool
adamc@1074 270
adamc@470 271 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adam@1778 272 -> t ::: Type -> sql_injectable (option t)
adam@1778 273 -> sql_exp tables agg exps (option t)
adam@1778 274 -> sql_exp tables agg exps (option t)
adam@1778 275 -> sql_exp tables agg exps bool
adamc@470 276
adamc@470 277 val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adam@1778 278 -> t ::: Type -> sql_injectable (option t)
adam@1778 279 -> sql_exp tables agg exps (option t)
adamc@470 280 -> option t
adam@1778 281 -> sql_exp tables agg exps bool
adam@1360 282
adam@1360 283 val mkRead' : t ::: Type -> (string -> option t) -> string -> read t
adam@1787 284
adam@1787 285 val postFields : postBody -> list (string * string)