# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1235501439 18000
# Node ID 6a6eb9882d57ae076bf8bd66fb77ebf50a0a35ed
# Parent  e68de2a5506b1a100841dc71168c4e60e8e0cb0f
Top.Fold.mp

diff -r e68de2a5506b -r 6a6eb9882d57 lib/ur/top.ur
--- a/lib/ur/top.ur	Tue Feb 24 13:46:08 2009 -0500
+++ b/lib/ur/top.ur	Tue Feb 24 13:50:39 2009 -0500
@@ -29,6 +29,17 @@
                             [[nm] ~ r1'] [[nm = v] ++ r1' ~ r2] =>
                f [nm] [v] [r1' ++ r2] acc !)
            (fn [[] ~ r2] => f2 [tf] f i) !
+
+    fun mp K1 K2 (f ::: K1 -> K2) (r ::: {K1})
+        (fold : folder r)
+        (tf :: {K2} -> Type)
+        (f : nm :: Name -> v :: K2 -> r :: {K2} -> tf r
+             -> [[nm] ~ r] => tf ([nm = v] ++ r))
+        (i : tf []) =
+        fold [fn r => tf (map f r)]
+        (fn (nm :: Name) (v :: K1) (rest :: {K1}) (acc : tf (map f rest)) [[nm] ~ rest] =>
+            f [nm] [f v] [map f rest] acc !)
+        i
 end
 
 
diff -r e68de2a5506b -r 6a6eb9882d57 lib/ur/top.urs
--- a/lib/ur/top.urs	Tue Feb 24 13:46:08 2009 -0500
+++ b/lib/ur/top.urs	Tue Feb 24 13:50:39 2009 -0500
@@ -12,6 +12,8 @@
                -> [[nm] ~ r] => folder r -> folder ([nm = v] ++ r)
     val concat : K --> r1 ::: {K} -> r2 ::: {K}
                  -> [r1 ~ r2] => folder r1 -> folder r2 -> folder (r1 ++ r2)
+    val mp : K1 --> K2 --> f ::: (K1 -> K2) -> r ::: {K1}
+             -> folder r -> folder (map f r)
 end