{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Typing.Test where import Test.Tasty import Test.Tasty.HUnit import Control.Applicative (Applicative(..)) import Control.Arrow (left) import Data.Map.Strict (Map) import Data.Maybe (isJust) import Data.NonNull (NonNull) import Data.Proxy import Data.Ratio (Ratio) import Data.Text (Text) import Data.List.NonEmpty (NonEmpty) import GHC.Exts (Constraint) import Prelude hiding (exp) import qualified Data.Function as Fun import qualified Data.Map.Strict as Map import qualified Data.MonoTraversable as MT import qualified Data.Sequences as Seqs import qualified System.IO as IO import qualified Text.Megaparsec as P import Language.Symantic.Grammar import Language.Symantic import Language.Symantic.Lib hiding ((<$>), (<*), show) import Grammar.Megaparsec -- -- P.ParsecT instances -- instance ( ParsecC e s , Gram_Source src (P.ParsecT e s m) ) => Gram_Type src (P.ParsecT e s m) -- * Tests type SS = [ Proxy (->) , Proxy Bool , Proxy [] , Proxy () , Proxy (,) , Proxy Char , Proxy Either , Proxy Int , Proxy Integer , Proxy IO , Proxy IO.Handle , Proxy IO.IOMode , Proxy Ordering , Proxy Map , Proxy Maybe , Proxy NonNull , Proxy Ratio , Proxy Text , Proxy Applicative , Proxy Bounded , Proxy Enum , Proxy Eq , Proxy Foldable , Proxy Functor , Proxy Integral , Proxy Monad , Proxy Monoid , Proxy MT.MonoFoldable , Proxy MT.MonoFunctor , Proxy Num , Proxy Ord , Proxy Real , Proxy Seqs.IsSequence , Proxy Seqs.SemiSequence , Proxy Show , Proxy Traversable ] type SRC = SrcTe (NonEmpty P.SourcePos) SS cs :: Source src => Name2Type src cs = Map.insert "String" (Len2Type $ \len -> TypeT $ tyConstLen @(K []) @[] len `tyApp` tyConstLen @(K Char) @Char len) $ inj_Name2Type (Proxy @SS) tests :: TestTree tests = testGroup "Typing" $ [ testGroup "readType" $ let run inp (TypeT exp :: TypeT SRC '[]) = testCase inp $ got @?= Right (Right $ TypeVT exp) where got :: Either (P.ParseError Char P.Dec) (Either (Error_Type SRC) (TypeVT SRC)) got = readType cs <$> P.runParser (unCF g) "" inp g :: Gram_Type SRC g => CF g (AST_Type SRC) g = g_type <* eoi in let (==>) = run; infixr 0 ==> in [ "Bool" ==> TypeT $ tyBool , "(->) Bool" ==> TypeT $ tyFun `tyApp` tyBool , "[]" ==> TypeT $ tyConst @(K []) @[] , "[Char]" ==> TypeT $ tyList tyChar , "[Char -> [Char]]" ==> TypeT $ tyList (tyChar ~> tyList tyChar) , "([])" ==> TypeT $ tyConst @(K []) @[] , "[()]" ==> TypeT $ tyList tyUnit , "()" ==> TypeT $ tyUnit , "(())" ==> TypeT $ tyUnit , "(,)" ==> TypeT $ tyConst @(K (,)) @(,) , "((,))" ==> TypeT $ tyConst @(K (,)) @(,) , "(,) Int" ==> TypeT $ tyConst @(K (,)) @(,) `tyApp` tyInt , "(Bool)" ==> TypeT $ tyBool , "((Bool))" ==> TypeT $ tyBool , "(Bool, Int)" ==> TypeT $ tyBool `tyTuple2` tyInt , "((Bool, Int))" ==> TypeT $ tyBool `tyTuple2` tyInt , "((Bool, Int), Char)" ==> TypeT $ (tyBool `tyTuple2` tyInt) `tyTuple2` tyChar , "(Bool, Int) -> Char" ==> TypeT $ (tyBool `tyTuple2` tyInt) ~> tyChar , "(Bool -> Int)" ==> TypeT $ tyBool ~> tyInt , "String" ==> TypeT $ tyList tyChar , "[Char] -> String" ==> TypeT $ tyList tyChar ~> tyList tyChar , "String -> [Char]" ==> TypeT $ tyList tyChar ~> tyList tyChar , "Maybe Bool" ==> TypeT $ tyMaybe tyBool , "Either Bool Int" ==> TypeT $ tyEither tyBool tyInt , "Bool -> Int" ==> TypeT $ tyBool ~> tyInt , "(Bool -> Int) -> Char" ==> TypeT $ (tyBool ~> tyInt) ~> tyChar , "Bool -> (Int -> Char)" ==> TypeT $ tyBool ~> (tyInt ~> tyChar) , "Bool -> Int -> Char" ==> TypeT $ tyBool ~> tyInt ~> tyChar , "Bool -> (Int -> Char) -> ()" ==> TypeT $ tyBool ~> (tyInt ~> tyChar) ~> tyUnit , "IO" ==> TypeT $ tyConst @(K IO) @IO , "Traversable IO" ==> TypeT $ tyTraversable (tyConst @(K IO) @IO) , "Monad IO" ==> TypeT $ tyMonad (tyConst @(K IO) @IO) , "(->) (IO Bool)" ==> TypeT $ tyConst @(K (->)) @(->) `tyApp` (tyIO tyBool) , "Monad IO" ==> TypeT $ tyMonad (tyConst @(K IO) @IO) , "Eq" ==> TypeT $ tyConst @(K Eq) @Eq , "Eq Bool" ==> TypeT $ tyEq tyBool ] , testGroup "Parsing errors" $ let run inp = testCase inp $ got @?= Left () where got :: Either () (AST_Type SRC) got = left (\(_::P.ParseError (P.Token String) P.Dec) -> ()) $ P.runParser (unCF g) "" inp g :: Gram_Type SRC g => CF g (AST_Type SRC) g = g_type <* eoi in run <$> [ "Bool, Int" , "(Bool -> Int) Char" ] , testGroup "Compiling errors" $ let run inp = testCase inp $ got @?= Right (Left ()) where got :: Either (P.ParseError Char P.Dec) (Either () (TypeVT SRC)) got = left (Fun.const ()) . readType cs <$> P.runParser (unCF g) "" inp g :: Gram_Type SRC g => CF g (AST_Type SRC) g = g_type <* eoi in run <$> [ "NonExistingType" , "Bool Int" , "[IO]" , "(->) IO" , "(->) Bool Int Char" , "Monad Eq" ] , testGroup "proveConstraint" $ let (==>) (typ::Type SRC '[] (t::Constraint)) expected = testCase (show typ) $ isJust (proveConstraint typ) @?= expected in [ tyEq tyBool ==> True , tyOrd tyBool ==> True , tyFunctor (tyConst @(K Maybe) @Maybe) ==> True , tyFunctor (tyConst @(K IO) @IO) ==> True , tyMonad (tyConst @(K IO) @IO) ==> True , tyTraversable (tyConst @(K IO) @IO) ==> False ] ]