CurryInfo: contract-prover-4.0.0 / ContractProver.writeTransformedFCY

 
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

 no demanded arguments

 deterministic operation

 
Writes the transformed FlatCurry program together with the contents
of the auxiliary `ContractChecker` module.

 <FAILING>

 referentially transparent operation

 no fixity defined

 {(_,_,_) |-> _}

 writeTransformedFCY

 no precedence defined

 _

 ToolOptions.Options -> String -> FlatCurry.Types.Prog -> Prelude.IO ()

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term