Library for representation and computation of narrowings on first-order terms and representation of narrowing strategies.
Author: Jan-Hendrik Matthes
Version: November 2016
defaultNOptions
:: NOptions a
The default narrowing options. |
showNarrowing
:: (a -> String) -> Narrowing a -> String
Transforms a narrowing into a string representation. |
stdNStrategy
:: [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]
The standard narrowing strategy. |
imNStrategy
:: [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]
The innermost narrowing strategy. |
omNStrategy
:: [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]
The outermost narrowing strategy. |
loNStrategy
:: [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]
The leftmost outermost narrowing strategy. |
lazyNStrategy
:: [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]
The lazy narrowing strategy. |
wnNStrategy
:: [(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]
The weakly needed narrowing strategy. |
narrowBy
:: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [(Term a,Term a)] -> Int -> Term a -> [(FM Int (Term a),Term a)]
Narrows a term with the given strategy and term rewriting system by the given number of steps. |
narrowByL
:: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [[(Term a,Term a)]] -> Int -> Term a -> [(FM Int (Term a),Term a)]
Narrows a term with the given strategy and list of term rewriting systems by the given number of steps. |
narrowingBy
:: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [(Term a,Term a)] -> Int -> Term a -> [Narrowing a]
Returns a list of narrowings for a term with the given strategy, the given term rewriting system and the given number of steps. |
narrowingByL
:: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [[(Term a,Term a)]] -> Int -> Term a -> [Narrowing a]
Returns a list of narrowings for a term with the given strategy, the given list of term rewriting systems and the given number of steps. |
narrowingTreeBy
:: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [(Term a,Term a)] -> Int -> Term a -> NarrowingTree a
Returns a narrowing tree for a term with the given strategy, the given term rewriting system and the given number of steps. |
narrowingTreeByL
:: ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [[(Term a,Term a)]] -> Int -> Term a -> NarrowingTree a
Returns a narrowing tree for a term with the given strategy, the given list of term rewriting systems and the given number of steps. |
solveEq
:: NOptions a -> ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [(Term a,Term a)] -> Term a -> [FM Int (Term a)]
Solves a term equation with the given strategy, the given term rewriting system and the given options. |
solveEqL
:: NOptions a -> ([(Term a,Term a)] -> Term a -> [([Int],(Term a,Term a),FM Int (Term a))]) -> [[(Term a,Term a)]] -> Term a -> [FM Int (Term a)]
Solves a term equation with the given strategy, the given list of term rewriting systems and the given options. |
dotifyNarrowingTree
:: (a -> String) -> NarrowingTree a -> String
Transforms a narrowing tree into a graphical representation by using the DOT graph description language. |
writeNarrowingTree
:: (a -> String) -> NarrowingTree a -> String -> IO ()
Writes the graphical representation of a narrowing tree with the DOT graph description language to a file with the given filename. |
A narrowing strategy represented as a function that takes a term rewriting system and a term and returns a list of triples consisting of a position, a rule and a substitution, parameterized over the kind of function symbols, e.g., strings.
Type synonym: NStrategy a = TRS a -> Term a -> [(Pos,Rule a,Subst a)]
Representation of a narrowing on first-order terms, parameterized over the kind of function symbols, e.g., strings.
Constructors:
NTerm
:: (Term a) -> Narrowing a
: The narrowed term t
.
NStep
:: (Term a) -> Pos -> (Subst a) -> (Narrowing a) -> Narrowing a
: The narrowing of term t
at position p
with
substitution sub
to narrowing n
.
Representation of a narrowing tree for first-order terms, parameterized over the kind of function symbols, e.g., strings.
Constructors:
NTree
:: (Term a) -> [(Pos,Subst a,NarrowingTree a)] -> NarrowingTree a
: The narrowing of term t
to a new term with a list of
narrowing steps ns
.
Representation of narrowing options for solving term equations, parameterized over the kind of function symbols, e.g., strings.
Constructors:
NOptions
:: Bool -> (RStrategy a) -> NOptions a
Fields:
normalize
:: Bool
: Indicates whether a term should be normalized before
computing further narrowing steps.
rStrategy
:: (RStrategy a)
: The reduction strategy to normalize a term.
The default narrowing options. |
Transforms a narrowing into a string representation. |
The standard narrowing strategy. |
The innermost narrowing strategy. |
The outermost narrowing strategy. |
The leftmost outermost narrowing strategy. |
The lazy narrowing strategy. |
The weakly needed narrowing strategy. |
Narrows a term with the given strategy and term rewriting system by the given number of steps. |
Narrows a term with the given strategy and list of term rewriting systems by the given number of steps. |
Returns a list of narrowings for a term with the given strategy, the given term rewriting system and the given number of steps. |
Returns a list of narrowings for a term with the given strategy, the given list of term rewriting systems and the given number of steps. |
Returns a narrowing tree for a term with the given strategy, the given term rewriting system and the given number of steps. |
Returns a narrowing tree for a term with the given strategy, the given list of term rewriting systems and the given number of steps. |
Solves a term equation with the given strategy, the given term rewriting
system and the given options. The term has to be of the form
|
Solves a term equation with the given strategy, the given list of term
rewriting systems and the given options. The term has to be of the form
|
Transforms a narrowing tree into a graphical representation by using the DOT graph description language. |
Writes the graphical representation of a narrowing tree with the DOT graph description language to a file with the given filename. |