package beluga

  1. Overview
  2. Docs
Implementation of contextual modal logic for reasoning with higher-order abstract syntax

Install

Dune Dependency

Authors

Maintainers

Sources

beluga-1.1.2.tbz
sha256=b212cd25f28487591e7eb08207f31c45c1329cdd5f76544aca00904089ed8718
sha512=2e1e029912a6352733a44689a38cc9161a49c870990930e4432e48c2e376902b18bd5f21d64db936dfb0574fffb69ed17eecde2823f2295fc7bb7255b81638aa

CHANGES.md.html

v1.1.2

Added

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

Fixed

  • 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.

v1.1.1

Added

  • Added support for fixity pragmas before declarations (#270).

Changed

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

Fixed

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

v1.1

Added

  • 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.

Changed

  • 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.

Fixed

  • 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.

Removed

  • Harpoon sequencing of REPL commands with ; is no longer supported.

  • Context variable arrow types [ctx] → [⊢ unit] are no longer supported.

OCaml

Innovation. Community. Security.