peterbb/ocaml-abt

Library implementing abstract binding trees

Abstract Binding Trees

This is an implementation of abstract binding trees (ABT) in Ocaml. A user of the library defines two modules defined by the interfaces SORT and OPERATOR, and the library will from this give:

• A module implementing multi-sorted abstract binding trees with variables (subject to substitution) and symbols (subject to renameing). Terms are considered equal up to renaming of bound variables and symbols.
• A pretty printer and a parser.

Building

The library depends on menhirLib. Build by executing jbuilder build. Run tests by executing jbuilder runtest.

Credits

Based on ABT's as described in Robert Harper's Practical Foundations of Programming Languages and Jon Sterling's implementation in SML.

ocaml-abt's Issues

Syntactic sugar when parsing.

In addition to parsing ABT's in their standard form, the parser also supports special syntax for binary operators. One can write for instance write {t0 -> t1} instead of ->(t0; t1).

Question: Should the library have more support for syntactic sugar?

Add support for augmenting ABTs with extra information.

It should be possible to augment ABTs with different kinds of information. For instance, it should be possible to annotate an ABT with debugging information (line, column and filename).

The target can either be to only support such simple annotation, or maybe one could add more
complicated information. E.g. add information about the type of each sub-expression.

One potential source of problems, is if someone stores ABT's as annotations inside ABT's, and expect abstraction to work. It will not work, if annotations are implemented naively.

Improve error reporting

Currently, the different functions implemented in Language.Make(_) will throw different
exceptions when the user does something wrong. Figuring out exactly how to propagate errors to the user of the library must be sorted out.