Language/Symantic/Typing/Test.hs

   1 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   3 {-# LANGUAGE NoMonomorphismRestriction #-}
   4 {-# LANGUAGE StandaloneDeriving #-}
   5 {-# LANGUAGE TypeInType #-}
   6 {-# OPTIONS_GHC -fno-warn-orphans #-}
   7 module Typing.Test where
   8
   9 import Test.Tasty
  10 import Test.Tasty.HUnit
  11
  12 import Control.Applicative (Applicative(..), Alternative(..))
  13 import Control.Arrow (left)
  14 import qualified Data.Char as Char
  15 import Data.Functor.Identity
  16 import Data.Maybe (isJust)
  17 import Data.Proxy
  18 import Data.Semigroup ((<>))
  19 import Data.Text (Text)
  20 import qualified Data.Text as Text
  21 import qualified Data.Text.IO as Text
  22 import GHC.Exts (Constraint)
  23 import Prelude hiding (exp)
  24 import qualified Text.Megaparsec as P
  25 import qualified Text.Megaparsec.Lexer as L
  26
  27 import Language.Symantic.Lib.Data.Type.List
  28 import Language.Symantic.Parsing
  29 import Language.Symantic.Parsing.Grammar
  30 import Language.Symantic.Typing
  31 import Language.Symantic.Compiling ((~>))
  32
  33 import Parsing.Test
  34 import Parsing.Grammar.Test
  35
  36 -- * Tests
  37 type Tys = Constants ++ '[Proxy String]
  38
  39 tests :: TestTree
  40 tests = testGroup "Typing" $
  41  [ testGroup "compile_type" $
  42         let (==>) inp exp = testCase inp $ got @?= Right (Right (exp::EType Tys))
  43                 where got = (compile_etype <$>) $ (`runParser` inp) $ unCF $ typeP <* eof in
  44         uncurry (==>) <$>
  45          [ ("Bool", EType $ ty @Bool)
  46          , ("[]", EType $ ty @[])
  47          , ("[Char]", EType $ ty @[] :$ ty @Char)
  48          , ("([])", EType $ ty @[])
  49          , ("[()]", EType $ ty @[] :$ ty @())
  50          , ("()", EType $ ty @())
  51          , ("(())", EType $ ty @())
  52          , ("(,)", EType $ ty @(,))
  53          , ("((,))", EType $ ty @(,))
  54          , ("(,) Int", EType $ ty @(,) :$ ty @Int)
  55          , ("(Bool)", EType $ ty @Bool)
  56          , ("((Bool))", EType $ ty @Bool)
  57          , ("(Bool, Int)", EType $ ty @(,) :$ ty @Bool :$ ty @Int)
  58          , ("((Bool, Int))", EType $ ty @(,) :$ ty @Bool :$ ty @Int)
  59          , ("((Bool, Int), Char)", EType $ ty @(,) :$ (ty @(,) :$ ty @Bool :$ ty @Int) :$ ty @Char)
  60          , ("(Bool, Int) -> Char", EType $ (ty @(,) :$ ty @Bool :$ ty @Int) ~> ty @Char)
  61          , ("(Bool -> Int)", EType $ ty @Bool ~> ty @Int)
  62          , ("String", EType $ ty @[] :$ ty @Char)
  63          , ("[Char] -> String", EType $ (ty @[] :$ ty @Char) ~> (ty @[] :$ ty @Char))
  64          , ("String -> [Char]", EType $ (ty @[] :$ ty @Char) ~> (ty @[] :$ ty @Char))
  65          , ("Maybe Bool", EType $ ty @Maybe :$ ty @Bool)
  66          , ("Either Bool Int", EType $ ty @Either :$ ty @Bool :$ ty @Int)
  67          , ("Bool -> Int", EType $ ty @Bool ~> ty @Int)
  68          , ("(Bool -> Int) -> Char", EType $ (ty @Bool ~> ty @Int) ~> ty @Char)
  69          , ("Bool -> (Int -> Char)", EType $ ty @Bool ~> (ty @Int ~> ty @Char))
  70          , ("Bool -> Int -> Char", EType $ ty @Bool ~> ty @Int ~> ty @Char)
  71          , ("Bool -> (Int -> Char) -> ()", EType $ ty @Bool ~> (ty @Int ~> ty @Char) ~> ty @())
  72          , ("IO", EType $ ty @IO)
  73          , ("Eq", EType $ ty @Eq)
  74          , ("Eq Bool", EType $ ty @Eq :$ ty @Bool)
  75          , ("Traversable IO", EType $ ty @Traversable :$ ty @IO)
  76          , ("Monad IO", EType $ ty @Monad :$ ty @IO)
  77          , ("(->) Bool", EType $ ty @(->) :$ ty @Bool)
  78          , ("(->) (IO Bool)", EType $ ty @(->) :$ (ty @IO :$ ty @Bool))
  79          , ("Monad IO", EType $ ty @Monad :$ ty @IO)
  80          ]
  81          , testGroup "Parsing errors" $
  82                 let (==>) inp _exp = testCase inp $ got @?= Left ()
  83                         where got = left (const ()) $ (`runParser` inp) $ unCF $ typeP <* eof in
  84                 uncurry (==>) <$>
  85                  [ ("Bool, Int", ())
  86                  , ("(Bool -> Int) Char", ())
  87                  ]
  88          , testGroup "Compiling errors" $
  89                 let (==>) inp _exp = testCase inp $ got @?= Right (Left () :: Either () (EType Tys))
  90                         where got = (left (const ()) . compile_etype <$>) $
  91                                 (`runParser` inp) $ unCF $ typeP <* eof in
  92                 uncurry (==>) <$>
  93                  [ ("NonExistingType", ())
  94                  , ("Bool Int", ())
  95                  , ("[IO]", ())
  96                  , ("(->) IO", ())
  97                  , ("(->) Bool Int Char", ())
  98                  , ("Monad Eq", ())
  99                  ]
 100  , testGroup "proj_con" $
 101         let (==>) (typ::Type Constants (h::Constraint)) expected =
 102                 testCase (show_type typ) $
 103                 isJust (proj_con typ) @?= expected in
 104          [ ty @Eq :$ ty @Bool ==> True
 105          , ty @Ord :$ ty @Bool ==> True
 106          , ty @Functor :$ ty @Maybe ==> True
 107          , ty @Functor :$ ty @IO ==> True
 108          , ty @Monad :$ ty @IO ==> True
 109          , ty @Traversable :$ ty @IO ==> False
 110          ]
 111  ]