{-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE RankNTypes #-} module Main (main) where import qualified Data.List as List import Data.Text (Text) import qualified Data.Text as T import qualified Data.Text.IO as T import System.IO import Lang.Crucible.Syntax.Concrete (defaultParserHooks) import Lang.Crucible.Syntax.ExprParse import Lang.Crucible.Syntax.Monad import Lang.Crucible.Syntax.Prog (doParseCheck) import Lang.Crucible.Syntax.SExpr import Test.Tasty (defaultMain, TestTree, testGroup) import Test.Tasty.Golden import Test.Tasty.HUnit import qualified Text.Megaparsec as MP import System.FilePath import System.Directory import What4.ProgramLoc (Position(SourcePos), Posd(..)) main :: IO () main = do wd <- getCurrentDirectory putStrLn $ "Looking for tests in " ++ wd parseTests <- findTests "Parsing round-trips" "test-data" testParser let allTests = testGroup "Tests" [syntaxParsing, parseTests] defaultMain allTests findTests :: String -> FilePath -> (FilePath -> FilePath -> IO ()) -> IO TestTree findTests group_name test_dir test_action = do inputs <- findByExtension [".cbl"] test_dir return $ testGroup group_name [ goldenFileTestCase input test_action | input <- List.sort inputs ] goldenFileTestCase :: FilePath -> (FilePath -> FilePath -> IO ()) -> TestTree goldenFileTestCase input test_action = goldenVsFileDiff (takeBaseName input) -- test name (\x y -> ["diff", "-u", x, y]) goodFile -- golden file path outFile (test_action input outFile) -- action whose result is tested where outFile = replaceExtension input ".out" goodFile = replaceExtension input ".out.good" testParser :: FilePath -> FilePath -> IO () testParser inFile outFile = do contents <- T.readFile inFile let ?parserHooks = defaultParserHooks withFile outFile WriteMode $ doParseCheck inFile contents True data Lam = Lam [Text] (Datum TrivialAtom) deriving (Eq, Show) syntaxParsing :: TestTree syntaxParsing = let anyUnit :: SyntaxParse TrivialAtom () anyUnit = anything *> pure () vars :: SyntaxParse TrivialAtom [TrivialAtom] vars = describe "sequence of variable bindings" $ rep atomic distinctVars :: SyntaxParse TrivialAtom [TrivialAtom] distinctVars = sideCondition' "sequence of distinct variable bindings" (\xs -> List.nub xs == xs) vars lambda = fmap (\(_, (xs, (body, ()))) -> Lam [x | TrivialAtom x <- xs] (syntaxToDatum body)) (cons (atom "lambda") $ cons distinctVars $ cons anything $ emptyList) in testGroup "Syntax parsing lib" [ testCase "Empty list is empty list" $ do x <- syntaxTest "()" emptyList x @?= Right () , testCase "Empty list is not atom" $ do x <- syntaxTest "()" (atom ("foo" :: TrivialAtom)) x @?= Left (SyntaxError $ pure $ Reason { expr = Syntax {unSyntax = Posd {pos = fakeFilePos 1 1, pos_val = List []}} , message = "foo" }) , testCase "Atom is not empty list" $ do x <- syntaxTest "foo" emptyList x @?= Left (SyntaxError $ pure $ Reason { expr = Syntax {unSyntax = Posd {pos = fakeFilePos 1 1, pos_val = Atom (TrivialAtom "foo")}} , message = "empty expression ()" }) , testCase "Three element list of whatever" $ do x <- syntaxTest "(delicious avocado toast)" (list [anyUnit, anyUnit, anyUnit]) x @?= Right [(), (), ()] , testCase "Three element list of whatever, again" $ do x <- syntaxTest "(delicious (avocado and tomato) toast)" (list [anyUnit, anyUnit, anyUnit]) x @?= Right [(), (), ()] , testCase "Three element list of atoms" $ do x <- syntaxTest "(delicious avocado toast)" (list [atomic, atomic, atomic]) x @?= Right [TrivialAtom "delicious", TrivialAtom "avocado", TrivialAtom "toast"] , testCase "Three element list of non-atoms isn't atoms" $ do x <- syntaxTest "((delicious) avocado toast)" (list [atomic, atomic, atomic]) x @?= Left (SyntaxError $ pure $ Reason { expr = Syntax $ Posd { pos = fakeFilePos 1 2 , pos_val = List [ Syntax (Posd (fakeFilePos 1 3) (Atom (TrivialAtom "delicious"))) ] } , message = "an atom" }) , testCase "Three element list of non-atoms still isn't atoms" $ do x <- syntaxTest "(delicious (avocado) toast)" (list [atomic, atomic, atomic]) x @?= Left (SyntaxError $ pure $ Reason { expr = Syntax $ Posd { pos = fakeFilePos 1 12 , pos_val = List [ Syntax (Posd (fakeFilePos 1 13) (Atom (TrivialAtom "avocado"))) ] } , message = "an atom" }) , testCase "Many three-element lists of whatever (1)" $ do x <- syntaxTest "((delicious avocado toast))" (rep $ list [anything, anything, anything] *> pure ()) x @?= Right [()] , testCase "Many three-element lists of whatever (0)" $ do x <- syntaxTest "()" (rep $ list [anything, anything, anything] *> pure ()) x @?= Right [] , testCase "Many three-element lists of whatever (4)" $ do x <- syntaxTest "((programming is fun) (a b c) (x y z) (hello (more stuff) fits))" (rep $ list [anything, anything, anything] *> pure ()) x @?= Right [(), (), (), ()] , testCase "Many three-element lists of whatever failing on third sublist" $ do x <- syntaxTest "((programming is fun) (a b c) (x y) (hello (more stuff) fits))" (rep $ list [anything, anything, anything] *> pure ()) x @?= Left (SyntaxError $ pure $ Reason { expr = Syntax (Posd (fakeFilePos 1 31) (List [ Syntax (Posd (fakeFilePos 1 32) (Atom (TrivialAtom "x"))) , Syntax (Posd (fakeFilePos 1 34) (Atom (TrivialAtom "y")))])) , message = "3 expressions" }) , testCase "Realistic example 1" $ do x <- syntaxTest "(lambda (x y z) y)" lambda x @?= Right (Lam ["x", "y", "z"] (Datum (Atom "y"))) , testCase "Realistic example 2" $ do x <- syntaxTest "(lambda (x y (z)) y)" lambda x @?= Left (SyntaxError $ pure $ Reason { expr = Syntax (Posd (fakeFilePos 1 14) (List [Syntax {unSyntax = Posd {pos = fakeFilePos 1 15, pos_val = Atom (TrivialAtom "z")}}])) , message = "an atom" }) , testCase "Realistic example 3" $ do x <- syntaxTest "(lambda x x)" lambda x @?= Left (SyntaxError $ pure $ Reason { expr = Syntax (Posd (fakeFilePos 1 9) (Atom "x")) , message = "sequence of variable bindings" }) , testCase "Realistic example 4" $ do x <- syntaxTest "(lambda (x y x) y)" lambda x @?= Left (SyntaxError $ pure $ Reason { expr = Syntax (Posd (fakeFilePos 1 9) (List [ Syntax {unSyntax = Posd {pos = fakeFilePos 1 10, pos_val = Atom (TrivialAtom "x")}} , Syntax {unSyntax = Posd {pos = fakeFilePos 1 12, pos_val = Atom (TrivialAtom "y")}} , Syntax {unSyntax = Posd {pos = fakeFilePos 1 14, pos_val = Atom (TrivialAtom "x")}} ])) , message = "sequence of distinct variable bindings" }) ] fakeFile :: Text fakeFile = "test input" fakeFilePos :: Int -> Int -> Position fakeFilePos = SourcePos fakeFile syntaxTest :: Text -> SyntaxParse TrivialAtom a -> IO (Either (SyntaxError TrivialAtom) a) syntaxTest txt p = case MP.parse (skipWhitespace *> sexp (TrivialAtom <$> identifier) <* MP.eof) (T.unpack fakeFile) txt of Left err -> error $ "Reader error: " ++ MP.errorBundlePretty err Right sexpr -> syntaxParseIO p sexpr