diff options
author | 2011-06-27 21:36:32 +0100 | |
---|---|---|
committer | 2011-06-27 21:36:32 +0100 | |
commit | 1cf91890aef13e748affc7f792be4872317096a7 (patch) | |
tree | baaa835948c7145928d1263ae22b5021dd37eac8 | |
parent | 81ecb7715080bda3c819e382b1634fc07ea595eb (diff) |
recToList
-rw-r--r-- | lib/ur/list.ur | 4 | ||||
-rw-r--r-- | lib/ur/list.urs | 4 |
2 files changed, 8 insertions, 0 deletions
diff --git a/lib/ur/list.ur b/lib/ur/list.ur index d0c2e7a1..32a9679c 100644 --- a/lib/ur/list.ur +++ b/lib/ur/list.ur @@ -353,3 +353,7 @@ fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) = case assoc x ls of None => (x, y) :: ls | Some _ => ls + +fun recToList [a ::: Type] [r ::: {Unit}] (fl : folder r) + = @foldUR [a] [fn _ => list a] (fn [nm ::_] [rest ::_] [[nm] ~ rest] x xs => + x :: xs) [] fl diff --git a/lib/ur/list.urs b/lib/ur/list.urs index 8284510d..dc8fdeba 100644 --- a/lib/ur/list.urs +++ b/lib/ur/list.urs @@ -79,3 +79,7 @@ val replaceNth : a ::: Type -> list a -> int -> a -> list a val assoc : a ::: Type -> b ::: Type -> eq a -> a -> t (a * b) -> option b val assocAdd : a ::: Type -> b ::: Type -> eq a -> a -> b -> t (a * b) -> t (a * b) + +(** Converting records to lists *) + +val recToList : a ::: Type -> r ::: {Unit} -> folder r -> $(mapU a r) -> t a |