swarm-0.7.0.0: test/unit/TestEval.hs
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Swarm unit tests
module TestEval where
import Control.Lens ((^.), _3)
import Data.Char (ord)
import Data.Fix
import Data.Map qualified as M
import Data.Text (Text)
import Data.Text qualified as T
import Graphics.Vty.Input.Events qualified as V
import Swarm.Game.State
import Swarm.Game.Value (Valuable (..))
import Swarm.Language.Key
import Swarm.Language.Syntax.Direction
import Swarm.Language.Types
import Swarm.Language.Value
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck
import TestUtil
import Witch (from)
testEval :: GameState -> TestTree
testEval g =
testGroup
"Language - evaluation"
[ testGroup
"arithmetic"
[ testProperty
"addition"
(\a b -> binOp a "+" b `evaluatesToP` VInt (a + b))
, testProperty
"subtraction"
(\a b -> binOp a "-" b `evaluatesToP` VInt (a - b))
, testProperty
"multiplication"
(\a b -> binOp a "*" b `evaluatesToP` VInt (a * b))
, testProperty
"division"
(\a (NonZero b) -> binOp a "/" b `evaluatesToP` VInt (a `div` b))
, testProperty
"exponentiation"
(\a (NonNegative b) -> binOp a "^" b `evaluatesToP` VInt (a ^ (b :: Integer)))
]
, testGroup
"int comparison"
[ testProperty
"=="
(\a b -> binOp a "==" b `evaluatesToP` VBool ((a :: Integer) == b))
, testProperty
"<"
(\a b -> binOp a "<" b `evaluatesToP` VBool ((a :: Integer) < b))
, testProperty
"<="
(\a b -> binOp a "<=" b `evaluatesToP` VBool ((a :: Integer) <= b))
, testProperty
">"
(\a b -> binOp a ">" b `evaluatesToP` VBool ((a :: Integer) > b))
, testProperty
">="
(\a b -> binOp a ">=" b `evaluatesToP` VBool ((a :: Integer) >= b))
, testProperty
"!="
(\a b -> binOp a "!=" b `evaluatesToP` VBool ((a :: Integer) /= b))
]
, testGroup
"pair comparison"
[ testProperty
"=="
(\a b -> binOp a "==" b `evaluatesToP` VBool ((a :: (Integer, Integer)) == b))
, testProperty
"<"
(\a b -> binOp a "<" b `evaluatesToP` VBool ((a :: (Integer, Integer)) < b))
, testProperty
"<="
(\a b -> binOp a "<=" b `evaluatesToP` VBool ((a :: (Integer, Integer)) <= b))
, testProperty
">"
(\a b -> binOp a ">" b `evaluatesToP` VBool ((a :: (Integer, Integer)) > b))
, testProperty
">="
(\a b -> binOp a ">=" b `evaluatesToP` VBool ((a :: (Integer, Integer)) >= b))
, testProperty
"!="
(\a b -> binOp a "!=" b `evaluatesToP` VBool ((a :: (Integer, Integer)) /= b))
]
, testGroup
"boolean operators"
[ testCase
"and"
("true && false" `evaluatesTo` VBool False)
, testCase
"or"
("true || false" `evaluatesTo` VBool True)
]
, testGroup
"sum types #224"
[ testCase
"inl"
("inl 3" `evaluatesTo` VInj False (VInt 3))
, testCase
"inr"
("inr \"hi\"" `evaluatesTo` VInj True (VText "hi"))
, testCase
"inl a < inl b"
("inl 3 < inl 4" `evaluatesTo` VBool True)
, testCase
"inl b < inl a"
("inl 4 < inl 3" `evaluatesTo` VBool False)
, testCase
"inl < inr"
("inl 3 < inr true" `evaluatesTo` VBool True)
, testCase
"inl 4 < inr 3"
("inl 4 < inr 3" `evaluatesTo` VBool True)
, testCase
"inr < inl"
("inr 3 < inl true" `evaluatesTo` VBool False)
, testCase
"inr 3 < inl 4"
("inr 3 < inl 4" `evaluatesTo` VBool False)
, testCase
"inr a < inr b"
("inr 3 < inr 4" `evaluatesTo` VBool True)
, testCase
"inr b < inr a"
("inr 4 < inr 3" `evaluatesTo` VBool False)
, testCase
"case inl"
("case (inl 2) (\\x. x + 1) (\\y. y * 17)" `evaluatesTo` VInt 3)
, testCase
"case inr"
("case (inr 2) (\\x. x + 1) (\\y. y * 17)" `evaluatesTo` VInt 34)
, testCase
"nested 1"
("(\\x : Int + Bool + Text. case x (\\q. 1) (\\s. case s (\\y. 2) (\\z. 3))) (inl 3)" `evaluatesTo` VInt 1)
, testCase
"nested 2"
("(\\x : Int + Bool + Text. case x (\\q. 1) (\\s. case s (\\y. 2) (\\z. 3))) (inr (inl false))" `evaluatesTo` VInt 2)
, testCase
"nested 2"
("(\\x : Int + Bool + Text. case x (\\q. 1) (\\s. case s (\\y. 2) (\\z. 3))) (inr (inr \"hi\"))" `evaluatesTo` VInt 3)
]
, testGroup
"operator evaluation"
[ testCase
"application operator #239"
("(\\x. -x) $ (\\x. x^2) $ 2" `evaluatesTo` VInt (-4))
]
, testGroup
"recursive bindings"
[ testCase
"factorial"
("let fac = \\n. if (n==0) {1} {n * fac (n-1)} in fac 15" `evaluatesTo` VInt 1307674368000)
, testCase
"loop detected"
("let x = x in x" `throwsError` ("loop detected" `T.isInfixOf`))
]
, testGroup
"delay"
[ testCase
"force / delay"
("force {10}" `evaluatesTo` VInt 10)
, testCase
"force x2 / delay x2"
("force (force { {10} })" `evaluatesTo` VInt 10)
, testCase
"if is lazy"
("if true {1} {1/0}" `evaluatesTo` VInt 1)
, testCase
"function with if is not lazy"
( "let f = \\x. \\y. if true {x} {y} in f 1 (1/0)"
`throwsError` ("by zero" `T.isInfixOf`)
)
, testCase
"memoization baseline"
( "def fac = \\n. if (n==0) {1} {n * fac (n-1)} end; def f10 = fac 10 end; let x = f10 in noop"
`evaluatesToInAtMost` (VUnit, 535)
)
, testCase
"memoization"
( "def fac = \\n. if (n==0) {1} {n * fac (n-1)} end; def f10 = fac 10 end; let x = f10 in let y = f10 in noop"
`evaluatesToInAtMost` (VUnit, 540)
)
]
, testGroup
"conditions"
[ testCase
"if true"
("if true {1} {2}" `evaluatesTo` VInt 1)
, testCase
"if false"
("if false {1} {2}" `evaluatesTo` VInt 2)
, testCase
"if (complex condition)"
("if (let x = 3 + 7 in not (x < 2^5)) {1} {2}" `evaluatesTo` VInt 2)
]
, testGroup
"exceptions"
[ testCase
"fail"
("fail \"foo\"" `throwsError` ("foo" `T.isInfixOf`))
, testCase
"try / no exception 1"
("try {pure 1} {pure 2}" `evaluatesTo` VInt 1)
, testCase
"try / no exception 2"
("try {pure 1} {let x = x in x}" `evaluatesTo` VInt 1)
, testCase
"try / fail"
("try {fail \"foo\"} {pure 3}" `evaluatesTo` VInt 3)
, testCase
"try / fail / fail"
("try {fail \"foo\"} {fail \"bar\"}" `throwsError` ("bar" `T.isInfixOf`))
, testCase
"try / div by 0"
("try {pure (1/0)} {pure 3}" `evaluatesTo` VInt 3)
]
, testGroup
"text"
[ testCase
"format int"
("format 1" `evaluatesTo` VText "1")
, testCase
"format sum"
("format (inl 1)" `evaluatesTo` VText "inl 1")
, testCase
"format function"
("format (\\x. x + 1)" `evaluatesTo` VText "\\x. x + 1")
, testCase
"format forall"
("format \"∀\"" `evaluatesTo` VText "\"∀\"")
, testCase
"concat"
("\"x = \" ++ format (2+3) ++ \"!\"" `evaluatesTo` VText "x = 5!")
, testProperty
"number of characters"
( \s ->
("chars " <> tquote s) `evaluatesToP` VInt (fromIntegral $ length s)
)
, testProperty
"split undo concatenation"
( \s1 s2 ->
-- \s1.\s2. (s1,s2) == split (chars s1) (s1 ++ s2)
let (t1, t2) = (tquote s1, tquote s2)
in T.concat ["(", t1, ",", t2, ") == split (chars ", t1, ") (", t1, " ++ ", t2, ")"]
`evaluatesToP` VBool True
)
, testProperty
"charAt"
$ \i (NonEmpty s) ->
let i' = i `mod` length s
in T.concat ["charAt ", from @String (show i'), " ", tquote s]
`evaluatesToP` VInt (fromIntegral (ord (s !! i')))
, testCase
"toChar 97"
("toChar 97 == \"a\"" `evaluatesTo` VBool True)
, testProperty
"chars/toChar"
( \(NonNegative (i :: Integer)) ->
T.concat ["chars (toChar ", from @String (show i), ")"]
`evaluatesToP` VInt 1
)
, testProperty
"charAt/toChar"
( \(NonNegative i) ->
T.concat ["charAt 0 (toChar ", from @String (show i), ")"]
`evaluatesToP` VInt i
)
]
, testGroup
"read"
[ testCase
"read Unit"
("read @Unit \"()\"" `evaluatesToV` ())
, testCase
"read Unit with spaces"
("read @Unit \" () \"" `evaluatesToV` ())
, testCase
"no read Unit"
("read @Unit \"xyz\"" `throwsError` ("Could not read" `T.isInfixOf`))
, testCase
"read Int"
("read @Int \"32\"" `evaluatesToV` (32 :: Integer))
, testCase
"read negative Int"
("read @Int \"-32\"" `evaluatesToV` (-32 :: Integer))
, testCase
"read Int with spaces"
("read @Int \" - 32 \"" `evaluatesToV` (-32 :: Integer))
, testCase
"no read Int"
("read @Int \"32.0\"" `throwsError` ("Could not read" `T.isInfixOf`))
, testCase
"read false"
("read @Bool \"false\"" `evaluatesToV` False)
, testCase
"read true"
("read @Bool \"true\"" `evaluatesToV` True)
, testCase
"read forward"
( "read @Dir \"forward\""
`evaluatesTo` VDir (DRelative (DPlanar DForward))
)
, testCase
"read east"
("read @Dir \"east\"" `evaluatesTo` VDir (DAbsolute DEast))
, testCase
"read down"
("read @Dir \"down\"" `evaluatesTo` VDir (DRelative DDown))
, testCase
"read text"
("read @Text \"\\\"hi\\\"\"" `evaluatesToV` ("hi" :: Text))
, testCase
"read sum inl"
( "read @(Int + Bool) \"inl 3\""
`evaluatesToV` Left @Integer @Bool 3
)
, testCase
"read sum inr"
( "read @(Int + Bool) \"inr true\""
`evaluatesToV` Right @Integer True
)
, testCase
"read nested sum"
( "read @((Int + Bool) + Unit) \"inl (inr true)\""
`evaluatesToV` Left @_ @() (Right @Integer True)
)
, testCase
"read pair"
( "read @(Int * Bool) \"(3, true)\""
`evaluatesToV` (3 :: Integer, True)
)
, testCase
"read pair with non-atomic value"
( "read @(Int * (Unit + Bool)) \"(3, inr true)\""
`evaluatesToV` (3 :: Integer, Right @() True)
)
, testCase
"read nested pair"
( "read @(Int * Bool * Unit) \"(3, true, ())\""
`evaluatesToV` (3 :: Integer, (True, ()))
)
, testCase
"read left-nested pair"
( "read @((Int * Bool) * Unit) \"((3, true), ())\""
`evaluatesToV` ((3 :: Integer, True), ())
)
, testCase
"read empty record"
("read @[] \"[]\"" `evaluatesTo` VRcd M.empty)
, testCase
"read singleton record"
( "read @[x : Int] \"[x = 2]\""
`evaluatesTo` VRcd (M.singleton "x" (VInt 2))
)
, testCase
"read doubleton record"
( "read @[x : Int, y : Bool + Unit] \"[x = 2, y = inr ()]\""
`evaluatesTo` (VRcd . M.fromList $ [("x", VInt 2), ("y", VInj True VUnit)])
)
, testCase
"read permuted doubleton record"
( "read @[x : Int, y : Bool + Unit] \"[y = inr (), x = 2]\""
`evaluatesTo` (VRcd . M.fromList $ [("x", VInt 2), ("y", VInj True VUnit)])
)
, testCase
"no read record with repeated fields"
( "read @[x : Int] \"[x = 2, x = 3]\""
`throwsError` ("Could not read" `T.isInfixOf`)
)
, testCase
"read key"
( "read @Key \"key \\\"M-C-F5\\\"\""
`evaluatesTo` VKey (mkKeyCombo [V.MCtrl, V.MMeta] (V.KFun 5))
)
, testCase
"read recursive list"
( "read @(rec l. Unit + (Int * l)) \"inr (3, inr (5, inl ()))\""
`evaluatesToV` [3 :: Integer, 5]
)
, testCase
"read paper with int"
("read @Int \"paper: 52\"" `evaluatesToV` (52 :: Integer))
, testCase
"read paper with tuple"
( "read @(Int * Bool * Unit) \"paper: (3, false, ())\""
`evaluatesToV` (3 :: Integer, (False, ()))
)
, testCase
"read random entity with tuple"
( "read @(Int * Bool * Unit) \"foo: (3, false, ())\""
`evaluatesToV` (3 :: Integer, (False, ()))
)
, testCase
"read Text value containing colon"
( "read @Text \"\\\"hi: there\\\"\""
`evaluatesToV` ("hi: there" :: Text)
)
, testCase
"read at user-defined type Foo = Int"
( "tydef Foo = Int end; read @Foo \"3\""
`evaluatesToV` (3 :: Integer)
)
, testCase
"read at user-defined recursive type"
( "tydef List a = rec l. Unit + a * l end; read @(List(Int)) \"inr (1, inl ())\""
`evaluatesToV` [1 :: Integer]
)
, testCase
"read at complex type with user-defined types"
( "tydef Foo = Int end; read @(Bool * Foo) \"(True, 3)\""
`evaluatesToV` (True, 3 :: Integer)
)
, testCase
"read at nested user-defined type"
( "tydef A = Int end; tydef B = Bool end; tydef C = B * A end; read @C \"(True, 3)\""
`evaluatesToV` (True, 3 :: Integer)
)
]
, testGroup
"records - #1093"
[ testCase
"empty record"
("[]" `evaluatesTo` VRcd M.empty)
, testCase
"singleton record"
("[y = 3 + 4]" `evaluatesTo` VRcd (M.singleton "y" (VInt 7)))
, testCase
"record equality up to reordering"
("[x = 2, y = 3] == [y = 3, x = 2]" `evaluatesTo` VBool True)
, testCase
"record projection"
("[x = 2, y = 3].x" `evaluatesTo` VInt 2)
, testCase
"nested record projection"
("let r = [x=2, y=3] in let z = [q = r, n=\"hi\"] in z.q.y" `evaluatesTo` VInt 3)
, testCase
"record punning"
( "let x = 2 in let y = 3 in [x,y,z=\"hi\"]"
`evaluatesTo` VRcd (M.fromList [("x", VInt 2), ("y", VInt 3), ("z", VText "hi")])
)
, testCase
"record comparison"
("[y=1, x=2] < [x=3,y=0]" `evaluatesTo` VBool True)
, testCase
"record comparison"
("[y=1, x=3] < [x=3,y=0]" `evaluatesTo` VBool False)
, testCase
"record function"
("let f : [x:Int, y:Text] -> Int = \\r.r.x + 1 in f [x=3,y=\"hi\"]" `evaluatesTo` VInt 4)
, testCase
"format record"
("format [y = 2, x = 1+2]" `evaluatesTo` VText "[x = 3, y = 2]")
, testCase
"record fields don't scope over other fields"
( "let x = 1 in [x = x + 1, y = x]"
`evaluatesTo` VRcd (M.fromList [("x", VInt 2), ("y", VInt 1)])
)
]
, testGroup
"scope - #681"
[ testCase
"binder in local scope"
("def f = a <- scan down end; let a = 2 in f; pure (a+1)" `evaluatesTo` VInt 3)
, testCase
"binder in local scope, no type change"
("def f = a <- pure 1 end; let a = 2 in f; pure a" `evaluatesTo` VInt 2)
, testCase
"repeat with scan"
("def x = \\n. \\c. if (n==0) {} {c; x (n-1) c} end; x 10 ( c <- scan down; case c (\\_. say \"Hi\") (\\_. pure ()))" `evaluatesTo` VUnit)
, testCase
"nested recursion with binder - #1032"
("def go = \\n. if (n > 0) {i <- pure n; s <- go (n-1); pure (s+i)} {pure 0} end; go 4" `evaluatesTo` VInt 10)
, testCase
"binder in local scope - #1796"
("def x = \\x.x end; def foo = x <- pure 0 end; foo; pure (x 42)" `evaluatesTo` VInt 42)
]
, testGroup
"nesting"
[ testCase
"def nested in def"
("def x : Cmd Int = def y : Int = 3 end; pure (y + 2) end; x" `evaluatesTo` VInt 5)
, testCase
"nested def does not escape"
( "def z = 1 end; def x = def z = 3 end; pure (z + 2) end; n <- x; pure (n + z)"
`evaluatesTo` VInt 6
)
, testCase
"nested tydef"
( "def x = (tydef X = Int end; def z : X = 3 end; pure (z + 2)) end; x"
`evaluatesTo` VInt 5
)
]
, testCase
"tydef does not prevent forcing of recursive variables"
("def forever = \\c. c; forever c end; tydef X = Int end; def go = forever move end" `evaluatesTo` VUnit)
, testGroup
"term-level types"
[ testCase
"Int"
("@Int" `evaluatesTo` VType TyInt)
, testCase
"Int * Bool"
("@(Int * Bool)" `evaluatesTo` VType (TyInt :*: TyBool))
, testCase
"foo"
("@(rec a. a)" `evaluatesTo` VType (TyRec "a" (Fix (TyRecVarF NZ))))
, testCase
"list"
("@(rec l. Unit + Int * l)" `evaluatesTo` VType (TyRec "l" (TyUnit :+: (TyInt :*: Fix (TyRecVarF NZ)))))
]
]
where
tquote :: String -> Text
tquote = T.pack . show
throwsError :: Text -> (Text -> Bool) -> Assertion
throwsError tm p = do
result <- evaluate tm
case result of
Right _ -> assertFailure "Unexpected success"
Left err ->
p err
@? "Expected predicate did not hold on error message "
++ from @Text @String err
evaluatesTo :: Text -> Value -> Assertion
evaluatesTo tm val = do
result <- evaluate tm
assertBool "" $ Right val == (fst <$> result)
evaluatesToV :: Valuable v => Text -> v -> Assertion
evaluatesToV tm val = tm `evaluatesTo` asValue val
evaluatesToP :: Text -> Value -> Property
evaluatesToP tm val = ioProperty $ do
result <- evaluate tm
return . property $ Right val == (fst <$> result)
evaluatesToInAtMost :: Text -> (Value, Int) -> Assertion
evaluatesToInAtMost tm (val, maxSteps) = do
result <- evaluate tm
case result of
Left err -> assertFailure ("Evaluation failed: " ++ from @Text @String err)
Right (v, steps) -> do
assertBool "Values are not equal" (val == v)
assertBool ("Took more than " ++ show maxSteps ++ " steps!") (steps <= maxSteps)
evaluate :: Text -> IO (Either Text (Value, Int))
evaluate = fmap (^. _3) . eval g
binOp :: Show a => a -> String -> a -> Text
binOp a op b = from @String (p (show a) ++ op ++ p (show b))
where
p x = "(" ++ x ++ ")"