PAKCS
Exported names: Imported modules:

Module Normalization

This module implements normalization of FlatCurry programs and expressions. This includes

  • $\alpha$-conversion (renaming of variables)
  • flattening (lifting nested applications to let bindings)
  • Ordering of let declarations in the order in which the bound variables occur in the expression.

Furthermore, a compression of expressions is implemented which simplifies expressions by

  • Removing unused variable bindings
  • Removing failing non-deterministic branches
  • Substituting variable bindings which are not shared
  • Removing failing alternatives in case expression

Author: Björn Peemöller

Version: April 2015

Summary of exported operations:

eqNorm :: Expr -> Expr -> Bool   
normalizeExpr :: Expr -> Expr   
Normalization of an expression which may contain free variables.
normalizeFreeExpr :: Expr -> Expr   
Like normalizeExpr, but unbound variables in the expression retain their indizes.
renameFreeExpr :: Expr -> Expr   
Renaming of an expression such that afterwards the variables defined in the expression are numbered from max(1, maxFreeVar + 1) upwards and the variables free in the expression retain their indizes.
renameExprSubst :: Expr -> (Expr,[(Int,Int)])   
Renaming of an expression such that the variables defined in the expression are numbered from max(1, maxFreeVar + 1) upwards and the variables free in the expression from -1 downwards.
freshResultant :: Int -> (((String,String),[Int]),Expr) -> (((String,String),[Int]),Expr)   
Create a fresh variant of a resultant by numbering all variables from i onwards.
freshRule :: Int -> Rule -> Rule   
Create a fresh variant of a rule by numbering all variables from i onwards.
renameResultant :: (((String,String),[Int]),Expr) -> (((String,String),[Int]),Expr)   
Renaming of a resultant such that the variables are numbered from 1 onwards, starting with the function's parameters.
renameFuncDecl :: FuncDecl -> FuncDecl   
Renaming of a function declaration such that the variables are numbered from 1 onwards, starting with the function's parameters.
eqRen :: Expr -> Expr -> Bool   
Are two expression equal up to a renaming of local variables?
renameExpr :: Expr -> Expr   
Renaming of an expression such that afterwards the variables defined in the expression are numbered from 1 upwards and the variables free in the expression are numbered from -1 downwards.
simplifyExpr :: Expr -> Expr   
Simplification of FlatCurry expressions.

Exported operations:

eqNorm :: Expr -> Expr -> Bool   

normalizeExpr :: Expr -> Expr   

Normalization of an expression which may contain free variables. This includes: 1) Compression of the expression (see below). 1) The order of let-bound variables and free variables is changed to the order of the occurences of the bindings in the expression. 1) Unbound variables are renumbered from -1 downwards, bound variables from 1 upwards in the order of their occurence.

normalizeFreeExpr :: Expr -> Expr   

Like normalizeExpr, but unbound variables in the expression retain their indizes.

renameFreeExpr :: Expr -> Expr   

Renaming of an expression such that afterwards the variables defined in the expression are numbered from max(1, maxFreeVar + 1) upwards and the variables free in the expression retain their indizes.

renameExprSubst :: Expr -> (Expr,[(Int,Int)])   

Renaming of an expression such that the variables defined in the expression are numbered from max(1, maxFreeVar + 1) upwards and the variables free in the expression from -1 downwards. The resulting substitution contains the mapping from the former unbound variables to the latter unbound variables.

freshResultant :: Int -> (((String,String),[Int]),Expr) -> (((String,String),[Int]),Expr)   

Create a fresh variant of a resultant by numbering all variables from i onwards.

freshRule :: Int -> Rule -> Rule   

Create a fresh variant of a rule by numbering all variables from i onwards.

renameResultant :: (((String,String),[Int]),Expr) -> (((String,String),[Int]),Expr)   

Renaming of a resultant such that the variables are numbered from 1 onwards, starting with the function's parameters.

renameFuncDecl :: FuncDecl -> FuncDecl   

Renaming of a function declaration such that the variables are numbered from 1 onwards, starting with the function's parameters.

eqRen :: Expr -> Expr -> Bool   

Are two expression equal up to a renaming of local variables?

renameExpr :: Expr -> Expr   

Renaming of an expression such that afterwards the variables defined in the expression are numbered from 1 upwards and the variables free in the expression are numbered from -1 downwards.

simplifyExpr :: Expr -> Expr   

Simplification of FlatCurry expressions. This consists of the following steps:

  • Locally introduces free variables that are not used are removed.
  • Or applied to failed is reduced to the alternative expression.
  • If Or is applied to two calls to cond sharing the same first condition, the condition is lifted above the Or construct.
  • If Or is applied to two case expressions scrutinizing the same expression, the case expression is lifted upwards and the corresponding branches are combined using Or.
  • Case branches directly calling failed are removed. If all branches are removed, the expression is reduced to failed instead.
  • Evaluation annotations SQ e are moved downwards until a potentially evaluable expression in encountered.
  • Let-bindings which refer to another variable or are only used once are inserted and removed afterwards.
  • Unused let-bindings are removed.