fix issue with try in parser, improve parse error message

This commit is contained in:
2026-01-16 10:30:41 -08:00
parent 997adfd04c
commit a21dd2fd94
4 changed files with 33 additions and 9 deletions

View File

@@ -442,9 +442,11 @@ quantity = fromMaybe Many <$> optional (Zero <$ keyword "0")
ebind : Parser Telescope
ebind = do
-- don't commit until we see the ":"
symbol "("
quant <- quantity
names <- try (some (addPos varname) <* symbol ":")
(quant, names) <- try $ do
symbol "("
quant <- quantity
names <- some (addPos varname) <* symbol ":"
pure (quant,names)
ty <- typeExpr
symbol ")"
pure $ map (makeBind quant ty) names
@@ -662,8 +664,10 @@ parseNorm = DCheck <$> getPos <* keyword "#check" <*> typeExpr <* keyword ":" <*
parseDecl : Parser Decl
parseDecl = parseMixfix <|> parsePType <|> parsePFunc
<|> parseNorm <|> parseData <|> parseShortData <|> parseSig <|> parseDef
<|> parseNorm <|> parseData <|> parseShortData
<|> parseClass <|> parseInstance <|> parseRecord
-- We'll put the backtracing stuff last, but there is a commit issue in parseDef
<|> parseSig <|> parseDef

View File

@@ -63,7 +63,7 @@ partialParse fn pa ops toks = case runP pa emptyBounds toks False ops (emptyFC'
try : a. Parser a -> Parser a
try (P pa) = P $ \last toks com ops col => case pa last toks com ops col of
(Fail x err last toks com ops) => Fail x err last toks False ops
(Fail x err last toks _ ops) => Fail x err last toks com ops
res => res
@@ -71,8 +71,8 @@ fail : ∀ a. String -> Parser a
fail msg = P $ \last toks com ops col => Fail False (perror col.file toks msg) last toks com ops
fatal : a. String -> Parser a
fatal msg = P $ \last toks com ops col => Fail True (perror col.file toks msg) last toks com ops
-- fatal : ∀ a. String -> Parser a
-- fatal msg = P $ \last toks com ops col => Fail True (perror col.file toks msg) last toks com ops
getOps : Parser (Operators)
@@ -85,7 +85,7 @@ addOp nm prec fix = P $ \ last toks com ops col =>
case parts of
"" :: key :: rule => OK MkUnit last toks com (updateMap key (MkOp nm prec fix False rule) ops)
key :: rule => OK MkUnit last toks com (updateMap key (MkOp nm prec fix True rule) ops)
Nil => Fail True (perror col.file toks "Internal error parsing mixfix") last toks com ops
Nil => Fail False (perror col.file toks "Internal error parsing mixfix") last toks com ops
instance Functor Parser where
map f (P pa) = P $ \ last toks com ops col => map f (pa last toks com ops col)
@@ -211,7 +211,7 @@ token' : Kind -> Parser String
token' k = satisfy (\t => t.val.kind == k) "Expected a \{show k} token"
keyword' : String -> Parser Unit
keyword' kw = ignore $ satisfy (\t => t.val.text == kw && (t.val.kind == Keyword || t.val.kind == Symbol || t.val.kind == Number)) "Expected \{kw}"
keyword' kw = ignore $ satisfy (\t => t.val.text == kw && (t.val.kind == Keyword || t.val.kind == Symbol || t.val.kind == Number)) "Expected '\{kw}'"
-- expect indented token of given kind

14
tests/ErrMsg.newt Normal file
View File

@@ -0,0 +1,14 @@
module ErrMsg
import Prelude
infixl 5 _$$_
_$$_ : Nat (Nat Nat) Nat
a $$ b = a + b a
-- Say something other than expected record
-- Why do we get there? shouldn't the progress made by parseDef short circuit the <|>?
blah : Nat Nat
blah x = x $$ $ \ y => y

6
tests/ErrMsg.newt.fail Normal file
View File

@@ -0,0 +1,6 @@
*** Process tests/ErrMsg.newt
module Prelude
module ErrMsg
ERROR at tests/ErrMsg.newt:13:15--13:16: trailing operator
Compile failed