4

I'm trying to formalise a regular expression based string search tool in Idris (current status here). But I'm fighting with the problem of parsing regular expressions. I've tried to build a small parsing library but gave up on this in favor to use Lightyear, a parsing combinator library for Idris.

Since I'm used to Haskell, I've tried to use a similar strategy that I would do using Parsec. My main problem is how to handle left recursion on Lightyear parsers? I've tried several encodings but pretty much all parsers end up looping and causing segmentation faults in generated code.

5
  • 1
    Well, you can get rid of the left recursion. Given A ::= Aa | b you can use the equivalent grammar: A' ::= bA'' A'' ::= aA'' | "" (you can do this even with more productions and if the recursion is indirect, although it becomes too long for a comment.
    – Bakuriu
    Oct 30, 2015 at 18:33
  • Hi Bakuriu. I've tried to remove left recursion from the grammar, but it still stuck, the parser loops and causes a segmentation fault. Later, I'll post the grammar, but I believe that I removed it correctly. Oct 30, 2015 at 18:40
  • 2
    The standard Parsec solution is to factor left recursion into chainl. Oct 30, 2015 at 19:20
  • I know it. My problem is that if it is possible to write a chainl combinator in Idris using already implemented lightyear library combinators. Oct 30, 2015 at 19:24
  • On an unrelated note, you might be interested in my aGdaREP project. The core algorithm is adapted from Alexandre Agular and Bassel Mannaa's 2009 technical report (pdf). My parser is awful though so it won't be much help there.
    – gallais
    Nov 3, 2015 at 11:10

2 Answers 2

4

I don't know Lightyear, but I had some success porting Parsec to Idris:

module Parser

data Parser : Type -> Type where
     P : (String -> List (a, String)) -> Parser a

unP : Parser a -> String -> List (a, String)
unP (P f) = f

total stripPrefix : (Eq a) => List a -> List a -> Maybe (List a)
stripPrefix [] ys = Just ys
stripPrefix (x::xs) (y::ys) = if (x == y) then stripPrefix xs ys else Nothing
stripPrefix _ _  = Nothing

total token : String -> Parser ()
token tk = P $ \s => case stripPrefix (unpack tk) (unpack s) of
      Just s' => [((), pack s')]
      Nothing => []

total skip : Parser ()
skip = P $ \s => case unpack s of
     [] => []
     (_::s') => [((), pack s')]

instance Functor Parser where
  map f p = P $ \s => map (\(x, s') => (f x, s')) (unP p s)

instance Applicative Parser where
  pure x = P $ \s => [(x, s)]
  (P pf) <*> (P px) = P $ \s => concat (map (\(f, s') => map (\(x, s'') => (f x, s'')) (px s')) (pf s))

instance Alternative Parser where
  empty = P $ \s => []
  (P p1) <|> (P p2) = P $ \s => case p1 s of
     [] => p2 s
     results => results

instance Monad Parser where
  px >>= f = P $ \s => concat (map (\(x, s') => unP (f x) s') (unP px s))

total runParser : Parser a -> String -> Maybe a
runParser (P p) s = case p s of
  [(x, "")] => Just x
  _         => Nothing

This allows a straight copy-paste implementation of chainl:

chainl1 : Parser a -> Parser (a -> a -> a) -> Parser a
chainl1 p op = p >>= rest
  where
    rest x = do { f <- op; y <- p; rest $ f x y } <|> return x

chainl : Parser a -> Parser (a -> a -> a) -> a -> Parser a
chainl p op x = chainl1 p op <|> return x

We can then take a straight transliteration of the expression parser from the chainl docs (I'm too lazy to implement a proper integer parser so we'll just use unary):

parens : Parser a -> Parser a
parens p = token "(" *> p <* token ")"

symbol : String -> Parser ()
symbol = token

integer : Parser Nat
integer = P $ \s => case unpack s of
     ('Z'::s') => [(Z, pack s')]
     ('S'::s') => map (\(n, s'') => (S n, s'')) $ unP integer (pack s')
     _ => []

mutual
    expr : Parser Nat
    expr = term   `chainl1` addop

    term : Parser Nat
    term = factor `chainl1` mulop

    factor : Parser Nat
    factor  = parens expr <|> integer

    mulop : Parser (Nat -> Nat -> Nat)
    mulop = (symbol "*" *> pure (*)) <|>
            (symbol "/" *> pure div)

    addop : Parser (Nat -> Nat -> Nat)
    addop = (symbol "+" *> pure (+)) <|>
            (symbol "-" *> pure (-))

Now, if you try this:

main : IO ()
main = do
  s <- getLine
  printLn $ runParser expr s

then it will have the same divergant behaviour that you've observed. However, we can make two small changes:

  1. Introduce a lazy alternative combinator:

    orElse : Parser a -> Lazy (Parser a) -> Parser a
    orElse p1 p2 = P $ \s => case unP p1 s of
       [] => unP p2 s
       results => results
    
  2. Make sure the recursive part of factor, i.e. the parens expr part, is in this lazy position, by flipping the two alternatives:

    factor = integer `orElse`  parens expr
    

This then works as expected:

13:06:07 [cactus@galaxy brainfuck]$ idris Expr.idr -o Expr
13:06:27 [cactus@galaxy brainfuck]$ echo "SZ+(SSZ*SSSZ)" | ./Expr
Just 7
1
  • 2
    Thanks for your points. The Lightyear library has a "lazy" choice combinator in which the second parser is lazy. This solved my problem. Oct 31, 2015 at 16:11
0

The chainl and chainl1 combinators can be used with the Lightyear package. However, they are provided by default. I've added the combinators to my own modules where I've needed them:

chainl1 : Parser a -> Parser (a -> a -> a) -> Parser a
chainl1 p op = p >>= rest
  where rest a1 = (do f <- op
                      a2 <- p
                      rest (f a1 a2)) <|> pure a1

chainl : Parser a -> Parser (a -> a -> a) -> a -> Parser a
chainl p op a = (p `chainl1` op) <|> pure a

Seems to work fine. Hope that helps.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.