package beluga

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Implementation of contextual modal logic for reasoning with higher-order abstract syntax

Install

dune-project

Dependency

sha256=b212cd25f28487591e7eb08207f31c45c1329cdd5f76544aca00904089ed8718

sha512=2e1e029912a6352733a44689a38cc9161a49c870990930e4432e48c2e376902b18bd5f21d64db936dfb0574fffb69ed17eecde2823f2295fc7bb7255b81638aa

Added C. Sano, R. Kavanagh and B. Pientka's artifact for "Mechanizing Session-Types Using a Structural View" as a case study (#271).

Support postponed fixity pragmas in modules.
The hole _ in the LF term \x._ is parsed as a wildcard instead of as an identifier.
Shadowed bindings in a module are no longer brought into scope when the module is opened.
Support postponed fixity pragmas in Harpoon sessions.

Updated the Beluga mode for Emacs to use the 'cl-lib library instead of 'cl.

Colouring of error messages is fixed for the Beluga mode for Emacs using the 'ansi-color library (requires Emacs >= v28.1).

Parsing and disambiguation of non-normal expressions is supported.
Parsing of prefix, infix and postfix operators is supported for computation-level type family constants and constructors, as well as type-annotated programs and values.
Improved error-reporting with printing of source code.
Pretty-printing of Beluga signatures to HTML now supports hyperlinks for constants to their declaration site.

Underscores (_) in LF term and type constant declarations are treated as wildcards. This means that a constant a : oft M A -> equiv M N _ -> oft N _ stands for a : oft M A -> equiv M N B -> oft N C as opposed to a : oft M A -> equiv M N A -> oft N A.
Substitution meta-objects need to be prefixed by $. That is, the plain substitution [g |- $S] must be written as $[g |- $S], and the renaming substitution [g |-# $S] must be written as $[g |-# $S].
Substitution meta-types need to be prefixed by $. That is, the plain substitution meta-type [g |- h] must be written as $[g |- h], and the renaming substitution meta-type [g |-# h] must be written as $[g |-# h].
Parameter types need to be prefixed by #. That is, {#p : [g |- nat]} must be written as {#p : #[g |- nat]}.
Identifier overloading is disallowed. This means that term-level constants may not be overloaded with type-level constants.
Freezing of type family declarations is more strict. This means that old-style LF term-level constants cannot be added to type families after any declaration other than old-style LF type or term-level constant declarations.
Destructors for coinductive type families use postfix notation, like projections or field accesses (i.e., s .hd, s .tl). This applies both in computation-level patterns and expressions.
Namespaces are now fully supported in Beluga signatures.

Interactive Harpoon sessions are now local to the referencing environment in which they are declared.
Lexing of nested delimited comments %{{, }}% and %{, }% is fixed.
--open pragmas behave like OCaml's open directive, whereby declarations introduced by --open are not re-exported, and not copy/pasted textually.

On This Page