Module Rewriting.Position

Library for representation of positions in first-order terms.

Author: Jan-Hendrik Matthes

Version: February 2020

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.

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.