# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1325804644 18000
# Node ID e7d64ea0f922ca7a69cbba88a298ce1210a22636
# Parent  296807a9fd50e4f7ccdc61d4277f4779acd5b4c9
Variant.weaken, mp, and mapR

diff -r 296807a9fd50 -r e7d64ea0f922 variant.ur
--- a/variant.ur	Mon Jan 02 17:23:31 2012 -0500
+++ b/variant.ur	Thu Jan 05 18:04:04 2012 -0500
@@ -36,6 +36,13 @@
     match v ({nm = Some}
                  ++ @map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl)
 
+fun weaken [r1 ::: {Type}] [r2 ::: {Type}] [r1 ~ r2] (fl : folder r1) (v : variant r1) : variant (r1 ++ r2) =
+    match v
+    (@fold [fn r => r' :: {Type} -> [r ~ r'] => $(map (fn t => t -> variant (r ++ r')) r)]
+      (fn [nm :: Name] [t ::_] [r ::_] [[nm] ~ r] (acc : r' :: {Type} -> [r ~ r'] => $(map (fn t => t -> variant (r ++ r')) r)) [r'::_] [[nm = t] ++ r ~ r'] =>
+          {nm = make [nm]} ++ acc [[nm = t] ++ r'])
+      (fn [r'::_] [[] ~ r'] => {}) fl [r2] !)
+
 fun eq [r] (fl : folder r) (v1 : variant (mapU {} r)) (v2 : variant (mapU {} r)) : bool =
     match v1
     (@fold [fn r => r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)]
@@ -54,6 +61,14 @@
         f' (make [nm] {}) (acc [[nm] ++ r'] f' acc'))
     (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f
 
+fun mp [r ::: {Unit}] [t ::: Type] (fl : folder r) (f : variant (mapU {} r) -> t) : $(mapU t r) =
+    @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t) -> $(mapU t r)]
+    (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
+                     (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t) -> $(mapU t r))
+                     [r' ::_] [[nm] ++ r ~ r'] f' =>
+        {nm = f' (make [nm] {})} ++ acc [[nm] ++ r'] f')
+    (fn [r' ::_] [[] ~ r'] _ => {}) 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)
@@ -65,6 +80,14 @@
 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 mapR [tr] [t] [r] (fl : folder r) (f : variant (mapU {} r) -> tr -> t) (record : $(mapU tr r)) : $(mapU t r) =
+    @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t) -> $(mapU tr r) -> $(mapU t r)]
+    (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
+                     (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t) -> $(mapU tr r) -> $(mapU t r))
+                     [r' ::_] [[nm] ++ r ~ r'] f' vs =>
+        {nm = f' (make [nm] {}) vs.nm} ++ acc [[nm] ++ r'] f' (vs -- nm))
+    (fn [r' ::_] [[] ~ r'] _ _ => {}) fl [[]] ! f record
+
 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 =
diff -r 296807a9fd50 -r e7d64ea0f922 variant.urs
--- a/variant.urs	Mon Jan 02 17:23:31 2012 -0500
+++ b/variant.urs	Thu Jan 05 18:04:04 2012 -0500
@@ -10,6 +10,9 @@
                                                                     -> variant ([nm = t] ++ ts) -> option t
 val testLess : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ts -> variant ([nm = t] ++ ts) -> option t
 
+val weaken : r1 ::: {Type} -> r2 ::: {Type} -> [r1 ~ r2] => folder r1
+             -> variant r1 -> variant (r1 ++ r2)
+
 val testEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] =>
     Eq.eq r ([nm = t] ++ ts)
     -> folder r
@@ -22,6 +25,8 @@
     -> f t
     -> variant (map f r)
 
+val mp : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t) -> $(mapU t r)
+
 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
@@ -29,6 +34,8 @@
 val appR : m ::: (Type -> Type) -> monad m
            -> tr ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> m {}) -> $(mapU tr r) -> m {}
 
+val mapR : tr ::: Type -> t ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> t) -> $(mapU tr r) -> $(mapU t r)
+
 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