CurryInfo: verify-3.1.0 / ToVerifier.generateTheoremsForModule

 
generateTheoremsForModule :: Options -> String -> IO ()
generateTheoremsForModule opts mname = do
  prog <- readCurry mname
  let propNames = map funcName (filter isProperty (functions prog))
      optNames  = nub (filter (\ (mn,_) -> null mn || mn == progName prog)
                              (optTheorems opts))
  if null optNames
   then if null propNames
        then putStrLn $ "No properties found in module `"++mname++"'!"
        else generateTheorems opts { optTheorems = propNames}
   else let qnames = map (\ (mn,pn) ->
                            (if null mn then progName prog else mn, pn))
                         optNames
         in if all (`elem` propNames) qnames
             then generateTheorems (opts { optTheorems = qnames })
             else error $ unwords ("Properties not found:" :
                                   map (\ (mn,pn) -> '`':mn++"."++pn++"'")
                                       (filter (`notElem` propNames) qnames))

 no demanded arguments

 deterministic operation

 
Generate a file for each theorem found in a module.

 might be indeterministic

 no fixity defined

 {(_,_) |-> _}

 generateTheoremsForModule

 no precedence defined

 _

 VerifyOptions.Options -> String -> Prelude.IO ()

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term