git.iko.soy/Idris-dev
on master help sign in
add Data.CoList with unfoldr to contrib
9cdbf3eHeather
libs/contrib/Data/CoList.idrnew file+32
compare with master
unifiedsplit
@@ -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
2
2
3opts = "--nobasepkgs --total -i ../prelude -i ../base"
3opts = "--nobasepkgs --total -i ../prelude -i ../base"
4modules = Control.Algebra,
4modules = Control.Algebra,
5− Control.Algebra.Lattice, Control.Algebra.VectorSpace,
5+ Control.Algebra.Lattice, Control.Algebra.VectorSpace,
6− Control.Algebra.NumericInstances,
6+ Control.Algebra.NumericInstances,
7 Control.Isomorphism.Primitives,
7 Control.Isomorphism.Primitives,
8 Control.Partial,
8 Control.Partial,
9 Control.WellFounded,
9 Control.WellFounded,
@@ -15,6 +15,7 @@ modules = Control.Algebra,
15 Data.BoundedList,
15 Data.BoundedList,
16 Data.Heap,
16 Data.Heap,
17 Data.SortedMap, Data.SortedSet,
17 Data.SortedMap, Data.SortedSet,
18+ Data.CoList,
18
19
19 Decidable.Decidable, Decidable.Order,
20 Decidable.Decidable, Decidable.Order,
20
21