symantic-lib/Language/Symantic/Typing/Test.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 module Typing.Test where
   4
   5 import Test.Tasty
   6 import Test.Tasty.HUnit
   7
   8 import Control.Applicative (Applicative(..))
   9 import Control.Arrow (left)
  10 import Data.Maybe (isJust)
  11 import Data.Proxy
  12 import GHC.Exts (Constraint)
  13 import Prelude hiding (exp)
  14 import qualified Text.Megaparsec as P
  15
  16 import Language.Symantic.Parsing
  17 import Language.Symantic.Typing
  18 import Language.Symantic.Lib ()
  19 import Language.Symantic.Lib.Lambda ((~>))
  20 import Language.Symantic.Helper.Data.Type.List
  21
  22 import Parsing.Test
  23
  24 -- * Tests
  25 type Tys = TyConsts ++ '[Proxy String]
  26 instance
  27  ( ParsecC e s
  28  , Gram_Meta meta (P.ParsecT e s m)
  29  ) => Gram_Type meta (P.ParsecT e s m)
  30
  31 tests :: TestTree
  32 tests = testGroup "Typing" $
  33  [ testGroup "compile_Type" $
  34         let run inp exp = testCase inp $ got @?= Right (Right exp)
  35                 where
  36                 got :: Either (P.ParseError Char P.Dec)
  37                               (Either (Error_Type P.SourcePos '[Proxy Token_Type])
  38                                       (EType Tys))
  39                 got = compile_EType <$> P.runParser (unCF g) "" inp
  40                 g :: Gram_Type P.SourcePos g => CF g (TokType P.SourcePos)
  41                 g = typeG <* eoi in
  42         let (==>) = run; infixr 0 ==> in
  43          [ "Bool"                        ==> EType $ ty @Bool
  44          , "[]"                          ==> EType $ ty @[]
  45          , "[Char]"                      ==> EType $ ty @[] :$ ty @Char
  46          , "[Char -> [Char]]"            ==> EType $ ty @[] :$ (ty @Char ~> ty @[] :$ ty @Char)
  47          , "([])"                        ==> EType $ ty @[]
  48          , "[()]"                        ==> EType $ ty @[] :$ ty @()
  49          , "()"                          ==> EType $ ty @()
  50          , "(())"                        ==> EType $ ty @()
  51          , "(,)"                         ==> EType $ ty @(,)
  52          , "((,))"                       ==> EType $ ty @(,)
  53          , "(,) Int"                     ==> EType $ ty @(,) :$ ty @Int
  54          , "(Bool)"                      ==> EType $ ty @Bool
  55          , "((Bool))"                    ==> EType $ ty @Bool
  56          , "(Bool, Int)"                 ==> EType $ ty @(,) :$ ty @Bool :$ ty @Int
  57          , "((Bool, Int))"               ==> EType $ ty @(,) :$ ty @Bool :$ ty @Int
  58          , "((Bool, Int), Char)"         ==> EType $ ty @(,) :$ (ty @(,) :$ ty @Bool :$ ty @Int) :$ ty @Char
  59          , "(Bool, Int) -> Char"         ==> EType $ (ty @(,) :$ ty @Bool :$ ty @Int) ~> ty @Char
  60          , "(Bool -> Int)"               ==> EType $ ty @Bool ~> ty @Int
  61          , "String"                      ==> EType $ ty @[] :$ ty @Char
  62          , "[Char] -> String"            ==> EType $ ty @[] :$ ty @Char ~> ty @[] :$ ty @Char
  63          , "String -> [Char]"            ==> EType $ ty @[] :$ ty @Char ~> ty @[] :$ ty @Char
  64          , "Maybe Bool"                  ==> EType $ ty @Maybe :$ ty @Bool
  65          , "Either Bool Int"             ==> EType $ ty @Either :$ ty @Bool :$ ty @Int
  66          , "Bool -> Int"                 ==> EType $ ty @Bool ~> ty @Int
  67          , "(Bool -> Int) -> Char"       ==> EType $ (ty @Bool ~> ty @Int) ~> ty @Char
  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) ~> ty @()
  71          , "IO"                          ==> EType $ ty @IO
  72          , "Eq"                          ==> EType $ ty @Eq
  73          , "Eq Bool"                     ==> EType $ ty @Eq :$ ty @Bool
  74          , "Traversable IO"              ==> EType $ ty @Traversable :$ ty @IO
  75          , "Monad IO"                    ==> EType $ ty @Monad :$ ty @IO
  76          , "(->) Bool"                   ==> EType $ ty @(->) :$ ty @Bool
  77          , "(->) (IO Bool)"              ==> EType $ ty @(->) :$ (ty @IO :$ ty @Bool)
  78          , "Monad IO"                    ==> EType $ ty @Monad :$ ty @IO
  79          ]
  80          , testGroup "Parsing errors" $
  81                 let run inp = testCase inp $ got @?= Left ()
  82                         where
  83                         got :: Either () (TokType P.SourcePos)
  84                         got = left (\(_::P.ParseError (P.Token String) P.Dec) -> ()) $ P.runParser (unCF g) "" inp
  85                         g :: Gram_Type P.SourcePos g => CF g (TokType P.SourcePos)
  86                         g = typeG <* eoi in
  87                 run <$>
  88                  [ "Bool, Int"
  89                  , "(Bool -> Int) Char"
  90                  ]
  91          , testGroup "Compiling errors" $
  92                 let run inp = testCase inp $ got @?= Right (Left ())
  93                         where
  94                         got :: Either (P.ParseError Char P.Dec) (Either () (EType Tys))
  95                         got = left (const ()) . compile_EType <$> P.runParser (unCF g) "" inp
  96                         g :: Gram_Type P.SourcePos g => CF g (TokType P.SourcePos)
  97                         g = typeG <* eoi in
  98                 run <$>
  99                  [ "NonExistingType"
 100                  , "Bool Int"
 101                  , "[IO]"
 102                  , "(->) IO"
 103                  , "(->) Bool Int Char"
 104                  , "Monad Eq"
 105                  ]
 106  , testGroup "proj_TyCon" $
 107         let (==>) (typ::Type TyConsts (h::Constraint)) expected =
 108                 testCase (show_Type typ) $
 109                 isJust (proj_TyCon typ) @?= expected in
 110          [ ty @Eq          :$ ty @Bool  ==> True
 111          , ty @Ord         :$ ty @Bool  ==> True
 112          , ty @Functor     :$ ty @Maybe ==> True
 113          , ty @Functor     :$ ty @IO    ==> True
 114          , ty @Monad       :$ ty @IO    ==> True
 115          , ty @Traversable :$ ty @IO    ==> False
 116          ]
 117  ]