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 instance
  73  ( ParsecC e s
  74  , Gram_Source src (P.ParsecT e s m)
  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  ]