Parser combinators for Idris
Idris Shell Makefile
Latest commit 6d65ad1 Nov 23, 2016 @ziman committed on GitHub Merge pull request #49 from justjoheinz/fix/runtests
Fix runtests script for Mac OS X
Failed to load latest commit information.
examples Change return to pure to avoid deprecation warnings Nov 23, 2016
tests Fix runtests script for Mac OS X Nov 23, 2016
.gitignore Updates. Aug 6, 2015
LICENSE License added. Dec 10, 2013
Lightyear.idr Update lightyear to current Idris offerings. Feb 5, 2016
Makefile Don't fail if tests/*.ibc don't exist Aug 2, 2016


Lightweight parser combinator library for Idris, inspired by Parsec.

Module overview:

  • Lightyear.Core: central definitions + instances
  • Lightyear.Errmsg: error message formatting, mainly internal library
  • Lightyear.Combinators: generic combinators like many or sepBy
  • Lightyear.Char: char-bound parsers like char or space
  • Lightyear.Strings: string-bound parsers like strings or lexeme


This package is used (almost) the same way as Parsec, except for one difference: backtracking.


  • Parsec combinators won't backtrack if a branch of <|> has consumed any input, hence Parsec parsers require an explicit try.

  • Lightyear parsers are backtrack-by-default and there is the commitTo combinator that makes the parser commit to that branch.

In other words, the following two pieces of code are equivalent (using illustrative combinator names):


elem :: Parser Int
elem = (try (string "0x") >> hexNumber) <|> decNumber


elem : Parser Int
elem = (string "0x" $> commitTo hexNumber) <|> decNumber
-- which may be abbreviated as:
--   = (string "0x" >! hexNumber) <|> decNumber

After reading the prefix 0x, both parsers commit to reading a hexadecimal number or nothing at all — Parsec does this automatically, Lightyear uses the commitTo combinator for this purpose. On the other hand, Parsec requires the string "0x" to be wrapped in try because if we are reading 0123, we definitely don't want to commit to the left branch upon seeing the leading 0.

For convenience, commitTo is merged in monadic and applicative operators, yielding the operators >!=, >!, <$!>, <$!, and $!>. The ! in the names is inspired by the notation used for cuts in Prolog.

A parser that uses commitment might look like this (notice the leading char '@' that leads to commitment):

entry : Parser Entry
entry = char '@' >! do
  typ <- pack <@> some (satisfy (/= '{'))
  token "{"
  ident <- pack <@> some (satisfy (/= ','))
  token ","
  items <- item `sepBy` comma
  token "}"
  return $ En typ ident items


Lightyear is used to parse BibTeX in bibdris.


$ make clean
$ make test
$ make install