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.Grammar
  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.Grammar.Test
  23
  24 -- * Tests
  25 type Tys = Constants ++ '[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 (==>) 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 <$>) $ (`runParser` inp) $ unCF p
  40                 p :: Gram_Type P.SourcePos p => CF p (TokType P.SourcePos)
  41                 p = typeG <* eoi in
  42         uncurry (==>) <$>
  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 (==>) inp _exp = testCase inp $ got @?= Left ()
  82                         where
  83                         got :: Either () (TokType P.SourcePos)
  84                         got = left (const ()) $ (`runParser` inp) $ unCF p
  85                         p :: Gram_Type P.SourcePos p => CF p (TokType P.SourcePos)
  86                         p = typeG <* eoi in
  87                 uncurry (==>) <$>
  88                  [ ("Bool, Int", ())
  89                  , ("(Bool -> Int) Char", ())
  90                  ]
  91          , testGroup "Compiling errors" $
  92                 let (==>) inp _exp = testCase inp $ got @?= Right (Left ())
  93                         where
  94                         got :: Either (P.ParseError Char P.Dec) (Either () (EType Tys))
  95                         got = (left (const ()) . compile_etype <$>) $ (`runParser` inp) $ unCF p
  96                         p :: Gram_Type P.SourcePos p => CF p (TokType P.SourcePos)
  97                         p = typeG <* eoi in
  98                 uncurry (==>) <$>
  99                  [ ("NonExistingType", ())
 100                  , ("Bool Int", ())
 101                  , ("[IO]", ())
 102                  , ("(->) IO", ())
 103                  , ("(->) Bool Int Char", ())
 104                  , ("Monad Eq", ())
 105                  ]
 106  , testGroup "proj_con" $
 107         let (==>) (typ::Type Constants (h::Constraint)) expected =
 108                 testCase (show_type typ) $
 109                 isJust (proj_con 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  ]