diff options
Diffstat (limited to 'lambda-calcul/haskell/test/Minilang')
| -rw-r--r-- | lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs | 26 | ||||
| -rw-r--r-- | lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs | 96 |
2 files changed, 85 insertions, 37 deletions
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs index d772fe0..f07b5a2 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs @@ -2,8 +2,11 @@ module Minilang.Lambda.EvalSpec (spec) where import Control.Concurrent (threadDelay) import Control.Concurrent.Async (race_) -import Minilang.Lambda.Eval (Term (..), Value, eval, normalise) -import Test.Hspec (Spec, describe, it, pending, shouldBe) +import Minilang.Lambda.Eval (Term (..), Value (..), eval, normalise) +import Test.Hspec (Spec, describe, it, shouldBe) +import Test.Hspec.QuickCheck (prop) +import Data.Text (pack) +import Test.QuickCheck (NonEmptyList (..), arbitrary, forAll, (===)) spec :: Spec spec = do @@ -65,6 +68,25 @@ spec = do normalise (App (App add' one) one) `shouldBe` two + describe "integer literals" $ do + -- An integer literal is already a normal form: normalise must return it unchanged. + prop "any integer literal normalises to itself" $ \n -> + normalise (Num n) === Num (n :: Int) + + -- eval on a bare Num must always produce the VNum value form, never a closure + -- or neutral, regardless of the integer's sign or magnitude. + prop "eval of any integer literal produces VNum" $ \n -> + eval [] (Num n) === VNum (n :: Int) + + -- A number is not a function. Applying it to any argument must leave a stuck + -- neutral application: App (Num n) (normalise arg). We test this with free + -- variables as arguments, which are themselves already in normal form. + prop "an integer in function position produces a stuck application" $ + forAll arbitrary $ \n -> + forAll (getNonEmpty <$> arbitrary) $ \x -> + normalise (App (Num n) (Var (pack x))) + === App (Num (n :: Int)) (Var (pack x)) + -- describe "call-by-name eval" $ do -- it "evaluates 'x' as itself" $ do -- normalise' (Var "x") `shouldBe` Var "x" diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs index 932eff6..e9cfc6b 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs @@ -4,31 +4,33 @@ module Minilang.Lambda.ParserSpec where -import Data.Either (isRight) +import Data.Either (isLeft, isRight) import Data.Function ((&)) import Data.Text (Text, pack) import qualified Data.Text as Text import Minilang.Lambda.Eval (Term (Lam)) import qualified Minilang.Lambda.Eval as Eval import Minilang.Lambda.Parser (AST (..), desugar, initialChars, parse, parseProgram, pretty, restChars) -import Test.Hspec (Spec, it, parallel, shouldBe, shouldSatisfy) +import Test.Hspec (Spec, describe, it, parallel, shouldBe, shouldSatisfy) import Test.Hspec.QuickCheck (prop) -import Test.QuickCheck - ( Arbitrary (..), - Gen, - NonEmptyList (..), - counterexample, - elements, - forAll, - forAllShrink, - listOf, - oneof, - resize, - sized, - vectorOf, - (===), - (==>), - ) +import Test.QuickCheck ( + Arbitrary (..), + Gen, + NonEmptyList (..), + Positive (..), + counterexample, + elements, + forAll, + forAllShrink, + listOf, + oneof, + resize, + sized, + suchThat, + vectorOf, + (===), + (==>), + ) -- ((f x) y) --> (f x y) -- (lam (x) (lam (y) y)) --> (lam (x y) y) @@ -103,6 +105,15 @@ spec = parallel $ do let text = pretty ast in parse text `shouldBe` Right ast + describe "integer literals" $ do + prop "any integer rendered by pretty parses back to the same Lit" $ \n -> + parse (pretty (Lit n)) === Right (Lit (n :: Int)) + + prop "a '-' separated from digits by spaces does not parse as an integer literal" $ + forAll (getPositive <$> (arbitrary :: Gen (Positive Int))) $ \n -> + let spaced = "- " <> Text.pack (show n) + in parse spaced `shouldSatisfy` (/= Right (Lit (negate n))) + it "parses multiline program with blank lines" $ do let program = "(def id (lam (x) x))\n\ @@ -111,10 +122,10 @@ spec = parallel $ do \(def apply (lam (f x) (f x)))\n\ \(apply id const)" expected = - [ Def "id" (Abs ["x"] (Sym "x")), - Def "const" (Abs ["x", "y"] (Sym "x")), - Def "apply" (Abs ["f", "x"] (App (Sym "f") (Sym "x") [])), - App + [ Def "id" (Abs ["x"] (Sym "x")) + , Def "const" (Abs ["x", "y"] (Sym "x")) + , Def "apply" (Abs ["f", "x"] (App (Sym "f") (Sym "x") [])) + , App (Sym "apply") (Sym "id") [Sym "const"] @@ -136,35 +147,50 @@ newtype Identifier = Identifier {unIdent :: Text} instance Arbitrary Identifier where arbitrary = - Identifier . pack - <$> ((:) <$> elements initialChars <*> listOf (elements restChars)) + ( Identifier . pack + <$> ((:) <$> elements initialChars <*> listOf (elements restChars)) + ) + `suchThat` (not . isIntLiteral . unIdent) + where + -- An identifier whose first characters would be consumed as an integer + -- literal by the parser must be excluded: the parser tries `lit` before + -- `sym`, so any string starting with digits, or with '-' immediately + -- followed by digits, would produce a Lit rather than a Sym. + isIntLiteral t = + case Text.unpack t of + ('-' : d : _) -> isDigit d + (d : _) -> isDigit d + [] -> False + isDigit c = c >= '0' && c <= '9' instance Arbitrary AST where arbitrary = genAst 10 shrink = \case Sym _ -> [] + Lit _ -> [] Abs bind body -> case shrink (Identifier <$> bind) of [] -> shrink body bind' -> [ shrunkAbs (unIdent <$> bound) body' - | bound <- bind', - body' <- shrink body + | bound <- bind' + , body' <- shrink body ] - where - shrunkAbs [] b = b - shrunkAbs bound b = Abs bound b + where + shrunkAbs [] b = b + shrunkAbs bound b = Abs bound b App x y [] -> [x, y] App x y rest -> (App x y <$> shrink rest) <> [x, y] Def _name body -> shrink body -- never generated genAst :: Int -> Gen AST -genAst 0 = Sym . unIdent <$> arbitrary +genAst 0 = oneof [Sym . unIdent <$> arbitrary, Lit <$> arbitrary] genAst depth = oneof - [ Sym . unIdent <$> arbitrary, - genAbstraction depth, - genApplication depth + [ Sym . unIdent <$> arbitrary + , Lit <$> arbitrary + , genAbstraction depth + , genApplication depth ] genDef :: Int -> Gen AST @@ -173,8 +199,8 @@ genDef n = Def . unIdent <$> arbitrary <*> genAst n genApplication :: Int -> Gen AST genApplication depth = do App <$> genAst d <*> genAst d <*> reasonablySized (listOf $ genAst d) - where - d = depth - 1 + where + d = depth - 1 genAbstraction :: Int -> Gen AST genAbstraction depth = do |