package logtk

  1. Overview
  2. Docs
On This Page
  1. Positions
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

Positions

type split = {
  1. lit_pos : Position.t;
  2. term_pos : Position.t;
  3. 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
val at : t -> Position.t -> term

Subterm at given position, or

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

Replace subterm, or

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?