package term-tools

  1. Overview
  2. Docs

Module type Intf.ZipperSource

The module type of zippers.

This module implements zippers over first-order terms.

For advanced users: as an extension over plain zippers, the module also allows to edit a term lazily applied to a substitution. In plain words, the variables contained in terms may point to other terms, specified by a substitution provided at zipper creation time. One can then navigate and edit the induced graph in a purely applicative fashion.

type term

The type of terms.

type t

The type of zippers.

type 'a with_state

For plain zippers, 'a with_state = 'a. When doing term graph edition, this type encapsulates the underlying substitution.

val pp : t Fmt.t

Pretty-printing zippers.

val compare : t -> t -> int

compare is a total order.

val equal : t -> t -> bool

equal z1 z2 tests whether z1 and z2 are equal.

val cursor : t -> term

cursor z is the term under focus of z.

val path : t -> int list

path z is the path from the root to the term under focus of z.

val of_term : term with_state -> t

of_term t is the zipper of the term t.

val to_term : t -> term with_state

to_term z is the term represented by the zipper z.

val move_up : t -> t option

move_up z is the zipper obtained by moving up in the zipper z.

val deref : t -> t option

For experienced users only. deref z is

  • None when cursor z is not a variable
  • If cursor z is a variable k and k is not bound in the underlying substitution, deref z is also None
  • Otherwise, deref z is Some z' where z' is a zipper located at the term associated to k.
val move_at : t -> int -> t option

move_at z i is the zipper obtained by moving at the index i.

For experienced users/experimental: when doing term graph edition, in the case where cursor z is a variable in the domain of the underlying substitution, move_at z i will silently perform a deref before moving at the index i of the obtained term.

val move_at_exn : t -> int -> t

move_at_exn z i is the exception-raising vaeriant of move_at.

Raises Invalid_argument if i is out of bounds.

val replace : term -> t -> t

replace t z is the zipper obtained by replacing the term at the focus of z by t.

val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a

fold f acc z folds a zipper over the subterms of cursor z (including cursor z).

fold does not follow the links given by the substitution underlying z, if any.

type var := int
val fold_variables : (var -> t -> 'a -> 'a) -> t -> 'a -> 'a

fold_variables f acc z folds a zipper over the subterms of cursor z which are variables.

fold_variables does not follow the links given by the substitution underlying z, if any.