Module Rewriting.Position

Library for representation of positions in first-order terms.

Author: Jan-Hendrik Matthes

Version: November 2016

Summary of exported operations:

 showPos :: [Int] -> String    Transforms a position into a string representation. eps :: [Int]    The root position of a term. above :: [Int] -> [Int] -> Bool    Checks whether the first position is above the second position. below :: [Int] -> [Int] -> Bool    Checks whether the first position is below the second position. leftOf :: [Int] -> [Int] -> Bool    Checks whether the first position is left from the second position. rightOf :: [Int] -> [Int] -> Bool    Checks whether the first position is right from the second position. disjoint :: [Int] -> [Int] -> Bool    Checks whether two positions are disjoint. positions :: Term a -> [[Int]]    Returns a list of all positions in a term. (.>) :: [Int] -> [Int] -> [Int]    Concatenates two positions. (|>) :: Term a -> [Int] -> Term a    Returns the subterm of a term at the given position if the position exists within the term. replaceTerm :: Term a -> [Int] -> Term a -> Term a    Replaces the subterm of a term at the given position with the given term if the position exists within the term.

Exported datatypes:

Pos

A position in a term represented as a list of integers greater than zero.

Type synonym: Pos = [Int]

Exported operations:

 showPos :: [Int] -> String    Transforms a position into a string representation.
 eps :: [Int]    The root position of a term. Further infos: solution complete, i.e., able to compute all solutions
 above :: [Int] -> [Int] -> Bool    Checks whether the first position is above the second position.
 below :: [Int] -> [Int] -> Bool    Checks whether the first position is below the second position.
 leftOf :: [Int] -> [Int] -> Bool    Checks whether the first position is left from the second position.
 rightOf :: [Int] -> [Int] -> Bool    Checks whether the first position is right from the second position.
 disjoint :: [Int] -> [Int] -> Bool    Checks whether two positions are disjoint.
 positions :: Term a -> [[Int]]    Returns a list of all positions in a term.
 (.>) :: [Int] -> [Int] -> [Int]    Concatenates two positions. Further infos: solution complete, i.e., able to compute all solutions
 (|>) :: Term a -> [Int] -> Term a    Returns the subterm of a term at the given position if the position exists within the term. Further infos: partially defined
 replaceTerm :: Term a -> [Int] -> Term a -> Term a    Replaces the subterm of a term at the given position with the given term if the position exists within the term.