summaryrefslogtreecommitdiff
path: root/lib/basis.urs
blob: a095a57eb0a4e3b8e7f2fc3e92b9d55a194a1718 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
type int
type float
type string

type unit = {}

datatype bool = False | True

datatype option t = None | Some of t


(** Basic type classes *)

class eq
val eq : t ::: Type -> eq t -> t -> t -> bool
val ne : t ::: Type -> eq t -> t -> t -> bool
val eq_int : eq int
val eq_string : eq string
val eq_bool : eq bool


(** String operations *)

val strcat : string -> string -> string

class show
val show : t ::: Type -> show t -> t -> string
val show_int : show int
val show_float : show float
val show_string : show string
val show_bool : show bool

class read
val read : t ::: Type -> read t -> string -> option t
val readError : t ::: Type -> read t -> string -> t
(* [readError] calls [error] if the input is malformed. *)
val read_int : read int
val read_float : read float
val read_string : read string
val read_bool : read bool


(** SQL *)

con sql_table :: {Type} -> Type

(*** Queries *)

con sql_query :: {{Type}} -> {Type} -> Type
con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type
con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type

con sql_subset :: {{Type}} -> {{Type}} -> Type
val sql_subset : keep_drop :: {({Type} * {Type})}
        -> sql_subset
                (fold (fn nm => fn fields :: ({Type} * {Type}) => fn acc =>
                        [nm] ~ acc => fields.1 ~ fields.2 =>
                        [nm = fields.1 ++ fields.2] ++ acc) [] keep_drop)
                (fold (fn nm => fn fields :: ({Type} * {Type}) => fn acc =>
                        [nm] ~ acc =>
                        [nm = fields.1] ++ acc) [] keep_drop)
val sql_subset_all : tables :: {{Type}}
        -> sql_subset tables tables

val sql_query1 : tables ::: {{Type}}
        -> grouped ::: {{Type}}
        -> selectedFields ::: {{Type}}
        -> selectedExps ::: {Type}
        -> {From : $(fold (fn nm => fn fields :: {Type} => fn acc =>
                [nm] ~ acc => [nm = sql_table fields] ++ acc) [] tables),
            Where : sql_exp tables [] [] bool,
            GroupBy : sql_subset tables grouped,
            Having : sql_exp grouped tables [] bool,
            SelectFields : sql_subset grouped selectedFields,
            SelectExps : $(fold (fn nm => fn t :: Type => fn acc =>
                [nm] ~ acc => [nm = sql_exp grouped tables [] t] ++ acc) [] selectedExps) }
        -> sql_query1 tables selectedFields selectedExps

type sql_relop 
val sql_union : sql_relop
val sql_intersect : sql_relop
val sql_except : sql_relop
val sql_relop : tables1 ::: {{Type}}
        -> tables2 ::: {{Type}}
        -> selectedFields ::: {{Type}}
        -> selectedExps ::: {Type}
        -> sql_relop
        -> sql_query1 tables1 selectedFields selectedExps
        -> sql_query1 tables2 selectedFields selectedExps
        -> sql_query1 selectedFields selectedFields selectedExps

type sql_direction
val sql_asc : sql_direction
val sql_desc : sql_direction

con sql_order_by :: {{Type}} -> {Type} -> Type
val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
        -> sql_exp tables [] exps t -> sql_direction -> sql_order_by tables exps
        -> sql_order_by tables exps

type sql_limit
val sql_no_limit : sql_limit
val sql_limit : int -> sql_limit

type sql_offset
val sql_no_offset : sql_offset
val sql_offset : int -> sql_offset

val sql_query : tables ::: {{Type}}
        -> selectedFields ::: {{Type}}
        -> selectedExps ::: {Type}
        -> {Rows : sql_query1 tables selectedFields selectedExps,
            OrderBy : sql_order_by tables selectedExps,
            Limit : sql_limit,
            Offset : sql_offset}
        -> sql_query selectedFields selectedExps

val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} -> fieldType ::: Type -> agg ::: {{Type}}
        -> exps ::: {Type}
        -> tab :: Name -> field :: Name
        -> sql_exp ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) agg exps fieldType

val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type} -> nm :: Name
        -> sql_exp tabs agg ([nm = t] ++ rest) t

class sql_injectable
val sql_bool : sql_injectable bool
val sql_int : sql_injectable int
val sql_float : sql_injectable float
val sql_string : sql_injectable string
val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
        -> sql_injectable t -> t -> sql_exp tables agg exps t

con sql_unary :: Type -> Type -> Type
val sql_not : sql_unary bool bool
val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> arg ::: Type -> res ::: Type
        -> sql_unary arg res -> sql_exp tables agg exps arg -> sql_exp tables agg exps res

con sql_binary :: Type -> Type -> Type -> Type
val sql_and : sql_binary bool bool bool
val sql_or : sql_binary bool bool bool
val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
        -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
        -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1 -> sql_exp tables agg exps arg2
        -> sql_exp tables agg exps res

type sql_comparison
val sql_eq : sql_comparison
val sql_ne : sql_comparison
val sql_lt : sql_comparison
val sql_le : sql_comparison
val sql_gt : sql_comparison
val sql_ge : sql_comparison
val sql_comparison : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
        -> t ::: Type
        -> sql_comparison
        -> sql_exp tables agg exps t -> sql_exp tables agg exps t
        -> sql_exp tables agg exps bool

val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
        -> unit -> sql_exp tables agg exps int

con sql_aggregate :: Type -> Type
val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type
        -> sql_aggregate t -> sql_exp agg agg exps t -> sql_exp tables agg exps t

class sql_summable
val sql_summable_int : sql_summable int
val sql_summable_float : sql_summable float
val sql_avg : t ::: Type -> sql_summable t -> sql_aggregate t
val sql_sum : t ::: Type -> sql_summable t -> sql_aggregate t

class sql_maxable
val sql_maxable_int : sql_maxable int
val sql_maxable_float : sql_maxable float
val sql_maxable_string : sql_maxable string
val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t
val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t


(*** Executing queries *)

con transaction :: Type -> Type
val return : t ::: Type
        -> t -> transaction t
val bind : t1 ::: Type -> t2 ::: Type
        -> transaction t1 -> (t1 -> transaction t2)
        -> transaction t2

val query : tables ::: {{Type}} -> exps ::: {Type} -> tables ~ exps
        -> state ::: Type
        -> sql_query tables exps
        -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
                -> state
                -> transaction state)
        -> state
        -> transaction state


(*** Database mutators *)

type dml
val dml : dml -> transaction unit

val insert : fields ::: {Type}
        -> sql_table fields
        -> $(fold (fn nm (t :: Type) acc => [nm] ~ acc =>
                [nm = sql_exp [T = fields] [] [] t] ++ acc) [] fields)
        -> dml

val update : changed ::: {Type} -> unchanged ::: {Type} -> changed ~ unchanged
        -> $(fold (fn nm (t :: Type) acc => [nm] ~ acc =>
                [nm = sql_exp [T = changed ++ unchanged] [] [] t] ++ acc) [] changed)
        -> sql_table (changed ++ unchanged)
        -> sql_exp [T = changed ++ unchanged] [] [] bool
        -> dml

val delete : fields ::: {Type}
        -> sql_table fields
        -> sql_exp [T = fields] [] [] bool
        -> dml


(** XML *)

con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type


con xml :: {Unit} -> {Type} -> {Type} -> Type
val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type} -> attrsGiven ~ attrsAbsent
        -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
        -> useOuter ::: {Type} -> useInner ::: {Type} -> useOuter ~ useInner
        -> bindOuter ::: {Type} -> bindInner ::: {Type} -> bindOuter ~ bindInner
        -> $attrsGiven
        -> tag (attrsGiven ++ attrsAbsent) ctxOuter ctxInner useOuter bindOuter
        -> xml ctxInner useInner bindInner
        -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
val join : ctx ::: {Unit} 
        -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
        -> use1 ~ bind1 -> bind1 ~ bind2
        -> xml ctx use1 bind1
        -> xml ctx (use1 ++ bind1) bind2
        -> xml ctx use1 (bind1 ++ bind2)
val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type} -> bind ::: {Type}
        -> use1 ~ use2
        -> xml ctx use1 bind
        -> xml ctx (use1 ++ use2) bind

con xhtml = xml [Html]
con page = xhtml [] []

(*** HTML details *)

con html = [Html]
con head = [Head]
con body = [Body]
con lform = [Body, LForm]

val head : unit -> tag [] html head [] []
val title : unit -> tag [] head [] [] []

val body : unit -> tag [] html body [] []
con bodyTag = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx -> unit
        -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
con bodyTagStandalone = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx -> unit
        -> tag attrs ([Body] ++ ctx) [] [] []

val br : bodyTagStandalone []

val p : bodyTag []
val b : bodyTag []
val i : bodyTag []
val font : bodyTag [Size = int, Face = string]

val h1 : bodyTag []
val li : bodyTag []

val a : bodyTag [Link = transaction page]

val lform : ctx ::: {Unit} -> [Body] ~ ctx -> bind ::: {Type}
        -> xml lform [] bind
        -> xml ([Body] ++ ctx) [] []
con lformTag = fn ty :: Type => fn inner :: {Unit} => fn attrs :: {Type} =>
        ctx ::: {Unit} -> [LForm] ~ ctx
        -> nm :: Name -> unit
        -> tag attrs ([LForm] ++ ctx) inner [] [nm = ty]
val textbox : lformTag string [] []
val password : lformTag string [] []
val ltextarea : lformTag string [] []

val checkbox : lformTag bool [] []

con radio = [Body, Radio]
val radio : lformTag string radio []
val radioOption : unit -> tag [Value = string] radio [] [] []

con select = [Select]
val lselect : lformTag string select []
val loption : unit -> tag [Value = string] select [] [] []

val submit : ctx ::: {Unit} -> [LForm] ~ ctx
        -> use ::: {Type} -> unit
        -> tag [Action = $use -> transaction page] ([LForm] ++ ctx) ([LForm] ++ ctx) use []


(** Aborting *)

val error : t ::: Type -> xml [Body] [] [] -> t