From e19fbf489f43d538354255e293102a5c6013c6a9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Wed, 20 Jul 2022 16:24:03 +0200 Subject: [PATCH] Implement some error messages (#1396) (#1400) * Implement error message for double braces * Implement error message for implicit pattern on the left of an application * Implement error message for constructor expected on the left of an application Co-authored-by: Jan Mas Rovira --- src/Juvix/Syntax/Concrete/Scoped/Error.hs | 6 ++ .../Syntax/Concrete/Scoped/Error/Types.hs | 67 +++++++++++++++++++ .../Syntax/Concrete/Scoped/Pretty/Base.hs | 6 ++ src/Juvix/Syntax/Concrete/Scoped/Scoper.hs | 24 ++++--- src/Juvix/Translation/ScopedToAbstract.hs | 29 ++++---- test/Scope/Negative.hs | 21 ++++++ .../ConstructorExpectedLeftApplication.juvix | 6 ++ .../ImplicitPatternLeftApplication.juvix | 6 ++ tests/negative/NestedPatternBraces.juvix | 6 ++ 9 files changed, 149 insertions(+), 22 deletions(-) create mode 100644 tests/negative/ConstructorExpectedLeftApplication.juvix create mode 100644 tests/negative/ImplicitPatternLeftApplication.juvix create mode 100644 tests/negative/NestedPatternBraces.juvix diff --git a/src/Juvix/Syntax/Concrete/Scoped/Error.hs b/src/Juvix/Syntax/Concrete/Scoped/Error.hs index 80db0b085..34ab25d06 100644 --- a/src/Juvix/Syntax/Concrete/Scoped/Error.hs +++ b/src/Juvix/Syntax/Concrete/Scoped/Error.hs @@ -33,6 +33,9 @@ data ScoperError | ErrMultipleCompileRuleSameBackend MultipleCompileRuleSameBackend | ErrWrongKindExpressionCompileBlock WrongKindExpressionCompileBlock | ErrDuplicateInductiveParameterName DuplicateInductiveParameterName + | ErrDoubleBracesPattern DoubleBracesPattern + | ErrImplicitPatternLeftApplication ImplicitPatternLeftApplication + | ErrConstructorExpectedLeftApplication ConstructorExpectedLeftApplication deriving stock (Show) instance ToGenericError ScoperError where @@ -60,3 +63,6 @@ instance ToGenericError ScoperError where ErrMultipleCompileRuleSameBackend e -> genericError e ErrWrongKindExpressionCompileBlock e -> genericError e ErrDuplicateInductiveParameterName e -> genericError e + ErrDoubleBracesPattern e -> genericError e + ErrImplicitPatternLeftApplication e -> genericError e + ErrConstructorExpectedLeftApplication e -> genericError e diff --git a/src/Juvix/Syntax/Concrete/Scoped/Error/Types.hs b/src/Juvix/Syntax/Concrete/Scoped/Error/Types.hs index 0a3439ec8..488902f42 100644 --- a/src/Juvix/Syntax/Concrete/Scoped/Error/Types.hs +++ b/src/Juvix/Syntax/Concrete/Scoped/Error/Types.hs @@ -546,3 +546,70 @@ instance ToGenericError DuplicateInductiveParameterName where <> "." <> line <> "Inductive parameter names can not be repeated." + +newtype DoubleBracesPattern = DoubleBracesPattern + { _doubleBracesPatternArg :: PatternArg + } + deriving stock (Show) + +makeLenses ''DoubleBracesPattern + +instance ToGenericError DoubleBracesPattern where + genericError e = + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [i] + } + where + pat :: PatternArg + pat = e ^. doubleBracesPatternArg + i = getLoc pat + msg = + "Double braces are not valid:" + -- TODO add bold to braces + <+> braces (ppCode pat) + +newtype ImplicitPatternLeftApplication = ImplicitPatternLeftApplication + { _implicitPatternLeftApplication :: PatternApp + } + deriving stock (Show) + +makeLenses ''ImplicitPatternLeftApplication + +instance ToGenericError ImplicitPatternLeftApplication where + genericError e = + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [i] + } + where + pat :: PatternApp + pat = e ^. implicitPatternLeftApplication + i = getLoc pat + msg = + "Pattern matching an implicit argument cannot occur on the left of an application:" + <+> ppCode pat + +newtype ConstructorExpectedLeftApplication = ConstructorExpectedLeftApplication + { _constructorExpectedLeftApplicationPattern :: Pattern + } + deriving stock (Show) + +makeLenses ''ConstructorExpectedLeftApplication + +instance ToGenericError ConstructorExpectedLeftApplication where + genericError e = + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [i] + } + where + pat :: Pattern + pat = e ^. constructorExpectedLeftApplicationPattern + i = getLoc pat + msg = + "Constructor expected on the left of a pattern application:" + <+> ppCode pat diff --git a/src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs b/src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs index b1983c397..dca4110df 100644 --- a/src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs +++ b/src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs @@ -660,6 +660,12 @@ instance PrettyCode PatternArg where p <- ppCode (a ^. patternArgPattern) return (bracesIf (Implicit == a ^. patternArgIsImplicit) p) +instance PrettyCode PatternApp where + ppCode (PatternApp l r) = do + l' <- ppLeftExpression appFixity l + r' <- ppRightExpression appFixity r + return $ l' <+> r' + ppPatternParenType :: forall s r. (SingI s, Member (Reader Options) r) => PatternParensType s -> Sem r (Doc Ann) ppPatternParenType p = case sing :: SStage s of SParsed -> ppCode p diff --git a/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs b/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs index 741d7f0b2..a56e546ae 100644 --- a/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs +++ b/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs @@ -1420,7 +1420,7 @@ parseTerm = -- Infix Patterns ------------------------------------------------------------------------------- -type ParsePat = P.Parsec () [PatternAtom 'Scoped] +type ParsePat = P.ParsecT () [PatternAtom 'Scoped] (Sem '[Error ScoperError]) makePatternTable :: PatternAtoms 'Scoped -> [[P.Operator ParsePat PatternArg]] @@ -1543,11 +1543,18 @@ parsePatternTerm = do _ -> Nothing parseBraces :: ParsePat PatternArg - parseBraces = P.token bracesPat mempty + parseBraces = do + res <- P.token bracesPat mempty + case res of + Left er -> P.lift (throw er) + Right a -> return a where - bracesPat :: PatternAtom 'Scoped -> Maybe PatternArg + bracesPat :: PatternAtom 'Scoped -> Maybe (Either ScoperError PatternArg) bracesPat s = case s of - PatternAtomBraces r -> Just (set patternArgIsImplicit Implicit r) + PatternAtomBraces r + | Implicit <- r ^. patternArgIsImplicit -> + Just (Left (ErrDoubleBracesPattern (DoubleBracesPattern r))) + | otherwise -> Just (Right (set patternArgIsImplicit Implicit r)) _ -> Nothing parseParens :: ParsePat PatternArg @@ -1587,15 +1594,16 @@ parsePatternAtoms :: PatternAtoms 'Scoped -> Sem r PatternArg parsePatternAtoms atoms@(PatternAtoms sec' _) = do - case res of - Left {} -> throw (ErrInfixPattern (InfixErrorP atoms)) - Right r -> return r + case run (runError res) of + Left e -> throw e -- Scoper effect error + Right Left {} -> throw (ErrInfixPattern (InfixErrorP atoms)) -- Megaparsec error + Right (Right r) -> return r where sec = toList sec' tbl = makePatternTable atoms parser :: ParsePat PatternArg parser = runM (mkPatternParser tbl) <* P.eof - res = P.parse parser filePath sec + res = P.runParserT parser filePath sec filePath :: FilePath filePath = "tmp" diff --git a/src/Juvix/Translation/ScopedToAbstract.hs b/src/Juvix/Translation/ScopedToAbstract.hs index cac5f9973..4ff394619 100644 --- a/src/Juvix/Translation/ScopedToAbstract.hs +++ b/src/Juvix/Translation/ScopedToAbstract.hs @@ -341,31 +341,35 @@ goFunctionParameter (FunctionParameter {..}) = do } goPatternApplication :: + Member (Error ScoperError) r => PatternApp -> Sem r Abstract.ConstructorApp goPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternApplication a) goPatternConstructor :: + Member (Error ScoperError) r => ConstructorRef -> Sem r Abstract.ConstructorApp goPatternConstructor a = uncurry Abstract.ConstructorApp <$> viewApp (PatternConstructor a) goInfixPatternApplication :: + Member (Error ScoperError) r => PatternInfixApp -> Sem r Abstract.ConstructorApp goInfixPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternInfixApplication a) goPostfixPatternApplication :: + Member (Error ScoperError) r => PatternPostfixApp -> Sem r Abstract.ConstructorApp goPostfixPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternPostfixApplication a) -viewApp :: forall r. Pattern -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg]) -viewApp = \case +viewApp :: forall r. Member (Error ScoperError) r => Pattern -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg]) +viewApp p = case p of PatternConstructor c -> return (goConstructorRef c, []) - PatternApplication (PatternApp l r) -> do + PatternApplication app@(PatternApp _ r) -> do r' <- goPatternArg r - second (`snoc` r') <$> viewAppLeft l + second (`snoc` r') <$> viewAppLeft app PatternInfixApplication (PatternInfixApp l c r) -> do l' <- goPatternArg l r' <- goPatternArg r @@ -377,19 +381,16 @@ viewApp = \case PatternWildcard {} -> err PatternEmpty {} -> err where - viewAppLeft :: PatternArg -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg]) - viewAppLeft p - -- TODO proper error - | Implicit <- p ^. patternArgIsImplicit = error "An implicit pattern cannot be on the left of an application" - | otherwise = viewApp (p ^. patternArgPattern) - -- TODO proper error - err :: a - err = error "constructor expected on the left of a pattern application" + viewAppLeft :: PatternApp -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg]) + viewAppLeft app@(PatternApp l _) + | Implicit <- l ^. patternArgIsImplicit = throw (ErrImplicitPatternLeftApplication (ImplicitPatternLeftApplication app)) + | otherwise = viewApp (l ^. patternArgPattern) + err = throw (ErrConstructorExpectedLeftApplication (ConstructorExpectedLeftApplication p)) goConstructorRef :: ConstructorRef -> Abstract.ConstructorRef goConstructorRef (ConstructorRef' n) = Abstract.ConstructorRef (goName n) -goPatternArg :: PatternArg -> Sem r Abstract.PatternArg +goPatternArg :: Member (Error ScoperError) r => PatternArg -> Sem r Abstract.PatternArg goPatternArg p = do pat' <- goPattern (p ^. patternArgPattern) return @@ -398,7 +399,7 @@ goPatternArg p = do _patternArgPattern = pat' } -goPattern :: Pattern -> Sem r Abstract.Pattern +goPattern :: Member (Error ScoperError) r => Pattern -> Sem r Abstract.Pattern goPattern p = case p of PatternVariable a -> return $ Abstract.PatternVariable (goSymbol a) PatternConstructor c -> Abstract.PatternConstructorApp <$> goPatternConstructor c diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index 405fbec15..ed910006c 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -205,6 +205,27 @@ scoperErrorTests = $ \case ErrQualSymNotInScope {} -> Nothing _ -> wrongError, + NegTest + "Double braces in pattern" + "." + "NestedPatternBraces.juvix" + $ \case + ErrDoubleBracesPattern {} -> Nothing + _ -> wrongError, + NegTest + "Pattern matching an implicit argument on the left of an application" + "." + "ImplicitPatternLeftApplication.juvix" + $ \case + ErrImplicitPatternLeftApplication {} -> Nothing + _ -> wrongError, + NegTest + "Constructor expected on the left of a pattern application" + "." + "ConstructorExpectedLeftApplication.juvix" + $ \case + ErrConstructorExpectedLeftApplication {} -> Nothing + _ -> wrongError, NegTest "Compile block for a unsupported kind of expression" "CompileBlocks" diff --git a/tests/negative/ConstructorExpectedLeftApplication.juvix b/tests/negative/ConstructorExpectedLeftApplication.juvix new file mode 100644 index 000000000..1a2a39806 --- /dev/null +++ b/tests/negative/ConstructorExpectedLeftApplication.juvix @@ -0,0 +1,6 @@ +module ConstructorExpectedLeftApplication; + +f : {A : Type} -> A -> A; +f (x y) := x; + +end; diff --git a/tests/negative/ImplicitPatternLeftApplication.juvix b/tests/negative/ImplicitPatternLeftApplication.juvix new file mode 100644 index 000000000..15fb15bfd --- /dev/null +++ b/tests/negative/ImplicitPatternLeftApplication.juvix @@ -0,0 +1,6 @@ +module ImplicitPatternLeftApplication; + +f : {A : Type} -> A -> A; +f ({x} y) := y; + +end; diff --git a/tests/negative/NestedPatternBraces.juvix b/tests/negative/NestedPatternBraces.juvix new file mode 100644 index 000000000..4b21a8aa5 --- /dev/null +++ b/tests/negative/NestedPatternBraces.juvix @@ -0,0 +1,6 @@ +module NestedPatternBraces; + +a : {A : Type} → Type; +a {{A}} ≔ a; + +end;