From 52a3eed162a130d49333e39893c0752cc021945f Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 18 Apr 2024 17:01:59 +0100 Subject: [PATCH] Support `extract-module-statements` attribute in juvix code blocks (#2734) This PR adds support for the `extract-module-statements` attribute for Juvix code blocks: So if you write something like the following block in a Juvix markdown file: ```` ```juvix extract-module-statements module Foo; type T := t; end; ``` ```` The statement `type T := t;` from the body of the module is rendered in the output. The `module Foo;` , and `end;` lines are not rendered in the output. A block with the `extract-module-statements` must contain a single local module statement and nothing else. An error is reported if this is not the case. The `extract-module-statements` attribute also takes an optional argument. It sets the number of statements from the module body to drop from the output. In the following example, the output will contain the single line `a : T := t;`. ```` ```juvix extract-module-statements 1 module Foo; type T := t; a : T := t; end; ``` ```` --------- Co-authored-by: Jan Mas Rovira --- .../Markdown/Data/MkJuvixBlockOptions.hs | 66 +++++++++++++++++ .../Compiler/Backend/Markdown/Data/Types.hs | 59 +++------------ src/Juvix/Compiler/Backend/Markdown/Error.hs | 38 ++++++++++ .../Markdown/Translation/FromTyped/Source.hs | 64 +++++++++++----- src/Juvix/Parser/Error.hs | 45 ++---------- src/Juvix/Parser/Error/Base.hs | 43 +++++++++++ test/BackendMarkdown/Negative.hs | 73 +++++++++++++++---- .../InvalidCodeBlockExtraAttribute.juvix.md | 9 +++ .../InvalidCodeBlockUnknownAttribute.juvix.md | 9 +++ ...InvalidExtractModuleBlockNoModule.juvix.md | 9 +++ ...idExtractModuleBlockNotJustModule.juvix.md | 12 +++ tests/positive/Markdown/Test.juvix.md | 19 ++++- tests/positive/Markdown/markdown/Test.md | 16 +++- 13 files changed, 339 insertions(+), 123 deletions(-) create mode 100644 src/Juvix/Compiler/Backend/Markdown/Data/MkJuvixBlockOptions.hs create mode 100644 src/Juvix/Parser/Error/Base.hs create mode 100644 tests/negative/Markdown/InvalidCodeBlockExtraAttribute.juvix.md create mode 100644 tests/negative/Markdown/InvalidCodeBlockUnknownAttribute.juvix.md create mode 100644 tests/negative/Markdown/InvalidExtractModuleBlockNoModule.juvix.md create mode 100644 tests/negative/Markdown/InvalidExtractModuleBlockNotJustModule.juvix.md diff --git a/src/Juvix/Compiler/Backend/Markdown/Data/MkJuvixBlockOptions.hs b/src/Juvix/Compiler/Backend/Markdown/Data/MkJuvixBlockOptions.hs new file mode 100644 index 000000000..b4953f8ae --- /dev/null +++ b/src/Juvix/Compiler/Backend/Markdown/Data/MkJuvixBlockOptions.hs @@ -0,0 +1,66 @@ +module Juvix.Compiler.Backend.Markdown.Data.MkJuvixBlockOptions where + +import Juvix.Parser.Error.Base +import Juvix.Prelude.Base +import Juvix.Prelude.Parsing hiding (runParser) +import Juvix.Prelude.Path +import Text.Megaparsec qualified as P +import Text.Megaparsec.Char.Lexer qualified as L + +data MkJuvixBlockOptions + = MkJuvixBlockOptionsHide + | MkJuvixBlockOptionsShow + | MkJuvixBlockOptionsExtractModule JuvixBlockOptionsExtractModule + deriving stock (Eq, Show) + +newtype JuvixBlockOptionsExtractModule = JuvixBlockOptionsExtractModule + { _juvixBlockOptionsExtractModuleDrop :: Int + } + deriving stock (Eq, Show) + +makeLenses ''JuvixBlockOptionsExtractModule + +optionExtractModuleStatements :: (IsString s) => s +optionExtractModuleStatements = "extract-module-statements" + +optionHide :: (IsString s) => s +optionHide = "hide" + +parseJuvixBlockOptions :: Path Abs File -> Text -> Either MegaparsecError MkJuvixBlockOptions +parseJuvixBlockOptions p = mapLeft MegaparsecError . P.runParser parseOptions (toFilePath p) + +type Parser = P.Parsec Void Text + +spaceConsumer :: Parser () +spaceConsumer = L.space space1 empty empty + +lexeme :: Parser a -> Parser a +lexeme = L.lexeme spaceConsumer + +symbol :: Text -> Parser () +symbol = void . L.symbol spaceConsumer + +decimal :: Parser Int +decimal = lexeme L.decimal + +parseOptions :: Parser MkJuvixBlockOptions +parseOptions = do + spaceConsumer + opts <- + parseHide + <|> parseExtractModule + <|> parseShow + eof + return opts + +parseShow :: Parser MkJuvixBlockOptions +parseShow = return MkJuvixBlockOptionsShow + +parseHide :: Parser MkJuvixBlockOptions +parseHide = symbol optionHide $> MkJuvixBlockOptionsHide + +parseExtractModule :: Parser MkJuvixBlockOptions +parseExtractModule = do + symbol optionExtractModuleStatements + dropNum <- fromMaybe 0 <$> optional decimal + return (MkJuvixBlockOptionsExtractModule (JuvixBlockOptionsExtractModule dropNum)) diff --git a/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs b/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs index 6ed14f423..f9e3fc8b9 100644 --- a/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs +++ b/src/Juvix/Compiler/Backend/Markdown/Data/Types.hs @@ -1,20 +1,20 @@ -module Juvix.Compiler.Backend.Markdown.Data.Types where +module Juvix.Compiler.Backend.Markdown.Data.Types + ( module Juvix.Compiler.Backend.Markdown.Data.Types, + module Juvix.Compiler.Backend.Markdown.Data.MkJuvixBlockOptions, + ) +where import Commonmark qualified as MK import Data.Text qualified as T +import Juvix.Compiler.Backend.Markdown.Data.MkJuvixBlockOptions import Juvix.Data.Loc import Juvix.Prelude hiding (Raw) import Juvix.Prelude.Pretty import Text.Show qualified as Show -newtype MkJuvixBlockOptions = MkJuvixBlockOptions - { _mkJuvixBlockOptionsHide :: Bool - } - deriving stock (Eq, Ord) - data JuvixCodeBlock = JuvixCodeBlock { _juvixCodeBlock :: Text, - _juvixCodeBlockOptions :: MkJuvixBlockOptions, + _juvixCodeBlockOptions :: Text, _juvixCodeBlockInterval :: Maybe Interval } deriving stock (Eq, Ord) @@ -26,33 +26,16 @@ data TextBlock = TextBlock deriving stock (Eq, Ord) makeLenses ''JuvixCodeBlock -makeLenses ''MkJuvixBlockOptions makeLenses ''TextBlock -defaultMkJuvixBlockOptions :: MkJuvixBlockOptions -defaultMkJuvixBlockOptions = - MkJuvixBlockOptions - { _mkJuvixBlockOptionsHide = False - } - instance Show TextBlock where show t = T.unpack (t ^. textBlock) -textJuvixBlockOptions :: MkJuvixBlockOptions -> Text -textJuvixBlockOptions opt = - T.intercalate " " $ - catMaybes - [ if opt ^. mkJuvixBlockOptionsHide then Just "hide" else Nothing - ] - -instance Show MkJuvixBlockOptions where - show opt = T.unpack (textJuvixBlockOptions opt) - textJuvixCodeBlock :: JuvixCodeBlock -> Text textJuvixCodeBlock cb = mconcat [ "```juvix", - textJuvixBlockOptions (cb ^. juvixCodeBlockOptions), + cb ^. juvixCodeBlockOptions, nl, cb ^. juvixCodeBlock, "```" @@ -83,19 +66,6 @@ instance Monoid TextBlock where } mappend = (<>) -instance Semigroup MkJuvixBlockOptions where - a <> b = - MkJuvixBlockOptions - { _mkJuvixBlockOptionsHide = a ^. mkJuvixBlockOptionsHide || b ^. mkJuvixBlockOptionsHide - } - -instance Monoid MkJuvixBlockOptions where - mempty = - MkJuvixBlockOptions - { _mkJuvixBlockOptionsHide = False - } - mappend = (<>) - instance Semigroup Mk where a <> MkNull = a MkNull <> a = a @@ -190,25 +160,20 @@ instance MK.IsInline TextBlock where toTextBlock t | otherwise = mempty -getJuvixBlockOptions :: Text -> MkJuvixBlockOptions -getJuvixBlockOptions = \case - "hide" -> mempty {_mkJuvixBlockOptionsHide = True} - _ -> mempty - nl' :: Mk nl' = toMK nl processCodeBlock :: Text -> Text -> Maybe Interval -> Mk processCodeBlock info t loc = - case T.splitOn " " (T.strip info) of - ("juvix" : opts) -> + case T.stripPrefix "juvix" (T.strip info) of + Just opts -> MkJuvixCodeBlock JuvixCodeBlock { _juvixCodeBlock = t, - _juvixCodeBlockOptions = foldMap getJuvixBlockOptions opts, + _juvixCodeBlockOptions = opts, _juvixCodeBlockInterval = loc } - _ -> + Nothing -> let b = "```" <> info <> t <> "```" in MkTextBlock TextBlock {_textBlock = b, _textBlockInterval = loc} diff --git a/src/Juvix/Compiler/Backend/Markdown/Error.hs b/src/Juvix/Compiler/Backend/Markdown/Error.hs index ad1ec48b4..a9cc15541 100644 --- a/src/Juvix/Compiler/Backend/Markdown/Error.hs +++ b/src/Juvix/Compiler/Backend/Markdown/Error.hs @@ -1,18 +1,24 @@ module Juvix.Compiler.Backend.Markdown.Error where +import Juvix.Compiler.Backend.Markdown.Data.Types import Juvix.Compiler.Concrete.Language import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Pretty +import Juvix.Parser.Error.Base import Juvix.Prelude data MarkdownBackendError = ErrInternalNoMarkdownInfo NoMarkdownInfoError | ErrNoJuvixCodeBlocks NoJuvixCodeBlocksError + | ErrInvalidExtractModuleBlock InvalidExtractModuleBlockError + | ErrInvalidCodeBlockAttribtues InvalidCodeBlockAttributesError deriving stock (Show) instance ToGenericError MarkdownBackendError where genericError = \case ErrInternalNoMarkdownInfo e -> genericError e ErrNoJuvixCodeBlocks e -> genericError e + ErrInvalidExtractModuleBlock e -> genericError e + ErrInvalidCodeBlockAttribtues e -> genericError e newtype NoMarkdownInfoError = NoMarkdownInfoError { _noMarkdownInfoFilepath :: Path Abs File @@ -49,3 +55,35 @@ instance ToGenericError NoJuvixCodeBlocksError where where i :: Interval i = singletonInterval . mkInitialLoc $ _noJuvixCodeBlocksErrorFilepath + +data InvalidExtractModuleBlockError = InvalidExtractModuleBlockError + { _invalidExtractModuleBlockErrorInterval :: Maybe Interval, + _invalidExtractModuleBlockErrorPath :: Path Abs File + } + deriving stock (Show) + +instance ToGenericError InvalidExtractModuleBlockError where + genericError InvalidExtractModuleBlockError {..} = do + let msg :: Doc Ann + msg = "Juvix code blocks with attribute" <+> optionExtractModuleStatements <+> "must contain a single local module" + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [i] + } + where + i :: Interval + i = + fromMaybe + (singletonInterval (mkInitialLoc (_invalidExtractModuleBlockErrorPath))) + _invalidExtractModuleBlockErrorInterval + +newtype InvalidCodeBlockAttributesError = InvalidCodeBlockAttributesError + { _invalidCodeBlockAttributesErrorMegaparsecError :: MegaparsecError + } + deriving stock (Show) + +instance ToGenericError InvalidCodeBlockAttributesError where + genericError InvalidCodeBlockAttributesError {..} = + genericError _invalidCodeBlockAttributesErrorMegaparsecError diff --git a/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs b/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs index 80fe7851d..7e652651d 100644 --- a/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs +++ b/src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs @@ -86,7 +86,7 @@ fromJuvixMarkdown opts = do _processingStateStmtsSeparation = sepr, _processingStateStmts = indModuleFilter $ m ^. Concrete.moduleBody } - (_, r) <- runState st . runReader htmlOptions . runReader opts $ go + (_, r) <- runState st . runReader htmlOptions . runReader opts $ go fname return $ MK.toPlainText r Nothing -> throw @@ -104,34 +104,49 @@ go :: ( Members '[ Reader HtmlRender.HtmlOptions, Reader ProcessJuvixBlocksArgs, - State ProcessingState + State ProcessingState, + Error MarkdownBackendError ] r ) => + Path Abs File -> Sem r Mk -go = do +go fname = do stmts <- gets @ProcessingState (^. processingStateStmts) sepr <- gets @ProcessingState (^. processingStateStmtsSeparation) mk <- gets @ProcessingState (^. processingStateMk) - case (sepr, stmts) of - ([], _) -> return mk - ((n : ns), _) -> do + case sepr of + [] -> return mk + (n : ns) -> do case mk of MkNull -> return mk MkTextBlock _ -> return mk MkConcat l r -> do modify (set processingStateMk l) - lS <- go + lS <- go fname modify (set processingStateMk r) - MkConcat lS <$> go + MkConcat lS <$> go fname MkJuvixCodeBlock j -> do + opts <- case parseJuvixBlockOptions fname (j ^. juvixCodeBlockOptions) of + Left e -> + throw + ( ErrInvalidCodeBlockAttribtues + (InvalidCodeBlockAttributesError e) + ) + Right o -> return o + m <- asks @ProcessJuvixBlocksArgs (^. processJuvixBlocksArgsModule) isFirstBlock <- gets @ProcessingState (^. processingStateFirstBlock) - let stmts' = take n stmts + stmts' <- + let blockStmts = take n stmts + in case opts of + MkJuvixBlockOptionsExtractModule o -> + checkExtractModule j (o ^. juvixBlockOptionsExtractModuleDrop) blockStmts + _ -> return blockStmts htmlStatements :: [Html] <- mapM (\s -> goRender s <> pure htmlSemicolon) stmts' @@ -153,15 +168,14 @@ go = do Text.intercalate "\n\n" $ map (toStrict . Html.renderHtml) htmlStatements - let _processingStateMk = - if j ^. juvixCodeBlockOptions . mkJuvixBlockOptionsHide - then MkNull - else - MkTextBlock - TextBlock - { _textBlock = Text.replace "\n" "
" resHtml, - _textBlockInterval = j ^. juvixCodeBlockInterval - } + let _processingStateMk = case opts of + MkJuvixBlockOptionsHide -> MkNull + _ -> + MkTextBlock + TextBlock + { _textBlock = Text.replace "\n" "
" resHtml, + _textBlockInterval = j ^. juvixCodeBlockInterval + } let newState = ProcessingState { _processingStateFirstBlock = False, @@ -171,6 +185,20 @@ go = do } modify @ProcessingState $ const newState return _processingStateMk + where + checkExtractModule :: JuvixCodeBlock -> Int -> [Concrete.Statement 'Concrete.Scoped] -> Sem r [Concrete.Statement 'Concrete.Scoped] + checkExtractModule j dropNum xs = case xs of + [Concrete.StatementModule m] -> do + return (drop dropNum (indModuleFilter (m ^. Concrete.moduleBody))) + _ -> + throw + ( ErrInvalidExtractModuleBlock + ( InvalidExtractModuleBlockError + { _invalidExtractModuleBlockErrorPath = fname, + _invalidExtractModuleBlockErrorInterval = j ^. juvixCodeBlockInterval + } + ) + ) goRender :: (Concrete.PrettyPrint c, Members '[Reader HtmlRender.HtmlOptions, Reader ProcessJuvixBlocksArgs] r) => diff --git a/src/Juvix/Parser/Error.hs b/src/Juvix/Parser/Error.hs index bd2267020..8e2fa0f1f 100644 --- a/src/Juvix/Parser/Error.hs +++ b/src/Juvix/Parser/Error.hs @@ -1,4 +1,8 @@ -module Juvix.Parser.Error where +module Juvix.Parser.Error + ( module Juvix.Parser.Error, + module Juvix.Parser.Error.Base, + ) +where import Commonmark qualified as MK import Juvix.Compiler.Backend.Markdown.Error @@ -7,9 +11,9 @@ import Juvix.Compiler.Concrete.Pretty.Options (fromGenericOptions) import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Pretty import Juvix.Compiler.Pipeline.Loader.PathResolver.Error import Juvix.Extra.Paths +import Juvix.Parser.Error.Base import Juvix.Prelude import Text.Megaparsec qualified as M -import Text.Megaparsec.Error (errorOffset) import Text.Parsec.Error qualified as P import Text.Parsec.Pos qualified as P @@ -33,43 +37,6 @@ instance ToGenericError ParserError where ErrDanglingJudoc e -> genericError e ErrMarkdownBackend e -> genericError e -instance Pretty MegaparsecError where - pretty (MegaparsecError b) = pretty (M.errorBundlePretty b) - -instance HasLoc MegaparsecError where - getLoc (MegaparsecError b) = singletonInterval (mkLoc offset sourcePos) - where - state :: M.PosState Text - state = M.bundlePosState b - offset = errorOffset (head (M.bundleErrors b)) - - sourcePos :: M.SourcePos - sourcePos = - (snd . head . fst) - (M.attachSourcePos errorOffset (M.bundleErrors b) state) - -newtype MegaparsecError = MegaparsecError - { _megaParsecError :: M.ParseErrorBundle Text Void - } - deriving stock (Show) - -instance ToGenericError MegaparsecError where - genericError e = - return - GenericError - { _genericErrorLoc = i, - _genericErrorMessage = mkAnsiText $ pretty @_ @AnsiStyle e, - _genericErrorIntervals = [i] - } - where - i = getLoc e - --- | Use only for debugging -fromMegaParsecError :: Either MegaparsecError a -> a -fromMegaParsecError = \case - Left e -> error (prettyText e) - Right a -> a - newtype CommonmarkError = CommonmarkError { _commonMarkError :: MK.ParseError } diff --git a/src/Juvix/Parser/Error/Base.hs b/src/Juvix/Parser/Error/Base.hs new file mode 100644 index 000000000..1232dc2a2 --- /dev/null +++ b/src/Juvix/Parser/Error/Base.hs @@ -0,0 +1,43 @@ +module Juvix.Parser.Error.Base where + +import Juvix.Prelude +import Juvix.Prelude.Pretty +import Text.Megaparsec qualified as M +import Text.Megaparsec.Error (errorOffset) + +instance Pretty MegaparsecError where + pretty (MegaparsecError b) = pretty (M.errorBundlePretty b) + +instance HasLoc MegaparsecError where + getLoc (MegaparsecError b) = singletonInterval (mkLoc offset sourcePos) + where + state :: M.PosState Text + state = M.bundlePosState b + offset = errorOffset (head (M.bundleErrors b)) + + sourcePos :: M.SourcePos + sourcePos = + (snd . head . fst) + (M.attachSourcePos errorOffset (M.bundleErrors b) state) + +newtype MegaparsecError = MegaparsecError + { _megaParsecError :: M.ParseErrorBundle Text Void + } + deriving stock (Show) + +instance ToGenericError MegaparsecError where + genericError e = + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = mkAnsiText $ pretty @_ @AnsiStyle e, + _genericErrorIntervals = [i] + } + where + i = getLoc e + +-- | Use only for debugging +fromMegaParsecError :: Either MegaparsecError a -> a +fromMegaParsecError = \case + Left e -> error (prettyText e) + Right a -> a diff --git a/test/BackendMarkdown/Negative.hs b/test/BackendMarkdown/Negative.hs index 2617fb9d4..0cb4b9a47 100644 --- a/test/BackendMarkdown/Negative.hs +++ b/test/BackendMarkdown/Negative.hs @@ -2,6 +2,9 @@ module BackendMarkdown.Negative where import Base import Juvix.Compiler.Backend.Markdown.Error +import Juvix.Compiler.Backend.Markdown.Translation.FromTyped.Source +import Juvix.Compiler.Concrete qualified as Concrete +import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper import Juvix.Parser.Error type FailMsg = String @@ -10,7 +13,7 @@ data NegTest = NegTest { _name :: String, _relDir :: Path Rel Dir, _file :: Path Rel File, - _checkErr :: ParserError -> Maybe FailMsg + _checkErr :: JuvixError -> Maybe FailMsg } testDescr :: NegTest -> TestDescr @@ -22,12 +25,33 @@ testDescr NegTest {..} = _testRoot = tRoot, _testAssertion = Single $ do entryPoint <- testDefaultEntryPointIO tRoot file' - result <- testTaggedLockedToIO (runIOEither entryPoint upToParsing) - case mapLeft fromJuvixError result of - Left (Just err) -> whenJust (_checkErr err) assertFailure - Right _ -> assertFailure "Unexpected success." - Left Nothing -> assertFailure "Unexpected error." + result <- testTaggedLockedToIO (runIOEither entryPoint upToScoping) + case result of + Left err -> whenJust (_checkErr err) assertFailure + Right (_, pipelineRes) -> checkResult pipelineRes } + where + checkResult :: PipelineResult Scoper.ScoperResult -> IO () + checkResult PipelineResult {..} = do + let m = _pipelineResult ^. Scoper.resultModule + opts = + ProcessJuvixBlocksArgs + { _processJuvixBlocksArgsConcreteOpts = Concrete.defaultOptions, + _processJuvixBlocksArgsUrlPrefix = "", + _processJuvixBlocksArgsIdPrefix = "", + _processJuvixBlocksArgsNoPath = True, + _processJuvixBlocksArgsExt = ".html", + _processJuvixBlocksArgsStripPrefix = "", + _processJuvixBlocksArgsComments = Comments mempty, + _processJuvixBlocksArgsFolderStructure = False, + _processJuvixBlocksArgsModule = m, + _processJuvixBlocksArgsOutputDir = + root $(mkRelDir "markdown") + } + res = fromJuvixMarkdown' opts + case res of + Left err -> whenJust (_checkErr (JuvixError err)) assertFailure + Right _ -> assertFailure "Unexpected success" allTests :: TestTree allTests = @@ -38,8 +62,8 @@ allTests = root :: Path Abs Dir root = relToProject $(mkRelDir "tests/negative") -wrongError :: Maybe FailMsg -wrongError = Just "Incorrect error" +wrongError :: JuvixError -> Maybe FailMsg +wrongError e = Just ("unexpected error: " <> unpack (renderTextDefault e)) tests :: [NegTest] tests = @@ -47,14 +71,35 @@ tests = "Empty file" $(mkRelDir "Markdown") $(mkRelFile "Empty.juvix.md") - $ \case - ErrMarkdownBackend (ErrNoJuvixCodeBlocks _) -> Nothing - _ -> wrongError, + $ \e -> case fromJuvixError e of + Just (ErrMarkdownBackend (ErrNoJuvixCodeBlocks _)) -> Nothing + _ -> wrongError e, NegTest "No Juvix code blocks" $(mkRelDir "Markdown") $(mkRelFile "NoJuvixCodeBlocks.juvix.md") - $ \case - ErrMarkdownBackend (ErrNoJuvixCodeBlocks _) -> Nothing - _ -> wrongError + $ \e -> case fromJuvixError e of + Just (ErrMarkdownBackend (ErrNoJuvixCodeBlocks _)) -> Nothing + _ -> wrongError e, + NegTest + "extract-module-statements with no local module" + $(mkRelDir "Markdown") + $(mkRelFile "InvalidExtractModuleBlockNoModule.juvix.md") + $ \e -> case fromJuvixError e of + Just (ErrInvalidExtractModuleBlock _) -> Nothing + _ -> wrongError e, + NegTest + "extract-module-statements with no local module" + $(mkRelDir "Markdown") + $(mkRelFile "InvalidExtractModuleBlockNotJustModule.juvix.md") + $ \e -> case fromJuvixError e of + Just (ErrInvalidExtractModuleBlock _) -> Nothing + _ -> wrongError e, + NegTest + "code block with both hide and extract-module-statements" + $(mkRelDir "Markdown") + $(mkRelFile "InvalidCodeBlockExtraAttribute.juvix.md") + $ \e -> case fromJuvixError e of + Just (ErrInvalidCodeBlockAttribtues _) -> Nothing + _ -> wrongError e ] diff --git a/tests/negative/Markdown/InvalidCodeBlockExtraAttribute.juvix.md b/tests/negative/Markdown/InvalidCodeBlockExtraAttribute.juvix.md new file mode 100644 index 000000000..056f7a359 --- /dev/null +++ b/tests/negative/Markdown/InvalidCodeBlockExtraAttribute.juvix.md @@ -0,0 +1,9 @@ +# Title + +```juvix +module InvalidExtractModuleBlockExtraAttribute; +``` + +```juvix hide extract-module-statements +type T := t; +``` diff --git a/tests/negative/Markdown/InvalidCodeBlockUnknownAttribute.juvix.md b/tests/negative/Markdown/InvalidCodeBlockUnknownAttribute.juvix.md new file mode 100644 index 000000000..e091b3d25 --- /dev/null +++ b/tests/negative/Markdown/InvalidCodeBlockUnknownAttribute.juvix.md @@ -0,0 +1,9 @@ +# Title + +```juvix +module InvalidExtractModuleBlockUnknownAttribute; +``` + +```juvix invalid-attribute +type T := t; +``` diff --git a/tests/negative/Markdown/InvalidExtractModuleBlockNoModule.juvix.md b/tests/negative/Markdown/InvalidExtractModuleBlockNoModule.juvix.md new file mode 100644 index 000000000..bcb6b4142 --- /dev/null +++ b/tests/negative/Markdown/InvalidExtractModuleBlockNoModule.juvix.md @@ -0,0 +1,9 @@ +# Title + +```juvix +module InvalidExtractModuleBlockNoModule; +``` + +```juvix extract-module-statements +type T := t; +``` diff --git a/tests/negative/Markdown/InvalidExtractModuleBlockNotJustModule.juvix.md b/tests/negative/Markdown/InvalidExtractModuleBlockNotJustModule.juvix.md new file mode 100644 index 000000000..a54edf9da --- /dev/null +++ b/tests/negative/Markdown/InvalidExtractModuleBlockNotJustModule.juvix.md @@ -0,0 +1,12 @@ +# Title + +```juvix +module InvalidExtractModuleBlockNotJustModule; +``` + +```juvix extract-module-statements +module Inner; + type T1 := t1; +end; +type T2 := t2; +``` diff --git a/tests/positive/Markdown/Test.juvix.md b/tests/positive/Markdown/Test.juvix.md index d9d76cb7c..7146c7971 100644 --- a/tests/positive/Markdown/Test.juvix.md +++ b/tests/positive/Markdown/Test.juvix.md @@ -22,6 +22,23 @@ fib : Nat → Nat → Nat → Nat fibonacci (n : Nat) : Nat := fib n 0 1; ``` +The `extract-module-statements` attribute can be used to display only the statements contained in a module in the output. + +```juvix extract-module-statements +module Foo1; + type T := t; +end; +``` + +You can pass a number to the `extract-module-statements` attribute to drop that number of statements from the start of the module. + +```juvix extract-module-statements 1 +module Foo2; + type T := t; + a : T := t; +end; +``` + Commands like `typecheck` and `compile` can be used with Juvix Markdown files. ```juvix @@ -89,4 +106,4 @@ We also use other markup for documentation such as: | n zero := n | n (suc m) := suc (add n m); end; - ``` \ No newline at end of file + ``` diff --git a/tests/positive/Markdown/markdown/Test.md b/tests/positive/Markdown/markdown/Test.md index 0a45d0a79..50f1e7793 100644 --- a/tests/positive/Markdown/markdown/Test.md +++ b/tests/positive/Markdown/markdown/Test.md @@ -9,11 +9,19 @@ Certain blocks can be hidden from the output by adding the `hide` attribute, as -
fib : Nat → Nat → Nat → Nat
  | zero x1 _ := x1
  | (suc n) x1 x2 := fib n x2 (x1 + x2);

fibonacci (n : Nat) : Nat := fib n 0 1;
+
fib : Nat → Nat → Nat → Nat
  | zero x1 _ := x1
  | (suc n) x1 x2 := fib n x2 (x1 + x2);

fibonacci (n : Nat) : Nat := fib n 0 1;
+ +The `extract-module-statements` attribute can be used to display only the statements contained in a module in the output. + +
type T := t;
+ +You can pass a number to the `extract-module-statements` attribute to drop that number of statements from the start of the module. + +
a : T := t;
Commands like `typecheck` and `compile` can be used with Juvix Markdown files. -
main : IO := readLn (printNatLn ∘ fibonacci ∘ stringToNat);
+
main : IO := readLn (printNatLn ∘ fibonacci ∘ stringToNat);
Other code blocks are not touched, e.g: @@ -57,8 +65,8 @@ We also use other markup for documentation such as: Initial function arguments that match variables or wildcards in all clauses can be moved to the left of the colon in the function definition. For example, - 
module move-to-left;
  import Stdlib.Data.Nat open;
  
  add (n : Nat) : Nat -> Nat
    | zero := n
    | (suc m) := suc (add n m);
end;
+ 
module move-to-left;
  import Stdlib.Data.Nat open;
  
  add (n : Nat) : Nat -> Nat
    | zero := n
    | (suc m) := suc (add n m);
end;
is equivalent to - 
module example-add;
  import Stdlib.Data.Nat open;
  
  add : Nat -> Nat -> Nat
    | n zero := n
    | n (suc m) := suc (add n m);
end;
+ 
module example-add;
  import Stdlib.Data.Nat open;
  
  add : Nat -> Nat -> Nat
    | n zero := n
    | n (suc m) := suc (add n m);
end;