Mercurial > urweb

comparison lib/basis.urs @ 244:71bafe66dbe1

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