-------------------------------------------------------------------------
--- A tool to verify Curry programs w.r.t. failing computations.
--- Thus, a program successfully verified by this tool should never
--- fail at run-time (apart from explicit error) provided that
--- the call types are satisfied when invoking a function.
---
--- @author Michael Hanus
--- @version October 2024
-------------------------------------------------------------------------

module Main where

import Control.Monad               ( unless, when )
import Curry.Compiler.Distribution ( curryCompiler )
import Data.Char                   ( toLower )
import Data.IORef
import Data.List
import Data.Maybe                  ( isNothing )
import System.Environment          ( getArgs )
import System.IO                   ( hFlush, stdout )

import Debug.Trace ( trace )

-- Imports from dependencies:
import Analysis.Types             ( Analysis, analysisName, startValue )
import Analysis.TermDomain
import Analysis.Values
import Control.Monad.Trans.Class  ( lift )
import Control.Monad.Trans.State  ( StateT, get, put, execStateT )
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Time                  ( ClockTime )
import Debug.Profile
import FlatCurry.AddTypes         ( applyTSubst, splitArgTypes )
import FlatCurry.Goodies
import FlatCurry.Names
import FlatCurry.NormalizeLet
import FlatCurry.Print
import FlatCurry.Types
import JSON.Data
import JSON.Pretty                ( ppJSON )
import System.CurryPath           ( runModuleAction )
import System.Directory           ( createDirectoryIfMissing, doesFileExist
                                  , removeDirectory )
import System.FilePath            ( (</>) )
import System.Path                ( fileInPath )
import System.Process             ( exitWith )
import XML

-- Imports from package modules:
import FlatCurry.Build
import FlatCurry.Simplify         ( simpExpr )
import Verify.CallTypes
import Verify.Files
import Verify.Helpers
import Verify.IOTypes
import Verify.NonFailConditions
import Verify.Options
import Verify.ProgInfo
import Verify.Statistics
import Verify.WithSMT

------------------------------------------------------------------------------
banner :: String
banner = unlines [bannerLine, bannerText, bannerLine]
 where
  bannerText = "Curry Non-Failure Verifier (Version of 24/10/24)"
  bannerLine = take (length bannerText) (repeat '=')

main :: IO ()
main = do
  args <- getArgs
  (opts0,progs) <- processOptions banner args
  -- set analysis to top values if unspecified
  let opts = if null (optDomainID opts0)
               then opts0 { optDomainID = analysisName resultValueAnalysisTop }
               else opts0
  when (optDeleteCache opts0) $ deleteVerifyCacheDirectory opts0
  case progs of
    [] -> unless (optDeleteCache opts0) $ do
            putStrLn "Module name missing!"
            putStrLn "Try option '--help' for usage information."
            exitWith 1
    ms -> do
      if optDomainID opts == analysisName resultValueAnalysisTop
        then runWith resultValueAnalysisTop opts ms
        else
          if optDomainID opts == analysisName resultValueAnalysis2
            then runWith resultValueAnalysis2 opts ms
            else
              if optDomainID opts == analysisName resultValueAnalysis5
                then runWith resultValueAnalysis5 opts ms
                else error "Unknown analysis domain ID!"
 where
  runWith analysis opts ms = do
    printWhenStatus opts banner
    pistore <- newIORef emptyProgInfo
    astore  <- newIORef (AnaStore [])
    mapM_ (runModuleAction (verifyModuleIfNew analysis pistore astore opts)) ms

--- Verify a single module if necessary, i.e., not previously verified.
verifyModuleIfNew :: TermDomain a => Analysis a -> IORef ProgInfo
                  -> IORef (AnalysisStore a) -> Options -> String -> IO ()
verifyModuleIfNew valueanalysis pistore astore opts0 mname = do
  z3exists <- fileInPath "z3"
  let z3msg = "Option '--nosmt' activated since SMT solver Z3 not found in PATH!"
  opts <- if z3exists || not (optSMT opts0)
            then return opts0
            else do putStrLn z3msg
                    return opts0 { optSMT = False }
  printWhenStatus opts $ "Processing module '" ++ mname ++ "':"
  flatprog <- getFlatProgFor pistore mname
  outdatedtypes <- typeFilesOutdated opts mname
  if outdatedtypes || optRerun opts || not (null (optFunction opts))
    then verifyModule valueanalysis pistore astore opts mname flatprog
    else do
      printWhenStatus opts "Reading call types from previous verification..."
      let fdecls       = progFuncs flatprog
          visfuncs     = filter (\fn -> optGenerated opts || isCurryID fn)
                                (map funcName
                                     (filter ((== Public) . funcVisibility)
                                             fdecls))
          visfuncset   = Set.fromList visfuncs
          isVisible qf = Set.member qf visfuncset
      (ctypes,nfconds) <- readCallCondTypes opts mname
      const (printVerifyResults opts mname isVisible fdecls ctypes nfconds)
            -- Hack: this unused expression is necessary to convince the type
            -- checker that both expressions are parametric over the same
            -- type variable `a`:
            (snd (head ctypes) == Just [startValue valueanalysis])
      return ()

--- Verify a single module.
verifyModule :: TermDomain a => Analysis a -> IORef ProgInfo
             -> IORef (AnalysisStore a) -> Options -> String -> Prog -> IO ()
verifyModule valueanalysis pistore astore opts mname flatprog = do
  let orgfdecls    = progFuncs flatprog
      numfdecls    = length orgfdecls
      visfuncs     = filter (\fn -> optGenerated opts || isCurryID fn)
                            (map funcName (filter ((== Public) . funcVisibility)
                                          orgfdecls))
      numvisfuncs  = length visfuncs
      visfuncset   = Set.fromList visfuncs
      isVisible qf = Set.member qf visfuncset
  imps@(impconsinfos,impacalltypes,impnftypes,impiotypes) <-
    if optImports opts
      then do
        whenStatus opts $ putStr $ "Reading abstract types of imports: " ++
          unwords (progImports flatprog)
        -- use quiet mode for imports when showing only verification results:
        let impopts = if optVerb opts == 1 then opts { optVerb = 0 } else opts
        readTypesOfModules impopts
                           (verifyModuleIfNew valueanalysis pistore astore)
                           (progImports flatprog)
      else return ([],[],[],[])
  if optTime opts then do whenStatus opts $ putStr "..."
                          (id $## imps) `seq` printWhenStatus opts "done"
                  else printWhenStatus opts ""
  let modconsinfos = consInfoOfTypeDecls (progTypes flatprog)
      consinfos = modconsinfos ++ impconsinfos
      -- verify function declarations with completed branches:
      fdecls  = map (completeBranchesInFunc consinfos False) orgfdecls
      funusage = funcDecls2Usage mname fdecls
  mtime <- getModuleModTime mname
  -- infer initial abstract call types:
  mboldacalltypes <- readCallTypeFile opts mtime mname
  (acalltypes, numntacalltypes, numpubacalltypes) <- id $!!
    inferCallTypes opts consinfos isVisible mname mtime flatprog mboldacalltypes
  -- infer in/out types:
  (iotypes, numntiotypes, numpubntiotypes) <- id $!!
    inferIOTypes opts valueanalysis astore isVisible flatprog
  -- read previously inferred non-fail conditions:
  mbnfconds <- readNonFailCondFile opts mtime mname

  vstate <- initVerifyState pistore flatprog consinfos
                            (Map.fromList impacalltypes)
                            (Map.fromList impnftypes)
                            (Map.fromList acalltypes)
                            (Map.fromList (iotypes ++ impiotypes))
                            (maybe [] id mbnfconds) opts
  enforceNormalForm opts "VERIFYSTATE" vstate
  printWhenAll opts $ unlines $
    ("Function usage in module '" ++ mname ++ "':") :
    map (\ (qf, qfs) -> snd qf ++ ": used in " ++
                        unwords (map (snd . funcName) qfs))
        (Map.toList funusage)
  let withverify = optVerify opts &&
                   (null (optFunction opts) ||
                    isNothing mbnfconds || isNothing mboldacalltypes)
  (vnumits, vtime, vst) <-
   if withverify
     then do
       printWhenStatus opts $ "Start verification of '" ++ mname ++ "' (" ++
         show numfdecls ++ " functions):"
       pi1 <- getProcessInfos
       (numits,st) <- tryVerifyProg opts 0 vstate mname funusage fdecls
       pi2 <- getProcessInfos
       printVerifyResult opts st mname isVisible
       let tdiff = maybe 0 id (lookup ElapsedTime pi2) -
                   maybe 0 id (lookup ElapsedTime pi1)
       when (optTime opts && optVerb opts > 0) $ putStrLn $
         "TOTAL VERIFICATION TIME: " ++ show tdiff ++ " msec"
       return (numits, tdiff, st)
     else return (0, 0, vstate)
  -- print statistics:
  let finalacalltypes   = Map.toList (vstCallTypes vst)
      finalntacalltypes = filter (not . isTotalACallType . snd) finalacalltypes
      (stattxt,statcsv) = showStatistics opts vtime vnumits isVisible
                            numvisfuncs numfdecls
                            (numpubntiotypes, numntiotypes)
                            (numpubacalltypes, numntacalltypes)
                            finalntacalltypes
                            (map fst (vstFunConds vst)) (vstStats vst)
  when (optStats opts) $ putStr stattxt
  when withverify $ do
    storeTypes opts mname fdecls modconsinfos finalacalltypes
      (filter (isVisible .fst) finalntacalltypes) (vstFunConds vst) iotypes
    storeStatistics opts mname stattxt statcsv
    when (optStoreFuncs opts) $ do
      let nfname = mname ++ ".NONFAIL"
          flname = mname ++ ".FAIL"
          totalfuncs = filter (isTotalACallType . snd) finalacalltypes
      writeFile nfname
        (unlines (map (\((mn,fn),_) -> mn ++ " " ++ fn) totalfuncs))
      printWhenStatus opts $
        "Non-failing functions stored in '" ++ nfname ++ "'."
      writeFile flname
        (unlines (map (\((mn,fn),_) -> mn ++ " " ++ fn) finalntacalltypes))
      printWhenStatus opts $
        "Possibly failing functions stored in '" ++ flname ++ "'."
  unless (null (optFunction opts)) $ showFunctionInfo opts mname vst
  when (vstError vst) $ exitWith 1

--- Infer the initial (abstract) call types of all functions in a program and
--- return them together with the number of all/public non-trivial call types.
--- The last argument are the already stored old call types, if they are
--- up to date.
inferCallTypes :: TermDomain a => Options -> [(QName,ConsInfo)]
               -> (QName -> Bool)
               -> String -> ClockTime -> Prog -> Maybe [(QName,ACallType a)]
               -> IO ([(QName, ACallType a)], Int, Int)
inferCallTypes opts consinfos isVisible mname mtime flatprog
               mboldacalltypes = do
  oldpubcalltypes <- readPublicCallTypeModule opts consinfos mtime mname
  let fdecls       = progFuncs flatprog
  let calltypes    = unionBy (\x y -> fst x == fst y) oldpubcalltypes
                             (map (callTypeFunc opts consinfos) fdecls)
      ntcalltypes  = filter (not . isTotalCallType . snd) calltypes
      pubcalltypes = filter (isVisible . fst) ntcalltypes
  if optVerb opts > 2
    then putStrLn $ unlines $ "CONCRETE CALL TYPES OF ALL OPERATIONS:" :
           showFunResults prettyFunCallTypes calltypes
    else when (optVerb opts > 2 || optCallTypes opts) $
      putStrLn $ unlines $
        ("NON-TRIVIAL CONCRETE CALL TYPES OF " ++
         (if optPublic opts then "PUBLIC" else "ALL") ++ " OPERATIONS:") :
        showFunResults prettyFunCallTypes
         (sortFunResults (if optPublic opts then pubcalltypes else ntcalltypes))

  let pubmodacalltypes = map (funcCallType2AType consinfos) oldpubcalltypes
      acalltypes = unionBy (\x y -> fst x == fst y) pubmodacalltypes
                           (maybe (map (funcCallType2AType consinfos) calltypes)
                                  id
                                  mboldacalltypes)
      ntacalltypes  = filter (not . isTotalACallType . snd) acalltypes
      pubacalltypes = filter (isVisible . fst) ntacalltypes
  if optVerb opts > 2
    then putStrLn $ unlines $ "ABSTRACT CALL TYPES OF ALL OPERATIONS:" :
           showFunResults prettyFunCallAType acalltypes
    else when (optVerb opts > 2 || optCallTypes opts) $
      putStrLn $ unlines $
        ("NON-TRIVIAL ABSTRACT CALL TYPES OF " ++
         (if optPublic opts then "PUBLIC" else "ALL") ++ " OPERATIONS:") :
        showFunResults prettyFunCallAType
          (sortFunResults $ if optPublic opts then pubacalltypes
                                              else ntacalltypes)
  return (acalltypes, length ntacalltypes, length pubacalltypes)

--- Infer the in/out types of all functions in a program and return them
--- together with the number of all and public non-trivial in/out types.
inferIOTypes :: TermDomain a => Options -> Analysis a -> IORef (AnalysisStore a)
             -> (QName -> Bool) -> Prog
             -> IO ([(QName, InOutType a)], Int, Int)
inferIOTypes opts valueanalysis astore isVisible flatprog = do
  rvmap <- loadAnalysisWithImports astore valueanalysis opts flatprog
  let iotypes      = map (inOutATypeFunc rvmap) (progFuncs flatprog)
      ntiotypes    = filter (not . isAnyIOType . snd) iotypes
      pubntiotypes = filter (isVisible . fst) ntiotypes
  if optVerb opts > 2
    then putStrLn $ unlines $ "INPUT/OUTPUT TYPES OF ALL OPERATIONS:" :
           showFunResults showIOT iotypes
    else when (optVerb opts > 2 || optIOTypes opts) $
      putStrLn $ unlines $
        ("NON-TRIVIAL INPUT/OUTPUT TYPES OF " ++
         (if optPublic opts then "PUBLIC" else "ALL") ++ " OPERATIONS:") :
        showFunResults showIOT
          (sortFunResults (if optPublic opts then pubntiotypes else ntiotypes))
  return (iotypes, length ntiotypes, length pubntiotypes)

-- Shows the call and in/out type of a given function defined in the module.
showFunctionInfo :: TermDomain a => Options -> String -> VerifyState a -> IO ()
showFunctionInfo opts mname vst = do
  let f = optFunction opts
      qf = (mname, f)
  fdecls <- currentFuncDecls vst
  if qf `notElem` map funcName fdecls
    then putStrLn $ "Function '" ++ snd qf ++ "' not defined!"
    else do
      let iot   = maybe (trivialInOutType 0) id (Map.lookup qf (vstIOTypes vst))
          ctype = maybe (Just [anyType]) id (Map.lookup qf (vstCallTypes vst))
      putStrLn $ "Function '" ++ f ++ "':"
      putStrLn $ "In/out type: " ++ showIOT iot
      putStrLn $ "Call type  : " ++ prettyFunCallAType ctype
      maybe (return ())
            (\nfc -> putStrLn $ showConditions fdecls [(qf,nfc)])
            (lookup qf (vstFunConds vst))

-- Try to verify a module, possibly in several iterations.
-- The second argument is the number of already performed iterations,
-- the first component of the result is the total number of iterations.
tryVerifyProg :: TermDomain a => Options -> Int -> VerifyState a -> String
              -> Map.Map QName [FuncDecl] -> [FuncDecl]
              -> IO (Int,VerifyState a)
tryVerifyProg opts numits vstate mname funusage fdecls = do
  st <- execStateT (mapM_ verifyFunc fdecls) vstate
  -- remove NewFailed information about unchanged operations
  -- (usually, these are failed operations with changed conditions)
  let newfailures = filter (\(qf,ct) -> maybe True (\fct -> ct /= fct)
                                          (Map.lookup qf (vstCallTypes st)))
                           (vstNewFailed st)
  unless (null newfailures || optVerb opts < 2) $ printFailures st
  unless (null newfailures) $ printWhenStatus opts $ unlines $
    "Operations with refined call types (used in future analyses):" :
    showFunResults prettyFunCallAType (reverse newfailures)
  let newcts = Map.union (Map.fromList newfailures) (vstCallTypes st)
  enforceNormalForm opts "NEWCALLTYPES" newcts
  let (failconds,refineconds) =
         partition (\(qf,_) -> qf `elem` (map fst (vstFunConds st)))
                   (vstNewFunConds st)
      newfailconds = filter (\(qf,_) -> (qf,nfcFalse) `notElem` vstFunConds st)
                            failconds
      -- Condition for next iteration: set already existing conditions to
      -- `False` to avoid infinite refinements
      nextfunconds = (unionBy (\x y -> fst x == fst y)
                              (map (\(qf,_) -> (qf, nfcFalse)) newfailconds)
                              (vstFunConds st)) ++ refineconds
      newrefineconds = newfailconds ++ refineconds
  --fdecls <- currentFuncDecls st
  unless (null newrefineconds) $ printWhenStatus opts $
    "Operations with refined call conditions (used in future analyses):\n" ++
    showConditions fdecls newrefineconds
  let st' = st { vstCallTypes = newcts, vstNewFailed = []
               , vstFunConds = nextfunconds, vstNewFunConds = [] }
  if null newfailures && null newrefineconds
    then do printFailures st'
            -- remove always failing conditions (since the call types are
            -- always failing for such functions):
            let st'' = st' { vstFunConds =
                               filter ((/= nfcFalse) . snd) nextfunconds }
            return (numits + 1, st'')
    else do
      let -- functions with refined call types:
          rfuns = map fst (filter (not . isFailACallType . snd) newfailures)
          newfdecls =
            foldr unionFDecls
              (filter (\fd -> funcName fd `elem` rfuns) fdecls)
              (map (\qf -> maybe [] id (Map.lookup qf funusage))
                   (union (map fst newfailures) (map fst newrefineconds)))
      printWhenStatus opts $ "Repeat verification with new call types..." ++
        "(" ++ show (length newfdecls) ++ " functions)"
      --putStrLn $ unlines $
      --  showFunResults prettyFunCallAType (sortFunResults $ vstCallTypes st')
      tryVerifyProg opts (numits + 1) st' mname funusage newfdecls
 where
  failLine = take 78 (repeat '!')
  failComment = failLine ++ "\nPROGRAM CONTAINS POSSIBLY FAILING "

  printFailures st = whenStatus opts $ do
    unless (null (vstFailedFuncs st)) $
      putStrLn $ failComment ++ "FUNCTION CALLS:\n" ++
         unlines (map (\ (qf,_,e) -> "Function '" ++ snd qf ++
                                     "': call '" ++ showExp e ++ "'")
                      (reverse (vstFailedFuncs st)) ++ [failLine])
    unless (null (vstPartialBranches st)) $
      putStrLn $ failComment ++ "FUNCTIONS:\n" ++
         unlines
           (map (\ (qf,_,e,cs) -> showIncompleteBranch qf e cs)
                (reverse (vstPartialBranches st)) ++ [failLine])

--- Prints a message about the result of the module verification.
printVerifyResult :: TermDomain a => Options -> VerifyState a -> String
                  -> (QName -> Bool) -> IO ()
printVerifyResult opts vst mname isvisible = do
  fdecls <- currentFuncDecls vst
  printVerifyResults opts mname isvisible fdecls
                     (Map.toList (vstCallTypes vst)) (vstFunConds vst)

------------------------------------------------------------------------------
-- Print the verification results in the required format.
printVerifyResults :: TermDomain a => Options -> String -> (QName -> Bool)
                   -> [FuncDecl] -> [(QName,ACallType a)]
                   -> [(QName,NonFailCond)] -> IO ()
printVerifyResults opts mname isvisible fdecls ctypes nfconds
  | optVerb opts == 0
  = return ()
  | optFormat opts == FormatJSON
  = putStrLn $ ppJSON $ JArray $
      map callAType2JSON (sortFunResults (filter (showFun . fst) ctypes))
  | optFormat opts == FormatXML
  = putStrLn $ showXmlDoc $ xml "results" $
      map callAType2XML (sortFunResults (filter (showFun . fst) ctypes))
  | otherwise
  = do
    putStr $ "MODULE '" ++ mname ++ "' VERIFIED"
    let calltypes = filter (\(qf,ct) -> not (isTotalACallType ct) && showFun qf)
                           ctypes
        funconds = filter (showFun . fst) nfconds
    if null calltypes
      then putStrLn "\n"
      else putStrLn $ unlines $ " W.R.T. NON-TRIVIAL ABSTRACT CALL TYPES:"
             : showFunResults prettyFunCallAType
                 (sortFunResults (filter ((`notElem` (map fst funconds)) . fst)
                                         calltypes))
    unless (null funconds) $
      putStrLn $ "NON-FAIL CONDITIONS FOR OTHERWISE FAILING FUNCTIONS:\n" ++
                 showConditions fdecls (sortFunResults funconds)
 where
  showFun qf = not (optPublic opts) || isvisible qf

  callAType2JSON (qf@(mn,fn),fct) =
    JObject [("module", JString mn),
             ("name"  , JString fn),
             ("result", JString (showCallATypeOrNonFailCond qf fct))]

  callAType2XML (qf@(mn,fn),fct) =
    xml "operation" [xml "module" [xtxt mn],
                     xml "name"   [xtxt fn],
                     xml "result" [xtxt (showCallATypeOrNonFailCond qf fct)]]

  showCallATypeOrNonFailCond qf ct =
    maybe
      (showCallAType ct)
      (\nfc -> showFuncDeclAsLambda (snd (genNonFailFunction fdecls (qf,nfc))))
      (lookup qf nfconds)

  showCallAType ct | isTotalACallType ct = "FAIL-FREE"
                   | isFailACallType ct  = "FAILING"
                   | otherwise           = prettyFunCallAType ct

-- Shows a message about an incomplete branch.
-- If the third argument is the empty list, it is a literal branch.
showIncompleteBranch :: QName -> Expr -> [QName] -> String
showIncompleteBranch qf e cs@(_:_) =
  "Function '" ++ snd qf ++ "': constructor" ++
  (if length cs > 1 then "s" else "") ++ " '" ++
  unwords (map snd cs) ++ "' " ++
  (if length cs > 1 then "are" else "is") ++ " not covered in:\n" ++
  showExp e
showIncompleteBranch qf e [] =
  "Function '" ++ snd qf ++ "': the case on literals might be incomplete:\n" ++
  showExp e

------------------------------------------------------------------------------
-- The state of the transformation process contains
-- * the list of all function declarations of the current module
-- * the current function to be analyzed (name, arity, rule arguments)
-- * a list of all constructors grouped by types
-- * a fresh variable index
-- * a list of all variables and their bound expressions
-- * a list of all variables and their input/output types
-- * the call condition of the current branch expressed as a (Boolean) FlatCurry
--   expression which contains a "hole" to extend it with further conjunctions
-- * the call types of all imported operations
-- * the call types of operations of the current module
-- * the input/output types of all operations
-- * the list of failed function calls
-- * the list of incomplete case expressions
-- * the list of functions marked as failing in this iteration
-- * some statistics
-- * the tool options
-- * a Boolean flag which is `True` if some error occurred
-- It is parameterized over the abstract term domain.
data VerifyState a = VerifyState
  { vstModules     :: IORef ProgInfo    -- all infos about loaded modules
  , vstCurrModule  :: String            -- name of the current module
  , vstCurrFunc    :: (QName,Int,[Int]) -- name/arity/args of current function
  , vstConsInfos   :: [(QName,ConsInfo)]-- infos about all constructors
  , vstFreshVar    :: Int               -- fresh variable index in a rule
  , vstVarExp      :: [(Int,TypeExpr,Expr)] -- map variable to its type and
                                            -- subexpression
  , vstVarTypes    :: VarTypesMap a     -- map variable to its abstract types
  , vstCondition   :: Expr -> Expr      -- current branch condition (with hole)
  , vstImpCallTypes:: Map.Map QName (ACallType a) -- call types of imports
  , vstCallTypes   :: Map.Map QName (ACallType a) -- call types of module
  , vstIOTypes     :: Map.Map QName (InOutType a) -- in/out type for all funcs
  , vstFailedFuncs :: [(QName,Int,Expr)]   -- functions with illegal calls
  , vstPartialBranches :: [(QName,Int,Expr,[QName])] -- incomplete branches
  , vstNewFailed   :: [(QName,ACallType a)] -- new failed function call types
  , vstImpFunConds :: Map.Map QName NonFailCond -- call conditions of imports
  , vstFunConds    :: [(QName,NonFailCond)] -- call conditions of functions
  , vstNewFunConds :: [(QName,NonFailCond)] -- functions with new call conds
  , vstStats       :: (Int,Int,Int)         -- number of: non-trivial calls /
                                            -- incomplete cases /
                                            -- SMT-checked non-trivial calls
  , vstToolOpts    :: Options
  , vstError       :: Bool
  }

--- Initializes the verification state.
initVerifyState :: TermDomain a => IORef ProgInfo -> Prog -> [(QName,ConsInfo)]
                -> Map.Map QName (ACallType a) -> Map.Map QName NonFailCond
                -> Map.Map QName (ACallType a)
                -> Map.Map QName (InOutType a)
                -> [(QName,NonFailCond)] -> Options
                -> IO (VerifyState a)
initVerifyState pistore flatprog consinfos impacalltypes impfconds acalltypes
                iotypes nfconds opts = do
  unless (null nonfailconds) $ printWhenDetails opts $
    "INITIAL NON-FAIL CONDITIONS:\n" ++
    showConditions (progFuncs flatprog) nonfailconds
  return $ VerifyState pistore (progName flatprog) (("",""),0,[]) consinfos 0
                       [] [] id impacalltypes nfacalltypes iotypes [] [] []
                       impfconds nonfailconds [] (0,0,0) opts False
 where
  nonfailconds = unionBy (\x y -> fst x == fst y) nfconds
                         (nonFailCondsOfModule flatprog)

  -- set the call types of operations with non-fail conditions to "failed"
  nfacalltypes = Map.insertList
                   (map (\(qf,_) -> (qf, failACallType)) nonfailconds)
                   acalltypes

-- The type of the state monad contains the verification state.
type VerifyStateM atype a = StateT (VerifyState atype) IO a

-- Sets the name and arity of the current function in the state.
setToolError :: TermDomain a => VerifyStateM a ()
setToolError = do
  st <- get
  put $ st { vstError = True }

-- Gets the function declarations of the current module.
currentFuncDecls :: TermDomain a => VerifyState a -> IO [FuncDecl]
currentFuncDecls st = do
   prog <- getFlatProgFor (vstModules st) (vstCurrModule st)
   return $ progFuncs prog

-- Sets the name and arity of the current function in the state.
setCurrentFunc :: TermDomain a => QName -> Int -> [Int] -> VerifyStateM a ()
setCurrentFunc qf ar vs = do
  st <- get
  put $ st { vstCurrFunc = (qf,ar,vs) }

-- Gets the name of the current function in the state.
getCurrentFuncName :: TermDomain a => VerifyStateM a QName
getCurrentFuncName = do
  st <- get
  return $ let (qf,_,_) = vstCurrFunc st in qf

-- Gets information about all constructors.
getConsInfos :: TermDomain a => VerifyStateM a [(QName,ConsInfo)]
getConsInfos = get >>= return . vstConsInfos

-- Sets the fresh variable index in the state.
setFreshVarIndex :: TermDomain a => Int -> VerifyStateM a ()
setFreshVarIndex fvi = do
  st <- get
  put $ st { vstFreshVar = fvi }

-- Gets a new fresh variable index.
newFreshVarIndex :: TermDomain a => VerifyStateM a Int
newFreshVarIndex = do
  v <- fmap vstFreshVar get
  setFreshVarIndex (v + 1)
  return v

-- Adds a new (more restricted) inferred call type for a function
-- which will be used in the next iteration. If there is already
-- a more restricted call type, they will be joined.
addCallTypeRestriction :: TermDomain a => QName -> ACallType a -> VerifyStateM a ()
addCallTypeRestriction qf ctype = do
  st <- get
  maybe (put $ st { vstNewFailed = (qf,ctype) : (vstNewFailed st) } )
        (\ct -> do
           let newct = joinACallType ct ctype
           put $ st { vstNewFailed = unionBy (\x y -> fst x == fst y)
                                             [(qf,newct)] (vstNewFailed st) })
        (lookup qf (vstNewFailed st))

-- Adds a new condition (provided as the second argument as a FlatCurry
-- expression) to the call condition for the current function (first argument)
-- so that it will be used in the next iteration.
-- If there is already a new refined call condition, they will be combined.
-- If the condition is `True`, i.e., the call condition cannot be refined,
-- then the current branch condition will be negated and added
-- so that the current branch is not reachable.
-- Furthermore, the call type of the current function is set to
-- always failing.
addConditionRestriction :: TermDomain a => QName -> Expr -> VerifyStateM a ()
addConditionRestriction qf cond = do
  st <- get
  when (optSMT (vstToolOpts st)) $ do
    let (_,_,vs) = vstCurrFunc st
    oldcalltype <- getCallType qf 0
    let totaloldct = isTotalACallType oldcalltype
        -- express oldcalltype as a condition to be added to `cond`:
        oldcalltypecond = aCallType2Bool (vstConsInfos st) vs oldcalltype
    branchcond <- getExpandedCondition
    newbranchcond <- getExpandedConditionWithConj cond
    let newcond = fcAnd oldcalltypecond
                    (if cond == fcTrue
                       then fcNot branchcond
                       else -- current branch condition implies new condition:
                            fcOr (fcNot branchcond) newbranchcond)
    printIfVerb 2 $ "New call condition for function '" ++ snd qf ++ "': " ++
                    showSimpExp newcond ++
                 (if totaloldct then "" else " (due to non-trivial call type)")
    printIfVerb 3 $ "Check satisfiability of new call condition..."
    unsat <- isUnsatisfiable newcond
    when unsat $ printIfVerb 2 $ "...is unsatisfiable"
    vartypes <- fmap (map (\(v,t,_) -> (v,t))) getVarExps
    setNewFunCondition qf (if unsat then nfcFalse
                                    else genNonFailCond vartypes newcond)
  addCallTypeRestriction qf failACallType

--- Sets a new non-fail condition for a function.
--- If the function has already a new non-fail condition, they will be combined.
setNewFunCondition :: TermDomain a => QName -> NonFailCond -> VerifyStateM a ()
setNewFunCondition qf newcond = do
  st <- get
  maybe (put $ st { vstNewFunConds = (qf,newcond) : (vstNewFunConds st) } )
        (\prevcond -> do
          let newct = combineNonFailConds prevcond newcond
          put $ st { vstNewFunConds = unionBy (\x y -> fst x == fst y)
                                        [(qf,newct)] (vstNewFunConds st) })
        (lookup qf (vstNewFunConds st))

--- Tries to generate a Boolean condition from an abstract call type,
--- if possible.
aCallType2Bool :: TermDomain a => [(QName,ConsInfo)] -> [Int] -> ACallType a -> Expr
aCallType2Bool _       _  Nothing      = fcFalse
aCallType2Bool consinfos vs (Just argts) =
  if all isAnyType argts
    then fcTrue
    else fcAnds (map act2cond (zip vs argts))
 where
  act2cond (v,at) = fcAnds $
    map (\ct -> if all isAnyType (argTypesOfCons ct (arityOfCons consinfos ct) at)
                  then transTester consinfos ct (Var v)
                  else fcFalse )
        (consOfType at)


-- Adds a failed function call (represented by the FlatCurry expression)
-- to the current function. If the second argument is `Just vts`, then
-- this call is not failed provided that it can be ensured that the
-- variable types `vts` hold. This information is used to refine the
-- call type of the current function, if possible.
-- Similarly, this call is not failed provided that the third argument
-- (a condition represented as a FlatCurry expression) is not failed so that
-- this condition is also used to refine the call condition of the current
-- function.
addFailedFunc :: TermDomain a => Expr -> Maybe [(Int,a)] -> Expr -> VerifyStateM a ()
addFailedFunc exp mbvts cond = do
  st <- get
  let (qf,ar,args) = vstCurrFunc st
  put $ st { vstFailedFuncs = union [(qf,ar,exp)] (vstFailedFuncs st) }
  maybe (addConditionRestriction qf cond)
        (\vts ->
           if any ((`elem` args) . fst) vts
             then do
               oldct <- getCallType qf ar
               let ncts  = map (\v -> maybe anyType id (lookup v vts)) args
                   newct = maybe Nothing
                                 (\oldcts -> Just (map (uncurry joinType)
                                                       (zip oldcts ncts)))
                                 oldct
               if oldct == newct
                 then noRefinementFor qf
                 else do
                   printIfVerb 2 $ "TRY TO REFINE FUNCTION CALL TYPE OF " ++
                                   snd qf ++ " TO: " ++ prettyFunCallAType newct
               addCallTypeRestriction qf newct
             else noRefinementFor qf
        )
        mbvts
 where
  noRefinementFor qf = do
    printIfVerb 2 $ "CANNOT REFINE ABSTRACT CALL TYPE OF FUNCTION " ++ snd qf
    addConditionRestriction qf cond

-- Adds an info about cases with missing branches in the current function.
addMissingCase :: TermDomain a => Expr -> [QName] -> VerifyStateM a ()
addMissingCase exp qcs = do
  st <- get
  let (qf,ar,_) = vstCurrFunc st
  put $
    st { vstPartialBranches = union [(qf,ar,exp,qcs)] (vstPartialBranches st) }
  addCallTypeRestriction qf failACallType

-- Sets the types and expressions for variables.
getVarExps :: TermDomain a => VerifyStateM a [(Int,TypeExpr,Expr)]
getVarExps = fmap vstVarExp get

-- Sets the types and expressions for variables.
setVarExps :: TermDomain a => [(Int,TypeExpr,Expr)] -> VerifyStateM a ()
setVarExps varexps = do
  st <- get
  put $ st { vstVarExp = varexps }

-- Sets the FlatCurry type of a given variable.
-- This is used to specialize numeric types during verification
-- of predefined numeric operations.
setVarExpTypeOf :: TermDomain a => Int -> TypeExpr -> VerifyStateM a ()
setVarExpTypeOf var te = do
  st <- get
  put $ st { vstVarExp = map (\(v,t,e) -> if v==var then (v,te,e) else (v,t,e))
                             (vstVarExp st) }

-- Adds types and expressions for new variables.
addVarExps :: TermDomain a => [(Int,TypeExpr,Expr)] -> VerifyStateM a ()
addVarExps varexps = do
  st <- get
  put $ st { vstVarExp = vstVarExp st ++ varexps }

-- Get all currently stored variable types.
getVarTypes :: TermDomain a => VerifyStateM a (VarTypesMap a)
getVarTypes = fmap vstVarTypes get

-- Gets the currently stored types for a given variable.
getVarTypeOf :: TermDomain a => Int -> VerifyStateM a (VarTypes a)
getVarTypeOf v = do
  st <- get
  return $ maybe [] id (lookup v (vstVarTypes st))

-- Sets all variable types.
setVarTypes :: TermDomain a => VarTypesMap a -> VerifyStateM a ()
setVarTypes vartypes = do
  st <- get
  put $ st { vstVarTypes = vartypes }

-- Adds a new variable type to the current set of variable types.
-- It could be an alternative type for an already existent variable or
-- a type for a new variable.
addVarType :: TermDomain a => Int -> VarTypes a -> VerifyStateM a ()
addVarType v vts = do
  st <- get
  put $ st { vstVarTypes = addVarType2Map v vts (vstVarTypes st) }

-- Adding multiple variable types:
addVarTypes :: TermDomain a => VarTypesMap a -> VerifyStateM a ()
addVarTypes vtsmap = do
  st <- get
  put $ st { vstVarTypes = concVarTypesMap (vstVarTypes st) vtsmap }

-- Adds a new variable `Any` type to the current set of variable types.
addVarAnyType :: TermDomain a => Int -> VerifyStateM a ()
addVarAnyType v = addVarType v (ioVarType anyType)

-- Removes an `Any` type for a given variable from the current
-- set of variable types.
-- Used to remove the initial `Any` types in let bindings.
removeVarAnyType :: TermDomain a => Int -> VerifyStateM a ()
removeVarAnyType v = do
  st <- get
  let vtsmap = vstVarTypes st
      vtsmap' = maybe vtsmap
                      (\vts -> setVarTypeInMap v
                                               (filter (not . isAnyIOType) vts)
                                               vtsmap)
                      (lookup v vtsmap)
  put $ st { vstVarTypes = vtsmap' }
 where
  isAnyIOType (vt,vs) =
    case (vt,vs) of (IOT [([], at)], []) -> isAnyType at
                    _                    -> False

-- Gets current branch condition in internal representation.
getCondition :: TermDomain a => VerifyStateM a (Expr -> Expr)
getCondition = fmap vstCondition get

-- Gets the expanded current branch condition.
getExpandedCondition :: TermDomain a => VerifyStateM a Expr
getExpandedCondition = do
  st <- get
  return $ expandExpr (vstVarExp st) (vstCondition st fcTrue)

-- Gets the expanded current branch condition where a conjunct has been added.
getExpandedConditionWithConj :: TermDomain a => Expr -> VerifyStateM a Expr
getExpandedConditionWithConj conj = do
  st <- get
  return $ expandExpr (vstVarExp st) (vstCondition st conj)

-- Sets the current branch condition in internal representation.
setCondition :: TermDomain a => (Expr -> Expr) -> VerifyStateM a ()
setCondition expf = do
  st <- get
  put $ st { vstCondition = expf }

-- Sets the initial condition for a function call.
setCallCondition :: TermDomain a => Expr -> VerifyStateM a ()
setCallCondition exp = do
  st <- get
  put $ st { vstCondition = fcAnd exp }

-- Adds a conjunct to the current condition.
addConjunct :: TermDomain a => Expr -> VerifyStateM a ()
addConjunct exp = do
  st <- get
  put $ st { vstCondition = \c -> (vstCondition st) (fcAnd exp c) }

-- Adds to the current condition an equality between a variable and
-- a constructor applied to a list of fresh pattern variables.
-- This condition is expressed as a case expression where
-- the hole of the current condition is in the branch for the given
-- constructor and all alternative branches return a `False` value.
addSingleCase :: TermDomain a => Int -> QName -> [Int] -> VerifyStateM a ()
addSingleCase casevar qc branchvars = do
  st <- get
  let siblings    = siblingsOfCons (vstConsInfos st) qc
      catchbranch = if null siblings then []
                                     else [Branch (Pattern anonCons []) fcFalse]
  put $ st { vstCondition =
               \c -> (vstCondition st)
                       (Case Rigid (Var casevar)
                          ([Branch (Pattern qc branchvars) c] ++ catchbranch)) }

-- Adds an equality between a variable and an expression as a conjunct
-- to the current condition.
addEquVarCondition :: TermDomain a => Int -> Expr -> VerifyStateM a ()
addEquVarCondition var exp = do
  let conj = if exp == fcTrue
               then Var var
               else if exp == fcFalse
                      then fcNot (Var var)
                      else Comb FuncCall (pre "==") [Var var, exp]
                           -- note: the Eq class dictioniary is missing...
  addConjunct conj

-- Gets the possible non-fail condition of a given operation.
getNonFailConditionOf :: TermDomain a => QName -> VerifyStateM a (Maybe NonFailCond)
getNonFailConditionOf qf = do
  st <- get
  return $ maybe (Map.lookup qf (vstImpFunConds st))
                 Just
                 (lookup qf (vstFunConds st))

-- Gets the abstract call type of a given operation.
-- The trivial abstract call type is returned for encapsulated search operations.
getCallType :: TermDomain a => QName -> Int -> VerifyStateM a (ACallType a)
getCallType qf ar
  | isEncSearchOp qf || isSetFunOp qf
  = return trivialACallType
  | otherwise
  = do
  st <- get
  return $
    if qf == pre "error" && optError (vstToolOpts st)
      then failACallType
      else maybe (maybe (trace ("Warning: call type of operation " ++
                                show qf ++ " not found!") trivialACallType)
                        id
                        (Map.lookup qf (vstImpCallTypes st)))
                 id
                 (Map.lookup qf (vstCallTypes st))
 where
  trivialACallType = Just $ take ar (repeat anyType)

-- Gets the in/out type for an operation of a given arity.
-- If the operation is not found, returns a general type.
-- The trivial in/out type is returned for encapsulated search operations.
getFuncType :: TermDomain a => QName -> Int -> VerifyStateM a (InOutType a)
getFuncType qf ar
  | isEncSearchOp qf || isSetFunOp qf
  = return $ trivialInOutType ar
  | otherwise
  = do st <- get
       maybe (do lift $ putStrLn $
                   "WARNING: in/out type of '" ++ show qf ++ "' not found!"
                 return $ trivialInOutType ar)
             return
             (Map.lookup qf (vstIOTypes st))

-- Increment number of checks of non-trivial function calls.
incrNonTrivialCall :: TermDomain a => VerifyStateM a ()
incrNonTrivialCall = do
  st <- get
  put $ st { vstStats = (\ (f,c,s) -> (f+1,c,s)) (vstStats st) }

-- Increment number of checks of incomplete case expressions.
incrIncompleteCases :: TermDomain a => VerifyStateM a ()
incrIncompleteCases = do
  st <- get
  put $ st { vstStats = (\ (f,c,s) -> (f,c+1,s)) (vstStats st) }

-- Increment number of checks of unsatisfiability with SMT.
incrUnsatSMT :: TermDomain a => VerifyStateM a ()
incrUnsatSMT = do
  st <- get
  put $ st { vstStats = (\ (f,c,s) -> (f,c,s+1)) (vstStats st) }

-- Gets the tool options from the current state.
getToolOptions :: TermDomain a => VerifyStateM a Options
getToolOptions = get >>= return . vstToolOpts

--- Prints a string with `putStrLn` if the verbosity is at least as the given
--- one.
printIfVerb :: TermDomain a => Int -> String -> VerifyStateM a ()
printIfVerb v s = do
  opts <- getToolOptions
  when (optVerb opts >= v) $ lift $ putStrLn s

------------------------------------------------------------------------------

-- Verify a FlatCurry function declaration.
verifyFunc :: TermDomain a => FuncDecl -> VerifyStateM a ()
verifyFunc (Func qf ar _ ftype rule) = case rule of
  Rule vs exp -> unless noVerify $ do
                   setCurrentFunc qf ar vs
                   verifyFuncRule vs ftype (normalizeLet exp)
  External _  -> return ()
 where
  noVerify = qf `elem` noVerifyFunctions ||
             nonfailSuffix `isSuffixOf` snd qf

-- A list of operations that do not need to be verified.
-- These are operations that are non-failing but this property
-- cannot be ensured by the current tool.
noVerifyFunctions :: [QName]
noVerifyFunctions =
  [ pre "aValueChar" -- is non-failing if minBound <= maxBound, which is True
  ]

verifyFuncRule :: TermDomain a => [Int] -> TypeExpr -> Expr -> VerifyStateM a ()
verifyFuncRule vs ftype exp = do
  setFreshVarIndex (maximum (0 : vs ++ allVars exp) + 1)
  setVarExps  (map (\(v,te) -> (v, te, Var v)) (funcType2TypedVars vs ftype))
  qf <- getCurrentFuncName
  mbnfcond <- getNonFailConditionOf qf
  maybe
    (setCallCondition fcTrue)
    (\(nfcvars,fcond) -> do
      let freenfcargs = filter ((`notElem` vs) . fst) nfcvars
      newfvars <- mapM (\_ -> newFreshVarIndex) freenfcargs
      -- add renamed free variables of condition to the current set of variables
      addVarExps (map (\(v,(_,t)) -> (v,t,Var v)) (zip newfvars freenfcargs))
      -- rename free variables before adding the condition:
      setCallCondition $ expandExpr (map (\(nv,(v,t)) -> (v,t,Var nv))
                                         (zip newfvars freenfcargs))  fcond)
     mbnfcond
  printIfVerb 3 $ "CHECKING FUNCTION " ++ snd qf
  ctype    <- getCallType qf (length vs)
  rhstypes <- mapM (\f -> getCallType f 0) (funcsInExpr exp)
  if all isTotalACallType (ctype:rhstypes)
    then printIfVerb 3 $ "not checked since trivial"
    else maybe (maybe
                  (printIfVerb 3 "not checked since marked as always failing")
                  (\_ -> do
                    setVarTypes (map (\v -> (v, [(IOT [([], anyType)], [])]))
                                     vs)
                    showVarExpTypes
                    verifyExpr True exp
                    return () )
                  mbnfcond)
               (\atargs -> do
                  setVarTypes (map (\(v,at) -> (v, [(IOT [([], at)], [])]))
                                   (zip vs atargs))
                  showVarExpTypes
                  verifyExpr True exp
                  return ())
               ctype
  printIfVerb 3 $ take 70 (repeat '-')

-- Shows the current variable expressions and types if verbosity > 2.
showVarExpTypes :: TermDomain a => VerifyStateM a ()
showVarExpTypes = do
  qf <- getCurrentFuncName
  opts <- getToolOptions
  when (optVerb opts > 3) $ do
    st <- get
    lift $ putStr $
      "Current set of variables in function " ++ snd qf ++
      ":\nVariable bindings:\n" ++
      unlines (map (\ (v,te,e) -> showBindExp v e ++
                     if te == unknownType then "" else " :: " ++ showTypeExp te)
                   (vstVarExp st))
    vartypes <- getVarTypes
    lift $ putStr $ "Variable types\n" ++ showVarTypes vartypes
    cond <- getExpandedCondition
    lift $ putStrLn $ "Current condition: " ++ showSimpExp cond

-- Verify an expression (if the first argument is `True`) and,
-- if the expression is not a variable, create a fresh
-- variable and a binding for this variable.
-- The variable which identifies the expression is returned.
verifyExpr :: TermDomain a => Bool -> Expr -> VerifyStateM a Int
verifyExpr verifyexp exp = case exp of
  Var v -> do iots <- if verifyexp then verifyVarExpr v exp
                                   else return [(v, ioVarType anyType)]
              addVarTypes iots
              return v
  _     -> do v <- newFreshVarIndex
              addVarExps [(v, unknownType, exp)]
              iots <- if verifyexp then verifyVarExpr v exp
                                   else return [(v, ioVarType anyType)]
              addVarTypes iots
              return v

-- Verify an expression identified by variable (first argument).
-- The in/out variable types collected for the variable are returned.
verifyVarExpr :: TermDomain a => Int -> Expr -> VerifyStateM a (VarTypesMap a)
verifyVarExpr ve exp = case exp of
  Var v         -> if v == ve
                     then return []
                     else do
                       --lift $ putStrLn $ "Expression with different vars: " ++
                       --                  show (v,ve)
                       --showVarExpTypes
                       vtypes <- getVarTypeOf v
                       -- TODO: improve by handling equality constraint v==ve
                       -- instead of copying the current types for v to ve:
                       return $ [(ve, vtypes)]
  Lit l         -> return [(ve, [(IOT [([], aLit l)], [])])]
  Comb ct qf es -> checkPredefinedOp exp $ do
    vs <- if isEncSearchOp qf
            then -- for encapsulated search, failures in arguments are hidden
                 mapM (verifyExpr False) es
            else if isSetFunOp qf
                   then -- for a set function, the function argument is hidden
                        mapM (\ (i,e) -> verifyExpr (i>0) e)
                             (zip [0..] es)
                   else mapM (verifyExpr True) es
    case ct of
      FuncCall -> do verifyFuncCall exp qf vs
                     ftype <- getFuncType qf (length vs)
                     return [(ve, [(ftype, vs)])]
      FuncPartCall n -> -- note: also partial calls are considered as constr.
                  do ctype <- getCallType qf (n + length es)
                     unless (isTotalACallType ctype) $ do
                       printIfVerb 3 $ "UNSATISFIED ABSTRACT CALL TYPE: " ++
                         "partial application of non-total function\n"
                       addFailedFunc exp Nothing fcTrue
                     -- note: also partial calls are considered as constructors
                     returnConsIOType qf vs ve
      _        -> returnConsIOType qf vs ve
  Let bs e      -> do addVarExps (map (\(v,be) -> (v, unknownType, be)) bs)
                      mapM_ (addVarAnyType . fst) bs
                      iotss <- mapM (\ (v,be) -> verifyVarExpr v be) bs
                      -- remove initially set anyType's for the bound vars:
                      mapM_ (removeVarAnyType . fst) bs
                      addVarTypes (concat iotss)
                      mapM_ (addAnyTypeIfUnknown . fst) bs
                      verifyVarExpr ve e
  Free vs e     -> do addVarExps (map (\v -> (v, unknownType, Var v)) vs)
                      mapM_ addVarAnyType vs
                      verifyVarExpr ve e
  Or e1 e2      -> do iots1 <- verifyVarExpr ve e1 -- 
                      iots2 <- verifyVarExpr ve e2
                      return (concVarTypesMap iots1 iots2)
  Case _ ce bs  -> do cv <- verifyExpr True ce
                      verifyMissingBranches exp cv bs
                      iotss <- mapM (verifyBranch cv ve) bs
                      return (foldr concVarTypesMap [] iotss)
  Typed e _     -> verifyVarExpr ve e -- TODO: use type info
 where
  -- adds Any type for a variable if it is unknown
  addAnyTypeIfUnknown v = do
    vts <- getVarTypeOf v
    when (null vts) (addVarAnyType v)

  -- Return an input/output type for a constructor and its arguments
  returnConsIOType qc vs rv = do
    vts <- getVarTypes
    let vstypes = map (flip getVarType vts) vs
    --let anys = anyTypes (length vs)  -- TODO: use vs types from VarTypes!!!!
    --return [(rv, IOT [(anys, aCons qc anys)], vs)]
    return [(rv, [(IOT [(vstypes, aCons qc vstypes)], vs)])]

-- Verify the abstract type or non-fail condition of a function call.
-- The second argument is the function call as a FlatCurry expression,
-- the third argument is the function name, and the fourth argument
-- are the argument variables.
verifyFuncCall :: TermDomain a => Expr -> QName -> [Int] -> VerifyStateM a ()
verifyFuncCall exp qf vs = do
  opts <- fmap vstToolOpts get
  if qf == pre "failed" || (optError opts && qf == pre "error")
    then do
      bcond  <- getExpandedCondition
      unsat  <- incrNonTrivialCall >> incrUnsatSMT >> isUnsatisfiable bcond
      if unsat
        then do currfn <- getCurrentFuncName
                printIfVerb 3 $ "FUNCTION " ++ snd currfn ++ ": CALL TO " ++
                  snd qf ++ showArgumentVars vs ++ " NOT REACHABLE\n"
        else addFailedFunc exp Nothing fcTrue
    else do atype <- getCallType qf (length vs)
            if isTotalACallType atype
              then return ()
              else do mbnfcond <- getNonFailConditionOf qf
                      verifyNonTrivFuncCall exp qf vs atype mbnfcond

-- Verify the non-trivial abstract type or non-fail condition
--  of a function call.
-- The first argument is the expression of the call (used to show
-- the possible failed expression), the second and third arguments
-- are the name and the arguments of the current function call.
-- The last argument is the possible non-fail condition for this function.
verifyNonTrivFuncCall :: TermDomain a => Expr -> QName -> [Int]
                      -> ACallType a -> Maybe NonFailCond -> VerifyStateM a ()
verifyNonTrivFuncCall exp qf vs atype mbnfcond = do
  incrNonTrivialCall
  currfn <- getCurrentFuncName
  printIfVerb 3 $ "FUNCTION " ++ snd currfn ++ ": VERIFY CALL TO " ++
                  snd qf ++ showArgumentVars vs ++
                  "\n  w.r.t. call type: " ++ prettyFunCallAType atype
  callcond <- maybe
    (return fcFalse)
    (\(nfcvars,nfcond) -> do
      -- compute the precondition for this call by renaming the arguments:
      let freenfcargs = filter ((`notElem` [1..length vs]) . fst) nfcvars
      newfvars <- mapM (\_ -> newFreshVarIndex) freenfcargs
      -- add renamed free variables of condition to the current set of variables
      addVarExps (map (\(v,(_,t)) -> (v,t,Var v)) (zip newfvars freenfcargs))
      -- rename variable in condition:
      let rnmcvars = zip [1.. length vs] vs ++
                     map (\(nv,(v,_)) -> (v, nv)) (zip newfvars freenfcargs)
      st <- get
      let callcond0 = expandExpr (vstVarExp st) (renameAllVars rnmcvars nfcond)
      printIfVerb 3 $ "  and call condition: " ++ showSimpExp callcond0
      return callcond0)
    mbnfcond
  showVarExpTypes
  --allvts <- getVarTypes
  --printIfVerb 3 $ "Current variable types:\n" ++ showVarTypes allvts
  svts <- fmap simplifyVarTypes getVarTypes
  printIfVerb 4 $ "Simplified variable types:\n" ++ showVarTypes svts
  let vts = map (\v -> (v, getVarType v svts)) vs
  printIfVerb 3 $ "Variable types in this call: " ++ printVATypes vts
  if subtypeOfRequiredCallType (map snd vts) atype
    then printIfVerb 3 "CALL TYPE SATISFIED\n"
    else -- Check whether types of call argument variables can be made
         -- more specific to satisfy the call type. If all these variables
         -- are parameters of the current functions, specialize the
         -- call type of this function and analyze it again.
         do printIfVerb 3 "UNSATISFIED ABSTRACT CALL TYPE\n"
            maybe
              (if callcond == fcFalse
                 then addFailedFunc exp Nothing callcond
                 else do
                  -- check whether the negated call condition is unsatisfiable
                  -- (if yes: call condition holds)
                  implcond <- getExpandedConditionWithConj (fcNot callcond)
                  implied  <- incrUnsatSMT >> isUnsatisfiable implcond
                  if implied
                    then printIfVerb 3 "CALL CONDITION SATISFIED\n"
                    else addFailedFunc exp Nothing callcond)
              (\newvts -> do
                 printIfVerb 3 $ "COULD BE SATISFIED BY ENSURING:\n" ++
                                 printVATypes newvts
                 addFailedFunc exp (Just newvts) fcTrue
              )
              (specializeToRequiredType vts atype)
 where
  printVATypes = intercalate ", " . map (\ (v,t) -> show v ++ '/' : showType t)

-- Auxiliary operation to support specific handling of applying predefined
-- operations with specific non-fail conditions.
-- If the current expression (first argument) is not a specific
-- predefined operation, the computation will be continued by calling
-- the second argument (a continuation).
-- For instance, division operations require that the second argument is
-- non-zero. If this argument is a constant, it will be immediately checked,
-- otherwise a non-fail condition will be generated and checked.
-- Since such primitive operations can be invoked by FlatCurry expressions
-- with various structures (due to the numeric type classes),
-- these structures will be checked.
checkPredefinedOp :: TermDomain a => Expr -> VerifyStateM a (VarTypesMap a)
                  -> VerifyStateM a (VarTypesMap a)
checkPredefinedOp exp cont = case exp of
  -- check integer division:
  Comb FuncCall ap1 [Comb FuncCall ap2 [Comb FuncCall qf _, arg1], arg2]
    | ap1 == apply && ap2 == apply && qf `elem` intDivOps
    -> tryCheckNumValue (intValue arg2) qf arg1 arg2 fcInt
  -- check float division:
  Comb FuncCall qf [arg1, arg2]
    | qf == pre "_impl#/#Prelude.Fractional#Prelude.Float#"
    -> tryCheckNumValue (floatValue arg2) qf arg1 arg2 fcFloat
  Comb FuncCall ap1 [Comb FuncCall ap2 [Comb FuncCall qf _, arg1], arg2]
    | ap1 == apply && ap2 == apply && qf `elem` floatDivOps
    -> tryCheckNumValue (floatValue arg2) qf arg1 arg2 fcFloat
  -- check sqrt call:
  Comb FuncCall ap1 [Comb FuncCall qf [], arg]
    | ap1 == apply && qf == pre "_impl#sqrt#Prelude.Floating#Prelude.Float#"
    -> maybe (verifyPredefinedOp qf [arg] fcFloat)
             (\x -> do unless (x >= 0) $ addFailedFunc exp Nothing fcFalse
                       return [])
             (floatValue arg)
  _ -> cont
 where
  tryCheckNumValue mbx qf arg1 arg2 te =
    maybe (verifyPredefinedOp qf [arg1,arg2] te)
          (\z -> do if z == 0 then addFailedFunc exp Nothing fcFalse
                              else printIfVerb 4 nonZeroOkMsg
                    verifyExpr True arg1
                    return [])
          mbx

  verifyPredefinedOp qf args te =
     maybe (do printIfVerb 0 $
                 "WARNING: non-fail condition of " ++ snd qf ++ " not found!"
               cont)
           (\nfc -> do vs <- mapM (verifyExpr True) args
                       mapM_ (\v -> setVarExpTypeOf v te) vs
                       verifyNonTrivFuncCall exp qf vs failACallType (Just nfc)
                       return [])
           (lookupPredefinedNonFailCond qf)

  intValue e = case e of
    Lit (Intc i) -> Just i
    Comb FuncCall ap [ Comb FuncCall fromint _ , nexp]
      | ap == apply && fromint == pre "fromInt" -> intValue nexp
    _            -> Nothing

  floatValue e = case e of
    Lit (Floatc f) -> Just f
    Comb FuncCall ap [ Comb FuncCall fromfloat _ , nexp]
      | ap == apply && fromfloat == pre "fromFloat" -> floatValue nexp
    Comb FuncCall ap [(Comb FuncCall fromint _), nexp]
       | ap == apply && fromint == pre "fromInt" -> fmap fromInt (intValue nexp)
    Comb FuncCall negFloat [fexp]
      | negFloat == pre "_impl#negate#Prelude.Num#Prelude.Float#"
                   -> fmap negate (floatValue fexp)
    _              -> Nothing

  apply = pre "apply"

  nonZeroOkMsg = "Divion with non-zero constant is non-failing"

-- Verify whether missing branches exists and are not reachable.
verifyMissingBranches :: TermDomain a => Expr -> Int -> [BranchExpr] -> VerifyStateM a ()
verifyMissingBranches _ _ [] = do
  currfn <- getCurrentFuncName
  error $ "Function " ++ snd currfn ++ " contains case with empty branches!"
verifyMissingBranches exp casevar (Branch (LPattern lit) _ : bs) = do
  incrIncompleteCases
  currfn <- getCurrentFuncName
  let lits = lit : map (patLiteral . branchPattern) bs
  cvtype <- getVarTypes >>= return . getVarType casevar
  unless (isSubtypeOf cvtype (foldr1 lubType (map aLit lits))) $ do
    printIfVerb 3 $ showIncompleteBranch currfn exp [] ++ "\n"
    showVarExpTypes
    addMissingCase exp []
verifyMissingBranches exp casevar (Branch (Pattern qc _) _ : bs) = do
  consinfos <- getConsInfos
  let otherqs  = map ((\p -> (patCons p, length(patArgs p))) . branchPattern) bs
      siblings = siblingsOfCons consinfos qc
      missingcs = siblings \\ otherqs -- constructors having no branches
  currfn <- getCurrentFuncName
  unless (null missingcs) $ do
    printIfVerb 0 $ -- just for checking in order to refactor in the future...
      "MISSING CONSTRUCTORS " ++ show missingcs ++ " IN FUNCTION " ++ snd currfn
    incrIncompleteCases
    cvtype <- getVarTypes >>= return . getVarType casevar
    let posscs = map fst
                     (filter (\(c,ar) -> let ctype = aCons c (anyTypes ar)
                                         in joinType cvtype ctype /= emptyType)
                             missingcs)
    cond <- getExpandedCondition
    unless (null posscs) $
      if cond == fcTrue
        then do
          printIfVerb 3 $ showIncompleteBranch currfn exp posscs ++ "\n"
          showVarExpTypes
          addMissingCase exp posscs
        else do
          showVarExpTypes
          unsatcons <- fmap concat $ mapM checkMissCons posscs
          unless (null unsatcons) $ do
            printIfVerb 3 $
              "UNCOVERED CONSTRUCTORS: " ++ unwords (map snd unsatcons)
            setNewFunCondition currfn nfcFalse
            addMissingCase exp unsatcons
 where
  -- check whether a constructor is excluded by the current call condition:
  checkMissCons cs = do
    printIfVerb 4 $ "CHECKING UNREACHABILITY OF CONSTRUCTOR " ++ snd cs
    consinfos <- getConsInfos
    let iscons = transTester consinfos cs (Var casevar)
    bcond <- getExpandedCondition
    unsat <- isUnsatisfiable (fcAnd iscons bcond)
    return $ if unsat then [] else [cs]

-- Gets the state information which might be changed during branch verification.
getBranchState :: TermDomain a => VerifyStateM a ([(Int,TypeExpr,Expr)], VarTypesMap a, Expr -> Expr)
getBranchState = do
  ves  <- getVarExps
  vts  <- getVarTypes
  cond <- getCondition
  return (ves,vts,cond)

-- Gets the state information which might be changed during branch verification.
restoreBranchState :: TermDomain a => ([(Int,TypeExpr,Expr)], VarTypesMap a, Expr -> Expr) -> VerifyStateM a ()
restoreBranchState (ves,vts,cond) = do
  setVarExps ves
  setVarTypes vts
  setCondition cond

-- Verify a branch where the first argument is the case argument variable
-- and the second argument is the variable identifying the case expression.
verifyBranch :: TermDomain a => Int -> Int -> BranchExpr -> VerifyStateM a (VarTypesMap a)
verifyBranch casevar ve (Branch (LPattern l) e) = do
  bstate <- getBranchState
  vts  <- getVarTypes
  let branchvartypes = bindVarInIOTypes casevar (aLit l) vts
  printIfVerb 4 $ "BRANCH WITH LITERAL '" ++ show l ++ "'"
  addEquVarCondition casevar (Lit l)
  if isEmptyType (getVarType casevar branchvartypes)
    then return [] -- unreachable branch
    else do setVarTypes branchvartypes
            iots <- verifyVarExpr ve e
            restoreBranchState bstate
            return iots
verifyBranch casevar ve (Branch (Pattern qc vs) e) = do
  bstate <- getBranchState
  ves  <- getVarExps
  consinfos <- getConsInfos
  let vet = maybe unknownType snd3 (find ((== casevar) . fst3) ves)
  addVarExps (map (\ (v,vt) -> (v, vt, Var v))
                  (zip vs (if vet == unknownType
                             then repeat unknownType
                             else patArgTypes consinfos vet)))
  vts  <- getVarTypes
  let pattype        = aCons qc (anyTypes (length vs))
      branchvartypes = simplifyVarTypes (bindVarInIOTypes casevar pattype vts)
      casevartype    = getVarType casevar branchvartypes
  -- add single case for case variable and pattern to the current condition:
  if null vs then addEquVarCondition casevar (Comb ConsCall qc [])
             else addSingleCase casevar qc vs
  printIfVerb 4 $ "BRANCH WITH CONSTRUCTOR '" ++ snd qc ++ "'"
  showVarExpTypes
  if isEmptyType casevartype
    then do restoreBranchState bstate
            return [] -- unreachable branch
    else do setVarTypes branchvartypes
            mapM_ (\(v,t) -> addVarType v (ioVarType t))
                  (zip vs (argTypesOfCons qc (length vs) casevartype))
            iots <- verifyVarExpr ve e
            restoreBranchState bstate
            return iots
 where
  -- compute the argument types from the result type `pt` of the branch variable
  -- where some regularly occurring constructors are directly implemented
  patArgTypes consinfos pt
    | qc == pre ":"
    = case pt of TCons tc [et] | tc == pre "[]" -> [et, pt]
                 _                              -> noPatTypeErr
    | qc == pre "(,)"
    = case pt of TCons tc [t1,t2] | tc == pre "(,)" -> [t1,t2]
                 _                                  -> noPatTypeErr
    | qc == pre "Just"
    = case pt of TCons tc [t] | tc == pre "Maybe" -> [t]
                 _                                -> noPatTypeErr
    | otherwise
    = maybe (error $ "Info about constructor '" ++ snd qc ++ "' not found!")
            (\(_,ConsType tes tc tvs,_) ->
              case pt of
                TCons dtc ats | tc == dtc -> map (applyTSubst (zip tvs ats)) tes
                _                         -> noPatTypeErr
            )
            (lookup qc consinfos)

  noPatTypeErr = error $
    "verifyBranch: cannot compute pattern argument types for " ++ snd qc

-- Gets the abstract type of a variable w.r.t. a set of variable types.
getVarType :: TermDomain a => Int -> VarTypesMap a -> a
getVarType v vtsmap =
  maybe (error $ "Type of variable " ++ show v ++ " not found!")
        (\vts -> let rts = concatMap (\ (IOT iots, _) -> map snd iots) vts
                 in if null rts then emptyType
                                else foldr1 lubType rts)
        (lookup v vtsmap)

------------------------------------------------------------------------------
--- Computes for a given set of function declarations in a module
--- a mapping from module function names to the list of function
--- declarations where these names are used in the right-hand side.
funcDecls2Usage :: String -> [FuncDecl] -> Map.Map QName [FuncDecl]
funcDecls2Usage mname fdecls = addFDecls (Map.empty) fdecls
 where
  addFDecls m []       = m
  addFDecls m (fd:fds) =
    let rhsfuns = filter (\f -> fst f == mname) (usedFuncsInFunc fd)
    in Map.insertListWith unionFDecls (map (\qf -> (qf,[fd])) rhsfuns)
                          (addFDecls m fds)

unionFDecls :: [FuncDecl] -> [FuncDecl] -> [FuncDecl]
unionFDecls = unionBy (\fd1 fd2 -> funcName fd1 == funcName fd2)

--- Get function names used in the right-hand side of a function declaration.
usedFuncsInFunc :: FuncDecl -> [QName]
usedFuncsInFunc = usedFuncsInRule . funcRule

--- Get function names used in the right-hand side of a rule.
usedFuncsInRule :: Rule -> [QName]
usedFuncsInRule = trRule (\_ body -> funcsInExpr body) (\_ -> [])

------------------------------------------------------------------------------
--- A list of any types of a given length.
anyTypes :: TermDomain a => Int -> [a]
anyTypes n = take n (repeat anyType)

------------------------------------------------------------------------------
-- Utilities

-- I/O action to force evaluation of the argument to normal form.
enforceNormalForm :: Options -> String -> a -> IO ()
enforceNormalForm opts s x
  | optEnforceNF opts
  = do whenStatus opts $ putStr $ "EVALUATE " ++ s ++ " TO NORMAL FORM..."
       hFlush stdout
       (id $!! x) `seq` return ()
       printWhenStatus opts "DONE"
  | otherwise
  = return ()

------------------------------------------------------------------------------
-- Shows the simplified expression.
showSimpExp :: Expr -> String
showSimpExp = showExp . simpExpr

--- Checks the unsatisfiability of a Boolean expression w.r.t. a set
--- of variables (second argument) with an SMT solver.
isUnsatisfiable :: TermDomain a => Expr -> VerifyStateM a Bool
isUnsatisfiable bexp = do
  st <- get
  if optSMT (vstToolOpts st)
    then do
      fname  <- getCurrentFuncName
      vts <- fmap (map (\(v,te,_) -> (v,te))) getVarExps
      let allvs    = allFreeVars bexp
      let vtypes   = filter ((`elem` allvs) . fst) vts
          question = "Verifying function " ++ snd fname ++ ":\n\n" ++
                     "IS\n  " ++ showSimpExp bexp ++ "\nUNSATISFIABLE?"
      unless (all (`elem` map fst vtypes) allvs) $ lift $ putStrLn $
        "WARNING in operation '" ++ snd fname ++
        "': missing variables in unsatisfiability check!"
      consinfos <- getConsInfos
      answer <- lift $ checkUnsatisfiabilityWithSMT (vstToolOpts st)
                         fname question (vstModules st) consinfos vtypes bexp
      maybe (setToolError >> return False) return answer
    else return False

------------------------------------------------------------------------------