package tyabt

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Legend:
Library
Module
Module type
Parameter
Class
Class type

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

Parameters

module Sort : Sort

module Operator : Operator

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 =

| [] : ('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 : Format.formatter -> _ t -> unit

Pretty-prints an ABT.