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  Non-deterministic 
Read and transform a module in FlatCurry format.
transformChoiceInProg :: Prog -> Prog  Deterministic 
Replace all occurrences of Prelude.? in a FlatCurry program by Or expressions.
removeTopForallType :: Prog -> Prog  Deterministic 
Remove the top-level ForallType constructors from all function signatures.
completeBranchesInFunc :: [((String,String),(Int,ConsType,[((String,String),Int)]))] -> Bool -> FuncDecl -> FuncDecl  Deterministic 
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)]))]  Deterministic 
Transforms a list of type declarations into constructor information.
consInfoOfTypeDecl :: TypeDecl -> [((String,String),(Int,ConsType,[((String,String),Int)]))]  Deterministic 
Transforms a type declaration into constructor information.
infoOfCons :: [((String,String),(Int,ConsType,[((String,String),Int)]))] -> (String,String) -> (Int,ConsType,[((String,String),Int)])  Deterministic 
Gets the the information about a given constructor name.
arityOfCons :: [((String,String),(Int,ConsType,[((String,String),Int)]))] -> (String,String) -> Int  Deterministic 
Gets the arity of a constructor from information about all constructors.
siblingsOfCons :: [((String,String),(Int,ConsType,[((String,String),Int)]))] -> (String,String) -> [((String,String),Int)]  Deterministic 
Gets the siblings of a constructor w.r.t.
isCompleteConstructorList :: [((String,String),(Int,ConsType,[((String,String),Int)]))] -> [(String,String)] -> Bool  Deterministic 
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  Deterministic 
prog2ModInfo :: Prog -> ModInfo  Deterministic 
addModInfoFor :: IORef ProgInfo -> String -> IO ()  Non-deterministic 
Read a module and adds the info for it.
hasModInfoFor :: IORef ProgInfo -> String -> IO Bool  Deterministic 
Does the info for a module with a given name already exists?
getModInfoFor :: IORef ProgInfo -> String -> IO ModInfo  Non-deterministic 
Gets the info for a module with a given name.
getFlatProgFor :: IORef ProgInfo -> String -> IO Prog  Non-deterministic 
Gets the FlatCurry program for a module with a given name.
getTypeDeclOf :: IORef ProgInfo -> (String,String) -> IO TypeDecl  Non-deterministic 
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:

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:

ModInfo

Constructors:

Exported operations:

readTransFlatCurry :: String -> IO Prog  Non-deterministic 

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  Deterministic 

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

removeTopForallType :: Prog -> Prog  Deterministic 

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

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

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)]))]  Deterministic 

Transforms a list of type declarations into constructor information.

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

Transforms a type declaration into constructor information.

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

Gets the the information about a given constructor name.

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

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

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

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

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

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  Deterministic 

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

prog2ModInfo :: Prog -> ModInfo  Deterministic 

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

Read a module and adds the info for it.

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

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

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

Gets the info for a module with a given name. If it is not already stored, read the module and store it.

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

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

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

Gets the type declaration for a given type constructor.