0

Note: This was originally posted with incorrect error message and is now corrected.

Am trying to compile the Agda source code associated with the paper Total Parser Combinators by Nils Anders Danielsson. The source code is available here github. When compiling I am getting the following error:

Not in scope:
return′
at parser-combinators-master/TotalParserCombinators/Parser.agda:99,46-53 when scope checking return′

I am using Agda version 2.6.2 and have updated std-lib using cabal (according to instructions on Agda Wiki) and the agda/libs/agda-stdlib/README.agda states

This version of the library has been tested using Agda 2.6.2.

I am very much not not an Agda expert; my motivation is the paper as opposed to the code per se. It would, however, be extremely useful to have the code working.

Any pointers on where to look, what to check or to try greatly appreciated.

systemcpro
  • 856
  • 1
  • 7
  • 15
  • `NamePart` is defined in [`Mixfix/Operator.agda`](https://github.com/nad/parser-combinators/blob/f396c054e9d6554871691ce6ccbadbaa53dd8402/Mixfix/Operator.agda#L20). AFAICT the repository does not contain a `mixfix.agda` file so the error message you get is strange. (It does contain a `Mixfix.agda` file but that does not explicitly mention `NamePart` at all so I don't see why it would attempt to scope-check it). – gallais Feb 08 '23 at 12:13
  • @gallais Thank you for checking it for me. You are correct, it is my mistake. Humblest apologies. That is the error from the code from the paper [https://www.cse.chalmers.se/~nad/publications/danielsson-norell-mixfix.pdf](Parsing Mixfix Operators) which is a sort of precursor to the paper mentioned. In my desperation I thought I would try to get that working and see how that went. The ACTUAL error is Not in scope: return′ at parser-combinators-master/TotalParserCombinators/Parser.agda:99,46-53 – systemcpro Feb 08 '23 at 13:03
  • @gallais Have edited post to reflect the actual error message and hide my embrassment :( – systemcpro Feb 08 '23 at 13:13

0 Answers0