Module FlatCurry.Annotated.TypeSubst

Type substitutions on type-annotated AnnotatedFlatCurry

Author: Bjoern Peemoeller

Version: September 2014

Summary of exported operations:

showAFCSubst :: Map Int TypeExpr -> String   
emptyAFCSubst :: Map Int TypeExpr   
The empty substitution
lookupAFCSubst :: Map Int TypeExpr -> Int -> Maybe TypeExpr   
Searches the substitution for a mapping from the given variable index to a term.
substFunc :: Map Int TypeExpr -> AFuncDecl TypeExpr -> AFuncDecl TypeExpr   
Applies a substitution to a function.
substRule :: Map Int TypeExpr -> ARule TypeExpr -> ARule TypeExpr   
Applies a substitution to a type expression.
substExpr :: Map Int TypeExpr -> AExpr TypeExpr -> AExpr TypeExpr   
Applies a substitution to a type expression.
substSnd :: Map Int TypeExpr -> (a,TypeExpr) -> (a,TypeExpr)   
substBranch :: Map Int TypeExpr -> ABranchExpr TypeExpr -> ABranchExpr TypeExpr   
Applies a substitution to a branch expression.
substPattern :: Map Int TypeExpr -> APattern TypeExpr -> APattern TypeExpr   
Applies a substitution to a pattern.
subst :: Map Int TypeExpr -> TypeExpr -> TypeExpr   
Looks up a type in a substitution and converts the resulting Term to a TypeExpr.

Exported datatypes:


AFCSubst

The (abstract) data type for substitutions on TypeExpr.

Type synonym: AFCSubst = Map TVarIndex TypeExpr


Exported operations:

showAFCSubst :: Map Int TypeExpr -> String   

emptyAFCSubst :: Map Int TypeExpr   

The empty substitution

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

lookupAFCSubst :: Map Int TypeExpr -> Int -> Maybe TypeExpr   

Searches the substitution for a mapping from the given variable index to a term.

Example call:
(lookupAFCSubst subst i)
Parameters:
  • subst : the substitution to search
  • i : the index to search for
Returns:
the found type expression or Nothing

substFunc :: Map Int TypeExpr -> AFuncDecl TypeExpr -> AFuncDecl TypeExpr   

Applies a substitution to a function.

Example call:
(substFunc sub f)
Parameters:
  • sub : the substitution
  • f : the function
Returns:
the function with the substitution applied

substRule :: Map Int TypeExpr -> ARule TypeExpr -> ARule TypeExpr   

Applies a substitution to a type expression.

Example call:
(substRule sub r)
Parameters:
  • sub : the substitution
  • r : the rule
Returns:
the rule with the substitution applied

substExpr :: Map Int TypeExpr -> AExpr TypeExpr -> AExpr TypeExpr   

Applies a substitution to a type expression.

Example call:
(substExpr sub ex)
Parameters:
  • sub : the substitution
  • ex : the expression
Returns:
the expression with the substitution applied

substSnd :: Map Int TypeExpr -> (a,TypeExpr) -> (a,TypeExpr)   

substBranch :: Map Int TypeExpr -> ABranchExpr TypeExpr -> ABranchExpr TypeExpr   

Applies a substitution to a branch expression.

Example call:
(substBranch sub b)
Parameters:
  • sub : the substitution
  • b : the branch
Returns:
the branch with the substitution applied

substPattern :: Map Int TypeExpr -> APattern TypeExpr -> APattern TypeExpr   

Applies a substitution to a pattern.

Example call:
(substPattern sub p)
Parameters:
  • sub : the substitution
  • p : the pattern
Returns:
the pattern with the substitution applied

subst :: Map Int TypeExpr -> TypeExpr -> TypeExpr   

Looks up a type in a substitution and converts the resulting Term to a TypeExpr. Returns a given default value if the lookup fails.

Example call:
(subst t e sub)
Parameters:
  • t : the type to look up
  • e : the default value
  • sub : the substitution to search in
Returns:
either the looked-up and converted type or the default type