~jojo/Carth

05958034c644c6adc8e432f978a0b4966588242a — JoJo 1 year, 9 months ago 4138135
Impl all error-tests of err.carth as proper tests in CheckSpec.hs
3 files changed, 148 insertions(+), 174 deletions(-)

D examples/err.carth
M src/Parse.hs
M test/CheckSpec.hs
D examples/err.carth => examples/err.carth +0 -112
@@ 1,112 0,0 @@
(import std)

;; Start not defined
(define (start _) (undefined unit))

;; Invalid user type signature
;; (define: (invalid-user-type-signature x)
;;     (forall [a b c] (Fun a a))
;;   x)

;; Arity mismatch for constructor
;; (define arity-mismatch-for-constructor
;;   (match (Integ 1)
;;     [(Integ foo bar) foo]))

;; Conflicting definitions of variables in pattern
;; (define conflicting-defs-in-pat
;;   (match (IntPair 1 2)
;;     [(IntPair a a) a]))

;; Undefined constructor
;; (define undef-ctor ThisCtorIsUndefined)

;; Undefined variable
;; (define undef-var this-var-is-undefined)

;; Infinite type
;; (define infinite-type (Wrap infinite-type))

;; Type mismatch
;; (define type-mismatch (Integ "foo"))

;; Conflicting definitions for type
;; (type Foo)
;; (type Foo)

;; Conflicting definitions for constructor
;; a)
;; (type Foo Bar Bar)
;; b)
;; (type Baz Baz)
;; (type Quux Baz)

;; Redundant case in pattern match
;; (define foo
;;   (fun-match
;;     (case true 0)
;;     (case true 1)
;;     (case false 2)))

;; Inexhaustive patterns
;; (define foo
;;   (fun-match
;;     (case true 0)))

;; Extern is not monomorphic
;; (extern foo (Fun a Int))

;; Found hole
;; (define foo
;;   _)

;; Type has infinite size due to recursion
;; (type Foo (Foo Foo))

;; Undefined type
;; a)
;; (type Foo (Foo Bar))
;; b)
;; TODO: This one compiles
;; (define: foo
;;     (Fun Int Foo)
;;   (undefined unit))

;; Could not fully infer type of expression. Unbound type variable.
;; (define foo
;;   (seq (undefined unit)
;;        123))

;; Incorrect type of start
;; (define: start
;;     Int
;;   (undefined unit))

;; Non-function variable definition is recursive
;; (define: foo
;;     Int
;;   (+ foo 1))

;; Arity mismatch for instantiation of type
;; a)
;; (type Foo (Foo List))
;; b)
;; TODO: This is not an error, but should be
;; (define: foo
;;     (Fun Int List)
;;   (undefined unit))

;; Conflicting definitions for variable
;; a)
;; (define foo +)
;; (define foo -)
;; b)
;; (define foo
;;   (let ((a 1)
;;         (a 2))
;;     a))

;; Helpers
(type (Wrap a) (Wrap a))
(type Integ (Integ Int))
(type IntPair (IntPair Int Int))

M src/Parse.hs => src/Parse.hs +1 -0
@@ 12,6 12,7 @@ module Parse
    , Source
    , parse
    , parse'
    , toplevels
    , reserveds
    , ns_scheme
    , ns_pat

M test/CheckSpec.hs => test/CheckSpec.hs +147 -62
@@ 4,101 4,186 @@ module CheckSpec where

import Test.Hspec

import AnnotAst
import qualified Ast
import qualified DesugaredAst as Des
import Parse
import Check
import TypeErr

pStartNotDefined = "(define foo unit)"
pInvalidUserTypeSig = concat
    [ "(define: (invalid-user-type-signature x)"
    , "    (forall (a b c) (Fun a a))"
    , "  x)"
    ]
pCtorArityMismatch = concat
    [ "(type Integ (Integ Int))"
    , "(define arity-mismatch-for-constructor"
    , "  (match (Integ 1)"
    , "    (case (Integ foo bar) foo)))"
    ]
pConflictingPatVarDefs = concat
    [ "(type 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 =
    "(type Integ (Integ Int)) (define type-mismatch (Integ true))"
pConflictingTypeDef = "(type Foo) (type Foo)"
pConflictingCtorDef_a = "(type Foo Bar Bar)"
pConflictingCtorDef_b = "(type Baz Baz) (type Quux Baz)"
pRedundantCase = concat
    [ "(define foo"
    , "  (fun-match"
    , "    (case true 0)"
    , "    (case true 1)"
    , "    (case false 2)))"
    ]
pInexhaustivePats = "(define foo (fun-match (case true 0)))"
pExternNotMonomorphic = "(extern foo (Fun a Int))"
pFoundHole = "(define foo _)"
pRecTypeDef = "(type Foo (Foo Foo))"
pUndefType_a = "(type Foo (Foo Bar))"
pUndefType_b = "(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))"
    ]
pWrongStartType = "(define: start Int (undefined unit))"
pRecursiveVarDef = "(define: foo Int (+ foo 1))"
pTypeInstArityMismatch = "(type (Foo a) (Foo a)) (type Bar (Bar Foo))"
pConflictingVarDef_a = "(define foo +) (define foo -)"
pConflictingVarDef_b = "(define foo (let ((a 1) (a 2)) a))"

spec :: Spec
spec = do
    let mainDef = "(define (main _) unit)"
    let p0 = "(define (foo _) unit)"
    let p1 = unlines ["(define: (id x) (forall [] (Fun a a)) x)", mainDef]
    let p2 = unlines
            [ "(type Foo Bar (Baz Int))"
            , "(define foo (fun-match [(Bar x) x]))"
            , mainDef
            ]
    let p3 = unlines
            [ "(type (Pair a b) (Pair a b))"
            , "(define foo (fun-match [(Pair x x) x]))"
            , mainDef
            ]
    let p4 = unlines ["(define foo (fun-match [Foo 3]))", mainDef]
    let p5 = unlines ["(define foo x)", mainDef]
    let p6 = unlines ["(define foo (foo foo))", mainDef]
    let p7 = unlines ["(define: (foo _) (Fun Int Int) 3.1415)", mainDef]
    let p8 = unlines ["(type Foo Bar)", "(type Foo Baz)", mainDef]
    let p9 = unlines ["(type Foo1 Bar)", "(type Foo2 Bar)", mainDef]
    let p10 =
            unlines
                [ "(type Foo Bar)"
                , "(define foo (fun-match [Bar 1] [Bar 2]))"
                , mainDef
                ]
    let p11 =
            unlines
                [ "(type Foo Bar Baz)"
                , "(define foo (fun-match [Bar 1]))"
                , mainDef
                ]
    let startDef = "(define (start _) unit)"
    describe "typecheck" $ do
        it "detects when main is not defined"
            $ shouldSatisfy (typecheck' p0)
        it "detects when start is not defined"
            $ shouldSatisfy (typecheck' pStartNotDefined)
            $ \case
                Right (Left MainNotDefined) -> True
                Right (Left StartNotDefined) -> True
                _ -> False
        it "detects invalid user type signatures"
            $ shouldSatisfy (typecheck' p1)
            $ shouldSatisfy (typecheck' pInvalidUserTypeSig)
            $ \case
                Right (Left (InvalidUserTypeSig _ _ _)) -> True
                Right (Left (InvalidUserTypeSig{})) -> True
                _ -> False
        it "detects arity mismatch in constructor"
            $ shouldSatisfy (typecheck' p2)
            $ shouldSatisfy (typecheck' pCtorArityMismatch)
            $ \case
                Right (Left (CtorArityMismatch _ _ _ _)) -> True
                Right (Left (CtorArityMismatch{})) -> True
                _ -> False
        it "detects conflicting pattern variable defs"
            $ shouldSatisfy (typecheck' p3)
            $ shouldSatisfy (typecheck' pConflictingPatVarDefs)
            $ \case
                Right (Left (ConflictingPatVarDefs _ _)) -> True
                Right (Left (ConflictingPatVarDefs{})) -> True
                _ -> False
        it "detects undefined constructors"
            $ shouldSatisfy (typecheck' p4)
            $ shouldSatisfy (typecheck' pUndefCtor)
            $ \case
                Right (Left (UndefCtor _ _)) -> True
                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 undefined variables" $ shouldSatisfy (typecheck' p5) $ \case
            Right (Left (UndefVar _ _)) -> True
            _ -> False
        it "detects infinite types" $ shouldSatisfy (typecheck' p6) $ \case
            Right (Left (InfType _ _ _ _ _)) -> True
            _ -> False
        it "detects type unification failure"
            $ shouldSatisfy (typecheck' p7)
            $ shouldSatisfy (typecheck' pUnificationFailed)
            $ \case
                Right (Left (UnificationFailed _ _ _ _ _)) -> True
                Right (Left (UnificationFailed{})) -> True
                _ -> False
        it "detects conflicting type definitions"
            $ shouldSatisfy (typecheck' p8)
            $ shouldSatisfy (typecheck' pConflictingTypeDef)
            $ \case
                Right (Left (ConflictingTypeDef _)) -> True
                Right (Left (ConflictingTypeDef{})) -> True
                _ -> False
        it "detects conflicting constructor definitions"
            $ shouldSatisfy (typecheck' p9)
        it "detects conflicting constructor definitions, withing"
            $ shouldSatisfy (typecheck' pConflictingCtorDef_a)
            $ \case
                Right (Left (ConflictingCtorDef _)) -> True
                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' p10)
            $ shouldSatisfy (typecheck' pRedundantCase)
            $ \case
                Right (Left (RedundantCase _)) -> True
                Right (Left (RedundantCase{})) -> True
                _ -> False
        it "detects inexhaustive patterns"
            $ shouldSatisfy (typecheck' p11)
            $ 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 var defs"
            $ shouldSatisfy (typecheck' pUndefType_b)
            $ \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 `start` is wrong"
            $ shouldSatisfy (typecheck' pWrongStartType)
            $ \case
                Right (Left (WrongStartType{})) -> 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 (InexhaustivePats _ _)) -> True
                Right (Left (ConflictingVarDef{})) -> True
                _ -> False

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