Rakarake/churf
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

started on cleaner unit tests

Browse source
This commit is contained in:
sebastian 2023-03-25 00:02:38 +01:00
parent accbd4eea6
commit 05333c5689
2 changed files with 78 additions and 93 deletions
Download patch file Download diff file Expand all files Collapse all files

9
tests/DoStrings.hs Normal file
View file

@ -0,0 +1,9 @@
module DoStrings where
import Prelude hiding ((>>), (>>=))
(>>) :: String -> String -> String
(>>) str1 str2 = str1 ++ "\n" ++ str2
(>>=) :: String -> (String -> String) -> String
(>>=) str f = f str

162
tests/Tests.hs
View file

@ -1,109 +1,85 @@
{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE QualifiedDo #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# LANGUAGE NoImplicitPrelude #-}
{-# HLINT ignore "Use <$>" #-}
{-# HLINT ignore "Use camelCase" #-}
module Main where module Main where
import Data.Either (isLeft, isRight) import Control.Monad ((<=<))
import Data.Map (Map) import DoStrings qualified as D
import Data.Map qualified as M import Grammar.Par (myLexer, pProgram)
import Grammar.Abs
import Test.Hspec import Test.Hspec
import Test.QuickCheck import Prelude (Bool (..), Either (..), IO, fmap, not, ($), (.))
import TypeChecker.TypeChecker
import TypeChecker.TypeCheckerIr ( -- import Test.QuickCheck
Ctx (..), import TypeChecker.TypeChecker (typecheck)
Env (..),
Error,
Infer,
)
import TypeChecker.TypeCheckerIr qualified as T
main :: IO () main :: IO ()
main = hspec $ do main = hspec $ do
infer_elit ok1
infer_eann ok2
infer_eid bad1
infer_eabs bad2
test_id_function
infer_elit = describe "algoW used on ELit" $ do ok1 =
it "infers the type mono Int" $ do specify "Basic polymorphism with multiple type variables" $
getType (ELit (LInt 0)) `shouldBe` Right (T.TLit "Int") run
( D.do
const
"main = const 'a' 65 ;"
)
`shouldSatisfy` ok
ok2 =
specify "Head with a correct signature is accepted" $
run
( D.do
list
headSig
head
)
`shouldSatisfy` ok
it "infers the type mono Int" $ do bad1 =
getType (ELit (LInt 9999)) `shouldBe` Right (T.TLit "Int") specify "Infinite type unification should not succeed" $
run
( D.do
"main = \\x. x x ;"
)
`shouldSatisfy` bad
infer_eann = describe "algoW used on EAnn" $ do bad2 =
it "infers the type and checks if the annotated type matches" $ do specify "Pattern matching using different types should not succeed" $
getType (EAnn (ELit $ LInt 0) (TLit "Int")) `shouldBe` Right (T.TLit "Int") run
( D.do
list
"bad xs = case xs of {"
" 1 => 0 ;"
" Nil => 0 ;"
"};"
)
`shouldSatisfy` bad
it "fails if the annotated type does not match with the inferred type" $ do run = typecheck <=< pProgram . myLexer
getType (EAnn (ELit $ LInt 0) (TVar $ MkTVar "a")) `shouldSatisfy` isLeft
it "should be possible to annotate with a more specific type" $ do ok (Right _) = True
let annotated_lambda = EAnn (EAbs "x" (EVar "x")) (TFun (TLit "Int") (TLit "Int")) ok (Left _) = False
in getType annotated_lambda `shouldBe` Right (T.TFun (T.TLit "Int") (T.TLit "Int"))
it "should fail if the annotated type is more general than the inferred type" $ do bad = not . ok
getType (EAnn (ELit (LInt 0)) (TVar $ MkTVar "a")) `shouldSatisfy` isLeft
it "should fail if the annotated type is an arrow but the annotated type is not" $ do -- FUNCTIONS
getType (EAnn (EAbs "x" (EVar "x")) (TVar $ MkTVar "a")) `shouldSatisfy` isLeft
infer_eid = describe "algoW used on EVar" $ do const = D.do
it "should fail if the variable is not added to the environment" $ do "const : a -> b -> a ;"
property $ \x -> getType (EVar (LIdent (x :: String))) `shouldSatisfy` isLeft "const x y = x ;"
list = D.do
"data List (a) where"
" {"
" Nil : List (a)"
" Cons : a -> List (a) -> List (a)"
" };"
it "should succeed if the type exist in the environment" $ do headSig = D.do
property $ \x -> do "head : List (a) -> a ;"
let env = Env 0 mempty mempty head = D.do
let t = T.TVar $ T.MkTVar "a" "head xs = "
let ctx = Ctx (M.singleton (T.Ident (x :: String)) t) " case xs of {"
getTypeC env ctx (EVar (LIdent x)) `shouldBe` Right (T.TVar $ T.MkTVar "a") " Cons x xs => x ;"
" };"
infer_eabs = describe "algoW used on EAbs" $ do
it "should infer the argument type as int if the variable is used as an int" $ do
let lambda = EAbs "x" (EAdd (EVar "x") (ELit (LInt 0)))
getType lambda `shouldBe` Right (T.TFun (T.TLit "Int") (T.TLit "Int"))
it "should infer the argument type as polymorphic if it is not used in the lambda" $ do
let lambda = EAbs "x" (ELit (LInt 0))
getType lambda `shouldSatisfy` isArrowPolyToMono
it "should infer a variable as function if used as one" $ do
let lambda = EAbs "f" (EAbs "x" (EApp (EVar "f") (EVar "x")))
let isOk (Right (T.TFun (T.TFun (T.TVar _) (T.TVar _)) (T.TFun (T.TVar _) (T.TVar _)))) = True
isOk _ = False
getType lambda `shouldSatisfy` isOk
churf_id :: Bind
churf_id = Bind "id" ["x"] (EVar "x")
churf_add :: Bind
churf_add = Bind "add" ["x", "y"] (EAdd (EVar "x") (EVar "y"))
churf_main :: Bind
churf_main = Bind "main" [] (EApp (EApp (EVar "id") (EVar "add")) (ELit (LInt 0)))
prg = Program [DBind churf_main, DBind churf_add, DBind churf_id]
test_id_function :: SpecWith ()
test_id_function =
describe "typechecking a program with id, add and main, where id is applied to add in main" $ do
it "should succeed to find the correct type" $ do
typecheck prg `shouldSatisfy` isRight
isArrowPolyToMono :: Either Error T.Type -> Bool
isArrowPolyToMono (Right (T.TFun (T.TVar _) (T.TLit _))) = True
isArrowPolyToMono _ = False
-- | Empty environment
getType :: Exp -> Either Error T.Type
getType e = pure snd <*> run (inferExp e)
-- | Custom environment
getTypeC :: Env -> Ctx -> Exp -> Either Error T.Type
getTypeC env ctx e = pure snd <*> runC env ctx (inferExp e)