Mercurial > urweb
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) |