Mercurial > urweb
comparison lib/ur/basis.urs @ 678:5ff1ff38e2db
Preliminary work supporting channels in databases
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 26 Mar 2009 16:22:34 -0400 |
parents | e0c186464612 |
children | 5bbb542243e8 |
comparison
equal
deleted
inserted
replaced
677:81573f62d6c3 | 678:5ff1ff38e2db |
---|---|
103 | 103 |
104 | 104 |
105 (** JavaScript-y gadgets *) | 105 (** JavaScript-y gadgets *) |
106 | 106 |
107 val alert : string -> transaction unit | 107 val alert : string -> transaction unit |
108 | |
109 | |
110 (** Channels *) | |
111 | |
112 con channel :: Type -> Type | |
113 val channel : t ::: Type -> transaction (channel t) | |
114 val subscribe : t ::: Type -> channel t -> transaction unit | |
115 val send : t ::: Type -> channel t -> t -> transaction unit | |
116 val recv : t ::: Type -> channel t -> transaction t | |
108 | 117 |
109 | 118 |
110 (** SQL *) | 119 (** SQL *) |
111 | 120 |
112 con sql_table :: {Type} -> Type | 121 con sql_table :: {Type} -> Type |
194 val sql_int : sql_injectable_prim int | 203 val sql_int : sql_injectable_prim int |
195 val sql_float : sql_injectable_prim float | 204 val sql_float : sql_injectable_prim float |
196 val sql_string : sql_injectable_prim string | 205 val sql_string : sql_injectable_prim string |
197 val sql_time : sql_injectable_prim time | 206 val sql_time : sql_injectable_prim time |
198 | 207 |
208 class sql_injectable_nullable | |
209 val sql_channel : t ::: Type -> sql_injectable_nullable (channel t) | |
210 | |
199 class sql_injectable | 211 class sql_injectable |
200 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t | 212 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t |
201 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t) | 213 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t) |
214 val sql_nullable : t ::: Type -> sql_injectable_nullable t -> sql_injectable (option t) | |
202 | 215 |
203 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} | 216 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} |
204 -> t ::: Type | 217 -> t ::: Type |
205 -> sql_injectable t -> t -> sql_exp tables agg exps t | 218 -> sql_injectable t -> t -> sql_exp tables agg exps t |
206 | 219 |
452 (** Aborting *) | 465 (** Aborting *) |
453 | 466 |
454 val error : t ::: Type -> xml [Body] [] [] -> t | 467 val error : t ::: Type -> xml [Body] [] [] -> t |
455 | 468 |
456 | 469 |
457 (** Channels *) | |
458 | |
459 con channel :: Type -> Type | |
460 val channel : t ::: Type -> transaction (channel t) | |
461 val subscribe : t ::: Type -> channel t -> transaction unit | |
462 val send : t ::: Type -> channel t -> t -> transaction unit | |
463 val recv : t ::: Type -> channel t -> transaction t |