Add integers parsing

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