Library improvements; proper list [un]urlification; remove server-side ServerCalls; eta reduction in type inference

1 files changed, 24 insertions, 0 deletions

diff --git a/lib/ur/monad.urs b/lib/ur/monad.urs
index b3cb3d6f..662d780f 100644
--- a/lib/ur/monad.urs
+++ b/lib/ur/monad.urs
@@ -3,3 +3,27 @@ val exec : m ::: (Type -> Type) -> monad m -> ts ::: {Type}
 
 val ignore : m ::: (Type -> Type) -> monad m -> t ::: Type
              -> m t -> m unit
+
+val foldR : K --> m ::: (Type -> Type) -> monad m
+            -> tf :: (K -> Type)
+            -> tr :: ({K} -> Type)
+            -> (nm :: Name -> t :: K -> rest :: {K}
+                -> [[nm] ~ rest] =>
+                tf t -> tr rest -> m (tr ([nm = t] ++ rest)))
+            -> tr []
+            -> r :: {K} -> folder r -> $(map tf r) -> m (tr r)
+
+val foldR2 : K --> m ::: (Type -> Type) -> monad m
+             -> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
+             -> tr :: ({K} -> Type)
+             -> (nm :: Name -> t :: K -> rest :: {K}
+                 -> [[nm] ~ rest] =>
+                       tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest)))
+             -> tr []
+             -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r)
+
+val mapR : K --> m ::: (Type -> Type) -> monad m
+           -> tf :: (K -> Type)
+           -> tr :: (K -> Type)
+           -> (nm :: Name -> t :: K -> tf t -> m (tr t))
+           -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r))