Mercurial > urweb

annotate lib/ur/top.urs @ 1891:779c390382b9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Manual: add a pointer to background reading on inference rule notation
author Adam Chlipala <adam@chlipala.net>
date Sun, 17 Nov 2013 07:54:59 -0500
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)