From 548b576aa13d644907c9ef1cbd0aaa7997dcf455 Mon Sep 17 00:00:00 2001
From: Sean Gillespie <sean@mistersg.net>
Date: Wed, 8 Mar 2017 11:53:40 -0500
Subject: [PATCH] Update SystemF TypeChecker
Implement Type Application
---
src/Language/SystemF/TypeCheck.hs | 38 +++++++++++++++++++++++++-
test/Language/SystemF/TypeCheckSpec.hs | 25 +++++++++++++++--
2 files changed, 59 insertions(+), 4 deletions(-)
diff --git a/src/Language/SystemF/TypeCheck.hs b/src/Language/SystemF/TypeCheck.hs
index 5cc824f..87928c8 100644
--- a/src/Language/SystemF/TypeCheck.hs
+++ b/src/Language/SystemF/TypeCheck.hs
@@ -18,7 +18,7 @@ typecheck uniqs ctx (Var v) = tcVar uniqs ctx v
typecheck uniqs ctx (Abs n t body) = tcAbs uniqs ctx n t body
typecheck uniqs ctx (App e1 e2) = tcApp uniqs ctx e1 e2
typecheck uniqs ctx (TyAbs t body) = tcTyAbs uniqs ctx t body
-typecheck _ _ _ = undefined
+typecheck uniqs ctx (TyApp e ty) = tcTyApp uniqs ctx e ty
tcVar :: (Ord n, Eq n, PrettyPrint n)
=> UniqueSupply n
@@ -67,12 +67,48 @@ tcTyAbs :: (Ord n, Eq n, PrettyPrint n)
tcTyAbs uniqs ctx ty body = TyForAll ty <$> typecheck uniqs ctx' body
where ctx' = insert ty (TyVar ty) ctx
+tcTyApp :: (Ord n, Eq n, PrettyPrint n)
+ => UniqueSupply n
+ -> Context n (Ty n)
+ -> SystemFExpr n n
+ -> Ty n
+ -> Either String (Ty n)
+tcTyApp uniqs ctx (TyAbs t expr) ty = typecheck uniqs ctx expr'
+ where expr' = sub t ty expr
+tcTyApp uniqs ctx expr ty = typecheck uniqs ctx expr
+
-- Utilities
unique :: UniqueSupply t
-> Either String t
unique (u:_) = return u
unique _ = fail "Unique supply ran out"
+sub :: Eq n
+ => n
+ -> Ty n
+ -> SystemFExpr n n
+ -> SystemFExpr n n
+sub name ty (App e1 e2) = App (sub name ty e1) (sub name ty e2)
+sub name ty (Abs n ty' e) = Abs n (subTy name ty ty') (sub name ty e)
+sub name ty (TyAbs ty' e) = TyAbs ty' (sub name ty e)
+sub name ty (TyApp e ty') = TyApp (sub name ty e) (subTy name ty ty')
+sub name ty expr = expr
+
+subTy :: Eq n
+ => n
+ -> Ty n
+ -> Ty n
+ -> Ty n
+subTy name ty (TyArrow t1 t2)
+ = TyArrow (subTy name ty t1) (subTy name ty t2)
+subTy name ty ty'@(TyVar name')
+ | name == name' = ty
+ | otherwise = ty'
+subTy name t1 t2@(TyForAll name' t2')
+ | name == name' = t2
+ | otherwise = TyForAll name' (subTy name t2 t2')
+
+
tyMismatchMsg :: (PrettyPrint t, PrettyPrint t')
=> t
-> t'
diff --git a/test/Language/SystemF/TypeCheckSpec.hs b/test/Language/SystemF/TypeCheckSpec.hs
index 8676ba5..24274d6 100644
--- a/test/Language/SystemF/TypeCheckSpec.hs
+++ b/test/Language/SystemF/TypeCheckSpec.hs
@@ -5,9 +5,15 @@ import Data.Map
import Test.Hspec
+import Language.Lambda.Util.PrettyPrint
import Language.SystemF.Expression
import Language.SystemF.TypeCheck
+tc :: (Ord n, Eq n, PrettyPrint n)
+ => UniqueSupply n
+ -> [(n, Ty n)]
+ -> SystemFExpr n n
+ -> Either String (Ty n)
tc uniqs ctx = typecheck uniqs (fromList ctx)
spec :: Spec
@@ -51,6 +57,19 @@ spec = describe "typecheck" $ do
tc ["A"] [] (TyAbs "X" (Var "x")) `shouldBe` Right (TyForAll "X" (TyVar "A"))
it "typechecks type abstractions with simple abstraction" $
- tc [] [] (TyAbs "X" (Abs "x" (TyVar "X") (Var "X"))) `shouldBe`
- Right (TyForAll "X" (TyArrow (TyVar "X") (TyVar "X")))
-
+ tc [] [] (TyAbs "X" (Abs "x" (TyVar "X") (Var "x")))
+ `shouldBe` Right (TyForAll "X" (TyArrow (TyVar "X") (TyVar "X")))
+
+ it "typechecks type abstractions with application" $
+ tc [] [("y", TyVar "Y")]
+ (App (TyApp (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) (TyVar "Y"))
+ (Var "y"))
+ `shouldBe` Right (TyVar "Y")
+
+ it "typechecks simple type applications" $
+ tc [] [("x", TyVar "A")] (TyApp (TyAbs "X" (Var "x")) (TyVar "X"))
+ `shouldBe` Right (TyVar "A")
+
+ it "typechecks type applications with simple abstraction" $
+ tc [] [] (TyApp (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) (TyVar "Y"))
+ `shouldBe` Right (TyArrow (TyVar "Y") (TyVar "Y"))
--
GitLab