Mercurial > urweb
changeset 1768:a613cae954ca
Some standard library additions from Edward Z. Yang
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sat, 19 May 2012 11:32:12 -0400 |
| parents | 92cfc69419bd |
| children | b042c50de57c |
| files | lib/ur/list.ur lib/ur/list.urs lib/ur/monad.ur lib/ur/monad.urs tests/monad.urp tests/monadTest.ur |
| diffstat | 6 files changed, 35 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/list.ur Thu May 17 10:20:24 2012 -0400 +++ b/lib/ur/list.ur Sat May 19 11:32:12 2012 -0400 @@ -424,3 +424,16 @@ fun splitAt [a] (n : int) (xs : list a) : list a * list a = (take n xs, drop n xs) + +fun mapXiM [m ::: Type -> Type] (_ : monad m) [a] [ctx ::: {Unit}] (f : int -> a -> m (xml ctx [] [])) : t a -> m (xml ctx [] []) = + let + fun mapXiM' i ls = + case ls of + [] => return <xml/> + | x :: ls => + this <- f i x; + rest <- mapXiM' (i+1) ls; + return <xml>{this}{rest}</xml> + in + mapXiM' 0 + end
--- a/lib/ur/list.urs Thu May 17 10:20:24 2012 -0400 +++ b/lib/ur/list.urs Sat May 19 11:32:12 2012 -0400 @@ -36,6 +36,8 @@ val mapXM : m ::: (Type -> Type) -> monad m -> a ::: Type -> ctx ::: {Unit} -> (a -> m (xml ctx [] [])) -> t a -> m (xml ctx [] []) +val mapXiM : m ::: (Type -> Type) -> monad m -> a ::: Type -> ctx ::: {Unit} -> (int -> a -> m (xml ctx [] [])) -> t a -> m (xml ctx [] []) + val filter : a ::: Type -> (a -> bool) -> t a -> t a val exists : a ::: Type -> (a -> bool) -> t a -> bool
--- a/lib/ur/monad.ur Thu May 17 10:20:24 2012 -0400 +++ b/lib/ur/monad.ur Sat May 19 11:32:12 2012 -0400 @@ -12,6 +12,8 @@ v <- m; return (f v) +val liftM = @@mp + fun foldR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: {K} -> Type] (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] => @@ -122,3 +124,8 @@ f [nm] [t] r1.nm r2.nm r3.nm) (fn _ _ _ => return ()) fl + +fun liftM2 [m ::: Type -> Type] (_ : monad m) [a] [b] [c] (f : a -> b -> c) (mx : m a) (my : m b) : m c = + x <- mx; + y <- my; + return (f x y)
--- a/lib/ur/monad.urs Thu May 17 10:20:24 2012 -0400 +++ b/lib/ur/monad.urs Sat May 19 11:32:12 2012 -0400 @@ -7,6 +7,13 @@ val mp : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> (a -> b) -> m a -> m b +val liftM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type + -> (a -> b) -> m a -> m b +(* Haskell-style synonym for [mp] *) + +val liftM2 : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> c ::: Type + -> (a -> b -> c) -> m a -> m b -> m c + val foldR : K --> m ::: (Type -> Type) -> monad m -> tf :: (K -> Type) -> tr :: ({K} -> Type)