Module Analysis.TotallyDefined
- Exported Datatypes
- Exported Functions
Imported modules:

Module Analysis.TotallyDefined

Pattern completeness and totally definedness analysis for Curry programs

This analysis checks for each function in a Curry program whether this function is completely defined, i.e., reducible on all ground constructor terms

Author

Johannes Koj, Michael Hanus

Version

February 2025

Exported Datatypes:

Completeness

Exported Functions:

patCompAnalysis showComplete showSibling showSiblingAndDecl showTotalFunc showTotally siblingCons siblingConsAndDecl totalAnalysis totalFuncAnalysis

Exported Datatypes

data Completeness

Constructors:

Complete :: Completeness
InComplete :: Completeness
InCompleteOr :: Completeness

Known instances:

ReadWrite Completeness
Eq Completeness
Show Completeness
Read Completeness

Exported Functions

showSibling :: AOutFormat -> [((String, String), Int)] -> String

An analysis to compute the sibling constructors (belonging to the same data type) for a data constructor. Shows the result of the sibling constructors analysis, i.e., shows a list of constructor names together with their arities.

siblingCons :: Analysis [((String, String), Int)]

showSiblingAndDecl :: AOutFormat -> (TypeDecl, [((String, String), Int)]) -> String

An analysis to compute the sibling constructors (belonging to the same data type) and type declaration for a data constructor. Shows the result of the sibling constructors analysis, i.e., shows a tuple of a type declaration and a list of constructor names together with their arities.

siblingConsAndDecl :: Analysis (TypeDecl, [((String, String), Int)])

patCompAnalysis :: Analysis Completeness

Pattern completeness analysis

showComplete :: AOutFormat -> Completeness -> String

Further infos:

solution complete, i.e., able to compute all solutions

totalAnalysis :: Analysis Bool

An operation is totally defined if it is pattern complete and depends only on totally defined functions.

showTotally :: AOutFormat -> Bool -> String

Further infos:

solution complete, i.e., able to compute all solutions

showTotalFunc :: AOutFormat -> Bool -> String

Further infos:

solution complete, i.e., able to compute all solutions

totalFuncAnalysis :: Analysis Bool

An operation is totally and functionally defined if it is totally defined and functionally defined (see Analysis.Deterministic). Thus, it is defined without any pattern failures in the sense of purely functional programming.