CurryInfo: verify-non-fail-2.0.0 / Main.verifyNonTrivFuncCall

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)

no demanded arguments

deterministic operation

-- 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.

might be indeterministic

no fixity defined

verifyNonTrivFuncCall

no precedence defined

_

Analysis.TermDomain.TermDomain a => FlatCurry.Types.Expr -> (String, String)
-> [Prelude.Int] -> Prelude.Maybe [a]
-> Prelude.Maybe ([(Prelude.Int, FlatCurry.Types.TypeExpr)], FlatCurry.Types.Expr)
-> Control.Monad.Trans.State.StateT (VerifyState a) Prelude.IO ()

operation might suspend on free variables

possibly non-terminating

possibly non-reducible on same data term