-----------------------------------------------------------------------------
--- A tool to verify non-failure properties of Curry operations.
---
--- @author  Michael Hanus
--- @version August 2020
---------------------------------------------------------------------------

module Main where

import Directory    ( doesFileExist )
import FilePath     ( (</>) )
import Integer      ( ilog )
import IOExts
import List         ( (\\), elemIndex, find, isPrefixOf, isSuffixOf
                    , maximum, minimum, partition, splitOn, union )
import Maybe        ( catMaybes )
import State
import System

-- Imports from dependencies:
import Analysis.ProgInfo
import Analysis.TotallyDefined ( siblingCons )
import Analysis.Types
import Contract.Names
import Contract.Usage          ( checkContractUsage )
import CASS.Server             ( analyzeGeneric, analyzePublic )
import Debug.Profile
import FlatCurry.Annotated.TypeSubst ( substRule )
import FlatCurry.Files               ( readFlatCurryInt )
import FlatCurry.Types
import FlatCurry.Annotated.Goodies
import ShowFlatCurry                 ( showCurryModule )
import System.Path                   ( fileInPath )

-- Imports from package modules:
import ESMT
import Curry2SMT
import FlatCurry.Typed.Read
import FlatCurry.Typed.Goodies
import FlatCurry.Typed.Names
import FlatCurry.Typed.Types
import PackageConfig ( packagePath )
import ToolOptions
import VerifierState

------------------------------------------------------------------------
-- To support testing:

test :: Int -> String -> IO ()
test v = verifyNonFailingMod defaultOptions { optVerb = v }

testv :: String -> IO ()
testv = test 3

testcv :: String -> IO ()
testcv = verifyNonFailingMod defaultOptions { optVerb = 3, optContract = True }

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

banner :: String
banner = unlines [bannerLine,bannerText,bannerLine]
 where
   bannerText = "Fail-Free Verification Tool for Curry (Version of 03/08/20)"
   bannerLine = take (length bannerText) (repeat '=')

---------------------------------------------------------------------------
main :: IO ()
main = do
  args <- getArgs
  (opts,progs) <- processOptions banner args
  let optname = optName opts
  if not (null optname)
    then putStrLn $ "Non-failure condition for '" ++ optname ++ "':\n" ++
                    encodeContractName (optname ++ "'nonfail")
    else do
      z3exists <- fileInPath "z3"
      if z3exists
        then do
          when (optVerb opts > 0) $ putStrLn banner
          verifyNonFailingModules opts [] progs
        else do
          putStrLn "NON-FAILING ANALYSIS SKIPPED:"
          putStrLn "The SMT solver Z3 is required for the verifier to work"
          putStrLn "but the program 'z3' is not found on the PATH!"
          exitWith 1

verifyNonFailingModules :: Options -> [String] -> [String] -> IO ()
verifyNonFailingModules _ _ [] = done
verifyNonFailingModules opts verifiedmods (mod:mods)
  | mod `elem` verifiedmods
  = verifyNonFailingModules opts verifiedmods mods
  | optRec opts
  = do (Prog _ imps _ _ _) <- readFlatCurryInt mod
       let newimps = filter (`notElem` verifiedmods) imps
       if null newimps
         then do printWhenStatus opts ""
                 verifyNonFailingMod opts mod
                 verifyNonFailingModules opts (mod:verifiedmods) mods
         else verifyNonFailingModules opts verifiedmods
                     (newimps ++ mod : (mods \\ newimps))
  | otherwise -- non-recursive
  = do verifyNonFailingMod opts mod
       verifyNonFailingModules opts (mod:verifiedmods) mods


verifyNonFailingMod :: Options -> String -> IO ()
verifyNonFailingMod opts modname = do
  printWhenStatus opts $ "Analyzing module '" ++ modname ++ "':"
  prog <- readSimpTypedFlatCurryWithSpec opts modname
  let errs = checkContractUsage (progName prog)
               (map (\fd -> (snd (funcName fd), funcType fd)) (progFuncs prog))
  unless (null errs) $ do
    putStr $ unlines (map showOpError errs)
    exitWith 1
  impprogs <- mapIO (readSimpTypedFlatCurryWithSpec opts) (progImports prog)
  let allprogs = prog : impprogs
      vinfo  = foldr addFunsToVerifyInfo (initVerifyInfo opts)
                     (map progFuncs allprogs)
      vstate = foldr addProgToState (initVState vinfo) allprogs
  siblingconsinfo <- loadAnalysisWithImports siblingCons prog
  pi1 <- getProcessInfos
  printWhenAll opts $ unlines $
    ["ORIGINAL PROGRAM:", line, showCurryModule (unAnnProg prog), line]
  vstref <- newIORef vstate
  proveNonFailingFuncs opts siblingconsinfo vstref (progFuncs prog)
  stats <- readIORef vstref
  pi2 <- getProcessInfos
  let tdiff = maybe 0 id (lookup ElapsedTime pi2) -
              maybe 0 id (lookup ElapsedTime pi1)
  when (optTime opts) $ putStrLn $
    "TOTAL VERIFICATION TIME  : " ++ show tdiff ++ " msec"
  when (optVerb opts > 0 || not (isVerified stats)) $
    putStr (showStats stats)
 where
  line = take 78 (repeat '-')

  showOpError (qf,err) =
    snd qf ++ " (module " ++ fst qf ++ "): " ++ err

-- Loads CASS analysis results for a module and its imported entities.
loadAnalysisWithImports :: Analysis a -> TAProg -> IO (ProgInfo a)
loadAnalysisWithImports analysis prog = do
  maininfo <- analyzeGeneric analysis (progName prog)
                >>= return . either id error
  impinfos <- mapIO (\m -> analyzePublic analysis m >>=
                                                     return . either id error)
                    (progImports prog)
  return $ foldr combineProgInfo maininfo impinfos

---------------------------------------------------------------------------
-- The state of the transformation process contains
-- * the current assertion
-- * a fresh variable index
-- * a list of all introduced variables and their types:
data TransState = TransState
  { preCond    :: Term
  , freshVar   :: Int
  , varTypes   :: [(Int,TypeExpr)]
  }

makeTransState :: Int -> [(Int,TypeExpr)] -> TransState
makeTransState = TransState tTrue

-- Increments fresh variable index.
incFreshVarIndex :: TransState -> TransState
incFreshVarIndex st = st { freshVar = freshVar st + 1 }

-- Adds variables to the state.
addVarTypes :: [(Int,TypeExpr)] -> TransState -> TransState
addVarTypes vts st = st { varTypes = vts ++ varTypes st }

---------------------------------------------------------------------------
-- Prove that a list of defined functions is fail free (w.r.t. their
-- non-fail conditions).
proveNonFailingFuncs :: Options -> ProgInfo [(QName,Int)] -> IORef VState
                     -> [TAFuncDecl] -> IO ()
proveNonFailingFuncs opts siblingconsinfo vstref =
  mapIO_ (proveNonFailingFunc opts siblingconsinfo vstref)

-- Prove that a function is fail free (w.r.t. their non-fail condition).
proveNonFailingFunc :: Options -> ProgInfo [(QName,Int)] -> IORef VState
                    -> TAFuncDecl -> IO ()
proveNonFailingFunc opts siblingconsinfo vstref fdecl =
  unless (isContractOp (funcName fdecl) || isProperty fdecl) $ do
    printWhenIntermediate opts $
      "Operation to be analyzed: " ++ snd (funcName fdecl)
    modifyIORef vstref incNumAllInStats
    let efdecl = etaExpandFuncDecl fdecl
    proveNonFailingRule opts siblingconsinfo vstref
                        (funcName efdecl) (funcType efdecl)
                        (funcRule efdecl)

-- Prove that a function rule is fail free (w.r.t. their non-fail condition).
-- The rule is in eta-expanded form.
proveNonFailingRule :: Options -> ProgInfo [(QName,Int)] -> IORef VState
                    -> QName -> TypeExpr -> TARule -> IO ()
proveNonFailingRule _ _ vstref qn ftype (AExternal _ _) = do
  ti <- readVerifyInfoRef vstref
  let atypes = argTypes ftype
      args   = zip [1 .. length atypes] atypes
      (nfcond,_)  = nonfailPreCondExpOf ti qn ftype args (makeTransState 0 [])
  unless (nfcond == tTrue) $ modifyIORef vstref incNumNFCInStats
proveNonFailingRule opts siblingconsinfo vstref qn@(_,fn) ftype
                    (ARule _ rargs rhs) = do
  ti <- readVerifyInfoRef vstref
  let -- compute non-fail precondition of operation:
      s0 = makeTransState (maximum (0 : map fst rargs ++ allVars rhs) + 1) rargs
      (precondformula,s1)  = nonfailPreCondExpOf ti qn ftype rargs s0
      s2 = s1 { preCond = precondformula }
  unless (precondformula == tTrue)  $ modifyIORef vstref incNumNFCInStats
  -- verify only if the precondition is different from always failing:
  unless (precondformula == tFalse) $ proveNonFailExp ti s2 rhs
 where
  proveNonFailExp ti pts exp = case simpExpr exp of
    AComb _ ct (qf,qfty) args -> do
      mapIO_ (proveNonFailExp ti pts) args
      when (isCombTypeFuncPartCall ct) $
        let qnnonfail = toNonFailQName qf
        in maybe done -- h.o. call nonfailing if op. has no non-fail cond.
             (\_ -> do
               let reason = "due to call '" ++ ppTAExpr exp ++ "'"
               modifyIORef vstref (addFailedFuncToStats fn reason)
               printWhenIntermediate opts $
                 fn ++ ": POSSIBLY FAILING CALL OF '" ++ snd qf ++ "'")
             (find (\fd -> funcName fd == qnnonfail) (nfConds ti))
      when (ct==FuncCall) $ do
        printWhenIntermediate opts $ "Analyzing call to " ++ snd qf
        let ((bs,_)    ,pts1) = normalizeArgs args pts
            (bindexps  ,pts2) = mapS (binding2SMT True ti) bs pts1
            callargs = zip (map fst bs) (map annExpr args)
            (nfcondcall,pts3) = nonfailPreCondExpOf ti qf qfty callargs pts2
        -- TODO: select from 'bindexps' only demanded argument positions
        valid <- if nfcondcall == tTrue
                   then return (Just True) -- true non-fail cond. is valid
                   else do
                     modifyIORef vstref incFailTestInStats
                     let title = "SMT script to verify non-failing call of '" ++
                                 snd qf ++ "' in function '" ++ fn ++ "'"
                     checkImplicationWithSMT opts vstref title (varTypes pts3)
                          (preCond pts) (tConj bindexps) nfcondcall
        if valid == Just True
          then do
            printWhenIntermediate opts $
              fn ++ ": NON-FAILING CALL OF '" ++ snd qf ++ "'"
          else do
            let reason = if valid == Nothing
                           then "due to SMT error"
                           else "due to call '" ++ ppTAExpr exp ++ "'"
            modifyIORef vstref (addFailedFuncToStats fn reason)
            printWhenIntermediate opts $
              fn ++ ": POSSIBLY FAILING CALL OF '" ++ snd qf ++ "'"
    ACase _ _ e brs -> do
      proveNonFailExp ti pts e
      maybe
       (-- check a case expression for missing constructors:
        let freshvar = freshVar pts
            freshtypedvar = (freshvar, annExpr e)
            (be,pts1) = binding2SMT True ti (freshvar,e) (incFreshVarIndex pts)
            pts2 = pts1 { preCond = tConj [preCond pts, be]
                        , varTypes = freshtypedvar : varTypes pts1 }
            misscons = missingConsInBranch siblingconsinfo brs
        in do mapIO_ (verifyMissingCons pts2 freshtypedvar exp) misscons
              mapIO_ (proveNonFailBranch ti pts2 freshtypedvar) brs
       )
       (\ (fe,te) ->
           -- check a Boolean case with True/False branch:
           let (be,pts1) = pred2SMT e pts
               ptsf = pts1 { preCond = tConj [preCond pts, tNot be] }
               ptst = pts1 { preCond = tConj [preCond pts, be] }
           in do proveNonFailExp ti ptsf fe
                 proveNonFailExp ti ptst te
       )
       (testBoolCase brs)
    AOr _ e1 e2 -> do proveNonFailExp ti pts e1
                      proveNonFailExp ti pts e2
    ALet _ bs e -> do let ((rbs,re), pts1) = renameLetVars pts bs e
                      mapIO_ (proveNonFailExp ti pts1) (map snd rbs)
                      proveNonFailExp ti pts1 re
    AFree _ fvs e -> do let ((_,re), pts1) = renameFreeVars pts fvs e
                        proveNonFailExp ti pts1 re
    ATyped _ e _ -> proveNonFailExp ti pts e
    AVar _ _ -> done
    ALit _ _ -> done

  -- verify whether a variable (2. argument) can have the constructor (3. arg.)
  -- as a value w.r.t. the collected assertions
  verifyMissingCons pts (var,vartype) exp (cons,_) = do
    let title = "check missing constructor case '" ++ snd cons ++
                "' in function '" ++ fn ++ "'"
    printWhenIntermediate opts $
      title ++ "\nVAR: " ++ show (var,vartype) ++ "\nCASE:: " ++
      show (unAnnExpr (simpExpr exp))
    modifyIORef vstref incPatTestInStats

    valid <- checkImplicationWithSMT opts vstref ("SMT script to " ++ title)
               (varTypes pts) (preCond pts) tTrue
               (tNot (constructorTest False cons (TSVar var) vartype))
    unless (valid == Just True) $ do
      let reason = if valid == Nothing
                     then "due to SMT error"
                     else "maybe not defined on constructor '" ++
                          showQName cons ++ "'"
      modifyIORef vstref (addFailedFuncToStats fn reason)
      printWhenIntermediate opts $
        "POSSIBLY FAILING BRANCH in function '" ++ fn ++
        "' with constructor " ++ snd cons

  proveNonFailBranch ti pts (var,vartype) branch = do
    let (ABranch p e, pts1) = renamePatternVars pts branch
        -- set pattern type correctly (important for [] pattern)
        bpat = pat2smt (setAnnPattern vartype p)
        npts = pts1 { preCond = tConj [preCond pts1, tEquVar var bpat] }
    proveNonFailExp ti npts e

-- Returns the constructors (name/arity) which are missing in the given
-- branches of a case construct.
missingConsInBranch :: ProgInfo [(QName,Int)] -> [TABranchExpr] -> [(QName,Int)]
missingConsInBranch _ [] =
  error "missingConsInBranch: case with empty branches!"
missingConsInBranch _ (ABranch (ALPattern _ _) _ : _) =
  error "TODO: case with literal pattern"
missingConsInBranch siblingconsinfo
                    (ABranch (APattern _ (cons,_) _) _ : brs) =
  let othercons = maybe (error $ "Sibling constructors of " ++
                                 showQName cons ++ " not found!")
                        id
                        (lookupProgInfo cons siblingconsinfo)
      branchcons = map (patCons . branchPattern) brs
  in filter ((`notElem` branchcons) . fst) othercons

-- Simplifies a FlatCurry expression (only at the top-level!)
-- by considering the semantics of some predefined operations.
simpExpr :: TAExpr -> TAExpr
simpExpr exp = case exp of
  AComb ty FuncCall (qf,_) args ->
    if qf == pre "?"
      then AOr ty (args!!0) (args!!1)
      else if qf == pre "ord" || qf == pre "id" -- ops without preconditions
             then head args -- note: Char is implemented as Int in SMT
             else exp
  _ -> exp

-- Translates a FlatCurry expression to a Boolean formula representing
-- the binding of a variable (represented by its index in the first
-- component) to the translated expression (second component).
-- The translated expression is normalized when necessary.
-- For this purpose, a "fresh variable index" is passed as a state.
-- Moreover, the returned state contains also the types of all fresh variables.
-- If the first argument is `False`, the expression is not strictly demanded,
-- i.e., possible contracts of it (if it is a function call) are ignored.
binding2SMT :: Bool -> VerifyInfo -> (Int,TAExpr) -> State TransState Term
binding2SMT demanded ti (resvar,exp) =
 case simpExpr exp of
  AVar _ i -> returnS $ if resvar==i then tTrue
                                     else tEquVar resvar (TSVar i)
  ALit _ l -> returnS (tEquVar resvar (lit2smt l))
  AComb rtype ct (qf,_) args ->
    normalizeArgs args `bindS` \ (bs,nargs) ->
    -- TODO: select from 'bindexps' only demanded argument positions
    mapS (binding2SMT (isPrimOp qf || optStrict (toolOpts ti)) ti) bs
         `bindS` \bindexps ->
    comb2bool qf rtype ct nargs bs bindexps
  ALet _ bs e ->
    mapS (binding2SMT False ti)
         (map (\ ((i,_),ae) -> (i,ae)) bs) `bindS` \bindexps ->
    binding2SMT demanded ti (resvar,e) `bindS` \bexp ->
    returnS (tConj (bindexps ++ [bexp]))
  AOr _ e1 e2  ->
    binding2SMT demanded ti (resvar,e1) `bindS` \bexp1 ->
    binding2SMT demanded ti (resvar,e2) `bindS` \bexp2 ->
    returnS (tDisj [bexp1, bexp2])
  ACase _ _ e brs   ->
    getS `bindS` \ts ->
    let freshvar = freshVar ts
    in putS (addVarTypes [(freshvar, annExpr e)] (incFreshVarIndex ts)) `bindS_`
       binding2SMT demanded ti (freshvar,e) `bindS` \argbexp ->
       mapS branch2bool (map (\b->(freshvar,b)) brs) `bindS` \bbrs ->
       returnS (tConj [argbexp, tDisj bbrs])
  ATyped _ e _ -> binding2SMT demanded ti (resvar,e)
  AFree _ _ _ -> error "Free variables not yet supported!"
 where
   comb2bool qf rtype ct nargs bs bindexps
    | qf == pre "otherwise"
      -- specific handling for the moment since the front end inserts it
      -- as the last alternative of guarded rules...
    = returnS (tEquVar resvar tTrue)
    | ct == ConsCall
    = returnS (tConj (bindexps ++
                     [tEquVar resvar
                              (TComb (cons2SMT (null nargs) False qf rtype)
                                     (map arg2bool nargs))]))
    | qf == pre "apply"
    = -- cannot translate h.o. apply: ignore it
      returnS tTrue
    | isPrimOp qf
    = returnS (tConj (bindexps ++
                     [tEquVar resvar
                              (TComb (cons2SMT True False qf rtype)
                                     (map arg2bool nargs))]))
    | otherwise -- non-primitive operation: add contract only if demanded
    = let targs = zip (map fst bs) (map annExpr nargs) in
      preCondExpOf ti qf targs `bindS` \precond ->
      postCondExpOf ti qf (targs ++ [(resvar,rtype)]) `bindS` \postcond ->
      returnS (tConj (bindexps ++
                     if demanded && optContract (toolOpts ti)
                       then [precond,postcond]
                       else []))

   branch2bool (cvar, ABranch p e) =
     binding2SMT demanded ti (resvar,e) `bindS` \branchbexp ->
     getS `bindS` \ts ->
     putS ts { varTypes = patvars ++ varTypes ts} `bindS_`
     returnS (tConj [ tEquVar cvar (pat2smt p), branchbexp])
    where
     patvars = if isConsPattern p
                 then patArgs p
                 else []

   arg2bool e = case e of AVar _ i -> TSVar i
                          ALit _ l -> lit2smt l
                          _ -> error $ "Not normalized: " ++ show e

-- Returns the conjunction of the non-failure condition and precondition
-- (if the tool option `contract` is set) expression for a given operation
-- and its arguments (which are assumed to be variable indices).
-- Rename all local variables by adding the `freshvar` index to them.
nonfailPreCondExpOf :: VerifyInfo -> QName -> TypeExpr -> [(Int,TypeExpr)]
                    -> State TransState Term
nonfailPreCondExpOf ti qf ftype args =
  if optContract (toolOpts ti)
    then nonfailCondExpOf ti qf ftype args `bindS` \ (fvars,nfcond) ->
         preCondExpOf     ti qf (args ++ fvars) `bindS` \precond ->
         -- simplify term in order to check later for trivial precondition
         returnS (simpTerm (tConj [nfcond,precond]))
    else nonfailCondExpOf ti qf ftype args `bindS` \ (_,rt) -> returnS rt

-- Returns the non-failure condition expression for a given operation
-- and its arguments (which are assumed to be variable indices).
-- All local variables are renamed by adding the `freshvar` index to them.
-- If the non-failure condition requires more arguments (due to a
-- higher-order call), fresh arguments are added which are also returned.
nonfailCondExpOf :: VerifyInfo -> QName -> TypeExpr -> [(Int,TypeExpr)]
                 -> State TransState ([(Int,TypeExpr)], Term)
nonfailCondExpOf ti qf ftype args =
  maybe
    (predefs qf)
    (\fd -> let moreargs = funcArity fd - length args in
            if moreargs > 0
              then -- eta-expand function call with fresh variables so that one
                   -- can check non-fail conditions with a greater arity:
                let etatypes = argTypes (dropArgTypes (length args) ftype) in
                getFreshVarsForTypes (take moreargs etatypes) `bindS` \fvars ->
                applyFunc fd (args ++ fvars) `bindS` pred2SMT `bindS` \rt ->
                returnS (fvars,rt)
              else if moreargs < 0
                     then error $ "Operation '" ++ snd qf ++
                                  "': nonfail condition has too few arguments!"
                     else applyFunc fd args `bindS` pred2SMT `bindS` \rt ->
                          returnS ([],rt) )
    (find (\fd -> decodeContractQName (funcName fd) == toNonFailQName qf)
          (nfConds ti))
 where
  predefs qn | qn `elem` [pre "failed", pre "=:="] ||
               (qn == pre "error" && optError (toolOpts ti))
             = returnS ([],tFalse)
             | otherwise = returnS ([],tTrue)

-- Returns the precondition expression for a given operation
-- and its arguments (which are assumed to be variable indices).
-- Rename all local variables by adding the `freshvar` index to them.
preCondExpOf :: VerifyInfo -> QName -> [(Int,TypeExpr)] -> State TransState Term
preCondExpOf ti qf args =
  maybe (returnS tTrue)
        (\fd -> applyFunc fd args `bindS` pred2SMT)
        (find (\fd -> funcName fd == toPreCondQName qf) (preConds ti))

-- Returns the postcondition expression for a given operation
-- and its arguments (which are assumed to be variable indices).
-- Rename all local variables by adding `freshvar` to them and
-- return the new freshvar value.
postCondExpOf :: VerifyInfo -> QName -> [(Int,TypeExpr)]
              -> State TransState Term
postCondExpOf ti qf args =
  maybe (returnS tTrue)
        (\fd -> applyFunc fd args `bindS` pred2SMT)
        (find (\fd -> funcName fd == toPostCondQName qf) (postConds ti))


-- Applies a function declaration on a list of arguments,
-- which are assumed to be variable indices, and returns
-- the renamed body of the function declaration.
-- All local variables are renamed by adding `freshvar` to them.
-- Also the new fresh variable index is returned.
applyFunc :: TAFuncDecl -> [(Int,TypeExpr)] -> State TransState TAExpr
applyFunc fdecl targs s0 =
  let tsub = maybe (error $ "applyFunc: types\n" ++
                            show (argTypes (funcType fdecl)) ++ "\n" ++
                            show (map snd targs) ++ "\ndo not match!")
                   id
                   (matchTypes (argTypes (funcType fdecl)) (map snd targs))
      (ARule _ orgargs orgexp) = substRule tsub (funcRule fdecl)
      exp = rnmAllVars (renameRuleVar orgargs) orgexp
      s1  = s0 { freshVar = max (freshVar s0)
                                (maximum (0 : args ++ allVars exp) + 1) }
  in (simpExpr $ applyArgs exp (drop (length orgargs) args), s1)
 where
  args = map fst targs
  -- renaming function for variables in original rule:
  renameRuleVar orgargs r = maybe (r + freshVar s0)
                                  (args!!)
                                  (elemIndex r (map fst orgargs))

  applyArgs e [] = e
  applyArgs e (v:vs) =
    -- simple hack for eta-expansion since the type annotations are not used:
    -- TODO: compute correct type annotations!!! (required for overloaded nils)
    let e_v =  AComb failed FuncCall
                     (pre "apply", failed) [e, AVar failed v]
    in applyArgs e_v vs

-- Translates a Boolean FlatCurry expression into a Boolean formula.
-- Calls to user-defined functions are replaced by the first argument
-- (which might be true or false).
pred2SMT :: TAExpr -> State TransState Term
pred2SMT exp = case simpExpr exp of
  AVar _ i              -> returnS (TSVar i)
  ALit _ l              -> returnS (lit2smt l)
  AComb _ ct (qf,ftype) args -> comb2bool qf ftype ct (length args) args
  _                          -> returnS (tComb (show exp) []) -- TODO!
 where
  comb2bool qf ftype ct ar args
    | qf == pre "[]" && ar == 0
    = returnS (sortedConst "nil" (polytype2sort (annExpr exp)))
    | qf == pre "not" && ar == 1
    = pred2SMT (head args) `bindS` \barg -> returnS (tNot barg)
    | qf == pre "null" && ar == 1
    = let arg = head args
      in pred2SMT arg `bindS` \barg ->
         getS `bindS` \tstate ->
         returnS (tEqu barg
                       (sortedConst "nil"
                                    (polytype2sort (typeOfVar tstate arg))))
    | qf == pre "apply"
    = -- cannot translate h.o. apply: replace it by new variable
      getS `bindS` \ts ->
      let fvar = freshVar ts
          nts  = addVarTypes [(fvar,annExpr exp)] (incFreshVarIndex ts)
      in putS nts `bindS_`
         returnS (TSVar fvar)
    | qf == pre "/="
    = comb2bool (pre "==") ftype ct ar args `bindS` \be ->
      returnS (tNot be)
    | otherwise
    = mapS pred2SMT args `bindS` \bargs ->
      returnS (TComb (cons2SMT (ct /= ConsCall || not (null bargs))
                               False qf ftype)
                     bargs)

  typeOfVar tstate e = case e of
    AVar _ i -> maybe (error $ "pred2SMT: variable " ++ show i ++ " not found")
                      id
                      (lookup i (varTypes tstate))
    _        -> annExpr e -- might not be correct due to applyFunc!

normalizeArgs :: [TAExpr] -> State TransState ([(Int,TAExpr)],[TAExpr])
normalizeArgs [] = returnS ([],[])
normalizeArgs (e:es) = case e of
  AVar _ i -> normalizeArgs es `bindS` \ (bs,nes) ->
              returnS ((i,e):bs, e:nes)
  _        -> getS `bindS` \ts ->
              let fvar = freshVar ts
                  nts  = addVarTypes [(fvar,annExpr e)] (incFreshVarIndex ts)
              in putS nts `bindS_`
                 normalizeArgs es `bindS` \ (bs,nes) ->
                 returnS ((fvar,e):bs, AVar (annExpr e) fvar : nes)


-- Get for the types (given in the first argument) fresh typed variables.
getFreshVarsForTypes :: [TypeExpr] -> State TransState [(VarIndex, TypeExpr)]
getFreshVarsForTypes types pts =
  let n     = length types
      fv    = freshVar pts
      vars  = take n [fv ..]
      tvars = zip vars types
  in (tvars, pts { freshVar = fv + n, varTypes = tvars ++ varTypes pts })


-- Rename let-bound variables in a let expression.
renameLetVars :: TransState -> [((VarIndex, TypeExpr), TAExpr)] -> TAExpr
              -> (([((VarIndex, TypeExpr), TAExpr)], TAExpr),TransState)
renameLetVars pts bindings exp =
  let args = map (fst . fst) bindings
      minarg = minimum (0 : args)
      maxarg = maximum (0 : args)
      fv     = freshVar pts
      rnm i = if i `elem` args then i - minarg + fv else i
      nargs = map (\ ((v,t),_) -> (rnm v,t)) bindings
  in ((map (\ ((v,t),be) -> ((rnm v,t), rnmAllVars rnm be)) bindings,
       rnmAllVars rnm exp),
      pts { freshVar = fv + maxarg - minarg + 1
          , varTypes = nargs ++ varTypes pts })


-- Rename free variables introduced in an expression.
renameFreeVars :: TransState -> [(VarIndex, TypeExpr)] -> TAExpr
              -> (([(VarIndex, TypeExpr)], TAExpr),TransState)
renameFreeVars pts freevars exp =
  let args = map fst freevars
      minarg = minimum (0 : args)
      maxarg = maximum (0 : args)
      fv     = freshVar pts
      rnm i = if i `elem` args then i - minarg + fv else i
      nargs = map (\ (v,t) -> (rnm v,t)) freevars
  in ((map (\ (v,t) -> (rnm v,t)) freevars, rnmAllVars rnm exp),
      pts { freshVar = fv + maxarg - minarg + 1
          , varTypes = nargs ++ varTypes pts })


-- Rename argument variables of constructor pattern
renamePatternVars :: TransState -> TABranchExpr -> (TABranchExpr,TransState)
renamePatternVars pts (ABranch p e) =
  if isConsPattern p
    then let args = map fst (patArgs p)
             minarg = minimum (0 : args)
             maxarg = maximum (0 : args)
             fv = freshVar pts
             rnm i = if i `elem` args then i - minarg + fv else i
             nargs = map (\ (v,t) -> (rnm v,t)) (patArgs p)
         in (ABranch (updPatArgs (map (\ (v,t) -> (rnm v,t))) p)
                     (rnmAllVars rnm e),
             pts { freshVar = fv + maxarg - minarg + 1
                 , varTypes = nargs ++ varTypes pts })
    else (ABranch p e, pts)


---------------------------------------------------------------------------
-- Calls the SMT solver to check whether an assertion implies some
-- property.
checkImplicationWithSMT :: Options -> IORef VState -> String -> [(Int,TypeExpr)]
                        -> Term -> Term -> Term -> IO (Maybe Bool)
checkImplicationWithSMT opts vstref scripttitle vartypes
                        assertion impbindings imp = do
  let (pretypes,usertypes) =
         partition ((== "Prelude") . fst)
                   (foldr union [] (map (tconsOfTypeExpr . snd) vartypes))
  vst <- readIORef vstref
  let allsyms = catMaybes
                  (map (\n -> maybe Nothing Just (untransOpName n))
                       (map qidName
                         (allQIdsOfTerm (tConj [assertion, impbindings, imp]))))
  unless (null allsyms) $ printWhenIntermediate opts $
    "Translating operations into SMT: " ++
    unwords (map showQName allsyms)
  smtfuncs <- funcs2SMT vstref allsyms
  let decls = map (maybe (error "Internal error: some datatype not found!") id)
                  (map (tdeclOf vst) usertypes)
      smt   = concatMap preludeType2SMT (map snd pretypes) ++
              [ EmptyLine ] ++
              (if null decls
                 then []
                 else [ Comment "User-defined datatypes:" ] ++
                      map tdecl2SMT decls) ++
              [ EmptyLine, smtfuncs, EmptyLine
              , Comment "Free variables:" ] ++
              map typedVar2SMT vartypes ++
              [ EmptyLine
              , Comment "Boolean formula of assertion (known properties):"
              , sAssert assertion, EmptyLine
              , Comment "Bindings of implication:"
              , sAssert impbindings, EmptyLine
              , Comment "Assert negated implication:"
              , sAssert (tNot imp), EmptyLine
              , Comment "check satisfiability:"
              , CheckSat
              , Comment "if unsat, the implication is valid"
              ]
  --putStrLn $ "SMT commands as Curry term:\n" ++ show smt
  smtprelude <- readFile (packagePath </> "include" </> "Prelude.smt")
  let smtinput = "; " ++ scripttitle ++ "\n\n" ++ smtprelude ++ showSMT smt
  printWhenAll opts $ "SMT SCRIPT:\n" ++ showWithLineNums smtinput
  printWhenAll opts $ "CALLING Z3 (with options: -smt2 -T:5)..."
  (ecode,out,err) <- evalCmd "z3" ["-smt2", "-in", "-T:5"] smtinput
  when (ecode>0) $ do printWhenAll opts $ "EXIT CODE: " ++ show ecode
                      writeFile "error.smt" smtinput
  printWhenAll opts $ "RESULT:\n" ++ out
  unless (null err) $ printWhenAll opts $ "ERROR:\n" ++ err
  let pcvalid = let ls = lines out in not (null ls) && head ls == "unsat"
  return (if ecode>0 then Nothing else Just pcvalid)
 where
  line = take 78 (repeat '-')

-- Operations axiomatized by specific smt scripts (no longer necessary
-- since these scripts are now automatically generated by Curry2SMT.funcs2SMT).
-- However, for future work, it might be reasonable to cache these scripts
-- for faster contract checking.
axiomatizedOps :: [String]
axiomatizedOps = ["Prelude_null","Prelude_take","Prelude_length"]

---------------------------------------------------------------------------
-- Translate a typed variables to an SMT declaration:
typedVar2SMT :: (Int,TypeExpr) -> Command
typedVar2SMT (i,te) = DeclareVar (SV i (polytype2sort te))

-- Gets all type constructors of a type expression.
tconsOfTypeExpr :: TypeExpr -> [QName]
tconsOfTypeExpr (TVar _) = []
tconsOfTypeExpr (FuncType a b) =  union (tconsOfTypeExpr a) (tconsOfTypeExpr b)
tconsOfTypeExpr (TCons qName texps) =
  foldr union [qName] (map tconsOfTypeExpr texps)
tconsOfTypeExpr (ForallType _ te) =  tconsOfTypeExpr te

---------------------------------------------------------------------------
-- Auxiliaries:

--- Tests whether the given branches of a case expressions
--- are a Boolean case distinction.
--- If yes, the expressions of the `False` and `True` branch
--- are returned.
testBoolCase :: [TABranchExpr] -> Maybe (TAExpr,TAExpr)
testBoolCase brs =
  if length brs /= 2 then Nothing
                     else case (brs!!0, brs!!1) of
    (ABranch (APattern _ (c1,_) _) e1, ABranch (APattern _ (c2,_) _) e2) ->
      if c1 == pre "False" && c2 == pre "True"  then Just (e1,e2) else
      if c1 == pre "True"  && c2 == pre "False" then Just (e2,e1) else Nothing
    _ -> Nothing

--- Shows a text with line numbers prefixed:
showWithLineNums :: String -> String
showWithLineNums txt =
  let txtlines  = lines txt
      maxlog    = ilog (length txtlines + 1)
      showNum n = (take (maxlog - ilog n) (repeat ' ')) ++ show n ++ ": "
  in unlines . map (uncurry (++)) . zip (map showNum [1..]) $ txtlines

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

{-

Still to be done:

- consider encapsulated search


Verified system libraries:

- Prelude
- Char
- Either
- ErrorState
- Integer
- Maybe
- State
- ShowS

 Prelude Char Either ErrorState Integer Maybe State ShowS

-}