package tyabt

  1. Overview
  2. Docs

Functor building an implementation of abstract binding trees given a signature.

Parameters

module Sort : Sort

Signature

module Sort : Sort with type 'sort t = 'sort Sort.t
module Operator : Operator with type ('arity, 'sort) t = ('arity, 'sort) Operator.t
module Variable : Variable with type 'sort sort = 'sort Sort.t
type 'valence t

An abstract binding tree (ABT). 'valence is a phantom type parameter representing the valence of the ABT.

type ('arity, 'sort) operands =
  1. | [] : ('sort ar, 'sort) operands
    (*

    An empty list of operands.

    *)
  2. | :: : 'valence t * ('arity, 'sort) operands -> ('valence -> 'arity, 'sort) operands
    (*

    An operand followed by a list of operands.

    *)

A list of operands.

type 'valence view =
  1. | Abs : 'sort Variable.t * 'valence t -> ('sort -> 'valence) view
    (*

    An abstractor, which binds a variable within a term.

    *)
  2. | Op : ('arity, 'sort) Operator.t * ('arity, 'sort) operands -> 'sort va view
    (*

    An operator applied to operands.

    *)
  3. | Var : 'sort Variable.t -> 'sort va view
    (*

    A variable.

    *)

A view of an ABT.

val abs : 'sort Variable.t -> 'valence t -> ('sort -> 'valence) t

Constructs an abstractor ABT.

val op : ('arity, 'sort) Operator.t -> ('arity, 'sort) operands -> 'sort va t

Constructs an operation ABT.

val var : 'sort Variable.t -> 'sort va t

Constructs a variable ABT.

val into : 'valence view -> 'valence t

Constructs an ABT from a view.

val out : 'valence t -> 'valence view

Views an ABT.

val subst : 'sort Sort.t -> ('sort Variable.t -> 'sort va t option) -> 'valence t -> 'valence t

Applies a substitution to the ABT.

val aequiv : 'valence t -> 'valence t -> bool

Checks two ABTs for alpha-equivalence. Two ABTs are alpha-equivalent iff they are structurally equal up to renaming of bound variables.

val pp_print : Stdlib.Format.formatter -> _ t -> unit

Pretty-prints an ABT.