git.iko.soy/Idris-dev
on master help sign in
Move parsing of 'case' out of simpleExpr
c15b21bEdwin Brady
src/Idris/ParseExpr.hs+2−2
compare with master
unifiedsplit
@@ -181,6 +181,7 @@ InternalExpr ::=
181 | Let
181 | Let
182 | RewriteTerm
182 | RewriteTerm
183 | Pi
183 | Pi
184+ | CaseExpr
184 | DoBlock
185 | DoBlock
185 ;
186 ;
186@
187@
@@ -199,6 +200,7 @@ internalExpr syn =
199 <|> rewriteTerm syn
200 <|> rewriteTerm syn
200 <|> try(pi syn)
201 <|> try(pi syn)
201 <|> doBlock syn
202 <|> doBlock syn
203+ <|> caseExpr syn
202 <|> simpleExpr syn
204 <|> simpleExpr syn
203 <?> "expression"
205 <?> "expression"
204
206
@@ -263,7 +265,6 @@ SimpleExpr ::=
263 | 'refl' ('{' Expr '}')?
265 | 'refl' ('{' Expr '}')?
264 | ProofExpr
266 | ProofExpr
265 | TacticsExpr
267 | TacticsExpr
266− | CaseExpr
267 | FnName
268 | FnName
268 | List
269 | List
269 | Comprehension
270 | Comprehension
@@ -290,7 +291,6 @@ simpleExpr syn =
290 <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))
291 <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))
291 <|> proofExpr syn
292 <|> proofExpr syn
292 <|> tacticsExpr syn
293 <|> tacticsExpr syn
293− <|> caseExpr syn
294 <|> do reserved "Type"; return PType
294 <|> do reserved "Type"; return PType
295 <|> try (do c <- constant
295 <|> try (do c <- constant
296 fc <- getFC
296 fc <- getFC
src/Idris/ParseHelpers.hs+2−1
@@ -260,7 +260,8 @@ operatorLetter = oneOf opChars
260-- | Parses an operator
260-- | Parses an operator
261operator :: MonadicParsing m => m String
261operator :: MonadicParsing m => m String
262operator = do op <- token . some $ operatorLetter
262operator = do op <- token . some $ operatorLetter
263+ when (op `elem` [":", "=>", "->", "<-", "=", "?="]) $
263− when (op == ":") $ fail "(:) is not a valid operator"
264+ fail $ op ++ " is not a valid operator"
264 return op
265 return op
265
266
266{- * Position helpers -}
267{- * Position helpers -}