sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page
At a surface level, the Beluga implementation produces two executables:
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.
Support
is the library of miscellaneous utility functions, data structures, and extensions to imported libraries.Optparser
is a library for parsing CLI arguments using combinators.Beluga_syntax
is the library defining the data types for the various syntaxes and common syntactic elements of Beluga and Harpoon.Beluga_parser
is the library for parsing Beluga signatures and Harpoon commands.Beluga_html
is a library for pretty-printing external Beluga signatures to HTML.Beluga
is 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.Harpoon
is the new interactive frontend to Beluga.