Module DSDCurryTransform

A transformation from a Curry program with pre/postconditions into a Curry program where these conditions are integrated into the code

Summary of exported operations:

dsdSourceDir :: String   
:: String   
defaultTParam :: TParam   
setStrictAssert :: TParam -> TParam   
setLazyAssert :: TParam -> TParam   
setEnforceAssert :: TParam -> TParam   
setEncapsulate :: TParam -> TParam   
withEncapsulate :: TParam -> Bool   
setSinglePostSpecs :: TParam -> TParam   
withSinglePostSpecs :: TParam -> Bool   
executeProg :: TParam -> Bool   
setExecuteProg :: TParam -> TParam   
withDebugging :: TParam -> Bool   
setDebugging :: TParam -> TParam   
checkKind :: TParam -> CExpr   
main :: IO ()   
transformedModName :: String -> String   
loadPAKCS :: TParam -> String -> IO ()   
transform :: TParam -> String -> IO ()   
isRealFuncDecl :: CFuncDecl -> Bool   
isUnknown :: [CRule] -> Bool   
copyImportModules :: TParam -> IO ()   
getFunSpecifications :: CurryProg -> [CFuncDecl]   
getPreConditions :: CurryProg -> [CFuncDecl]   
getPostConditions :: CurryProg -> [CFuncDecl]   
transformProgram :: TParam -> [CFuncDecl] -> [CFuncDecl] -> [CFuncDecl] -> [CFuncDecl] -> CurryProg -> CurryProg   
addCmtFuncInProg :: CurryProg -> CurryProg   
genFunction4Spec :: TParam -> [CFuncDecl] -> CFuncDecl -> [CFuncDecl]   
genPostCond4Spec :: TParam -> [CFuncDecl] -> [CFuncDecl] -> CFuncDecl -> [CFuncDecl]   
genFunction4PostCond :: TParam -> [CFuncDecl] -> CFuncDecl -> [CFuncDecl]   
addContract :: TParam -> [CFuncDecl] -> [CFuncDecl] -> CFuncDecl -> CFuncDecl   
getArgResultTypes :: CTypeExpr -> [CTypeExpr]   
toPolymorphicAssertTypes :: CTypeExpr -> CExpr   
toAssertTypes :: ((Int,String) -> CExpr) -> CTypeExpr -> CExpr   
transPCType :: String -> CTypeExpr -> CTypeExpr   
arityOfType :: CTypeExpr -> Int   
isSpecName :: String -> Bool   
isDetSpecName :: String -> Bool   
dropSpecName :: String -> String   
isPreCondName :: String -> Bool   
dropPreCondName :: String -> String   
isPostCondName :: String -> Bool   
dropPostCondName :: String -> String   
aMod :: a -> (String,a)   
sfMod :: a -> (String,a)   
setFun :: Int -> (String,String) -> [CExpr] -> CExpr   
genAssertInstance :: CTypeDecl -> CFuncDecl   
toLocalAssertType :: CTypeExpr -> CExpr   
resultType :: CTypeExpr -> CTypeExpr   
replaceResultType :: CTypeExpr -> CTypeExpr -> CTypeExpr   
extendFuncType :: CTypeExpr -> CTypeExpr -> CTypeExpr   
copyFileOnDemand :: String -> String -> IO ()   
Copy a file on demand, i.e., do not copy it if the target file exists with the same time stamp and size.
deleteCmt :: CFuncDecl -> CFuncDecl   
Deletes the comment in a function declaration.
deleteCmtIfEmpty :: CFuncDecl -> CFuncDecl   
Deletes the comment in a function declaration if it is the empty string.

Exported datatypes:


TParam

Constructors:

  • TParam :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> TParam

Exported operations:

dsdSourceDir :: String   

defaultTParam :: TParam   

Further infos:
  • solution complete, i.e., able to compute all solutions

setStrictAssert :: TParam -> TParam   

Further infos:
  • solution complete, i.e., able to compute all solutions

setLazyAssert :: TParam -> TParam   

Further infos:
  • solution complete, i.e., able to compute all solutions

setEnforceAssert :: TParam -> TParam   

Further infos:
  • solution complete, i.e., able to compute all solutions

setEncapsulate :: TParam -> TParam   

Further infos:
  • solution complete, i.e., able to compute all solutions

withEncapsulate :: TParam -> Bool   

Further infos:
  • solution complete, i.e., able to compute all solutions

setSinglePostSpecs :: TParam -> TParam   

Further infos:
  • solution complete, i.e., able to compute all solutions

withSinglePostSpecs :: TParam -> Bool   

Further infos:
  • solution complete, i.e., able to compute all solutions

executeProg :: TParam -> Bool   

Further infos:
  • solution complete, i.e., able to compute all solutions

setExecuteProg :: TParam -> TParam   

Further infos:
  • solution complete, i.e., able to compute all solutions

withDebugging :: TParam -> Bool   

Further infos:
  • solution complete, i.e., able to compute all solutions

setDebugging :: TParam -> TParam   

Further infos:
  • solution complete, i.e., able to compute all solutions

checkKind :: TParam -> CExpr   

main :: IO ()   

transformedModName :: String -> String   

Further infos:
  • solution complete, i.e., able to compute all solutions

loadPAKCS :: TParam -> String -> IO ()   

transform :: TParam -> String -> IO ()   

isRealFuncDecl :: CFuncDecl -> Bool   

isUnknown :: [CRule] -> Bool   

copyImportModules :: TParam -> IO ()   

genFunction4Spec :: TParam -> [CFuncDecl] -> CFuncDecl -> [CFuncDecl]   

Further infos:
  • partially defined

genPostCond4Spec :: TParam -> [CFuncDecl] -> [CFuncDecl] -> CFuncDecl -> [CFuncDecl]   

Further infos:
  • partially defined

genFunction4PostCond :: TParam -> [CFuncDecl] -> CFuncDecl -> [CFuncDecl]   

Further infos:
  • partially defined

addContract :: TParam -> [CFuncDecl] -> [CFuncDecl] -> CFuncDecl -> CFuncDecl   

Further infos:
  • partially defined

toAssertTypes :: ((Int,String) -> CExpr) -> CTypeExpr -> CExpr   

transPCType :: String -> CTypeExpr -> CTypeExpr   

arityOfType :: CTypeExpr -> Int   

isSpecName :: String -> Bool   

isDetSpecName :: String -> Bool   

dropSpecName :: String -> String   

isPreCondName :: String -> Bool   

dropPreCondName :: String -> String   

isPostCondName :: String -> Bool   

dropPostCondName :: String -> String   

aMod :: a -> (String,a)   

Further infos:
  • solution complete, i.e., able to compute all solutions

sfMod :: a -> (String,a)   

Further infos:
  • solution complete, i.e., able to compute all solutions

setFun :: Int -> (String,String) -> [CExpr] -> CExpr   

genAssertInstance :: CTypeDecl -> CFuncDecl   

Further infos:
  • partially defined

extendFuncType :: CTypeExpr -> CTypeExpr -> CTypeExpr   

Further infos:
  • solution complete, i.e., able to compute all solutions

copyFileOnDemand :: String -> String -> IO ()   

Copy a file on demand, i.e., do not copy it if the target file exists with the same time stamp and size.

deleteCmt :: CFuncDecl -> CFuncDecl   

Deletes the comment in a function declaration.

Further infos:
  • solution complete, i.e., able to compute all solutions

deleteCmtIfEmpty :: CFuncDecl -> CFuncDecl   

Deletes the comment in a function declaration if it is the empty string.