| definition: |
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 printInfoLine $ "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))
printInfoLine $ "Function '" ++ f ++ "':"
printInfoLine $ "In/out type: " ++ showIOT iot
printInfoLine $ "Call type : " ++ prettyFunCallAType ctype
maybe (return ())
(\nfc -> printInfoLine $ showConditions fdecls [(qf,nfc)])
(lookup qf (vstFunConds vst))
|
| demand: |
no demanded arguments |
| deterministic: |
deterministic operation |
| documentation: |
-- Shows the call and in/out type of a given function defined in the module. |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| name: |
showFunctionInfo |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
Analysis.TermDomain.TermDomain a => Verify.Options.Options -> String -> 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 |