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.Map.Strict (Map)
  11 import Data.Maybe (isJust)
  12 import Data.NonNull (NonNull)
  13 import Data.Proxy
  14 import Data.Ratio (Ratio)
  15 import Data.Text (Text)
  16 import GHC.Exts (Constraint)
  17 import Prelude hiding (exp)
  18 import qualified Data.Function as Fun
  19 import qualified Data.Map.Strict as Map
  20 import qualified Data.MonoTraversable as MT
  21 import qualified Data.Sequences as Seqs
  22 import qualified System.IO as IO
  23 import qualified Text.Megaparsec as P
  24
  25 import Language.Symantic.Grammar
  26 import Language.Symantic
  27 import Language.Symantic.Lib hiding ((<$>), (<*), show)
  28
  29 import Grammar.MegaParsec
  30
  31 -- * Tests
  32 type SS =
  33  [ Proxy (->)
  34  , Proxy Bool
  35  , Proxy []
  36  , Proxy ()
  37  , Proxy (,)
  38  , Proxy Char
  39  , Proxy Either
  40  , Proxy Int
  41  , Proxy Integer
  42  , Proxy IO
  43  , Proxy IO.Handle
  44  , Proxy IO.IOMode
  45  , Proxy Ordering
  46  , Proxy Map
  47  , Proxy Maybe
  48  , Proxy NonNull
  49  , Proxy Ratio
  50  , Proxy Text
  51  , Proxy Applicative
  52  , Proxy Bounded
  53  , Proxy Enum
  54  , Proxy Eq
  55  , Proxy Foldable
  56  , Proxy Functor
  57  , Proxy Integral
  58  , Proxy Monad
  59  , Proxy Monoid
  60  , Proxy MT.MonoFoldable
  61  , Proxy MT.MonoFunctor
  62  , Proxy Num
  63  , Proxy Ord
  64  , Proxy Real
  65  , Proxy Seqs.IsSequence
  66  , Proxy Seqs.SemiSequence
  67  , Proxy Show
  68  , Proxy Traversable
  69  ]
  70 type SRC = SrcTe P.SourcePos SS
  71 instance
  72  ( ParsecC e s
  73  , Gram_Meta (Text_of_Source src) (P.ParsecT e s m)
  74  , Inj_Source (Text_of_Source src) src
  75  ) => Gram_Type src (P.ParsecT e s m)
  76
  77 cs :: Source src => Name2Type src
  78 cs =
  79         Map.insert "String"
  80          (Len2Type $ \len -> TypeT $
  81                 tyConstLen @(K [])   @[]   len `tyApp`
  82                 tyConstLen @(K Char) @Char len) $
  83         inj_Name2Type (Proxy @SS)
  84
  85 tests :: TestTree
  86 tests = testGroup "Typing" $
  87  [ testGroup "readTy" $
  88         let run inp (TypeT exp :: TypeT SRC '[]) =
  89                 testCase inp $ got @?= Right (Right $ TypeVT exp)
  90                 where
  91                 got :: Either (P.ParseError Char P.Dec)
  92                               (Either (Error_Type SRC) (TypeVT SRC))
  93                 got = readTy cs <$> P.runParser (unCF g) "" inp
  94                 g :: Gram_Type SRC g => CF g (AST_Type SRC)
  95                 g = g_type <* eoi in
  96         let (==>) = run; infixr 0 ==> in
  97          [ "Bool"                        ==> TypeT $ tyBool
  98          , "(->) Bool"                   ==> TypeT $ tyFun `tyApp` tyBool
  99          , "[]"                          ==> TypeT $ tyConst @(K []) @[]
 100          , "[Char]"                      ==> TypeT $ tyList tyChar
 101          , "[Char -> [Char]]"            ==> TypeT $ tyList (tyChar ~> tyList tyChar)
 102          , "([])"                        ==> TypeT $ tyConst @(K []) @[]
 103          , "[()]"                        ==> TypeT $ tyList tyUnit
 104          , "()"                          ==> TypeT $ tyUnit
 105          , "(())"                        ==> TypeT $ tyUnit
 106          , "(,)"                         ==> TypeT $ tyConst @(K (,)) @(,)
 107          , "((,))"                       ==> TypeT $ tyConst @(K (,)) @(,)
 108          , "(,) Int"                     ==> TypeT $ tyConst @(K (,)) @(,) `tyApp` tyInt
 109          , "(Bool)"                      ==> TypeT $ tyBool
 110          , "((Bool))"                    ==> TypeT $ tyBool
 111          , "(Bool, Int)"                 ==> TypeT $ tyBool `tyTuple2` tyInt
 112          , "((Bool, Int))"               ==> TypeT $ tyBool `tyTuple2` tyInt
 113          , "((Bool, Int), Char)"         ==> TypeT $ (tyBool `tyTuple2` tyInt) `tyTuple2` tyChar
 114          , "(Bool, Int) -> Char"         ==> TypeT $ (tyBool `tyTuple2` tyInt) ~> tyChar
 115          , "(Bool -> Int)"               ==> TypeT $ tyBool ~> tyInt
 116          , "String"                      ==> TypeT $ tyList tyChar
 117          , "[Char] -> String"            ==> TypeT $ tyList tyChar ~> tyList tyChar
 118          , "String -> [Char]"            ==> TypeT $ tyList tyChar ~> tyList tyChar
 119          , "Maybe Bool"                  ==> TypeT $ tyMaybe tyBool
 120          , "Either Bool Int"             ==> TypeT $ tyEither tyBool tyInt
 121          , "Bool -> Int"                 ==> TypeT $ tyBool ~> tyInt
 122          , "(Bool -> Int) -> Char"       ==> TypeT $ (tyBool ~> tyInt) ~> tyChar
 123          , "Bool -> (Int -> Char)"       ==> TypeT $ tyBool ~> (tyInt ~> tyChar)
 124          , "Bool -> Int -> Char"         ==> TypeT $ tyBool ~> tyInt ~> tyChar
 125          , "Bool -> (Int -> Char) -> ()" ==> TypeT $ tyBool ~> (tyInt ~> tyChar) ~> tyUnit
 126          , "IO"                          ==> TypeT $ tyConst @(K IO) @IO
 127          , "Traversable IO"              ==> TypeT $ tyTraversable (tyConst @(K IO) @IO)
 128          , "Monad IO"                    ==> TypeT $ tyMonad (tyConst @(K IO) @IO)
 129          , "(->) (IO Bool)"              ==> TypeT $ tyConst @(K (->)) @(->) `tyApp` (tyIO tyBool)
 130          , "Monad IO"                    ==> TypeT $ tyMonad (tyConst @(K IO) @IO)
 131          , "Eq"                          ==> TypeT $ tyConst @(K Eq) @Eq
 132          , "Eq Bool"                     ==> TypeT $ tyEq tyBool
 133          ]
 134          , testGroup "Parsing errors" $
 135                 let run inp = testCase inp $ got @?= Left ()
 136                         where
 137                         got :: Either () (AST_Type SRC)
 138                         got = left (\(_::P.ParseError (P.Token String) P.Dec) -> ()) $ P.runParser (unCF g) "" inp
 139                         g :: Gram_Type SRC g => CF g (AST_Type SRC)
 140                         g = g_type <* eoi in
 141                 run <$>
 142                  [ "Bool, Int"
 143                  , "(Bool -> Int) Char"
 144                  ]
 145          , testGroup "Compiling errors" $
 146                 let run inp = testCase inp $ got @?= Right (Left ())
 147                         where
 148                         got :: Either (P.ParseError Char P.Dec) (Either () (TypeVT SRC))
 149                         got = left (Fun.const ()) . readTy cs <$> P.runParser (unCF g) "" inp
 150                         g :: Gram_Type SRC g => CF g (AST_Type SRC)
 151                         g = g_type <* eoi in
 152                 run <$>
 153                  [ "NonExistingType"
 154                  , "Bool Int"
 155                  , "[IO]"
 156                  , "(->) IO"
 157                  , "(->) Bool Int Char"
 158                  , "Monad Eq"
 159                  ]
 160  , testGroup "proveConstraint" $
 161         let (==>) (typ::Type SRC '[] (t::Constraint)) expected =
 162                 testCase (show typ) $
 163                 isJust (proveConstraint typ) @?= expected in
 164          [ tyEq          tyBool                      ==> True
 165          , tyOrd         tyBool                      ==> True
 166          , tyFunctor     (tyConst @(K Maybe) @Maybe) ==> True
 167          , tyFunctor     (tyConst @(K IO) @IO)       ==> True
 168          , tyMonad       (tyConst @(K IO) @IO)       ==> True
 169          , tyTraversable (tyConst @(K IO) @IO)       ==> False
 170          ]
 171  ]