+{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Typing.Test where
import Control.Applicative (Applicative(..))
import Control.Arrow (left)
+import Data.Functor.Identity (Identity(..))
+import Data.List.NonEmpty (NonEmpty)
+import Data.Map.Strict (Map)
import Data.Maybe (isJust)
+import Data.NonNull (NonNull)
import Data.Proxy
+import Data.Ratio (Ratio)
+import Data.Text (Text)
import GHC.Exts (Constraint)
import Prelude hiding (exp)
+import qualified Control.Monad.Classes.Run as MC
+import qualified Control.Monad.Trans.State.Strict as SS
+import qualified Data.Function as Fun
+import qualified Data.Map.Strict as Map
+import qualified Data.MonoTraversable as MT
+import qualified Data.Sequences as Seqs
+import qualified System.IO as IO
import qualified Text.Megaparsec as P
+import qualified Text.Megaparsec.Prim as P
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Lib ()
-import Language.Symantic.Lib.Lambda ((~>))
-import Language.Symantic.Helper.Data.Type.List
+import Language.Symantic.Grammar
+import Language.Symantic
+import Language.Symantic.Lib hiding ((<$>), (<*), show)
-import Parsing.Test
+import Grammar.Megaparsec ()
-- * Tests
-type Tys = Constants ++ '[Proxy String]
-instance
- ( ParsecC e s
- , Gram_Meta meta (P.ParsecT e s m)
- ) => Gram_Type meta (P.ParsecT e s m)
+type SS =
+ [ Proxy (->)
+ , Proxy Bool
+ , Proxy []
+ , Proxy ()
+ , Proxy (,)
+ , Proxy Char
+ , Proxy Either
+ , Proxy Int
+ , Proxy Integer
+ , Proxy IO
+ , Proxy IO.Handle
+ , Proxy IO.IOMode
+ , Proxy Ordering
+ , Proxy Map
+ , Proxy Maybe
+ , Proxy NonNull
+ , Proxy Ratio
+ , Proxy Text
+ , Proxy Applicative
+ , Proxy Bounded
+ , Proxy Enum
+ , Proxy Eq
+ , Proxy Foldable
+ , Proxy Functor
+ , Proxy Integral
+ , Proxy Monad
+ , Proxy Monoid
+ , Proxy MT.MonoFoldable
+ , Proxy MT.MonoFunctor
+ , Proxy Num
+ , Proxy Ord
+ , Proxy Real
+ , Proxy Seqs.IsSequence
+ , Proxy Seqs.SemiSequence
+ , Proxy Show
+ , Proxy Traversable
+ ]
+type SRC = SrcTe (NonEmpty P.SourcePos) SS
+
+impsTy :: Imports NameTy
+impsTy = importTypes @SS []
+
+modsTy :: Source src => ModulesTy src
+modsTy =
+ Map.insert ([] `Mod` "String")
+ (TypeTLen $ \len -> TypeT $
+ tyConstLen @(K []) @[] len `tyApp`
+ tyConstLen @(K Char) @Char len) $
+ modulesTyInj @SS
+
+parseTy ::
+ forall src g err inp.
+ g ~ P.ParsecT err inp (SS.StateT (Imports NameTy, ModulesTy src) Identity) =>
+ P.MonadParsec err inp (P.ParsecT err inp g) =>
+ Gram_Type src g =>
+ P.Token inp ~ Char =>
+ inp -> Either (P.ParseError Char err) (AST_Type src)
+parseTy inp =
+ runIdentity $
+ MC.evalStateStrict (impsTy, modsTy @src) $
+ P.runParserT g "" inp
+ where g = unCF $ g_type <* eoi
tests :: TestTree
tests = testGroup "Typing" $
- [ testGroup "compile_Type" $
- let run inp exp = testCase inp $ got @?= Right (Right exp)
+ [ testGroup "readType" $
+ let run inp (TypeT exp :: TypeT SRC '[]) =
+ testCase inp $ got @?= Right (Right $ TypeVT exp)
where
got :: Either (P.ParseError Char P.Dec)
- (Either (Error_Type P.SourcePos '[Proxy Token_Type])
- (EType Tys))
- got = compile_EType <$> P.runParser (unCF g) "" inp
- g :: Gram_Type P.SourcePos g => CF g (TokType P.SourcePos)
- g = typeG <* eoi in
+ (Either (Error_Type SRC) (TypeVT SRC))
+ got = readType <$> parseTy inp
+ in
let (==>) = run; infixr 0 ==> in
- [ "Bool" ==> EType $ ty @Bool
- , "[]" ==> EType $ ty @[]
- , "[Char]" ==> EType $ ty @[] :$ ty @Char
- , "[Char -> [Char]]" ==> EType $ ty @[] :$ (ty @Char ~> ty @[] :$ ty @Char)
- , "([])" ==> EType $ ty @[]
- , "[()]" ==> EType $ ty @[] :$ ty @()
- , "()" ==> EType $ ty @()
- , "(())" ==> EType $ ty @()
- , "(,)" ==> EType $ ty @(,)
- , "((,))" ==> EType $ ty @(,)
- , "(,) Int" ==> EType $ ty @(,) :$ ty @Int
- , "(Bool)" ==> EType $ ty @Bool
- , "((Bool))" ==> EType $ ty @Bool
- , "(Bool, Int)" ==> EType $ ty @(,) :$ ty @Bool :$ ty @Int
- , "((Bool, Int))" ==> EType $ ty @(,) :$ ty @Bool :$ ty @Int
- , "((Bool, Int), Char)" ==> EType $ ty @(,) :$ (ty @(,) :$ ty @Bool :$ ty @Int) :$ ty @Char
- , "(Bool, Int) -> Char" ==> EType $ (ty @(,) :$ ty @Bool :$ ty @Int) ~> ty @Char
- , "(Bool -> Int)" ==> EType $ ty @Bool ~> ty @Int
- , "String" ==> EType $ ty @[] :$ ty @Char
- , "[Char] -> String" ==> EType $ ty @[] :$ ty @Char ~> ty @[] :$ ty @Char
- , "String -> [Char]" ==> EType $ ty @[] :$ ty @Char ~> ty @[] :$ ty @Char
- , "Maybe Bool" ==> EType $ ty @Maybe :$ ty @Bool
- , "Either Bool Int" ==> EType $ ty @Either :$ ty @Bool :$ ty @Int
- , "Bool -> Int" ==> EType $ ty @Bool ~> ty @Int
- , "(Bool -> Int) -> Char" ==> EType $ (ty @Bool ~> ty @Int) ~> ty @Char
- , "Bool -> (Int -> Char)" ==> EType $ ty @Bool ~> (ty @Int ~> ty @Char)
- , "Bool -> Int -> Char" ==> EType $ ty @Bool ~> ty @Int ~> ty @Char
- , "Bool -> (Int -> Char) -> ()" ==> EType $ ty @Bool ~> (ty @Int ~> ty @Char) ~> ty @()
- , "IO" ==> EType $ ty @IO
- , "Eq" ==> EType $ ty @Eq
- , "Eq Bool" ==> EType $ ty @Eq :$ ty @Bool
- , "Traversable IO" ==> EType $ ty @Traversable :$ ty @IO
- , "Monad IO" ==> EType $ ty @Monad :$ ty @IO
- , "(->) Bool" ==> EType $ ty @(->) :$ ty @Bool
- , "(->) (IO Bool)" ==> EType $ ty @(->) :$ (ty @IO :$ ty @Bool)
- , "Monad IO" ==> EType $ ty @Monad :$ ty @IO
+ [ "Bool" ==> TypeT $ tyBool
+ , "(->) Bool" ==> TypeT $ tyFun `tyApp` tyBool
+ , "[]" ==> TypeT $ tyConst @(K []) @[]
+ , "[Char]" ==> TypeT $ tyList tyChar
+ , "[Char -> [Char]]" ==> TypeT $ tyList (tyChar ~> tyList tyChar)
+ , "([])" ==> TypeT $ tyConst @(K []) @[]
+ , "[()]" ==> TypeT $ tyList tyUnit
+ , "()" ==> TypeT $ tyUnit
+ , "(())" ==> TypeT $ tyUnit
+ , "(,)" ==> TypeT $ tyConst @(K (,)) @(,)
+ , "((,))" ==> TypeT $ tyConst @(K (,)) @(,)
+ , "(,) Int" ==> TypeT $ tyConst @(K (,)) @(,) `tyApp` tyInt
+ , "(Bool)" ==> TypeT $ tyBool
+ , "((Bool))" ==> TypeT $ tyBool
+ , "(Bool, Int)" ==> TypeT $ tyBool `tyTuple2` tyInt
+ , "((Bool, Int))" ==> TypeT $ tyBool `tyTuple2` tyInt
+ , "((Bool, Int), Char)" ==> TypeT $ (tyBool `tyTuple2` tyInt) `tyTuple2` tyChar
+ , "(Bool, Int) -> Char" ==> TypeT $ (tyBool `tyTuple2` tyInt) ~> tyChar
+ , "(Bool -> Int)" ==> TypeT $ tyBool ~> tyInt
+ , "String" ==> TypeT $ tyList tyChar
+ , "[Char] -> String" ==> TypeT $ tyList tyChar ~> tyList tyChar
+ , "String -> [Char]" ==> TypeT $ tyList tyChar ~> tyList tyChar
+ , "Maybe Bool" ==> TypeT $ tyMaybe tyBool
+ , "Either Bool Int" ==> TypeT $ tyEither tyBool tyInt
+ , "Bool -> Int" ==> TypeT $ tyBool ~> tyInt
+ , "(Bool -> Int) -> Char" ==> TypeT $ (tyBool ~> tyInt) ~> tyChar
+ , "Bool -> (Int -> Char)" ==> TypeT $ tyBool ~> (tyInt ~> tyChar)
+ , "Bool -> Int -> Char" ==> TypeT $ tyBool ~> tyInt ~> tyChar
+ , "Bool -> (Int -> Char) -> ()" ==> TypeT $ tyBool ~> (tyInt ~> tyChar) ~> tyUnit
+ , "IO" ==> TypeT $ tyConst @(K IO) @IO
+ , "Traversable IO" ==> TypeT $ tyTraversable (tyConst @(K IO) @IO)
+ , "Monad IO" ==> TypeT $ tyMonad (tyConst @(K IO) @IO)
+ , "(->) (IO Bool)" ==> TypeT $ tyConst @(K (->)) @(->) `tyApp` (tyIO tyBool)
+ , "Monad IO" ==> TypeT $ tyMonad (tyConst @(K IO) @IO)
+ , "Eq" ==> TypeT $ tyConst @(K Eq) @Eq
+ , "Eq Bool" ==> TypeT $ tyEq tyBool
]
, testGroup "Parsing errors" $
let run inp = testCase inp $ got @?= Left ()
where
- got :: Either () (TokType P.SourcePos)
- got = left (\(_::P.ParseError (P.Token String) P.Dec) -> ()) $ P.runParser (unCF g) "" inp
- g :: Gram_Type P.SourcePos g => CF g (TokType P.SourcePos)
- g = typeG <* eoi in
+ got :: Either () (AST_Type SRC)
+ got = left (\(_::P.ParseError (P.Token String) P.Dec) -> ()) $ parseTy inp in
run <$>
[ "Bool, Int"
, "(Bool -> Int) Char"
+ , "NonExistingType"
]
, testGroup "Compiling errors" $
let run inp = testCase inp $ got @?= Right (Left ())
where
- got :: Either (P.ParseError Char P.Dec) (Either () (EType Tys))
- got = left (const ()) . compile_EType <$> P.runParser (unCF g) "" inp
- g :: Gram_Type P.SourcePos g => CF g (TokType P.SourcePos)
- g = typeG <* eoi in
+ got :: Either (P.ParseError Char P.Dec) (Either () (TypeVT SRC))
+ got = left (Fun.const ()) . readType <$> parseTy inp in
run <$>
- [ "NonExistingType"
- , "Bool Int"
+ [ "Bool Int"
, "[IO]"
, "(->) IO"
, "(->) Bool Int Char"
, "Monad Eq"
]
- , testGroup "proj_TyCon" $
- let (==>) (typ::Type Constants (h::Constraint)) expected =
- testCase (show_Type typ) $
- isJust (proj_TyCon typ) @?= expected in
- [ ty @Eq :$ ty @Bool ==> True
- , ty @Ord :$ ty @Bool ==> True
- , ty @Functor :$ ty @Maybe ==> True
- , ty @Functor :$ ty @IO ==> True
- , ty @Monad :$ ty @IO ==> True
- , ty @Traversable :$ ty @IO ==> False
+ , testGroup "proveConstraint" $
+ let (==>) (typ::Type SRC SS (t::Constraint)) expected =
+ let imps = importTypes @SS [] in
+ let conf = config_Doc_Type{config_Doc_Type_imports = imps} in
+ testCase (showType conf typ) $
+ isJust (proveConstraint typ) @?= expected in
+ [ tyEq tyBool ==> True
+ , tyOrd tyBool ==> True
+ , tyFunctor (tyConst @(K Maybe) @Maybe) ==> True
+ , tyFunctor (tyConst @(K IO) @IO) ==> True
+ , tyMonad (tyConst @(K IO) @IO) ==> True
+ , tyTraversable (tyConst @(K IO) @IO) ==> False
]
]
sourcephile / git / haskell / symantic.git / blobdiff