{-# 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.Maybe (isJust) import Data.Proxy import GHC.Exts (Constraint) import Prelude hiding (exp) import qualified Text.Megaparsec as P import Language.Symantic.Lib.Data.Type.List import Language.Symantic.Parsing.Grammar import Language.Symantic.Typing import Language.Symantic.Compiling ((~>)) import Parsing.Grammar.Test -- * Tests type Tys = Constants ++ '[Proxy String] instance ( ParsecC e s , Gram_Meta meta (P.ParsecT e s m) ) => Gram_Type meta (P.ParsecT e s m) tests :: TestTree tests = testGroup "Typing" $ [ testGroup "compile_type" $ let (==>) inp exp = testCase inp $ got @?= Right (Right exp) where got :: Either (P.ParseError Char P.Dec) (Either (Error_Type P.SourcePos '[Proxy Token_Type]) (EType Tys)) got = (compile_etype <$>) $ (`runParser` inp) $ unCF p p :: Gram_Type P.SourcePos p => CF p (TokType P.SourcePos) p = typeG <* eoi in uncurry (==>) <$> [ ("Bool", EType $ ty @Bool) , ("[]", EType $ ty @[]) , ("[Char]", EType $ ty @[] :$ ty @Char) , ("[Char -> [Char]]", EType $ ty @[] :$ (ty @Char ~> ty @[] :$ ty @Char)) , ("([])", EType $ ty @[]) , ("[()]", EType $ ty @[] :$ ty @()) , ("()", EType $ ty @()) , ("(())", EType $ ty @()) , ("(,)", EType $ ty @(,)) , ("((,))", EType $ ty @(,)) , ("(,) Int", EType $ ty @(,) :$ ty @Int) , ("(Bool)", EType $ ty @Bool) , ("((Bool))", EType $ ty @Bool) , ("(Bool, Int)", EType $ ty @(,) :$ ty @Bool :$ ty @Int) , ("((Bool, Int))", EType $ ty @(,) :$ ty @Bool :$ ty @Int) , ("((Bool, Int), Char)", EType $ ty @(,) :$ (ty @(,) :$ ty @Bool :$ ty @Int) :$ ty @Char) , ("(Bool, Int) -> Char", EType $ (ty @(,) :$ ty @Bool :$ ty @Int) ~> ty @Char) , ("(Bool -> Int)", EType $ ty @Bool ~> ty @Int) , ("String", EType $ ty @[] :$ ty @Char) , ("[Char] -> String", EType $ (ty @[] :$ ty @Char) ~> (ty @[] :$ ty @Char)) , ("String -> [Char]", EType $ (ty @[] :$ ty @Char) ~> (ty @[] :$ ty @Char)) , ("Maybe Bool", EType $ ty @Maybe :$ ty @Bool) , ("Either Bool Int", EType $ ty @Either :$ ty @Bool :$ ty @Int) , ("Bool -> Int", EType $ ty @Bool ~> ty @Int) , ("(Bool -> Int) -> Char", EType $ (ty @Bool ~> ty @Int) ~> ty @Char) , ("Bool -> (Int -> Char)", EType $ ty @Bool ~> (ty @Int ~> ty @Char)) , ("Bool -> Int -> Char", EType $ ty @Bool ~> ty @Int ~> ty @Char) , ("Bool -> (Int -> Char) -> ()", EType $ ty @Bool ~> (ty @Int ~> ty @Char) ~> ty @()) , ("IO", EType $ ty @IO) , ("Eq", EType $ ty @Eq) , ("Eq Bool", EType $ ty @Eq :$ ty @Bool) , ("Traversable IO", EType $ ty @Traversable :$ ty @IO) , ("Monad IO", EType $ ty @Monad :$ ty @IO) , ("(->) Bool", EType $ ty @(->) :$ ty @Bool) , ("(->) (IO Bool)", EType $ ty @(->) :$ (ty @IO :$ ty @Bool)) , ("Monad IO", EType $ ty @Monad :$ ty @IO) ] , testGroup "Parsing errors" $ let (==>) inp _exp = testCase inp $ got @?= Left () where got :: Either () (TokType P.SourcePos) got = left (const ()) $ (`runParser` inp) $ unCF p p :: Gram_Type P.SourcePos p => CF p (TokType P.SourcePos) p = typeG <* eoi in uncurry (==>) <$> [ ("Bool, Int", ()) , ("(Bool -> Int) Char", ()) ] , testGroup "Compiling errors" $ let (==>) inp _exp = testCase inp $ got @?= Right (Left ()) where got :: Either (P.ParseError Char P.Dec) (Either () (EType Tys)) got = (left (const ()) . compile_etype <$>) $ (`runParser` inp) $ unCF p p :: Gram_Type P.SourcePos p => CF p (TokType P.SourcePos) p = typeG <* eoi in uncurry (==>) <$> [ ("NonExistingType", ()) , ("Bool Int", ()) , ("[IO]", ()) , ("(->) IO", ()) , ("(->) Bool Int Char", ()) , ("Monad Eq", ()) ] , testGroup "proj_con" $ let (==>) (typ::Type Constants (h::Constraint)) expected = testCase (show_type typ) $ isJust (proj_con typ) @?= expected in [ ty @Eq :$ ty @Bool ==> True , ty @Ord :$ ty @Bool ==> True , ty @Functor :$ ty @Maybe ==> True , ty @Functor :$ ty @IO ==> True , ty @Monad :$ ty @IO ==> True , ty @Traversable :$ ty @IO ==> False ] ]