comparison lib/top.ur @ 471:20fab0e96217

Tree demo working (and other assorted regressions fixed)
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 19:43:48 -0500
parents 7cb418e9714f
children 5d494183ca89
comparison
equal deleted inserted replaced
470:7cb418e9714f 471:20fab0e96217
228 228
229 fun eqNullable (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type}) 229 fun eqNullable (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type})
230 (t ::: Type) (_ : sql_injectable (option t)) 230 (t ::: Type) (_ : sql_injectable (option t))
231 (e1 : sql_exp tables agg exps (option t)) 231 (e1 : sql_exp tables agg exps (option t))
232 (e2 : sql_exp tables agg exps (option t)) = 232 (e2 : sql_exp tables agg exps (option t)) =
233 (SQL ({[e1]} IS NULL AND {[e2]} IS NULL) OR {[e1]} = {[e2]}) 233 (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2})
234 234
235 fun eqNullable' (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type}) 235 fun eqNullable' (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type})
236 (t ::: Type) (inj : sql_injectable (option t)) 236 (t ::: Type) (inj : sql_injectable (option t))
237 (e1 : sql_exp tables agg exps (option t)) 237 (e1 : sql_exp tables agg exps (option t))
238 (e2 : option t) = 238 (e2 : option t) =
239 case e2 of 239 case e2 of
240 None => (SQL {[e1]} IS NULL) 240 None => (SQL {e1} IS NULL)
241 | Some _ => sql_comparison sql_eq e1 (@sql_inject inj e2) 241 | Some _ => sql_comparison sql_eq e1 (@sql_inject inj e2)