{-# LANGUAGE DeriveDataTypeable #-}

module Main where

import Language.Boogie.AST
import Language.Boogie.Util
import Language.Boogie.Position
import qualified Language.Boogie.Parser as Parser (program)
import Language.Boogie.TypeChecker
import Language.Boogie.PrettyPrinter
import Language.Boogie.Interpreter
import Language.Boogie.Tester
import System.Environment
import System.Console.CmdArgs
import System.Random
import Data.Time.Calendar
import Data.List
import Data.Map (Map, (!))
import qualified Data.Map as M
import Control.Monad.State
import Control.Applicative
import Text.PrettyPrint hiding (mode)
import Text.ParserCombinators.Parsec (parse, parseFromFile)

programName = "boogaloo"
versionName = "0.1"
releaseDate = fromGregorian 2012 10 25

-- | Execute or test a Boogie program, according to command-line arguments
main = do
  res <- cmdArgsRun $ mode
  case res of
    Exec file entry -> executeFromFile file entry
    args -> testFromFile (file args) (proc_ args) (testMethod args) (verbose args)

{- Command line arguments -}

data CommandLineArgs
    = Exec { file :: String, entry :: String }
    | Test { file :: String, proc_ :: [String], limits :: (Integer, Integer), dlimits :: (Integer, Integer), verbose :: Bool  }
    | RTest { file :: String, proc_ :: [String], limits :: (Integer, Integer), dlimits :: (Integer, Integer), tc_count :: Int, seed :: Maybe Int, verbose :: Bool }
      deriving (Data, Typeable, Show, Eq)

execute = Exec {
  entry = "Main"  &= help "Program entry point (must not have in- or out-parameters)" &= typ "PROCEDURE",
  file  = ""      &= typFile &= argPos 0
  } &= auto &= help "Execute program"
      
test_ = Test {
  proc_   = []      &= help "Procedures to test" &= typ "PROCEDURE",
  limits  = (-3, 3) &= help "Interval of input values to try for an integer variable" &= typ "NUM, NUM",
  dlimits = (0, 2)  &= help dlimitsMsg &= typ "NUM, NUM" ,
  file    = ""      &= typFile &= argPos 0,
  verbose = False   &= help verboseMsg
  } &= help "Test program exhaustively"
  
rtest = RTest {
  proc_     = []        &= help "Procedures to test" &= typ "PROCEDURE",
  limits    = (-32, 32) &= help "Interval of input values to draw from for an integer variable" &= typ "NUM, NUM",
  dlimits   = (0, 2)    &= help dlimitsMsg &= typ "NUM, NUM",
  tc_count  = 10        &= help "Number of test cases to generate per procedure implementation" &= name "n" &= typ "NUM",
  seed      = Nothing   &= help "Seed for the random number generator" &= typ "NUM",
  file      = ""        &= typFile &= argPos 0,
  verbose = False       &= help verboseMsg
  } &= help "Test program on random inputs"
  
dlimitsMsg = "Given a map with an integer domain, different range values will be tried for domain values in this interval"
verboseMsg = "Output all executed test cases"
    
mode = cmdArgsMode $ modes [execute, test_, rtest] &= 
  help "Boogie interpreter" &= 
  program programName &= 
  summary (programName ++ " v" ++ versionName ++ ", " ++ showGregorian releaseDate)
  
-- | Set up a test method depending on command-line arguments  
testMethod :: CommandLineArgs -> Program -> Context -> [Id] -> IO [TestCase]
testMethod (Test _ _ limits dlimits _ ) program context procNames = 
  let settings = ExhaustiveSettings {
      esIntRange = interval limits,
      esIntMapDomainRange = interval dlimits,
      esGenericTypeRange = defaultGenericTypeRange context,
      esMapTypeRange = defaultMapTypeRange context
    }
  in return $ testProgram settings program context procNames
testMethod (RTest _ _ limits dlimits tc_count seed _) program context procNames = do
  defaultGen <- getStdGen
  randomGen <- case seed of
    Nothing -> getStdGen
    Just s -> return $ mkStdGen s
  let settings = RandomSettings {
      rsRandomGen = randomGen,
      rsCount = tc_count,
      rsIntLimits = limits,
      rsIntMapDomainRange = interval dlimits,
      rsGenericTypeRange = defaultGenericTypeRange context,
      rsMapTypeRange = defaultMapTypeRange context     
    }  
  return $ testProgram settings program context procNames
    
{- Interfacing internal modules -}

-- | Execute procedure entryPoint from file
-- | and output either errors or the final values of global variables
executeFromFile :: String -> String -> IO ()
executeFromFile file entryPoint = runOnFile printFinalState file
  where
    printFinalState p context = case M.lookup entryPoint (ctxProcedures context) of
      Nothing -> print (text "Cannot find program entry point" <+> text entryPoint)
      Just sig -> if not (goodEntryPoint sig)
        then print (text "Program entry point" <+> text entryPoint <+> text "does not have the required signature" <+> doubleQuotes (sigDoc [] []))
        else case executeProgram p context entryPoint of
          Left err -> print err
          Right env -> (print . varsDoc . envGlobals) env
    goodEntryPoint sig = null (psigTypeVars sig) && null (psigArgTypes sig) && null (psigRetTypes sig)

-- | Test procedures procNames from file with a testMethod
-- | and output the test outcomes
testFromFile :: String -> [String] -> (Program -> Context -> [String] -> IO [TestCase]) -> Bool -> IO ()
testFromFile file procNames testMethod printAll = runOnFile printTestOutcomes file
  where
    printTestOutcomes p context = do
      let (present, missing) = partition (`M.member` ctxProcedures context) procNames
      when (not (null missing)) $ print (text "Cannot find procedures under test:" <+> commaSep (map text missing))
      testResults <- testMethod p context present
      print $ testSessionSummary testResults
      when printAll $ putStr "\n" >> mapM_ print testResults

-- | Parse file, type-check the resulting program, then execute command on the resulting program and type context
runOnFile :: (Program -> Context -> IO ()) -> String -> IO ()      
runOnFile command file = do 
  parseResult <- parseFromFile Parser.program file
  case parseResult of
    Left parseErr -> print parseErr
    Right p -> case checkProgram p of
      Left typeErrs -> print (typeErrorsDoc typeErrs)
      Right context -> command p context
      
{- Helpers for testing internal functions -}      
      
-- | Harness for testing various internal functions
harness file = runOnFile printOutcome file
  where
    printOutcome p context = do
      let env = execState (collectDefinitions p) emptyEnv { envTypeContext = context }
      print $ envGlobals env
      
-- | Test that print . parse == print . parse . print .parse      
testParser :: String -> IO ()      
testParser file = do
  result <- parseFromFile Parser.program file
  case (result) of
    Left err -> print err
    Right p -> do
      case parse Parser.program ('*' : file) (show p) of
        Left err -> print err
        Right p' -> if p == p'
          then putStr ("Passed.\n")
          else putStr ("Failed with different ASTs.\n")