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

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