diff options
Diffstat (limited to 'lambda-calcul/haskell/test/Minilang')
6 files changed, 286 insertions, 14 deletions
diff --git a/lambda-calcul/haskell/test/Minilang/IntegrationSpec.hs b/lambda-calcul/haskell/test/Minilang/IntegrationSpec.hs index fa87cef..ef05e20 100644 --- a/lambda-calcul/haskell/test/Minilang/IntegrationSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/IntegrationSpec.hs @@ -7,6 +7,7 @@ import Data.Aeson (eitherDecodeFileStrict) import Data.Proxy (Proxy (..)) import Data.Text (Text) import Minilang.API +import Minilang.REPL.Types (Evaluator (..)) import Minilang.Server (Server (..), startServer, stopServer) import Network.HTTP.Client (defaultManagerSettings, newManager) import Servant.API ((:<|>) (..)) @@ -24,7 +25,6 @@ leaderboardClient :: ClientM [Score] scoreClient :: Maybe Token -> ClientM Score challengeClient :: Maybe Token -> ClientM Challenge answerClient :: Maybe Token -> Text -> ClientM () - registerClient :<|> unregisterClient :<|> leaderboardClient @@ -57,7 +57,7 @@ runC env action = spec :: Spec spec = - around withServer $ + around (withServer DeBruijn) $ describe "Full contest integration" $ do it "Alice can solve all challenges and reach the maximum grade" $ \Server{serverPort} -> do @@ -102,5 +102,5 @@ solveChallenge env token Challenge{level, answer} = do -- | Spawn the real server (which itself reads challenges.json and picks a -- free port) and tear it down after the test. -withServer :: (Server -> IO ()) -> IO () -withServer = bracket (startServer 0) stopServer +withServer :: Evaluator -> (Server -> IO ()) -> IO () +withServer evaluator = bracket (startServer 0 evaluator) stopServer diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs index 85c9d6b..eaff77c 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs @@ -1,9 +1,9 @@ {-# LANGUAGE TypeApplications #-} module Minilang.Lambda.DeBruijnSpec where -import Minilang.Lambda.DeBruijn (DeBruijn (..), eval, toDeBruijn, eval') +import Minilang.Lambda.DeBruijn (DeBruijn (..), Env, builtinDeBruijnEnv, eval, toDeBruijn, eval') import qualified Minilang.Lambda.Eval as Eval -import Test.Hspec (Spec, it, shouldBe) +import Test.Hspec (Spec, describe, it, shouldBe) import Data.Text (Text) spec :: Spec @@ -21,5 +21,63 @@ spec = do it "evaluates deBruijn term in env" $ do let term = App (FV "z") (FV "t") - env = [("z", toDeBruijn $ Eval.Lam "x" (Eval.Var "x"))] - eval' @Text env term `shouldBe` FV "t" + env = [("z", toDeBruijn $ Eval.Lam "x" (Eval.Var "x"))] + eval' env term `shouldBe` FV "t" + + describe "built-in arithmetic" $ do + let benv = builtinDeBruijnEnv :: Env Text + + it "(+ 3 4) reduces to FNum 7" $ + eval' benv (App (App (FBuiltin "+") (FNum 3)) (FNum 4)) + `shouldBe` FNum 7 + + it "(- 10 3) reduces to FNum 7" $ + eval' benv (App (App (FBuiltin "-") (FNum 10)) (FNum 3)) + `shouldBe` FNum 7 + + it "(* 2 5) reduces to FNum 10" $ + eval' benv (App (App (FBuiltin "*") (FNum 2)) (FNum 5)) + `shouldBe` FNum 10 + + it "(div 10 3) reduces to FNum 3" $ + eval' benv (App (App (FBuiltin "div") (FNum 10)) (FNum 3)) + `shouldBe` FNum 3 + + it "(mod 10 3) reduces to FNum 1" $ + eval' benv (App (App (FBuiltin "mod") (FNum 10)) (FNum 3)) + `shouldBe` FNum 1 + + it "(= 3 3) reduces to Church True" $ + eval' benv (App (App (FBuiltin "=") (FNum 3)) (FNum 3)) + `shouldBe` Lam "f" (Lam "t" (Var "t" 0)) + + it "(= 3 4) reduces to Church False" $ + eval' benv (App (App (FBuiltin "=") (FNum 3)) (FNum 4)) + `shouldBe` Lam "f" (Lam "t" (Var "f" 1)) + + it "(< 2 5) reduces to Church True" $ + eval' benv (App (App (FBuiltin "<") (FNum 2)) (FNum 5)) + `shouldBe` Lam "f" (Lam "t" (Var "t" 0)) + + it "(< 5 2) reduces to Church False" $ + eval' benv (App (App (FBuiltin "<") (FNum 5)) (FNum 2)) + `shouldBe` Lam "f" (Lam "t" (Var "f" 1)) + + it "(neg 7) reduces to FNum -7" $ + eval' benv (App (FBuiltin "neg") (FNum 7)) + `shouldBe` FNum (-7) + + it "(+ 1) partial: stays as a spine without reducing" $ + eval' benv (App (FBuiltin "+") (FNum 1)) + `shouldBe` App (FBuiltin "+") (FNum 1) + + it "(div 1 0) stays stuck" $ + eval' benv (App (App (FBuiltin "div") (FNum 1)) (FNum 0)) + `shouldBe` App (App (FBuiltin "div") (FNum 1)) (FNum 0) + + it "(+ x 1) with free x stays stuck" $ + eval' benv (App (App (FBuiltin "+") (FV "x")) (FNum 1)) + `shouldBe` App (App (FBuiltin "+") (FV "x")) (FNum 1) + + it "lookup of '+' in builtin env yields FBuiltin" $ + eval' benv (FV "+") `shouldBe` FBuiltin "+" diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs index f07b5a2..e5075f0 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs @@ -1,11 +1,21 @@ +{-# LANGUAGE LambdaCase #-} 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, shouldBe) +import Data.Aeson (eitherDecodeFileStrict) +import Data.Text (Text, pack) +import qualified Data.Text as Text +import Minilang.API (Challenge (..)) +import Minilang.Lambda (loadProgram) +import qualified Minilang.Lambda.DeBruijn as DB +import Minilang.Lambda.DeBruijn (toDeBruijn) +import Minilang.Lambda.Eval (Env, Term (..), Value (..), eval, normalise, builtinEnvValue, newEnv) +import Minilang.Lambda.Infer (newContext) +import Minilang.Lambda.Parser (parseProgram) +import Minilang.REPL.Types (Evaluator (..), Language (..)) +import Test.Hspec (Spec, describe, it, runIO, shouldBe) import Test.Hspec.QuickCheck (prop) -import Data.Text (pack) import Test.QuickCheck (NonEmptyList (..), arbitrary, forAll, (===)) spec :: Spec @@ -87,6 +97,113 @@ spec = do normalise (App (Num n) (Var (pack x))) === App (Num (n :: Int)) (Var (pack x)) + describe "built-in arithmetic" $ do + -- Basic two-argument reductions + it "(+ 3 4) normalises to 7" $ + normalise (App (App (Var "+") (Num 3)) (Num 4)) `shouldBe` Num 7 + + it "(- 10 3) normalises to 7" $ + normalise (App (App (Var "-") (Num 10)) (Num 3)) `shouldBe` Num 7 + + it "(* 2 5) normalises to 10" $ + normalise (App (App (Var "*") (Num 2)) (Num 5)) `shouldBe` Num 10 + + it "(div 10 3) normalises to 3" $ + normalise (App (App (Var "div") (Num 10)) (Num 3)) `shouldBe` Num 3 + + it "(mod 10 3) normalises to 1" $ + normalise (App (App (Var "mod") (Num 10)) (Num 3)) `shouldBe` Num 1 + + it "(= 3 3) normalises to Church True" $ + normalise (App (App (Var "=") (Num 3)) (Num 3)) + `shouldBe` Lam "f" (Lam "t" (Var "t")) + + it "(= 3 4) normalises to Church False" $ + normalise (App (App (Var "=") (Num 3)) (Num 4)) + `shouldBe` Lam "f" (Lam "t" (Var "f")) + + it "(< 2 5) normalises to Church True" $ + normalise (App (App (Var "<") (Num 2)) (Num 5)) + `shouldBe` Lam "f" (Lam "t" (Var "t")) + + it "(< 5 2) normalises to Church False" $ + normalise (App (App (Var "<") (Num 5)) (Num 2)) + `shouldBe` Lam "f" (Lam "t" (Var "f")) + + -- Compose with Church ite: (ite (= 3 3) (Num 1) (Num 2)) == 1 + -- ite c t e = c e t (True picks second arg, False picks first) + it "(= 3 3) composes with Church ite to select then-branch" $ + let ite = Lam "c" (Lam "t" (Lam "e" (App (App (Var "c") (Var "e")) (Var "t")))) + in normalise (App (App (App ite (App (App (Var "=") (Num 3)) (Num 3))) (Num 1)) (Num 2)) + `shouldBe` Num 1 + + it "(< 5 2) composes with Church ite to select else-branch" $ + let ite = Lam "c" (Lam "t" (Lam "e" (App (App (Var "c") (Var "e")) (Var "t")))) + in normalise (App (App (App ite (App (App (Var "<") (Num 5)) (Num 2))) (Num 1)) (Num 2)) + `shouldBe` Num 2 + + it "(neg 7) normalises to -7" $ + normalise (App (Var "neg") (Num 7)) `shouldBe` Num (-7) + + it "(neg -3) normalises to 3" $ + normalise (App (Var "neg") (Num (-3))) `shouldBe` Num 3 + + -- Nested arithmetic + it "(* 2 (+ 1 4)) normalises to 10" $ + normalise (App (App (Var "*") (Num 2)) (App (App (Var "+") (Num 1)) (Num 4))) + `shouldBe` Num 10 + + -- Properties + prop "addition is commutative" $ \x y -> + normalise (App (App (Var "+") (Num x)) (Num y)) + === normalise (App (App (Var "+") (Num y)) (Num (x :: Int))) + + prop "subtraction is the inverse of addition" $ \x y -> + normalise (App (App (Var "-") (App (App (Var "+") (Num x)) (Num y))) (Num y)) + === Num (x :: Int) + + prop "multiplication by 0 is 0" $ \x -> + normalise (App (App (Var "*") (Num x)) (Num 0)) + === Num (0 :: Int) + + prop "neg is its own inverse" $ \x -> + normalise (App (Var "neg") (App (Var "neg") (Num x))) + === Num (x :: Int) + + -- Partial application + it "(+ 1) evaluates to a Builtin waiting for one more arg" $ + eval builtinEnvValue (App (Var "+") (Num 1)) + `shouldBe` Builtin "+" 1 [VNum 1] + + it "partial builtin applied to its last arg reduces" $ + eval builtinEnvValue (App (App (Var "+") (Num 1)) (Num 2)) + `shouldBe` VNum 3 + + it "partial builtin passed through a lambda reduces when applied" $ + normalise (App (Lam "f" (App (App (Var "f") (Num 3)) (Num 4))) (Var "+")) + `shouldBe` Num 7 + + -- Stuck / neutral cases + it "(+ x 1) with free x stays stuck" $ + normalise (App (App (Var "+") (Var "x")) (Num 1)) + `shouldBe` App (App (Var "+") (Var "x")) (Num 1) + + it "(div 1 0) stays stuck" $ + normalise (App (App (Var "div") (Num 1)) (Num 0)) + `shouldBe` App (App (Var "div") (Num 1)) (Num 0) + + it "(mod 5 0) stays stuck" $ + normalise (App (App (Var "mod") (Num 5)) (Num 0)) + `shouldBe` App (App (Var "mod") (Num 5)) (Num 0) + + describe "evaluator equivalence on challenges" $ do + challenges <- runIO $ + eitherDecodeFileStrict "challenges.json" >>= \case + Left err -> fail $ "Could not load challenges.json: " <> err + Right cs -> pure (cs :: [Challenge]) + + mapM_ (challengeEquivalenceTest newEnv) challenges + -- describe "call-by-name eval" $ do -- it "evaluates 'x' as itself" $ do -- normalise' (Var "x") `shouldBe` Var "x" @@ -96,6 +213,41 @@ spec = do -- shouldDiverge $ -- normalise' omega +-- | For a single challenge expression, parse it and run both evaluators, +-- asserting they produce alpha-equivalent results. +-- Alpha-equivalence is checked by converting both results to De Bruijn-indexed +-- form (which strips variable names) before comparing. +challengeEquivalenceTest :: Env -> Challenge -> Spec +challengeEquivalenceTest env Challenge{level, expr} = + it ("level " <> show level <> ": " <> Text.unpack (Text.take 60 expr)) $ + case parseProgram expr of + Left err -> + fail $ "Parse error for level " <> show level <> ": " <> show err + Right asts -> + let runWith ev = loadProgram ev Untyped env newContext asts + extractTerms (Right (terms, _, _)) = map fst terms + extractTerms (Left err) = error $ "Type error: " <> show err + -- Convert to annotation-erased De Bruijn to compare up to + -- alpha-equivalence. Both evaluators may choose different fresh + -- names for lambda binders (NbE normalises under binders and must + -- avoid capture); erasing names leaves only structure and indices. + toAlpha = map (eraseNames . toDeBruijn) . extractTerms + debruijnTerms = toAlpha (runWith DeBruijn) + nbeTerms = toAlpha (runWith NbE) + in nbeTerms `shouldBe` debruijnTerms + +-- | Erase all name annotations from a 'DeBruijn' term, leaving only the +-- structural skeleton (indices, numeric literals, free-variable names, and +-- builtin names). Two terms that are identical up to alpha-renaming of bound +-- variables will be equal after erasure. +eraseNames :: DB.DeBruijn Text -> DB.DeBruijn () +eraseNames (DB.FV x) = DB.FV x +eraseNames (DB.FNum n) = DB.FNum n +eraseNames (DB.FBuiltin b) = DB.FBuiltin b +eraseNames (DB.Var _ i) = DB.Var () i +eraseNames (DB.Lam _ body) = DB.Lam () (eraseNames body) +eraseNames (DB.App f a) = DB.App (eraseNames f) (eraseNames a) + shouldDiverge :: Term -> IO () shouldDiverge t = race_ diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs index e9cfc6b..08ec661 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs @@ -11,6 +11,7 @@ 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 Minilang.Lambda.Eval (normalise) import Test.Hspec (Spec, describe, it, parallel, shouldBe, shouldSatisfy) import Test.Hspec.QuickCheck (prop) import Test.QuickCheck ( @@ -114,6 +115,66 @@ spec = parallel $ do let spaced = "- " <> Text.pack (show n) in parse spaced `shouldSatisfy` (/= Right (Lit (negate n))) + describe "arithmetic operators" $ do + -- Operator names are valid identifiers: they parse as Sym and round-trip. + it "parses + as a symbol" $ + parse "+" `shouldBe` Right (Sym "+") + + it "parses - as a symbol" $ + parse "-" `shouldBe` Right (Sym "-") + + it "parses * as a symbol" $ + parse "*" `shouldBe` Right (Sym "*") + + it "parses div as a symbol" $ + parse "div" `shouldBe` Right (Sym "div") + + it "parses mod as a symbol" $ + parse "mod" `shouldBe` Right (Sym "mod") + + it "parses = as a symbol" $ + parse "=" `shouldBe` Right (Sym "=") + + it "parses < as a symbol" $ + parse "<" `shouldBe` Right (Sym "<") + + it "parses neg as a symbol" $ + parse "neg" `shouldBe` Right (Sym "neg") + + -- Full expression parses and round-trips + it "parses (+ 3 4) and pretty-prints back" $ + let expr = App (Sym "+") (Lit 3) [Lit 4] + in parse "(+ 3 4)" `shouldBe` Right expr + + it "pretty (+ 3 4) round-trips through parse" $ + let expr = App (Sym "+") (Lit 3) [Lit 4] + in parse (pretty expr) `shouldBe` Right expr + + -- desugar of an arithmetic expression produces a normalised integer + it "desugar and normalise (+ 3 4) == Num 7" $ + normalise (desugar (App (Sym "+") (Lit 3) [Lit 4])) `shouldBe` Eval.Num 7 + + it "desugar and normalise (* 2 (+ 1 4)) == Num 10" $ + normalise (desugar (App (Sym "*") (Lit 2) [App (Sym "+") (Lit 1) [Lit 4]])) + `shouldBe` Eval.Num 10 + + -- Comparison operators produce Church booleans + it "desugar and normalise (= 3 3) == Church True" $ + normalise (desugar (App (Sym "=") (Lit 3) [Lit 3])) + `shouldBe` Eval.Lam "f" (Eval.Lam "t" (Eval.Var "t")) + + it "desugar and normalise (= 3 4) == Church False" $ + normalise (desugar (App (Sym "=") (Lit 3) [Lit 4])) + `shouldBe` Eval.Lam "f" (Eval.Lam "t" (Eval.Var "f")) + + it "desugar and normalise (< 2 5) == Church True" $ + normalise (desugar (App (Sym "<") (Lit 2) [Lit 5])) + `shouldBe` Eval.Lam "f" (Eval.Lam "t" (Eval.Var "t")) + + -- A partial application (missing second arg) pretty-prints as an App + it "pretty (+ 1) is \"(+ 1)\"" $ + pretty (App (Sym "+") (Lit 1) []) `shouldBe` "(+ 1)" + it "parses multiline program with blank lines" $ do let program = "(def id (lam (x) x))\n\ diff --git a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs index bd64adf..e382df4 100644 --- a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs @@ -66,7 +66,7 @@ spec = parallel $ out `shouldBe` [ "Bye!", - "(lam (z s) (s ((lam (n z s) (s n)) (lam (z s) z)))) : <?>" + "(lam (z s) (s (lam (z s) (s (lam (z s) z))))) : <?>" ] it "do typecheck term when language is set to 'Typed'" $ do @@ -80,7 +80,7 @@ spec = parallel $ out `shouldBe` [ "Bye!", - "(lam (z s) (s ((lam (n z s) (s n)) (lam (z s) z)))) : a -> ((d -> ((g -> h -> g) -> f) -> f) -> j) -> j", + "(lam (z s) (s (lam (z s) (s (lam (z s) z))))) : a -> ((c -> ((e -> f -> e) -> g) -> g) -> h) -> h", "Language set to Typed" ] diff --git a/lambda-calcul/haskell/test/Minilang/ServerSpec.hs b/lambda-calcul/haskell/test/Minilang/ServerSpec.hs index f61969a..2860c40 100644 --- a/lambda-calcul/haskell/test/Minilang/ServerSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/ServerSpec.hs @@ -17,6 +17,7 @@ import qualified Data.Text.Lazy as LT import Data.Text.Lazy.Encoding (decodeUtf8) import Minilang.API (Challenge (..), Score (..), User (..), defaultChallenges, newToken) import Minilang.App (makeEnv) +import Minilang.REPL.Types (Evaluator (..)) import Minilang.Server (serveAPI) import Network.Wai (Application) import Network.Wai.Test (SResponse) @@ -200,7 +201,7 @@ arrayOfLengthOf _ len = MatchBody $ \_ actual -> app :: StdGen -> IO Application app g = do - env <- makeEnv g defaultChallenges + env <- makeEnv g defaultChallenges DeBruijn pure $ serveAPI env testSeed :: StdGen |