package um-abt

  1. Overview
  2. Docs

Module type Abt.SyntaxSource

Sourcetype 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

Sourceval 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.

Sourceval of_var : Var.t -> t

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

Sourceval v : string -> t

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

Sourceval op : t Op.t -> t

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

Sourceval (#.) : 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.

Sourceval 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.

Sourceval 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

Sourceval to_string : t -> string

to_string t is the representation of t as a string

Sourceval equal : t -> t -> bool

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

Sourceval 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

Sourceval subterms : t -> t list

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

Sourceval free_vars : t -> Var.Set.t

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

Sourceval is_closed : t -> bool

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

Sourcemodule Unification : sig ... end