Mercurial > urweb

annotate lib/ur/top.urs @ 2129:e0843b2a636d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Make flattening of reactive HTML trees iterative instead of recursive, to avoid stack overflows
author Adam Chlipala <adam@chlipala.net>
date Sun, 08 Mar 2015 11:12:28 -0400
parents a3435112b83e
children 2d9e40e726f2
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
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