Module type Abt.Syntax
The interface of the family of UABTs representings a syntax
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 int
matching the name ofbnd
are bound tobnd
.
val v : string -> t
v x
is a leaf in the ABT consisting of a variable namedx
val (#.) : string -> t -> t
x #. t
is a new abt obtained by binding all free variables namedx
int
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) abtt
.
val subst : Var.Binding.t -> value:t -> t -> t
subst bnd ~value t
is a new ABT obtained by substitutingvalue
for all variables bound tobnd
.
val subst_var : string -> value:t -> t -> t
subst_var name ~value t
is a new abt obtained by substitutingvalue
for the outermost scope of variables bound toname
int
val to_sexp : t -> Sexplib.Sexp.t
to_sexp t
is the representation oft
as an s-expression
val of_sexp : Sexplib.Sexp.t -> t
of_sexp s
is Abt represented by the s-expressions
val to_string : t -> string
to_string t
is the representation oft
as a string
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 is_closed : t -> bool
is_closed t
iftrue
if there are no free variables int
, otherwise false
module Unification : sig ... end