Parseque

Port of the agdarsec total parser combinator library to Rocq/Coq.

Meta

• Author(s):
  • G. Allais (initial)
• Rocq-community maintainer(s):
  • Wolfgang Meier (@womeier)
• License: MIT License
• Compatible Rocq/Coq versions: 9.0 or later (for older versions see opam/nix)
• Additional dependencies: none
• Rocq/Coq namespace: parseque
• Related publication(s):
  • agdarsec - Total Parser Combinators

Building and installation instructions

The easiest way to install the latest released version of Parseque is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install rocq-parseque

To instead build and install manually, do:

git clone https://github.com/rocq-community/parseque.git
cd parseque
make   # or make -j <number-of-cores-on-your-machine> 
make install

Documentation

This Rocq/Coq library is a port of the agdarsec library for Agda. The core design of agdarsec is described in this paper, while this blog post describes instrumentation.

It may be helpful to seek inspiration from a larger example. See e.g. the WasmCert parser of the WebAssembly binary format.