|
definition:
|
simplifyPostConditionsWithTheorems :: Int -> [CFuncDecl] -> [CFuncDecl]
-> IO [CFuncDecl]
simplifyPostConditionsWithTheorems verb theofuncs postconds = do
theoTRS <- mapM safeFromFuncDecl theofuncs >>= return . concat
if null theoTRS
then return postconds
else do
let simprules = concatMap theoremToSimpRules theoTRS ++ standardSimpRules
when (verb>1) $ putStr $ unlines
[ "THEOREMS (with existing proof files):", showTRS snd theoTRS,
"SIMPLIFICATION RULES (for postcondition reduction):"
, showTRS snd simprules]
simppostconds <- mapM (safeSimplifyPostCondition verb simprules) postconds
return (concat simppostconds)
where
safeFromFuncDecl fd =
catch (return $!! (snd (fromFuncDecl fd)))
(\e -> do
putStrLn $ show e ++ "\nTheorem \"" ++
snd (funcName fd) ++
"\" not used for simplification (too complex)."
return [])
|
|
demand:
|
no demanded arguments
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
-- Simplify the postconditions contained in the third argument w.r.t. a given
-- list of theorems (second argument).
-- If the verbosity (first argument) is greater than 1, the details
-- about the theorems, simplifcation rules, and reduced postconditions
-- are shown.
|
|
failfree:
|
<FAILING>
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{(_,_,_) |-> _}
|
|
name:
|
simplifyPostConditionsWithTheorems
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
Prelude.Int -> [AbstractCurry.Types.CFuncDecl]
-> [AbstractCurry.Types.CFuncDecl] -> Prelude.IO [AbstractCurry.Types.CFuncDecl]
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
possibly non-reducible on same data term
|