Module Logtk.Position

Positions in terms, clauses...

Positions are used to indicate a given occurrence of an object in a tree-like structure.

Typically, we use positions to refer to a particular occurrence of a term in another (bigger) term, or in a literal, or in a clause.

A pair of {term,clause,literal} + position represents a context, that is, a {term,clause,literal} with a hole at the given position, where we can put a different term.

type t =
  1. | Stop
  2. | Type of t
    (*

    Switch to type

    *)
  3. | Left of t
    (*

    Left term in curried application

    *)
  4. | Right of t
    (*

    Right term in curried application, and subterm of binder

    *)
  5. | Head of t
    (*

    Head of uncurried term

    *)
  6. | Arg of int * t
    (*

    argument term in uncurried term, or in multiset

    *)
  7. | Body of t
    (*

    Body of binder or horn clause

    *)

A position is a path in a tree

type position = t
val stop : t
val type_ : t -> t
val left : t -> t
val right : t -> t
val head : t -> t
val body : t -> t
val arg : int -> t -> t
val size : t -> int
val opp : t -> t

Opposite position, when it makes sense (left/right)

val rev : t -> t

Reverse the position

val append : t -> t -> t

Append two positions

val is_prefix : t -> t -> bool

is_prefix a b is true iff a is a prefix of b

val is_strict_prefix : t -> t -> bool

is_prefix a b is true iff a is a prefix of b and a != b

val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
val num_of_funs : t -> int
val until_first_fun : t -> t
include Interfaces.PRINT with type t := t
val to_string : t -> string
module Map : sig ... end

Position builder

module Build : sig ... end

Pairing of value with Pos

Positions act a bit like lenses, in the sense that they compose nicely and designat paths in objects

module With : sig ... end