From 354087b24447baa981240a7ce39b291db8095c95 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sat, 26 Jan 2019 18:25:33 -0500 Subject: [PATCH] [ test ] Fix test --- OwO.cabal | 1 + src/full/OwO/TypeChecking.hs | 10 ++------ src/full/OwO/TypeChecking/Desugar.hs | 19 ++++++--------- src/full/OwO/TypeChecking/Monad.hs | 7 ++++++ src/test/Main.hs | 35 +++++++++++++++++----------- 5 files changed, 38 insertions(+), 34 deletions(-) diff --git a/OwO.cabal b/OwO.cabal index 7eacc90..b799abe 100644 --- a/OwO.cabal +++ b/OwO.cabal @@ -114,6 +114,7 @@ Test-Suite tests main-is: Main.hs build-depends: OwO , base >= 4.8 && < 5 + , containers >= 0.5.10 && < 0.7 , hspec , process , mtl >= 2.2.1 && < 2.3 diff --git a/src/full/OwO/TypeChecking.hs b/src/full/OwO/TypeChecking.hs index ddb2180..64d2b67 100644 --- a/src/full/OwO/TypeChecking.hs +++ b/src/full/OwO/TypeChecking.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-} @@ -36,14 +37,7 @@ import OwO.TypeChecking.Reduce literalType :: LiteralInfo -> Type literalType _ = Var __TODO__ ---checkDecl :: - -typeCheckFile - :: ( MonadState TCState m - , MonadError TCError m - ) - => PsiFile - -> m () +typeCheckFile :: TCM m => PsiFile -> m () typeCheckFile file = do let decls = declarations file moduleName = topLevelModuleName file diff --git a/src/full/OwO/TypeChecking/Desugar.hs b/src/full/OwO/TypeChecking/Desugar.hs index bfb20c0..2090b79 100644 --- a/src/full/OwO/TypeChecking/Desugar.hs +++ b/src/full/OwO/TypeChecking/Desugar.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-} @@ -50,26 +51,22 @@ data DesugarError -- ^ Invalid syntax, but allowed by parser, disallowed by desugarer deriving (Eq, Show) +type DesugarMonad m = (MonadState AstContext m, MonadError DesugarError m) + concreteToAbstractDecl - :: ( MonadState AstContext m - , MonadError DesugarError m - ) + :: DesugarMonad m => [PsiDeclaration] -> m [DesugarError] concreteToAbstractDecl = concreteToAbstractDecl' [] concreteToAbstractTerm - :: ( MonadState AstContext m - , MonadError DesugarError m - ) + :: DesugarMonad m => PsiTerm -> m AstTerm concreteToAbstractTerm = concreteToAbstractTerm' [] concreteToAbstractDecl' - :: ( MonadState AstContext m - , MonadError DesugarError m - ) + :: DesugarMonad m => [TypeSignature] -- Unimplemented declarations -> [PsiDeclaration] @@ -121,9 +118,7 @@ concreteToAbstractDecl' sigs (d : ds) = checkTerm = concreteToAbstractTerm' [] concreteToAbstractTerm' - :: ( MonadState AstContext m - , MonadError DesugarError m - ) + :: DesugarMonad m => [AstBinderInfo] -- Local variables -> PsiTerm diff --git a/src/full/OwO/TypeChecking/Monad.hs b/src/full/OwO/TypeChecking/Monad.hs index 8a5fde2..6f13324 100644 --- a/src/full/OwO/TypeChecking/Monad.hs +++ b/src/full/OwO/TypeChecking/Monad.hs @@ -1,10 +1,15 @@ +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE FlexibleContexts #-} -- | OwO's type checking state is a state monad transformer. -- We call it TypeCheckingMonad, in short TCM, as Agda does. module OwO.TypeChecking.Monad where +import Control.Monad.Except (MonadError (..)) +import Control.Monad.State (MonadState (..)) + import qualified Data.Text as T import OwO.Options @@ -48,3 +53,5 @@ data TCError = DesugarErr DesugarError | OtherErr String deriving (Eq, Show) + +type TCM m = (MonadState TCState m, MonadError TCError m) diff --git a/src/test/Main.hs b/src/test/Main.hs index e3ebe56..25dd950 100644 --- a/src/test/Main.hs +++ b/src/test/Main.hs @@ -1,15 +1,20 @@ +{-# LANGUAGE FlexibleContexts #-} module Main where -- import Control.Monad.IO.Class (liftIO) +import Control.Monad.Except (runExceptT) import Control.Monad.State (runStateT) +import Control.Monad.Identity (runIdentity) import Data.Either (isLeft, isRight) import qualified Data.Text as T +import qualified Data.Map as Map import Test.Hspec import System.Exit (ExitCode (..), exitWith) import OwO.Syntax.Concrete +import OwO.Syntax.Context (emptyCtx) import OwO.Syntax.Module import OwO.Syntax.Parser (parseNaiveWith) import OwO.Syntax.Parser.NaiveParser as NP @@ -23,46 +28,48 @@ checkExit n = exitWith n main :: IO () main = hspec $ do - describe "Simple reference resolving" $ do - let pre = parseNaiveWith $ snd <$> NP.declarationsP [] - p = (concreteToAbstractDecl <$>) . pre + describe "simple reference resolving" $ do + let p str = do + decls <- flip parseNaiveWith str $ snd <$> NP.declarationsP [] + let tcm = concreteToAbstractDecl decls + runExceptT $ runStateT tcm emptyCtx let ok (Right (Right _)) = True ok _ = False - it "Should resolve built-in definitions" $ do + it "should resolve built-in definitions" $ do p "{ a = Type }" `shouldSatisfy` ok p "{ id = Type -> Type }" `shouldSatisfy` ok p "{ id = Type1 -> Type2 }" `shouldSatisfy` ok p "{ id = TypeInf -> Type0 }" `shouldSatisfy` ok - it "Should resolve contextual definitions" $ do + it "should resolve contextual definitions" $ do p "{ a = Type; b = a }" `shouldSatisfy` ok p "{ postulate { a : Type } ; id = a -> a }" `shouldSatisfy` ok p "{ id = \\x -> x }" `shouldSatisfy` ok - it "Should give unresolved-reference" $ do + it "should give unresolved-reference" $ do let notOk (Right (Left (UnresolvedReferenceError _))) = True notOk _ = False p "{ a = b }" `shouldSatisfy` notOk p "{ a : b }" `shouldSatisfy` notOk p "{ id = \\x -> y }" `shouldSatisfy` notOk - it "Should give unimplemented errors" $ do - let notOk (Right (Left (NoImplementationError _))) = True + it "should give unimplemented errors" $ do + let notOk (Right (Right (NoImplementationError _ : _, _))) = True notOk _ = False p "{ a : Type }" `shouldSatisfy` notOk p "{ id : Type -> Type }" `shouldSatisfy` notOk describe "Infix declaration parsing" $ do - it "Should not parse incorrect infix declarations" $ do + it "should not parse incorrect infix declarations" $ do let p = parseNaiveWith NP.fixityP p "infixl 1 233" `shouldSatisfy` isLeft p "infixr +" `shouldSatisfy` isLeft p "infix 1" `shouldSatisfy` isLeft - it "Should parse simple infix declarations" $ do + it "should parse simple infix declarations" $ do let p = parseNaiveWith NP.fixityP p "infixl 1 +" `shouldSatisfy` isRight p "infixr 2 -" `shouldSatisfy` isRight @@ -70,26 +77,26 @@ main = hspec $ do describe "Type signature parsing" $ do - it "Should not parse errored files" $ do + it "should not parse errored files" $ do let p = parseNaiveSimple p "module A where\na :" `shouldSatisfy` isLeft p "module B where\n: b" `shouldSatisfy` isLeft - it "Should parse simple type signatures" $ do + it "should parse simple type signatures" $ do let p = parseNaiveSimple p "module A where\na : b" `shouldSatisfy` isRight p "module A where\na:b" `shouldSatisfy` isRight describe "Module name parsing" $ do - it "Should not work for errored files" $ do + it "should not work for errored files" $ do let p = parseNaiveSimple p "" `shouldSatisfy` isLeft p "module" `shouldSatisfy` isLeft p "module where" `shouldSatisfy` isLeft p "where" `shouldSatisfy` isLeft - it "Should parse module name" $ do + it "should parse module name" $ do let p s = moduleNameList . topLevelModuleName <$> parseNaiveSimple s p "module A where\n" `shouldBe` Right [T.pack "A"] p "module A.B where\n" `shouldBe` Right (T.pack <$> ["A", "B"])