Mercurial > urweb

annotate lib/basis.urs @ 411:06fcddcd20d3

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