module Ltree:`sig`

..`end`

Abstract syntax trees with binders and quantifiers

An abstract syntax tree with binders extends a basic first-order term structure with let bindings and quantifiers. The abstract syntax tree is parametrized by the three types of its symbols, its free variables and its sorts.

A basic term is a tree structure, where a term is either a leaf containing a symbol or a variable. A term can also be a node containing a symbol with one or more subterms. All symbols are variadic and arity constraints are not checked or enforced in this module.

For let bindings and quantifiers we add typed lambda abstractions and distinguish between free and bound variables. A typed lambda abstraction is a term where one or more variables are bound. We do nameless abstraction with de Bruijn indexes, hence a bound variables is just its index, whereas free variables are values of the type of free variables.

A let binding is a lambda abstraction of `n`

bound variables
together with `n`

terms that are to be substituted for the bound
variables. Quantifiers are just lambda abstractions.

In order to maintain invariants about de Bruijn indexes, the type of an abstract syntax term is private to this module and terms must be created with the appropriate constructors.

In addition, there is a type of flat terms, where the topmost let
binding has been evaluated. An abstract syntax term can be
converted to a flat term with the `Ltree.S.destruct`

function, which
distributes let bindings over nodes and ensures that the top
symbols of the term is a node, a leaf or a variable. Subterms of a
nodes are abstract syntax terms with binders and `Ltree.S.destruct`

can
be repeatedly applied to these subterms.

Tail-recursive fold and map functions are provided. The
`Ltree.S.eval_t`

function presents the subterms bottom-up and
right-to-left to the folding function and lazily evaluates all let
bindings. It fails when the term contains quantifiers. The
`Ltree.S.map`

function presents all subterms to the function, again
bottom-up and right-to-left, let bindings are not unfolded. Hence,
not every subterm is a proper abstract syntax term and the mapping
function is given the number of let binding the subterm is under
as an argument.

**Author(s):** Christoph Sticksel

module type BaseTypes =`sig`

..`end`

Input signature for functor

module type S =`sig`

..`end`

Output signature of functor

module Make:

Functor to create a higher-order abstract syntax tree module