Skip to content

Commit

Permalink
Support extract-module-statements n
Browse files Browse the repository at this point in the history 
The argument `n` is the number of statements to drop from the module statements
  • Loading branch information
@paulcadman
paulcadman committed Apr 17, 2024
1 parent 37a79bb commit b21d592
Show file tree
Hide file tree
Showing 4 changed files with 39 additions and 19 deletions.
28 changes: 17 additions & 11 deletions src/Juvix/Compiler/Backend/Markdown/Data/MkJuvixBlockOptions.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,21 +10,22 @@ import Text.Megaparsec.Char.Lexer qualified as L
data MkJuvixBlockOptions
= MkJuvixBlockOptionsHide
| MkJuvixBlockOptionsShow
| MkJuvixBlockOptionsExtractModule
deriving stock (Eq, Ord, Bounded, Enum, Show)
| 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"

renderJuvixBlockOptions :: MkJuvixBlockOptions -> Text
renderJuvixBlockOptions = \case
MkJuvixBlockOptionsHide -> optionHide
MkJuvixBlockOptionsShow -> ""
MkJuvixBlockOptionsExtractModule -> optionExtractModuleStatements

parseJuvixBlockOptions :: Path Abs File -> Text -> Either MegaparsecError MkJuvixBlockOptions
parseJuvixBlockOptions p = mapLeft MegaparsecError . P.runParser parseOptions (toFilePath p)

Expand All @@ -39,6 +40,9 @@ lexeme = L.lexeme spaceConsumer
symbol :: Text -> Parser ()
symbol = void . L.symbol spaceConsumer

decimal :: Parser Int
decimal = lexeme L.decimal

parseOptions :: Parser MkJuvixBlockOptions
parseOptions = spaceConsumer >> parseHide <|> parseExtractModule <|> parseShow

Expand All @@ -49,7 +53,9 @@ parseHide :: Parser MkJuvixBlockOptions
parseHide = symbol optionHide $> MkJuvixBlockOptionsHide <* lexeme eof

parseExtractModule :: Parser MkJuvixBlockOptions
parseExtractModule =
parseExtractModule = do
symbol optionExtractModuleStatements
$> MkJuvixBlockOptionsExtractModule
<* lexeme eof
dropNum <- fromMaybe 0 <$> optional decimal
let res =
MkJuvixBlockOptionsExtractModule (JuvixBlockOptionsExtractModule dropNum)
return res <* lexeme eof
9 changes: 5 additions & 4 deletions src/Juvix/Compiler/Backend/Markdown/Translation/FromTyped/Source.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,8 @@ go fname = do
stmts' <-
let blockStmts = take n stmts
in case opts of
MkJuvixBlockOptionsExtractModule -> checkExtractModule j blockStmts
MkJuvixBlockOptionsExtractModule o ->
checkExtractModule j (o ^. juvixBlockOptionsExtractModuleDrop) blockStmts
_ -> return blockStmts

htmlStatements :: [Html] <-
Expand Down Expand Up @@ -185,10 +186,10 @@ go fname = do
modify @ProcessingState $ const newState
return _processingStateMk
where
checkExtractModule :: JuvixCodeBlock -> [Concrete.Statement 'Concrete.Scoped] -> Sem r [Concrete.Statement 'Concrete.Scoped]
checkExtractModule j xs = case xs of
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 (indModuleFilter (m ^. Concrete.moduleBody))
return (drop dropNum (indModuleFilter (m ^. Concrete.moduleBody)))
_ ->
throw
( ErrInvalidExtractModuleBlock
Expand Down
11 changes: 10 additions & 1 deletion tests/positive/Markdown/Test.juvix.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,11 +25,20 @@ 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 Foo;
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
Expand Down
10 changes: 7 additions & 3 deletions tests/positive/Markdown/markdown/Test.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,13 @@ The `extract-module-statements` attribute can be used to display only the statem

<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">type</span> <span id="YTest:8"><span class="annot"><a href="X#YTest:8"><span class="annot"><a href="X#YTest:8"><span class="ju-inductive">T</span></a></span></a></span></span> <span class="ju-keyword">:=</span> <span id="YTest:9"><span class="annot"><a href="X#YTest:9"><span class="annot"><a href="X#YTest:9"><span class="ju-constructor">t</span></a></span></a></span></span><span class="ju-delimiter">;</span></pre></code></pre>

You can pass a number to the `extract-module-statements` attribute to drop that number of statements from the start of the module.

<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="YTest:15"><span class="annot"><a href="X#YTest:15"><span class="annot"><a href="X#YTest:15"><span class="ju-function">a</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YTest:12"><span class="ju-inductive">T</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:13"><span class="ju-constructor">t</span></a></span><span class="ju-delimiter">;</span></pre></code></pre>

Commands like `typecheck` and `compile` can be used with Juvix Markdown files.

<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="YTest:12"><span class="annot"><a href="X#YTest:12"><span class="annot"><a href="X#YTest:12"><span class="ju-function">main</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YStdlib.System.IO.Base:1"><span class="ju-axiom">IO</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YStdlib.System.IO.String:2"><span class="ju-axiom">readLn</span></a></span> <span class="annot"><a href="X#YStdlib.System.IO.Nat:2"><span class="ju-function"><span class="ju-delimiter">(</span>printNatLn</span></a></span> <span class="annot"><a href="X#YStdlib.Function:1"><span class="ju-function">∘</span></a></span> <span class="annot"><a href="X#YTest:2"><span class="ju-function">fibonacci</span></a></span> <span class="annot"><a href="X#YStdlib.Function:1"><span class="ju-function">∘</span></a></span> <span class="annot"><a href="X#YStdlib.Data.Nat:2"><span class="ju-axiom">stringToNat</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span></pre></code></pre>
<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="YTest:17"><span class="annot"><a href="X#YTest:17"><span class="annot"><a href="X#YTest:17"><span class="ju-function">main</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YStdlib.System.IO.Base:1"><span class="ju-axiom">IO</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YStdlib.System.IO.String:2"><span class="ju-axiom">readLn</span></a></span> <span class="annot"><a href="X#YStdlib.System.IO.Nat:2"><span class="ju-function"><span class="ju-delimiter">(</span>printNatLn</span></a></span> <span class="annot"><a href="X#YStdlib.Function:1"><span class="ju-function">∘</span></a></span> <span class="annot"><a href="X#YTest:2"><span class="ju-function">fibonacci</span></a></span> <span class="annot"><a href="X#YStdlib.Function:1"><span class="ju-function">∘</span></a></span> <span class="annot"><a href="X#YStdlib.Data.Nat:2"><span class="ju-axiom">stringToNat</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span></pre></code></pre>

Other code blocks are not touched, e.g:

Expand Down Expand Up @@ -61,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,

<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">module</span> <span id="YTest:16"><span class="annot"><a href="X#YTest:16"><span class="annot"><a href="X#YTest:16"><span class="ju-var">move-to-left</span></a></span></a></span></span><span class="ju-delimiter">;</span><br/> <span class="ju-keyword">import</span> <span id="YStdlib.Data.Nat:0"><span class="annot"><a href="X#YStdlib.Data.Nat:0"><span class="annot"><a href="X#YStdlib.Data.Nat:0"><span class="ju-var">Stdlib<span class="ju-delimiter">.</span>Data<span class="ju-delimiter">.</span>Nat</span></a></span></a></span></span> <span class="ju-keyword">open</span><span class="ju-delimiter">;</span><br/> <span id="YTest:13"><span class="annot"><a href="X#YTest:13"><span class="annot"><a href="X#YTest:13"><span class="ju-function"><br/> add</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="X#YTest:14"><span class="ju-var">n</span></a></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-&gt;</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:2"><span class="ju-constructor">zero</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:14"><span class="ju-var">n</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:3"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="YTest:15"><span class="annot"><a href="X#YTest:15"><span class="annot"><a href="X#YTest:15"><span class="ju-var">m</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:3"><span class="ju-constructor">suc</span></a></span> <span class="annot"><a href="X#YTest:13"><span class="ju-function"><span class="ju-delimiter">(</span>add</span></a></span> <span class="annot"><a href="X#YTest:14"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#YTest:15"><span class="ju-var">m</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><span class="ju-keyword">end</span><span class="ju-delimiter">;</span></pre></code></pre>
<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">module</span> <span id="YTest:21"><span class="annot"><a href="X#YTest:21"><span class="annot"><a href="X#YTest:21"><span class="ju-var">move-to-left</span></a></span></a></span></span><span class="ju-delimiter">;</span><br/> <span class="ju-keyword">import</span> <span id="YStdlib.Data.Nat:0"><span class="annot"><a href="X#YStdlib.Data.Nat:0"><span class="annot"><a href="X#YStdlib.Data.Nat:0"><span class="ju-var">Stdlib<span class="ju-delimiter">.</span>Data<span class="ju-delimiter">.</span>Nat</span></a></span></a></span></span> <span class="ju-keyword">open</span><span class="ju-delimiter">;</span><br/> <span id="YTest:18"><span class="annot"><a href="X#YTest:18"><span class="annot"><a href="X#YTest:18"><span class="ju-function"><br/> add</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="X#YTest:19"><span class="ju-var">n</span></a></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-&gt;</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:2"><span class="ju-constructor">zero</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:19"><span class="ju-var">n</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:3"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="YTest:20"><span class="annot"><a href="X#YTest:20"><span class="annot"><a href="X#YTest:20"><span class="ju-var">m</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:3"><span class="ju-constructor">suc</span></a></span> <span class="annot"><a href="X#YTest:18"><span class="ju-function"><span class="ju-delimiter">(</span>add</span></a></span> <span class="annot"><a href="X#YTest:19"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#YTest:20"><span class="ju-var">m</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><span class="ju-keyword">end</span><span class="ju-delimiter">;</span></pre></code></pre>

is equivalent to

<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">module</span> <span id="YTest:21"><span class="annot"><a href="X#YTest:21"><span class="annot"><a href="X#YTest:21"><span class="ju-var">example-add</span></a></span></a></span></span><span class="ju-delimiter">;</span><br/> <span class="ju-keyword">import</span> <span id="YStdlib.Data.Nat:0"><span class="annot"><a href="X#YStdlib.Data.Nat:0"><span class="annot"><a href="X#YStdlib.Data.Nat:0"><span class="ju-var">Stdlib<span class="ju-delimiter">.</span>Data<span class="ju-delimiter">.</span>Nat</span></a></span></a></span></span> <span class="ju-keyword">open</span><span class="ju-delimiter">;</span><br/> <span id="YTest:17"><span class="annot"><a href="X#YTest:17"><span class="annot"><a href="X#YTest:17"><span class="ju-function"><br/> add</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-&gt;</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-&gt;</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span id="YTest:18"><span class="annot"><a href="X#YTest:18"><span class="annot"><a href="X#YTest:18"><span class="ju-var">n</span></a></span></a></span></span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:2"><span class="ju-constructor">zero</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:18"><span class="ju-var">n</span></a></span><br/> <span class="ju-keyword">|</span> <span id="YTest:19"><span class="annot"><a href="X#YTest:19"><span class="annot"><a href="X#YTest:19"><span class="ju-var">n</span></a></span></a></span></span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:3"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="YTest:20"><span class="annot"><a href="X#YTest:20"><span class="annot"><a href="X#YTest:20"><span class="ju-var">m</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:3"><span class="ju-constructor">suc</span></a></span> <span class="annot"><a href="X#YTest:17"><span class="ju-function"><span class="ju-delimiter">(</span>add</span></a></span> <span class="annot"><a href="X#YTest:19"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#YTest:20"><span class="ju-var">m</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><span class="ju-keyword">end</span><span class="ju-delimiter">;</span></pre></code></pre>
<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">module</span> <span id="YTest:26"><span class="annot"><a href="X#YTest:26"><span class="annot"><a href="X#YTest:26"><span class="ju-var">example-add</span></a></span></a></span></span><span class="ju-delimiter">;</span><br/> <span class="ju-keyword">import</span> <span id="YStdlib.Data.Nat:0"><span class="annot"><a href="X#YStdlib.Data.Nat:0"><span class="annot"><a href="X#YStdlib.Data.Nat:0"><span class="ju-var">Stdlib<span class="ju-delimiter">.</span>Data<span class="ju-delimiter">.</span>Nat</span></a></span></a></span></span> <span class="ju-keyword">open</span><span class="ju-delimiter">;</span><br/> <span id="YTest:22"><span class="annot"><a href="X#YTest:22"><span class="annot"><a href="X#YTest:22"><span class="ju-function"><br/> add</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-&gt;</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-&gt;</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:1"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span id="YTest:23"><span class="annot"><a href="X#YTest:23"><span class="annot"><a href="X#YTest:23"><span class="ju-var">n</span></a></span></a></span></span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:2"><span class="ju-constructor">zero</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:23"><span class="ju-var">n</span></a></span><br/> <span class="ju-keyword">|</span> <span id="YTest:24"><span class="annot"><a href="X#YTest:24"><span class="annot"><a href="X#YTest:24"><span class="ju-var">n</span></a></span></a></span></span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:3"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="YTest:25"><span class="annot"><a href="X#YTest:25"><span class="annot"><a href="X#YTest:25"><span class="ju-var">m</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Nat.Base:3"><span class="ju-constructor">suc</span></a></span> <span class="annot"><a href="X#YTest:22"><span class="ju-function"><span class="ju-delimiter">(</span>add</span></a></span> <span class="annot"><a href="X#YTest:24"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#YTest:25"><span class="ju-var">m</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><span class="ju-keyword">end</span><span class="ju-delimiter">;</span></pre></code></pre>

0 comments on commit b21d592

Please sign in to comment.