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 impsTy :: Imports NameTy
  74 impsTy = importTypes @SS []
  75
  76 modsTy :: Source src => ModulesTy src
  77 modsTy =
  78         Map.insert ([] `Mod` "String")
  79          (TypeTLen $ \len -> TypeT $
  80                 tyConstLen @(K [])   @[]   len `tyApp`
  81                 tyConstLen @(K Char) @Char len) $
  82         modulesTyInj @SS
  83
  84 tests :: TestTree
  85 tests = testGroup "Typing" $
  86  [ testGroup "readType" $
  87         let run inp (TypeT exp :: TypeT SRC '[]) =
  88                 testCase inp $ got @?= Right (Right $ TypeVT exp)
  89                 where
  90                 got :: Either (P.ParseError Char P.Dec)
  91                               (Either (Error_Type SRC) (TypeVT SRC))
  92                 got = readType impsTy modsTy <$> P.runParser (unCF g) "" inp
  93                 g :: Gram_Type SRC g => CF g (AST_Type SRC)
  94                 g = g_type <* eoi in
  95         let (==>) = run; infixr 0 ==> in
  96          [ "Bool"                        ==> TypeT $ tyBool
  97          , "(->) Bool"                   ==> TypeT $ tyFun `tyApp` tyBool
  98          , "[]"                          ==> TypeT $ tyConst @(K []) @[]
  99          , "[Char]"                      ==> TypeT $ tyList tyChar
 100          , "[Char -> [Char]]"            ==> TypeT $ tyList (tyChar ~> tyList tyChar)
 101          , "([])"                        ==> TypeT $ tyConst @(K []) @[]
 102          , "[()]"                        ==> TypeT $ tyList tyUnit
 103          , "()"                          ==> TypeT $ tyUnit
 104          , "(())"                        ==> TypeT $ tyUnit
 105          , "(,)"                         ==> TypeT $ tyConst @(K (,)) @(,)
 106          , "((,))"                       ==> TypeT $ tyConst @(K (,)) @(,)
 107          , "(,) Int"                     ==> TypeT $ tyConst @(K (,)) @(,) `tyApp` tyInt
 108          , "(Bool)"                      ==> TypeT $ tyBool
 109          , "((Bool))"                    ==> TypeT $ tyBool
 110          , "(Bool, Int)"                 ==> TypeT $ tyBool `tyTuple2` tyInt
 111          , "((Bool, Int))"               ==> TypeT $ tyBool `tyTuple2` tyInt
 112          , "((Bool, Int), Char)"         ==> TypeT $ (tyBool `tyTuple2` tyInt) `tyTuple2` tyChar
 113          , "(Bool, Int) -> Char"         ==> TypeT $ (tyBool `tyTuple2` tyInt) ~> tyChar
 114          , "(Bool -> Int)"               ==> TypeT $ tyBool ~> tyInt
 115          , "String"                      ==> TypeT $ tyList tyChar
 116          , "[Char] -> String"            ==> TypeT $ tyList tyChar ~> tyList tyChar
 117          , "String -> [Char]"            ==> TypeT $ tyList tyChar ~> tyList tyChar
 118          , "Maybe Bool"                  ==> TypeT $ tyMaybe tyBool
 119          , "Either Bool Int"             ==> TypeT $ tyEither tyBool tyInt
 120          , "Bool -> Int"                 ==> TypeT $ tyBool ~> tyInt
 121          , "(Bool -> Int) -> Char"       ==> TypeT $ (tyBool ~> tyInt) ~> tyChar
 122          , "Bool -> (Int -> Char)"       ==> TypeT $ tyBool ~> (tyInt ~> tyChar)
 123          , "Bool -> Int -> Char"         ==> TypeT $ tyBool ~> tyInt ~> tyChar
 124          , "Bool -> (Int -> Char) -> ()" ==> TypeT $ tyBool ~> (tyInt ~> tyChar) ~> tyUnit
 125          , "IO"                          ==> TypeT $ tyConst @(K IO) @IO
 126          , "Traversable IO"              ==> TypeT $ tyTraversable (tyConst @(K IO) @IO)
 127          , "Monad IO"                    ==> TypeT $ tyMonad (tyConst @(K IO) @IO)
 128          , "(->) (IO Bool)"              ==> TypeT $ tyConst @(K (->)) @(->) `tyApp` (tyIO tyBool)
 129          , "Monad IO"                    ==> TypeT $ tyMonad (tyConst @(K IO) @IO)
 130          , "Eq"                          ==> TypeT $ tyConst @(K Eq) @Eq
 131          , "Eq Bool"                     ==> TypeT $ tyEq tyBool
 132          ]
 133          , testGroup "Parsing errors" $
 134                 let run inp = testCase inp $ got @?= Left ()
 135                         where
 136                         got :: Either () (AST_Type SRC)
 137                         got = left (\(_::P.ParseError (P.Token String) P.Dec) -> ()) $ P.runParser (unCF g) "" inp
 138                         g :: Gram_Type SRC g => CF g (AST_Type SRC)
 139                         g = g_type <* eoi in
 140                 run <$>
 141                  [ "Bool, Int"
 142                  , "(Bool -> Int) Char"
 143                  ]
 144          , testGroup "Compiling errors" $
 145                 let run inp = testCase inp $ got @?= Right (Left ())
 146                         where
 147                         got :: Either (P.ParseError Char P.Dec) (Either () (TypeVT SRC))
 148                         got = left (Fun.const ()) . readType impsTy modsTy <$> P.runParser (unCF g) "" inp
 149                         g :: Gram_Type SRC g => CF g (AST_Type SRC)
 150                         g = g_type <* eoi in
 151                 run <$>
 152                  [ "NonExistingType"
 153                  , "Bool Int"
 154                  , "[IO]"
 155                  , "(->) IO"
 156                  , "(->) Bool Int Char"
 157                  , "Monad Eq"
 158                  ]
 159  , testGroup "proveConstraint" $
 160         let (==>) (typ::Type SRC SS (t::Constraint)) expected =
 161                 let imps = importTypes @SS [] in
 162                 let conf = config_Doc_Type{config_Doc_Type_imports = imps} in
 163                 testCase (showType conf typ) $
 164                 isJust (proveConstraint typ) @?= expected in
 165          [ tyEq          tyBool                      ==> True
 166          , tyOrd         tyBool                      ==> True
 167          , tyFunctor     (tyConst @(K Maybe) @Maybe) ==> True
 168          , tyFunctor     (tyConst @(K IO) @IO)       ==> True
 169          , tyMonad       (tyConst @(K IO) @IO)       ==> True
 170          , tyTraversable (tyConst @(K IO) @IO)       ==> False
 171          ]
 172  ]