CurryInfo: contract-prover-4.0.0 / ContractProver.writeTransformedFCY

definition:
writeTransformedFCY :: Options -> String -> Prog -> IO ()
writeTransformedFCY opts progfile prog = do
  ccpath <- getContractCheckerModulePath
  ccprog <- runModuleActionQuiet readFlatCurry ccpath
  let rnmccprog = FCG.rnmProg (FCG.progName prog) ccprog
      ccimps    = FCG.progImports rnmccprog
      ccfuncs   = FCG.progFuncs rnmccprog
  writeFCY progfile
           (FCG.updProgFuncs (++ ccfuncs)
                             (FCG.updProgImports (`union` ccimps) prog))
  printWhenStatus opts $ "Transformed program written to: " ++ progfile
demand:
no demanded arguments
deterministic:
deterministic operation
documentation:
-- Writes the transformed FlatCurry program together with the contents
-- of the auxiliary `ContractChecker` module.
failfree:
<FAILING>
indeterministic:
referentially transparent operation
infix:
no fixity defined
iotype:
{(_,_,_) |-> _}
name:
writeTransformedFCY
precedence:
no precedence defined
result-values:
_
signature:
ToolOptions.Options -> String -> FlatCurry.Types.Prog -> Prelude.IO ()
solution-complete:
operation might suspend on free variables
terminating:
possibly non-terminating
totally-defined:
possibly non-reducible on same data term