At a surface level, the Beluga implementation produces two executables:
- The Beluga CLI
- The Harpoon CLI
The Beluga CLI includes a legacy interactive mode interpreter. This is used by the
replay executable to interactively test some of the functionalities of the core Beluga system. This interactive system is mostly superseded by Harpoon.
The Beluga system is comprised of multiple private libraries. These are listed below in topological order of dependency.
Supportis the library of miscellaneous utility functions, data structures, and extensions to imported libraries.
Optparseris a library for parsing CLI arguments using combinators.
Beluga_syntaxis the library defining the data types for the various syntaxes and common syntactic elements of Beluga and Harpoon.
Beluga_parseris the library for parsing Beluga signatures and Harpoon commands.
Beluga_htmlis a library for pretty-printing external Beluga signatures to HTML.
Belugais the core library of Beluga, which deals with signature reconstruction, type-checking, coverage-checking and termination-checking. It also features modules handling the legacy interactive mode for Beluga, as well as proof search using logic programming.
Harpoonis the new interactive frontend to Beluga.