Mercurial > urweb
diff lib/ur/monad.ur @ 937:37dd42935dad
Summary row with aggregates
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 15 Sep 2009 10:18:56 -0400 |
parents | 321a2d6feb40 |
children | 8d3aa6c7cee0 |
line wrap: on
line diff
--- a/lib/ur/monad.ur Tue Sep 15 09:45:46 2009 -0400 +++ b/lib/ur/monad.ur Tue Sep 15 10:18:56 2009 -0400 @@ -59,3 +59,12 @@ v' <- f [nm] [t] v; return (acc ++ {nm = v'})) {} + +fun mapR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: K -> Type] + (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t)) = + @@foldR2 [m] _ [tf1] [tf2] [fn r => $(map tr r)] + (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v1 : tf1 t) (v2 : tf2 t) + (acc : $(map tr rest)) => + v' <- f [nm] [t] v1 v2; + return (acc ++ {nm = v'})) + {}