Library for representation and computation of definitional trees and representation of the reduction strategy phi.
Author: JanHendrik Matthes
Version: February 2020
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. 
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
.
Returns the root symbol (variable or constructor) of a definitional tree.

Returns the pattern of a definitional tree.

Checks whether a term has a definitional tree with the same constructor pattern in the given list of definitional trees. 
Returns a list of definitional trees with the same constructor pattern for a term from the given list of definitional trees. 
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. 
Returns a list of all inductive positions in a term rewriting system. 
Returns a list of definitional trees for a term rewriting system. 
Returns a list of definitional trees for a list of term rewriting systems. 
Returns the position and the definitional trees from the given list of
definitional trees for the leftmost outermost defined constructor in a
term or 
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. 
Transforms a definitional tree into a graphical representation by using the DOT graph description language. 
Writes the graphical representation of a definitional tree with the DOT graph description language to a file with the given filename. 