Module Rewriting.DefinitionalTree

dtRoot :: DefTree a -> Either Int a   

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

Further infos:

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

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.