~jojo/Carth

843a98535842ded005e3d05797ee68fb3c38e472 — JoJo 1 year, 3 months ago ce8b838
Extract tests from CheckSpec to individual files in test/tests/bad

SystemSpec now runs those and verifies the type errors match what's expected
M carth.cabal => carth.cabal +1 -1
@@ 98,7 98,7 @@ test-suite carth-test
  type: exitcode-stdio-1.0
  main-is: Spec.hs
  other-modules:
      CheckSpec
      SystemSpec
  hs-source-dirs:
      test
  ghc-options: -threaded -rtsopts -with-rtsopts=-N -Weverything -Werror -Wno-safe -Wno-unsafe -Wno-missing-import-lists -Wno-missing-exported-signatures -Wno-missing-export-lists -Wno-missing-local-signatures -Wno-missing-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-name-shadowing -Wno-orphans -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unticked-promoted-constructors -Wno-missing-deriving-strategies -Wno-missing-export-lists

M src/Inferred.hs => src/Inferred.hs +5 -4
@@ 1,4 1,4 @@
{-# LANGUAGE LambdaCase, TemplateHaskell, DataKinds, TupleSections #-}
{-# LANGUAGE LambdaCase, TemplateHaskell, DataKinds, TupleSections, DeriveDataTypeable #-}

-- | Type annotated AST as a result of typechecking
module Inferred (module Inferred, WithPos(..), TVar(..), TPrim(..), Const(..)) where


@@ 11,6 11,7 @@ import Data.Bifunctor
import Lens.Micro.Platform (makeLenses)

import Misc
import Data.Data
import qualified Parsed
import Parsed (TVar(..), Const(..))
import SrcPos


@@ 40,7 41,7 @@ data TypeErr
    | RecursiveVarDef (WithPos String)
    | TypeInstArityMismatch SrcPos String Int Int
    | ConflictingVarDef SrcPos String
    deriving Show
    deriving (Show, Data)

type TConst = TypeAst.TConst Type



@@ 50,12 51,12 @@ data Type
    | TConst TConst
    | TFun Type Type
    | TBox Type
    deriving (Show, Eq, Ord)
    deriving (Show, Eq, Ord, Data)

data Scheme = Forall
    { _scmParams :: (Set TVar)
    , _scmBody :: Type
    } deriving (Show, Eq)
    } deriving (Show, Eq, Data)
makeLenses ''Scheme

type Id = WithPos String

M src/Parse.hs => src/Parse.hs +2 -4
@@ 250,10 250,8 @@ ns_num = do
    pure (Lit e)

ns_nat :: Parser Word
ns_nat = choice [ string "0b" *> Lexer.binary
                , string "0x" *> Lexer.hexadecimal
                , Lexer.decimal
                ]
ns_nat =
    choice [string "0b" *> Lexer.binary, string "0x" *> Lexer.hexadecimal, Lexer.decimal]

strlit :: Parser String
strlit = andSkipSpaceAfter ns_strlit

M src/Parsed.hs => src/Parsed.hs +7 -5
@@ 1,5 1,6 @@
{-# LANGUAGE LambdaCase, TypeSynonymInstances, FlexibleInstances
           , MultiParamTypeClasses, KindSignatures, DataKinds #-}
           , MultiParamTypeClasses, KindSignatures, DataKinds
           , DeriveDataTypeable #-}

module Parsed (module Parsed, TPrim(..), TConst) where



@@ 8,6 9,7 @@ import Data.Set (Set)
import Data.Bifunctor
import Control.Arrow ((>>>))

import Data.Data
import SrcPos
import FreeVars
import TypeAst


@@ 16,12 18,12 @@ import TypeAst
data IdCase = Big | Small

newtype Id (case' :: IdCase) = Id (WithPos String)
    deriving (Show, Eq, Ord)
    deriving (Show, Eq, Ord, Data)

data TVar
    = TVExplicit (Id 'Small)
    | TVImplicit Int
    deriving (Show, Eq, Ord)
    deriving (Show, Eq, Ord, Data)

-- TODO: Now that AnnotAst.Type is not just an alias to Ast.Type, it makes sense
--       to add SrcPos-itions to Ast.Type! Would simplify / improve error


@@ 32,10 34,10 @@ data Type
    | TConst (TConst Type)
    | TFun Type Type
    | TBox Type
    deriving (Show, Eq, Ord)
    deriving (Show, Eq, Ord, Data)

data Scheme = Forall SrcPos (Set TVar) Type
     deriving (Show, Eq)
     deriving (Show, Eq, Data)

data Pat
    = PConstruction SrcPos (Id 'Big) [Pat]

M src/SrcPos.hs => src/SrcPos.hs +5 -2
@@ 1,15 1,18 @@
{-# LANGUAGE DeriveDataTypeable #-}

module SrcPos where

import Text.Megaparsec.Pos
import Data.Data


data SrcPos = SrcPos
    { srcName :: FilePath
    , srcLine :: Word
    , srcColumn :: Word
    } deriving (Show, Eq, Ord)
    } deriving (Show, Eq, Ord, Data)

data WithPos a = WithPos SrcPos a
data WithPos a = WithPos SrcPos a deriving (Data)

class HasPos a where
    getPos :: a -> SrcPos

M src/TypeAst.hs => src/TypeAst.hs +4 -1
@@ 1,8 1,11 @@
{-# LANGUAGE DeriveDataTypeable #-}

-- | This module mostly exists to expost the builtin types via convenient variables,
--   instead of requiring redefinitions or manually typing the strings of TConst's, which
--   would be prone to typo errors.
module TypeAst where

import Data.Data
import Data.Word

data TPrim


@@ 14,7 17,7 @@ data TPrim
    | TF32
    | TF64
    | TF128
    deriving (Show, Eq, Ord)
    deriving (Show, Eq, Ord, Data)

type TConst t = (String, [t])


D test/CheckSpec.hs => test/CheckSpec.hs +0 -185
@@ 1,185 0,0 @@
{-# LANGUAGE LambdaCase #-}

module CheckSpec where

import Test.Hspec

import qualified Parsed
import qualified Checked
import Parse
import Check
import Err

pMainNotDefined = "(define foo Unit)"
pInvalidUserTypeSig = concat
    ["(define: (invalid-user-type-signature x)", "    (forall (a b c) (Fun a a))", "  x)"]
pCtorArityMismatch = concat
    [ "(data Integ (Integ Int))"
    , "(define arity-mismatch-for-constructor"
    , "  (match (Integ 1)"
    , "    (case (Integ foo bar) foo)))"
    ]
pConflictingPatVarDefs = concat
    [ "(data IntPair (IntPair Int Int))"
    , "(define conflicting-defs-in-pat"
    , "  (match (IntPair 1 2)"
    , "    (case (IntPair a a) a)))"
    ]
pUndefCtor = "(define undef-ctor ThisCtorIsUndefined)"
pUndefVar = "(define undef-var this-var-is-undefined)"
pInfType = "(define (infinite-type x) (infinite-type x infinite-type))"
pUnificationFailed = "(data Integ (Integ Int)) (define type-mismatch (Integ True))"
pConflictingTypeDef = "(data Foo) (data Foo)"
pConflictingCtorDef_a = "(data Foo Bar Bar)"
pConflictingCtorDef_b = "(data Baz Baz) (data Quux Baz)"
pRedundantCase = concat
    [ "(define foo"
    , "  (fmatch"
    , "    (case True 0)"
    , "    (case True 1)"
    , "    (case False 2)))"
    ]
pInexhaustivePats = "(define foo (fmatch (case True 0)))"
pExternNotMonomorphic = "(extern foo (Fun a Int))"
pFoundHole = "(define foo _)"
pRecTypeDef = "(data Foo (Foo Foo))"
pUndefType_a = "(data Foo (Foo Bar))"
pUndefType_b = "(extern foo (Fun Int Foo))"
pUndefType_c = "(define: (foo x) (Fun Int Foo) (foo x))"
pUnboundTVar = unlines
    [ "(define (seq a b) b)"
    , "(define (undef a) (undef a))"
    , "(define (foo a) (seq (undef Unit) 123))"
    ]
pWrongMainType = "(define: main Int (undefined Unit))"
pRecursiveVarDef = "(define: foo Int (+ foo 1))"
pTypeInstArityMismatch = "(data (Foo a) (Foo a)) (data Bar (Bar Foo))"
pConflictingVarDef_a = "(define foo +) (define foo -)"
pConflictingVarDef_b = "(define foo (letrec ((a 1) (a 2)) a))"

spec :: Spec
spec = do
    describe "typecheck" $ do
        it "detects when main is not defined"
            $ shouldSatisfy (typecheck' pMainNotDefined)
            $ \case
                  Right (Left MainNotDefined) -> True
                  _ -> False
        it "detects invalid user type signatures"
            $ shouldSatisfy (typecheck' pInvalidUserTypeSig)
            $ \case
                  Right (Left (InvalidUserTypeSig{})) -> True
                  _ -> False
        it "detects arity mismatch in constructor"
            $ shouldSatisfy (typecheck' pCtorArityMismatch)
            $ \case
                  Right (Left (CtorArityMismatch{})) -> True
                  _ -> False
        it "detects conflicting pattern variable defs"
            $ shouldSatisfy (typecheck' pConflictingPatVarDefs)
            $ \case
                  Right (Left (ConflictingPatVarDefs{})) -> True
                  _ -> False
        it "detects undefined constructors"
            $ shouldSatisfy (typecheck' pUndefCtor)
            $ \case
                  Right (Left (UndefCtor{})) -> True
                  _ -> False
        it "detects undefined variables" $ shouldSatisfy (typecheck' pUndefVar) $ \case
            Right (Left (UndefVar{})) -> True
            _ -> False
        it "detects infinite types" $ shouldSatisfy (typecheck' pInfType) $ \case
            Right (Left (InfType{})) -> True
            _ -> False
        it "detects type unification failure"
            $ shouldSatisfy (typecheck' pUnificationFailed)
            $ \case
                  Right (Left (UnificationFailed{})) -> True
                  _ -> False
        it "detects conflicting type definitions"
            $ shouldSatisfy (typecheck' pConflictingTypeDef)
            $ \case
                  Right (Left (ConflictingTypeDef{})) -> True
                  _ -> False
        it "detects conflicting constructor definitions, withing"
            $ shouldSatisfy (typecheck' pConflictingCtorDef_a)
            $ \case
                  Right (Left (ConflictingCtorDef{})) -> True
                  _ -> False
        it "detects conflicting constructor definitions, between"
            $ shouldSatisfy (typecheck' pConflictingCtorDef_b)
            $ \case
                  Right (Left (ConflictingCtorDef{})) -> True
                  _ -> False
        it "detects redundant cases in patterns"
            $ shouldSatisfy (typecheck' pRedundantCase)
            $ \case
                  Right (Left (RedundantCase{})) -> True
                  _ -> False
        it "detects inexhaustive patterns"
            $ shouldSatisfy (typecheck' pInexhaustivePats)
            $ \case
                  Right (Left (InexhaustivePats{})) -> True
                  _ -> False
        it "detects non-monomorphic externs"
            $ shouldSatisfy (typecheck' pExternNotMonomorphic)
            $ \case
                  Right (Left (ExternNotMonomorphic{})) -> True
                  _ -> False
        it "finds holes" $ shouldSatisfy (typecheck' pFoundHole) $ \case
            Right (Left (FoundHole{})) -> True
            _ -> False
        it "detects type definitions recursive without indirection"
            $ shouldSatisfy (typecheck' pRecTypeDef)
            $ \case
                  Right (Left (RecTypeDef{})) -> True
                  _ -> False
        it "detects references to undefined types, in type defs"
            $ shouldSatisfy (typecheck' pUndefType_a)
            $ \case
                  Right (Left (UndefType{})) -> True
                  _ -> False
        it "detects references to undefined types, in extern decls"
            $ shouldSatisfy (typecheck' pUndefType_b)
            $ \case
                  Right (Left (UndefType{})) -> True
                  _ -> False
        it "detects references to undefined types, in var defs"
            $ shouldSatisfy (typecheck' pUndefType_c)
            $ \case
                  Right (Left (UndefType{})) -> True
                  _ -> False
        it "detects unbound type vars in var def bodies"
            $ shouldSatisfy (typecheck' pUnboundTVar)
            $ \case
                  Right (Left (UnboundTVar{})) -> True
                  _ -> False
        it "detects when the type of `main` is wrong"
            $ shouldSatisfy (typecheck' pWrongMainType)
            $ \case
                  Right (Left (WrongMainType{})) -> True
                  _ -> False
        it "detects recursive var defs"
            $ shouldSatisfy (typecheck' pRecursiveVarDef)
            $ \case
                  Right (Left (RecursiveVarDef{})) -> True
                  _ -> False
        it "detects arity mismatch of datatype instantiations"
            $ shouldSatisfy (typecheck' pTypeInstArityMismatch)
            $ \case
                  Right (Left (TypeInstArityMismatch{})) -> True
                  _ -> False
        it "detects conflicting var defs, at top-level"
            $ shouldSatisfy (typecheck' pConflictingVarDef_a)
            $ \case
                  Right (Left (ConflictingVarDef{})) -> True
                  _ -> False
        it "detects conflicting var defs, in let-form"
            $ shouldSatisfy (typecheck' pConflictingVarDef_b)
            $ \case
                  Right (Left (ConflictingVarDef{})) -> True
                  _ -> False

typecheck' :: String -> Either String (Either TypeErr Checked.Program)
typecheck' = fmap (\(_, ds, tds, es) -> typecheck (Parsed.Program ds tds es))
    . parse' toplevels "TEST"

A test/SystemSpec.hs => test/SystemSpec.hs +27 -0
@@ 0,0 1,27 @@
{-# LANGUAGE LambdaCase #-}

module SystemSpec where

import Data.Data
import Data.Functor
import Control.Monad
import System.Directory
import System.FilePath
import Test.Hspec

import Parse
import Check

spec :: Spec
spec = do
    -- describe "Good programs" $ do
    --     it "produce expected output" $ shouldSatisfy True id
    describe "Bad programs don't typecheck" $ do
        let d = "test/tests/bad"
        fs <- runIO $ listDirectory d <&> filter (isExtensionOf "carth")
        forM_ fs $ \f -> do
            expectedErr <- runIO $ fmap (drop 3 . head . lines) (readFile (d </> f))
            result <- runIO $ parse (d </> f)
            it (dropExtension f) $ shouldSatisfy (fmap typecheck result) $ \case
                Right (Left e) -> show (toConstr e) == expectedErr
                _ -> False

A test/tests/bad/conflicting-ctor-def_0.carth => test/tests/bad/conflicting-ctor-def_0.carth +3 -0
@@ 0,0 1,3 @@
;; ConflictingCtorDef

(data Foo Bar Bar)

A test/tests/bad/conflicting-ctor-def_1.carth => test/tests/bad/conflicting-ctor-def_1.carth +4 -0
@@ 0,0 1,4 @@
;; ConflictingCtorDef

(data Baz Baz)
(data Quux Baz)

A test/tests/bad/conflicting-pat-var-defs.carth => test/tests/bad/conflicting-pat-var-defs.carth +7 -0
@@ 0,0 1,7 @@
;; ConflictingPatVarDefs

(data IntPair (IntPair Int Int))

(define conflicting-defs-in-pat
  (match (IntPair 1 2)
    (case (IntPair a a) a)))

A test/tests/bad/conflicting-type-def.carth => test/tests/bad/conflicting-type-def.carth +4 -0
@@ 0,0 1,4 @@
;; ConflictingTypeDef

(data Foo)
(data Foo)

A test/tests/bad/conflicting-var-def_0.carth => test/tests/bad/conflicting-var-def_0.carth +4 -0
@@ 0,0 1,4 @@
;; ConflictingVarDef

(define foo +)
(define foo -)

A test/tests/bad/conflicting-var-def_1.carth => test/tests/bad/conflicting-var-def_1.carth +3 -0
@@ 0,0 1,3 @@
;; ConflictingVarDef

(define foo (letrec ((a 1) (a 2)) a))

A test/tests/bad/ctor-arity-mismatch.carth => test/tests/bad/ctor-arity-mismatch.carth +7 -0
@@ 0,0 1,7 @@
;; CtorArityMismatch

(data Integ (Integ Int))

(define arity-mismatch-for-constructor
  (match (Integ 1)
    (case (Integ foo bar) foo)))

A test/tests/bad/extern-not-monomorphic.carth => test/tests/bad/extern-not-monomorphic.carth +3 -0
@@ 0,0 1,3 @@
;; ExternNotMonomorphic

(extern foo (Fun a Int))

A test/tests/bad/found-hole.carth => test/tests/bad/found-hole.carth +3 -0
@@ 0,0 1,3 @@
;; FoundHole

(define foo _)

A test/tests/bad/inexhaustive-pats.carth => test/tests/bad/inexhaustive-pats.carth +3 -0
@@ 0,0 1,3 @@
;; InexhaustivePats

(define foo (fmatch (case True 0)))

A test/tests/bad/inf-type.carth => test/tests/bad/inf-type.carth +3 -0
@@ 0,0 1,3 @@
;; InfType

(define (infinite-type x) (infinite-type x infinite-type))

A test/tests/bad/invalid-user-type-sig.carth => test/tests/bad/invalid-user-type-sig.carth +5 -0
@@ 0,0 1,5 @@
;; InvalidUserTypeSig

(define: (invalid-user-type-signature x)
    (forall (a b c) (Fun a a))
  x)

A test/tests/bad/main-not-defined.carth => test/tests/bad/main-not-defined.carth +3 -0
@@ 0,0 1,3 @@
;; MainNotDefined

(define foo Unit)

A test/tests/bad/rec-type-def.carth => test/tests/bad/rec-type-def.carth +3 -0
@@ 0,0 1,3 @@
;; RecTypeDef

(data Foo (Foo Foo))

A test/tests/bad/recursive-var-def.carth => test/tests/bad/recursive-var-def.carth +3 -0
@@ 0,0 1,3 @@
;; RecursiveVarDef

(define: foo Int (+ foo 1))

A test/tests/bad/redundant-case.carth => test/tests/bad/redundant-case.carth +7 -0
@@ 0,0 1,7 @@
;; RedundantCase

(define foo
  (fmatch
    (case True 0)
    (case True 1)
    (case False 2)))

A test/tests/bad/type-inst-arity-mismatch.carth => test/tests/bad/type-inst-arity-mismatch.carth +4 -0
@@ 0,0 1,4 @@
;; TypeInstArityMismatch

(data (Foo a) (Foo a))
(data Bar (Bar Foo))

A test/tests/bad/unbound-tvar.carth => test/tests/bad/unbound-tvar.carth +5 -0
@@ 0,0 1,5 @@
;; UnboundTVar

(define (seq a b) b)
(define (undef a) (undef a))
(define (foo a) (seq (undef Unit) 123))

A test/tests/bad/undef-ctor.carth => test/tests/bad/undef-ctor.carth +3 -0
@@ 0,0 1,3 @@
;; UndefCtor

(define undef-ctor ThisCtorIsUndefined)

A test/tests/bad/undef-type_0.carth => test/tests/bad/undef-type_0.carth +3 -0
@@ 0,0 1,3 @@
;; UndefType

(data Foo (Foo Bar))

A test/tests/bad/undef-type_1.carth => test/tests/bad/undef-type_1.carth +3 -0
@@ 0,0 1,3 @@
;; UndefType

(extern foo (Fun Int Foo))

A test/tests/bad/undef-type_2.carth => test/tests/bad/undef-type_2.carth +3 -0
@@ 0,0 1,3 @@
;; UndefType

(define: (foo x) (Fun Int Foo) (foo x))

A test/tests/bad/undef-var.carth => test/tests/bad/undef-var.carth +3 -0
@@ 0,0 1,3 @@
;; UndefVar

(define undef-var this-var-is-undefined)

A test/tests/bad/unification-failed.carth => test/tests/bad/unification-failed.carth +5 -0
@@ 0,0 1,5 @@
;; UnificationFailed

(data Integ (Integ Int))

(define type-mismatch (Integ True))

A test/tests/bad/wrong-main-type.carth => test/tests/bad/wrong-main-type.carth +3 -0
@@ 0,0 1,3 @@
;; WrongMainType

(define: main Int (undefined Unit))