package logtk

  1. Overview
  2. Docs
package logtk
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.

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