OCaml logo

logtk

Core types and algorithms for logic
Overview Documentation
IN THIS PACKAGE
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 =
| Stop
| Type of t(*

Switch to type

*)
| Left of t(*

Left term in curried application

*)
| Right of t(*

Right term in curried application, and subterm of binder

*)
| Head of t(*

Head of uncurried term

*)
| Arg of int * t(*

argument term in uncurried term, or in multiset

*)
| 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 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