| definition: |
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 '-')
|
| demand: |
no demanded arguments |
| deterministic: |
deterministic operation |
| indeterministic: |
might be indeterministic |
| infix: |
no fixity defined |
| name: |
verifyFuncRule |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
Analysis.TermDomain.TermDomain a => [Prelude.Int] -> FlatCurry.Types.TypeExpr -> 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 |