mirror of
https://github.com/Lysxia/first-class-families.git
synced 2024-10-27 03:49:57 +03:00
Add unit tests
This commit is contained in:
parent
b83419031c
commit
e361c72ae0
@ -459,6 +459,16 @@ type instance Eval (Lookup (a :: k) (as :: [(k, b)])) =
|
||||
|
||||
-- | Find @Just@ the first element satisfying a predicate, or evaluate to
|
||||
-- @Nothing@ if no element satisfies the predicate.
|
||||
--
|
||||
-- === __Example__
|
||||
--
|
||||
-- >>> :kind! Eval (Find (TyEq 0) '[1,2,3])
|
||||
-- Eval (Find (TyEq 0) '[1,2,3]) :: Maybe Nat
|
||||
-- = 'Nothing
|
||||
--
|
||||
-- >>> :kind! Eval (Find (TyEq 0) '[1,2,3,0])
|
||||
-- Eval (Find (TyEq 0) '[1,2,3,0]) :: Maybe Nat
|
||||
-- = 'Just 0
|
||||
data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)
|
||||
type instance Eval (Find _p '[]) = 'Nothing
|
||||
type instance Eval (Find p (a ': as)) =
|
||||
@ -468,6 +478,12 @@ type instance Eval (Find p (a ': as)) =
|
||||
|
||||
|
||||
-- | Keep all elements that satisfy a predicate, remove all that don't.
|
||||
--
|
||||
-- === __Example__
|
||||
--
|
||||
-- >>> :kind! Eval (Filter ((>) 3) '[1,2,3,0])
|
||||
-- Eval (Filter ((>) 3) '[1,2,3,0]) :: [Nat]
|
||||
-- = '[1, 2, 0]
|
||||
data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]
|
||||
type instance Eval (Filter _p '[]) = '[]
|
||||
type instance Eval (Filter p (a ': as)) =
|
||||
@ -496,6 +512,16 @@ type instance Eval (PartHelp p a '(xs,ys)) =
|
||||
|
||||
|
||||
-- | Find the index of an element satisfying the predicate.
|
||||
--
|
||||
-- === __Example__
|
||||
--
|
||||
-- >>> :kind! Eval (FindIndex ((<=) 3) '[1,2,3,1,2,3])
|
||||
-- Eval (FindIndex ((<=) 3) '[1,2,3,1,2,3]) :: Maybe Nat
|
||||
-- = 'Just 2
|
||||
--
|
||||
-- >>> :kind! Eval (FindIndex ((>) 0) '[1,2,3,1,2,3])
|
||||
-- Eval (FindIndex ((>) 0) '[1,2,3,1,2,3]) :: Maybe Nat
|
||||
-- = 'Nothing
|
||||
data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)
|
||||
type instance Eval (FindIndex _p '[]) = 'Nothing
|
||||
type instance Eval (FindIndex p (a ': as)) =
|
||||
@ -507,6 +533,12 @@ type instance Eval (FindIndex p (a ': as)) =
|
||||
-- | Modify an element at a given index.
|
||||
--
|
||||
-- The list is unchanged if the index is out of bounds.
|
||||
--
|
||||
-- === __Example__
|
||||
--
|
||||
-- >>> :kind! Eval (SetIndex 2 7 '[1,2,3])
|
||||
-- Eval (SetIndex 2 7 '[1,2,3]) :: [Nat]
|
||||
-- = '[1, 2, 7]
|
||||
data SetIndex :: Nat -> a -> [a] -> Exp [a]
|
||||
type instance Eval (SetIndex n a' as) = SetIndexImpl n a' as
|
||||
|
||||
@ -515,7 +547,13 @@ type family SetIndexImpl (n :: Nat) (a' :: k) (as :: [k]) where
|
||||
SetIndexImpl 0 a' (_a ': as) = a' ': as
|
||||
SetIndexImpl n a' (a ': as) = a ': SetIndexImpl (n TL.- 1) a' as
|
||||
|
||||
|
||||
-- | Combine elements of two lists pairwise.
|
||||
--
|
||||
-- === __Example__
|
||||
--
|
||||
-- >>> :kind! Eval (ZipWith (+) '[1,2,3] '[1,1,1])
|
||||
-- Eval (ZipWith (+) '[1,2,3] '[1,1,1]) :: [Nat]
|
||||
-- = '[2, 3, 4]
|
||||
data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
|
||||
type instance Eval (ZipWith _f '[] _bs) = '[]
|
||||
type instance Eval (ZipWith _f _as '[]) = '[]
|
||||
|
73
test/test.hs
73
test/test.hs
@ -4,7 +4,21 @@
|
||||
TypeOperators #-}
|
||||
|
||||
import Data.Type.Equality ((:~:)(Refl))
|
||||
import Fcf
|
||||
import qualified Data.Monoid as Monoid
|
||||
|
||||
import Fcf.Core (Eval, type (@@))
|
||||
import Fcf.Combinators
|
||||
import Fcf.Utils (Case, type (-->), Error)
|
||||
import qualified Fcf.Utils as Case
|
||||
|
||||
import Fcf.Class.Bifunctor
|
||||
import Fcf.Class.Foldable
|
||||
import Fcf.Class.Monoid
|
||||
import Fcf.Class.Ord
|
||||
|
||||
import Fcf.Data.Function
|
||||
import Fcf.Data.List
|
||||
import Fcf.Data.Nat (type (+))
|
||||
|
||||
type UnitPrefix = Case
|
||||
[ 0 --> ""
|
||||
@ -13,7 +27,7 @@ type UnitPrefix = Case
|
||||
, 3 --> "kilo"
|
||||
, 6 --> "mega"
|
||||
, 9 --> "giga"
|
||||
, Any (Error @@ "Something Else")
|
||||
, Case.Any (Error @@ "Something Else")
|
||||
]
|
||||
|
||||
-- Compile-time tests
|
||||
@ -21,6 +35,61 @@ type UnitPrefix = Case
|
||||
_ = Refl :: Eval (UnitPrefix 0) :~: ""
|
||||
_ = Refl :: Eval (UnitPrefix 3) :~: "kilo"
|
||||
|
||||
-- * Class
|
||||
|
||||
-- ** Ord
|
||||
|
||||
_ = Refl :: Eval (Compare '( '(), 0 ) '( '(), 1 )) :~: 'LT
|
||||
_ = Refl :: Eval (Compare '( 1, 3 ) '( 1, 2 )) :~: 'GT
|
||||
_ = Refl :: Eval (Compare ('Left '()) ('Right 'LT)) :~: 'LT
|
||||
_ = Refl :: Eval (Compare ('Right 'EQ) ('Right 'EQ)) :~: 'EQ
|
||||
_ = Refl :: Eval (Compare '[ 'LT, 'EQ, 'GT ] '[ 'LT, 'EQ, 'GT ]) :~: 'EQ
|
||||
_ = Refl :: Eval (Compare 'True 'True) :~: 'EQ
|
||||
_ = Refl :: Eval (Compare "A" "B") :~: 'LT
|
||||
|
||||
_ = Refl :: Eval (1 <= 1) :~: 'True
|
||||
_ = Refl :: Eval (2 <= 1) :~: 'False
|
||||
_ = Refl :: Eval (1 < 1) :~: 'False
|
||||
_ = Refl :: Eval (1 < 2) :~: 'True
|
||||
_ = Refl :: Eval (1 >= 1) :~: 'True
|
||||
_ = Refl :: Eval (1 >= 2) :~: 'False
|
||||
_ = Refl :: Eval (1 > 1) :~: 'False
|
||||
_ = Refl :: Eval (2 > 1) :~: 'True
|
||||
|
||||
-- ** Monoid
|
||||
|
||||
_ = Refl :: Eval ('( '(), '[ 'LT, 'EQ ]) .<> '( '(), '[ 'GT ])) :~: '( '(), '[ 'LT, 'EQ, 'GT ])
|
||||
_ = Refl :: Eval ('Nothing .<> 'Just '[]) :~: 'Just '[]
|
||||
_ = Refl :: Eval ('LT .<> 'GT) :~: 'LT
|
||||
_ = Refl :: Eval ('EQ .<> 'GT) :~: 'GT
|
||||
_ = Refl :: Eval ('Monoid.All 'True .<> 'Monoid.All 'False) :~: 'Monoid.All 'False
|
||||
_ = Refl :: Eval ('Monoid.Any 'True .<> 'Monoid.Any 'False) :~: 'Monoid.Any 'True
|
||||
|
||||
-- ** Foldable
|
||||
|
||||
_ = Refl :: Eval (FoldMap (Pure1 'Monoid.All) '[ 'True, 'False ]) :~: 'Monoid.All 'False
|
||||
_ = Refl :: Eval (FoldMap (Pure1 'Monoid.All) 'Nothing) :~: 'Monoid.All 'True
|
||||
_ = Refl :: Eval (Foldr (.<>) 'LT '[ 'EQ, 'EQ ]) :~: 'LT
|
||||
_ = Refl :: Eval (And '[ 'False, 'False ]) :~: 'False
|
||||
_ = Refl :: Eval (Or '[ 'False, 'False ]) :~: 'False
|
||||
_ = Refl :: Eval (Concat ('Right 'LT)) :~: 'LT
|
||||
|
||||
_ = Refl :: FoldMapDefault_ (Pure1 'Monoid.All) 'Nothing :~: 'Monoid.All 'True
|
||||
_ = Refl :: FoldrDefault_ (.<>) 'LT '[ 'EQ, 'EQ ] :~: 'LT
|
||||
|
||||
-- ** Functor
|
||||
|
||||
_ = Refl :: Eval (Bimap ((+) 1) (Pure2 '(:) '()) '(8, '[])) :~: '(9, '[ '()])
|
||||
_ = Refl :: Eval (First ((+) 1) ('Left 8)) :~: 'Left 9
|
||||
_ = Refl :: Eval (First ((+) 1) ('Right 0)) :~: 'Right 0
|
||||
_ = Refl :: Eval (Second ((+) 1) ('Left 0)) :~: 'Left 0
|
||||
_ = Refl :: Eval (Second ((+) 1) ('Right 8)) :~: 'Right 9
|
||||
|
||||
-- ** Function
|
||||
|
||||
_ = Refl :: Eval (3 & Pure) :~: 3
|
||||
_ = Refl :: Eval (((+) `On` Length) '[1,2,3] '[1,2]) :~: 5
|
||||
|
||||
-- Dummy
|
||||
|
||||
main :: IO ()
|
||||
|
Loading…
Reference in New Issue
Block a user