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: April 2018

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 
totalAnalysis :: Analysis Bool  Non-deterministic 
A function is totally defined if it is pattern complete and depends only on totally defined functions.
showTotally :: AOutFormat -> Bool -> String  Deterministic 
patCompAnalysis :: Analysis Completeness  Non-deterministic 
Pattern completeness analysis
showComplete :: AOutFormat -> Completeness -> String  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 

totalAnalysis :: Analysis Bool  Non-deterministic 

A function 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

patCompAnalysis :: Analysis Completeness  Non-deterministic 

Pattern completeness analysis

showComplete :: AOutFormat -> Completeness -> String  Deterministic 

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