Module Literal.Pos

Positions

type split = {
lit_pos : Position.t;
term_pos : Position.t;
term : term;
}

Full description of a position in a literal. It contains:

  • lit_pos: the literal-prefix of the position
  • term_pos: the suffix that describes a subterm position
  • term: the term root, just under the literal itself. given this, applying T.Pos.at to the subterm position and the root term we obtain the sub-term itself.
val split : t -> Position.t -> split
raises Invalid_argument

if the position is incorrect

val at : t -> Position.t -> term

Subterm at given position, or

raises Invalid_argument

if the position is invalid

val replace : t -> at:Position.t -> by:term -> t

Replace subterm, or

raises Invalid_argument

if the position is invalid

val cut : t -> Position.t -> Position.t * Position.t

cut the subterm position off. For instance a position "left.1.2.stop" in an equation "l=r" will yield "left.stop", "1.2.stop".

it always holds that let a,b = cut p in Position.append a b = p

val root_term : t -> Position.t -> term

Obtain the term at the given position, at the root of the literal. It should hold that root_term lit p = [at lit (fst (cut p))].

val term_pos : t -> Position.t -> Position.t

term_pos lit p = snd (cut lit p), the subterm position.

val is_max_term : ord:Ordering.t -> t -> Position.t -> bool

Is the term at the given position, maximal in the literal w.r.t this ordering? In other words, if the term is replaced by a smaller term, can the whole literal becomes smaller?