From cf2a3e9a8c0ea080ae034abdf6db8fc3bb973b0a Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 16 May 2023 08:18:21 +0200 Subject: [PATCH 1/2] add dangling judoc error --- .../Concrete/Data/Highlight/PrettyJudoc.hs | 6 ++-- src/Juvix/Compiler/Concrete/Language.hs | 12 +++---- src/Juvix/Compiler/Concrete/Print/Base.hs | 2 +- .../Concrete/Translation/FromSource.hs | 32 +++++++++++++------ src/Juvix/Parser/Error.hs | 22 +++++++++++++ tests/negative/DanglingJudoc.juvix | 5 +++ 6 files changed, 59 insertions(+), 20 deletions(-) create mode 100644 tests/negative/DanglingJudoc.juvix diff --git a/src/Juvix/Compiler/Concrete/Data/Highlight/PrettyJudoc.hs b/src/Juvix/Compiler/Concrete/Data/Highlight/PrettyJudoc.hs index 7b90625696..e65ca56bfa 100644 --- a/src/Juvix/Compiler/Concrete/Data/Highlight/PrettyJudoc.hs +++ b/src/Juvix/Compiler/Concrete/Data/Highlight/PrettyJudoc.hs @@ -38,16 +38,16 @@ ppDoc :: Members '[Reader Options] r => Scoped.AName -> Maybe Internal.Expressio ppDoc n ty j = do n' <- ppScoped n ty' <- fmap ((n' <+> kwColon) <+>) <$> mapM ppInternal ty - j' <- join <$> mapM ppJudoc j + j' <- mapM ppJudoc j return $ case (ty', j') of (Just jty', Just jj') -> return (jty' <+> line <> line <> jj') _ -> ty' <|> j' -ppJudoc :: forall r. Members '[Reader Options] r => Judoc 'Scoped -> Sem r (Maybe (Doc CodeAnn)) +ppJudoc :: forall r. Members '[Reader Options] r => Judoc 'Scoped -> Sem r (Doc CodeAnn) ppJudoc (Judoc bs) = do void (ask @Options) -- to suppress redundant constraint warning - mapM ppBlocks (nonEmpty bs) + ppBlocks bs where ppBlocks :: NonEmpty (JudocBlock 'Scoped) -> Sem r (Doc CodeAnn) ppBlocks = fmap vsep2 . mapM ppBlock diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 8088a636cf..4829713397 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -888,9 +888,9 @@ data ExpressionAtoms (s :: Stage) = ExpressionAtoms } newtype Judoc (s :: Stage) = Judoc - { _block :: [JudocBlock s] + { _block :: NonEmpty (JudocBlock s) } - deriving newtype (Semigroup, Monoid) + deriving newtype (Semigroup) deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (Judoc s) @@ -1170,12 +1170,9 @@ getLocExpressionType = case sing :: SStage s of SParsed -> getLoc SScoped -> getLoc -getJudocLoc :: Judoc s -> Maybe Interval -getJudocLoc = fmap getLocSpan . nonEmpty . (^. block) - instance SingI s => HasLoc (TypeSignature s) where getLoc TypeSignature {..} = - (_sigDoc >>= getJudocLoc) + (getLoc <$> _sigDoc) ?<> (getLoc <$> _sigPragmas) ?<> (getLoc <$> _sigBuiltin) ?<> (getLoc <$> _sigTerminating) @@ -1185,6 +1182,9 @@ instance SingI s => HasLoc (TypeSignature s) where instance HasLoc (Example s) where getLoc e = e ^. exampleLoc +instance HasLoc (Judoc s) where + getLoc (Judoc j) = getLocSpan j + instance HasLoc (JudocBlock s) where getLoc = \case JudocParagraph ls -> getLocSpan ls diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 790949f134..cf9f81337d 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -164,7 +164,7 @@ instance PrettyPrint (JudocParagraphLine 'Scoped) where instance PrettyPrint (Judoc 'Scoped) where ppCode :: forall r. Members '[ExactPrint, Reader Options] r => Judoc 'Scoped -> Sem r () - ppCode (Judoc blocks) = sequenceWith paragraphSep (map ppCode blocks) >> line + ppCode (Judoc blocks) = sequenceWith paragraphSep (fmap ppCode blocks) >> line where paragraphSep :: Sem r () paragraphSep = line >> noLoc P.ppJudocStart >> line diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 7d1d3b06e5..30bd158273 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -241,16 +241,25 @@ statement :: (Members '[Files, Error ParserError, PathResolver, InfoTableBuilder statement = P.label "" $ do void (optional stashJudoc) void (optional stashPragmas) - (StatementOperator <$> operatorSyntaxDef) - <|> (StatementOpenModule <$> openModule) - <|> (StatementImport <$> import_) - <|> (StatementInductive <$> inductiveDef Nothing) - <|> (StatementModule <$> moduleDef) - <|> (StatementAxiom <$> axiomDef Nothing) - <|> builtinStatement - <|> ( either StatementTypeSignature StatementFunctionClause + ms <- + optional + ( StatementOperator <$> operatorSyntaxDef + <|> StatementOpenModule <$> openModule + <|> StatementImport <$> import_ + <|> StatementInductive <$> inductiveDef Nothing + <|> StatementModule <$> moduleDef + <|> StatementAxiom <$> axiomDef Nothing + <|> builtinStatement + <|> either StatementTypeSignature StatementFunctionClause <$> auxTypeSigFunClause - ) + ) + case ms of + Just s -> return s + Nothing -> do + mj <- peekJudoc + case mj of + Nothing -> P.failure Nothing mempty + Just j -> P.lift . throw . ErrDanglingJudoc . DanglingJudoc $ j stashPragmas :: forall r. (Members '[InfoTableBuilder, PragmasStash, NameIdGen] r) => ParsecS r () stashPragmas = do @@ -276,7 +285,7 @@ stashJudoc = do P.lift (modify (<> Just b)) where judocBlocks :: ParsecS r (Judoc 'Parsed) - judocBlocks = Judoc <$> some judocBlock + judocBlocks = Judoc <$> some1 judocBlock judocBlock :: ParsecS r (JudocBlock 'Parsed) judocBlock = do @@ -519,6 +528,9 @@ universe = do Just (lvl, i') -> Universe (Just lvl) (i <> i') ) +peekJudoc :: (Member JudocStash r) => ParsecS r (Maybe (Judoc 'Parsed)) +peekJudoc = P.lift get + getJudoc :: (Member JudocStash r) => ParsecS r (Maybe (Judoc 'Parsed)) getJudoc = P.lift $ do j <- get diff --git a/src/Juvix/Parser/Error.hs b/src/Juvix/Parser/Error.hs index c57a6f5738..82485ea662 100644 --- a/src/Juvix/Parser/Error.hs +++ b/src/Juvix/Parser/Error.hs @@ -14,6 +14,7 @@ data ParserError | ErrTopModulePath TopModulePathError | ErrWrongTopModuleName WrongTopModuleName | ErrStdinOrFile StdinOrFileError + | ErrDanglingJudoc DanglingJudoc deriving stock (Show) instance ToGenericError ParserError where @@ -22,6 +23,7 @@ instance ToGenericError ParserError where ErrTopModulePath e -> genericError e ErrWrongTopModuleName e -> genericError e ErrStdinOrFile e -> genericError e + ErrDanglingJudoc e -> genericError e instance Pretty MegaparsecError where pretty (MegaparsecError b) = pretty (M.errorBundlePretty b) @@ -114,3 +116,23 @@ instance ToGenericError StdinOrFileError where _genericErrorMessage = prettyError "Neither JUVIX_FILE_OR_PROJECT nor --stdin option is choosen", _genericErrorIntervals = [] } + +newtype DanglingJudoc = DanglingJudoc + { _danglingJudoc :: Judoc 'Parsed + } + deriving stock (Show) + +instance ToGenericError DanglingJudoc where + genericError :: Member (Reader GenericOptions) r => DanglingJudoc -> Sem r GenericError + genericError DanglingJudoc {..} = do + opts <- fromGenericOptions <$> ask + let msg = "Dangling judoc comment:\n" <+> ppCode opts _danglingJudoc + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = AnsiText msg, + _genericErrorIntervals = [i] + } + where + i :: Interval + i = getLoc _danglingJudoc diff --git a/tests/negative/DanglingJudoc.juvix b/tests/negative/DanglingJudoc.juvix new file mode 100644 index 0000000000..685ad20823 --- /dev/null +++ b/tests/negative/DanglingJudoc.juvix @@ -0,0 +1,5 @@ +module DanglingJudoc; + +axiom A : Type; + +--- hello From 712f48ba9f5bf928f5e9f78fa10aa44b26a599bf Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 16 May 2023 08:21:15 +0200 Subject: [PATCH 2/2] add test --- test/Parsing/Negative.hs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/test/Parsing/Negative.hs b/test/Parsing/Negative.hs index 24bba9cec0..6e8b6f9dbf 100644 --- a/test/Parsing/Negative.hs +++ b/test/Parsing/Negative.hs @@ -100,5 +100,13 @@ filesErrorTests = $ \case ErrTopModulePath TopModulePathError {_topModulePathError = ErrMissingModule {}} -> Nothing + _ -> wrongError, + negTest + "Dangling Judoc comment" + $(mkRelDir ".") + $(mkRelFile "DanglingJudoc.juvix") + $ \case + ErrDanglingJudoc + DanglingJudoc {} -> Nothing _ -> wrongError ]