Module FlatCurry.Typed.Read

Some operations to read type-annotated FlatCurry programs.

Author: Michael Hanus

Version: May 2021

Summary of exported operations:

readSimpTypedFlatCurryWithSpec :: String -> StateT VState IO (AProg TypeExpr)  Non-deterministic 
Reads a typed FlatCurry program together with a possible _SPEC program (containing further contracts) and simplify some expressions (see module FlatCurry.Typed.Simplify).
readTypedFlatCurryWithSpec :: String -> StateT VState IO (AProg TypeExpr)  Non-deterministic 
Reads a typed FlatCurry program together with a possible _SPEC program (containing further contracts).
readTypedFlatCurryFromPath :: String -> String -> IO (Maybe (AProg TypeExpr))  Non-deterministic 
Reads a typed FlatCurry program from the load path or the given path.
readTypedFlatCurryWithoutForall :: String -> IO (AProg TypeExpr)  Non-deterministic 
Reads a typed FlatCurry program and remove all leading ForallType quantifiers from function signatures.
stripForall :: TypeExpr -> TypeExpr  Deterministic 
getAllFunctions :: [AFuncDecl TypeExpr] -> [(String,String)] -> StateT VState IO [AFuncDecl TypeExpr]  Non-deterministic 
Extract all user-defined typed FlatCurry functions that might be called by a given list of functions.

Exported operations:

readSimpTypedFlatCurryWithSpec :: String -> StateT VState IO (AProg TypeExpr)  Non-deterministic 

Reads a typed FlatCurry program together with a possible _SPEC program (containing further contracts) and simplify some expressions (see module FlatCurry.Typed.Simplify).

readTypedFlatCurryWithSpec :: String -> StateT VState IO (AProg TypeExpr)  Non-deterministic 

Reads a typed FlatCurry program together with a possible _SPEC program (containing further contracts). All leading ForallType quantifiers are removed from function signatures since they are not relevant here.

readTypedFlatCurryFromPath :: String -> String -> IO (Maybe (AProg TypeExpr))  Non-deterministic 

Reads a typed FlatCurry program from the load path or the given path. All leading ForallType quantifiers are removed from function signatures.

readTypedFlatCurryWithoutForall :: String -> IO (AProg TypeExpr)  Non-deterministic 

Reads a typed FlatCurry program and remove all leading ForallType quantifiers from function signatures.

getAllFunctions :: [AFuncDecl TypeExpr] -> [(String,String)] -> StateT VState IO [AFuncDecl TypeExpr]  Non-deterministic 

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