Improve documentation of the Agda backend on the command line

[MatthewDaggitt]

Current running bnfc --help gives the output below, but it doesn't any reference to the Agda backend. Experimentally at least the -p option seems to work for Agda.

Target languages
    --java          Output Java code [default: for use with JLex and CUP]
    --haskell       Output Haskell code for use with Alex and Happy (default)
    --haskell-gadt  Output Haskell code which uses GADTs
    --latex         Output LaTeX code to generate a PDF description of the language
    --c             Output C code for use with FLex and Bison
    --cpp           Output C++ code for use with FLex and Bison
    --cpp-nostl     Output C++ code (without STL) for use with FLex and Bison
    --csharp        Output C# code for use with GPLEX and GPPG
    --ocaml         Output OCaml code for use with ocamllex and ocamlyacc
    --profile       Output Haskell code for rules with permutation profiles
    --pygments      Output a Python lexer for Pygments

Special options for the Haskell backend
  -p <namespace>                  Prepend <namespace> to the package/module name
  -d                              Put Haskell code in modules Lang.* instead of Lang*
                  --alex1         Use Alex 1.1 as Haskell lexer tool
                  --alex2         Use Alex 2 as Haskell lexer tool
                  --alex3         Use Alex 3 as Haskell lexer tool (default)
                  --sharestrings  Use string sharing in Alex 2 lexer
                  --bytestrings   Use byte string in Alex 2 lexer
                  --glr           Output Happy GLR parser
                  --ghc           Use ghc-specific language extensions
                  --functor       Make the AST a functor and use it to store the position of the nodes
                  --xml           Also generate a DTD and an XML printer
                  --xmlt          DTD and an XML printer, another encoding
                  --cnf           Use the CNF parser instead of happy
                  --agda          Also generate Agda bindings for the abstract syntax

Special options for the Java backend
  -l                        Add and set line_number field for all syntax classes
                            Java requires cup 0.11b-2014-06-11 or greater
  -p <namespace>            Prepend <namespace> to the package/module name
                  --jlex    Lex with JLex, parse with CUP (default)
                  --jflex   Lex with JFlex, parse with CUP
                  --antlr4  Lex and parse with antlr4

Special options for the C backend
  -l    Add and set line_number field for all syntax classes
        Java requires cup 0.11b-2014-06-11 or greater

Special options for the C++ backend
  -l                Add and set line_number field for all syntax classes
                    Java requires cup 0.11b-2014-06-11 or greater
  -p <namespace>    Prepend <namespace> to the package/module name

Special options for the C# backend
  -p <namespace>         Prepend <namespace> to the package/module name
                  --vs   Generate Visual Studio solution/project files
                  --wcf  Add support for Windows Communication Foundation,
                          by marking abstract syntax classes as DataContracts

[andreasabel]

--agda is just one of the options of the Haskell backend:

Special options for the Haskell backend
  -p NAMESPACE  --name-space=NAMESPACE  Prepend NAMESPACE to the package/module name
  -d                                    Put Haskell code in modules LANG.* instead of LANG* (recommended)
                --bytestrings           Use ByteString in Alex lexer [deprecated, use --text-token]
                --text-token            Use Text in Alex lexer
                --string-token          Use String in Alex lexer (default)
                --glr                   Output Happy GLR parser [deprecated]
                --functor               Make the AST a functor and use it to store the position of the nodes
                --generic               Derive Data and Generic instances for AST types
                --xml                   Also generate a DTD and an XML printer
                --xmlt                  DTD and an XML printer, another encoding
                --agda                  Also generate Agda bindings for the abstract syntax

But yes, it could be more explicit about the Agda backend. Also https://bnfc.readthedocs.io/en/latest/user_guide.html#agda-backend could be fleshed out a bit. (Btw, you seem to be using version 2.8.* of BNFC as some options have been removed in the mean time.)

[MatthewDaggitt]

Ah I'd missed that! Having said that my student was calling it as:

bnfc -d --agda VNNLIB-Standard/syntax.cf -o src -p VNNLIB

so I didn't even think to look under the Haskell docs. While it may be internally implemented as an option to the Haskell backend, it seems like from a CLI perspective that it can be used as a top-level language target and therefore should be documented as such?

Furthermore if there are Agda specific flags that need to be added in future, having it as it's own top-level language target seems like it might be a more extensible design? (even though it would obviously remain being implemented via the Haskell backend internally)