blob: b85587bb429f73974bfe3efe1f18a4fcabef630c (
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
|
type int
type float
type string
type unit = {}
datatype bool = False | True
(** SQL *)
con sql_table :: {Type} -> Type
(*** Queries *)
con sql_query :: {{Type}} -> Type
con sql_query1 :: {{Type}} -> {{Type}} -> Type
con sql_exp :: {{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}}
-> selected ::: {{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 selected}
-> sql_query1 tables selected
type sql_relop
val sql_union : sql_relop
val sql_intersect : sql_relop
val sql_except : sql_relop
val sql_relop : sql_relop
-> tables1 ::: {{Type}}
-> tables2 ::: {{Type}}
-> selected ::: {{Type}}
-> sql_query1 tables1 selected -> sql_query1 tables2 selected -> sql_query1 selected selected
type sql_direction
val sql_asc : sql_direction
val sql_desc : sql_direction
con sql_order_by :: {{Type}} -> Type
val sql_order_by_Nil : tables :: {{Type}} -> sql_order_by tables
val sql_order_by_Cons : tables ::: {{Type}} -> t ::: Type
-> sql_exp tables [] t -> sql_order_by tables
-> sql_order_by tables
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}}
-> selected ::: {{Type}}
-> {Rows : sql_query1 tables selected,
OrderBy : sql_order_by tables,
Limit : sql_limit,
Offset : sql_offset}
-> sql_query selected
val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} -> fieldType ::: Type -> agg ::: {{Type}}
-> tab :: Name -> field :: Name
-> sql_exp ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) agg fieldType
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}} -> t ::: Type -> t -> sql_injectable t -> sql_exp tables agg t
con sql_unary :: Type -> Type -> Type
val sql_not : sql_unary bool bool
val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> arg ::: Type -> res ::: Type
-> sql_unary arg res -> sql_exp tables agg arg -> sql_exp tables agg 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}} -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
-> sql_binary arg1 arg2 res -> sql_exp tables agg arg1 -> sql_exp tables agg arg2 -> sql_exp tables agg 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 : sql_comparison
-> tables ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> sql_exp tables agg t -> sql_exp tables agg t
-> sql_injectable t -> sql_exp tables agg bool
(** 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 = 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 -> page] ([LForm] ++ ctx) ([LForm] ++ ctx) use []
|
