Mercurial > urweb

annotate lib/basis.urs @ 417:e0e9e9eca1cb

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