| definition: |
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))
|
| demand: |
no demanded arguments |
| deterministic: |
deterministic operation |
| documentation: |
-- Generate a file for each theorem found in a module. |
| indeterministic: |
might be indeterministic |
| infix: |
no fixity defined |
| name: |
generateTheoremsForModule |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
VerifyOptions.Options -> String -> Prelude.IO () |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |