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