Exported names:
- Datatypes:
- ConsInfo
- ConsType
- ModInfo
- ProgInfo
- Constructors:
- ConsType
- ModInfo
- ProgInfo
- Fields:
- miCInfos
- miFTypes
- miProg
- progInfos
- Operations:
- addModInfoFor
- arityOfCons
- completeBranchesInFunc
- consInfoOfTypeDecl
- consInfoOfTypeDecls
- emptyProgInfo
- getFlatProgFor
- getModInfoFor
- getTypeDeclOf
- hasModInfoFor
- infoOfCons
- isCompleteConstructorList
- prog2ModInfo
- readTransFlatCurry
- removeTopForallType
- siblingsOfCons
- transformChoiceInProg
Imported modules:

Module Verify.ProgInfo

This module contains the definition and operations for a state containing information about already loaded FlatCurry programs. The state is used during the execution of the tool in order to avoid multiple loading of FlatCurry programs.

Author: Michael Hanus

Version: March 2024

Summary of exported operations:

readTransFlatCurry
                  ::  String -> IO Prog

Read and transform a module in FlatCurry format.

transformChoiceInProg
                  ::  Prog -> Prog

Replace all occurrences of Prelude.? in a FlatCurry program by Or expressions.

removeTopForallType
                  ::  Prog -> Prog

Remove the top-level ForallType constructors from all function signatures.

completeBranchesInFunc
                  ::  [((String,String),(Int,ConsType,[((String,String),Int)]))] -> Bool -> FuncDecl -> FuncDecl

Complete all partial case branches occurring in the body of a function by adding Prelude.failed branches.

consInfoOfTypeDecls
                  ::  [TypeDecl] -> [((String,String),(Int,ConsType,[((String,String),Int)]))]

Transforms a list of type declarations into constructor information.

consInfoOfTypeDecl
                  ::  TypeDecl -> [((String,String),(Int,ConsType,[((String,String),Int)]))]

Transforms a type declaration into constructor information.

infoOfCons
                  ::  [((String,String),(Int,ConsType,[((String,String),Int)]))] -> (String,String) -> (Int,ConsType,[((String,String),Int)])

Gets the the information about a given constructor name.

arityOfCons
                  ::  [((String,String),(Int,ConsType,[((String,String),Int)]))] -> (String,String) -> Int

Gets the arity of a constructor from information about all constructors.

siblingsOfCons
                  ::  [((String,String),(Int,ConsType,[((String,String),Int)]))] -> (String,String) -> [((String,String),Int)]

Gets the siblings of a constructor w.r.t.

isCompleteConstructorList
                  ::  [((String,String),(Int,ConsType,[((String,String),Int)]))] -> [(String,String)] -> Bool

Is a non-empty list of constructors complete, i.e., does it contain all the constructors of a type? The first argument contains information about all constructors in a program.

emptyProgInfo
                  ::  ProgInfo

prog2ModInfo
                  ::  Prog -> ModInfo

addModInfoFor
                  ::  IORef ProgInfo -> String -> IO ()

Read a module and adds the info for it.

hasModInfoFor
                  ::  IORef ProgInfo -> String -> IO Bool

Does the info for a module with a given name already exists?

getModInfoFor
                  ::  IORef ProgInfo -> String -> IO ModInfo

Gets the info for a module with a given name.

getFlatProgFor
                  ::  IORef ProgInfo -> String -> IO Prog

Gets the FlatCurry program for a module with a given name.

getTypeDeclOf
                  ::  IORef ProgInfo -> (String,String) -> IO TypeDecl

Gets the type declaration for a given type constructor.

Exported datatypes:

ConsInfo

The information about a constructor consists of the arity, type, and the siblings of the constructor. The siblings are represented as pairs of the qualified constructor name and their arity.

Type synonym: ConsInfo = (Int,ConsType,[(QName,Int)])

ConsType

The type of a constructor consists of the argument types, the type constructor and the type parameters of the constructor.

Constructors:

ConsType :: [TypeExpr] -> QName -> [Int] -> ConsType

ProgInfo

The global program information is a mapping from module names to infos about the module. The main program keeps an IORef to this structure.

Constructors:

ProgInfo :: [(String,ModInfo)] -> ProgInfo
Fields:
- progInfos :: [(String,ModInfo)]

ModInfo

Constructors:

ModInfo :: Prog -> (Map String TypeExpr) -> (Map String ConsInfo) -> ModInfo
Fields:
- miProg :: Prog
- miFTypes :: (Map String TypeExpr)
- miCInfos :: (Map String ConsInfo)

Exported operations:

readTransFlatCurry :: String -> IO Prog

Read and transform a module in FlatCurry format. In particular, occurrences of Prelude.? are transformed into Or expressions and top-level Forall quantifiers are removed in function signatures.

transformChoiceInProg :: Prog -> Prog

Replace all occurrences of Prelude.? in a FlatCurry program by Or expressions.

removeTopForallType :: Prog -> Prog

Remove the top-level ForallType constructors from all function signatures.

completeBranchesInFunc :: [((String,String),(Int,ConsType,[((String,String),Int)]))] -> Bool -> FuncDecl -> FuncDecl

Complete all partial case branches occurring in the body of a function by adding Prelude.failed branches. The first argument contains all data constructors grouped by their data type. If the second argument is True, only a single branch with an anonymous pattern is added (if necessary), otherwise branches for all missing patterns are added.

consInfoOfTypeDecls :: [TypeDecl] -> [((String,String),(Int,ConsType,[((String,String),Int)]))]

Transforms a list of type declarations into constructor information.

consInfoOfTypeDecl :: TypeDecl -> [((String,String),(Int,ConsType,[((String,String),Int)]))]

Transforms a type declaration into constructor information.

infoOfCons :: [((String,String),(Int,ConsType,[((String,String),Int)]))] -> (String,String) -> (Int,ConsType,[((String,String),Int)])

Gets the the information about a given constructor name.

arityOfCons :: [((String,String),(Int,ConsType,[((String,String),Int)]))] -> (String,String) -> Int

Gets the arity of a constructor from information about all constructors.

Further infos:

partially defined

siblingsOfCons :: [((String,String),(Int,ConsType,[((String,String),Int)]))] -> (String,String) -> [((String,String),Int)]

Gets the siblings of a constructor w.r.t. constructor information.

isCompleteConstructorList :: [((String,String),(Int,ConsType,[((String,String),Int)]))] -> [(String,String)] -> Bool

Is a non-empty list of constructors complete, i.e., does it contain all the constructors of a type? The first argument contains information about all constructors in a program.

Further infos: