Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix printing of parse errors in enumeration sequences #1070

Merged
merged 1 commit into from
Feb 10, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
60 changes: 30 additions & 30 deletions src/Cryptol/Parser/ParserUtils.hs
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ lexerP k = P $ \cfg p s ->
case sTokens s of
t : _ | Err e <- tokenType it ->
Left $ HappyErrorMsg (srcRange t) $
case e of
[case e of
UnterminatedComment -> "unterminated comment"
UnterminatedString -> "unterminated string"
UnterminatedChar -> "unterminated character"
Expand All @@ -79,14 +79,15 @@ lexerP k = P $ \cfg p s ->
T.unpack (tokenText it)
MalformedSelector -> "malformed selector: " ++
T.unpack (tokenText it)
]
where it = thing t

t : more -> unP (k t) cfg p s { sPrevTok = Just t, sTokens = more }
[] -> Left (HappyOutOfTokens (cfgSource cfg) p)

data ParseError = HappyError FilePath {- Name of source file -}
(Located Token) {- Offending token -}
| HappyErrorMsg Range String
| HappyErrorMsg Range [String]
| HappyUnexpected FilePath (Maybe (Located Token)) String
| HappyOutOfTokens FilePath Position
deriving (Show, Generic, NFData)
Expand Down Expand Up @@ -123,7 +124,7 @@ ppError (HappyOutOfTokens path pos) =
text "Unexpected end of file at:" <+>
text path <.> char ':' <.> pp pos

ppError (HappyErrorMsg p x) = text "Parse error at" <+> pp p $$ nest 2 (text x)
ppError (HappyErrorMsg p xs) = text "Parse error at" <+> pp p $$ nest 2 (vcat (map text xs))

ppError (HappyUnexpected path ltok e) =
text "Parse error at" <+>
Expand Down Expand Up @@ -159,13 +160,13 @@ happyError = P $ \cfg _ s ->
case sPrevTok s of
Just t -> Left (HappyError (cfgSource cfg) t)
Nothing ->
Left (HappyErrorMsg emptyRange "Parse error at the beginning of the file")
Left (HappyErrorMsg emptyRange ["Parse error at the beginning of the file"])

errorMessage :: Range -> String -> ParseM a
errorMessage r x = P $ \_ _ _ -> Left (HappyErrorMsg r x)
errorMessage :: Range -> [String] -> ParseM a
errorMessage r xs = P $ \_ _ _ -> Left (HappyErrorMsg r xs)

customError :: String -> Located Token -> ParseM a
customError x t = P $ \_ _ _ -> Left (HappyErrorMsg (srcRange t) x)
customError x t = P $ \_ _ _ -> Left (HappyErrorMsg (srcRange t) [x])

expected :: String -> ParseM a
expected x = P $ \cfg _ s ->
Expand Down Expand Up @@ -231,19 +232,19 @@ intVal :: Located Token -> ParseM Integer
intVal tok =
case tokenType (thing tok) of
Num x _ _ -> return x
_ -> errorMessage (srcRange tok) "Expected an integer"
_ -> errorMessage (srcRange tok) ["Expected an integer"]

mkFixity :: Assoc -> Located Token -> [LPName] -> ParseM (Decl PName)
mkFixity assoc tok qns =
do l <- intVal tok
unless (l >= 1 && l <= 100)
(errorMessage (srcRange tok) "Fixity levels must be between 1 and 100")
(errorMessage (srcRange tok) ["Fixity levels must be between 1 and 100"])
return (DFixity (Fixity assoc (fromInteger l)) qns)

fromStrLit :: Located Token -> ParseM (Located String)
fromStrLit loc = case tokenType (thing loc) of
StrLit str -> return loc { thing = str }
_ -> errorMessage (srcRange loc) "Expected a string literal"
_ -> errorMessage (srcRange loc) ["Expected a string literal"]


validDemotedType :: Range -> Type PName -> ParseM (Type PName)
Expand All @@ -264,14 +265,14 @@ validDemotedType rng ty =
TParens t -> validDemotedType rng t
TInfix{} -> ok

where bad x = errorMessage rng (x ++ " cannot be demoted.")
where bad x = errorMessage rng [x ++ " cannot be demoted."]
ok = return $ at rng ty

-- | Input fields are reversed!
mkRecord :: AddLoc b => Range -> (RecordMap Ident (Range, a) -> b) -> [Named a] -> ParseM b
mkRecord rng f xs =
case res of
Left (nm,(nmRng,_)) -> errorMessage nmRng ("Record has repeated field: " ++ show (pp nm))
Left (nm,(nmRng,_)) -> errorMessage nmRng ["Record has repeated field: " ++ show (pp nm)]
Right r -> pure $ at rng (f r)

where
Expand Down Expand Up @@ -325,7 +326,7 @@ eFromTo r e1 e2 e3 =
(Nothing, Just (e2', t), Nothing) -> eFromToType r e1 (Just e2') e3 (Just t)
(Nothing, Nothing, Just (e3', t)) -> eFromToType r e1 e2 e3' (Just t)
(Nothing, Nothing, Nothing) -> eFromToType r e1 e2 e3 Nothing
_ -> errorMessage r "A sequence enumeration may have at most one element type annotation."
_ -> errorMessage r ["A sequence enumeration may have at most one element type annotation."]
where
asETyped (ELocated e _) = asETyped e
asETyped (ETyped e t) = Just (e, t)
Expand All @@ -345,9 +346,9 @@ exprToNumT r expr =
Just t -> return t
Nothing -> bad
where
bad = errorMessage (fromMaybe r (getLoc expr)) $ unlines
bad = errorMessage (fromMaybe r (getLoc expr))
[ "The boundaries of .. sequences should be valid numeric types."
, "The expression `" ++ show expr ++ "` is not."
, "The expression `" ++ show (pp expr) ++ "` is not."
]


Expand Down Expand Up @@ -413,21 +414,21 @@ mkTypeInst x | nullIdent (thing (name x)) = PosInst (value x)

mkTParam :: Located Ident -> Maybe Kind -> ParseM (TParam PName)
mkTParam Located { srcRange = rng, thing = n } k
| n == widthIdent = errorMessage rng "`width` is not a valid type parameter name."
| n == widthIdent = errorMessage rng ["`width` is not a valid type parameter name."]
| otherwise = return (TParam (mkUnqual n) k (Just rng))

mkTySyn :: Located PName -> [TParam PName] -> Type PName -> ParseM (Decl PName)
mkTySyn ln ps b
| getIdent (thing ln) == widthIdent =
errorMessage (srcRange ln) "`width` is not a valid type synonym name."
errorMessage (srcRange ln) ["`width` is not a valid type synonym name."]

| otherwise =
return $ DType $ TySyn ln Nothing ps b

mkPropSyn :: Located PName -> [TParam PName] -> Type PName -> ParseM (Decl PName)
mkPropSyn ln ps b
| getIdent (thing ln) == widthIdent =
errorMessage (srcRange ln) "`width` is not a valid constraint synonym name."
errorMessage (srcRange ln) ["`width` is not a valid constraint synonym name."]

| otherwise =
DProp . PropSyn ln Nothing ps . thing <$> mkProp b
Expand All @@ -436,12 +437,12 @@ polyTerm :: Range -> Integer -> Integer -> ParseM (Bool, Integer)
polyTerm rng k p
| k == 0 = return (False, p)
| k == 1 = return (True, p)
| otherwise = errorMessage rng "Invalid polynomial coefficient"
| otherwise = errorMessage rng ["Invalid polynomial coefficient"]

mkPoly :: Range -> [ (Bool,Integer) ] -> ParseM (Expr PName)
mkPoly rng terms
| w <= toInteger (maxBound :: Int) = mk 0 (map fromInteger bits)
| otherwise = errorMessage rng ("Polynomial literal too large: " ++ show w)
| otherwise = errorMessage rng ["Polynomial literal too large: " ++ show w]

where
w = case terms of
Expand All @@ -455,8 +456,7 @@ mkPoly rng terms

mk res (n : ns)
| testBit res n = errorMessage rng
("Polynomial contains multiple terms with exponent "
++ show n)
["Polynomial contains multiple terms with exponent " ++ show n]
| otherwise = mk (setBit res n) ns


Expand Down Expand Up @@ -540,17 +540,17 @@ mkPrimTypeDecl mbDoc (Forall as qs st ~(Just schema_rng)) finK =
Just (n,xs) ->
do vs <- mapM tpK as
unless (distinct (map fst vs)) $
errorMessage schema_rng "Repeated parameters."
errorMessage schema_rng ["Repeated parameters."]
let kindMap = Map.fromList vs
lkp v = case Map.lookup (thing v) kindMap of
Just (k,tp) -> pure (k,tp)
Nothing ->
errorMessage
(srcRange v)
("Undefined parameter: " ++ show (pp (thing v)))
["Undefined parameter: " ++ show (pp (thing v))]
(as',ins) <- unzip <$> mapM lkp xs
unless (length vs == length xs) $
errorMessage schema_rng "All parameters should appear in the type."
errorMessage schema_rng ["All parameters should appear in the type."]

let ki = finK { thing = foldr KFun (thing finK) ins }

Expand All @@ -565,7 +565,7 @@ mkPrimTypeDecl mbDoc (Forall as qs st ~(Just schema_rng)) finK =
}
]

Nothing -> errorMessage schema_rng "Invalid primitive signature"
Nothing -> errorMessage schema_rng ["Invalid primitive signature"]

where
splitT r ty = case ty of
Expand All @@ -592,7 +592,7 @@ mkPrimTypeDecl mbDoc (Forall as qs st ~(Just schema_rng)) finK =
Just k -> pure (tpName tp, (tp,k))
Nothing ->
case tpRange tp of
Just r -> errorMessage r "Parameters need a kind annotation"
Just r -> errorMessage r ["Parameters need a kind annotation"]
Nothing -> panic "mkPrimTypeDecl"
[ "Missing range on schema parameter." ]

Expand Down Expand Up @@ -671,7 +671,7 @@ mkProp ty =
TTyApp{} -> err

where
err = errorMessage r "Invalid constraint"
err = errorMessage r ["Invalid constraint"]

-- | Make an ordinary module
mkModule :: Located ModName ->
Expand Down Expand Up @@ -708,7 +708,7 @@ ufToNamed (UpdField h ls e) =
(UpdSet, [l]) | RecordSel i Nothing <- thing l ->
pure Named { name = l { thing = i }, value = e }
_ -> errorMessage (srcRange (head ls))
"Invalid record field. Perhaps you meant to update a record?"
["Invalid record field. Perhaps you meant to update a record?"]

exprToFieldPath :: Expr PName -> ParseM [Located Selector]
exprToFieldPath e0 = reverse <$> go noLoc e0
Expand Down Expand Up @@ -744,7 +744,7 @@ exprToFieldPath e0 = reverse <$> go noLoc e0
}
]

_ -> errorMessage loc "Invalid label in record update."
_ -> errorMessage loc ["Invalid label in record update."]


mkSelector :: Token -> Selector
Expand Down
3 changes: 3 additions & 0 deletions tests/issues/issue975.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[ 0, -1 .. 0 ]
[ 10 .. () ]
[ \x -> x .. 42 ]
13 changes: 13 additions & 0 deletions tests/issues/issue975.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
Loading module Cryptol

Parse error at issue975.icry:1:6--1:8
The boundaries of .. sequences should be valid numeric types.
The expression `-1` is not.

Parse error at issue975.icry:2:9--2:11
The boundaries of .. sequences should be valid numeric types.
The expression `()` is not.

Parse error at issue975.icry:3:3--3:10
The boundaries of .. sequences should be valid numeric types.
The expression `\x -> x` is not.