git.iko.soy/Idris-dev
on master help sign in
add Data.CoList with unfoldr to contrib
commit9cdbf3e5933a61f0bb049661c1c09499f21dd021 authorHeather <heather@live.ru> dateTue 28 Apr 2015, 13:00 (11 years ago) parente7f9257
2 files changed+35−2
compare with master
unifiedsplit
libs/contrib/Data/CoList.idr+32 libs/contrib/contrib.ipkg+3−2
libs/contrib/Data/CoList.idrnew file+32
@@ -0,0 +1,32 @@
1+module Data.CoList
2+
3+%access public
4+
5+||| Idris will know that it always can produce a new element in finite time
6+codata CoList : Type -> Type
7+ where {
8+ Nil : CoList a;
9+ (::) : a -> CoList a -> CoList a
10+ }
11+
12+||| Take the first `n` elements of `xs`
13+|||
14+||| If there are not enough elements, return the whole coList.
15+||| @ n how many elements to take
16+||| @ xs the coList to take them from
17+takeCo : (n : Nat) -> (xs : CoList a) -> List a
18+takeCo Z _ = []
19+takeCo (S n) [] = []
20+takeCo (S n) (x::xs) = x :: takeCo n xs
21+
22+||| The unfoldr builds a list from a seed value. In some cases, unfoldr can undo a foldr operation.
23+|||
24+||| ``` idris example
25+||| unfoldr (\b => if b == 0 then Nothing else Just (b, b-1)) 10
26+||| ```
27+|||
28+unfoldr : (a -> Maybe (a, a)) -> a -> CoList a
29+unfoldr f x =
30+ case f x of
31+ Just (y, new_x) => y :: (unfoldr f new_x)
32+ _ => []
libs/contrib/contrib.ipkg+3−2
@@ -2,8 +2,8 @@ package contrib
22
33opts = "--nobasepkgs --total -i ../prelude -i ../base"
44modules = Control.Algebra,
5− Control.Algebra.Lattice, Control.Algebra.VectorSpace,
6− Control.Algebra.NumericInstances,
5+ Control.Algebra.Lattice, Control.Algebra.VectorSpace,
6+ Control.Algebra.NumericInstances,
77 Control.Isomorphism.Primitives,
88 Control.Partial,
99 Control.WellFounded,
@@ -15,6 +15,7 @@ modules = Control.Algebra,
1515 Data.BoundedList,
1616 Data.Heap,
1717 Data.SortedMap, Data.SortedSet,
18+ Data.CoList,
1819
1920 Decidable.Decidable, Decidable.Order,
2021