Nothing Special   »   [go: up one dir, main page]
Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix #405: support --functor in the Agda backend #406

Merged
merged 7 commits into from
Dec 23, 2021
Merged

Fix #405: support --functor in the Agda backend #406

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
d3fd356
Fix #405: support --functor in the Agda backend
andreasabel Dec 21, 2021
7ded4a4
Testing #405: use --functor with --agda in system testsuite
andreasabel Dec 21, 2021
1eab993
Re #405 (Agda/Functor): fix problem with underscores in category names
andreasabel Dec 22, 2021
80ccbfa
Re #405: implement `define` for Agda/Functor by parametrizing Haskell's
andreasabel Dec 22, 2021
af2cd4d
CHANGELOG #405
andreasabel Dec 22, 2021
c745f36
Agda makefile: use `${AGDA}` instead of just `agda`
andreasabel Dec 22, 2021
a964b7c
Document `--agda --functor` (#405)
andreasabel Dec 22, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 9 additions & 2 deletions docs/user_guide.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ Agda Backend

The Agda Backend (option ``--agda``, since 2.8.3) invokes the Haskell backend
and adds Agda-bindings for the generated parser, printer, and abstract syntax.
The bindings target the GHC backend of Agda, in version 2.5.4 or higher.
The bindings target the GHC backend of Agda, in version 2.6.0 or higher.
Example run::

bnfc --agda -m -d Calc.cf
Expand All @@ -20,17 +20,24 @@ The following files are created by the Agda backend, in addition to the files cr
- Agda data types bound to the corresponding types for abstract syntax trees in ``Abs.hs``.
- Agda bindings for the pretty-printing functions in ``Print.hs``.

Uses pragmas in mutual blocks, which is supported by Agda ≥ 2.6.0.

2. ``Parser.agda``: Agda bindings for the parser functions generated by ``Par.y``.

3. ``IOLib.agda``: Agda bindings for the Haskell IO monad and basic input/output functions.

4. ``Main.agda``: A test program invoking the parser, akin to ``Test.hs``.
Uses ``do`` notation, which is supported by Agda >=2.5.4.
Uses ``do`` notation, which is supported by Agda ≥ 2.5.4.

The Agda backend targets plain Agda with just the built-in types and
functions; no extra libraries required (also not the standard
library).

*Since 2.9.4:* Option ``--functor`` puts position information into the
Agda syntax trees (affects generated ``AST.agda``). Relies on the
primitive module ``Agda.Builtin.Maybe`` which is available from
Agda 2.6.2.

Java Backend
============

Expand Down
1 change: 1 addition & 0 deletions source/CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
Unreleased

* LBNF: empty tokens types are now forbidden [#388]
* Agda: support position information via `--functor` [#405]
* C/C++: use `size_t` and `-Wsign-conversion` [#391]
* C++: repair broken `--line-numbers` [#390], regression in 2.9.2 by [#349]

Expand Down
Loading