PAKCS
Exported names: Imported modules:

Module Rewriting.DefinitionalTree

Library for representation and computation of definitional trees and representation of the reduction strategy phi.

Author: Jan-Hendrik Matthes

Version: February 2020

Summary of exported operations:

dtRoot :: DefTree a -> Either Int a   
Returns the root symbol (variable or constructor) of a definitional tree.
dtPattern :: DefTree a -> Term a   
Returns the pattern of a definitional tree.
hasDefTree :: Eq a => [DefTree a] -> Term a -> Bool   
Checks whether a term has a definitional tree with the same constructor pattern in the given list of definitional trees.
selectDefTrees :: Eq a => [DefTree a] -> Term a -> [DefTree a]   
Returns a list of definitional trees with the same constructor pattern for a term from the given list of definitional trees.
fromDefTrees :: DefTree a -> Int -> [DefTree a] -> DefTree a   
Returns the definitional tree with the given index from the given list of definitional trees or the provided default definitional tree if the given index is not in the given list of definitional trees.
idtPositions :: [(Term a,Term a)] -> [[Int]]   
Returns a list of all inductive positions in a term rewriting system.
defTrees :: Eq a => [(Term a,Term a)] -> [DefTree a]   
Returns a list of definitional trees for a term rewriting system.
defTreesL :: Eq a => [[(Term a,Term a)]] -> [DefTree a]   
Returns a list of definitional trees for a list of term rewriting systems.
loDefTrees :: Eq a => [DefTree a] -> Term a -> Maybe ([Int],[DefTree a])   
Returns the position and the definitional trees from the given list of definitional trees for the leftmost outermost defined constructor in a term or Nothing if no such pair exists.
phiRStrategy :: Eq a => Int -> [(Term a,Term a)] -> Term a -> [[Int]]   
The reduction strategy phi.
dotifyDefTree :: (a -> String) -> DefTree a -> String   
Transforms a definitional tree into a graphical representation by using the DOT graph description language.
writeDefTree :: (a -> String) -> DefTree a -> String -> IO ()   
Writes the graphical representation of a definitional tree with the DOT graph description language to a file with the given filename.

Exported datatypes:

DefTree

Representation of a definitional tree, parameterized over the kind of function symbols, e.g., strings.

Constructors:

  • Leaf :: (Rule a) -> DefTree a : The leaf with rule r.
  • Branch :: (Term a) -> Pos -> [DefTree a] -> DefTree a : The branch with pattern pat, inductive position p and definitional subtrees dts.
  • Or :: (Term a) -> [DefTree a] -> DefTree a : The or node with pattern pat and definitional subtrees dts.

Exported operations:

dtRoot :: DefTree a -> Either Int a   

Returns the root symbol (variable or constructor) of a definitional tree.

dtPattern :: DefTree a -> Term a   

Returns the pattern of a definitional tree.

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

hasDefTree :: Eq a => [DefTree a] -> Term a -> Bool   

Checks whether a term has a definitional tree with the same constructor pattern in the given list of definitional trees.

selectDefTrees :: Eq a => [DefTree a] -> Term a -> [DefTree a]   

Returns a list of definitional trees with the same constructor pattern for a term from the given list of definitional trees.

fromDefTrees :: DefTree a -> Int -> [DefTree a] -> DefTree a   

Returns the definitional tree with the given index from the given list of definitional trees or the provided default definitional tree if the given index is not in the given list of definitional trees.

idtPositions :: [(Term a,Term a)] -> [[Int]]   

Returns a list of all inductive positions in a term rewriting system.

defTrees :: Eq a => [(Term a,Term a)] -> [DefTree a]   

Returns a list of definitional trees for a term rewriting system.

defTreesL :: Eq a => [[(Term a,Term a)]] -> [DefTree a]   

Returns a list of definitional trees for a list of term rewriting systems.

loDefTrees :: Eq a => [DefTree a] -> Term a -> Maybe ([Int],[DefTree a])   

Returns the position and the definitional trees from the given list of definitional trees for the leftmost outermost defined constructor in a term or Nothing if no such pair exists.

phiRStrategy :: Eq a => Int -> [(Term a,Term a)] -> Term a -> [[Int]]   

The reduction strategy phi. It uses the definitional tree with the given index for all constructor terms if possible or at least the first one.

dotifyDefTree :: (a -> String) -> DefTree a -> String   

Transforms a definitional tree into a graphical representation by using the DOT graph description language.

writeDefTree :: (a -> String) -> DefTree a -> String -> IO ()   

Writes the graphical representation of a definitional tree with the DOT graph description language to a file with the given filename.