adamc@56
|
1 type int
|
adamc@56
|
2 type float
|
adamc@56
|
3 type string
|
adamc@821
|
4 type char
|
adamc@436
|
5 type time
|
adamc@737
|
6 type blob
|
adamc@91
|
7
|
adamc@119
|
8 type unit = {}
|
adamc@119
|
9
|
adamc@186
|
10 datatype bool = False | True
|
adamc@186
|
11
|
adamc@288
|
12 datatype option t = None | Some of t
|
adamc@284
|
13
|
adamc@757
|
14 datatype list t = Nil | Cons of t * list t
|
adamc@757
|
15
|
adamc@91
|
16
|
adam@1287
|
17 (** Polymorphic variants *)
|
adam@1287
|
18
|
adam@1287
|
19 con variant :: {Type} -> Type
|
adam@1287
|
20 val make : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => t -> variant ([nm = t] ++ ts)
|
adam@1287
|
21 val match : ts ::: {Type} -> t ::: Type -> variant ts -> $(map (fn t' => t' -> t) ts) -> t
|
adam@1287
|
22
|
adam@1287
|
23
|
adamc@256
|
24 (** Basic type classes *)
|
adamc@256
|
25
|
adamc@256
|
26 class eq
|
adamc@256
|
27 val eq : t ::: Type -> eq t -> t -> t -> bool
|
adamc@257
|
28 val ne : t ::: Type -> eq t -> t -> t -> bool
|
adamc@256
|
29 val eq_int : eq int
|
adamc@394
|
30 val eq_float : eq float
|
adamc@256
|
31 val eq_string : eq string
|
adamc@821
|
32 val eq_char : eq char
|
adamc@256
|
33 val eq_bool : eq bool
|
adamc@437
|
34 val eq_time : eq time
|
adamc@422
|
35 val mkEq : t ::: Type -> (t -> t -> bool) -> eq t
|
adamc@256
|
36
|
adamc@389
|
37 class num
|
adamc@417
|
38 val zero : t ::: Type -> num t -> t
|
adamc@389
|
39 val neg : t ::: Type -> num t -> t -> t
|
adamc@389
|
40 val plus : t ::: Type -> num t -> t -> t -> t
|
adamc@389
|
41 val minus : t ::: Type -> num t -> t -> t -> t
|
adamc@389
|
42 val times : t ::: Type -> num t -> t -> t -> t
|
adamc@775
|
43 val divide : t ::: Type -> num t -> t -> t -> t
|
adamc@389
|
44 val mod : t ::: Type -> num t -> t -> t -> t
|
adamc@389
|
45 val num_int : num int
|
adamc@390
|
46 val num_float : num float
|
adamc@389
|
47
|
adamc@391
|
48 class ord
|
adamc@391
|
49 val lt : t ::: Type -> ord t -> t -> t -> bool
|
adamc@391
|
50 val le : t ::: Type -> ord t -> t -> t -> bool
|
adamc@391
|
51 val gt : t ::: Type -> ord t -> t -> t -> bool
|
adamc@391
|
52 val ge : t ::: Type -> ord t -> t -> t -> bool
|
adamc@391
|
53 val ord_int : ord int
|
adamc@394
|
54 val ord_float : ord float
|
adamc@394
|
55 val ord_string : ord string
|
adamc@821
|
56 val ord_char : ord char
|
adamc@394
|
57 val ord_bool : ord bool
|
adamc@437
|
58 val ord_time : ord time
|
adamc@961
|
59 val mkOrd : t ::: Type -> {Lt : t -> t -> bool, Le : t -> t -> bool} -> ord t
|
adamc@391
|
60
|
adamc@256
|
61
|
adamc@1061
|
62 (** Character operations *)
|
adamc@1061
|
63
|
adamc@1061
|
64 val isalnum : char -> bool
|
adamc@1061
|
65 val isalpha : char -> bool
|
adamc@1061
|
66 val isblank : char -> bool
|
adamc@1061
|
67 val iscntrl : char -> bool
|
adamc@1061
|
68 val isdigit : char -> bool
|
adamc@1061
|
69 val isgraph : char -> bool
|
adamc@1061
|
70 val islower : char -> bool
|
adamc@1061
|
71 val isprint : char -> bool
|
adamc@1061
|
72 val ispunct : char -> bool
|
adamc@1061
|
73 val isspace : char -> bool
|
adamc@1061
|
74 val isupper : char -> bool
|
adamc@1061
|
75 val isxdigit : char -> bool
|
adamc@1061
|
76 val tolower : char -> char
|
adamc@1061
|
77 val toupper : char -> char
|
adamc@1128
|
78 val ord : char -> int
|
adamc@1128
|
79 val chr : int -> char
|
adamc@1061
|
80
|
adamc@283
|
81 (** String operations *)
|
adamc@283
|
82
|
adamc@828
|
83 val strlen : string -> int
|
adam@1388
|
84 val strlenGe : string -> int -> bool
|
adamc@283
|
85 val strcat : string -> string -> string
|
adamc@821
|
86 val strsub : string -> int -> char
|
adamc@821
|
87 val strsuffix : string -> int -> string
|
adamc@829
|
88 val strchr : string -> char -> option string
|
adamc@829
|
89 val strindex : string -> char -> option int
|
adam@1390
|
90 val strsindex : string -> string -> option int
|
adamc@1272
|
91 val strcspn : string -> string -> int
|
adamc@829
|
92 val substring : string -> int -> int -> string
|
adamc@1023
|
93 val str1 : char -> string
|
adamc@283
|
94
|
adamc@286
|
95 class show
|
adamc@286
|
96 val show : t ::: Type -> show t -> t -> string
|
adamc@286
|
97 val show_int : show int
|
adamc@286
|
98 val show_float : show float
|
adamc@286
|
99 val show_string : show string
|
adamc@821
|
100 val show_char : show char
|
adamc@286
|
101 val show_bool : show bool
|
adamc@436
|
102 val show_time : show time
|
adamc@452
|
103 val mkShow : t ::: Type -> (t -> string) -> show t
|
adamc@286
|
104
|
adamc@290
|
105 class read
|
adamc@290
|
106 val read : t ::: Type -> read t -> string -> option t
|
adamc@292
|
107 val readError : t ::: Type -> read t -> string -> t
|
adamc@292
|
108 (* [readError] calls [error] if the input is malformed. *)
|
adamc@290
|
109 val read_int : read int
|
adamc@290
|
110 val read_float : read float
|
adamc@290
|
111 val read_string : read string
|
adamc@821
|
112 val read_char : read char
|
adamc@290
|
113 val read_bool : read bool
|
adamc@436
|
114 val read_time : read time
|
adamc@777
|
115 val mkRead : t ::: Type -> (string -> t) -> (string -> option t) -> read t
|
adamc@288
|
116
|
adamc@283
|
117
|
adamc@564
|
118 (** * Monads *)
|
adamc@564
|
119
|
adamc@711
|
120 class monad :: (Type -> Type) -> Type
|
adamc@564
|
121 val return : m ::: (Type -> Type) -> t ::: Type
|
adamc@564
|
122 -> monad m
|
adamc@564
|
123 -> t -> m t
|
adamc@564
|
124 val bind : m ::: (Type -> Type) -> t1 ::: Type -> t2 ::: Type
|
adamc@564
|
125 -> monad m
|
adamc@564
|
126 -> m t1 -> (t1 -> m t2)
|
adamc@564
|
127 -> m t2
|
adamc@564
|
128
|
adam@1544
|
129 val mkMonad : m ::: (Type -> Type)
|
adam@1544
|
130 -> {Return : t ::: Type -> t -> m t,
|
adam@1544
|
131 Bind : t1 ::: Type -> t2 ::: Type -> m t1 -> (t1 -> m t2) -> m t2}
|
adam@1544
|
132 -> monad m
|
adam@1544
|
133
|
adamc@456
|
134 con transaction :: Type -> Type
|
adamc@564
|
135 val transaction_monad : monad transaction
|
adamc@456
|
136
|
adamc@565
|
137 con source :: Type -> Type
|
adamc@565
|
138 val source : t ::: Type -> t -> transaction (source t)
|
adamc@575
|
139 val set : t ::: Type -> source t -> t -> transaction unit
|
adamc@601
|
140 val get : t ::: Type -> source t -> transaction t
|
adamc@565
|
141
|
adamc@565
|
142 con signal :: Type -> Type
|
adamc@565
|
143 val signal_monad : monad signal
|
adamc@565
|
144 val signal : t ::: Type -> source t -> signal t
|
adamc@841
|
145 val current : t ::: Type -> signal t -> transaction t
|
adamc@456
|
146
|
adamc@456
|
147
|
adam@1571
|
148 (** * Floats *)
|
adam@1571
|
149
|
adam@1571
|
150 val float : int -> float
|
adam@1571
|
151 val ceil : float -> int
|
adam@1571
|
152 val trunc : float -> int
|
adam@1571
|
153 val round : float -> int
|
adam@1571
|
154
|
adam@1571
|
155
|
adamc@1006
|
156 (** * Time *)
|
adamc@1006
|
157
|
adamc@1006
|
158 val now : transaction time
|
adamc@1050
|
159 val minTime : time
|
adam@1369
|
160 val addSeconds : time -> int -> time
|
adam@1514
|
161 val toSeconds : time -> int
|
adam@1514
|
162 val diffInSeconds : time -> time -> int
|
adam@1514
|
163 (* Earlier time first *)
|
adam@1359
|
164 val timef : string -> time -> string (* Uses strftime() format string *)
|
adam@1372
|
165 val readUtc : string -> option time
|
adamc@1006
|
166
|
adamc@1006
|
167
|
adam@1360
|
168 (** * Encryption *)
|
adam@1360
|
169
|
adam@1360
|
170 val crypt : string -> string -> string
|
adam@1360
|
171
|
adam@1360
|
172
|
adamc@456
|
173 (** HTTP operations *)
|
adamc@456
|
174
|
adamc@459
|
175 con http_cookie :: Type -> Type
|
adamc@459
|
176 val getCookie : t ::: Type -> http_cookie t -> transaction (option t)
|
adamc@1050
|
177 val setCookie : t ::: Type -> http_cookie t -> {Value : t,
|
adamc@1050
|
178 Expires : option time,
|
adamc@1050
|
179 Secure : bool} -> transaction unit
|
adamc@1050
|
180 val clearCookie : t ::: Type -> http_cookie t -> transaction unit
|
adamc@459
|
181
|
adam@1465
|
182 type requestHeader
|
adam@1465
|
183 val blessRequestHeader : string -> requestHeader
|
adam@1465
|
184 val checkRequestHeader : string -> option requestHeader
|
adam@1465
|
185 val getHeader : requestHeader -> transaction (option string)
|
adam@1465
|
186
|
adam@1465
|
187 type responseHeader
|
adam@1465
|
188 val blessResponseHeader : string -> responseHeader
|
adam@1465
|
189 val checkResponseHeader : string -> option responseHeader
|
adam@1465
|
190 val setHeader : responseHeader -> string -> transaction unit
|
adam@1465
|
191
|
adamc@456
|
192
|
adamc@566
|
193 (** JavaScript-y gadgets *)
|
adamc@566
|
194
|
adamc@566
|
195 val alert : string -> transaction unit
|
adam@1290
|
196 val confirm : string -> transaction bool
|
adamc@694
|
197 val spawn : transaction unit -> transaction unit
|
adamc@695
|
198 val sleep : int -> transaction unit
|
adamc@566
|
199
|
adamc@908
|
200 val rpc : t ::: Type -> transaction t -> transaction t
|
adamc@908
|
201
|
adamc@566
|
202
|
adamc@678
|
203 (** Channels *)
|
adamc@678
|
204
|
adamc@678
|
205 con channel :: Type -> Type
|
adamc@678
|
206 val channel : t ::: Type -> transaction (channel t)
|
adamc@678
|
207 val send : t ::: Type -> channel t -> t -> transaction unit
|
adamc@678
|
208 val recv : t ::: Type -> channel t -> transaction t
|
adamc@678
|
209
|
adamc@682
|
210 type client
|
adamc@682
|
211 val self : transaction client
|
adamc@682
|
212
|
adamc@678
|
213
|
adamc@203
|
214 (** SQL *)
|
adamc@203
|
215
|
adamc@705
|
216 con sql_table :: {Type} -> {{Unit}} -> Type
|
adamc@753
|
217 con sql_view :: {Type} -> Type
|
adamc@753
|
218
|
adamc@753
|
219 class fieldsOf :: Type -> {Type} -> Type
|
adamc@753
|
220 val fieldsOf_table : fs ::: {Type} -> keys ::: {{Unit}}
|
adamc@753
|
221 -> fieldsOf (sql_table fs keys) fs
|
adamc@753
|
222 val fieldsOf_view : fs ::: {Type}
|
adamc@753
|
223 -> fieldsOf (sql_view fs) fs
|
adamc@203
|
224
|
adamc@704
|
225 (*** Constraints *)
|
adamc@704
|
226
|
adamc@707
|
227 (**** Primary keys *)
|
adamc@707
|
228
|
adamc@707
|
229 class sql_injectable_prim
|
adamc@707
|
230 val sql_bool : sql_injectable_prim bool
|
adamc@707
|
231 val sql_int : sql_injectable_prim int
|
adamc@707
|
232 val sql_float : sql_injectable_prim float
|
adamc@707
|
233 val sql_string : sql_injectable_prim string
|
adamc@1011
|
234 val sql_char : sql_injectable_prim char
|
adamc@707
|
235 val sql_time : sql_injectable_prim time
|
adamc@737
|
236 val sql_blob : sql_injectable_prim blob
|
adamc@707
|
237 val sql_channel : t ::: Type -> sql_injectable_prim (channel t)
|
adamc@707
|
238 val sql_client : sql_injectable_prim client
|
adamc@707
|
239
|
adamc@1104
|
240 con serialized :: Type -> Type
|
adamc@1104
|
241 val serialize : t ::: Type -> t -> serialized t
|
adamc@1104
|
242 val deserialize : t ::: Type -> serialized t -> t
|
adamc@1104
|
243 val sql_serialized : t ::: Type -> sql_injectable_prim (serialized t)
|
adamc@1104
|
244
|
adamc@707
|
245 con primary_key :: {Type} -> {{Unit}} -> Type
|
adamc@707
|
246 val no_primary_key : fs ::: {Type} -> primary_key fs []
|
adamc@707
|
247 val primary_key : rest ::: {Type} -> t ::: Type -> key1 :: Name -> keys :: {Type}
|
adamc@707
|
248 -> [[key1] ~ keys] => [[key1 = t] ++ keys ~ rest]
|
adamc@707
|
249 => $([key1 = sql_injectable_prim t] ++ map sql_injectable_prim keys)
|
adamc@707
|
250 -> primary_key ([key1 = t] ++ keys ++ rest)
|
adamc@707
|
251 [Pkey = [key1] ++ map (fn _ => ()) keys]
|
adamc@707
|
252
|
adamc@707
|
253 (**** Other constraints *)
|
adamc@707
|
254
|
adamc@705
|
255 con sql_constraints :: {Type} -> {{Unit}} -> Type
|
adamc@705
|
256 (* Arguments: column types, uniqueness implications of constraints *)
|
adamc@704
|
257
|
adamc@705
|
258 con sql_constraint :: {Type} -> {Unit} -> Type
|
adamc@704
|
259
|
adamc@705
|
260 val no_constraint : fs ::: {Type} -> sql_constraints fs []
|
adamc@705
|
261 val one_constraint : fs ::: {Type} -> unique ::: {Unit} -> name :: Name
|
adamc@705
|
262 -> sql_constraint fs unique
|
adamc@705
|
263 -> sql_constraints fs [name = unique]
|
adamc@705
|
264 val join_constraints : fs ::: {Type}
|
adamc@705
|
265 -> uniques1 ::: {{Unit}} -> uniques2 ::: {{Unit}} -> [uniques1 ~ uniques2]
|
adamc@705
|
266 => sql_constraints fs uniques1 -> sql_constraints fs uniques2
|
adamc@705
|
267 -> sql_constraints fs (uniques1 ++ uniques2)
|
adamc@705
|
268
|
adamc@709
|
269
|
adamc@705
|
270 val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type}
|
adamc@705
|
271 -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest]
|
adamc@705
|
272 => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique)
|
adamc@704
|
273
|
adamc@712
|
274 class linkable :: Type -> Type -> Type
|
adamc@712
|
275 val linkable_same : t ::: Type -> linkable t t
|
adamc@712
|
276 val linkable_from_nullable : t ::: Type -> linkable (option t) t
|
adamc@712
|
277 val linkable_to_nullable : t ::: Type -> linkable t (option t)
|
adamc@712
|
278
|
adamc@709
|
279 con matching :: {Type} -> {Type} -> Type
|
adamc@709
|
280 val mat_nil : matching [] []
|
adamc@712
|
281 val mat_cons : t1 ::: Type -> rest1 ::: {Type} -> t2 ::: Type -> rest2 ::: {Type}
|
adamc@709
|
282 -> nm1 :: Name -> nm2 :: Name
|
adamc@709
|
283 -> [[nm1] ~ rest1] => [[nm2] ~ rest2]
|
adamc@712
|
284 => linkable t1 t2
|
adamc@712
|
285 -> matching rest1 rest2
|
adamc@712
|
286 -> matching ([nm1 = t1] ++ rest1) ([nm2 = t2] ++ rest2)
|
adamc@709
|
287
|
adamc@709
|
288 con propagation_mode :: {Type} -> Type
|
adamc@709
|
289 val restrict : fs ::: {Type} -> propagation_mode fs
|
adamc@709
|
290 val cascade : fs ::: {Type} -> propagation_mode fs
|
adamc@709
|
291 val no_action : fs ::: {Type} -> propagation_mode fs
|
adamc@709
|
292 val set_null : fs ::: {Type} -> propagation_mode (map option fs)
|
adamc@709
|
293
|
adamc@709
|
294
|
adamc@709
|
295 val foreign_key : mine1 ::: Name -> t ::: Type -> mine ::: {Type} -> munused ::: {Type}
|
adamc@709
|
296 -> foreign ::: {Type} -> funused ::: {Type}
|
adamc@709
|
297 -> nm ::: Name -> uniques ::: {{Unit}}
|
adamc@709
|
298 -> [[mine1] ~ mine] => [[mine1 = t] ++ mine ~ munused]
|
adamc@709
|
299 => [foreign ~ funused] => [[nm] ~ uniques]
|
adamc@709
|
300 => matching ([mine1 = t] ++ mine) foreign
|
adamc@709
|
301 -> sql_table (foreign ++ funused) ([nm = map (fn _ => ()) foreign] ++ uniques)
|
adamc@709
|
302 -> {OnDelete : propagation_mode ([mine1 = t] ++ mine),
|
adamc@709
|
303 OnUpdate : propagation_mode ([mine1 = t] ++ mine)}
|
adamc@709
|
304 -> sql_constraint ([mine1 = t] ++ mine ++ munused) []
|
adamc@709
|
305
|
adamc@714
|
306 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
|
adamc@1072
|
307 val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
|
adamc@1072
|
308 -> fs' ::: {{Type}} -> agg' ::: {{Type}} -> exps' ::: {Type}
|
adamc@1072
|
309 -> [fs ~ fs'] => [agg ~ agg'] => [exps ~ exps'] =>
|
adamc@1072
|
310 sql_exp fs agg exps t
|
adamc@1072
|
311 -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') t
|
adamc@714
|
312
|
adamc@714
|
313 val check : fs ::: {Type}
|
adamc@714
|
314 -> sql_exp [] [] fs bool
|
adamc@714
|
315 -> sql_constraint fs []
|
adamc@714
|
316
|
adamc@714
|
317
|
adamc@204
|
318 (*** Queries *)
|
adamc@204
|
319
|
adam@1394
|
320 con sql_query :: {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
|
adam@1394
|
321 con sql_query1 :: {{Type}} -> {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type
|
adamc@204
|
322
|
adamc@223
|
323 con sql_subset :: {{Type}} -> {{Type}} -> Type
|
adamc@223
|
324 val sql_subset : keep_drop :: {({Type} * {Type})}
|
adamc@354
|
325 -> sql_subset
|
adamc@621
|
326 (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop)
|
adamc@621
|
327 (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop)
|
adamc@354
|
328 val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables
|
adamc@1072
|
329 val sql_subset_concat : big1 ::: {{Type}} -> little1 ::: {{Type}}
|
adamc@1072
|
330 -> big2 ::: {{Type}} -> little2 ::: {{Type}}
|
adamc@1072
|
331 -> [big1 ~ big2] => [little1 ~ little2] =>
|
adamc@1072
|
332 sql_subset big1 little1
|
adamc@1072
|
333 -> sql_subset big2 little2
|
adamc@1072
|
334 -> sql_subset (big1 ++ big2) (little1 ++ little2)
|
adamc@223
|
335
|
adamc@1191
|
336 con sql_from_items :: {{Type}} -> {{Type}} -> Type
|
adamc@748
|
337
|
adamc@1195
|
338 val sql_from_nil : free ::: {{Type}} -> sql_from_items free []
|
adamc@1191
|
339 val sql_from_table : free ::: {{Type}} -> t ::: Type -> fs ::: {Type}
|
adamc@753
|
340 -> fieldsOf t fs -> name :: Name
|
adamc@1191
|
341 -> t -> sql_from_items free [name = fs]
|
adamc@1192
|
342 val sql_from_query : free ::: {{Type}} -> fs ::: {Type} -> name :: Name
|
adam@1394
|
343 -> sql_query free [] [] fs
|
adamc@1192
|
344 -> sql_from_items free [name = fs]
|
adamc@1191
|
345 val sql_from_comma : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
|
adamc@748
|
346 -> [tabs1 ~ tabs2]
|
adamc@1191
|
347 => sql_from_items free tabs1 -> sql_from_items free tabs2
|
adamc@1191
|
348 -> sql_from_items free (tabs1 ++ tabs2)
|
adamc@1191
|
349 val sql_inner_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}}
|
adamc@1191
|
350 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
|
adamc@1191
|
351 => sql_from_items free tabs1 -> sql_from_items free tabs2
|
adamc@1191
|
352 -> sql_exp (free ++ tabs1 ++ tabs2) [] [] bool
|
adamc@1191
|
353 -> sql_from_items free (tabs1 ++ tabs2)
|
adamc@748
|
354
|
adamc@750
|
355 class nullify :: Type -> Type -> Type
|
adamc@750
|
356 val nullify_option : t ::: Type -> nullify (option t) (option t)
|
adamc@750
|
357 val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t)
|
adamc@750
|
358
|
adamc@1191
|
359 val sql_left_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}}
|
adamc@1191
|
360 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
|
adamc@750
|
361 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2)
|
adamc@1191
|
362 -> sql_from_items free tabs1 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
|
adamc@1191
|
363 -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool
|
adamc@1191
|
364 -> sql_from_items free (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2)
|
adamc@750
|
365
|
adamc@1191
|
366 val sql_right_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}}
|
adamc@1191
|
367 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
|
adamc@751
|
368 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1)
|
adamc@1191
|
369 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items free tabs2
|
adamc@1191
|
370 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool
|
adamc@1191
|
371 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2)
|
adamc@751
|
372
|
adamc@1191
|
373 val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}}
|
adamc@1191
|
374 -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2]
|
adamc@751
|
375 => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2))
|
adamc@1191
|
376 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1)
|
adamc@1191
|
377 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2)
|
adamc@1191
|
378 -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool
|
adamc@1191
|
379 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2))
|
adamc@751
|
380
|
adamc@1191
|
381 val sql_query1 : free ::: {{Type}}
|
adam@1394
|
382 -> afree ::: {{Type}}
|
adamc@1191
|
383 -> tables ::: {{Type}}
|
adamc@354
|
384 -> grouped ::: {{Type}}
|
adamc@354
|
385 -> selectedFields ::: {{Type}}
|
adamc@354
|
386 -> selectedExps ::: {Type}
|
adamc@1070
|
387 -> empties :: {Unit}
|
adamc@1191
|
388 -> [free ~ tables]
|
adamc@1191
|
389 => [free ~ grouped]
|
adam@1394
|
390 => [afree ~ tables]
|
adamc@1191
|
391 => [empties ~ selectedFields]
|
adamc@1070
|
392 => {Distinct : bool,
|
adamc@1191
|
393 From : sql_from_items free tables,
|
adam@1394
|
394 Where : sql_exp (free ++ tables) afree [] bool,
|
adamc@748
|
395 GroupBy : sql_subset tables grouped,
|
adam@1394
|
396 Having : sql_exp (free ++ grouped) (afree ++ tables) [] bool,
|
adamc@1070
|
397 SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields),
|
adam@1394
|
398 SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) [])
|
adamc@705
|
399 selectedExps) }
|
adam@1394
|
400 -> sql_query1 free afree tables selectedFields selectedExps
|
adamc@229
|
401
|
adamc@229
|
402 type sql_relop
|
adamc@229
|
403 val sql_union : sql_relop
|
adamc@229
|
404 val sql_intersect : sql_relop
|
adamc@229
|
405 val sql_except : sql_relop
|
adamc@1191
|
406 val sql_relop : free ::: {{Type}}
|
adam@1394
|
407 -> afree ::: {{Type}}
|
adamc@1191
|
408 -> tables1 ::: {{Type}}
|
adamc@354
|
409 -> tables2 ::: {{Type}}
|
adamc@354
|
410 -> selectedFields ::: {{Type}}
|
adamc@354
|
411 -> selectedExps ::: {Type}
|
adamc@354
|
412 -> sql_relop
|
adam@1427
|
413 -> bool (* ALL *)
|
adam@1394
|
414 -> sql_query1 free afree tables1 selectedFields selectedExps
|
adam@1394
|
415 -> sql_query1 free afree tables2 selectedFields selectedExps
|
adam@1394
|
416 -> sql_query1 free afree [] selectedFields selectedExps
|
adam@1394
|
417 val sql_forget_tables : free ::: {{Type}} -> afree ::: {{Type}} -> tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type}
|
adam@1394
|
418 -> sql_query1 free afree tables selectedFields selectedExps
|
adam@1394
|
419 -> sql_query1 free afree [] selectedFields selectedExps
|
adamc@229
|
420
|
adamc@230
|
421 type sql_direction
|
adamc@230
|
422 val sql_asc : sql_direction
|
adamc@230
|
423 val sql_desc : sql_direction
|
adamc@230
|
424
|
adamc@234
|
425 con sql_order_by :: {{Type}} -> {Type} -> Type
|
adamc@234
|
426 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
|
adamc@234
|
427 val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
|
adamc@354
|
428 -> sql_exp tables [] exps t -> sql_direction
|
adamc@354
|
429 -> sql_order_by tables exps
|
adamc@354
|
430 -> sql_order_by tables exps
|
adamc@230
|
431
|
adamc@231
|
432 type sql_limit
|
adamc@231
|
433 val sql_no_limit : sql_limit
|
adamc@231
|
434 val sql_limit : int -> sql_limit
|
adamc@354
|
435
|
adamc@232
|
436 type sql_offset
|
adamc@232
|
437 val sql_no_offset : sql_offset
|
adamc@232
|
438 val sql_offset : int -> sql_offset
|
adamc@232
|
439
|
adamc@1191
|
440 val sql_query : free ::: {{Type}}
|
adam@1394
|
441 -> afree ::: {{Type}}
|
adamc@1191
|
442 -> tables ::: {{Type}}
|
adamc@354
|
443 -> selectedFields ::: {{Type}}
|
adamc@354
|
444 -> selectedExps ::: {Type}
|
adamc@1191
|
445 -> [free ~ tables]
|
adam@1394
|
446 => {Rows : sql_query1 free afree tables selectedFields selectedExps,
|
adamc@1191
|
447 OrderBy : sql_order_by (free ++ tables) selectedExps,
|
adamc@354
|
448 Limit : sql_limit,
|
adamc@354
|
449 Offset : sql_offset}
|
adam@1394
|
450 -> sql_query free afree selectedFields selectedExps
|
adamc@204
|
451
|
adamc@354
|
452 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
|
adamc@354
|
453 -> fieldType ::: Type -> agg ::: {{Type}}
|
adamc@354
|
454 -> exps ::: {Type}
|
adamc@354
|
455 -> tab :: Name -> field :: Name
|
adamc@354
|
456 -> sql_exp
|
adamc@354
|
457 ([tab = [field = fieldType] ++ otherFields] ++ otherTabs)
|
adamc@354
|
458 agg exps fieldType
|
adamc@234
|
459
|
adamc@354
|
460 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type}
|
adamc@354
|
461 -> nm :: Name
|
adamc@354
|
462 -> sql_exp tabs agg ([nm = t] ++ rest) t
|
adamc@209
|
463
|
adamc@221
|
464 class sql_injectable
|
adamc@676
|
465 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t
|
adamc@676
|
466 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)
|
adamc@676
|
467
|
adamc@354
|
468 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
adamc@354
|
469 -> t ::: Type
|
adamc@354
|
470 -> sql_injectable t -> t -> sql_exp tables agg exps t
|
adamc@209
|
471
|
adamc@470
|
472 val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
adamc@470
|
473 -> t ::: Type
|
adamc@470
|
474 -> sql_exp tables agg exps (option t)
|
adamc@470
|
475 -> sql_exp tables agg exps bool
|
adamc@470
|
476
|
adam@1602
|
477 val sql_coalesce : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
adam@1602
|
478 -> t ::: Type
|
adam@1602
|
479 -> sql_exp tables agg exps (option t)
|
adam@1602
|
480 -> sql_exp tables agg exps t
|
adam@1602
|
481 -> sql_exp tables agg exps t
|
adam@1602
|
482
|
kkallio@1572
|
483 val sql_if_then_else : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
kkallio@1572
|
484 -> t ::: Type
|
kkallio@1572
|
485 -> sql_exp tables agg exps bool
|
kkallio@1572
|
486 -> sql_exp tables agg exps t
|
kkallio@1572
|
487 -> sql_exp tables agg exps t
|
kkallio@1572
|
488 -> sql_exp tables agg exps t
|
kkallio@1572
|
489
|
adamc@559
|
490 class sql_arith
|
adam@1427
|
491 val sql_arith_int : sql_arith int
|
adam@1427
|
492 val sql_arith_float : sql_arith float
|
adam@1427
|
493 val sql_arith_option : t ::: Type -> sql_arith t -> sql_arith (option t)
|
adamc@559
|
494
|
adamc@220
|
495 con sql_unary :: Type -> Type -> Type
|
adamc@220
|
496 val sql_not : sql_unary bool bool
|
adamc@354
|
497 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
adamc@354
|
498 -> arg ::: Type -> res ::: Type
|
adamc@354
|
499 -> sql_unary arg res -> sql_exp tables agg exps arg
|
adamc@354
|
500 -> sql_exp tables agg exps res
|
adamc@220
|
501
|
adamc@559
|
502 val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t
|
adamc@559
|
503
|
adamc@220
|
504 con sql_binary :: Type -> Type -> Type -> Type
|
adamc@220
|
505 val sql_and : sql_binary bool bool bool
|
adamc@220
|
506 val sql_or : sql_binary bool bool bool
|
adamc@234
|
507 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
adamc@354
|
508 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
|
adamc@354
|
509 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1
|
adamc@354
|
510 -> sql_exp tables agg exps arg2
|
adamc@354
|
511 -> sql_exp tables agg exps res
|
adamc@220
|
512
|
adamc@559
|
513 val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t
|
adamc@559
|
514 val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t
|
adamc@559
|
515 val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t
|
adamc@559
|
516 val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t
|
adamc@559
|
517 val sql_mod : sql_binary int int int
|
adamc@559
|
518
|
adamc@559
|
519 val sql_eq : t ::: Type -> sql_binary t t bool
|
adamc@559
|
520 val sql_ne : t ::: Type -> sql_binary t t bool
|
adamc@559
|
521 val sql_lt : t ::: Type -> sql_binary t t bool
|
adamc@559
|
522 val sql_le : t ::: Type -> sql_binary t t bool
|
adamc@559
|
523 val sql_gt : t ::: Type -> sql_binary t t bool
|
adamc@559
|
524 val sql_ge : t ::: Type -> sql_binary t t bool
|
adamc@203
|
525
|
kkallio@1607
|
526 val sql_like : sql_binary string string bool
|
kkallio@1607
|
527
|
adamc@235
|
528 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
adamc@544
|
529 -> sql_exp tables agg exps int
|
adamc@235
|
530
|
adamc@1187
|
531 con sql_aggregate :: Type -> Type -> Type
|
adamc@354
|
532 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
adamc@1187
|
533 -> dom ::: Type -> ran ::: Type
|
adamc@1187
|
534 -> sql_aggregate dom ran -> sql_exp agg agg exps dom
|
adamc@1187
|
535 -> sql_exp tables agg exps ran
|
adamc@1187
|
536
|
adamc@1187
|
537 val sql_count_col : t ::: Type -> sql_aggregate (option t) int
|
adamc@236
|
538
|
adamc@236
|
539 class sql_summable
|
adamc@236
|
540 val sql_summable_int : sql_summable int
|
adamc@236
|
541 val sql_summable_float : sql_summable float
|
adam@1357
|
542 val sql_summable_option : t ::: Type -> sql_summable t -> sql_summable (option t)
|
adam@1394
|
543 val sql_avg : t ::: Type -> nt ::: Type -> sql_summable t -> nullify t nt -> sql_aggregate t nt
|
adam@1394
|
544 val sql_sum : t ::: Type -> nt ::: Type -> sql_summable t -> nullify t nt -> sql_aggregate t nt
|
adamc@236
|
545
|
adamc@236
|
546 class sql_maxable
|
adamc@236
|
547 val sql_maxable_int : sql_maxable int
|
adamc@236
|
548 val sql_maxable_float : sql_maxable float
|
adamc@236
|
549 val sql_maxable_string : sql_maxable string
|
adamc@437
|
550 val sql_maxable_time : sql_maxable time
|
adam@1357
|
551 val sql_maxable_option : t ::: Type -> sql_maxable t -> sql_maxable (option t)
|
adam@1394
|
552 val sql_max : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
|
adam@1394
|
553 val sql_min : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt
|
adamc@236
|
554
|
adamc@441
|
555 con sql_nfunc :: Type -> Type
|
adamc@441
|
556 val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
adamc@441
|
557 -> t ::: Type
|
adamc@441
|
558 -> sql_nfunc t -> sql_exp tables agg exps t
|
adamc@441
|
559 val sql_current_timestamp : sql_nfunc time
|
adamc@441
|
560
|
adamc@746
|
561 con sql_ufunc :: Type -> Type -> Type
|
adamc@746
|
562 val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
adamc@746
|
563 -> dom ::: Type -> ran ::: Type
|
adamc@746
|
564 -> sql_ufunc dom ran -> sql_exp tables agg exps dom
|
adamc@746
|
565 -> sql_exp tables agg exps ran
|
adamc@746
|
566 val sql_octet_length : sql_ufunc blob int
|
adamc@1207
|
567 val sql_known : t ::: Type -> sql_ufunc t bool
|
adamc@746
|
568
|
adamc@235
|
569
|
adamc@1081
|
570 val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
|
adamc@1081
|
571 -> sql_injectable_prim t
|
adamc@1081
|
572 -> sql_exp tables agg exps t
|
adamc@1081
|
573 -> sql_exp tables agg exps (option t)
|
adamc@1081
|
574
|
adam@1421
|
575 val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type -> nt ::: Type
|
adam@1421
|
576 -> nullify t nt
|
adam@1394
|
577 -> sql_query tables agg [] [nm = t]
|
adam@1421
|
578 -> sql_exp tables agg exps nt
|
adamc@1191
|
579
|
adamc@243
|
580 (*** Executing queries *)
|
adamc@243
|
581
|
adamc@354
|
582 val query : tables ::: {{Type}} -> exps ::: {Type}
|
adamc@629
|
583 -> [tables ~ exps] =>
|
adamc@354
|
584 state ::: Type
|
adam@1394
|
585 -> sql_query [] [] tables exps
|
adamc@621
|
586 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
|
adamc@354
|
587 -> state
|
adamc@354
|
588 -> transaction state)
|
adamc@354
|
589 -> state
|
adamc@354
|
590 -> transaction state
|
adamc@243
|
591
|
adamc@243
|
592
|
adamc@299
|
593 (*** Database mutators *)
|
adamc@299
|
594
|
adamc@299
|
595 type dml
|
adamc@299
|
596 val dml : dml -> transaction unit
|
adam@1293
|
597 val tryDml : dml -> transaction (option string)
|
adam@1293
|
598 (* Returns an error message on failure. *)
|
adamc@299
|
599
|
adamc@705
|
600 val insert : fields ::: {Type} -> uniques ::: {{Unit}}
|
adamc@705
|
601 -> sql_table fields uniques
|
adamc@621
|
602 -> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
|
adamc@354
|
603 -> dml
|
adamc@299
|
604
|
adamc@705
|
605 val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} ->
|
adamc@629
|
606 [changed ~ unchanged] =>
|
adamc@621
|
607 $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
|
adamc@705
|
608 -> sql_table (changed ++ unchanged) uniques
|
adamc@354
|
609 -> sql_exp [T = changed ++ unchanged] [] [] bool
|
adamc@354
|
610 -> dml
|
adamc@299
|
611
|
adamc@705
|
612 val delete : fields ::: {Type} -> uniques ::: {{Unit}}
|
adamc@705
|
613 -> sql_table fields uniques
|
adamc@354
|
614 -> sql_exp [T = fields] [] [] bool
|
adamc@354
|
615 -> dml
|
adamc@299
|
616
|
adamc@338
|
617 (*** Sequences *)
|
adamc@338
|
618
|
adamc@338
|
619 type sql_sequence
|
adamc@338
|
620 val nextval : sql_sequence -> transaction int
|
adamc@1073
|
621 val setval : sql_sequence -> int -> transaction unit
|
adamc@338
|
622
|
adamc@299
|
623
|
adamc@203
|
624 (** XML *)
|
adamc@203
|
625
|
adamc@721
|
626 type css_class
|
adam@1477
|
627 val show_css_class : show css_class
|
adam@1567
|
628 val null : css_class
|
adam@1567
|
629 (* No special formatting *)
|
adam@1292
|
630 val classes : css_class -> css_class -> css_class
|
adam@1292
|
631 (* The equivalent of writing one class after the other, separated by a space, in
|
adam@1292
|
632 * an HTML 'class' attribute *)
|
adamc@718
|
633
|
adamc@720
|
634 con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
|
adamc@91
|
635
|
adamc@720
|
636 con xml :: {Unit} -> {Type} -> {Type} -> Type
|
adamc@720
|
637 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
|
adam@1358
|
638 val cdataChar : ctx ::: {Unit} -> use ::: {Type} -> char -> xml ctx use []
|
adamc@354
|
639 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type}
|
adamc@354
|
640 -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
|
adamc@354
|
641 -> useOuter ::: {Type} -> useInner ::: {Type}
|
adamc@354
|
642 -> bindOuter ::: {Type} -> bindInner ::: {Type}
|
adamc@629
|
643 -> [attrsGiven ~ attrsAbsent] =>
|
adamc@629
|
644 [useOuter ~ useInner] =>
|
adamc@629
|
645 [bindOuter ~ bindInner] =>
|
adamc@721
|
646 option css_class
|
adamc@721
|
647 -> $attrsGiven
|
adamc@629
|
648 -> tag (attrsGiven ++ attrsAbsent)
|
adamc@720
|
649 ctxOuter ctxInner useOuter bindOuter
|
adamc@720
|
650 -> xml ctxInner useInner bindInner
|
adamc@720
|
651 -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
|
adamc@140
|
652 val join : ctx ::: {Unit}
|
adamc@720
|
653 -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
|
adamc@720
|
654 -> [use1 ~ bind1] => [bind1 ~ bind2] =>
|
adamc@720
|
655 xml ctx use1 bind1
|
adamc@720
|
656 -> xml ctx (use1 ++ bind1) bind2
|
adamc@720
|
657 -> xml ctx use1 (bind1 ++ bind2)
|
adamc@354
|
658 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type}
|
adamc@720
|
659 -> bind ::: {Type}
|
adamc@629
|
660 -> [use1 ~ use2] =>
|
adamc@720
|
661 xml ctx use1 bind
|
adamc@720
|
662 -> xml ctx (use1 ++ use2) bind
|
adamc@91
|
663
|
adamc@110
|
664 con xhtml = xml [Html]
|
adamc@139
|
665 con page = xhtml [] []
|
adamc@720
|
666 con xbody = xml [Body] [] []
|
adamc@1277
|
667 con xtable = xml [Body, Table] [] []
|
adamc@720
|
668 con xtr = xml [Body, Tr] [] []
|
adamc@720
|
669 con xform = xml [Body, Form] [] []
|
adamc@110
|
670
|
adamc@718
|
671
|
adamc@204
|
672 (*** HTML details *)
|
adamc@204
|
673
|
adamc@140
|
674 con html = [Html]
|
adamc@140
|
675 con head = [Head]
|
adamc@140
|
676 con body = [Body]
|
adamc@361
|
677 con form = [Body, Form]
|
adamc@760
|
678 con subform = [Body, Subform]
|
adamc@332
|
679 con tabl = [Body, Table]
|
adamc@332
|
680 con tr = [Body, Tr]
|
adamc@93
|
681
|
adam@1370
|
682 type queryString
|
adam@1370
|
683 val show_queryString : show queryString
|
adam@1370
|
684
|
adamc@724
|
685 type url
|
adamc@1065
|
686 val show_url : show url
|
adamc@724
|
687 val bless : string -> url
|
adamc@770
|
688 val checkUrl : string -> option url
|
adamc@1085
|
689 val currentUrl : transaction url
|
adam@1386
|
690 val currentUrlHasPost : transaction bool
|
adam@1485
|
691 val currentUrlHasQueryString : transaction bool
|
adamc@1065
|
692 val url : transaction page -> url
|
adam@1370
|
693 val effectfulUrl : (option queryString -> transaction page) -> url
|
adamc@1065
|
694 val redirect : t ::: Type -> url -> transaction t
|
adamc@724
|
695
|
adam@1556
|
696 type id
|
adam@1556
|
697 val fresh : transaction id
|
adam@1556
|
698
|
adamc@847
|
699 val dyn : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> [ctx ~ body] => unit
|
adamc@847
|
700 -> tag [Signal = signal (xml (body ++ ctx) use bind)] (body ++ ctx) [] use bind
|
adamc@568
|
701
|
adamc@720
|
702 val head : unit -> tag [] html head [] []
|
adamc@720
|
703 val title : unit -> tag [] head [] [] []
|
adam@1556
|
704 val link : unit -> tag [Id = id, Rel = string, Typ = string, Href = url, Media = string] head [] [] []
|
adamc@110
|
705
|
adamc@892
|
706 val body : unit -> tag [Onload = transaction unit, Onresize = transaction unit, Onunload = transaction unit]
|
adamc@892
|
707 html body [] []
|
adamc@354
|
708 con bodyTag = fn (attrs :: {Type}) =>
|
adamc@354
|
709 ctx ::: {Unit} ->
|
adamc@629
|
710 [[Body] ~ ctx] =>
|
adamc@720
|
711 unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
|
adamc@354
|
712 con bodyTagStandalone = fn (attrs :: {Type}) =>
|
adamc@354
|
713 ctx ::: {Unit}
|
adamc@629
|
714 -> [[Body] ~ ctx] =>
|
adamc@720
|
715 unit -> tag attrs ([Body] ++ ctx) [] [] []
|
adamc@141
|
716
|
adam@1556
|
717 val br : bodyTagStandalone [Id = id]
|
adamc@119
|
718
|
adamc@892
|
719 con focusEvents = [Onblur = transaction unit, Onfocus = transaction unit]
|
adamc@892
|
720 con mouseEvents = [Onclick = transaction unit, Ondblclick = transaction unit,
|
adamc@892
|
721 Onmousedown = transaction unit, Onmousemove = transaction unit,
|
adamc@892
|
722 Onmouseout = transaction unit, Onmouseover = transaction unit,
|
adamc@894
|
723 Onmouseup = transaction unit]
|
adamc@895
|
724 con keyEvents = [Onkeydown = int -> transaction unit, Onkeypress = int -> transaction unit,
|
adamc@895
|
725 Onkeyup = int -> transaction unit]
|
adamc@895
|
726 (* Key arguments are character codes. *)
|
adamc@892
|
727 con resizeEvents = [Onresize = transaction unit]
|
adamc@691
|
728
|
adamc@892
|
729 con boxEvents = focusEvents ++ mouseEvents ++ keyEvents ++ resizeEvents
|
adamc@892
|
730 con tableEvents = focusEvents ++ mouseEvents ++ keyEvents
|
adamc@140
|
731
|
adam@1556
|
732 con boxAttrs = [Id = id, Title = string] ++ boxEvents
|
adam@1556
|
733 con tableAttrs = [Id = id, Title = string] ++ tableEvents
|
adamc@469
|
734
|
adamc@1047
|
735 val span : bodyTag boxAttrs
|
adamc@1047
|
736 val div : bodyTag boxAttrs
|
adamc@140
|
737
|
adamc@1047
|
738 val p : bodyTag boxAttrs
|
adamc@1047
|
739 val b : bodyTag boxAttrs
|
adamc@1047
|
740 val i : bodyTag boxAttrs
|
adamc@1047
|
741 val tt : bodyTag boxAttrs
|
kkallio@1452
|
742 val sub : bodyTag boxAttrs
|
kkallio@1452
|
743 val sup : bodyTag boxAttrs
|
adamc@410
|
744
|
adamc@1047
|
745 val h1 : bodyTag boxAttrs
|
adamc@1047
|
746 val h2 : bodyTag boxAttrs
|
adamc@1047
|
747 val h3 : bodyTag boxAttrs
|
adamc@1047
|
748 val h4 : bodyTag boxAttrs
|
adamc@1047
|
749 val h5 : bodyTag boxAttrs
|
adamc@1047
|
750 val h6 : bodyTag boxAttrs
|
adamc@717
|
751
|
adamc@1047
|
752 val li : bodyTag boxAttrs
|
adamc@1047
|
753 val ol : bodyTag boxAttrs
|
adamc@1047
|
754 val ul : bodyTag boxAttrs
|
adamc@140
|
755
|
adamc@1047
|
756 val hr : bodyTag boxAttrs
|
adamc@1047
|
757
|
vshabanoff@1560
|
758 val a : bodyTag ([Link = transaction page, Href = url, Target = string] ++ boxAttrs)
|
adamc@892
|
759
|
adam@1419
|
760 val img : bodyTag ([Alt = string, Src = url, Width = int, Height = int,
|
adamc@1129
|
761 Onabort = transaction unit, Onerror = transaction unit,
|
adamc@1047
|
762 Onload = transaction unit] ++ boxAttrs)
|
adamc@892
|
763
|
adamc@720
|
764 val form : ctx ::: {Unit} -> bind ::: {Type}
|
adamc@1120
|
765 -> [[Body, Form, Table] ~ ctx] =>
|
adam@1412
|
766 option css_class
|
adam@1412
|
767 -> xml ([Body, Form] ++ ctx) [] bind
|
adamc@756
|
768 -> xml ([Body] ++ ctx) [] []
|
adamc@756
|
769
|
adamc@756
|
770 val subform : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
|
adamc@756
|
771 -> [[Form] ~ ctx] =>
|
adamc@756
|
772 nm :: Name -> [[nm] ~ use] =>
|
adamc@1004
|
773 xml ([Form] ++ ctx) [] bind
|
adamc@756
|
774 -> xml ([Form] ++ ctx) use [nm = $bind]
|
adamc@758
|
775
|
adamc@758
|
776 val subforms : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
|
adamc@1004
|
777 -> [[Form, Subform] ~ ctx] =>
|
adamc@758
|
778 nm :: Name -> [[nm] ~ use] =>
|
adamc@1004
|
779 xml ([Subform] ++ ctx) [Entry = $bind] []
|
adamc@758
|
780 -> xml ([Form] ++ ctx) use [nm = list ($bind)]
|
adamc@758
|
781
|
adamc@758
|
782 val entry : ctx ::: {Unit} -> bind ::: {Type}
|
adamc@1004
|
783 -> [[Subform, Form] ~ ctx] =>
|
adamc@1004
|
784 xml ([Form] ++ ctx) [] bind
|
adamc@758
|
785 -> xml ([Subform] ++ ctx) [Entry = $bind] []
|
adamc@758
|
786
|
adamc@361
|
787 con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) =>
|
adamc@354
|
788 ctx ::: {Unit}
|
adamc@629
|
789 -> [[Form] ~ ctx] =>
|
adamc@354
|
790 nm :: Name -> unit
|
adamc@720
|
791 -> tag attrs ([Form] ++ ctx) inner [] [nm = ty]
|
adamc@1047
|
792 val hidden : formTag string [] [Id = string, Value = string]
|
adamc@892
|
793 val textbox : formTag string [] ([Value = string, Size = int, Source = source string, Onchange = transaction unit,
|
adamc@1047
|
794 Ontext = transaction unit] ++ boxAttrs)
|
adamc@1047
|
795 val password : formTag string [] ([Value = string, Size = int] ++ boxAttrs)
|
adamc@892
|
796 val textarea : formTag string [] ([Rows = int, Cols = int, Onchange = transaction unit,
|
adamc@1047
|
797 Ontext = transaction unit] ++ boxAttrs)
|
adamc@153
|
798
|
adamc@1047
|
799 val checkbox : formTag bool [] ([Checked = bool] ++ boxAttrs)
|
adamc@190
|
800
|
adamc@737
|
801 type file
|
adamc@737
|
802 val fileName : file -> option string
|
adamc@740
|
803 val fileMimeType : file -> string
|
adamc@737
|
804 val fileData : file -> blob
|
adamc@737
|
805
|
adamc@1047
|
806 val upload : formTag file [] ([Value = string, Size = int] ++ boxAttrs)
|
adamc@737
|
807
|
adamc@741
|
808 type mimeType
|
adamc@741
|
809 val blessMime : string -> mimeType
|
adamc@770
|
810 val checkMime : string -> option mimeType
|
adamc@741
|
811 val returnBlob : t ::: Type -> blob -> mimeType -> transaction t
|
adamc@745
|
812 val blobSize : blob -> int
|
adamc@1119
|
813 val textBlob : string -> blob
|
adamc@741
|
814
|
adam@1347
|
815 type postBody
|
adam@1347
|
816 val postType : postBody -> string
|
adam@1347
|
817 val postData : postBody -> string
|
adam@1347
|
818
|
adamc@153
|
819 con radio = [Body, Radio]
|
adam@1556
|
820 val radio : formTag string radio [Id = id]
|
adamc@1068
|
821 val radioOption : unit -> tag ([Value = string, Checked = bool] ++ boxAttrs) radio [] [] []
|
adamc@142
|
822
|
adamc@154
|
823 con select = [Select]
|
adamc@1047
|
824 val select : formTag string select ([Onchange = transaction unit] ++ boxAttrs)
|
adamc@720
|
825 val option : unit -> tag [Value = string, Selected = bool] select [] [] []
|
adamc@154
|
826
|
adamc@720
|
827 val submit : ctx ::: {Unit} -> use ::: {Type}
|
adamc@629
|
828 -> [[Form] ~ ctx] =>
|
adamc@354
|
829 unit
|
adamc@1047
|
830 -> tag ([Value = string, Action = $use -> transaction page] ++ boxAttrs)
|
adamc@720
|
831 ([Form] ++ ctx) ([Form] ++ ctx) use []
|
adamc@283
|
832
|
adam@1517
|
833 val image : ctx ::: {Unit} -> use ::: {Type}
|
adam@1517
|
834 -> [[Form] ~ ctx] =>
|
adam@1517
|
835 unit
|
adam@1517
|
836 -> tag ([Src = url, Width = int, Height = int, Alt = string, Action = $use -> transaction page] ++ boxAttrs)
|
adam@1517
|
837 ([Form] ++ ctx) ([Form] ++ ctx) use []
|
adam@1517
|
838
|
adam@1557
|
839 val label : bodyTag ([For = id, Accesskey = string] ++ tableAttrs)
|
adamc@1047
|
840
|
adamc@1047
|
841
|
adamc@601
|
842 (*** AJAX-oriented widgets *)
|
adamc@601
|
843
|
adamc@797
|
844 con cformTag = fn (attrs :: {Type}) (inner :: {Unit}) =>
|
adamc@601
|
845 ctx ::: {Unit}
|
adamc@629
|
846 -> [[Body] ~ ctx] =>
|
adamc@797
|
847 unit -> tag attrs ([Body] ++ ctx) inner [] []
|
adamc@601
|
848
|
adamc@892
|
849 val ctextbox : cformTag ([Value = string, Size = int, Source = source string, Onchange = transaction unit,
|
adamc@1047
|
850 Ontext = transaction unit] ++ boxAttrs) []
|
adamc@1047
|
851 val button : cformTag ([Value = string] ++ boxAttrs) []
|
adamc@797
|
852
|
adamc@1047
|
853 val ccheckbox : cformTag ([Value = bool, Size = int, Source = source bool] ++ boxAttrs) []
|
adamc@817
|
854
|
adamc@797
|
855 con cselect = [Cselect]
|
adamc@1047
|
856 val cselect : cformTag ([Source = source string, Onchange = transaction unit] ++ boxAttrs) cselect
|
adamc@797
|
857 val coption : unit -> tag [Value = string, Selected = bool] cselect [] [] []
|
adamc@601
|
858
|
adamc@1099
|
859 val ctextarea : cformTag ([Value = string, Rows = int, Cols = int, Source = source string, Onchange = transaction unit,
|
adamc@1099
|
860 Ontext = transaction unit] ++ boxAttrs) []
|
adamc@1099
|
861
|
adamc@720
|
862 (*** Tables *)
|
adamc@720
|
863
|
adamc@892
|
864 val tabl : other ::: {Unit} -> [other ~ [Body, Table]] => unit
|
adamc@1047
|
865 -> tag ([Border = int] ++ boxAttrs)
|
adamc@892
|
866 ([Body] ++ other) ([Body, Table] ++ other) [] []
|
adamc@892
|
867 val tr : other ::: {Unit} -> [other ~ [Body, Table, Tr]] => unit
|
adamc@1047
|
868 -> tag tableAttrs
|
adamc@892
|
869 ([Body, Table] ++ other) ([Body, Tr] ++ other) [] []
|
adamc@892
|
870 val th : other ::: {Unit} -> [other ~ [Body, Tr]] => unit
|
kkallio@1476
|
871 -> tag ([Colspan = int, Rowspan = int] ++ tableAttrs)
|
adamc@892
|
872 ([Body, Tr] ++ other) ([Body] ++ other) [] []
|
adamc@892
|
873 val td : other ::: {Unit} -> [other ~ [Body, Tr]] => unit
|
kkallio@1476
|
874 -> tag ([Colspan = int, Rowspan = int] ++ tableAttrs)
|
adamc@892
|
875 ([Body, Tr] ++ other) ([Body] ++ other) [] []
|
adamc@720
|
876
|
adamc@283
|
877
|
adamc@283
|
878 (** Aborting *)
|
adamc@283
|
879
|
adamc@726
|
880 val error : t ::: Type -> xbody -> t
|
adamc@720
|
881
|
adamc@729
|
882 (* Client-side-only handlers: *)
|
adamc@726
|
883 val onError : (xbody -> transaction unit) -> transaction unit
|
adamc@728
|
884 val onFail : (string -> transaction unit) -> transaction unit
|
adamc@729
|
885 val onConnectFail : transaction unit -> transaction unit
|
adamc@729
|
886 val onDisconnect : transaction unit -> transaction unit
|
adamc@729
|
887 val onServerError : (string -> transaction unit) -> transaction unit
|
adamc@727
|
888
|
adam@1555
|
889 (* More standard document-level JavaScript handlers *)
|
adam@1555
|
890 val onClick : transaction unit -> transaction unit
|
adam@1555
|
891 val onDblclick : transaction unit -> transaction unit
|
adam@1555
|
892 val onKeydown : (int -> transaction unit) -> transaction unit
|
adam@1555
|
893 val onKeypress : (int -> transaction unit) -> transaction unit
|
adam@1555
|
894 val onKeyup : (int -> transaction unit) -> transaction unit
|
adam@1555
|
895 val onMousedown : transaction unit -> transaction unit
|
adam@1555
|
896 val onMouseup : transaction unit -> transaction unit
|
adam@1555
|
897
|
adam@1559
|
898 (* Prevents default handling of current event *)
|
adam@1559
|
899 val preventDefault : transaction unit
|
adam@1559
|
900 (* Stops propagation of current event *)
|
adam@1559
|
901 val stopPropagation : transaction unit
|
adam@1559
|
902
|
adamc@727
|
903 val show_xml : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> show (xml ctx use bind)
|
adamc@1075
|
904
|
adamc@1075
|
905
|
adamc@1075
|
906 (** Tasks *)
|
adamc@1075
|
907
|
adam@1348
|
908 con task_kind :: Type -> Type
|
adam@1348
|
909 val initialize : task_kind unit
|
adam@1348
|
910 val clientLeaves : task_kind client
|
adam@1349
|
911 val periodic : int -> task_kind unit
|
adamc@1120
|
912
|
adamc@1120
|
913
|
adamc@1199
|
914 (** Information flow security *)
|
adamc@1199
|
915
|
adamc@1199
|
916 type sql_policy
|
adamc@1199
|
917
|
adamc@1214
|
918 val sendClient : tables ::: {{Type}} -> exps ::: {Type}
|
adam@1394
|
919 -> [tables ~ exps] => sql_query [] [] tables exps
|
adamc@1214
|
920 -> sql_policy
|
adamc@1199
|
921
|
adamc@1229
|
922 val sendOwnIds : sql_sequence -> sql_policy
|
adamc@1229
|
923
|
adamc@1220
|
924 val mayInsert : fs ::: {Type} -> tables ::: {{Type}} -> [[New] ~ tables]
|
adam@1394
|
925 => sql_query [] [] ([New = fs] ++ tables) []
|
adamc@1220
|
926 -> sql_policy
|
adamc@1220
|
927
|
adamc@1221
|
928 val mayDelete : fs ::: {Type} -> tables ::: {{Type}} -> [[Old] ~ tables]
|
adam@1394
|
929 => sql_query [] [] ([Old = fs] ++ tables) []
|
adamc@1221
|
930 -> sql_policy
|
adamc@1221
|
931
|
adamc@1223
|
932 val mayUpdate : fs ::: {Type} -> tables ::: {{Type}} -> [[Old, New] ~ tables]
|
adam@1394
|
933 => sql_query [] [] ([Old = fs, New = fs] ++ tables) []
|
adamc@1223
|
934 -> sql_policy
|
adamc@1223
|
935
|
adamc@1240
|
936 val also : sql_policy -> sql_policy -> sql_policy
|
adamc@1199
|
937
|
adamc@1120
|
938 val debug : string -> transaction unit
|
adam@1389
|
939 val naughtyDebug : string -> int
|
adamc@1250
|
940
|
adamc@1250
|
941 val rand : transaction int
|