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  Deterministic 
Transforms a position into a string representation.
eps :: [Int]  Deterministic 
The root position of a term.
above :: [Int] -> [Int] -> Bool  Deterministic 
Checks whether the first position is above the second position.
below :: [Int] -> [Int] -> Bool  Deterministic 
Checks whether the first position is below the second position.
leftOf :: [Int] -> [Int] -> Bool  Deterministic 
Checks whether the first position is left from the second position.
rightOf :: [Int] -> [Int] -> Bool  Deterministic 
Checks whether the first position is right from the second position.
disjoint :: [Int] -> [Int] -> Bool  Deterministic 
Checks whether two positions are disjoint.
positions :: Term a -> [[Int]]  Deterministic 
Returns a list of all positions in a term.
(.>) :: [Int] -> [Int] -> [Int]  Deterministic 
Concatenates two positions.
(|>) :: Term a -> [Int] -> Term a  Deterministic 
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  Deterministic 
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  Deterministic 

Transforms a position into a string representation.

eps :: [Int]  Deterministic 

The root position of a term.

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

above :: [Int] -> [Int] -> Bool  Deterministic 

Checks whether the first position is above the second position.

below :: [Int] -> [Int] -> Bool  Deterministic 

Checks whether the first position is below the second position.

leftOf :: [Int] -> [Int] -> Bool  Deterministic 

Checks whether the first position is left from the second position.

rightOf :: [Int] -> [Int] -> Bool  Deterministic 

Checks whether the first position is right from the second position.

disjoint :: [Int] -> [Int] -> Bool  Deterministic 

Checks whether two positions are disjoint.

positions :: Term a -> [[Int]]  Deterministic 

Returns a list of all positions in a term.

(.>) :: [Int] -> [Int] -> [Int]  Deterministic 

Concatenates two positions.

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

(|>) :: Term a -> [Int] -> Term a  Deterministic 

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  Deterministic 

Replaces the subterm of a term at the given position with the given term if the position exists within the term.