diff options
Diffstat (limited to 'lib/ur')
| -rw-r--r-- | lib/ur/list.ur | 26 | ||||
| -rw-r--r-- | lib/ur/list.urs | 6 |
2 files changed, 32 insertions, 0 deletions
diff --git a/lib/ur/list.ur b/lib/ur/list.ur index d28d2868..10877420 100644 --- a/lib/ur/list.ur +++ b/lib/ur/list.ur @@ -153,6 +153,16 @@ fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f = mapM' [] end +fun mapMi [m ::: (Type -> Type)] (_ : monad m) [a] [b] f = + let + fun mapM' i acc ls = + case ls of + [] => return (rev acc) + | x :: ls => x' <- f i x; mapM' (i + 1) (x' :: acc) ls + in + mapM' 0 [] + end + fun mapPartialM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f = let fun mapPartialM' acc ls = @@ -469,6 +479,22 @@ fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) = None => (x, y) :: ls | Some _ => ls +fun assocAddSorted [a] [b] (_ : eq a) (_ : ord a) (x : a) (y : b) (ls : t (a * b)) = + let + fun aas (ls : t (a * b)) (acc : t (a * b)) = + case ls of + [] => rev ((x, y) :: acc) + | (x', y') :: ls' => + if x' = x then + revAppend ((x, y) :: acc) ls' + else if x < x' then + revAppend ((x, y) :: acc) ls + else + aas ls' ((x', y') :: acc) + in + aas ls [] + end + 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 f4593dda..c1d46022 100644 --- a/lib/ur/list.urs +++ b/lib/ur/list.urs @@ -31,6 +31,9 @@ val mapXi : a ::: Type -> ctx ::: {Unit} -> (int -> a -> xml ctx [] []) -> t a - val mapM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> (a -> m b) -> t a -> m (t b) +val mapMi : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type + -> (int -> a -> m b) -> t a -> m (t b) + val mapPartialM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> (a -> m (option b)) -> t a -> m (t b) val mapXM : m ::: (Type -> Type) -> monad m -> a ::: Type -> ctx ::: {Unit} @@ -106,6 +109,9 @@ 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) +val assocAddSorted : a ::: Type -> b ::: Type -> eq a -> ord a -> a -> b -> t (a * b) -> t (a * b) +(* Assume the list is already sorted in ascending order and maintain that ordering. *) + (** Converting records to lists *) val recToList : a ::: Type -> r ::: {Unit} -> folder r -> $(mapU a r) -> t a |