From 1dacfa5434a9e096325d2344e23864a906290f34 Mon Sep 17 00:00:00 2001 From: Tia Shah Date: Thu, 26 Dec 2024 12:38:30 +0000 Subject: [PATCH] Edit check' and synth' --- src/TypeChecking.purs | 66 ++++++++++++++++++++++++++++++++++++-- test/TypeCheckingTest.purs | 15 ++++++++- 2 files changed, 78 insertions(+), 3 deletions(-) diff --git a/src/TypeChecking.purs b/src/TypeChecking.purs index cbe7ce1dc..20af8c734 100644 --- a/src/TypeChecking.purs +++ b/src/TypeChecking.purs @@ -10,7 +10,7 @@ import SExpr (Branch, Clause(..), Clauses(..), Expr(..), ListRest(..), ListRestP import Data.Maybe (Maybe(..)) import Control.Alt ((<|>)) import Bind (Bind, Var, varAnon, (↦), keys) -import Data.List (List(..), length, sortBy, zip, zipWith, (:), (\\), nub, find, singleton) +import Data.List (List(..), length, sortBy, zip, zipWith, (:), (\\), nub, find, singleton, foldM, index) import Util (Endo, type (×), (×), type (+), error, onlyIf) import Data.Foldable (all) import Data.Traversable (traverse) @@ -243,6 +243,40 @@ checkPattern' _ _ _ = Nothing checkBind' :: Context -> Bind Pattern -> Types -> Maybe Context checkBind' g (x ↦ pattern) ty = checkPattern' g pattern ty +synthPatterns' :: Context -> List Pattern -> Maybe Context +synthPatterns' g Nil = Just g +synthPatterns' g ((PVar var) : Nil) = Just g +synthPatterns' g (p : ps) = do + g' <- synthPattern' g p + g'' <- synthPatterns' g ps + Just (append g' g'') +synthPatterns' _ _ = Nothing + +synthPattern' :: Context -> Pattern -> Maybe Context +synthPattern' g (PVar x) = case lookup g x of + Just ty -> Just (singleton (Tuple x ty)) + Nothing -> Nothing +synthPattern' g (PConstr ctr patterns) = case (lookup g ctr) of + Just ty' -> case liftTypes ty' of + Tuple argTy retTy -> do + checkPatterns' g argTy patterns + _ -> Nothing +synthPattern' g (PListEmpty) = Just g +synthPattern' g (PListNonEmpty head tail) = do + g' <- synthPattern' g head + synthListPattern g' tail +synthPattern' _ _ = Nothing + + +synthListPattern :: Context -> ListRestPattern -> Maybe Context +synthListPattern g (PListEnd) = Just g +synthListPattern g (PListNext next rest) = do + g' <- synthPattern' g next + synthListPattern g' rest +synthListPattern g (PListVar var) = case lookup g var of + Just _ -> Just g + _ -> Nothing + checkRecordFields :: Context -> List (Bind Pattern) -> List (Tuple String Types) -> Maybe Context checkRecordFields g Nil _ = Just g checkRecordFields g (b : bs) ty = @@ -537,6 +571,17 @@ synth' g (Right (Dictionary u entries)) = case entries of Right true -> Right (TDict keyTy valTy) _ -> Left (TypeMismatch ("Cannot match expression with type " <> (prettyTypes (TDict keyTy valTy)))) Nil -> Left (InvalidSyntax "Null dictionary found") + +synth' g (Right (Lambda clauses)) = case clauses of + (Clauses (NonEmptyList (NonEmpty (Clause (Tuple (NonEmptyList (NonEmpty pattern Nil)) expr)) Nil))) -> case synthPattern' g pattern of + Just updatedG -> case synth' updatedG (Right expr) of + Right ty -> case index updatedG 0 of + Just elem -> Right (FunTy (snd elem) ty) + Nothing -> Left (TypeMismatch "Cannot match types") + Left err -> Left err + Nothing -> Left (InvalidSyntax "Pattern structure is invalid") + _ -> Left (InvalidSyntax "Clauses structure is invalid") + synth' _ _ = Left (InvalidSyntax "Not supported yet") @@ -695,6 +740,14 @@ check' g (Right (ListComp u expr qualifiers)) (TList ty) = case check' g (Right Right true -> check' context (Right (ListComp u expr qs)) (TList ty) _ -> Left (InvalidSyntax "Invalid syntax") Nil -> Right true + +check' g (Right (Lambda clauses)) (FunTy argTy retTy) = case clauses of + (Clauses (NonEmptyList (NonEmpty (Clause (Tuple (NonEmptyList (NonEmpty pattern Nil)) expr)) Nil))) -> case checkPattern' g pattern argTy of + Just context -> check' context (Right expr) retTy + Nothing -> Left (InvalidSyntax "Pattern structure is invalid") + _ -> Left (InvalidSyntax "Clauses structure is invalid") + + check' g (Right expr) ty = case synth' g (Right expr) of Left err -> Left err Right ty' -> @@ -708,4 +761,13 @@ prettyTypes :: Types -> String prettyTypes (TCons ty) = ty prettyTypes (TList ty) = "[" <> prettyTypes ty <> "]" prettyTypes (TDict ty1 ty2) = "{" <> prettyTypes ty1 <> ", " <> prettyTypes ty2 <> "}" -prettyTypes (FunTy ty1 ty2) = prettyTypes ty1 <> " -> " <> prettyTypes ty2 \ No newline at end of file +prettyTypes (FunTy ty1 ty2) = prettyTypes ty1 <> " -> " <> prettyTypes ty2 + +-- data Expr a +-- | Matrix a (Expr a) (Var × Var) (Expr a) +-- | Lambda (Clauses a) +-- | Project (Expr a) Var +-- | DProject (Expr a) (Expr a) +-- | App (Expr a) (Expr a) +-- | MatchAs (Expr a) (NonEmptyList (Pattern × Expr a)) +-- | LetRec (RecDefs a) (Expr a) \ No newline at end of file diff --git a/test/TypeCheckingTest.purs b/test/TypeCheckingTest.purs index 40ddf757f..1333b30a6 100644 --- a/test/TypeCheckingTest.purs +++ b/test/TypeCheckingTest.purs @@ -244,4 +244,17 @@ testCheck' = do let listCompTest = check' ((Tuple "x" (TList (TCons "Int"))):Nil) (runParser "[x | 1, 2, 3]" expr_) (TList (TCons "Int")) logTestResult "check' listComp" (listCompTest == Right true) let listCompTestInvalid = check' ((Tuple "x" (TList (TCons "Int"))):Nil) (runParser "[x | 1, 2, 3]" expr_) (TList (TCons "Str")) - logTestResult "check' listComp invalid" (listCompTestInvalid == (Left (TypeMismatch "Cannot match [Int] with [Str]"))) \ No newline at end of file + logTestResult "check' listComp invalid" (listCompTestInvalid == (Left (TypeMismatch "Cannot match [Int] with [Str]"))) + -- Lambda + let lambdaTest = check' Nil (runParser "fun x -> x + 1" program) (FunTy (TCons "Int") (TCons "Int")) + logTestResult "check' lambda" (lambdaTest == Right true) + let lambdaBool = check' Nil (runParser "fun x -> x > 1" program) (FunTy (TCons "Int") (TCons "Bool")) + logTestResult "check' lambda bool" (lambdaBool == Right true) + let lambdaTestInvalid = check' Nil (runParser "fun x -> x + 1" program) (FunTy (TCons "Int") (TCons "Str")) + logTestResult "check' lambda invalid" (lambdaTestInvalid == (Left (TypeMismatch "Cannot match Str with Int"))) + let lambdaBoolInvalid = check' Nil (runParser "fun x -> x > 1" program) (FunTy (TCons "Int") (TCons "Int")) + logTestResult "check' lambda bool invalid" (lambdaBoolInvalid == (Left (TypeMismatch "Cannot match Int with Bool"))) + + +-- > synth' ((Tuple "x" (TCons "Int")):Nil) (runParser "fun x -> x > 1" program) +-- (Right (FunTy (TCons "Int") (TCons "Bool"))) \ No newline at end of file