content: {-# 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
  
  