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