blob: 8299f20027ee537dab3b4f54393e2d07714c9f73 (
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
|
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_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_query : 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 tables selected}
-> sql_query selected
val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} -> fieldType ::: Type
-> tab :: Name -> field :: Name
-> agg ::: {{Type}}
-> 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 []
|
