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