diff lib/ur/monad.ur @ 1172:ad15700272f6

Changing foldRX to mapX
author Adam Chlipala <adamc@hcoop.net>
date Sun, 28 Feb 2010 13:06:10 -0500
parents 8d3aa6c7cee0
children 79f487f51d9f
line wrap: on
line diff
--- a/lib/ur/monad.ur	Sat Feb 27 16:49:11 2010 -0500
+++ b/lib/ur/monad.ur	Sun Feb 28 13:06:10 2010 -0500
@@ -51,6 +51,16 @@
      (fn _ _ _ => return i)
      fl
 
+fun mapR0 [K] [m] (_ : monad m) [tr :: K -> Type]
+         (f : nm :: Name -> t :: K -> m (tr t)) [r ::: {K}] (fl : folder r) =
+    @Top.fold [fn r => m ($(map tr r))]
+    (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : m ($(map tr rest))) =>
+        v <- f [nm] [t];
+        vs <- acc;
+        return (vs ++ {nm = v}))
+    (return {})
+    fl
+
 fun mapR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: K -> Type]
          (f : nm :: Name -> t :: K -> tf t -> m (tr t)) =
     @@foldR [m] _ [tf] [fn r => $(map tr r)]