diff options
author | Adam Chlipala <adam@chlipala.net> | 2016-09-24 10:42:48 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2016-09-24 10:42:48 -0400 |
commit | c98872439db4ffacd818c82b4d6e0498c342f225 (patch) | |
tree | 6eef3dee921b82508b5bac6cedbb4d55c89185d1 /lib/ur | |
parent | 27ab3e9439fab075c6c2ec1f88a603cd4f005caa (diff) |
Add mapUX_rev
Diffstat (limited to 'lib/ur')
-rw-r--r-- | lib/ur/top.ur | 7 | ||||
-rw-r--r-- | lib/ur/top.urs | 4 |
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} |