Module Ltree

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 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 (T : BaseTypes-> S with type symbol = T.symbol and type var = T.var and type sort = T.sort and type attr = T.attr
Functor to create a higher-order abstract syntax tree module