c15b21b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Move parsing of 'case' out of simpleExpr

Even if this is possible, using it as an application unbracketed would be unreadable! This speeds up parsing of nested case blocks massively. (Or should I say "unslows down").

commitc15b21bbaa6ffb6b345a36d49e18c6ae760d5591 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 4 Feb 2014, 20:32 (13 years ago) parent9e8f96c

2 files changed+4−3

compare with master

unifiedsplit

src/Idris/ParseExpr.hs+2−2 src/Idris/ParseHelpers.hs+2−1

src/Idris/ParseExpr.hs+2−2

@@ -181,6 +181,7 @@ InternalExpr ::=

181181 | Let

182182 | RewriteTerm

183183 | Pi

184+ | CaseExpr

184185 | DoBlock

185186 ;

186187@

@@ -199,6 +200,7 @@ internalExpr syn =

199200 <|> rewriteTerm syn

200201 <|> try(pi syn)

201202 <|> doBlock syn

203+ <|> caseExpr syn

202204 <|> simpleExpr syn

203205 <?> "expression"

204206

@@ -263,7 +265,6 @@ SimpleExpr ::=

263265 | 'refl' ('{' Expr '}')?

264266 | ProofExpr

265267 | TacticsExpr

266− | CaseExpr

267268 | FnName

268269 | List

269270 | Comprehension

@@ -290,7 +291,6 @@ simpleExpr syn =

290291 <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))

291292 <|> proofExpr syn

292293 <|> tacticsExpr syn

293− <|> caseExpr syn

294294 <|> do reserved "Type"; return PType

295295 <|> try (do c <- constant

296296 fc <- getFC

src/Idris/ParseHelpers.hs+2−1

@@ -260,7 +260,8 @@ operatorLetter = oneOf opChars

260260-- | Parses an operator

261261operator :: MonadicParsing m => m String

262262operator = do op <- token . some $ operatorLetter

263− when (op == ":") $ fail "(:) is not a valid operator"

263+ when (op `elem` [":", "=>", "->", "<-", "=", "?="]) $

264+ fail $ op ++ " is not a valid operator"

264265 return op

265266

266267{- * Position helpers -}