From 1cf91890aef13e748affc7f792be4872317096a7 Mon Sep 17 00:00:00 2001 From: Robin Green Date: Mon, 27 Jun 2011 21:36:32 +0100 Subject: recToList --- lib/ur/list.ur | 4 ++++ lib/ur/list.urs | 4 ++++ 2 files changed, 8 insertions(+) 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 -- cgit v1.2.3