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: November 2024

Summary of exported operations:

showSibling :: AOutFormat -> [((String,String),Int)] -> String  Deterministic 
An analysis to compute the sibling constructors (belonging to the same data type) for a data constructor.
siblingCons :: Analysis [((String,String),Int)]  Deterministic 
showSiblingAndDecl :: AOutFormat -> (TypeDecl,[((String,String),Int)]) -> String  Deterministic 
An analysis to compute the sibling constructors (belonging to the same data type) and type declaration for a data constructor.
siblingConsAndDecl :: Analysis (TypeDecl,[((String,String),Int)])  Deterministic 
patCompAnalysis :: Analysis Completeness  Non-deterministic 
Pattern completeness analysis
showComplete :: AOutFormat -> Completeness -> String  Deterministic 
totalAnalysis :: Analysis Bool  Non-deterministic 
An operation is totally defined if it is pattern complete and depends only on totally defined functions.
showTotally :: AOutFormat -> Bool -> String  Deterministic 
showTotalFunc :: AOutFormat -> Bool -> String  Deterministic 
totalFuncAnalysis :: Analysis Bool  Non-deterministic 
An operation is totally and functionally defined if it is totally defined and functionally defined (see Analysis.Deterministic).

Exported datatypes:

Completeness

Constructors:

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

Exported operations:

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

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

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

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

patCompAnalysis :: Analysis Completeness  Non-deterministic 

Pattern completeness analysis

showComplete :: AOutFormat -> Completeness -> String  Deterministic 

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

totalAnalysis :: Analysis Bool  Non-deterministic 

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

showTotally :: AOutFormat -> Bool -> String  Deterministic 

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

showTotalFunc :: AOutFormat -> Bool -> String  Deterministic 

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

totalFuncAnalysis :: Analysis Bool  Non-deterministic 

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.