package um-abt

  1. Overview
  2. Docs
package um-abt
Legend:
Library
Module
Module type
Parameter
Class
Class type

Make (Op) is a module for constructing and manipulating ABTs for the operators defined in Op.

Parameters

module Op : Operator

Signature

type t = private
  1. | Var of Var.t
    (*

    Variables

    *)
  2. | Bnd of Var.Binding.t * t
    (*

    Scoped variable binding

    *)
  3. | 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