Module Literal.Pos

module Pos: sig .. end

Positions

type split = {

	`lit_pos : Libzipperposition.Position.t;`
	`term_pos : Libzipperposition.Position.t;`
	`term : Literal.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 : Literal.t -> Libzipperposition.Position.t -> split

Raises Invalid_argument if the position is incorrect

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

Subterm at given position, or
Raises Invalid_argument if the position is invalid

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

Replace subterm, or
Raises Invalid_argument if the position is invalid

val cut : Literal.t ->
       Libzipperposition.Position.t ->
       Libzipperposition.Position.t * Libzipperposition.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 : Literal.t -> Libzipperposition.Position.t -> Literal.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 : Literal.t -> Libzipperposition.Position.t -> Libzipperposition.Position.t

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

val is_max_term : ord:Libzipperposition.Ordering.t ->
       Literal.t -> Libzipperposition.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?