ddc-code-0.4.2.1: tetra/base/Data/List.ds
module Data.List
export { singleton; replicate
; enumFromTo
; append
; length
; head
; tail; tail1
; last; index
; reverse
; map; mapS
; forS
; zipWith; zipWithS
; foldl; foldlS; sum; prod
; foldr; foldrS
; scanl
; filter; filterS
; any }
import Data.Numeric.Nat
where
-- | Standard Cons-lists.
data List (a: Data) where
Nil : List a
Cons : a -> List a -> List a
-- Constructors ---------------------------------------------------------------
-- | Construct a list containing a single element.
singleton (x: a): List a
= Cons x Nil
-- | Construct a list of the given length where all elements are'
-- the same value.
replicate (n: Nat#) (x: a): List a
| n == 0 = Nil
| otherwise = Cons x (replicate (n - 1) x)
-- | Construct a range of values.
enumFromTo (start: Nat#) (end: Nat#): List Nat#
| start >= end = singleton start
| otherwise = Cons start (enumFromTo (start + 1) end)
-- | Append two lists.
append (xx yy: List a): List a
= case xx of
Nil -> yy
Cons x xs -> Cons x (append xs yy)
-- Projections ----------------------------------------------------------------
-- | Take the length of a list.
length (xx: List a): Nat#
= case xx of
Nil -> 0
Cons x xs -> 1 + length xs
-- | Take the head of a list, if there is one.
head (def: a) (xx: List a): a
= case xx of
Nil -> def
Cons x xs -> x
-- | Take the tail of a list, if there is one.
tail (def: List a) (xx: List a): List a
= case xx of
Nil -> def
Cons x xs -> xs
-- | Like `tail`, but if there is only one element then keep it.
tail1 (def: a) (xx: List a): List a
= case xx of
Nil -> singleton def
Cons x xs
-> case xs of
Nil -> singleton x
_ -> xs
-- | Take the last element of a list, if there is one.
last (def: a) (xx: List a): a
= case xx of
Nil -> def
Cons x xs
-> case xs of
Nil -> x
Cons y ys -> last def xs
index (def: a) (n: Nat#) (xx: List a): a
= case xx of
Nil -> def
Cons x xs
-> case n of
0 -> x
_ -> index def (n - 1) xs
-- Transforms -----------------------------------------------------------------
-- | Reverse the elements of a list.
-- This is a naive O(n^2) version for testing purposes.
reverse (xx: List a): List a
= case xx of
Nil -> Nil
Cons x xs -> append (reverse xs) (singleton x)
-- Maps -----------------------------------------------------------------------
-- | Apply a worker function to every element of a list, yielding a new list.
map (f: a -> b) (xx: List a): List b
= case xx of
Nil -> Nil
Cons x xs -> Cons (f x) (map f xs)
-- | Apply a stateful worker function to every element of a list,
-- yielding a new list.
-- The worker is applied to the source elements left-to-right.
mapS (f: a -> S e b) (xx: List a): S e (List b)
= case xx of
Nil -> Nil
Cons x xs -> Cons (f x) (mapS f xs)
-- | Apply a function to all elements of a list, yielding nothing.
forS (xx: List a) (f: a -> S e Unit): S e Unit
= case xx of
Nil -> ()
Cons x xs
-> do f x
forS xs f
-- Zips -----------------------------------------------------------------------
zipWith (f: a -> b -> c)
(xx: List a) (yy: List b): List c
= case xx of
Nil -> Nil
Cons x xs
-> case yy of
Cons y ys
-> Cons (f x y) (zipWith f xs ys)
Nil -> Nil
zipWithS (f: a -> b -> S e c)
(xx: List a) (yy: List b): S e (List c)
= case xx of
Nil -> Nil
Cons x xs
-> case yy of
Cons y ys
-> Cons (f x y) (zipWithS f xs ys)
Nil -> Nil
-- Folds ----------------------------------------------------------------------
-- | Reduce a list with a binary function and zero value,
-- from left to right.
foldl (f: b -> a -> b) (z: b) (xx: List a): b
= case xx of
Nil -> z
Cons x xs -> foldl f (f z x) xs
-- | Reduce a list with a stateful binary function and zero value,
-- from left to right.
foldlS (f: b -> a -> S e b) (z: b) (xx: List a): S e b
= case xx of
Nil -> z
Cons x xs -> foldlS f (f z x) xs
-- | Reduce a list with a binary function and zero value,
-- from right to left.
foldr (f: a -> b -> b) (z: b) (xx: List a): b
= case xx of
Nil -> z
Cons x xs -> f x (foldr f z xs)
-- | Reduce a list with a stateful binary function and zero value,
-- from right to left.
foldrS (f: a -> b -> S e b) (z: b) (xx: List a): S e b
= case xx of
Nil -> z
Cons x xs -> f x (foldrS f z xs)
-- | Take the sum of a list of Nats.
sum (xs: List Nat#): Nat#
= foldl (+) 0 xs
-- | Take the product of a list of Nats.
prod (xs: List Nat#): Nat#
= foldl (*) 1 xs
-- Scans ----------------------------------------------------------------------
scanl (f: b -> a -> b) (acc: b) (xx: List a): List b
= case xx of
Nil
-> Cons acc Nil
Cons x xs
-> let acc' = f acc x
in Cons acc (scanl f acc' xs)
-- Filters --------------------------------------------------------------------
-- | Keep only those elements that match the given predicate.
filter (p: a -> Bool#) (xx: List a): List a
= case xx of
Nil -> Nil
Cons x xs
-> if p x
then Cons x (filter p xs)
else filter p xs
-- | Keep only those elements that match the given stateful predicate.
-- The predicate is applied to the list elements from left to right.
filterS (p: a -> S e Bool#) (xx: List a): S e (List a)
= case xx of
Nil -> Nil
Cons x xs
-> if p x
then Cons x (filterS p xs)
else filterS p xs
-- | Check if any of the members of the list match the given predicate.
any (p: a -> Bool#) (xx: List a): Bool#
= case xx of
Nil
-> False
Cons x xs
| p x -> True
| otherwise -> any p xs