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