symantic-lib/Language/Symantic/Typing/Test.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE UndecidableInstances #-}
   3 {-# OPTIONS_GHC -fno-warn-orphans #-}
   4 module Typing.Test where
   5
   6 import Test.Tasty
   7 import Test.Tasty.HUnit
   8
   9 import Control.Applicative (Applicative(..))
  10 import Control.Arrow (left)
  11 import Data.Functor.Identity (Identity(..))
  12 import Data.List.NonEmpty (NonEmpty)
  13 import Data.Map.Strict (Map)
  14 import Data.Maybe (isJust)
  15 import Data.NonNull (NonNull)
  16 import Data.Proxy
  17 import Data.Ratio (Ratio)
  18 import Data.Text (Text)
  19 import GHC.Exts (Constraint)
  20 import Prelude hiding (exp)
  21 import qualified Control.Monad.Classes.Run as MC
  22 import qualified Control.Monad.Trans.State.Strict as SS
  23 import qualified Data.Function as Fun
  24 import qualified Data.Map.Strict as Map
  25 import qualified Data.MonoTraversable as MT
  26 import qualified Data.Sequences as Seqs
  27 import qualified System.IO as IO
  28 import qualified Text.Megaparsec as P
  29 import qualified Text.Megaparsec.Prim as P
  30
  31 import Language.Symantic.Grammar
  32 import Language.Symantic
  33 import Language.Symantic.Lib hiding ((<$>), (<*), show)
  34
  35 import Grammar.Megaparsec ()
  36
  37 -- * Tests
  38 type SS =
  39  [ Proxy (->)
  40  , Proxy Bool
  41  , Proxy []
  42  , Proxy ()
  43  , Proxy (,)
  44  , Proxy Char
  45  , Proxy Either
  46  , Proxy Int
  47  , Proxy Integer
  48  , Proxy IO
  49  , Proxy IO.Handle
  50  , Proxy IO.IOMode
  51  , Proxy Ordering
  52  , Proxy Map
  53  , Proxy Maybe
  54  , Proxy NonNull
  55  , Proxy Ratio
  56  , Proxy Text
  57  , Proxy Applicative
  58  , Proxy Bounded
  59  , Proxy Enum
  60  , Proxy Eq
  61  , Proxy Foldable
  62  , Proxy Functor
  63  , Proxy Integral
  64  , Proxy Monad
  65  , Proxy Monoid
  66  , Proxy MT.MonoFoldable
  67  , Proxy MT.MonoFunctor
  68  , Proxy Num
  69  , Proxy Ord
  70  , Proxy Real
  71  , Proxy Seqs.IsSequence
  72  , Proxy Seqs.SemiSequence
  73  , Proxy Show
  74  , Proxy Traversable
  75  ]
  76 type SRC = SrcTe (NonEmpty P.SourcePos) SS
  77
  78 impsTy :: Imports NameTy
  79 impsTy = importTypes @SS []
  80
  81 modsTy :: Source src => ModulesTy src
  82 modsTy =
  83         Map.insert ([] `Mod` "String")
  84          (TypeTLen $ \len -> TypeT $
  85                 tyConstLen @(K [])   @[]   len `tyApp`
  86                 tyConstLen @(K Char) @Char len) $
  87         modulesTyInj @SS
  88
  89 parseTy ::
  90  forall src g err inp.
  91  g ~ P.ParsecT err inp (SS.StateT (Imports NameTy, ModulesTy src) Identity) =>
  92  P.MonadParsec err inp (P.ParsecT err inp g) =>
  93  Gram_Type src g =>
  94  P.Token inp ~ Char =>
  95  inp -> Either (P.ParseError Char err) (AST_Type src)
  96 parseTy inp =
  97         runIdentity $
  98         MC.evalStateStrict (impsTy, modsTy @src) $
  99         P.runParserT g "" inp
 100         where g = unCF $ g_type <* eoi
 101
 102 tests :: TestTree
 103 tests = testGroup "Typing" $
 104  [ testGroup "readType" $
 105         let run inp (TypeT exp :: TypeT SRC '[]) =
 106                 testCase inp $ got @?= Right (Right $ TypeVT exp)
 107                 where
 108                 got :: Either (P.ParseError Char P.Dec)
 109                               (Either (Error_Type SRC) (TypeVT SRC))
 110                 got = readType <$> parseTy inp
 111                 in
 112         let (==>) = run; infixr 0 ==> in
 113          [ "Bool"                        ==> TypeT $ tyBool
 114          , "(->) Bool"                   ==> TypeT $ tyFun `tyApp` tyBool
 115          , "[]"                          ==> TypeT $ tyConst @(K []) @[]
 116          , "[Char]"                      ==> TypeT $ tyList tyChar
 117          , "[Char -> [Char]]"            ==> TypeT $ tyList (tyChar ~> tyList tyChar)
 118          , "([])"                        ==> TypeT $ tyConst @(K []) @[]
 119          , "[()]"                        ==> TypeT $ tyList tyUnit
 120          , "()"                          ==> TypeT $ tyUnit
 121          , "(())"                        ==> TypeT $ tyUnit
 122          , "(,)"                         ==> TypeT $ tyConst @(K (,)) @(,)
 123          , "((,))"                       ==> TypeT $ tyConst @(K (,)) @(,)
 124          , "(,) Int"                     ==> TypeT $ tyConst @(K (,)) @(,) `tyApp` tyInt
 125          , "(Bool)"                      ==> TypeT $ tyBool
 126          , "((Bool))"                    ==> TypeT $ tyBool
 127          , "(Bool, Int)"                 ==> TypeT $ tyBool `tyTuple2` tyInt
 128          , "((Bool, Int))"               ==> TypeT $ tyBool `tyTuple2` tyInt
 129          , "((Bool, Int), Char)"         ==> TypeT $ (tyBool `tyTuple2` tyInt) `tyTuple2` tyChar
 130          , "(Bool, Int) -> Char"         ==> TypeT $ (tyBool `tyTuple2` tyInt) ~> tyChar
 131          , "(Bool -> Int)"               ==> TypeT $ tyBool ~> tyInt
 132          , "String"                      ==> TypeT $ tyList tyChar
 133          , "[Char] -> String"            ==> TypeT $ tyList tyChar ~> tyList tyChar
 134          , "String -> [Char]"            ==> TypeT $ tyList tyChar ~> tyList tyChar
 135          , "Maybe Bool"                  ==> TypeT $ tyMaybe tyBool
 136          , "Either Bool Int"             ==> TypeT $ tyEither tyBool tyInt
 137          , "Bool -> Int"                 ==> TypeT $ tyBool ~> tyInt
 138          , "(Bool -> Int) -> Char"       ==> TypeT $ (tyBool ~> tyInt) ~> tyChar
 139          , "Bool -> (Int -> Char)"       ==> TypeT $ tyBool ~> (tyInt ~> tyChar)
 140          , "Bool -> Int -> Char"         ==> TypeT $ tyBool ~> tyInt ~> tyChar
 141          , "Bool -> (Int -> Char) -> ()" ==> TypeT $ tyBool ~> (tyInt ~> tyChar) ~> tyUnit
 142          , "IO"                          ==> TypeT $ tyConst @(K IO) @IO
 143          , "Traversable IO"              ==> TypeT $ tyTraversable (tyConst @(K IO) @IO)
 144          , "Monad IO"                    ==> TypeT $ tyMonad (tyConst @(K IO) @IO)
 145          , "(->) (IO Bool)"              ==> TypeT $ tyConst @(K (->)) @(->) `tyApp` (tyIO tyBool)
 146          , "Monad IO"                    ==> TypeT $ tyMonad (tyConst @(K IO) @IO)
 147          , "Eq"                          ==> TypeT $ tyConst @(K Eq) @Eq
 148          , "Eq Bool"                     ==> TypeT $ tyEq tyBool
 149          ]
 150          , testGroup "Parsing errors" $
 151                 let run inp = testCase inp $ got @?= Left ()
 152                         where
 153                         got :: Either () (AST_Type SRC)
 154                         got = left (\(_::P.ParseError (P.Token String) P.Dec) -> ()) $ parseTy inp in
 155                 run <$>
 156                  [ "Bool, Int"
 157                  , "(Bool -> Int) Char"
 158                  , "NonExistingType"
 159                  ]
 160          , testGroup "Compiling errors" $
 161                 let run inp = testCase inp $ got @?= Right (Left ())
 162                         where
 163                         got :: Either (P.ParseError Char P.Dec) (Either () (TypeVT SRC))
 164                         got = left (Fun.const ()) . readType <$> parseTy inp in
 165                 run <$>
 166                  [ "Bool Int"
 167                  , "[IO]"
 168                  , "(->) IO"
 169                  , "(->) Bool Int Char"
 170                  , "Monad Eq"
 171                  ]
 172  , testGroup "proveConstraint" $
 173         let (==>) (typ::Type SRC SS (t::Constraint)) expected =
 174                 let imps = importTypes @SS [] in
 175                 let conf = config_Doc_Type{config_Doc_Type_imports = imps} in
 176                 testCase (showType conf typ) $
 177                 isJust (proveConstraint typ) @?= expected in
 178          [ tyEq          tyBool                      ==> True
 179          , tyOrd         tyBool                      ==> True
 180          , tyFunctor     (tyConst @(K Maybe) @Maybe) ==> True
 181          , tyFunctor     (tyConst @(K IO) @IO)       ==> True
 182          , tyMonad       (tyConst @(K IO) @IO)       ==> True
 183          , tyTraversable (tyConst @(K IO) @IO)       ==> False
 184          ]
 185  ]