Parsec chainl1 on failure

Question

I am trying to parse expressions from simply typed lambda calculus (F1) and I'm a struggling a bit with Parsec and can't figure out for the life of me how to solve my problem.

I have the following ADTs:

newtype LambdaVar = LV Char
  deriving (Eq, Ord)

data Type
  = TBool
  | TNat
  | Arr Type Type
  deriving Eq

data LambdaExpr
  = Abstr LambdaVar Type LambdaExpr
  | App LambdaExpr LambdaExpr
  | Var LambdaVar
  deriving Eq

newtype TypeContext = TC [(LambdaVar, Type)]
  deriving (Eq, Show)

data Expression = Expr TypeContext LambdaExpr Type
  deriving (Eq, Show)

with this parser:

type ParserT a b = ParsecT String a Identity b

parens :: ParserT a b -> ParserT a b
parens = between (char '(') (char ')')

symbol :: String -> ParserT a String
symbol p = spaces *> string p <* spaces

typeParser :: CharParser () Type
typeParser = arr <|> tbool <|> tnat
  where tbool = const TBool <$> string "Bool"
        tnat = const TNat <$> string "Nat"
        subtyp = parens arr <|> tbool <|> tnat
        arr = chainr1 subtyp $ try (symbol "->" *> pure Arr)

lambdaParser :: CharParser () LambdaExpr
lambdaParser = expr
  where expr = pApp <|> pAbstr <|> pVar
        pVar = Var . LV <$> letter
        pAbstr = Abstr <$> (LV <$> (char '\\' *> letter)) <*> (symbol ":" *> typeParser) <*> (char '.' *> expr)
        pApp = chainl1 subExpr (char ' ' *> pure App)
        subExpr = parens pApp <|> pAbstr <|> pVar

typeContextParser :: CharParser () TypeContext
typeContextParser = TC <$> ((,) <$> (LV <$> letter <* symbol ":") <*> typeParser) `sepBy` try (symbol ",")

expressionParser :: CharParser () Expression
expressionParser = Expr <$> (typeContextParser <* symbol "|-") <*> (lambdaParser <* symbol ":") <*> try typeParser

parse :: String -> Either ParseError Expression
parse = P.parse expressionParser ""

Now the problem arises when i.e. trying to parse an expression like

|- \x:Bool -> Nat.\y:Bool.x y : (Bool -> Nat) -> Bool -> Nat

and I try to parse it i will get an error:

unexpected ":"
expecting "(", "\\" or letter

So what happens here is that I have a space after x y so the parser assumes this will be an application but then finds a : which it can't parse as one, but I have no idea how to correct this behavior. I suppose I'd have to backtrack somehow with try but I just can't make it work.

ErikR ErikR · Accepted Answer · 2015-11-25T04:01:46

Please include your imports - it makes working with your code a lot easier.

I think I have gotten your parser to work by modifying all of the token parsers to also consume the white space immediately following the token.

For example, replace char x with (char x) <* spaces, string "->" with (string "->") <* spaces, etc.

Here is the working code:

{-# LANGUAGE NoMonomorphismRestriction, FlexibleContexts #-}

import Text.Parsec 
import qualified Text.Parsec as P
import Text.Parsec.Expr
import Text.ParserCombinators.Parsec.Char
import Data.Functor.Identity

newtype LambdaVar = LV Char
  deriving (Eq, Ord, Show)

data Type
  = TBool
  | TNat
  | Arr Type Type
  deriving (Eq, Show)

data LambdaExpr
  = Abstr LambdaVar Type LambdaExpr
  | App LambdaExpr LambdaExpr
  | Var LambdaVar
  deriving (Eq, Show)

newtype TypeContext = TC [(LambdaVar, Type)]
  deriving (Eq, Show)

data Expression = Expr TypeContext LambdaExpr Type
  deriving (Eq, Show)

type ParserT a b = ParsecT String a Identity b

lexeme p = p <* spaces

lchar = lexeme . char
lstring = lexeme . string

parens :: ParserT a b -> ParserT a b
parens = between (lchar '(') (lchar ')')

symbol :: String -> ParserT a String
symbol p = string p <* spaces

typeParser :: CharParser () Type
typeParser = arr <|> tbool <|> tnat
  where tbool = const TBool <$> lstring "Bool"
        tnat = const TNat <$> lstring "Nat"
        subtyp = parens arr <|> tbool <|> tnat
        arr = chainr1 subtyp $ try (symbol "->" *> pure Arr)

lambdaParser :: CharParser () LambdaExpr
lambdaParser = expr
  where expr = pApp <|> pAbstr <|> pVar
        pVar = Var . LV <$> (lexeme letter)
        pAbstr = Abstr <$> (LV <$> (lchar '\\' *> letter)) <*> (symbol ":" *> typeParser) <*> (lchar '.' *> expr)
        pApp = chainl1 subExpr (pure App)
        subExpr = parens pApp <|> pAbstr <|> pVar

typeContextParser :: CharParser () TypeContext
typeContextParser = TC <$> ((,) <$> (LV <$> letter <* symbol ":") <*> typeParser) `sepBy` try (symbol ",")

expressionParser :: CharParser () Expression
expressionParser = Expr <$> (typeContextParser <* symbol "|-") <*> (lambdaParser <* symbol ":") <*> try typeParser

parseIt :: String -> Either ParseError Expression
parseIt = P.parse expressionParser ""

test1 = parseIt
  "|- \\x:Bool -> Nat.\\y:Bool.x y : (Bool -> Nat) -> Bool -> Nat"
-- 1234 56789.123456789 .123456789.
--           1          2

Parsec chainl1 on failure

1 Answers