symantic-lib/test/HUnit/Typing.hs

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