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

definition: 
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
demand: 
no demanded arguments
deterministic: 
deterministic operation
documentation: 
-- 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.
indeterministic: 
might be indeterministic
infix: 
no fixity defined
name: 
addFailedFunc
precedence: 
no precedence defined
result-values: 
_
signature: 
Analysis.TermDomain.TermDomain a => FlatCurry.Types.Expr
-> Prelude.Maybe [(Prelude.Int, a)] -> FlatCurry.Types.Expr
-> Control.Monad.Trans.State.StateT (VerifyState a) Prelude.IO ()
solution-complete: 
operation might suspend on free variables
terminating: 
possibly non-terminating
totally-defined: 
possibly non-reducible on same data term