aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2016-09-24 10:42:48 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2016-09-24 10:42:48 -0400
commitc98872439db4ffacd818c82b4d6e0498c342f225 (patch)
tree6eef3dee921b82508b5bac6cedbb4d55c89185d1 /lib
parent27ab3e9439fab075c6c2ec1f88a603cd4f005caa (diff)
Add mapUX_rev
Diffstat (limited to 'lib')
-rw-r--r--lib/ur/top.ur7
-rw-r--r--lib/ur/top.urs4
2 files changed, 11 insertions, 0 deletions
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index 6c6c896c..02567917 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -179,6 +179,13 @@ fun mapUX [tf :: Type] [ctx :: {Unit}]
<xml>{f [nm] [rest] r}{acc}</xml>)
<xml/>
+fun mapUX_rev [tf :: Type] [ctx :: {Unit}]
+ (f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf -> xml ctx [] []) =
+ @@foldR [fn _ => tf] [fn _ => xml ctx [] []]
+ (fn [nm :: Name] [u :: Unit] [rest :: {Unit}] [[nm] ~ rest] r acc =>
+ <xml>{acc}{f [nm] [rest] r}</xml>)
+ <xml/>
+
fun mapX [K] [tf :: K -> Type] [ctx :: {Unit}]
(f : nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index 8273db0c..ec098955 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -126,6 +126,10 @@ val mapUX : tf :: Type -> ctx :: {Unit}
-> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] =>
tf -> xml ctx [] [])
-> r ::: {Unit} -> folder r -> $(mapU tf r) -> xml ctx [] []
+val mapUX_rev : tf :: Type -> ctx :: {Unit}
+ -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] =>
+ tf -> xml ctx [] [])
+ -> r ::: {Unit} -> folder r -> $(mapU tf r) -> xml ctx [] []
(* Generate some XML by mapping over a heterogenously-typed record *)
val mapX : K --> tf :: (K -> Type) -> ctx :: {Unit}