Mercurial > urweb

annotate lib/ur/top.urs @ 1466:e2d7bd41f527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remember to remove explicit table projections in SQLite UPDATE SET values
author Adam Chlipala <adam@chlipala.net>
date Mon, 30 May 2011 07:48:08 -0400
parents 44f78d6fec29
children aa0c6382aa57
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
adamc@898 24 con id = K ==> fn t :: K => t
adamc@329 25 con record = fn t :: {Type} => $t
adamc@637 26 con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1
adamc@637 27 con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2
adamc@637 28 con fst3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.1
adamc@637 29 con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2
adamc@637 30 con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3
adamc@329 31
adamc@643 32 con mapU = K ==> fn f :: K => map (fn _ :: Unit => f)
adamc@445 33
adam@1434 34 con ex :: K --> (K -> Type) -> Type
adamc@339 35
adam@1434 36 val ex_intro : K --> tf :: (K -> Type) -> choice :: K -> tf choice -> ex tf
adam@1434 37 val ex_elim : K --> tf ::: (K -> Type) -> ex tf -> res ::: Type -> (choice :: K -> tf choice -> res) -> res
adamc@339 38
adamc@325 39 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type
adamc@355 40 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3)
adamc@325 41
adamc@777 42 val show_option : t ::: Type -> show t -> show (option t)
adamc@777 43 val read_option : t ::: Type -> read t -> read (option t)
adamc@777 44
adamc@720 45 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
adamc@720 46 -> xml ctx use []
adamc@329 47
adamc@993 48 val map0 : K --> tf :: (K -> Type)
adamc@993 49 -> (t :: K -> tf t)
adamc@1093 50 -> r ::: {K} -> folder r -> $(map tf r)
adamc@898 51 val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
adamc@898 52 -> (t ::: K -> tf1 t -> tf2 t)
adamc@1093 53 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r)
adamc@937 54 val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf :: (K -> Type)
adamc@937 55 -> (t ::: K -> tf1 t -> tf2 t -> tf t)
adamc@1093 56 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r)
adamc@937 57 val map3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tf :: (K -> Type)
adamc@937 58 -> (t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t)
adamc@1093 59 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)
adamc@898 60
adamc@411 61 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
adamc@411 62 -> (nm :: Name -> rest :: {Unit}
adamc@629 63 -> [[nm] ~ rest] =>
adamc@411 64 tf -> tr rest -> tr ([nm] ++ rest))
adamc@1093 65 -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf r) -> tr r
adamc@411 66
adamc@418 67 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
adamc@418 68 -> (nm :: Name -> rest :: {Unit}
adamc@629 69 -> [[nm] ~ rest] =>
adamc@418 70 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
adamc@1093 71 -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r
adamc@418 72
adamc@623 73 val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type)
adamc@623 74 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@629 75 -> [[nm] ~ rest] =>
adamc@355 76 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@1093 77 -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r
adamc@336 78
adamc@623 79 val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
adamc@623 80 -> tr :: ({K} -> Type)
adamc@623 81 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@629 82 -> [[nm] ~ rest] =>
adamc@623 83 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@623 84 -> tr []
adamc@1093 85 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
adamc@623 86
adamc@910 87 val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
adamc@910 88 -> tr :: ({K} -> Type)
adamc@910 89 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@910 90 -> [[nm] ~ rest] =>
adamc@910 91 tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@910 92 -> tr []
adamc@1093 93 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r
adamc@910 94
adamc@1172 95 val mapUX : tf :: Type -> ctx :: {Unit}
adamc@1172 96 -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] =>
adamc@1172 97 tf -> xml ctx [] [])
adamc@1172 98 -> r ::: {Unit} -> folder r -> $(mapU tf r) -> xml ctx [] []
adamc@623 99
adamc@1172 100 val mapX : K --> tf :: (K -> Type) -> ctx :: {Unit}
adamc@1172 101 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@1172 102 -> [[nm] ~ rest] =>
adamc@1172 103 tf t -> xml ctx [] [])
adamc@1172 104 -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] []
adamc@445 105
adamc@1173 106 val mapUX2 : tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
adamc@1173 107 -> (nm :: Name -> rest :: {Unit}
adamc@1173 108 -> [[nm] ~ rest] =>
adamc@1173 109 tf1 -> tf2 -> xml ctx [] [])
adamc@1173 110 -> r ::: {Unit} -> folder r
adamc@1173 111 -> $(mapU tf1 r) -> $(mapU tf2 r) -> xml ctx [] []
adamc@1173 112
adamc@1172 113 val mapX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit}
adamc@1172 114 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@1172 115 -> [[nm] ~ rest] =>
adamc@1172 116 tf1 t -> tf2 t -> xml ctx [] [])
adamc@1172 117 -> r ::: {K} -> folder r
adamc@1172 118 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
adamc@1172 119
adamc@1172 120 val mapX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit}
adamc@1172 121 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@1172 122 -> [[nm] ~ rest] =>
adamc@1172 123 tf1 t -> tf2 t -> tf3 t -> xml ctx [] [])
adamc@1172 124 -> r ::: {K} -> folder r
adamc@1172 125 -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] []
adamc@910 126
adamc@1081 127 val queryL : tables ::: {{Type}} -> exps ::: {Type}
adamc@1081 128 -> [tables ~ exps] =>
adam@1394 129 sql_query [] [] tables exps
adamc@1081 130 -> transaction (list $(exps ++ map (fn fields :: {Type} => $fields) tables))
adamc@1081 131
adam@1321 132 val queryL1 : t ::: Name -> fs ::: {Type}
adam@1394 133 -> sql_query [] [] [t = fs] []
adam@1321 134 -> transaction (list $fs)
adam@1321 135
adamc@1177 136 val query1 : t ::: Name -> fs ::: {Type} -> state ::: Type
adam@1394 137 -> sql_query [] [] [t = fs] []
adamc@1177 138 -> ($fs -> state -> transaction state)
adamc@1177 139 -> state
adamc@1177 140 -> transaction state
adamc@1177 141
adamc@1177 142 val query1' : t ::: Name -> fs ::: {Type} -> state ::: Type
adam@1394 143 -> sql_query [] [] [t = fs] []
adamc@1177 144 -> ($fs -> state -> state)
adamc@1177 145 -> state
adamc@1177 146 -> transaction state
adamc@1177 147
adamc@682 148 val queryI : tables ::: {{Type}} -> exps ::: {Type}
adamc@682 149 -> [tables ~ exps] =>
adam@1394 150 sql_query [] [] tables exps
adamc@682 151 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@682 152 -> transaction unit)
adamc@682 153 -> transaction unit
adamc@682 154
adam@1363 155 val queryI1 : nm ::: Name -> fs ::: {Type}
adam@1394 156 -> sql_query [] [] [nm = fs] []
adam@1363 157 -> ($fs -> transaction unit)
adam@1363 158 -> transaction unit
adam@1363 159
adamc@1004 160 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adamc@629 161 -> [tables ~ exps] =>
adam@1394 162 sql_query [] [] tables exps
adamc@632 163 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@1004 164 -> xml ctx inp [])
adamc@1004 165 -> transaction (xml ctx inp [])
adamc@341 166
adam@1405 167 val queryXI : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1405 168 -> [tables ~ exps] =>
adam@1405 169 sql_query [] [] tables exps
adam@1405 170 -> (int -> $(exps ++ map (fn fields :: {Type} => $fields) tables)
adam@1405 171 -> xml ctx inp [])
adam@1405 172 -> transaction (xml ctx inp [])
adam@1405 173
adamc@1076 174 val queryX1 : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1394 175 -> sql_query [] [] [nm = fs] []
adamc@1076 176 -> ($fs -> xml ctx inp [])
adamc@1076 177 -> transaction (xml ctx inp [])
adamc@1076 178
adam@1405 179 val queryX1I : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1405 180 -> sql_query [] [] [nm = fs] []
adam@1405 181 -> (int -> $fs -> xml ctx inp [])
adam@1405 182 -> transaction (xml ctx inp [])
adam@1405 183
adamc@1032 184 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adamc@629 185 -> [tables ~ exps] =>
adam@1394 186 sql_query [] [] tables exps
adamc@632 187 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@1032 188 -> transaction (xml ctx inp []))
adamc@1032 189 -> transaction (xml ctx inp [])
adamc@1110 190 val queryX1' : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1394 191 -> sql_query [] [] [nm = fs] []
adamc@1110 192 -> ($fs -> transaction (xml ctx inp []))
adamc@1110 193 -> transaction (xml ctx inp [])
adamc@1110 194 val queryXE' : exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type}
adam@1394 195 -> sql_query [] [] [] exps
adamc@1110 196 -> ($exps -> transaction (xml ctx inp []))
adamc@1110 197 -> transaction (xml ctx inp [])
adamc@1110 198
adamc@1072 199 val hasRows : tables ::: {{Type}} -> exps ::: {Type}
adamc@1072 200 -> [tables ~ exps] =>
adam@1394 201 sql_query [] [] tables exps
adamc@1072 202 -> transaction bool
adamc@1072 203
adamc@355 204 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 205 -> [tables ~ exps] =>
adam@1394 206 sql_query [] [] tables exps
adamc@629 207 -> transaction
adamc@629 208 (option
adamc@629 209 $(exps
adamc@629 210 ++ map (fn fields :: {Type} => $fields) tables))
adamc@440 211
adamc@1003 212 val oneOrNoRows1 : nm ::: Name -> fs ::: {Type}
adam@1394 213 -> sql_query [] [] [nm = fs] []
adamc@1003 214 -> transaction (option $fs)
adamc@1003 215
adamc@1076 216 val oneOrNoRowsE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
adamc@1076 217 -> [tabs ~ [nm]] =>
adam@1394 218 sql_query [] [] (mapU [] tabs) [nm = t]
adamc@1006 219 -> transaction (option t)
adamc@1006 220
adamc@440 221 val oneRow : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 222 -> [tables ~ exps] =>
adam@1394 223 sql_query [] [] tables exps
adamc@629 224 -> transaction
adamc@629 225 $(exps
adamc@629 226 ++ map (fn fields :: {Type} => $fields) tables)
adamc@1003 227
adamc@1076 228 val oneRow1 : nm ::: Name -> fs ::: {Type}
adam@1394 229 -> sql_query [] [] [nm = fs] []
adamc@1076 230 -> transaction $fs
adamc@1076 231
adamc@1064 232 val oneRowE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
adamc@1064 233 -> [tabs ~ [nm]] =>
adam@1394 234 sql_query [] [] (mapU [] tabs) [nm = t]
adamc@1003 235 -> transaction t
adamc@1003 236
adamc@1074 237 val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us
adamc@1074 238 -> transaction bool
adamc@1074 239
adamc@470 240 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 241 -> t ::: Type -> sql_injectable (option t)
adamc@470 242 -> sql_exp tables agg exps (option t)
adamc@470 243 -> sql_exp tables agg exps (option t)
adamc@470 244 -> sql_exp tables agg exps bool
adamc@470 245
adamc@470 246 val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 247 -> t ::: Type -> sql_injectable (option t)
adamc@470 248 -> sql_exp tables agg exps (option t)
adamc@470 249 -> option t
adamc@470 250 -> sql_exp tables agg exps bool
adam@1360 251
adam@1360 252 val mkRead' : t ::: Type -> (string -> option t) -> string -> read t