To be able to use the getPosition defined in the parameters branch we need
the following combinators:

pre  : M a -> Parser M b -> Parser M (a * b)
post : Parser M a -> M b -> Parser M (a * b)

The currently released version fails to build with agda-stdlib 2.0. This is fixed in master, but that fails to build for a different reason:

/build/source/examples/Expr.agda:8,1-26
Importing module Level.Bounded using the --guardedness flag from a
module which does not.
when scope checking the declaration
  open import Level.Bounded

Cf. https://github.com/gallais/idris-tparsec/blob/master/src/TParsec/Combinators/JSON.idr

I have a basic but ~working CSV parser that, with a little polishing, might be of use to others. Is there any interest in integrating this as an example or separate module (similar to the JSON module)?

Best,

Chris

Hi, this is more of a question than anything, but I'm wondering if there's any relationship between the module Data.List.Sized and Agda's sized types. The latter have come in handy for me to be able to prove termination of some functions, and my impression is that the former are used to make sure the parsers are total, is this right? Thanks in advance for clarifying.

It would be nice to have:

reLex : (check : q -> Maybe p) ->  ∀[ Parser P v ] ->  ∀[ Parser Q v ]

where P and Q are essentially the same parameters except that P
has p as the token type while Q has q, which is larger.

My current use case: I want the user to provide a parser munching characters
but I'd like to use it in a context where a lexer has been run and some special
characters have been recognised as special. So I have:

data TOK = A | B | C Char

and I'd like reLex to run a modified view that takes check into account
so that the client's anyTok only succeeds if the TOK has the shape C c.

Right now, every parser failure returns the same value: 𝕄.∅. A library consumer can't keep track of e.g. which parser is running, where in the source the error was, or what caused the error.

I'm not sure what the best way to fix this is. parsec has a type ParseError and their version of runParser returns the equivalent of aParseError ⊎ Success. agdarsec could do something very similar. More generally, Parser could have another two parameters, say

• {ParseError : Set e}, and
• mkError : (m : ℕ) → Toks m → ParseError

where mkError m s would be used wherever 𝕄.∅ is now (m being the position in the stream).
This would allow users to ignore errors for performance reasons. (Of course, this specializes to the current behavior when ParseError ≡ 𝕄 and mkError ≡ λ _ _ → 𝕄.∅.)

In any case, this would require fundamentally changing the API, though I think it's necessary for any serious use.

Just by reading https://markkarpov.com/post/megaparsec-7.html, I can see:

• anyTokenBut
• noneOf

Hi, I'm new to Agda and having trouble using this library. When trying to load the Parentheses.agda example, I get the following error:

/home/siddharthist/code/agda/agdarsec/src/Induction/Nat/Strong.agda:23,21-27
Ambiguous name ≤-refl. It could refer to any one of
  Data.Nat.LTE.≤-refl
  bound at
  /home/siddharthist/code/agda/agdarsec/src/Data/Nat/LTE.agda:7,1-7
  Data.Nat.Properties.≤-refl
  bound at
  /home/siddharthist/code/agda/agda-stdlib/src/Data/Nat/Properties.agda:61,1-7
(hint: Use C-c C-w (in Emacs) if you want to know why)
when scope checking ≤-refl

If I replace the import like so, the loading progresses to the next file, where there is yet another conflict:

-- open import Data.Nat.LTE
open import Data.Nat.LTE hiding (≤-refl; ≤-trans; <⇒≤)

Any ideas why this might be happening? Thanks in advance, I look forward to using your code!

I'm currently trying to include agdarsec in nixpkgs: NixOS/nixpkgs#100351 But unfortunately it doesn't seem to build (possibly this has to do with the current version of the standard library). I tried master (b26230a) and the release v3.0.0.

With master, I get these errors:

[...]
    /nix/store/1b7jp08xlcbvankbf8aml162zmid00la-standard-library-1.4/src/Expr.agda
    /nix/store/1b7jp08xlcbvankbf8aml162zmid00la-standard-library-1.4/src/Expr.lagda
    /build/source/src/Expr.agda
    /build/source/src/Expr.lagda
    /build/source/Expr.agda
    /build/source/Expr.lagda
    /nix/store/vkm07q5a493h356zmlqzvn7sxc4r0wwv-Agda-2.6.1.2-data/share/ghc-8.10.2/x86_64-linux-ghc-8.10.2/Agda-2.6.1.2/lib/prim/Expr.agda
    /nix/store/vkm07q5a493h356zmlqzvn7sxc4r0wwv-Agda-2.6.1.2-data/share/ghc-8.10.2/x86_64-linux-ghc-8.10.2/Agda-2.6.1.2/lib/prim/Expr.lagda
  when scope checking the declaration
    import Expr

It seems like Expr cannot be imported. I'm not sure whether it's supposed to be part of agdarsec or part of the standard library.

Travis is super slow these days

It doesn't make much sense to have Text.Parser.Examples.
I should move that to examples/ on the same level as src/.