PAKCS
Exported names: Imported modules:

Module TypedFlatCurryGoodies

Some goodies to deal with type-annotated FlatCurry programs.

Author: Michael Hanus

Version: April 2018

Summary of exported operations:

readTypedFlatCurry :: String -> IO (AProg TypeExpr)   
Reads a typed FlatCurry program or exits with a failure message in case of some typing error.
readTypedFlatCurryWithSpec :: Options -> String -> IO (AProg TypeExpr)   
Reads a typed FlatCurry program together with a possible _SPEC program (containing further contracts) or exits with a failure message in case of some typing error.
unionTAProg :: AProg TypeExpr -> AProg TypeExpr -> AProg TypeExpr   
Returns the union of two typed FlatCurry programs.
getAllFunctions :: IORef VState -> [AFuncDecl TypeExpr] -> [(String,String)] -> IO [AFuncDecl TypeExpr]   
Extract all user-defined typed FlatCurry functions that might be called by a given list of functions.
funcsOfFuncDecl :: AFuncDecl TypeExpr -> [(String,String)]   
Returns the names of all functions/constructors occurring in the body of a function declaration.
ndExpr :: AExpr TypeExpr -> Bool   
Returns True if the expression is non-deterministic, i.e., if Or or Free occurs in the expression.
ppTAExpr :: AExpr TypeExpr -> String   
Pretty prints an expression.
setAnnPattern :: TypeExpr -> APattern TypeExpr -> APattern TypeExpr   
Sets the top annotation of a pattern.
isPrimOp :: (String,String) -> Bool   
Is a qualified FlatCurry name primitive?
preludePrimOps :: [(String,String)]   
Primitive operations of the prelude and their SMT names.
primCons :: [(String,String)]   
Primitive constructors from the prelude and their SMT names.
standardConstructors :: [(String,String)]   
etaExpandFuncDecl :: AFuncDecl TypeExpr -> AFuncDecl TypeExpr   
Eta-expansion of user-defined function declarations.
pre :: String -> (String,String)   
showQName :: (String,String) -> String   

Exported datatypes:

TAProg

Type synonym: TAProg = AProg TypeExpr

TAFuncDecl

Type synonym: TAFuncDecl = AFuncDecl TypeExpr

TARule

Type synonym: TARule = ARule TypeExpr

TAExpr

Type synonym: TAExpr = AExpr TypeExpr

TABranchExpr

Type synonym: TABranchExpr = ABranchExpr TypeExpr

TAPattern

Type synonym: TAPattern = APattern TypeExpr

Exported operations:

readTypedFlatCurry :: String -> IO (AProg TypeExpr)   

Reads a typed FlatCurry program or exits with a failure message in case of some typing error.

readTypedFlatCurryWithSpec :: Options -> String -> IO (AProg TypeExpr)   

Reads a typed FlatCurry program together with a possible _SPEC program (containing further contracts) or exits with a failure message in case of some typing error.

unionTAProg :: AProg TypeExpr -> AProg TypeExpr -> AProg TypeExpr   

Returns the union of two typed FlatCurry programs.

getAllFunctions :: IORef VState -> [AFuncDecl TypeExpr] -> [(String,String)] -> IO [AFuncDecl TypeExpr]   

Extract all user-defined typed FlatCurry functions that might be called by a given list of functions.

funcsOfFuncDecl :: AFuncDecl TypeExpr -> [(String,String)]   

Returns the names of all functions/constructors occurring in the body of a function declaration.

ndExpr :: AExpr TypeExpr -> Bool   

Returns True if the expression is non-deterministic, i.e., if Or or Free occurs in the expression.

ppTAExpr :: AExpr TypeExpr -> String   

Pretty prints an expression.

setAnnPattern :: TypeExpr -> APattern TypeExpr -> APattern TypeExpr   

Sets the top annotation of a pattern.

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

isPrimOp :: (String,String) -> Bool   

Is a qualified FlatCurry name primitive?

preludePrimOps :: [(String,String)]   

Primitive operations of the prelude and their SMT names.

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

primCons :: [(String,String)]   

Primitive constructors from the prelude and their SMT names.

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

standardConstructors :: [(String,String)]   

etaExpandFuncDecl :: AFuncDecl TypeExpr -> AFuncDecl TypeExpr   

Eta-expansion of user-defined function declarations.

pre :: String -> (String,String)   

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

showQName :: (String,String) -> String   

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