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