Mercurial > urweb

comparison lib/ur/basis.urs @ 602:1d34d916c206

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