tamarin-prover-term-0.8.5.1: Term manipulation library for the tamarin prover.

MaintainerBenedikt Schmidt <beschmi@gmail.com>
Safe HaskellNone

Term.Positions

Description

Positions and replacement in terms.

Synopsis

Documentation

type Position = [Int]Source

A position in a term is a list of integers.

atPos :: Ord a => Term a -> Position -> Term aSource

t atPos p returns the subterm of term t at position p. The standard notation for t atPos p is t|_p. atPos accounts for AC symbols by interpreting n-ary operator applications *[t1,t2,..tk-1,tk] as binary applications t1*(t2*..(tk-1*tk)..).

replacePos :: Ord a => Term a -> (Term a, Position) -> Term aSource

t replacePos (s,p) returns the term t' where the subterm at position p is replaced by s. The standard notation for t replacePos (s,p) is t[s]_p. replacePos accounts for AC symbols in the same ways as atPos. FIXME: The AC can be optimized.

positionsNonVar :: (Show a, Show b) => VTerm a b -> [Position]Source

positionsNonVar t returns all the non-variable positions in the term t. positionsNonVar accounts for AC symbols in the same ways as atPos.