diff options
Diffstat (limited to 'lambda-calcul/haskell/test/Minilang')
3 files changed, 252 insertions, 2 deletions
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs index eaff77c..f1802da 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs @@ -81,3 +81,37 @@ spec = do it "lookup of '+' in builtin env yields FBuiltin" $ eval' benv (FV "+") `shouldBe` FBuiltin "+" + + describe "string literals and builtins" $ do + let benv = builtinDeBruijnEnv :: Env Text + + it "FStr self-evaluates" $ + eval' benv (FStr "hello") `shouldBe` FStr "hello" + + it "(str-concat \"foo\" \"bar\") reduces to FStr \"foobar\"" $ + eval' benv (App (App (FBuiltin "str-concat") (FStr "foo")) (FStr "bar")) + `shouldBe` FStr "foobar" + + it "(str-length \"hello\") reduces to FNum 5" $ + eval' benv (App (FBuiltin "str-length") (FStr "hello")) + `shouldBe` FNum 5 + + it "(str-slice 1 3 \"abcde\") reduces to FStr \"bc\"" $ + eval' benv (App (App (App (FBuiltin "str-slice") (FNum 1)) (FNum 3)) (FStr "abcde")) + `shouldBe` FStr "bc" + + it "(str= \"abc\" \"abc\") reduces to Church True" $ + eval' benv (App (App (FBuiltin "str=") (FStr "abc")) (FStr "abc")) + `shouldBe` Lam "f" (Lam "t" (Var "t" 0)) + + it "(str= \"abc\" \"xyz\") reduces to Church False" $ + eval' benv (App (App (FBuiltin "str=") (FStr "abc")) (FStr "xyz")) + `shouldBe` Lam "f" (Lam "t" (Var "f" 1)) + + it "(str< \"a\" \"b\") reduces to Church True" $ + eval' benv (App (App (FBuiltin "str<") (FStr "a")) (FStr "b")) + `shouldBe` Lam "f" (Lam "t" (Var "t" 0)) + + it "(str-concat \"hello\") is partial: stays as App spine" $ + eval' benv (App (FBuiltin "str-concat") (FStr "hello")) + `shouldBe` App (FBuiltin "str-concat") (FStr "hello") diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs index e5075f0..96fff08 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs @@ -11,6 +11,7 @@ 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 qualified Data.Text as Text import Minilang.Lambda.Infer (newContext) import Minilang.Lambda.Parser (parseProgram) import Minilang.REPL.Types (Evaluator (..), Language (..)) @@ -196,6 +197,101 @@ spec = do normalise (App (App (Var "mod") (Num 5)) (Num 0)) `shouldBe` App (App (Var "mod") (Num 5)) (Num 0) + describe "string literals and builtins" $ do + -- Self-evaluation + it "string literal evaluates to itself" $ + normalise (Str "hello") `shouldBe` Str "hello" + + it "empty string evaluates to itself" $ + normalise (Str "") `shouldBe` Str "" + + prop "any string literal normalises to itself" $ \s -> + normalise (Str (Text.pack s)) === Str (Text.pack s) + + -- eval produces VStr + prop "eval of a string literal produces VStr" $ \s -> + eval [] (Str (Text.pack s)) === VStr (Text.pack s) + + -- String in function position is stuck + it "string in function position produces a stuck application" $ + normalise (App (Str "oops") (Var "x")) + `shouldBe` App (Str "oops") (Var "x") + + -- str-concat + it "(str-concat \"foo\" \"bar\") == \"foobar\"" $ + normalise (App (App (Var "str-concat") (Str "foo")) (Str "bar")) + `shouldBe` Str "foobar" + + it "(str-concat \"\" \"abc\") == \"abc\"" $ + normalise (App (App (Var "str-concat") (Str "")) (Str "abc")) + `shouldBe` Str "abc" + + prop "str-concat is associative" $ \a b c -> + let s x = Str (Text.pack x) + cat x y = App (App (Var "str-concat") x) y + in normalise (cat (cat (s a) (s b)) (s c)) + === normalise (cat (s a) (cat (s b) (s c))) + + -- str-length + it "(str-length \"hello\") == 5" $ + normalise (App (Var "str-length") (Str "hello")) `shouldBe` Num 5 + + it "(str-length \"\") == 0" $ + normalise (App (Var "str-length") (Str "")) `shouldBe` Num 0 + + prop "str-length of concat equals sum of lengths" $ \a b -> + let sa = Text.pack a; sb = Text.pack b + in normalise (App (Var "str-length") (App (App (Var "str-concat") (Str sa)) (Str sb))) + === normalise (App (App (Var "+") (App (Var "str-length") (Str sa))) + (App (Var "str-length") (Str sb))) + + -- str-slice + it "(str-slice 1 3 \"abcde\") == \"bc\"" $ + normalise (App (App (App (Var "str-slice") (Num 1)) (Num 3)) (Str "abcde")) + `shouldBe` Str "bc" + + it "(str-slice 0 0 \"abc\") == \"\"" $ + normalise (App (App (App (Var "str-slice") (Num 0)) (Num 0)) (Str "abc")) + `shouldBe` Str "" + + -- str= (Church booleans) + it "(str= \"abc\" \"abc\") == Church True" $ + normalise (App (App (Var "str=") (Str "abc")) (Str "abc")) + `shouldBe` Lam "f" (Lam "t" (Var "t")) + + it "(str= \"abc\" \"xyz\") == Church False" $ + normalise (App (App (Var "str=") (Str "abc")) (Str "xyz")) + `shouldBe` Lam "f" (Lam "t" (Var "f")) + + prop "str= is reflexive" $ \s -> + normalise (App (App (Var "str=") (Str (Text.pack s))) (Str (Text.pack s))) + === Lam "f" (Lam "t" (Var "t")) + + -- str< + it "(str< \"abc\" \"abd\") == Church True" $ + normalise (App (App (Var "str<") (Str "abc")) (Str "abd")) + `shouldBe` Lam "f" (Lam "t" (Var "t")) + + it "(str< \"b\" \"a\") == Church False" $ + normalise (App (App (Var "str<") (Str "b")) (Str "a")) + `shouldBe` Lam "f" (Lam "t" (Var "f")) + + -- Partial application + it "(str-concat \"hello\") is partial" $ + eval builtinEnvValue (App (Var "str-concat") (Str "hello")) + `shouldBe` Builtin "str-concat" 1 [VStr "hello"] + + -- Stuck: free variable argument + it "(str-concat x \"bar\") with free x stays stuck" $ + normalise (App (App (Var "str-concat") (Var "x")) (Str "bar")) + `shouldBe` App (App (Var "str-concat") (Var "x")) (Str "bar") + + -- Higher-order: pass builtin as function + it "str-concat passed as higher-order argument works" $ + normalise (App (Lam "f" (App (App (Var "f") (Str "hello")) (Str " world"))) + (Var "str-concat")) + `shouldBe` Str "hello world" + describe "evaluator equivalence on challenges" $ do challenges <- runIO $ eitherDecodeFileStrict "challenges.json" >>= \case @@ -243,6 +339,7 @@ challengeEquivalenceTest env Challenge{level, expr} = eraseNames :: DB.DeBruijn Text -> DB.DeBruijn () eraseNames (DB.FV x) = DB.FV x eraseNames (DB.FNum n) = DB.FNum n +eraseNames (DB.FStr s) = DB.FStr s eraseNames (DB.FBuiltin b) = DB.FBuiltin b eraseNames (DB.Var _ i) = DB.Var () i eraseNames (DB.Lam _ body) = DB.Lam () (eraseNames body) diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs index 08ec661..40866bb 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs @@ -10,7 +10,7 @@ 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 Minilang.Lambda.Parser (AST (..), desugar, initialChars, parse, parseProgram, pretty, restChars, escapeString) import Minilang.Lambda.Eval (normalise) import Test.Hspec (Spec, describe, it, parallel, shouldBe, shouldSatisfy) import Test.Hspec.QuickCheck (prop) @@ -175,6 +175,115 @@ spec = parallel $ do it "pretty (+ 1) is \"(+ 1)\"" $ pretty (App (Sym "+") (Lit 1) []) `shouldBe` "(+ 1)" + describe "string literals" $ do + -- Round-trip: parse . pretty == id for all safe StrLit values + prop "any StrLit rendered by pretty parses back to the same StrLit" $ + forAll genStrLit $ \ast -> + parse (pretty ast) === Right ast + + it "parses empty string literal" $ + parse "\"\"" `shouldBe` Right (StrLit "") + + it "parses simple string literal" $ + parse "\"hello\"" `shouldBe` Right (StrLit "hello") + + it "parses string with spaces" $ + parse "\"foo bar\"" `shouldBe` Right (StrLit "foo bar") + + it "parses escaped double-quote inside string" $ + parse "\"say \\\"hi\\\"\"" `shouldBe` Right (StrLit "say \"hi\"") + + it "parses escaped backslash inside string" $ + parse "\"back\\\\slash\"" `shouldBe` Right (StrLit "back\\slash") + + it "pretty-prints string with double-quote escaped" $ + pretty (StrLit "say \"hi\"") `shouldBe` "\"say \\\"hi\\\"\"" + + it "pretty-prints string with backslash escaped" $ + pretty (StrLit "back\\slash") `shouldBe` "\"back\\\\slash\"" + + -- desugar / normalise + it "desugar and normalise string self-evaluates" $ + normalise (desugar (StrLit "hello")) `shouldBe` Eval.Str "hello" + + it "desugar and normalise str-concat" $ + normalise (desugar (App (Sym "str-concat") (StrLit "foo") [StrLit "bar"])) + `shouldBe` Eval.Str "foobar" + + it "desugar and normalise str-length" $ + normalise (desugar (App (Sym "str-length") (StrLit "hello") [])) + `shouldBe` Eval.Num 5 + + it "desugar and normalise str-slice" $ + normalise (desugar (App (Sym "str-slice") (Lit 1) [Lit 3, StrLit "abcde"])) + `shouldBe` Eval.Str "bc" + + it "desugar and normalise str= equal strings gives Church True" $ + normalise (desugar (App (Sym "str=") (StrLit "abc") [StrLit "abc"])) + `shouldBe` Eval.Lam "f" (Eval.Lam "t" (Eval.Var "t")) + + it "desugar and normalise str= unequal strings gives Church False" $ + normalise (desugar (App (Sym "str=") (StrLit "abc") [StrLit "xyz"])) + `shouldBe` Eval.Lam "f" (Eval.Lam "t" (Eval.Var "f")) + + it "partial str-concat pretty-prints as application" $ + pretty (App (Sym "str-concat") (StrLit "hello") []) + `shouldBe` "(str-concat \"hello\")" + + describe "strings containing parentheses" $ do + -- The parser must not treat ( or ) inside a string literal as + -- delimiters for an application or lambda expression. + + it "parses a string containing only an opening paren" $ + parse "\"(\"" `shouldBe` Right (StrLit "(") + + it "parses a string containing only a closing paren" $ + parse "\")\"" `shouldBe` Right (StrLit ")") + + it "parses a string containing balanced parens" $ + parse "\"(hello)\"" `shouldBe` Right (StrLit "(hello)") + + it "parses a string containing doubly-nested parens" $ + parse "\"((nested))\"" `shouldBe` Right (StrLit "((nested))") + + it "parses a string containing unbalanced parens" $ + parse "\"a(b\"" `shouldBe` Right (StrLit "a(b") + + it "parses a string that looks like a lambda expression" $ + parse "\"(lam (x) x)\"" `shouldBe` Right (StrLit "(lam (x) x)") + + it "parses a string that looks like an application" $ + parse "\"(f x)\"" `shouldBe` Right (StrLit "(f x)") + + -- Round-trip: pretty-printing a StrLit with parens re-parses correctly + it "pretty-prints and re-parses string with opening paren" $ + parse (pretty (StrLit "(")) `shouldBe` Right (StrLit "(") + + it "pretty-prints and re-parses string with balanced parens" $ + parse (pretty (StrLit "(hello)")) `shouldBe` Right (StrLit "(hello)") + + it "pretty-prints and re-parses string with doubly-nested parens" $ + parse (pretty (StrLit "((x))")) `shouldBe` Right (StrLit "((x))") + + -- Property: any string containing only parens and letters round-trips + prop "strings with parentheses round-trip through pretty and parse" $ + forAll (StrLit . Text.pack <$> listOf (elements "abcdef()")) $ \ast -> + parse (pretty ast) === Right ast + + -- The paren-containing string is correctly passed through an application + it "paren string survives beta-reduction" $ + normalise (desugar (App (Abs ["x"] (Sym "x")) (StrLit "(hello)") [])) + `shouldBe` Eval.Str "(hello)" + + -- str-concat of two paren strings + it "str-concat of paren strings produces correct result" $ + normalise (desugar (App (Sym "str-concat") (StrLit "(") [StrLit ")"])) + `shouldBe` Eval.Str "()" + + it "str-length of paren string counts parens" $ + normalise (desugar (App (Sym "str-length") (StrLit "(hello)") [])) + `shouldBe` Eval.Num 7 + it "parses multiline program with blank lines" $ do let program = "(def id (lam (x) x))\n\ @@ -230,6 +339,7 @@ instance Arbitrary AST where shrink = \case Sym _ -> [] Lit _ -> [] + StrLit _ -> [] Abs bind body -> case shrink (Identifier <$> bind) of [] -> shrink body bind' -> @@ -245,15 +355,24 @@ instance Arbitrary AST where Def _name body -> shrink body -- never generated genAst :: Int -> Gen AST -genAst 0 = oneof [Sym . unIdent <$> arbitrary, Lit <$> arbitrary] +genAst 0 = oneof [Sym . unIdent <$> arbitrary, Lit <$> arbitrary, genStrLit] genAst depth = oneof [ Sym . unIdent <$> arbitrary , Lit <$> arbitrary + , genStrLit , genAbstraction depth , genApplication depth ] +-- | Generate a random string literal. We restrict the alphabet to printable +-- ASCII excluding @\"@ and @\\@ to keep round-trip tests simple; the escape +-- logic is tested separately. +genStrLit :: Gen AST +genStrLit = StrLit . pack <$> listOf (elements safeChars) + where + safeChars = filter (\c -> c /= '"' && c /= '\\') [' '..'~'] + genDef :: Int -> Gen AST genDef n = Def . unIdent <$> arbitrary <*> genAst n |