PAKCS
Exported names: Imported modules:

Module Substitution

This module defines substitutions on type annotated FlatCurry expressions

Author: Jan Tikovsky

Version: August 2017

Summary of exported operations:

emptySubst :: Ord a => FM a b   
Create an empty substitution
singleSubst :: Ord a => a -> b -> FM a b   
Substitute a single variable by an expression
mkSubst :: Ord a => [a] -> [b] -> FM a b   
Create a substitution from a list of variables and a list of expressions
bind :: Ord a => a -> b -> FM a b -> FM a b   
Extend a substitution with the given binding
dom :: FM a b -> [a]   
Extract the domain of a given substitution
range :: FM a b -> [b]   
Extract the range of a given substitution
restrict :: Eq a => [a] -> FM a b -> FM a b   
Restrict a substitution to a given domain
findSubstWithDefault :: Ord a => b -> a -> FM a b -> b   
Find a substitution for a variable with a given default value
compose :: SubstBy a => FM Int a -> FM Int a -> FM Int a   
Compose two substitutions s1 and s2.
unify :: [(TypeExpr,TypeExpr)] -> FM Int TypeExpr   
simple unification on FlatCurry type expression
unify' :: FM Int TypeExpr -> [(TypeExpr,TypeExpr)] -> Maybe (FM Int TypeExpr)   

Exported datatypes:

Subst

Representation of substitutions

Type synonym: Subst = FM

AExpSubst

Apply a substitution to a given FlatCurry expression substitution on type annotated FlatCurry expressions

Type synonym: AExpSubst = Subst VarIndex (AExpr TypeAnn)

TypeSubst

substitution on FlatCurry type expressions

Type synonym: TypeSubst = Subst TVarIndex TypeExpr

Exported operations:

emptySubst :: Ord a => FM a b   

Create an empty substitution

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

singleSubst :: Ord a => a -> b -> FM a b   

Substitute a single variable by an expression

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

mkSubst :: Ord a => [a] -> [b] -> FM a b   

Create a substitution from a list of variables and a list of expressions

bind :: Ord a => a -> b -> FM a b -> FM a b   

Extend a substitution with the given binding

dom :: FM a b -> [a]   

Extract the domain of a given substitution

range :: FM a b -> [b]   

Extract the range of a given substitution

restrict :: Eq a => [a] -> FM a b -> FM a b   

Restrict a substitution to a given domain

findSubstWithDefault :: Ord a => b -> a -> FM a b -> b   

Find a substitution for a variable with a given default value

compose :: SubstBy a => FM Int a -> FM Int a -> FM Int a   

Compose two substitutions s1 and s2. The resulting substitution has the same effect as applying first s2 and afterwards s1 on a term

unify :: [(TypeExpr,TypeExpr)] -> FM Int TypeExpr   

simple unification on FlatCurry type expression

unify' :: FM Int TypeExpr -> [(TypeExpr,TypeExpr)] -> Maybe (FM Int TypeExpr)