Module type Abt.Syntax

The interface of the family of UABTs representings a syntax

module Op : Operator
type t = private
| Var of Var.t


| Bnd of Var.Binding.t * t

Scoped variable binding

| Opr of t Op.t

Operators specified in Op

The type of ABT's constructed from the operators defind in O

include Ppx_sexp_conv_lib.Sexpable.S with type Syntax.t := t
val t_of_sexp : Sexplib0__.Sexp.t -> t
val sexp_of_t : t -> Sexplib0__.Sexp.t
val bind : Var.Binding.t -> t -> t

bind bnd t is a branch of the ABT, in which any free variables in t matching the name of bnd are bound to bnd.

val of_var : Var.t -> t

of_var v is a leaf in the ABT consisting of the variable v

val v : string -> t

v x is a leaf in the ABT consisting of a variable named x

val op : t Op.t -> t

op o is a branch in the ABT consisting of the operator o

val (#.) : string -> t -> t

x #. t is a new abt obtained by binding all free variables named x in t

Note that this does not substitute variables for a value, (for which, see subst). This only binds the free variables within the scope of an abstraction that ranges over the given (sub) abt t.

val subst : Var.Binding.t -> value:t -> t -> t

subst bnd ~value t is a new ABT obtained by substituting value for all variables bound to bnd.

val subst_var : string -> value:t -> t -> t

subst_var name ~value t is a new abt obtained by substituting value for the outermost scope of variables bound to name in t

val to_sexp : t -> Sexplib.Sexp.t

to_sexp t is the representation of t as an s-expression

val of_sexp : Sexplib.Sexp.t -> t

of_sexp s is Abt represented by the s-expression s

val to_string : t -> string

to_string t is the representation of t as a string

val equal : t -> t -> bool

equal t t' is true when t and t' are alpha equivalent and false otherwise

val case : var:(Var.t -> 'a) -> bnd:((Var.Binding.t * t) -> 'a) -> opr:(t Op.t -> 'a) -> t -> 'a

Case analysis for eleminating ABTs

This is an alternative to using pattern-based elimination.

parameter var

function to apply to variables

parameter bnd

function to apply to bindings

parameter opr

function to apply to operators

val subterms : t -> t list

subterms t is a list of all the subterms in t, including t itself

val free_vars : t -> Var.Set.t

free_vars t is the set of variables that are free in in t

val is_closed : t -> bool

is_closed t if true if there are no free variables in t, otherwise false

module Unification : sig ... end