mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 09:49:24 +03:00
[new] Add Colist and Colist1 to base (#997)
This commit is contained in:
Stefan Hoeck
GitHub
parent
cff7db38cb
commit
39824c6295
220
libs/base/Data/Colist.idr
Normal file
220
libs/base/Data/Colist.idr
Normal file
@ -0,0 +1,220 @@
|
||||
module Data.Colist
|
||||
|
||||
import Data.Maybe
|
||||
import Data.List
|
||||
import public Data.Zippable
|
||||
|
||||
%default total
|
||||
|
||||
||| A possibly finite Stream.
|
||||
public export
|
||||
data Colist : (a : Type) -> Type where
|
||||
Nil : Colist a
|
||||
(::) : a -> Inf (Colist a) -> Colist a
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Creating Colists
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
||| Convert a list to a `Colist`.
|
||||
public export
|
||||
fromList : List a -> Colist a
|
||||
fromList [] = Nil
|
||||
fromList (x :: xs) = x :: fromList xs
|
||||
|
||||
||| Convert a stream to a `Colist`.
|
||||
public export
|
||||
fromStream : Stream a -> Colist a
|
||||
fromStream (x :: xs) = x :: fromStream xs
|
||||
|
||||
||| Create a `Colist` of only a single element.
|
||||
public export
|
||||
singleton : a -> Colist a
|
||||
singleton a = a :: Nil
|
||||
|
||||
||| An infinite `Colist` of repetitions of the same element.
|
||||
public export
|
||||
repeat : a -> Colist a
|
||||
repeat v = v :: repeat v
|
||||
|
||||
||| Create a `Colist` of `n` replications of the given element.
|
||||
public export
|
||||
replicate : Nat -> a -> Colist a
|
||||
replicate 0 _ = Nil
|
||||
replicate (S k) x = x :: replicate k x
|
||||
|
||||
||| Produce a `Colist` by repeating a sequence.
|
||||
public export
|
||||
cycle : List a -> Colist a
|
||||
cycle Nil = Nil
|
||||
cycle (x :: xs) = run x xs
|
||||
where run : a -> List a -> Colist a
|
||||
run v [] = v :: run x xs
|
||||
run v (y :: ys) = v :: run y ys
|
||||
|
||||
||| Generate an infinite `Colist` by repeatedly applying a function.
|
||||
public export
|
||||
iterate : (a -> a) -> a -> Colist a
|
||||
iterate f a = a :: iterate f (f a)
|
||||
|
||||
||| Generate a `Colist` by repeatedly applying a function.
|
||||
||| This stops once the function returns `Nothing`.
|
||||
public export
|
||||
iterateMaybe : (f : a -> Maybe a) -> Maybe a -> Colist a
|
||||
iterateMaybe _ Nothing = Nil
|
||||
iterateMaybe f (Just x) = x :: iterateMaybe f (f x)
|
||||
|
||||
||| Generate an `Colist` by repeatedly applying a function
|
||||
||| to a seed value.
|
||||
||| This stops once the function returns `Nothing`.
|
||||
public export
|
||||
unfold : (f : s -> Maybe (s,a)) -> s -> Colist a
|
||||
unfold f s = case f s of
|
||||
Just (s2,a) => a :: unfold f s2
|
||||
Nothing => Nil
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Basic Functions
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
||| True, if this is the empty `Colist`.
|
||||
public export
|
||||
isNil : Colist a -> Bool
|
||||
isNil [] = True
|
||||
isNil _ = False
|
||||
|
||||
||| True, if the given `Colist` is non-empty.
|
||||
public export
|
||||
isCons : Colist a -> Bool
|
||||
isCons [] = False
|
||||
isCons _ = True
|
||||
|
||||
||| Concatenate two `Colist`s.
|
||||
public export
|
||||
append : Colist a -> Colist a -> Colist a
|
||||
append [] ys = ys
|
||||
append (x :: xs) ys = x :: append xs ys
|
||||
|
||||
||| Append a `Colist` to a `List`.
|
||||
public export
|
||||
lappend : List a -> Colist a -> Colist a
|
||||
lappend xs = append (fromList xs)
|
||||
|
||||
||| Append a `List` to a `Colist`.
|
||||
public export
|
||||
appendl : Colist a -> List a -> Colist a
|
||||
appendl xs = append xs . fromList
|
||||
|
||||
||| Try to extract the first element from a `Colist`.
|
||||
public export
|
||||
head : Colist a -> Maybe a
|
||||
head [] = Nothing
|
||||
head (x :: _) = Just x
|
||||
|
||||
||| Try to drop the first element from a `Colist`.
|
||||
||| This returns `Nothing` if the given `Colist` is
|
||||
||| empty.
|
||||
public export
|
||||
tail : Colist a -> Maybe (Colist a)
|
||||
tail [] = Nothing
|
||||
tail (_ :: xs) = Just xs
|
||||
|
||||
||| Take up to `n` elements from a `Colist`.
|
||||
public export
|
||||
take : (n : Nat) -> Colist a -> List a
|
||||
take 0 _ = Nil
|
||||
take (S k) [] = Nil
|
||||
take (S k) (x :: xs) = x :: take k xs
|
||||
|
||||
||| Take elements from a `Colist` up to and including the
|
||||
||| first element, for which `p` returns `True`.
|
||||
public export
|
||||
takeUntil : (p : a -> Bool) -> Colist a -> Colist a
|
||||
takeUntil _ [] = Nil
|
||||
takeUntil p (x :: xs) = if p x then [x] else x :: takeUntil p xs
|
||||
|
||||
||| Take elements from a `Colist` up to (but not including) the
|
||||
||| first element, for which `p` returns `True`.
|
||||
public export
|
||||
takeBefore : (a -> Bool) -> Colist a -> Colist a
|
||||
takeBefore _ [] = Nil
|
||||
takeBefore p (x :: xs) = if p x then [] else x :: takeBefore p xs
|
||||
|
||||
||| Take elements from a `Colist` while the given predicate
|
||||
||| returns `True`.
|
||||
public export
|
||||
takeWhile : (a -> Bool) -> Colist a -> Colist a
|
||||
takeWhile p = takeBefore (not . p)
|
||||
|
||||
||| Extract all values wrapped in `Just` from the beginning
|
||||
||| of a `Colist`. This stops, once the first `Nothing` is encountered.
|
||||
public export
|
||||
takeWhileJust : Colist (Maybe a) -> Colist a
|
||||
takeWhileJust [] = []
|
||||
takeWhileJust (Nothing :: _) = []
|
||||
takeWhileJust (Just x :: xs) = x :: takeWhileJust xs
|
||||
|
||||
||| Drop up to `n` elements from the beginning of the `Colist`.
|
||||
public export
|
||||
drop : (n : Nat) -> Colist a -> Colist a
|
||||
drop _ [] = Nil
|
||||
drop 0 xs = xs
|
||||
drop (S k) (x :: xs) = drop k xs
|
||||
|
||||
||| Try to extract the `n`-th element from a `Colist`.
|
||||
public export
|
||||
index : (n : Nat) -> Colist a -> Maybe a
|
||||
index _ [] = Nothing
|
||||
index 0 (x :: _) = Just x
|
||||
index (S k) (_ :: xs) = index k xs
|
||||
|
||||
||| Produce a `Colist` of left folds of prefixes of the given `Colist`.
|
||||
||| @ f the combining function
|
||||
||| @ acc the initial value
|
||||
||| @ xs the `Colist` to process
|
||||
public export
|
||||
scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Colist b) -> Colist a
|
||||
scanl _ acc Nil = [acc]
|
||||
scanl f acc (x :: xs) = acc :: scanl f (f acc x) xs
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Implementations
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
public export
|
||||
Semigroup (Colist a) where
|
||||
(<+>) = append
|
||||
|
||||
public export
|
||||
Monoid (Colist a) where
|
||||
neutral = Nil
|
||||
|
||||
public export
|
||||
Functor Colist where
|
||||
map f [] = []
|
||||
map f (x :: xs) = f x :: map f xs
|
||||
|
||||
public export
|
||||
Applicative Colist where
|
||||
pure = repeat
|
||||
|
||||
[] <*> _ = []
|
||||
_ <*> [] = []
|
||||
f :: fs <*> a :: as = f a :: (fs <*> as)
|
||||
|
||||
public export
|
||||
Zippable Colist where
|
||||
zipWith f as bs = [| f as bs |]
|
||||
|
||||
zipWith3 f as bs cs = [| f as bs cs |]
|
||||
|
||||
unzip xs = (map fst xs, map snd xs)
|
||||
|
||||
unzip3 xs = ( map (\(a,_,_) => a) xs
|
||||
, map (\(_,b,_) => b) xs
|
||||
, map (\(_,_,c) => c) xs
|
||||
)
|
||||
|
||||
unzipWith f = unzip . map f
|
||||
|
||||
unzipWith3 f = unzip3 . map f
|
||||
203
libs/base/Data/Colist1.idr
Normal file
203
libs/base/Data/Colist1.idr
Normal file
@ -0,0 +1,203 @@
|
||||
module Data.Colist1
|
||||
|
||||
import Data.Colist
|
||||
import Data.List1
|
||||
import Data.Nat
|
||||
import public Data.Zippable
|
||||
|
||||
%default total
|
||||
|
||||
||| A possibly finite, non-empty Stream.
|
||||
public export
|
||||
data Colist1 : (a : Type) -> Type where
|
||||
(:::) : a -> Colist a -> Colist1 a
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Creating Colist1
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
||| Convert a `List1` to a `Colist1`.
|
||||
public export
|
||||
fromList1 : List1 a -> Colist1 a
|
||||
fromList1 (h ::: t) = h ::: fromList t
|
||||
|
||||
||| Convert a stream to a `Colist1`.
|
||||
public export
|
||||
fromStream : Stream a -> Colist1 a
|
||||
fromStream (x :: xs) = x ::: fromStream xs
|
||||
|
||||
||| Try to convert a `Colist` to a `Colist1`. Returns `Nothing` if
|
||||
||| the given `Colist` is empty.
|
||||
public export
|
||||
fromColist : Colist a -> Maybe (Colist1 a)
|
||||
fromColist Nil = Nothing
|
||||
fromColist (x :: xs) = Just (x ::: xs)
|
||||
|
||||
||| Try to convert a list to a `Colist1`. Returns `Nothing` if
|
||||
||| the given list is empty.
|
||||
public export
|
||||
fromList : List a -> Maybe (Colist1 a)
|
||||
fromList = fromColist . fromList
|
||||
|
||||
||| Create a `Colist1` of only a single element.
|
||||
public export
|
||||
singleton : a -> Colist1 a
|
||||
singleton a = a ::: Nil
|
||||
|
||||
||| An infinite `Colist1` of repetitions of the same element.
|
||||
public export
|
||||
repeat : a -> Colist1 a
|
||||
repeat v = v ::: repeat v
|
||||
|
||||
||| Create a `Colist1` of `n` replications of the given element.
|
||||
public export
|
||||
replicate : (n : Nat) -> {auto 0 prf : IsSucc n} -> a -> Colist1 a
|
||||
replicate 0 _ impossible
|
||||
replicate (S k) x = x ::: replicate k x
|
||||
|
||||
||| Produce a `Colist1` by repeating a sequence
|
||||
public export
|
||||
cycle : List1 a -> Colist1 a
|
||||
cycle (x ::: xs) = x ::: cycle (xs ++ [x])
|
||||
|
||||
||| Generate an infinite `Colist1` by repeatedly applying a function.
|
||||
public export
|
||||
iterate : (f : a -> a) -> a -> Colist1 a
|
||||
iterate f a = a ::: iterate f (f a)
|
||||
|
||||
||| Generate a `Colist1` by repeatedly applying a function.
|
||||
||| This stops once the function returns `Nothing`.
|
||||
public export
|
||||
iterateMaybe : (f : a -> Maybe a) -> a -> Colist1 a
|
||||
iterateMaybe f a = a ::: iterateMaybe f (f a)
|
||||
|
||||
||| Generate a `Colist1` by repeatedly applying a function
|
||||
||| to a seed value.
|
||||
||| This stops once the function returns `Nothing`.
|
||||
public export
|
||||
unfold : (f : s -> Maybe (s,a)) -> s -> a -> Colist1 a
|
||||
unfold f s a = a ::: unfold f s
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Basic Functions
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
||| Convert a `Colist1` to a `Colist`
|
||||
public export
|
||||
forget : Colist1 a -> Colist a
|
||||
forget (h ::: t) = h :: t
|
||||
|
||||
||| Prepends an element to a `Colist1`.
|
||||
public export
|
||||
cons : (x : a) -> (xs : Colist1 a) -> Colist1 a
|
||||
cons x xs = x ::: forget xs
|
||||
|
||||
||| Concatenate two `Colist1`s
|
||||
public export
|
||||
append : Colist1 a -> Colist1 a -> Colist1 a
|
||||
append (h ::: t) ys = h ::: append t (forget ys)
|
||||
|
||||
||| Append a `Colist1` to a `List`.
|
||||
public export
|
||||
lappend : List a -> Colist1 a -> Colist1 a
|
||||
lappend Nil ys = ys
|
||||
lappend (x :: xs) ys = x ::: lappend xs (forget ys)
|
||||
|
||||
||| Append a `List` to a `Colist1`.
|
||||
public export
|
||||
appendl : Colist1 a -> List a -> Colist1 a
|
||||
appendl (x ::: xs) ys = x ::: appendl xs ys
|
||||
|
||||
||| Extract the first element from a `Colist1`
|
||||
public export
|
||||
head : Colist1 a -> a
|
||||
head (h ::: _) = h
|
||||
|
||||
||| Drop the first element from a `Colist1`
|
||||
public export
|
||||
tail : Colist1 a -> Colist a
|
||||
tail (_ ::: t) = t
|
||||
|
||||
||| Take up to `n` elements from a `Colist1`
|
||||
public export
|
||||
take : (n : Nat) -> {auto 0 prf : IsSucc n} -> Colist1 a -> List1 a
|
||||
take 0 _ impossible
|
||||
take (S k) (x ::: xs) = x ::: take k xs
|
||||
|
||||
||| Take elements from a `Colist1` up to and including the
|
||||
||| first element, for which `p` returns `True`.
|
||||
public export
|
||||
takeUntil : (p : a -> Bool) -> Colist1 a -> Colist1 a
|
||||
takeUntil p (x ::: xs) = if p x then singleton x else x ::: takeUntil p xs
|
||||
|
||||
||| Take elements from a `Colist1` up to (but not including) the
|
||||
||| first element, for which `p` returns `True`.
|
||||
public export
|
||||
takeBefore : (p : a -> Bool) -> Colist1 a -> Colist a
|
||||
takeBefore p = takeBefore p . forget
|
||||
|
||||
||| Take elements from a `Colist1` while the given predicate `p`
|
||||
||| returns `True`.
|
||||
public export
|
||||
takeWhile : (p : a -> Bool) -> Colist1 a -> Colist a
|
||||
takeWhile p = takeWhile p . forget
|
||||
|
||||
||| Extract all values wrapped in `Just` from the beginning
|
||||
||| of a `Colist1`. This stops, once the first `Nothing` is encountered.
|
||||
public export
|
||||
takeWhileJust : Colist1 (Maybe a) -> Colist a
|
||||
takeWhileJust = takeWhileJust . forget
|
||||
|
||||
||| Drop up to `n` elements from the beginning of the `Colist1`.
|
||||
public export
|
||||
drop : (n : Nat) -> Colist1 a -> Colist a
|
||||
drop n = drop n . forget
|
||||
|
||||
||| Try to extract the `n`-th element from a `Colist1`.
|
||||
public export
|
||||
index : (n : Nat) -> Colist1 a -> Maybe a
|
||||
index n = index n . forget
|
||||
|
||||
||| Produce a `Colist1` of left folds of prefixes of the given `Colist1`.
|
||||
||| @ f the combining function
|
||||
||| @ acc the initial value
|
||||
||| @ xs the `Colist1` to process
|
||||
export
|
||||
scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Colist1 b) -> Colist1 a
|
||||
scanl f acc (x ::: xs) = acc ::: scanl f (f acc x) xs
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Interfaces
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
public export
|
||||
Semigroup (Colist1 a) where
|
||||
(<+>) = append
|
||||
|
||||
public export
|
||||
Functor Colist1 where
|
||||
map f (x ::: xs) = f x ::: map f xs
|
||||
|
||||
public export
|
||||
Applicative Colist1 where
|
||||
pure = repeat
|
||||
|
||||
(f ::: fs) <*> (a ::: as) = f a ::: (fs <*> as)
|
||||
|
||||
public export
|
||||
Zippable Colist1 where
|
||||
zipWith f (x ::: xs) (y ::: ys) = f x y ::: zipWith f xs ys
|
||||
|
||||
zipWith3 f (x ::: xs) (y ::: ys) (z ::: zs) =
|
||||
f x y z ::: zipWith3 f xs ys zs
|
||||
|
||||
unzip xs = (map fst xs, map snd xs)
|
||||
|
||||
unzip3 xs = ( map (\(a,_,_) => a) xs
|
||||
, map (\(_,b,_) => b) xs
|
||||
, map (\(_,_,c) => c) xs
|
||||
)
|
||||
|
||||
unzipWith f = unzip . map f
|
||||
|
||||
unzipWith3 f = unzip3 . map f
|
||||
@ -28,6 +28,8 @@ modules = Control.App,
|
||||
Data.Bool,
|
||||
Data.Bool.Xor,
|
||||
Data.Buffer,
|
||||
Data.Colist,
|
||||
Data.Colist1,
|
||||
Data.DPair,
|
||||
Data.Either,
|
||||
Data.Fin,
|
||||
|
||||
Loading…
Reference in New Issue
Block a user