CurryInfo: contract-prover-4.0.0 / ContractProver.writeTransformedTAFCY

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