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