Module type `Tyabt.S`

Output signature of the functor Make.

module Sort : Sort

module Operator : Operator

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 = | ([]) : ('sort ar, 'sort) operands An empty list of operands. | (::) : 'valence t * ('arity, 'sort) operands -> ('valence -> 'arity, 'sort) operands An operand followed by a list of operands.: A list of operands.

type 'valence view = | Abs : 'sort Variable.t * 'valence t -> ('sort -> 'valence) view An abstractor, which binds a variable within a term. | Op : ('arity, 'sort) Operator.t * ('arity, 'sort) operands -> 'sort va view An operator applied to operands. | 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.