# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1325543011 18000
# Node ID 296807a9fd50e4f7ccdc61d4277f4779acd5b4c9
# Parent  875221eee9879ac1cca67d951a4732069c747288
Variant.foldR and appR

diff -r 875221eee987 -r 296807a9fd50 variant.ur
--- a/variant.ur	Sat Dec 31 15:49:54 2011 -0500
+++ b/variant.ur	Mon Jan 02 17:23:31 2012 -0500
@@ -54,6 +54,17 @@
         f' (make [nm] {}) (acc [[nm] ++ r'] f' acc'))
     (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f
 
+fun foldR [tr] [r] [t] (fl : folder r) (f : variant (mapU {} r) -> tr -> t -> t) (record : $(mapU tr r)) : t -> t =
+    @Top.foldUR [tr] [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t]
+    (fn [nm :: Name] [r ::_] [[nm] ~ r] (v : tr)
+                     (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t)
+                     [r' ::_] [[nm] ++ r ~ r'] f' acc' =>
+        f' (make [nm] {}) v (acc [[nm] ++ r'] f' acc'))
+    (fn [r' ::_] [[] ~ r'] _ x => x) fl record [[]] ! f
+
+fun appR [m] (_ : monad m) [tr] [r] (fl : folder r) (f : variant (mapU {} r) -> tr -> m {}) (record : $(mapU tr r)) : m {} =
+    @foldR fl (fn var this acc => f var this; acc) record (return ())
+
 fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type]
     (f : p :: K -> f p -> fr p -> t)
     [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t =
@@ -66,7 +77,7 @@
     (f : p :: K -> f1 p -> f2 p -> fr p -> t)
     [r ::: {K}] (fl : folder r) (v1 : variant (map f1 r)) (v2 : variant (map f2 r)) (r : $(map fr r)) : option t =
     match v1
-    (@foldR [fr] [fn r => others :: {K} -> [others ~ r] =>
+    (@Top.foldR [fr] [fn r => others :: {K} -> [others ~ r] =>
                      folder (r ++ others)
                      -> variant (map f2 (r ++ others))
                      -> $(map (fn p => f1 p -> option t) r)]
diff -r 875221eee987 -r 296807a9fd50 variant.urs
--- a/variant.urs	Sat Dec 31 15:49:54 2011 -0500
+++ b/variant.urs	Mon Jan 02 17:23:31 2012 -0500
@@ -24,6 +24,11 @@
 
 val fold : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t -> t) -> t -> t
 
+val foldR : tr ::: Type -> r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> tr -> t -> t) -> $(mapU tr r) -> t -> t
+
+val appR : m ::: (Type -> Type) -> monad m
+           -> tr ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> m {}) -> $(mapU tr r) -> m {}
+
 val destrR : K --> f :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
              -> (p :: K -> f p -> fr p -> t)
              -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t