mirror of
https://github.com/anoma/juvix.git
synced 2024-08-16 03:30:37 +03:00
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>
This commit is contained in:
Paul Cadman
GitHub
parent
75b5228258
commit
52a3eed162
@ -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))
|
||||
@ -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}
|
||||
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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" "<br/>" resHtml,
|
||||
_textBlockInterval = j ^. juvixCodeBlockInterval
|
||||
}
|
||||
let _processingStateMk = case opts of
|
||||
MkJuvixBlockOptionsHide -> MkNull
|
||||
_ ->
|
||||
MkTextBlock
|
||||
TextBlock
|
||||
{ _textBlock = Text.replace "\n" "<br/>" 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) =>
|
||||
|
||||
@ -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
|
||||
}
|
||||
|
||||
43
src/Juvix/Parser/Error/Base.hs
Normal file
43
src/Juvix/Parser/Error/Base.hs
Normal file
@ -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
|
||||
@ -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
|
||||
]
|
||||
|
||||
@ -0,0 +1,9 @@
|
||||
# Title
|
||||
|
||||
```juvix
|
||||
module InvalidExtractModuleBlockExtraAttribute;
|
||||
```
|
||||
|
||||
```juvix hide extract-module-statements
|
||||
type T := t;
|
||||
```
|
||||
@ -0,0 +1,9 @@
|
||||
# Title
|
||||
|
||||
```juvix
|
||||
module InvalidExtractModuleBlockUnknownAttribute;
|
||||
```
|
||||
|
||||
```juvix invalid-attribute
|
||||
type T := t;
|
||||
```
|
||||
@ -0,0 +1,9 @@
|
||||
# Title
|
||||
|
||||
```juvix
|
||||
module InvalidExtractModuleBlockNoModule;
|
||||
```
|
||||
|
||||
```juvix extract-module-statements
|
||||
type T := t;
|
||||
```
|
||||
@ -0,0 +1,12 @@
|
||||
# Title
|
||||
|
||||
```juvix
|
||||
module InvalidExtractModuleBlockNotJustModule;
|
||||
```
|
||||
|
||||
```juvix extract-module-statements
|
||||
module Inner;
|
||||
type T1 := t1;
|
||||
end;
|
||||
type T2 := t2;
|
||||
```
|
||||
@ -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;
|
||||
```
|
||||
```
|
||||
|
||||
@ -9,11 +9,19 @@ Certain blocks can be hidden from the output by adding the `hide` attribute, as
|
||||
|
||||
|
||||
|
||||
<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="YTest:1"><span class="annot"><a href="X#YTest:1"><span class="annot"><a href="X#YTest:1"><span class="ju-function">fib</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">→</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">→</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">→</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 id="YTest:4"><span class="annot"><a href="X#YTest:4"><span class="annot"><a href="X#YTest:4"><span class="ju-var">x1</span></a></span></a></span></span> <span class="ju-keyword">_</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:4"><span class="ju-var">x1</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:5"><span class="annot"><a href="X#YTest:5"><span class="annot"><a href="X#YTest:5"><span class="ju-var">n</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span id="YTest:6"><span class="annot"><a href="X#YTest:6"><span class="annot"><a href="X#YTest:6"><span class="ju-var">x1</span></a></span></a></span></span> <span id="YTest:7"><span class="annot"><a href="X#YTest:7"><span class="annot"><a href="X#YTest:7"><span class="ju-var">x2</span></a></span></a></span></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:1"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#YTest:5"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#YTest:7"><span class="ju-var">x2</span></a></span> <span class="annot"><a href="X#YTest:6"><span class="ju-var"><span class="ju-delimiter">(</span>x1</span></a></span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Trait.Natural:3"><span class="ju-function">+</span></a></span> <span class="annot"><a href="X#YTest:7"><span class="ju-var">x2</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><br/><span id="YTest:2"><span class="annot"><a href="X#YTest:2"><span class="annot"><a href="X#YTest:2"><span class="ju-function">fibonacci</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="X#YTest:8"><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">:=</span> <span class="annot"><a href="X#YTest:1"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#YTest:8"><span class="ju-var">n</span></a></span> <span class="ju-number">0</span> <span class="ju-number">1</span><span class="ju-delimiter">;</span></pre></code></pre>
|
||||
<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="YTest:1"><span class="annot"><a href="X#YTest:1"><span class="annot"><a href="X#YTest:1"><span class="ju-function">fib</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">→</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">→</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">→</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 id="YTest:3"><span class="annot"><a href="X#YTest:3"><span class="annot"><a href="X#YTest:3"><span class="ju-var">x1</span></a></span></a></span></span> <span class="ju-keyword">_</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:3"><span class="ju-var">x1</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:4"><span class="annot"><a href="X#YTest:4"><span class="annot"><a href="X#YTest:4"><span class="ju-var">n</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span id="YTest:5"><span class="annot"><a href="X#YTest:5"><span class="annot"><a href="X#YTest:5"><span class="ju-var">x1</span></a></span></a></span></span> <span id="YTest:6"><span class="annot"><a href="X#YTest:6"><span class="annot"><a href="X#YTest:6"><span class="ju-var">x2</span></a></span></a></span></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YTest:1"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#YTest:4"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#YTest:6"><span class="ju-var">x2</span></a></span> <span class="annot"><a href="X#YTest:5"><span class="ju-var"><span class="ju-delimiter">(</span>x1</span></a></span> <span class="annot"><a href="X#YJuvix.Builtin.V1.Trait.Natural:3"><span class="ju-function">+</span></a></span> <span class="annot"><a href="X#YTest:6"><span class="ju-var">x2</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><br/><span id="YTest:2"><span class="annot"><a href="X#YTest:2"><span class="annot"><a href="X#YTest:2"><span class="ju-function">fibonacci</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="X#YTest:7"><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">:=</span> <span class="annot"><a href="X#YTest:1"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#YTest:7"><span class="ju-var">n</span></a></span> <span class="ju-number">0</span> <span class="ju-number">1</span><span class="ju-delimiter">;</span></pre></code></pre>
|
||||
|
||||
The `extract-module-statements` attribute can be used to display only the statements contained in a module in the output.
|
||||
|
||||
<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:3"><span class="annot"><a href="X#YTest:3"><span class="annot"><a href="X#YTest:3"><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:
|
||||
|
||||
@ -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,
|
||||
|
||||
<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">module</span> <span id="YTest:12"><span class="annot"><a href="X#YTest:12"><span class="annot"><a href="X#YTest:12"><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:9"><span class="annot"><a href="X#YTest:9"><span class="annot"><a href="X#YTest:9"><span class="ju-function"><br/> add</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="X#YTest:10"><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">-></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:10"><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:11"><span class="annot"><a href="X#YTest:11"><span class="annot"><a href="X#YTest:11"><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:9"><span class="ju-function"><span class="ju-delimiter">(</span>add</span></a></span> <span class="annot"><a href="X#YTest:10"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#YTest:11"><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">-></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:17"><span class="annot"><a href="X#YTest:17"><span class="annot"><a href="X#YTest:17"><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: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-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">-></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">-></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:14"><span class="annot"><a href="X#YTest:14"><span class="annot"><a href="X#YTest:14"><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:14"><span class="ju-var">n</span></a></span><br/> <span class="ju-keyword">|</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">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:16"><span class="annot"><a href="X#YTest:16"><span class="annot"><a href="X#YTest:16"><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:15"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#YTest:16"><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">-></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">-></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>
|
||||
|
||||
Loading…
Reference in New Issue
Block a user