package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct