msyds/rlp
1
0
Fork 0
Code Issues 4 Pull Requests Actions Packages Projects Releases 2 Wiki Activity

fix hm tests

Browse Source
This commit is contained in:
crumbtoo
2023-12-29 13:54:09 -07:00
parent 35446533d7
commit b941347f82
2 changed files with 14 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
tst/Core/HindleyMilnerSpec.hs
View File

@@ -6,7 +6,8 @@ module Core.HindleyMilnerSpec
----------------------------------------------------------------------------------
import Core.Syntax
import Core.TH (coreExpr)
import Core.HindleyMilner (infer, check, TypeError(..), HMError)
import Core.HindleyMilner
import Control.Monad.Errorful
import Data.Either (isLeft)
import Test.Hspec
----------------------------------------------------------------------------------
@@ -16,24 +17,30 @@ spec :: Spec
spec = do
it "should infer `id 3` :: Int" $
let g = [ ("id", "a" :-> "a") ]
in infer g [coreExpr|id 3|] `shouldBe` Right TyInt
in infer' g [coreExpr|id 3|] `shouldBe` Right TyInt
it "should not infer `id 3` when `id` is specialised to `a -> a`" $
let g = [ ("id", ("a" :-> "a") :-> "a" :-> "a") ]
in infer g [coreExpr|id 3|] `shouldSatisfy` isLeft
in infer' g [coreExpr|id 3|] `shouldSatisfy` isLeft
-- TODO: property-based tests for let
it "should infer `let x = 3 in id x` :: Int" $
let g = [ ("id", "a" :-> "a") ]
e = [coreExpr|let {x = 3} in id x|]
in infer g e `shouldBe` Right TyInt
in infer' g e `shouldBe` Right TyInt
it "should infer `let x = 3; y = 2 in (+#) x y` :: Int" $
let g = [ ("+#", TyInt :-> TyInt :-> TyInt) ]
e = [coreExpr|let {x=3;y=2} in (+#) x y|]
in infer g e `shouldBe` Right TyInt
in infer' g e `shouldBe` Right TyInt
it "should find `3 :: Bool` contradictory" $
let e = [coreExpr|3|]
in check [] (TyCon "Bool") e `shouldSatisfy` isLeft
in check' [] (TyCon "Bool") e `shouldSatisfy` isLeft
infer' :: Context' -> Expr' -> Either TypeError Type
infer' g e = fmap fst . runErrorful $ infer g e
check' :: Context' -> Type -> Expr' -> Either TypeError ()
check' g t e = fmap fst . runErrorful $ check g t e