package logtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.PositionSource

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

erm,clause,literal

  1. position represents a context, that is, a

    erm,clause,literal

    with a hole at the given position, where we can put a different term.

Sourcetype 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

Sourcetype position = t
Sourceval stop : t
Sourceval type_ : t -> t
Sourceval left : t -> t
Sourceval right : t -> t
Sourceval head : t -> t
Sourceval body : t -> t
Sourceval arg : int -> t -> t
Sourceval opp : t -> t

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

Sourceval rev : t -> t

Reverse the position

Sourceval append : t -> t -> t

Append two positions

Sourceval is_prefix : t -> t -> bool

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

Sourceval is_strict_prefix : t -> t -> bool

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

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

Position builder

Sourcemodule 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

Sourcemodule With : sig ... end
OCaml

Innovation. Community. Security.