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@91
|
9
|
adamc@256
|
10 (** Basic type classes *)
|
adamc@256
|
11
|
adamc@256
|
12 class eq
|
adamc@256
|
13 val eq : t ::: Type -> eq t -> t -> t -> bool
|
adamc@257
|
14 val ne : t ::: Type -> eq t -> t -> t -> bool
|
adamc@256
|
15 val eq_int : eq int
|
adamc@256
|
16 val eq_string : eq string
|
adamc@256
|
17 val eq_bool : eq bool
|
adamc@256
|
18
|
adamc@256
|
19
|
adamc@283
|
20 (** String operations *)
|
adamc@283
|
21
|
adamc@283
|
22 val strcat : string -> string -> string
|
adamc@283
|
23
|
adamc@283
|
24
|
adamc@203
|
25 (** SQL *)
|
adamc@203
|
26
|
adamc@203
|
27 con sql_table :: {Type} -> Type
|
adamc@203
|
28
|
adamc@204
|
29 (*** Queries *)
|
adamc@204
|
30
|
adamc@233
|
31 con sql_query :: {{Type}} -> {Type} -> Type
|
adamc@233
|
32 con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type
|
adamc@234
|
33 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
|
adamc@204
|
34
|
adamc@223
|
35 con sql_subset :: {{Type}} -> {{Type}} -> Type
|
adamc@223
|
36 val sql_subset : keep_drop :: {({Type} * {Type})}
|
adamc@223
|
37 -> sql_subset
|
adamc@223
|
38 (fold (fn nm => fn fields :: ({Type} * {Type}) => fn acc =>
|
adamc@223
|
39 [nm] ~ acc => fields.1 ~ fields.2 =>
|
adamc@223
|
40 [nm = fields.1 ++ fields.2] ++ acc) [] keep_drop)
|
adamc@223
|
41 (fold (fn nm => fn fields :: ({Type} * {Type}) => fn acc =>
|
adamc@223
|
42 [nm] ~ acc =>
|
adamc@223
|
43 [nm = fields.1] ++ acc) [] keep_drop)
|
adamc@223
|
44 val sql_subset_all : tables :: {{Type}}
|
adamc@223
|
45 -> sql_subset tables tables
|
adamc@223
|
46
|
adamc@229
|
47 val sql_query1 : tables ::: {{Type}}
|
adamc@224
|
48 -> grouped ::: {{Type}}
|
adamc@233
|
49 -> selectedFields ::: {{Type}}
|
adamc@233
|
50 -> selectedExps ::: {Type}
|
adamc@223
|
51 -> {From : $(fold (fn nm => fn fields :: {Type} => fn acc =>
|
adamc@223
|
52 [nm] ~ acc => [nm = sql_table fields] ++ acc) [] tables),
|
adamc@234
|
53 Where : sql_exp tables [] [] bool,
|
adamc@224
|
54 GroupBy : sql_subset tables grouped,
|
adamc@234
|
55 Having : sql_exp grouped tables [] bool,
|
adamc@233
|
56 SelectFields : sql_subset grouped selectedFields,
|
adamc@233
|
57 SelectExps : $(fold (fn nm => fn t :: Type => fn acc =>
|
adamc@234
|
58 [nm] ~ acc => [nm = sql_exp grouped tables [] t] ++ acc) [] selectedExps) }
|
adamc@233
|
59 -> sql_query1 tables selectedFields selectedExps
|
adamc@229
|
60
|
adamc@229
|
61 type sql_relop
|
adamc@229
|
62 val sql_union : sql_relop
|
adamc@229
|
63 val sql_intersect : sql_relop
|
adamc@229
|
64 val sql_except : sql_relop
|
adamc@260
|
65 val sql_relop : tables1 ::: {{Type}}
|
adamc@229
|
66 -> tables2 ::: {{Type}}
|
adamc@233
|
67 -> selectedFields ::: {{Type}}
|
adamc@233
|
68 -> selectedExps ::: {Type}
|
adamc@260
|
69 -> sql_relop
|
adamc@233
|
70 -> sql_query1 tables1 selectedFields selectedExps
|
adamc@233
|
71 -> sql_query1 tables2 selectedFields selectedExps
|
adamc@233
|
72 -> sql_query1 selectedFields selectedFields selectedExps
|
adamc@229
|
73
|
adamc@230
|
74 type sql_direction
|
adamc@230
|
75 val sql_asc : sql_direction
|
adamc@230
|
76 val sql_desc : sql_direction
|
adamc@230
|
77
|
adamc@234
|
78 con sql_order_by :: {{Type}} -> {Type} -> Type
|
adamc@234
|
79 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
|
adamc@234
|
80 val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
|
adamc@268
|
81 -> sql_exp tables [] exps t -> sql_direction -> sql_order_by tables exps
|
adamc@234
|
82 -> sql_order_by tables exps
|
adamc@230
|
83
|
adamc@231
|
84 type sql_limit
|
adamc@231
|
85 val sql_no_limit : sql_limit
|
adamc@231
|
86 val sql_limit : int -> sql_limit
|
adamc@231
|
87
|
adamc@232
|
88 type sql_offset
|
adamc@232
|
89 val sql_no_offset : sql_offset
|
adamc@232
|
90 val sql_offset : int -> sql_offset
|
adamc@232
|
91
|
adamc@229
|
92 val sql_query : tables ::: {{Type}}
|
adamc@233
|
93 -> selectedFields ::: {{Type}}
|
adamc@233
|
94 -> selectedExps ::: {Type}
|
adamc@233
|
95 -> {Rows : sql_query1 tables selectedFields selectedExps,
|
adamc@234
|
96 OrderBy : sql_order_by tables selectedExps,
|
adamc@232
|
97 Limit : sql_limit,
|
adamc@232
|
98 Offset : sql_offset}
|
adamc@233
|
99 -> sql_query selectedFields selectedExps
|
adamc@204
|
100
|
adamc@225
|
101 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} -> fieldType ::: Type -> agg ::: {{Type}}
|
adamc@234
|
102 -> exps ::: {Type}
|
adamc@221
|
103 -> tab :: Name -> field :: Name
|
adamc@234
|
104 -> sql_exp ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) agg exps fieldType
|
adamc@234
|
105
|
adamc@234
|
106 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type} -> nm :: Name
|
adamc@234
|
107 -> sql_exp tabs agg ([nm = t] ++ rest) t
|
adamc@209
|
108
|
adamc@221
|
109 class sql_injectable
|
adamc@221
|
110 val sql_bool : sql_injectable bool
|
adamc@221
|
111 val sql_int : sql_injectable int
|
adamc@221
|
112 val sql_float : sql_injectable float
|
adamc@221
|
113 val sql_string : sql_injectable string
|
adamc@234
|
114 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
|
adamc@234
|
115 -> sql_injectable t -> t -> sql_exp tables agg exps t
|
adamc@209
|
116
|
adamc@220
|
117 con sql_unary :: Type -> Type -> Type
|
adamc@220
|
118 val sql_not : sql_unary bool bool
|
adamc@234
|
119 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> arg ::: Type -> res ::: Type
|
adamc@234
|
120 -> sql_unary arg res -> sql_exp tables agg exps arg -> sql_exp tables agg exps res
|
adamc@220
|
121
|
adamc@220
|
122 con sql_binary :: Type -> Type -> Type -> Type
|
adamc@220
|
123 val sql_and : sql_binary bool bool bool
|
adamc@220
|
124 val sql_or : sql_binary bool bool bool
|
adamc@234
|
125 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
adamc@234
|
126 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
|
adamc@234
|
127 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1 -> sql_exp tables agg exps arg2
|
adamc@234
|
128 -> sql_exp tables agg exps res
|
adamc@220
|
129
|
adamc@219
|
130 type sql_comparison
|
adamc@219
|
131 val sql_eq : sql_comparison
|
adamc@219
|
132 val sql_ne : sql_comparison
|
adamc@219
|
133 val sql_lt : sql_comparison
|
adamc@219
|
134 val sql_le : sql_comparison
|
adamc@219
|
135 val sql_gt : sql_comparison
|
adamc@219
|
136 val sql_ge : sql_comparison
|
adamc@253
|
137 val sql_comparison : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
adamc@236
|
138 -> t ::: Type
|
adamc@253
|
139 -> sql_comparison
|
adamc@234
|
140 -> sql_exp tables agg exps t -> sql_exp tables agg exps t
|
adamc@234
|
141 -> sql_exp tables agg exps bool
|
adamc@203
|
142
|
adamc@235
|
143 val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
|
adamc@235
|
144 -> unit -> sql_exp tables agg exps int
|
adamc@235
|
145
|
adamc@236
|
146 con sql_aggregate :: Type -> Type
|
adamc@236
|
147 val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
|
adamc@236
|
148 -> sql_aggregate t -> sql_exp agg agg exps t -> sql_exp tables agg exps t
|
adamc@236
|
149
|
adamc@236
|
150 class sql_summable
|
adamc@236
|
151 val sql_summable_int : sql_summable int
|
adamc@236
|
152 val sql_summable_float : sql_summable float
|
adamc@236
|
153 val sql_avg : t ::: Type -> sql_summable t -> sql_aggregate t
|
adamc@236
|
154 val sql_sum : t ::: Type -> sql_summable t -> sql_aggregate t
|
adamc@236
|
155
|
adamc@236
|
156 class sql_maxable
|
adamc@236
|
157 val sql_maxable_int : sql_maxable int
|
adamc@236
|
158 val sql_maxable_float : sql_maxable float
|
adamc@236
|
159 val sql_maxable_string : sql_maxable string
|
adamc@236
|
160 val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t
|
adamc@236
|
161 val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t
|
adamc@236
|
162
|
adamc@235
|
163
|
adamc@243
|
164 (*** Executing queries *)
|
adamc@243
|
165
|
adamc@243
|
166 con transaction :: Type -> Type
|
adamc@243
|
167 val return : t ::: Type
|
adamc@243
|
168 -> t -> transaction t
|
adamc@243
|
169 val bind : t1 ::: Type -> t2 ::: Type
|
adamc@243
|
170 -> transaction t1 -> (t1 -> transaction t2)
|
adamc@243
|
171 -> transaction t2
|
adamc@243
|
172
|
adamc@251
|
173 val query : tables ::: {{Type}} -> exps ::: {Type} -> tables ~ exps
|
adamc@252
|
174 -> state ::: Type
|
adamc@243
|
175 -> sql_query tables exps
|
adamc@251
|
176 -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
|
adamc@243
|
177 -> state
|
adamc@243
|
178 -> transaction state)
|
adamc@243
|
179 -> state
|
adamc@243
|
180 -> transaction state
|
adamc@243
|
181
|
adamc@243
|
182
|
adamc@203
|
183 (** XML *)
|
adamc@203
|
184
|
adamc@139
|
185 con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
|
adamc@91
|
186
|
adamc@91
|
187
|
adamc@139
|
188 con xml :: {Unit} -> {Type} -> {Type} -> Type
|
adamc@141
|
189 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
|
adamc@104
|
190 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type} -> attrsGiven ~ attrsAbsent
|
adamc@139
|
191 -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
|
adamc@139
|
192 -> useOuter ::: {Type} -> useInner ::: {Type} -> useOuter ~ useInner
|
adamc@139
|
193 -> bindOuter ::: {Type} -> bindInner ::: {Type} -> bindOuter ~ bindInner
|
adamc@104
|
194 -> $attrsGiven
|
adamc@139
|
195 -> tag (attrsGiven ++ attrsAbsent) ctxOuter ctxInner useOuter bindOuter
|
adamc@139
|
196 -> xml ctxInner useInner bindInner
|
adamc@139
|
197 -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
|
adamc@140
|
198 val join : ctx ::: {Unit}
|
adamc@139
|
199 -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
|
adamc@139
|
200 -> use1 ~ bind1 -> bind1 ~ bind2
|
adamc@140
|
201 -> xml ctx use1 bind1
|
adamc@140
|
202 -> xml ctx (use1 ++ bind1) bind2
|
adamc@140
|
203 -> xml ctx use1 (bind1 ++ bind2)
|
adamc@148
|
204 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type} -> bind ::: {Type}
|
adamc@148
|
205 -> use1 ~ use2
|
adamc@148
|
206 -> xml ctx use1 bind
|
adamc@148
|
207 -> xml ctx (use1 ++ use2) bind
|
adamc@91
|
208
|
adamc@110
|
209 con xhtml = xml [Html]
|
adamc@139
|
210 con page = xhtml [] []
|
adamc@110
|
211
|
adamc@204
|
212 (*** HTML details *)
|
adamc@204
|
213
|
adamc@140
|
214 con html = [Html]
|
adamc@140
|
215 con head = [Head]
|
adamc@140
|
216 con body = [Body]
|
adamc@141
|
217 con lform = [Body, LForm]
|
adamc@93
|
218
|
adamc@140
|
219 val head : unit -> tag [] html head [] []
|
adamc@140
|
220 val title : unit -> tag [] head [] [] []
|
adamc@110
|
221
|
adamc@140
|
222 val body : unit -> tag [] html body [] []
|
adamc@140
|
223 con bodyTag = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx -> unit
|
adamc@140
|
224 -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
|
adamc@141
|
225 con bodyTagStandalone = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx -> unit
|
adamc@141
|
226 -> tag attrs ([Body] ++ ctx) [] [] []
|
adamc@141
|
227
|
adamc@141
|
228 val br : bodyTagStandalone []
|
adamc@119
|
229
|
adamc@140
|
230 val p : bodyTag []
|
adamc@140
|
231 val b : bodyTag []
|
adamc@140
|
232 val i : bodyTag []
|
adamc@140
|
233 val font : bodyTag [Size = int, Face = string]
|
adamc@140
|
234
|
adamc@140
|
235 val h1 : bodyTag []
|
adamc@140
|
236 val li : bodyTag []
|
adamc@140
|
237
|
adamc@280
|
238 val a : bodyTag [Link = transaction page]
|
adamc@140
|
239
|
adamc@141
|
240 val lform : ctx ::: {Unit} -> [Body] ~ ctx -> bind ::: {Type}
|
adamc@141
|
241 -> xml lform [] bind
|
adamc@141
|
242 -> xml ([Body] ++ ctx) [] []
|
adamc@153
|
243 con lformTag = fn ty :: Type => fn inner :: {Unit} => fn attrs :: {Type} =>
|
adamc@141
|
244 ctx ::: {Unit} -> [LForm] ~ ctx
|
adamc@141
|
245 -> nm :: Name -> unit
|
adamc@153
|
246 -> tag attrs ([LForm] ++ ctx) inner [] [nm = ty]
|
adamc@153
|
247 val textbox : lformTag string [] []
|
adamc@155
|
248 val password : lformTag string [] []
|
adamc@153
|
249 val ltextarea : lformTag string [] []
|
adamc@153
|
250
|
adamc@190
|
251 val checkbox : lformTag bool [] []
|
adamc@190
|
252
|
adamc@153
|
253 con radio = [Body, Radio]
|
adamc@153
|
254 val radio : lformTag string radio []
|
adamc@153
|
255 val radioOption : unit -> tag [Value = string] radio [] [] []
|
adamc@142
|
256
|
adamc@154
|
257 con select = [Select]
|
adamc@154
|
258 val lselect : lformTag string select []
|
adamc@154
|
259 val loption : unit -> tag [Value = string] select [] [] []
|
adamc@154
|
260
|
adamc@142
|
261 val submit : ctx ::: {Unit} -> [LForm] ~ ctx
|
adamc@142
|
262 -> use ::: {Type} -> unit
|
adamc@280
|
263 -> tag [Action = $use -> transaction page] ([LForm] ++ ctx) ([LForm] ++ ctx) use []
|
adamc@283
|
264
|
adamc@283
|
265
|
adamc@283
|
266 (** Aborting *)
|
adamc@283
|
267
|
adamc@283
|
268 val error : t ::: Type -> xml [Body] [] [] -> t
|