-
Notifications
You must be signed in to change notification settings - Fork 57
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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 <janmasrovira@gmail.com>
- Loading branch information
1 parent
75b5228
commit 52a3eed
Showing
13 changed files
with
339 additions
and
123 deletions.
There are no files selected for viewing
66 changes: 66 additions & 0 deletions
66
src/Juvix/Compiler/Backend/Markdown/Data/MkJuvixBlockOptions.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.