-- Copyright 2020-2021 Google LLC
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
-- http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-- See the License for the specific language governing permissions and
-- limitations under the License.
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module TestUtils
( type (<), theFin, theSInt
, atNat, asFin, showTyped, showsPrecTyped
) where
import Data.Fin.Int (Fin)
import Data.SInt (SInt)
import Data.Typeable (Typeable, typeOf)
import GHC.TypeNats (CmpNat)
type m < n = CmpNat m n ~ 'LT
theSInt :: SInt n -> SInt n
theSInt = id
theFin :: Fin n -> Fin n
theFin = id
atNat :: SInt n -> p n -> p n
atNat _ = id
asFin :: Fin n -> SInt n -> Fin n
asFin = const
showsPrecTyped :: (Show a, Typeable a) => Int -> a -> ShowS
showsPrecTyped p x = showParen (p > 0) $
shows x . showString " :: " . shows (typeOf x)
showTyped :: (Show a, Typeable a) => a -> String
showTyped x = showsPrecTyped 0 x ""