primus-0.2.0.0: test/TestTypeLevel.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module TestTypeLevel where

import Primus.TypeLevel
import Data.List.NonEmpty (NonEmpty(..))
import Test.Tasty
import Data.Pos
import Test.Tasty.HUnit

doit :: IO ()
doit = defaultMain suite

suite :: TestTree
suite =
  testGroup
    "TestTypeLevel"
    [ testCase "LengthT" $
        pnat @(LengthT '[]) @?= 0
    , testCase "LengthT" $
        pnat @(LengthT '[ 1,2,3]) @?= 3
    , testCase "LengthT" $
        pnat @(LengthT '[ 1,2,3,4,5,6,7,8,9,10]) @?= 10
    , testCase "LengthT" $
        pnat @(LengthT '[ 1,2,3,4,5,6,7,8,9,10,11]) @?= 11
    , testCase "LengthT" $
        pnat @(LengthT '[ 1,2,3,4,5,6,7,8,9]) @?= 9
    , testCase "LastT" $
        pnat @(LastT '[ 1,2,3]) @?= 3
    , testCase "InitT" $
        fromNSP @(InitT '[ 1,2,3]) @?= _1P :| [_2P]
    , testCase "SnocT" $
        fromNSP @(SnocT '[ 1,2,3] 5) @?= _1P :| [_2P,_3P,_5P]
    , testCase "UnsnocT Fst" $
        fromNSP @(Fst (UnsnocT '[ 1,2,3,4])) @?= _1P :| [_2P,_3P]
    , testCase "UnsnocT Snd" $
        fromNP @(Snd (UnsnocT '[ 1,2,3,4])) @?= _4P
    ]