Module type `Abt.Syntax`Source

Sourcemodule Op : Operator

Sourcetype 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

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

Source

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

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

package um-abt

Module type Abt.SyntaxSource

Module type `Abt.Syntax`Source