Mercurial > urweb

comparison lib/basis.urs @ 345:b85e6ba56618

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge CDisjoint and TDisjoint
author Adam Chlipala <adamc@hcoop.net>
date Sat, 04 Oct 2008 15:50:28 -0400
parents f55034419a07
children 58eeeb3cbf40
comparison
equal deleted inserted replaced
344:3c0feecd057d 345:b85e6ba56618
187 val bind : t1 ::: Type -> t2 ::: Type 187 val bind : t1 ::: Type -> t2 ::: Type
188 -> transaction t1 -> (t1 -> transaction t2) 188 -> transaction t1 -> (t1 -> transaction t2)
189 -> transaction t2 189 -> transaction t2
190 190
191 val query : tables ::: {{Type}} -> exps ::: {Type} -> tables ~ exps 191 val query : tables ::: {{Type}} -> exps ::: {Type} -> tables ~ exps
192 -> state ::: Type 192 => state ::: Type
193 -> sql_query tables exps 193 -> sql_query tables exps
194 -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables) 194 -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
195 -> state 195 -> state
196 -> transaction state) 196 -> transaction state)
197 -> state 197 -> state
208 -> $(fold (fn nm (t :: Type) acc => [nm] ~ acc => 208 -> $(fold (fn nm (t :: Type) acc => [nm] ~ acc =>
209 [nm = sql_exp [] [] [] t] ++ acc) [] fields) 209 [nm = sql_exp [] [] [] t] ++ acc) [] fields)
210 -> dml 210 -> dml
211 211
212 val update : changed :: {Type} -> unchanged ::: {Type} -> changed ~ unchanged 212 val update : changed :: {Type} -> unchanged ::: {Type} -> changed ~ unchanged
213 -> $(fold (fn nm (t :: Type) acc => [nm] ~ acc => 213 => $(fold (fn nm (t :: Type) acc => [nm] ~ acc =>
214 [nm = sql_exp [T = changed ++ unchanged] [] [] t] ++ acc) [] changed) 214 [nm = sql_exp [T = changed ++ unchanged] [] [] t] ++ acc) [] changed)
215 -> sql_table (changed ++ unchanged) 215 -> sql_table (changed ++ unchanged)
216 -> sql_exp [T = changed ++ unchanged] [] [] bool 216 -> sql_exp [T = changed ++ unchanged] [] [] bool
217 -> dml 217 -> dml
218 218
233 233
234 234
235 con xml :: {Unit} -> {Type} -> {Type} -> Type 235 con xml :: {Unit} -> {Type} -> {Type} -> Type
236 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use [] 236 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
237 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type} -> attrsGiven ~ attrsAbsent 237 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type} -> attrsGiven ~ attrsAbsent
238 -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit} 238 => ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
239 -> useOuter ::: {Type} -> useInner ::: {Type} -> useOuter ~ useInner 239 -> useOuter ::: {Type} -> useInner ::: {Type} -> useOuter ~ useInner
240 -> bindOuter ::: {Type} -> bindInner ::: {Type} -> bindOuter ~ bindInner 240 => bindOuter ::: {Type} -> bindInner ::: {Type} -> bindOuter ~ bindInner
241 -> $attrsGiven 241 => $attrsGiven
242 -> tag (attrsGiven ++ attrsAbsent) ctxOuter ctxInner useOuter bindOuter 242 -> tag (attrsGiven ++ attrsAbsent) ctxOuter ctxInner useOuter bindOuter
243 -> xml ctxInner useInner bindInner 243 -> xml ctxInner useInner bindInner
244 -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner) 244 -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
245 val join : ctx ::: {Unit} 245 val join : ctx ::: {Unit}
246 -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type} 246 -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
247 -> use1 ~ bind1 -> bind1 ~ bind2 247 -> use1 ~ bind1 => bind1 ~ bind2
248 -> xml ctx use1 bind1 248 => xml ctx use1 bind1
249 -> xml ctx (use1 ++ bind1) bind2 249 -> xml ctx (use1 ++ bind1) bind2
250 -> xml ctx use1 (bind1 ++ bind2) 250 -> xml ctx use1 (bind1 ++ bind2)
251 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type} -> bind ::: {Type} 251 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type} -> bind ::: {Type}
252 -> use1 ~ use2 252 -> use1 ~ use2
253 -> xml ctx use1 bind 253 => xml ctx use1 bind
254 -> xml ctx (use1 ++ use2) bind 254 -> xml ctx (use1 ++ use2) bind
255 255
256 con xhtml = xml [Html] 256 con xhtml = xml [Html]
257 con page = xhtml [] [] 257 con page = xhtml [] []
258 con xbody = xml [Body] [] [] 258 con xbody = xml [Body] [] []
270 270
271 val head : unit -> tag [] html head [] [] 271 val head : unit -> tag [] html head [] []
272 val title : unit -> tag [] head [] [] [] 272 val title : unit -> tag [] head [] [] []
273 273
274 val body : unit -> tag [] html body [] [] 274 val body : unit -> tag [] html body [] []
275 con bodyTag = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx -> unit 275 con bodyTag = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx => unit
276 -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] [] 276 -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
277 con bodyTagStandalone = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx -> unit 277 con bodyTagStandalone = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx => unit
278 -> tag attrs ([Body] ++ ctx) [] [] [] 278 -> tag attrs ([Body] ++ ctx) [] [] []
279 279
280 val br : bodyTagStandalone [] 280 val br : bodyTagStandalone []
281 281
282 val p : bodyTag [] 282 val p : bodyTag []
287 val h1 : bodyTag [] 287 val h1 : bodyTag []
288 val li : bodyTag [] 288 val li : bodyTag []
289 289
290 val a : bodyTag [Link = transaction page] 290 val a : bodyTag [Link = transaction page]
291 291
292 val lform : ctx ::: {Unit} -> [Body] ~ ctx -> bind ::: {Type} 292 val lform : ctx ::: {Unit} -> [Body] ~ ctx => bind ::: {Type}
293 -> xml form [] bind 293 -> xml form [] bind
294 -> xml ([Body] ++ ctx) [] [] 294 -> xml ([Body] ++ ctx) [] []
295 con lformTag = fn ty :: Type => fn inner :: {Unit} => fn attrs :: {Type} => 295 con lformTag = fn ty :: Type => fn inner :: {Unit} => fn attrs :: {Type} =>
296 ctx ::: {Unit} -> [LForm] ~ ctx 296 ctx ::: {Unit} -> [LForm] ~ ctx
297 -> nm :: Name -> unit 297 => nm :: Name -> unit
298 -> tag attrs ([LForm] ++ ctx) inner [] [nm = ty] 298 -> tag attrs ([LForm] ++ ctx) inner [] [nm = ty]
299 val textbox : lformTag string [] [Value = string] 299 val textbox : lformTag string [] [Value = string]
300 val password : lformTag string [] [] 300 val password : lformTag string [] []
301 val ltextarea : lformTag string [] [] 301 val ltextarea : lformTag string [] []
302 302
309 con select = [Select] 309 con select = [Select]
310 val lselect : lformTag string select [] 310 val lselect : lformTag string select []
311 val loption : unit -> tag [Value = string] select [] [] [] 311 val loption : unit -> tag [Value = string] select [] [] []
312 312
313 val submit : ctx ::: {Unit} -> [LForm] ~ ctx 313 val submit : ctx ::: {Unit} -> [LForm] ~ ctx
314 -> use ::: {Type} -> unit 314 => use ::: {Type} -> unit
315 -> tag [Action = $use -> transaction page] ([LForm] ++ ctx) ([LForm] ++ ctx) use [] 315 -> tag [Action = $use -> transaction page] ([LForm] ++ ctx) ([LForm] ++ ctx) use []
316 316
317 (*** Tables *) 317 (*** Tables *)
318 318
319 val tabl : unit -> tag [Border = int] [Body] [Body, Table] [] [] 319 val tabl : unit -> tag [Border = int] [Body] [Body, Table] [] []