um-abt 0.1.5 · OCaml Package

module Op : Operator

type t = private

| Var of Var.t
(*
Variables
*)
| 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

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_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

package um-abt