comparison lib/ur/basis.urs @ 683:9a2c18dab11d

Expunging non-nullable rows
author Adam Chlipala <adamc@hcoop.net>
date Sun, 29 Mar 2009 13:30:01 -0400
parents 5bbb542243e8
children cc58941da3e2
comparison
equal deleted inserted replaced
682:5bbb542243e8 683:9a2c18dab11d
205 val sql_bool : sql_injectable_prim bool 205 val sql_bool : sql_injectable_prim bool
206 val sql_int : sql_injectable_prim int 206 val sql_int : sql_injectable_prim int
207 val sql_float : sql_injectable_prim float 207 val sql_float : sql_injectable_prim float
208 val sql_string : sql_injectable_prim string 208 val sql_string : sql_injectable_prim string
209 val sql_time : sql_injectable_prim time 209 val sql_time : sql_injectable_prim time
210 210 val sql_channel : t ::: Type -> sql_injectable_prim (channel t)
211 class sql_injectable_nullable 211 val sql_client : sql_injectable_prim client
212 val sql_channel : t ::: Type -> sql_injectable_nullable (channel t)
213 val sql_client : sql_injectable_nullable client
214 212
215 class sql_injectable 213 class sql_injectable
216 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t 214 val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t
217 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t) 215 val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)
218 val sql_nullable : t ::: Type -> sql_injectable_nullable t -> sql_injectable (option t)
219 216
220 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 217 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
221 -> t ::: Type 218 -> t ::: Type
222 -> sql_injectable t -> t -> sql_exp tables agg exps t 219 -> sql_injectable t -> t -> sql_exp tables agg exps t
223 220