Mercurial > urweb

comparison lib/top.ur @ 564:803b2f3bb86b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Monad type class seems to be working
author Adam Chlipala <adamc@hcoop.net>
date Fri, 19 Dec 2008 10:27:58 -0500
parents 5d494183ca89
children
comparison
equal deleted inserted replaced
563:44958d74c43f 564:803b2f3bb86b
28 f [choice] body 28 f [choice] body
29 29
30 fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) 30 fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type)
31 (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x) 31 (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x)
32 32
33 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) = 33 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) =
34 cdata (@show sh v) 34 cdata (show v)
35 35
36 fun foldUR (tf :: Type) (tr :: {Unit} -> Type) 36 fun foldUR (tf :: Type) (tr :: {Unit} -> Type)
37 (f : nm :: Name -> rest :: {Unit} 37 (f : nm :: Name -> rest :: {Unit}
38 -> fn [[nm] ~ rest] => 38 -> fn [[nm] ~ rest] =>
39 tf -> tr rest -> tr ([nm] ++ rest)) 39 tf -> tr rest -> tr ([nm] ++ rest))
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) (_ : 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_binary sql_eq e1 (@sql_inject inj e2) 241 | Some _ => sql_binary sql_eq e1 (sql_inject e2)