CurryInfo: verify-non-fail-2.0.0 / Verify.Statistics.showStatistics

showStatistics :: TermDomain a => Options -> Int -> Int -> (QName -> Bool)
               -> Int -> Int -> (Int,Int)
               -> (Int,Int) -> [(QName, ACallType a)] -> [QName]
               -> (Int,Int,Int) -> (String, [String])
showStatistics opts vtime numits isvisible numvisfuncs numallfuncs
               (numpubiotypes, numalliotypes)
               (numpubcalltypes, numallcalltypes)
               ntfinalcts withnonfailconds (numcalls, numcases, numunsats) =
  ( unlines $
      [ "Functions                      (public / all): " ++
        show numvisfuncs ++ " / " ++ show numallfuncs
      , "Non-trivial input/output types (public / all): " ++
        show numpubiotypes ++ " / " ++ show numalliotypes
      , "Initial non-trivial call types (public / all): " ++
        show numpubcalltypes ++ " / " ++ show numallcalltypes ] ++
      (if optVerify opts
         then [ "Final non-trivial call types   (public / all): " ++
                show numpubntfinalcts ++ " / " ++ show numallntfinalcts
              , "Final non-fail conditions      (public / all): " ++
                show numpubnfconds ++ " / " ++ show numallnfconds
              , "Final failing call types       (public / all): " ++
                show numfailpubcts ++ " / " ++ show numfailallcts
              , "Non-trivial function calls checked (total)   : " ++
                show numcalls
              , "Non-trivial function calls checked by SMT    : " ++
                show numunsats
              , "Incomplete case expressions checked          : " ++
                show numcases
              , "Number of iterations for call-type inference : " ++
                show numits
              , "Total verification in msecs                  : " ++
                show vtime ]
         else [])
  , map show [ numvisfuncs, numallfuncs, numpubiotypes, numalliotypes
             , numpubcalltypes, numallcalltypes
             , numpubntfinalcts, numallntfinalcts
             , numpubnfconds, numallnfconds
             , numfailpubcts, numfailallcts
             , numcalls, numunsats, numcases, numits, vtime ]
  )
 where
  ntfinalpubcts    = filter (isvisible . fst) ntfinalcts
  numallntfinalcts = length ntfinalcts - numallnfconds
  numpubntfinalcts = length ntfinalpubcts - numpubnfconds
  numallnfconds    = length withnonfailconds
  numpubnfconds    = length (filter isvisible withnonfailconds)
  numfailallcts    = length (filter (isFailACallType . snd) ntfinalcts)
                     - numallnfconds
  numfailpubcts    = length (filter (isFailACallType . snd) ntfinalpubcts)
                     - numpubnfconds

arguments 8 9 12

deterministic operation

-- Show statistics in textual and in CSV format:

(_, _, _, _, _, _, _, _, _, _, _, _)

referentially transparent operation

no fixity defined

{(_,_,_,_,_,_,_,{(,)},{(,)},_,_,{(,,)}) |-> {(,)}}

showStatistics

no precedence defined

{(,)}

Analysis.TermDomain.TermDomain a => Verify.Options.Options -> Prelude.Int
-> Prelude.Int -> ((String, String) -> Prelude.Bool) -> Prelude.Int
-> Prelude.Int -> (Prelude.Int, Prelude.Int) -> (Prelude.Int, Prelude.Int)
-> [((String, String), Prelude.Maybe [a])] -> [(String, String)]
-> (Prelude.Int, Prelude.Int, Prelude.Int) -> (String, [String])

operation might suspend on free variables

possibly non-terminating

possibly non-reducible on same data term