Mercurial > urweb

annotate lib/basis.urs @ 431:24d22b843729

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Change 'sed' invocation to work in OSX
author Adam Chlipala <adamc@hcoop.net>
date Sat, 25 Oct 2008 18:58:45 -0400
parents 0ce90d4d9ae7
children 024478c34f4d
rev   line source
adamc@56 1 type int
adamc@56 2 type float
adamc@56 3 type string
adamc@91 4
adamc@119 5 type unit = {}
adamc@119 6
adamc@186 7 datatype bool = False | True
adamc@186 8
adamc@288 9 datatype option t = None | Some of t
adamc@284 10
adamc@91 11
adamc@256 12 (** Basic type classes *)
adamc@256 13
adamc@256 14 class eq
adamc@256 15 val eq : t ::: Type -> eq t -> t -> t -> bool
adamc@257 16 val ne : t ::: Type -> eq t -> t -> t -> bool
adamc@256 17 val eq_int : eq int
adamc@394 18 val eq_float : eq float
adamc@256 19 val eq_string : eq string
adamc@256 20 val eq_bool : eq bool
adamc@422 21 val mkEq : t ::: Type -> (t -> t -> bool) -> eq t
adamc@256 22
adamc@389 23 class num
adamc@417 24 val zero : t ::: Type -> num t -> t
adamc@389 25 val neg : t ::: Type -> num t -> t -> t
adamc@389 26 val plus : t ::: Type -> num t -> t -> t -> t
adamc@389 27 val minus : t ::: Type -> num t -> t -> t -> t
adamc@389 28 val times : t ::: Type -> num t -> t -> t -> t
adamc@389 29 val div : t ::: Type -> num t -> t -> t -> t
adamc@389 30 val mod : t ::: Type -> num t -> t -> t -> t
adamc@389 31 val num_int : num int
adamc@390 32 val num_float : num float
adamc@389 33
adamc@391 34 class ord
adamc@391 35 val lt : t ::: Type -> ord t -> t -> t -> bool
adamc@391 36 val le : t ::: Type -> ord t -> t -> t -> bool
adamc@391 37 val gt : t ::: Type -> ord t -> t -> t -> bool
adamc@391 38 val ge : t ::: Type -> ord t -> t -> t -> bool
adamc@391 39 val ord_int : ord int
adamc@394 40 val ord_float : ord float
adamc@394 41 val ord_string : ord string
adamc@394 42 val ord_bool : ord bool
adamc@391 43
adamc@256 44
adamc@283 45 (** String operations *)
adamc@283 46
adamc@283 47 val strcat : string -> string -> string
adamc@283 48
adamc@286 49 class show
adamc@286 50 val show : t ::: Type -> show t -> t -> string
adamc@286 51 val show_int : show int
adamc@286 52 val show_float : show float
adamc@286 53 val show_string : show string
adamc@286 54 val show_bool : show bool
adamc@286 55
adamc@290 56 class read
adamc@290 57 val read : t ::: Type -> read t -> string -> option t
adamc@292 58 val readError : t ::: Type -> read t -> string -> t
adamc@292 59 (* [readError] calls [error] if the input is malformed. *)
adamc@290 60 val read_int : read int
adamc@290 61 val read_float : read float
adamc@290 62 val read_string : read string
adamc@290 63 val read_bool : read bool
adamc@288 64
adamc@283 65
adamc@203 66 (** SQL *)
adamc@203 67
adamc@203 68 con sql_table :: {Type} -> Type
adamc@203 69
adamc@204 70 (*** Queries *)
adamc@204 71
adamc@233 72 con sql_query :: {{Type}} -> {Type} -> Type
adamc@233 73 con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type
adamc@234 74 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
adamc@204 75
adamc@223 76 con sql_subset :: {{Type}} -> {{Type}} -> Type
adamc@223 77 val sql_subset : keep_drop :: {({Type} * {Type})}
adamc@354 78 -> sql_subset
adamc@354 79 (fold (fn nm (fields :: ({Type} * {Type}))
adamc@354 80 acc [[nm] ~ acc]
adamc@354 81 [fields.1 ~ fields.2] =>
adamc@354 82 [nm = fields.1 ++ fields.2]
adamc@354 83 ++ acc) [] keep_drop)
adamc@354 84 (fold (fn nm (fields :: ({Type} * {Type}))
adamc@354 85 acc [[nm] ~ acc] =>
adamc@354 86 [nm = fields.1] ++ acc)
adamc@354 87 [] keep_drop)
adamc@354 88 val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables
adamc@223 89
adamc@229 90 val sql_query1 : tables ::: {{Type}}
adamc@354 91 -> grouped ::: {{Type}}
adamc@354 92 -> selectedFields ::: {{Type}}
adamc@354 93 -> selectedExps ::: {Type}
adamc@354 94 -> {From : $(fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
adamc@354 95 [nm = sql_table fields] ++ acc)
adamc@354 96 [] tables),
adamc@354 97 Where : sql_exp tables [] [] bool,
adamc@354 98 GroupBy : sql_subset tables grouped,
adamc@354 99 Having : sql_exp grouped tables [] bool,
adamc@354 100 SelectFields : sql_subset grouped selectedFields,
adamc@354 101 SelectExps : $(fold (fn nm (t :: Type) acc [[nm] ~ acc] =>
adamc@354 102 [nm = sql_exp grouped tables [] t]
adamc@354 103 ++ acc) [] selectedExps) }
adamc@354 104 -> sql_query1 tables selectedFields selectedExps
adamc@229 105
adamc@229 106 type sql_relop
adamc@229 107 val sql_union : sql_relop
adamc@229 108 val sql_intersect : sql_relop
adamc@229 109 val sql_except : sql_relop
adamc@260 110 val sql_relop : tables1 ::: {{Type}}
adamc@354 111 -> tables2 ::: {{Type}}
adamc@354 112 -> selectedFields ::: {{Type}}
adamc@354 113 -> selectedExps ::: {Type}
adamc@354 114 -> sql_relop
adamc@354 115 -> sql_query1 tables1 selectedFields selectedExps
adamc@354 116 -> sql_query1 tables2 selectedFields selectedExps
adamc@354 117 -> sql_query1 selectedFields selectedFields selectedExps
adamc@229 118
adamc@230 119 type sql_direction
adamc@230 120 val sql_asc : sql_direction
adamc@230 121 val sql_desc : sql_direction
adamc@230 122
adamc@234 123 con sql_order_by :: {{Type}} -> {Type} -> Type
adamc@234 124 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
adamc@234 125 val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
adamc@354 126 -> sql_exp tables [] exps t -> sql_direction
adamc@354 127 -> sql_order_by tables exps
adamc@354 128 -> sql_order_by tables exps
adamc@230 129
adamc@231 130 type sql_limit
adamc@231 131 val sql_no_limit : sql_limit
adamc@231 132 val sql_limit : int -> sql_limit
adamc@354 133
adamc@232 134 type sql_offset
adamc@232 135 val sql_no_offset : sql_offset
adamc@232 136 val sql_offset : int -> sql_offset
adamc@232 137
adamc@229 138 val sql_query : tables ::: {{Type}}
adamc@354 139 -> selectedFields ::: {{Type}}
adamc@354 140 -> selectedExps ::: {Type}
adamc@354 141 -> {Rows : sql_query1 tables selectedFields selectedExps,
adamc@354 142 OrderBy : sql_order_by tables selectedExps,
adamc@354 143 Limit : sql_limit,
adamc@354 144 Offset : sql_offset}
adamc@354 145 -> sql_query selectedFields selectedExps
adamc@204 146
adamc@354 147 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
adamc@354 148 -> fieldType ::: Type -> agg ::: {{Type}}
adamc@354 149 -> exps ::: {Type}
adamc@354 150 -> tab :: Name -> field :: Name
adamc@354 151 -> sql_exp
adamc@354 152 ([tab = [field = fieldType] ++ otherFields] ++ otherTabs)
adamc@354 153 agg exps fieldType
adamc@234 154
adamc@354 155 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type}
adamc@354 156 -> nm :: Name
adamc@354 157 -> sql_exp tabs agg ([nm = t] ++ rest) t
adamc@209 158
adamc@221 159 class sql_injectable
adamc@221 160 val sql_bool : sql_injectable bool
adamc@221 161 val sql_int : sql_injectable int
adamc@221 162 val sql_float : sql_injectable float
adamc@221 163 val sql_string : sql_injectable string
adamc@354 164 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 165 -> t ::: Type
adamc@354 166 -> sql_injectable t -> t -> sql_exp tables agg exps t
adamc@209 167
adamc@220 168 con sql_unary :: Type -> Type -> Type
adamc@220 169 val sql_not : sql_unary bool bool
adamc@354 170 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 171 -> arg ::: Type -> res ::: Type
adamc@354 172 -> sql_unary arg res -> sql_exp tables agg exps arg
adamc@354 173 -> sql_exp tables agg exps res
adamc@220 174
adamc@220 175 con sql_binary :: Type -> Type -> Type -> Type
adamc@220 176 val sql_and : sql_binary bool bool bool
adamc@220 177 val sql_or : sql_binary bool bool bool
adamc@234 178 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 179 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
adamc@354 180 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1
adamc@354 181 -> sql_exp tables agg exps arg2
adamc@354 182 -> sql_exp tables agg exps res
adamc@220 183
adamc@219 184 type sql_comparison
adamc@219 185 val sql_eq : sql_comparison
adamc@219 186 val sql_ne : sql_comparison
adamc@219 187 val sql_lt : sql_comparison
adamc@219 188 val sql_le : sql_comparison
adamc@219 189 val sql_gt : sql_comparison
adamc@219 190 val sql_ge : sql_comparison
adamc@253 191 val sql_comparison : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@236 192 -> t ::: Type
adamc@253 193 -> sql_comparison
adamc@234 194 -> sql_exp tables agg exps t -> sql_exp tables agg exps t
adamc@234 195 -> sql_exp tables agg exps bool
adamc@203 196
adamc@235 197 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 198 -> unit -> sql_exp tables agg exps int
adamc@235 199
adamc@236 200 con sql_aggregate :: Type -> Type
adamc@354 201 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@354 202 -> t ::: Type
adamc@354 203 -> sql_aggregate t -> sql_exp agg agg exps t
adamc@354 204 -> sql_exp tables agg exps t
adamc@236 205
adamc@236 206 class sql_summable
adamc@236 207 val sql_summable_int : sql_summable int
adamc@236 208 val sql_summable_float : sql_summable float
adamc@236 209 val sql_avg : t ::: Type -> sql_summable t -> sql_aggregate t
adamc@236 210 val sql_sum : t ::: Type -> sql_summable t -> sql_aggregate t
adamc@236 211
adamc@236 212 class sql_maxable
adamc@236 213 val sql_maxable_int : sql_maxable int
adamc@236 214 val sql_maxable_float : sql_maxable float
adamc@236 215 val sql_maxable_string : sql_maxable string
adamc@236 216 val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t
adamc@236 217 val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t
adamc@236 218
adamc@235 219
adamc@243 220 (*** Executing queries *)
adamc@243 221
adamc@243 222 con transaction :: Type -> Type
adamc@243 223 val return : t ::: Type
adamc@354 224 -> t -> transaction t
adamc@243 225 val bind : t1 ::: Type -> t2 ::: Type
adamc@354 226 -> transaction t1 -> (t1 -> transaction t2)
adamc@354 227 -> transaction t2
adamc@243 228
adamc@354 229 val query : tables ::: {{Type}} -> exps ::: {Type}
adamc@354 230 -> fn [tables ~ exps] =>
adamc@354 231 state ::: Type
adamc@354 232 -> sql_query tables exps
adamc@356 233 -> ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
adamc@354 234 [nm = $fields] ++ acc) [] tables)
adamc@354 235 -> state
adamc@354 236 -> transaction state)
adamc@354 237 -> state
adamc@354 238 -> transaction state
adamc@243 239
adamc@243 240
adamc@299 241 (*** Database mutators *)
adamc@299 242
adamc@299 243 type dml
adamc@299 244 val dml : dml -> transaction unit
adamc@299 245
adamc@299 246 val insert : fields ::: {Type}
adamc@354 247 -> sql_table fields
adamc@354 248 -> $(fold (fn nm (t :: Type) acc [[nm] ~ acc] =>
adamc@354 249 [nm = sql_exp [] [] [] t] ++ acc)
adamc@354 250 [] fields)
adamc@354 251 -> dml
adamc@299 252
adamc@403 253 val update : unchanged ::: {Type} -> changed :: {Type} ->
adamc@354 254 fn [changed ~ unchanged] =>
adamc@354 255 $(fold (fn nm (t :: Type) acc [[nm] ~ acc] =>
adamc@354 256 [nm = sql_exp [T = changed ++ unchanged] [] [] t]
adamc@354 257 ++ acc)
adamc@354 258 [] changed)
adamc@354 259 -> sql_table (changed ++ unchanged)
adamc@354 260 -> sql_exp [T = changed ++ unchanged] [] [] bool
adamc@354 261 -> dml
adamc@299 262
adamc@299 263 val delete : fields ::: {Type}
adamc@354 264 -> sql_table fields
adamc@354 265 -> sql_exp [T = fields] [] [] bool
adamc@354 266 -> dml
adamc@299 267
adamc@338 268 (*** Sequences *)
adamc@338 269
adamc@338 270 type sql_sequence
adamc@338 271 val nextval : sql_sequence -> transaction int
adamc@338 272
adamc@299 273
adamc@203 274 (** XML *)
adamc@203 275
adamc@139 276 con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
adamc@91 277
adamc@91 278
adamc@139 279 con xml :: {Unit} -> {Type} -> {Type} -> Type
adamc@141 280 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
adamc@354 281 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type}
adamc@354 282 -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
adamc@354 283 -> useOuter ::: {Type} -> useInner ::: {Type}
adamc@354 284 -> bindOuter ::: {Type} -> bindInner ::: {Type}
adamc@354 285 -> fn [attrsGiven ~ attrsAbsent]
adamc@354 286 [useOuter ~ useInner]
adamc@354 287 [bindOuter ~ bindInner] =>
adamc@354 288 $attrsGiven
adamc@354 289 -> tag (attrsGiven ++ attrsAbsent)
adamc@354 290 ctxOuter ctxInner useOuter bindOuter
adamc@354 291 -> xml ctxInner useInner bindInner
adamc@354 292 -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
adamc@140 293 val join : ctx ::: {Unit}
adamc@139 294 -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
adamc@354 295 -> fn [use1 ~ bind1] [bind1 ~ bind2] =>
adamc@354 296 xml ctx use1 bind1
adamc@354 297 -> xml ctx (use1 ++ bind1) bind2
adamc@354 298 -> xml ctx use1 (bind1 ++ bind2)
adamc@354 299 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type}
adamc@354 300 -> bind ::: {Type}
adamc@354 301 -> fn [use1 ~ use2] =>
adamc@354 302 xml ctx use1 bind
adamc@354 303 -> xml ctx (use1 ++ use2) bind
adamc@91 304
adamc@110 305 con xhtml = xml [Html]
adamc@139 306 con page = xhtml [] []
adamc@325 307 con xbody = xml [Body] [] []
adamc@326 308 con xtr = xml [Body, Tr] [] []
adamc@361 309 con xform = xml [Body, Form] [] []
adamc@110 310
adamc@204 311 (*** HTML details *)
adamc@204 312
adamc@140 313 con html = [Html]
adamc@140 314 con head = [Head]
adamc@140 315 con body = [Body]
adamc@361 316 con form = [Body, Form]
adamc@332 317 con tabl = [Body, Table]
adamc@332 318 con tr = [Body, Tr]
adamc@93 319
adamc@140 320 val head : unit -> tag [] html head [] []
adamc@140 321 val title : unit -> tag [] head [] [] []
adamc@110 322
adamc@140 323 val body : unit -> tag [] html body [] []
adamc@354 324 con bodyTag = fn (attrs :: {Type}) =>
adamc@354 325 ctx ::: {Unit} ->
adamc@354 326 fn [[Body] ~ ctx] =>
adamc@354 327 unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
adamc@354 328 con bodyTagStandalone = fn (attrs :: {Type}) =>
adamc@354 329 ctx ::: {Unit}
adamc@354 330 -> fn [[Body] ~ ctx] =>
adamc@354 331 unit -> tag attrs ([Body] ++ ctx) [] [] []
adamc@141 332
adamc@141 333 val br : bodyTagStandalone []
adamc@119 334
adamc@140 335 val p : bodyTag []
adamc@140 336 val b : bodyTag []
adamc@140 337 val i : bodyTag []
adamc@407 338 val tt : bodyTag []
adamc@140 339 val font : bodyTag [Size = int, Face = string]
adamc@140 340
adamc@140 341 val h1 : bodyTag []
adamc@140 342 val li : bodyTag []
adamc@140 343
adamc@410 344 val hr : bodyTag []
adamc@410 345
adamc@280 346 val a : bodyTag [Link = transaction page]
adamc@140 347
adamc@361 348 val form : ctx ::: {Unit} -> bind ::: {Type}
adamc@354 349 -> fn [[Body] ~ ctx] =>
adamc@354 350 xml form [] bind
adamc@354 351 -> xml ([Body] ++ ctx) [] []
adamc@361 352 con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) =>
adamc@354 353 ctx ::: {Unit}
adamc@361 354 -> fn [[Form] ~ ctx] =>
adamc@354 355 nm :: Name -> unit
adamc@361 356 -> tag attrs ([Form] ++ ctx) inner [] [nm = ty]
adamc@361 357 val textbox : formTag string [] [Value = string]
adamc@361 358 val password : formTag string [] []
adamc@361 359 val textarea : formTag string [] []
adamc@153 360
adamc@361 361 val checkbox : formTag bool [] [Checked = bool]
adamc@190 362
adamc@153 363 con radio = [Body, Radio]
adamc@361 364 val radio : formTag string radio []
adamc@153 365 val radioOption : unit -> tag [Value = string] radio [] [] []
adamc@142 366
adamc@154 367 con select = [Select]
adamc@361 368 val select : formTag string select []
adamc@422 369 val option : unit -> tag [Value = string, Selected = bool] select [] [] []
adamc@154 370
adamc@354 371 val submit : ctx ::: {Unit} -> use ::: {Type}
adamc@361 372 -> fn [[Form] ~ ctx] =>
adamc@354 373 unit
adamc@406 374 -> tag [Value = string, Action = $use -> transaction page]
adamc@361 375 ([Form] ++ ctx) ([Form] ++ ctx) use []
adamc@283 376
adamc@325 377 (*** Tables *)
adamc@325 378
adamc@406 379 val tabl : other ::: {Unit} -> fn [other ~ [Body, Table]] =>
adamc@406 380 unit -> tag [Border = int] ([Body] ++ other) ([Body, Table] ++ other) [] []
adamc@406 381 val tr : other ::: {Unit} -> fn [other ~ [Body, Table, Tr]] =>
adamc@406 382 unit -> tag [] ([Body, Table] ++ other) ([Body, Tr] ++ other) [] []
adamc@406 383 val th : other ::: {Unit} -> fn [other ~ [Body, Tr]] =>
adamc@406 384 unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] []
adamc@406 385 val td : other ::: {Unit} -> fn [other ~ [Body, Tr]] =>
adamc@406 386 unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] []
adamc@325 387
adamc@283 388
adamc@283 389 (** Aborting *)
adamc@283 390
adamc@283 391 val error : t ::: Type -> xml [Body] [] [] -> t