diff --git a/app/Commands/Html.hs b/app/Commands/Html.hs
index b94a49d1bd..fe8e739c2e 100644
--- a/app/Commands/Html.hs
+++ b/app/Commands/Html.hs
@@ -1,7 +1,7 @@
module Commands.Html where
import Juvix.Prelude hiding (Doc)
-import Juvix.Syntax.Concrete.Scoped.Pretty.Html
+import Juvix.Syntax.Concrete.Scoped.Pretty.Html hiding (HtmlOptions)
import Options.Applicative
data HtmlOptions = HtmlOptions
diff --git a/app/Commands/Internal.hs b/app/Commands/Internal.hs
index c568e2e8e5..2c177a22f6 100644
--- a/app/Commands/Internal.hs
+++ b/app/Commands/Internal.hs
@@ -3,10 +3,12 @@ module Commands.Internal
module Commands.Internal.MicroJuvix,
module Commands.Internal.Parse,
module Commands.Internal.Scope,
+ module Commands.Internal.Doc,
module Commands.Internal.Termination,
)
where
+import Commands.Internal.Doc
import Commands.Internal.MicroJuvix
import Commands.Internal.Parse
import Commands.Internal.Scope
@@ -24,6 +26,7 @@ data InternalCommand
| Parse ParseOptions
| Scope ScopeOptions
| Termination TerminationCommand
+ | Doc DocOptions
parseInternalCommand :: Parser InternalCommand
parseInternalCommand =
@@ -35,12 +38,20 @@ parseInternalCommand =
commandMiniHaskell,
commandMonoJuvix,
commandParse,
+ commandDoc,
commandScope,
commandShowRoot,
commandTermination
]
)
+commandDoc :: Mod CommandFields InternalCommand
+commandDoc =
+ command "doc" $
+ info
+ (Doc <$> parseDoc)
+ (progDesc "Generate documentation")
+
commandHighlight :: Mod CommandFields InternalCommand
commandHighlight =
command "highlight" $
diff --git a/app/Commands/Internal/Doc.hs b/app/Commands/Internal/Doc.hs
new file mode 100644
index 0000000000..a2eb19f10e
--- /dev/null
+++ b/app/Commands/Internal/Doc.hs
@@ -0,0 +1,30 @@
+module Commands.Internal.Doc where
+
+import Juvix.Prelude hiding (Doc)
+import Options.Applicative
+
+data DocOptions = DocOptions
+ { _docOutputDir :: FilePath,
+ _docOpen :: Bool
+ }
+
+makeLenses ''DocOptions
+
+parseDoc :: Parser DocOptions
+parseDoc = do
+ _docOutputDir <-
+ option
+ str
+ ( long "output-dir"
+ <> metavar "DIR"
+ <> value "doc"
+ <> showDefault
+ <> help "html output directory"
+ <> action "directory"
+ )
+ _docOpen <-
+ switch
+ ( long "open"
+ <> help "open the documentation after generating it"
+ )
+ pure DocOptions {..}
diff --git a/app/Main.hs b/app/Main.hs
index e161999fb4..2f5052f840 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -9,6 +9,7 @@ import Data.HashMap.Strict qualified as HashMap
import Juvix.Analysis.Scoping.Scoper qualified as Scoper
import Juvix.Analysis.Termination qualified as Termination
import Juvix.Analysis.TypeChecking qualified as MicroTyped
+import Juvix.Documentation.Compiler qualified as Doc
import Juvix.Parsing.Parser qualified as Parser
import Juvix.Pipeline
import Juvix.Prelude hiding (Doc)
@@ -19,7 +20,7 @@ import Juvix.Syntax.Abstract.Pretty qualified as Abstract
import Juvix.Syntax.Concrete.Scoped.Highlight qualified as Highlight
import Juvix.Syntax.Concrete.Scoped.InfoTable qualified as Scoper
import Juvix.Syntax.Concrete.Scoped.Pretty qualified as Scoper
-import Juvix.Syntax.Concrete.Scoped.Pretty.Html
+import Juvix.Syntax.Concrete.Scoped.Pretty.Html qualified as Html
import Juvix.Syntax.MicroJuvix.MicroJuvixArityResult qualified as MicroArity
import Juvix.Syntax.MicroJuvix.Pretty qualified as Micro
import Juvix.Syntax.MiniHaskell.Pretty qualified as MiniHaskell
@@ -32,6 +33,7 @@ import Juvix.Translation.ScopedToAbstract qualified as Abstract
import Juvix.Utils.Version (runDisplayVersion)
import Options.Applicative
import System.Environment (getProgName)
+import System.Process qualified as Process
import Text.Show.Pretty hiding (Html)
juvixYamlFile :: FilePath
@@ -106,7 +108,7 @@ runCommand cmdWithOpts = do
Html HtmlOptions {..} -> do
res <- runPipeline (upToScoping entryPoint)
let m = head (res ^. Scoper.resultModules)
- embed (genHtml Scoper.defaultOptions _htmlRecursive _htmlTheme _htmlOutputDir _htmlPrintMetadata m)
+ embed (Html.genHtml Scoper.defaultOptions _htmlRecursive _htmlTheme _htmlOutputDir _htmlPrintMetadata m)
(Internal cmd') -> case cmd' of
Highlight -> do
res <- runPipelineEither (upToScoping entryPoint)
@@ -137,6 +139,14 @@ runCommand cmdWithOpts = do
(upToScoping entryPoint)
forM_ l $ \s -> do
renderStdOut (Scoper.ppOut (mkScopePrettyOptions globalOpts localOpts) s)
+ Doc localOpts -> do
+ l <-
+ (^. Scoper.mainModule)
+ <$> runPipeline
+ (upToScoping entryPoint)
+ let docDir = localOpts ^. docOutputDir
+ Doc.compileModuleHtmlText docDir "proj" l
+ embed (when (localOpts ^. docOpen) (Process.callProcess "xdg-open" [docDir Doc.indexFileName]))
MicroJuvix Pretty -> do
micro <-
head . (^. Micro.resultModules)
diff --git a/assets/linuwial.css b/assets/linuwial.css
new file mode 100644
index 0000000000..127d3dd6f2
--- /dev/null
+++ b/assets/linuwial.css
@@ -0,0 +1,883 @@
+@import "extra.css";
+
+/* @group Fundamentals */
+
+* { margin: 0; padding: 0 }
+
+/* Is this portable? */
+html {
+ background-color: white;
+ width: 100%;
+ height: 100%;
+}
+
+body {
+ background: #fefefe;
+ color: #111;
+ text-align: left;
+ min-height: 100vh;
+ position: relative;
+ -webkit-text-size-adjust: 100%;
+ -webkit-font-feature-settings: "kern" 1, "liga" 0;
+ -moz-font-feature-settings: "kern" 1, "liga" 0;
+ -o-font-feature-settings: "kern" 1, "liga" 0;
+ font-feature-settings: "kern" 1, "liga" 0;
+ letter-spacing: 0.0015rem;
+}
+
+#content a {
+ overflow-wrap: break-word;
+}
+
+p {
+ margin: 0.8em 0;
+}
+
+ul, ol {
+ margin: 0.8em 0 0.8em 2em;
+}
+
+dl {
+ margin: 0.8em 0;
+}
+
+dt {
+ font-weight: bold;
+}
+dd {
+ margin-left: 2em;
+}
+
+a { text-decoration: none; }
+a[href]:link { color: #D54E54; }
+a[href]:visited {color: #802e31; }
+a[href]:hover { text-decoration:underline; }
+
+a[href].def:link, a[href].def:visited { color: rgba(69, 59, 97, 0.8); }
+a[href].def:hover { color: rgb(78, 98, 114); }
+
+/* @end */
+
+/* @group Show and hide with JS */
+
+body.js-enabled .hide-when-js-enabled {
+ display: none;
+}
+
+/* @end */
+
+
+/* @group responsive */
+
+#package-header .caption {
+ margin: 0px 1em 0 2em;
+}
+
+@media only screen and (min-width: 1280px) {
+ #content {
+ width: 63vw;
+ max-width: 1450px;
+ }
+
+ #table-of-contents {
+ position: fixed;
+ max-width: 10vw;
+ top: 10.2em;
+ left: 2em;
+ bottom: 1em;
+ overflow-y: auto;
+ }
+
+ #synopsis {
+ display: block;
+ position: fixed;
+ float: left;
+ top: 5em;
+ bottom: 1em;
+ right: 0;
+ max-width: 65vw;
+ overflow-y: auto;
+ /* Ensure that synopsis covers everything (including MathJAX markup) */
+ z-index: 1;
+ }
+
+ #synopsis .show {
+ border: 1px solid #5E5184;
+ padding: 0.7em;
+ max-height: 65vh;
+ }
+
+}
+
+@media only screen and (max-width: 1279px) {
+ #content {
+ width: 80vw;
+ }
+
+ #synopsis {
+ display: block;
+ padding: 0;
+ position: relative;
+ margin: 0;
+ width: 100%;
+ }
+}
+
+@media only screen and (max-width: 999px) {
+ #content {
+ width: 93vw;
+ }
+}
+
+
+/* menu for wider screens
+
+ Display the package name at the left and the menu links at the right,
+ inline with each other:
+ The package name Source . Contents . Index
+*/
+@media only screen and (min-width: 1000px) {
+ #package-header {
+ text-align: left;
+ white-space: nowrap;
+ height: 40px;
+ padding: 4px 1.5em 0px 1.5em;
+ overflow: visible;
+
+ display: flex;
+ justify-content: space-between;
+ align-items: center;
+ }
+
+ #package-header .caption {
+ display: inline-block;
+ margin: 0;
+ }
+
+ #package-header ul.links {
+ margin: 0;
+ display: inline-table;
+ }
+
+ #package-header .caption + ul.links {
+ margin-left: 1em;
+ }
+}
+
+/* menu for smaller screens
+
+Display the package name on top of the menu links and center both elements:
+ The package name
+ Source . Contents . Index
+*/
+@media only screen and (max-width: 999px) {
+ #package-header {
+ text-align: center;
+ padding: 6px 0 4px 0;
+ overflow: hidden;
+ }
+
+ #package-header ul.links {
+ display: block;
+ text-align: center;
+ margin: 0;
+
+ /* Hide scrollbar but allow scrolling menu links horizontally */
+ white-space: nowrap;
+ overflow-x: auto;
+ overflow-y: hidden;
+ margin-bottom: -17px;
+ height: 50px;
+ }
+
+ #package-header .caption {
+ display: block;
+ margin: 4px 0;
+ text-align: center;
+ }
+
+ #package-header ul.links::-webkit-scrollbar {
+ display: none;
+ }
+
+ #package-header ul.links li:first-of-type {
+ padding-left: 1em;
+ }
+
+ #package-header ul.links li:last-of-type {
+ /*
+ The last link of the menu should offer the same distance to the right
+ as the #package-header enforces at the left.
+ */
+ padding-right: 1em;
+ }
+
+ #package-header .caption + ul.links {
+ padding-top: 9px;
+ }
+
+ #module-header table.info {
+ float: none;
+ top: 0;
+ margin: 0 auto;
+ overflow: hidden;
+ max-width: 80vw;
+ }
+}
+
+/* @end */
+
+
+/* @group Fonts & Sizes */
+
+/* Basic technique & IE workarounds from YUI 3
+ For reasons, see:
+ http://yui.yahooapis.com/3.1.1/build/cssfonts/fonts.css
+ */
+
+ body, button {
+ font: 400 14px/1.4 'PT Sans',
+ /* Fallback Font Stack */
+ -apple-system,
+ BlinkMacSystemFont,
+ 'Segoe UI',
+ Roboto,
+ Oxygen-Sans,
+ Cantarell,
+ 'Helvetica Neue',
+ sans-serif;
+ *font-size: medium; /* for IE */
+ *font:x-small; /* for IE in quirks mode */
+ }
+
+h1 { font-size: 146.5%; /* 19pt */ }
+h2 { font-size: 131%; /* 17pt */ }
+h3 { font-size: 116%; /* 15pt */ }
+h4 { font-size: 100%; /* 13pt */ }
+h5 { font-size: 100%; /* 13pt */ }
+
+table {
+ font-size:inherit;
+ font:100%;
+}
+
+pre, code, kbd, samp, tt, .src {
+ font-family:monospace;
+}
+
+.links, .link {
+ font-size: 85%; /* 11pt */
+}
+
+#module-header .caption {
+ font-size: 182%; /* 24pt */
+}
+
+#module-header .caption sup {
+ font-size: 80%;
+ font-weight: normal;
+}
+
+#package-header #page-menu a:link, #package-header #page-menu a:visited { color: white; }
+
+
+.info {
+ font-size: 90%;
+}
+
+
+/* @end */
+
+/* @group Common */
+
+.caption, h1, h2, h3, h4, h5, h6, summary {
+ font-weight: bold;
+ color: #D84E53;
+ margin: 1.5em 0 1em 0;
+}
+
+
+* + h1, * + h2, * + h3, * + h4, * + h5, * + h6 {
+ margin-top: 2em;
+}
+
+h1 + h2, h2 + h3, h3 + h4, h4 + h5, h5 + h6 {
+ margin-top: inherit;
+}
+
+ul li + li {
+ margin-top: 0.2rem;
+}
+
+ul + p {
+ margin-top: 0.93em;
+}
+
+p + ul {
+ margin-top: 0.5em;
+}
+
+p {
+ margin-top: 0.7rem;
+}
+
+ul, ol {
+ margin: 0.8em 0 0.8em 2em;
+}
+
+ul.links {
+ list-style: none;
+ text-align: left;
+ font-size: 0.95em;
+}
+
+#package-header ul.links, #package-header ul.links button {
+ font-size: 1rem;
+}
+
+ul.links li {
+ display: inline;
+ white-space: nowrap;
+ padding: 0;
+}
+
+ul.links > li + li:before {
+ content: '\00B7';
+}
+
+ul.links li a {
+ padding: 0.2em 0.5em;
+}
+
+.hide { display: none; }
+.show { display: inherit; }
+.clear { clear: both; }
+
+.collapser:before, .expander:before, .noexpander:before {
+ font-size: 1.2em;
+ color: #9C5791;
+ display: inline-block;
+ padding-right: 7px;
+}
+
+.collapser:before {
+ content: '▿';
+}
+.expander:before {
+ content: '▹';
+}
+.noexpander:before {
+ content: '▿';
+ visibility: hidden;
+}
+
+.collapser, .expander {
+ cursor: pointer;
+}
+
+.instance.collapser, .instance.expander {
+ margin-left: 0px;
+ background-position: left center;
+ min-width: 9px;
+ min-height: 9px;
+}
+
+summary {
+ cursor: pointer;
+ outline: none;
+}
+
+pre {
+ padding: 0.5rem 1rem;
+ margin: 1em 0 0 0;
+ background-color: #f7f7f7;
+ overflow: auto;
+ border: 1px solid #ddd;
+ border-radius: 0.3em;
+}
+
+pre + p {
+ margin-top: 1em;
+}
+
+pre + pre {
+ margin-top: 0.5em;
+}
+
+blockquote {
+ border-left: 3px solid #c7a5d3;
+ background-color: #eee4f1;
+ margin: 0.5em;
+ padding: 0.0005em 0.3em 0.5em 0.5em;
+}
+
+.src {
+ background: #f2f2f2;
+ padding: 0.2em 0.5em;
+}
+
+.keyword { font-weight: normal; }
+.def { font-weight: bold; }
+
+@media print {
+ #footer { display: none; }
+}
+
+/* @end */
+
+/* @group Page Structure */
+
+#content {
+ margin: 3em auto 6em auto;
+ padding: 0;
+}
+
+#package-header {
+ background: #803353;
+ border-bottom: 5px solid rgba(69, 59, 97, 0.5);
+ color: #ddd;
+ position: relative;
+ font-size: 1.2em;
+ text-align: left;
+ margin: 0 auto;
+}
+
+#package-header .caption {
+ color: white;
+ font-style: normal;
+ font-size: 1rem;
+ font-weight: bold;
+}
+
+#module-header .caption {
+ font-weight: bold;
+ border-bottom: 1px solid #ddd;
+}
+
+table.info {
+ float: right;
+ padding: 0.5em 1em;
+ border: 1px solid #ddd;
+ color: rgb(78,98,114);
+ background-color: #fff;
+ max-width: 60%;
+ border-spacing: 0;
+ position: relative;
+ top: -0.78em;
+ margin: 0 0 0 2em;
+}
+
+.info th {
+ padding: 0 1em 0 0;
+ text-align: right;
+}
+
+#style-menu li {
+ display: block;
+ border-style: none;
+ list-style-type: none;
+}
+
+#footer {
+ background: #ededed;
+ border-top: 1px solid #aaa;
+ padding: 0.5em 0;
+ color: #222;
+ text-align: center;
+ width: 100%;
+ height: 7em;
+ margin-top: 3em;
+ position: relative;
+ clear: both;
+}
+
+#footer #tara {
+ width: 4em;
+}
+
+/* @end */
+
+/* @group Front Matter */
+
+#synopsis .caption,
+#contents-list .caption {
+ font-size: 1rem;
+}
+
+#synopsis, #table-of-contents {
+ font-size: 16px;
+}
+
+#contents-list {
+ background: #f4f4f4;
+ padding: 1em;
+ margin: 0;
+}
+
+#contents-list .caption {
+ text-align: left;
+ margin: 0;
+}
+
+#contents-list ul {
+ list-style: none;
+ margin: 0;
+ margin-top: 10px;
+ font-size: 14px;
+}
+
+#contents-list ul ul {
+ margin-left: 1.5em;
+}
+
+#description .caption {
+ display: none;
+}
+
+#synopsis summary {
+ display: block;
+ float: right;
+ width: 29px;
+ color: rgba(255,255,255,0);
+ height: 110px;
+ margin: 0;
+ font-size: 1px;
+ padding: 0;
+ background: url(synopsis.png) no-repeat 0px -8px;
+}
+
+#synopsis details[open] > summary {
+ background: url(synopsis.png) no-repeat -75px -8px;
+}
+
+#synopsis ul {
+ height: 100%;
+ overflow: auto;
+ padding: 0.5em;
+ margin: 0;
+}
+
+#synopsis ul ul {
+ overflow: hidden;
+}
+
+#synopsis ul,
+#synopsis ul li.src {
+ background-color: rgb(250,247,224);
+ white-space: nowrap;
+ list-style: none;
+ margin-left: 0;
+}
+
+#interface td.src {
+ white-space: nowrap;
+}
+
+/* @end */
+
+/* @group Main Content */
+
+#interface div.top + div.top {
+ margin-top: 1.5em;
+}
+
+#interface p + div.top,
+#interface h1 + div.top,
+#interface h2 + div.top,
+#interface h3 + div.top,
+#interface h4 + div.top,
+#interface h5 + div.top {
+ margin-top: 1em;
+}
+#interface .src .selflink,
+#interface .src .link {
+ float: right;
+ color: #888;
+ padding: 0 7px;
+ -moz-user-select: none;
+ font-weight: bold;
+ line-height: 30px;
+}
+#interface .src .selflink {
+ margin: 0 -0.5em 0 0.5em;
+}
+
+#interface span.fixity {
+ color: #919191;
+ border-left: 1px solid #919191;
+ padding: 0.2em 0.5em 0.2em 0.5em;
+ margin: 0 -1em 0 1em;
+}
+
+#interface span.rightedge {
+ border-left: 1px solid #919191;
+ padding: 0.2em 0 0.2em 0;
+ margin: 0 0 0 1em;
+}
+
+#interface table { border-spacing: 2px; }
+#interface td {
+ vertical-align: top;
+ padding-left: 0.5em;
+}
+
+#interface td.doc p {
+ margin: 0;
+}
+#interface td.doc p + p {
+ margin-top: 0.8em;
+}
+
+.doc table {
+ border-collapse: collapse;
+ border-spacing: 0px;
+}
+
+.doc th,
+.doc td {
+ padding: 5px;
+ border: 1px solid #ddd;
+}
+
+.doc th {
+ background-color: #f0f0f0;
+}
+
+.clearfix:after {
+ clear: both;
+ content: " ";
+ display: block;
+ height: 0;
+ visibility: hidden;
+}
+
+.subs, .top > .doc, .subs > .doc {
+ padding-left: 1em;
+ border-left: 1px solid gainsboro;
+ margin-bottom: 1em;
+}
+
+.top .subs {
+ margin-bottom: 0.6em;
+}
+
+.subs.fields ul {
+ list-style: none;
+ display: table;
+ margin: 0;
+}
+
+.subs.fields ul li {
+ display: table-row;
+}
+
+.subs ul li dfn {
+ display: table-cell;
+ font-style: normal;
+ font-weight: bold;
+ margin: 1px 0;
+ white-space: nowrap;
+}
+
+.subs ul li > .doc {
+ display: table-cell;
+ padding-left: 0.5em;
+ margin-bottom: 0.5em;
+}
+
+.subs ul li > .doc p {
+ margin: 0;
+}
+
+.subs .subs p.src {
+ border: none;
+ background-color: #f8f8f8;
+}
+
+.subs .subs .caption {
+ margin-top: 1em ;
+ margin-bottom: 0px;
+}
+
+.subs p.caption {
+ margin-top: 0;
+}
+
+.subs .subs .caption + .src {
+ margin: 0px;
+ margin-top: 8px;
+}
+
+.subs .subs .src + .src {
+ margin: 7px 0 0 0;
+}
+
+/* Render short-style data instances */
+.inst ul {
+ height: 100%;
+ padding: 0.5em;
+ margin: 0;
+}
+
+.inst, .inst li {
+ list-style: none;
+ margin-left: 1em;
+}
+
+/* Workaround for bug in Firefox (issue #384) */
+.inst-left {
+ float: left;
+}
+
+.top p.src {
+ border-bottom: 3px solid #e5e5e5;
+ line-height: 2rem;
+ margin-bottom: 1em;
+}
+
+.warning {
+ color: red;
+}
+
+.arguments {
+ margin-top: -0.4em;
+}
+.arguments .caption {
+ display: none;
+}
+
+.fields { padding-left: 1em; }
+
+.fields .caption { display: none; }
+
+.fields p { margin: 0 0; }
+
+/* this seems bulky to me
+.methods, .constructors {
+ background: #f8f8f8;
+ border: 1px solid #eee;
+}
+*/
+
+/* @end */
+
+/* @group Auxillary Pages */
+
+
+.extension-list {
+ list-style-type: none;
+ margin-left: 0;
+}
+
+#mini {
+ margin: 0 auto;
+ padding: 0 1em 1em;
+}
+
+#mini > * {
+ font-size: 93%; /* 12pt */
+}
+
+#mini #module-list .caption,
+#mini #module-header .caption {
+ font-size: 125%; /* 15pt */
+}
+
+#mini #interface h1,
+#mini #interface h2,
+#mini #interface h3,
+#mini #interface h4 {
+ font-size: 109%; /* 13pt */
+ margin: 1em 0 0;
+}
+
+#mini #interface .top,
+#mini #interface .src {
+ margin: 0;
+}
+
+#mini #module-list ul {
+ list-style: none;
+ margin: 0;
+}
+
+#alphabet ul {
+ list-style: none;
+ padding: 0;
+ margin: 0.5em 0 0;
+ text-align: center;
+}
+
+#alphabet li {
+ display: inline;
+ margin: 0 0.25em;
+}
+
+#alphabet a {
+ font-weight: bold;
+}
+
+#index .caption,
+#module-list .caption { font-size: 131%; /* 17pt */ }
+
+#index table {
+ margin-left: 2em;
+}
+
+#index .src {
+ font-weight: bold;
+}
+#index .alt {
+ font-size: 77%; /* 10pt */
+ font-style: italic;
+ padding-left: 2em;
+}
+
+#index td + td {
+ padding-left: 1em;
+}
+
+#module-list ul {
+ list-style: none;
+ margin: 0 0 0 2em;
+}
+
+#module-list li {
+ clear: right;
+}
+
+#module-list span.collapser,
+#module-list span.expander {
+ background-position: 0 0.3em;
+}
+
+#module-list .package {
+ float: right;
+}
+
+:target {
+ background: -webkit-linear-gradient(top, transparent 0%, transparent 65%, #fbf36d 60%, #fbf36d 100%);
+ background: -moz-linear-gradient(top, transparent 0%, transparent 65%, #fbf36d 60%, #fbf36d 100%);
+ background: -o-linear-gradient(top, transparent 0%, transparent 65%, #fbf36d 60%, #fbf36d 100%);
+ background: -ms-linear-gradient(top, transparent 0%, transparent 65%, #fbf36d 60%, #fbf36d 100%);
+ background: linear-gradient(to bottom, transparent 0%, transparent 65%, #fbf36d 60%, #fbf36d 100%);
+}
+
+:target:hover {
+ background: -webkit-linear-gradient(top, transparent 0%, transparent 0%, #fbf36d 0%, #fbf36d 100%);
+ background: -moz-linear-gradient(top, transparent 0%, transparent 0%, #fbf36d 0%, #fbf36d 100%);
+ background: -o-linear-gradient(top, transparent 0%, transparent 0%, #fbf36d 0%, #fbf36d 100%);
+ background: -ms-linear-gradient(top, transparent 0%, transparent 0%, #fbf36d 0%, #fbf36d 100%);
+ background: linear-gradient(to bottom, transparent 0%, transparent 0%, #fbf36d 0%, #fbf36d 100%);
+}
+
+/* @end */
+
+/* @group Dropdown menus */
+
+#preferences-menu, #style-menu {
+ width: 25em;
+ overflow-y: auto;
+}
+
+/* @end */
diff --git a/assets/source-ayu-light.css b/assets/source-ayu-light.css
index fca4920f0e..dddaa497d2 100644
--- a/assets/source-ayu-light.css
+++ b/assets/source-ayu-light.css
@@ -39,6 +39,10 @@ body {
color: #000000;
}
+.ju-define {
+ font-weight: bold;
+}
+
a:hover, a.hover-highlight {
background-color: #dadbdc ;
}
diff --git a/assets/source-nord.css b/assets/source-nord.css
index d21ad7ba35..0d7cb6949b 100644
--- a/assets/source-nord.css
+++ b/assets/source-nord.css
@@ -39,6 +39,10 @@ body {
color: #d8dee9
}
+.ju-defined {
+ font-weight: bold;
+}
+
a:link, a:visited {
text-decoration: none;
}
diff --git a/examples/milestone/MiniTicTacToe/MiniTicTacToe.juvix b/examples/milestone/MiniTicTacToe/MiniTicTacToe.juvix
index f8a3b69ec2..61bb1cae94 100644
--- a/examples/milestone/MiniTicTacToe/MiniTicTacToe.juvix
+++ b/examples/milestone/MiniTicTacToe/MiniTicTacToe.juvix
@@ -1,18 +1,27 @@
+--- Tic-tac-toe is a paper-and-pencil game for two players who take turns marking the spaces
+--- in a three-by-three grid with X or O.
+---
+--- The player who succeeds in placing three of their marks in a horizontal, vertical, or
+--- diagonal row is the winner. It is a solved game, with a forced draw assuming best play from both players.
+---
+--- The function ;run; contains the game logic.
module MiniTicTacToe;
open import Stdlib.Data.Nat.Ord;
open import Stdlib.Prelude;
---------------------------------------------------------------------------------
-- Render Utils
---------------------------------------------------------------------------------
infixr 5 ++str;
+--- Concatenation of ;String;s
axiom ++str : String → String → String;
compile ++str {
c ↦ "concat";
};
+--- Concatenates a list of strings
+---
+--- ;concat (("a" ∷ nil) ∷ ("b" ∷ nil)); evaluates to ;"a" ∷ "b" ∷ nil;
concat : List String → String;
concat ≔ foldl (++str) "";
@@ -22,62 +31,77 @@ surround x xs ≔ (x ∷ intersperse x xs) ++ (x ∷ nil);
intercalate : String → List String → String;
intercalate sep xs ≔ concat (intersperse sep xs);
+--- Joins a list of strings with the newline character
unlines : List String → String;
unlines ≔ intercalate "\n";
---------------------------------------------------------------------------------
-- Symbol
---------------------------------------------------------------------------------
+--- A symbol represents a token that can be placed in a square
inductive Symbol {
+--- The circle token
O : Symbol;
+--- The cross token
X : Symbol;
};
+--- Equality for ;Symbol;s
==Symbol : Symbol → Symbol → Bool;
==Symbol O O ≔ true;
==Symbol X X ≔ true;
==Symbol _ _ ≔ false;
+--- Turns ;O; into ;X; and ;X; into ;O;
switch : Symbol → Symbol;
switch O ≔ X;
switch X ≔ O;
+--- Textual representation of a ;Symbol;
showSymbol : Symbol → String;
showSymbol O ≔ "O";
showSymbol X ≔ "X";
---------------------------------------------------------------------------------
-- Square
---------------------------------------------------------------------------------
-
+--- A square is each of the holes in a board
inductive Square {
+ --- An empty square has a ;ℕ; that uniquely identifies it
empty : ℕ → Square;
+ --- An occupied square has a ;Symbol; in it
occupied : Symbol → Square;
};
+--- Equality for ;Square;s
==Square : Square → Square → Bool;
==Square (empty m) (empty n) ≔ m == n;
==Square (occupied s) (occupied t) ≔ ==Symbol s t;
==Square _ _ ≔ false;
+--- Textual representation of a ;Square;
showSquare : Square → String;
showSquare (empty n) ≔ " " ++str natToStr n ++str " ";
showSquare (occupied s) ≔ " " ++str showSymbol s ++str " ";
---------------------------------------------------------------------------------
--- Board
---------------------------------------------------------------------------------
+-- A row in a board implemented as ;List Square;
+-- Row : Type;
+-- Row ≔ List Square;
+
+-- A column in a board implemented as ;List Square;
+-- Column : Type;
+-- Column ≔ Row;
+-- TODO use a type alias?
+--- A grid of squares
inductive Board {
board : List (List Square) → Board;
};
+--- Returns the list of numbers corresponding to the empty ;Square;s
possibleMoves : List Square → List ℕ;
possibleMoves nil ≔ nil;
possibleMoves ((empty n) ∷ xs) ≔ n ∷ possibleMoves xs;
possibleMoves (_ ∷ xs) ≔ possibleMoves xs;
+--- ;true; if all the ;Square;s in the list are equal
full : List Square → Bool;
full (a ∷ b ∷ c ∷ nil) ≔ (==Square a b) && (==Square b c);
@@ -90,51 +114,54 @@ columns ≔ transpose;
rows : List (List Square) → List (List Square);
rows ≔ id;
-showRow : List Square → String;
+--- Textual representation of a ;(List Square);
+showRow : (List Square) → String;
showRow xs ≔ concat (surround "|" (map showSquare xs));
showBoard : Board → String;
showBoard (board squares) ≔ unlines (surround "+---+---+---+" (map showRow squares));
---------------------------------------------------------------------------------
-- Error
---------------------------------------------------------------------------------
inductive Error {
+--- no error occurred
noError : Error;
+--- a non-fatal error occurred
continue : String → Error;
+--- a fatal occurred
terminate : String → Error;
};
---------------------------------------------------------------------------------
-- GameState
---------------------------------------------------------------------------------
inductive GameState {
state : Board → Symbol → Error → GameState;
};
+--- Textual representation of a ;GameState;
showGameState : GameState → String;
showGameState (state b _ _) ≔ showBoard b;
+--- Projects the player
player : GameState → Symbol;
player (state _ p _) ≔ p;
+--- initial ;GameState;
beginState : GameState;
beginState ≔ state
(board (map (map empty) ((one ∷ two ∷ three ∷ nil) ∷ (four ∷ five ∷ six ∷ nil) ∷ (seven ∷ eight ∷ nine ∷ nil) ∷ nil)))
X
noError;
+--- ;true; if some player has won the game
won : GameState → Bool;
won (state (board squares) _ _) ≔ any full (diagonals squares ++ rows squares ++ columns squares);
+--- ;true; if there is a draw
draw : GameState → Bool;
draw (state (board squares) _ _) ≔ null (possibleMoves (flatten squares));
---------------------------------------------------------------------------------
-- Move
---------------------------------------------------------------------------------
replace : Symbol → ℕ → Square → Square;
replace player k (empty n) ≔ if (n Stdlib.Data.Nat.Ord.== k) (occupied player) (empty n);
@@ -158,9 +185,7 @@ playMove (just k) (state (board s) player e) ≔
(switch player)
noError));
---------------------------------------------------------------------------------
-- IO Utils
---------------------------------------------------------------------------------
axiom readline : String;
compile readline {
@@ -173,9 +198,7 @@ compile parsePositiveInt {
c ↦ "parsePositiveInt";
};
---------------------------------------------------------------------------------
-- IO
---------------------------------------------------------------------------------
validMove : ℕ → Maybe ℕ;
validMove n ≔ if ((n <= nine) && (n >= one)) (just n) nothing;
@@ -195,9 +218,11 @@ run _ (state b p (terminate msg)) ≔ putStrLn ("\n" ++str (showGameState (state
run f (state b p (continue msg)) ≔ run f (f (putStr (msg ++str prompt (state b p noError)) , state b p noError));
run f x ≔ run f (f (putStr (prompt x) , x));
+--- The welcome message
welcome : String;
welcome ≔ "MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move";
+--- The entry point of the program
main : IO;
main ≔ putStrLn welcome >> run do beginState;
end;
diff --git a/src/Juvix/Analysis/Scoping/Scoper.hs b/src/Juvix/Analysis/Scoping/Scoper.hs
index 620ae51ed8..c82d3ffea0 100644
--- a/src/Juvix/Analysis/Scoping/Scoper.hs
+++ b/src/Juvix/Analysis/Scoping/Scoper.hs
@@ -409,7 +409,8 @@ checkTypeSignature ::
checkTypeSignature TypeSignature {..} = do
sigType' <- checkParseExpressionAtoms _sigType
sigName' <- bindFunctionSymbol _sigName
- registerFunction' TypeSignature {_sigName = sigName', _sigType = sigType', ..}
+ sigDoc' <- mapM checkJudoc _sigDoc
+ registerFunction' TypeSignature {_sigName = sigName', _sigType = sigType', _sigDoc = sigDoc', ..}
checkConstructorDef ::
Members '[Error ScoperError, Reader LocalVars, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
@@ -418,10 +419,12 @@ checkConstructorDef ::
checkConstructorDef InductiveConstructorDef {..} = do
constructorType' <- checkParseExpressionAtoms _constructorType
constructorName' <- bindConstructorSymbol _constructorName
+ doc' <- mapM checkJudoc _constructorDoc
registerConstructor'
InductiveConstructorDef
{ _constructorName = constructorName',
- _constructorType = constructorType'
+ _constructorType = constructorType',
+ _constructorDoc = doc'
}
withParams ::
@@ -464,11 +467,13 @@ checkInductiveDef ::
checkInductiveDef ty@InductiveDef {..} = do
withParams _inductiveParameters $ \inductiveParameters' -> do
inductiveType' <- mapM checkParseExpressionAtoms _inductiveType
+ inductiveDoc' <- mapM checkJudoc _inductiveDoc
inductiveName' <- bindInductiveSymbol _inductiveName
inductiveConstructors' <- mapM checkConstructorDef _inductiveConstructors
registerInductive'
InductiveDef
{ _inductiveName = inductiveName',
+ _inductiveDoc = inductiveDoc',
_inductiveBuiltin = _inductiveBuiltin,
_inductiveParameters = inductiveParameters',
_inductiveType = inductiveType',
@@ -508,7 +513,7 @@ checkTopModule ::
Members '[Error ScoperError, Reader ScopeParameters, Files, State ScoperState, InfoTableBuilder, Parser.InfoTableBuilder, NameIdGen] r =>
Module 'Parsed 'ModuleTop ->
Sem r (ModuleRef'' 'S.NotConcrete 'ModuleTop)
-checkTopModule m@(Module path params body) = do
+checkTopModule m@(Module path params doc body) = do
checkPath
r <- checkedModule
modify (over (scoperModulesCache . cachedModules) (HashMap.insert path r))
@@ -554,11 +559,13 @@ checkTopModule m@(Module path params body) = do
localScope $
withParams params $ \params' -> do
(_moduleExportInfo, body') <- checkModuleBody body
+ doc' <- mapM checkJudoc doc
let _moduleRefModule =
Module
{ _modulePath = path',
_moduleParameters = params',
- _moduleBody = body'
+ _moduleBody = body',
+ _moduleDoc = doc'
}
_moduleRefName = set S.nameConcrete () path'
return ModuleRef'' {..}
@@ -588,12 +595,13 @@ checkLocalModule ::
Module 'Parsed 'ModuleLocal ->
Sem r (Module 'Scoped 'ModuleLocal)
checkLocalModule Module {..} = do
- (_moduleExportInfo, moduleBody', moduleParameters') <-
+ (_moduleExportInfo, moduleBody', moduleParameters', moduleDoc') <-
withScope $
withParams _moduleParameters $ \p' -> do
inheritScope
(e, b) <- checkModuleBody _moduleBody
- return (e, b, p')
+ doc' <- mapM checkJudoc _moduleDoc
+ return (e, b, p', doc')
_modulePath' <- reserveSymbolOf S.KNameLocalModule _modulePath
let moduleId = _modulePath' ^. S.nameId
_moduleRefName = set S.nameConcrete () _modulePath'
@@ -601,7 +609,8 @@ checkLocalModule Module {..} = do
Module
{ _modulePath = _modulePath',
_moduleParameters = moduleParameters',
- _moduleBody = moduleBody'
+ _moduleBody = moduleBody',
+ _moduleDoc = moduleDoc'
}
entry :: ModuleRef' 'S.NotConcrete
entry = mkModuleRef' @'ModuleLocal ModuleRef'' {..}
@@ -844,7 +853,8 @@ checkAxiomDef ::
checkAxiomDef AxiomDef {..} = do
axiomType' <- localScope (checkParseExpressionAtoms _axiomType)
axiomName' <- bindAxiomSymbol _axiomName
- registerAxiom' AxiomDef {_axiomName = axiomName', _axiomType = axiomType', ..}
+ axiomDoc' <- localScope (mapM checkJudoc _axiomDoc)
+ registerAxiom' AxiomDef {_axiomName = axiomName', _axiomType = axiomType', _axiomDoc = axiomDoc', ..}
checkCompile ::
Members '[InfoTableBuilder, Error ScoperError, State Scope, Reader LocalVars, State ScoperState] r =>
@@ -1211,6 +1221,21 @@ checkExpressionAtoms ::
checkExpressionAtoms (ExpressionAtoms l i) = do
(`ExpressionAtoms` i) <$> mapM checkExpressionAtom l
+checkJudoc ::
+ Members '[Error ScoperError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder, NameIdGen] r =>
+ Judoc 'Parsed ->
+ Sem r (Judoc 'Scoped)
+checkJudoc (Judoc atoms) = Judoc <$> mapM checkJudocAtom atoms
+
+checkJudocAtom ::
+ Members '[Error ScoperError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder, NameIdGen] r =>
+ JudocAtom 'Parsed ->
+ Sem r (JudocAtom 'Scoped)
+checkJudocAtom = \case
+ JudocText t -> return (JudocText t)
+ JudocNewline -> return JudocNewline
+ JudocExpression e -> JudocExpression <$> checkParseExpressionAtoms e
+
checkParseExpressionAtoms ::
Members '[Error ScoperError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder, NameIdGen] r =>
ExpressionAtoms 'Parsed ->
diff --git a/src/Juvix/Analysis/Scoping/ScoperResult.hs b/src/Juvix/Analysis/Scoping/ScoperResult.hs
index 5eb5f19c39..8ff1ea2963 100644
--- a/src/Juvix/Analysis/Scoping/ScoperResult.hs
+++ b/src/Juvix/Analysis/Scoping/ScoperResult.hs
@@ -15,3 +15,6 @@ data ScoperResult = ScoperResult
}
makeLenses ''ScoperResult
+
+mainModule :: Lens' ScoperResult (Module 'Scoped 'ModuleTop)
+mainModule = resultModules . _head
diff --git a/src/Juvix/Documentation/Compiler.hs b/src/Juvix/Documentation/Compiler.hs
new file mode 100644
index 0000000000..da548ad576
--- /dev/null
+++ b/src/Juvix/Documentation/Compiler.hs
@@ -0,0 +1,461 @@
+module Juvix.Documentation.Compiler where
+
+import Data.ByteString qualified as BS
+import Data.ByteString.Builder qualified as Builder
+import Data.HashMap.Strict qualified as HashMap
+import Data.Time.Clock
+import Juvix.Documentation.Extra
+import Juvix.Internal.Strings qualified as Str
+import Juvix.Prelude
+import Juvix.Prelude qualified as Prelude
+import Juvix.Prelude.Html
+import Juvix.Prelude.Pretty
+import Juvix.Syntax.Concrete.Language
+import Juvix.Syntax.Concrete.Scoped.Name qualified as S
+import Juvix.Syntax.Concrete.Scoped.Pretty
+import Juvix.Syntax.Concrete.Scoped.Pretty.Html hiding (go)
+import Juvix.Syntax.Concrete.Scoped.Utils
+import Juvix.Syntax.NameId
+import Juvix.Utils.Paths
+import Juvix.Utils.Version
+import Text.Blaze.Html.Renderer.Utf8 qualified as Html
+-- import Data.HashMap.Strict qualified as HashMap
+import Text.Blaze.Html5 as Html hiding (map)
+import Text.Blaze.Html5.Attributes qualified as Attr
+
+data DocParams = DocParams
+ { _docParamBase :: Text,
+ _docOutputDir :: FilePath
+ }
+
+makeLenses ''DocParams
+
+data Tree k a = Tree
+ { _treeLabel :: a,
+ _treeChildren :: HashMap k (Tree k a)
+ }
+
+makeLenses ''Tree
+
+type ModuleTree = Tree Symbol (Maybe TopModulePath)
+
+indexTree :: [TopModulePath] -> Tree Symbol (Maybe TopModulePath)
+indexTree = foldr insertModule emptyTree
+ where
+ insertModule :: TopModulePath -> ModuleTree -> ModuleTree
+ insertModule m@(TopModulePath ps s) t = go (Just t) (snoc ps s)
+ where
+ go :: Maybe ModuleTree -> [Symbol] -> ModuleTree
+ go tree = \case
+ [] -> set treeLabel (Just m) t'
+ (k : ks) -> over (treeChildren . at k) (Just . flip go ks) t'
+ where
+ t' :: ModuleTree
+ t' = fromMaybe emptyTree tree
+ emptyTree :: Tree Symbol (Maybe TopModulePath)
+ emptyTree = Tree Nothing mempty
+
+indexFileName :: FilePath
+indexFileName = "index.html"
+
+createIndexFile ::
+ forall r.
+ Members '[Reader DocParams, Embed IO, Reader HtmlOptions] r =>
+ [TopModulePath] ->
+ Sem r ()
+createIndexFile ps = do
+ outDir <- asks (^. docOutputDir)
+ indexHtml >>= writeHtml (outDir indexFileName) . template mempty
+ where
+ indexHtml :: Sem r Html
+ indexHtml = do
+ tree' <- root tree
+ return $
+ Html.div ! Attr.id "content" $
+ Html.div ! Attr.id "module-list" $
+ (p ! Attr.class_ "caption" $ "Modules")
+ <> tree'
+ tree :: ModuleTree
+ tree = indexTree ps
+ root :: ModuleTree -> Sem r Html
+ root (Tree _ t) = do
+ c' <- mconcatMapM (uncurry goChild) (HashMap.toList t)
+ return $ ul c'
+
+ goChild :: Symbol -> ModuleTree -> Sem r Html
+ goChild s (Tree lbl children) = node
+ where
+ nodeRow :: Sem r Html
+ nodeRow = case lbl of
+ Nothing ->
+ return $
+ Html.span ! Attr.class_ attrBare $
+ toHtml (prettyText s)
+ Just lbl' -> do
+ lnk <- nameIdAttrRef lbl' Nothing
+ return $
+ Html.span ! Attr.class_ attrBare $
+ (a ! Attr.href lnk $ toHtml (prettyText lbl'))
+ attrBase :: Html.AttributeValue
+ attrBase = "details-toggle-control details-toggle collapser"
+ -- dataDetailsId :: AttributeValue -> Attribute
+ -- dataDetailsId = Html.dataAttribute "details-id"
+ attrBare :: Html.AttributeValue
+ attrBare = attrBase <> "module"
+ -- attr :: Html.AttributeValue
+ -- attr = case lbl of
+ -- Nothing -> attrBare
+ -- Just {} -> attrBase
+ node :: Sem r Html
+ node = do
+ row' <- nodeRow
+ childs' <- childs
+ return (row' <>? childs')
+ where
+ childs :: Sem r (Maybe Html)
+ childs
+ | null children = return Nothing
+ | otherwise = do
+ c' <- mapM (uncurry goChild) (HashMap.toList children)
+ return $
+ Just $
+ details ! Attr.open "open" $
+ -- (summary ! Attr.class_ "hide-when-js-enabled" $ "Submodules")
+ summary "Subtree"
+ <> ul (mconcatMap li c')
+
+compileModuleHtmlText :: Members '[Embed IO] r => FilePath -> Text -> Module 'Scoped 'ModuleTop -> Sem r ()
+compileModuleHtmlText dir baseName m = runReader params $ do
+ copyAssets
+ mapM_ goTopModule topModules
+ runReader docHtmlOpts (createIndexFile (map topModulePath (toList topModules)))
+ where
+ copyAssets :: forall s. Members '[Embed IO, Reader DocParams] s => Sem s ()
+ copyAssets = do
+ toAssetsDir <- ( "assets") <$> asks (^. docOutputDir)
+ let writeAsset :: (FilePath, BS.ByteString) -> Sem s ()
+ writeAsset (filePath, fileContents) =
+ Prelude.embed $ BS.writeFile (toAssetsDir takeFileName filePath) fileContents
+ Prelude.embed (createDirectoryIfMissing True toAssetsDir)
+ mapM_ writeAsset assetFiles
+ where
+ assetFiles :: [(FilePath, BS.ByteString)]
+ assetFiles = $(assetsDir)
+
+ params :: DocParams
+ params =
+ DocParams
+ { _docParamBase = baseName,
+ _docOutputDir = dir
+ }
+ topModules :: HashMap NameId (Module 'Scoped 'ModuleTop)
+ topModules = getAllModules m
+
+writeHtml :: Members '[Embed IO] r => FilePath -> Html -> Sem r ()
+writeHtml f h = Prelude.embed $ do
+ createDirectoryIfMissing True dir
+ Builder.writeFile f (Html.renderHtmlBuilder h)
+ where
+ dir :: FilePath
+ dir = takeDirectory f
+
+moduleDocPath :: Members '[Reader HtmlOptions, Reader DocParams] r => Module 'Scoped 'ModuleTop -> Sem r FilePath
+moduleDocPath m = do
+ relPath <- moduleDocRelativePath (m ^. modulePath . S.nameConcrete)
+ outDir <- asks (^. docOutputDir)
+ return (outDir relPath)
+
+topModulePath ::
+ Module 'Scoped 'ModuleTop -> TopModulePath
+topModulePath = (^. modulePath . S.nameConcrete)
+
+srcHtmlOpts :: HtmlOptions
+srcHtmlOpts = HtmlOptions HtmlSrc
+
+docHtmlOpts :: HtmlOptions
+docHtmlOpts = HtmlOptions HtmlDoc
+
+template :: Html -> Html -> Html
+template rightMenu' content' = do
+ docTypeHtml (mhead <> body')
+ where
+ mhead :: Html
+ mhead =
+ Html.head $
+ title titleStr
+ <> Html.meta
+ ! Attr.httpEquiv "Content-Type"
+ ! Attr.content "text/html; charset=UTF-8"
+ <> Html.meta
+ ! Attr.name "viewport"
+ ! Attr.content "width=device-width, initial-scale=1"
+ <> mathJaxCdn
+ -- <> highlightJs
+ <> livejs
+ <> ayuCss
+ <> linuwialCss
+
+ titleStr :: Html
+ titleStr = "Juvix Documentation"
+
+ packageHeader :: Html
+ packageHeader =
+ Html.div ! Attr.id "package-header" $
+ ( Html.span ! Attr.class_ "caption" $
+ "package name - version"
+ )
+ <> rightMenu'
+
+ body' :: Html
+ body' =
+ body ! Attr.class_ "js-enabled" $
+ packageHeader
+ <> content'
+ <> mfooter
+
+ mfooter :: Html
+ mfooter =
+ Html.div ! Attr.id "footer" $
+ ( p
+ ( "Build by "
+ <> (Html.a ! Attr.href Str.juvixDotOrg $ "Juvix")
+ <> " version "
+ <> toHtml versionDoc
+ )
+ )
+ <> ( Html.a ! Attr.href Str.juvixDotOrg $
+ Html.img
+ ! Attr.id "tara"
+ ! Attr.src "assets/Seating_Tara_smiling.svg"
+ ! Attr.alt "Tara"
+ )
+
+-- | This function compiles a datalang module into Html documentation.
+goTopModule ::
+ forall r.
+ Members '[Reader DocParams, Embed IO] r =>
+ Module 'Scoped 'ModuleTop ->
+ Sem r ()
+goTopModule m = do
+ runReader docHtmlOpts $ do
+ fpath <- moduleDocPath m
+ Prelude.embed (putStrLn ("processing " <> pack fpath))
+ docHtml >>= writeHtml fpath
+
+ runReader srcHtmlOpts $ do
+ fpath <- moduleDocPath m
+ srcHtml >>= writeHtml fpath
+ where
+ tmp :: TopModulePath
+ tmp = m ^. modulePath . S.nameConcrete
+
+ srcHtml :: forall s. Members '[Reader HtmlOptions, Embed IO] s => Sem s Html
+ srcHtml = do
+ utc <- Prelude.embed getCurrentTime
+ return (genModuleHtml defaultOptions True utc Ayu m)
+
+ docHtml :: forall s. Members '[Reader HtmlOptions] s => Sem s Html
+ docHtml = do
+ content' <- content
+ rightMenu' <- rightMenu
+ return (template rightMenu' content')
+ where
+ rightMenu :: Sem s Html
+ rightMenu = do
+ sourceRef' <- local (set htmlOptionsKind HtmlSrc) (nameIdAttrRef tmp Nothing)
+ return $
+ ul ! Attr.id "page-menu" ! Attr.class_ "links" $
+ li (a ! Attr.href sourceRef' $ "Source")
+ <> li (a ! Attr.href (fromString indexFileName) $ "Index")
+
+ content :: Sem s Html
+ content = do
+ preface' <- docPreface
+ interface' <- interface
+ return $
+ Html.div ! Attr.id "content" $
+ moduleHeader
+ <> toc
+ <> preface'
+ -- <> synopsis
+ <> interface'
+
+ docPreface :: Sem s Html
+ docPreface = do
+ pref <- goJudocMay (m ^. moduleDoc)
+ return $
+ Html.div ! Attr.id "description" $
+ Html.div ! Attr.class_ "doc" $
+ ( a ! Attr.id "sec:description" ! Attr.href "sec:description" $
+ h1 "Description"
+ )
+ <> pref
+
+ toc :: Html
+ toc =
+ Html.div ! Attr.id "table-of-contents" $
+ Html.div ! Attr.id "contents-list" $
+ ( p
+ ! Attr.class_ "caption"
+ ! Attr.onclick "window.scrollTo(0,0)"
+ $ "Contents"
+ )
+ <> tocEntries
+ where
+ tocEntries :: Html
+ tocEntries =
+ ul $
+ li (a ! Attr.href "#sec:description" $ "Description")
+ <> li (a ! Attr.href "#sec:interface" $ "Definitions")
+
+ moduleHeader :: Html
+ moduleHeader =
+ Html.div ! Attr.id "module-header" $
+ (p ! Attr.class_ "caption" $ toHtml (prettyText tmp))
+
+ interface :: Sem s Html
+ interface = do
+ sigs' <- mconcatMapM goStatement (m ^. moduleBody)
+ return $
+ Html.div ! Attr.id "interface" $
+ ( a ! Attr.id "sec:interface" ! Attr.href "sec:interface" $
+ h1 "Definitions"
+ )
+ <> sigs'
+
+goJudocMay :: Members '[Reader HtmlOptions] r => Maybe (Judoc 'Scoped) -> Sem r Html
+goJudocMay = maybe (return mempty) goJudoc
+
+goJudoc :: forall r. Members '[Reader HtmlOptions] r => Judoc 'Scoped -> Sem r Html
+goJudoc (Judoc atoms) = mconcatMapM goParagraph paragraphs
+ where
+ goParagraph :: [JudocAtom 'Scoped] -> Sem r Html
+ goParagraph = fmap p . mconcatMapM goAtom
+ goAtom :: JudocAtom 'Scoped -> Sem r Html
+ goAtom = \case
+ JudocNewline -> return " "
+ JudocExpression e -> ppCodeHtml e
+ JudocText txt -> return (toHtml txt)
+ paragraphs :: [[JudocAtom 'Scoped]]
+ paragraphs = splitOn [JudocNewline, JudocNewline] atoms
+
+goStatement :: Members '[Reader HtmlOptions] r => Statement 'Scoped -> Sem r Html
+goStatement = \case
+ StatementTypeSignature t -> goTypeSignature t
+ StatementAxiom t -> goAxiom t
+ StatementInductive t -> goInductive t
+ StatementOpenModule t -> goOpen t
+ _ -> mempty
+
+goOpen :: forall r. Members '[Reader HtmlOptions] r => OpenModule 'Scoped -> Sem r Html
+goOpen op
+ | Public <- op ^. openPublic = noDefHeader <$> ppCodeHtml op
+ | otherwise = mempty
+
+goAxiom :: forall r. Members '[Reader HtmlOptions] r => AxiomDef 'Scoped -> Sem r Html
+goAxiom axiom = do
+ header' <- axiomHeader
+ defHeader tmp uid header' Nothing
+ where
+ uid :: NameId
+ uid = axiom ^. axiomName . S.nameId
+ tmp :: TopModulePath
+ tmp = axiom ^. axiomName . S.nameDefinedIn . S.absTopModulePath
+ axiomHeader :: Sem r Html
+ axiomHeader = ppCodeHtml (set axiomDoc Nothing axiom)
+
+goInductive :: forall r. Members '[Reader HtmlOptions] r => InductiveDef 'Scoped -> Sem r Html
+goInductive def = do
+ sig' <- inductiveHeader
+ header' <- defHeader tmp uid sig' (def ^. inductiveDoc)
+ body' <- goConstructors (def ^. inductiveConstructors)
+ return (header' <> body')
+ where
+ uid :: NameId
+ uid = def ^. inductiveName . S.nameId
+ tmp :: TopModulePath
+ tmp = def ^. inductiveName . S.nameDefinedIn . S.absTopModulePath
+ inductiveHeader :: Sem r Html
+ inductiveHeader =
+ runReader defaultOptions (ppInductiveSignature def) >>= ppCodeHtml
+
+goConstructors :: forall r. Members '[Reader HtmlOptions] r => [InductiveConstructorDef 'Scoped] -> Sem r Html
+goConstructors cc = do
+ tbl' <- table . tbody <$> mconcatMapM goConstructor cc
+ return $
+ Html.div ! Attr.class_ "subs constructors" $
+ (p ! Attr.class_ "caption" $ "Constructors")
+ <> tbl'
+ where
+ goConstructor :: InductiveConstructorDef 'Scoped -> Sem r Html
+ goConstructor c = do
+ src' <- srcPart
+ doc' <- docPart
+ return (tr (src' <> doc'))
+ where
+ docPart :: Sem r Html
+ docPart = do
+ td ! Attr.class_ "doc"
+ <$> goJudocMay (c ^. constructorDoc)
+
+ srcPart :: Sem r Html
+ srcPart = do
+ sig' <- ppCodeHtml (set constructorDoc Nothing c)
+ return $
+ td ! Attr.class_ "src" $
+ sig'
+
+noDefHeader :: Html -> Html
+noDefHeader = p ! Attr.class_ "src"
+
+defHeader :: forall r. Members '[Reader HtmlOptions] r => TopModulePath -> NameId -> Html -> Maybe (Judoc 'Scoped) -> Sem r Html
+defHeader tmp uid sig mjudoc = do
+ funHeader' <- functionHeader
+ judoc' <- judoc
+ return $
+ Html.div ! Attr.class_ "top" $
+ funHeader'
+ <> judoc'
+ where
+ judoc :: Sem r Html
+ judoc = do
+ judoc' <- goJudocMay mjudoc
+ return (Html.div ! Attr.class_ "doc" $ judoc')
+
+ functionHeader :: Sem r Html
+ functionHeader = do
+ sourceLink' <- sourceAndSelfLink tmp uid
+ return $ noDefHeader (sig <> sourceLink')
+
+goTypeSignature :: forall r. Members '[Reader HtmlOptions] r => TypeSignature 'Scoped -> Sem r Html
+goTypeSignature sig = do
+ sig' <- typeSig
+ defHeader tmp uid sig' (sig ^. sigDoc)
+ where
+ tmp :: TopModulePath
+ tmp = sig ^. sigName . S.nameDefinedIn . S.absTopModulePath
+ uid :: NameId
+ uid = sig ^. sigName . S.nameId
+ typeSig :: Sem r Html
+ typeSig = ppCodeHtml (set sigDoc Nothing sig)
+
+sourceAndSelfLink :: Members '[Reader HtmlOptions] r => TopModulePath -> NameId -> Sem r Html
+sourceAndSelfLink tmp name = do
+ ref' <- local (set htmlOptionsKind HtmlSrc) (nameIdAttrRef tmp (Just name))
+ return $
+ ( a
+ ! Attr.href ref'
+ ! Attr.class_ "link"
+ $ "Source"
+ )
+ <> ( a
+ ! Attr.href (selfLinkName name)
+ ! Attr.class_ "selflink"
+ $ "#"
+ )
+
+tagIden :: IsString a => NameId -> a
+tagIden x = fromText $ prettyText x
+
+selfLinkName :: IsString a => NameId -> a
+selfLinkName x = fromText $ "#" <> tagIden x
diff --git a/src/Juvix/Documentation/Extra.hs b/src/Juvix/Documentation/Extra.hs
new file mode 100644
index 0000000000..d064cce9cb
--- /dev/null
+++ b/src/Juvix/Documentation/Extra.hs
@@ -0,0 +1,48 @@
+module Juvix.Documentation.Extra where
+
+import Juvix.Prelude
+import Text.Blaze.Html5 as Html hiding (map)
+import Text.Blaze.Html5.Attributes qualified as Attr
+
+mathJaxCdn :: Html
+mathJaxCdn = script1 <> script2
+ where
+ script1 =
+ script
+ ! Attr.src src1
+ $ mempty
+ script2 =
+ script
+ ! Attr.type_ "text/javascript"
+ ! Attr.id "MathJax-script"
+ ! Attr.src src2
+ $ mempty
+ src1 :: AttributeValue
+ src1 = "https://polyfill.io/v3/polyfill.min.js?features=es6"
+ src2 :: AttributeValue
+ src2 = "https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js"
+
+-- | This is useful fore debugging only. Note that it only works on a server
+-- protocol, opening the file from the local system won't work. For that, one
+-- can use @python3 -m http.server@.
+livejs :: Html
+livejs =
+ script
+ ! Attr.type_ "text/javascript"
+ ! Attr.src "https://livejs.com/live.js"
+ $ mempty
+
+linuwialCss :: Html
+linuwialCss =
+ link
+ ! Attr.href "assets/linuwial.css"
+ ! Attr.rel "stylesheet"
+ ! Attr.type_ "text/css"
+ ! Attr.title "Linuwial"
+
+sourceCss :: Html
+sourceCss =
+ link
+ ! Attr.href "assets/source.css"
+ ! Attr.rel "stylesheet"
+ ! Attr.type_ "text/css"
diff --git a/src/Juvix/Internal/Strings.hs b/src/Juvix/Internal/Strings.hs
index b3c8d40117..1d6f5e019a 100644
--- a/src/Juvix/Internal/Strings.hs
+++ b/src/Juvix/Internal/Strings.hs
@@ -8,6 +8,9 @@ module_ = "module"
axiom :: IsString s => s
axiom = "axiom"
+judocStart :: IsString s => s
+judocStart = "---"
+
end :: IsString s => s
end = "end"
@@ -235,3 +238,6 @@ putStrLn_ = "putStrLn"
juvixFunctionT :: IsString s => s
juvixFunctionT = "juvix_function_t"
+
+juvixDotOrg :: IsString s => s
+juvixDotOrg = "https://juvix.org"
diff --git a/src/Juvix/Parsing/Lexer.hs b/src/Juvix/Parsing/Lexer.hs
index be2ab47bdc..ab87099130 100644
--- a/src/Juvix/Parsing/Lexer.hs
+++ b/src/Juvix/Parsing/Lexer.hs
@@ -23,13 +23,26 @@ makeLenses ''ParserParams
space :: forall r. Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
space = L.space space1 lineComment block
where
+ skipLineComment :: ParsecS r ()
+ skipLineComment = do
+ notFollowedBy (P.chunk Str.judocStart)
+ void (P.chunk "--")
+ void (P.takeWhileP Nothing (/= '\n'))
+
lineComment :: ParsecS r ()
- lineComment =
- interval (L.skipLineComment "--") >>= lift . registerComment . snd
+ lineComment = comment_ skipLineComment
block :: ParsecS r ()
- block =
- interval (L.skipBlockComment "{-" "-}") >>= lift . registerComment . snd
+ block = comment_ (L.skipBlockComment "{-" "-}")
+
+comment :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r a -> ParsecS r a
+comment c = do
+ (a, i) <- interval c
+ P.lift (registerComment i)
+ return a
+
+comment_ :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r a -> ParsecS r ()
+comment_ = void . comment
lexeme :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r a -> ParsecS r a
lexeme = L.lexeme space
diff --git a/src/Juvix/Parsing/Parser.hs b/src/Juvix/Parsing/Parser.hs
index f4a61d0d11..d805ebfdd4 100644
--- a/src/Juvix/Parsing/Parser.hs
+++ b/src/Juvix/Parsing/Parser.hs
@@ -8,6 +8,7 @@ where
import Data.List.NonEmpty.Extra qualified as NonEmpty
import Data.Singletons
+import Juvix.Internal.Strings qualified as Str
import Juvix.Parsing.Error
import Juvix.Parsing.InfoTable
import Juvix.Parsing.InfoTableBuilder
@@ -16,12 +17,11 @@ import Juvix.Parsing.ParserResult
import Juvix.Pipeline.EntryPoint
import Juvix.Prelude
import Juvix.Prelude.Pretty (Pretty, prettyText)
+import Juvix.Syntax.Concrete.Base (MonadParsec (takeWhile1P))
import Juvix.Syntax.Concrete.Base qualified as P
import Juvix.Syntax.Concrete.Language
---------------------------------------------------------------------------------
--- Running the parser
---------------------------------------------------------------------------------
+type JudocStash = State (Maybe (Judoc 'Parsed))
entryParser ::
Members '[Files, Error ParserError] r =>
@@ -46,7 +46,11 @@ entryParser e = do
-- an empty string.
runModuleParser :: FilePath -> FilePath -> Text -> Either ParserError (InfoTable, Module 'Parsed 'ModuleTop)
runModuleParser root fileName input =
- case run $ runInfoTableBuilder $ runReader params $ P.runParserT topModuleDef fileName input of
+ case run $
+ runInfoTableBuilder $
+ runReader params $
+ evalState (Nothing @(Judoc 'Parsed)) $
+ P.runParserT topModuleDef fileName input of
(_, Left err) -> Left (ParserError err)
(tbl, Right r) -> return (tbl, r)
where
@@ -56,32 +60,29 @@ runModuleParser root fileName input =
}
top ::
- Members '[Reader ParserParams, InfoTableBuilder] r =>
+ Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r =>
ParsecS r a ->
ParsecS r a
top p = space >> p <* (optional kwSemicolon >> P.eof)
topModuleDef ::
- Members '[Reader ParserParams, InfoTableBuilder] r =>
+ Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r =>
ParsecS r (Module 'Parsed 'ModuleTop)
-topModuleDef = top moduleDef
-
-topStatement ::
- Members '[Reader ParserParams, InfoTableBuilder] r =>
- ParsecS r (Statement 'Parsed)
-topStatement = top statement
+topModuleDef = do
+ void (optional judocBlock)
+ top moduleDef
--------------------------------------------------------------------------------
-- Symbols and names
--------------------------------------------------------------------------------
-symbol :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r Symbol
+symbol :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r Symbol
symbol = uncurry (flip WithLoc) <$> identifierL
-dottedSymbol :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (NonEmpty Symbol)
+dottedSymbol :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (NonEmpty Symbol)
dottedSymbol = fmap (uncurry (flip WithLoc)) <$> dottedIdentifier
-name :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r Name
+name :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r Name
name = do
parts <- dottedSymbol
return $ case nonEmptyUnsnoc parts of
@@ -91,18 +92,19 @@ name = do
mkTopModulePath :: NonEmpty Symbol -> TopModulePath
mkTopModulePath l = TopModulePath (NonEmpty.init l) (NonEmpty.last l)
-symbolList :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (NonEmpty Symbol)
+symbolList :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (NonEmpty Symbol)
symbolList = braces (P.sepBy1 symbol kwSemicolon)
-topModulePath :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r TopModulePath
+topModulePath :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r TopModulePath
topModulePath = mkTopModulePath <$> dottedSymbol
--------------------------------------------------------------------------------
-- Top level statement
--------------------------------------------------------------------------------
-statement :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (Statement 'Parsed)
-statement =
+statement :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (Statement 'Parsed)
+statement = do
+ void (optional judocBlock)
(StatementOperator <$> operatorSyntaxDef)
<|> (StatementOpenModule <$> openModule)
<|> (StatementImport <$> import_)
@@ -116,17 +118,46 @@ statement =
<$> auxTypeSigFunClause
)
-builtinInductive :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r BuiltinInductive
+judocBlock :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r ()
+judocBlock = do
+ b :: Judoc 'Parsed <- mconcat . toList <$> P.some judocLine
+ P.lift (modify (<> Just b))
+
+judocLine :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (Judoc 'Parsed)
+judocLine = lexeme $ do
+ comment_ (P.chunk Str.judocStart)
+ ln <- Judoc . (`snoc` JudocNewline) <$> many judocAtom
+ P.newline
+ return ln
+
+judocAtom :: forall r. Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (JudocAtom 'Parsed)
+judocAtom =
+ JudocText <$> judocText
+ <|> JudocExpression <$> judocExpression
+ where
+ judocText :: ParsecS r Text
+ judocText = comment (takeWhile1P Nothing isValidText)
+ where
+ isValidText :: Char -> Bool
+ isValidText = (`notElem` ['\n', ';'])
+ judocExpression :: ParsecS r (ExpressionAtoms 'Parsed)
+ judocExpression = do
+ comment_ (P.char ';')
+ e <- parseExpressionAtoms
+ comment_ (P.char ';')
+ return e
+
+builtinInductive :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r BuiltinInductive
builtinInductive = builtinHelper
-builtinFunction :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r BuiltinFunction
+builtinFunction :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r BuiltinFunction
builtinFunction = builtinHelper
-builtinAxiom :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r BuiltinAxiom
+builtinAxiom :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r BuiltinAxiom
builtinAxiom = builtinHelper
builtinHelper ::
- (Members '[Reader ParserParams, InfoTableBuilder] r, Bounded a, Enum a, Pretty a) =>
+ (Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r, Bounded a, Enum a, Pretty a) =>
ParsecS r a
builtinHelper =
P.choice
@@ -134,24 +165,24 @@ builtinHelper =
| a <- allElements
]
-builtinInductiveDef :: Members '[Reader ParserParams, InfoTableBuilder] r => BuiltinInductive -> ParsecS r (InductiveDef 'Parsed)
+builtinInductiveDef :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => BuiltinInductive -> ParsecS r (InductiveDef 'Parsed)
builtinInductiveDef = inductiveDef . Just
builtinAxiomDef ::
- Members '[Reader ParserParams, InfoTableBuilder] r =>
+ Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r =>
BuiltinAxiom ->
ParsecS r (AxiomDef 'Parsed)
builtinAxiomDef = axiomDef . Just
builtinTypeSig ::
- Members '[Reader ParserParams, InfoTableBuilder] r =>
+ Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r =>
BuiltinFunction ->
ParsecS r (TypeSignature 'Parsed)
builtinTypeSig b = do
fun <- symbol
typeSignature False fun (Just b)
-builtinStatement :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (Statement 'Parsed)
+builtinStatement :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (Statement 'Parsed)
builtinStatement = do
kwBuiltin
(builtinInductive >>= fmap StatementInductive . builtinInductiveDef)
@@ -162,7 +193,7 @@ builtinStatement = do
-- Compile
--------------------------------------------------------------------------------
-compileBlock :: forall r. Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (Compile 'Parsed)
+compileBlock :: forall r. Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (Compile 'Parsed)
compileBlock = do
kwCompile
_compileName <- symbol
@@ -181,10 +212,10 @@ compileBlock = do
-- Foreign
--------------------------------------------------------------------------------
-backend :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r Backend
+backend :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r Backend
backend = ghc $> BackendGhc <|> cBackend $> BackendC
-foreignBlock :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ForeignBlock
+foreignBlock :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r ForeignBlock
foreignBlock = do
kwForeign
_foreignBackend <- backend
@@ -195,10 +226,10 @@ foreignBlock = do
-- Operator syntax declaration
--------------------------------------------------------------------------------
-precedence :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r Precedence
+precedence :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r Precedence
precedence = PrecNat <$> (fst <$> decimal)
-operatorSyntaxDef :: forall r. Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r OperatorSyntaxDef
+operatorSyntaxDef :: forall r. Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r OperatorSyntaxDef
operatorSyntaxDef = do
_fixityArity <- arity
_fixityPrecedence <- precedence
@@ -218,7 +249,7 @@ operatorSyntaxDef = do
-- Import statement
--------------------------------------------------------------------------------
-import_ :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (Import 'Parsed)
+import_ :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (Import 'Parsed)
import_ = do
kwImport
_importModule <- topModulePath
@@ -228,7 +259,7 @@ import_ = do
-- Expression
--------------------------------------------------------------------------------
-expressionAtom :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (ExpressionAtom 'Parsed)
+expressionAtom :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (ExpressionAtom 'Parsed)
expressionAtom =
AtomLiteral <$> P.try literal
<|> (AtomIdentifier <$> name)
@@ -242,7 +273,7 @@ expressionAtom =
<|> braces (AtomBraces <$> withLoc parseExpressionAtoms)
parseExpressionAtoms ::
- Members '[Reader ParserParams, InfoTableBuilder] r =>
+ Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r =>
ParsecS r (ExpressionAtoms 'Parsed)
parseExpressionAtoms = do
(_expressionAtoms, _expressionAtomsLoc) <- interval (P.some expressionAtom)
@@ -252,38 +283,34 @@ parseExpressionAtoms = do
-- Holes
--------------------------------------------------------------------------------
-hole :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (HoleType 'Parsed)
+hole :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (HoleType 'Parsed)
hole = snd <$> interval kwHole
--------------------------------------------------------------------------------
-- Literals
--------------------------------------------------------------------------------
-literalInteger :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r LiteralLoc
+literalInteger :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r LiteralLoc
literalInteger = do
(x, loc) <- integer
return (WithLoc loc (LitInteger x))
-literalString :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r LiteralLoc
+literalString :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r LiteralLoc
literalString = do
(x, loc) <- string
return (WithLoc loc (LitString x))
-literal :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r LiteralLoc
+literal :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r LiteralLoc
literal = do
l <-
literalInteger
<|> literalString
P.lift (registerLiteral l)
---------------------------------------------------------------------------------
--- Let expression
---------------------------------------------------------------------------------
-
-letClause :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (LetClause 'Parsed)
+letClause :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (LetClause 'Parsed)
letClause = either LetTypeSig LetFunClause <$> auxTypeSigFunClause
-letBlock :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (LetBlock 'Parsed)
+letBlock :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (LetBlock 'Parsed)
letBlock = do
kwLet
_letClauses <- braces (P.sepEndBy letClause kwSemicolon)
@@ -295,7 +322,7 @@ letBlock = do
-- Universe expression
--------------------------------------------------------------------------------
-universe :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r Universe
+universe :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r Universe
universe = do
i <- snd <$> interval kwType
uni <- optional decimal
@@ -305,12 +332,14 @@ universe = do
Just (lvl, i') -> Universe (Just lvl) (i <> i')
)
--------------------------------------------------------------------------------
--- Type signature declaration
--------------------------------------------------------------------------------
+getJudoc :: Members '[JudocStash] r => ParsecS r (Maybe (Judoc 'Parsed))
+getJudoc = P.lift $ do
+ j <- get
+ put (Nothing @(Judoc 'Parsed))
+ return j
typeSignature ::
- Members '[Reader ParserParams, InfoTableBuilder] r =>
+ Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r =>
Bool ->
Symbol ->
Maybe BuiltinFunction ->
@@ -318,11 +347,12 @@ typeSignature ::
typeSignature _sigTerminating _sigName _sigBuiltin = do
kwColon
_sigType <- parseExpressionAtoms
+ _sigDoc <- getJudoc
return TypeSignature {..}
-- | Used to minimize the amount of required @P.try@s.
auxTypeSigFunClause ::
- Members '[Reader ParserParams, InfoTableBuilder] r =>
+ Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r =>
ParsecS r (Either (TypeSignature 'Parsed) (FunctionClause 'Parsed))
auxTypeSigFunClause = do
terminating <- isJust <$> optional kwTerminating
@@ -330,16 +360,13 @@ auxTypeSigFunClause = do
(Left <$> typeSignature terminating sym Nothing)
<|> (Right <$> functionClause sym)
--------------------------------------------------------------------------------
--- Axioms
--------------------------------------------------------------------------------
-
axiomDef ::
- Members '[Reader ParserParams, InfoTableBuilder] r =>
+ Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r =>
Maybe BuiltinAxiom ->
ParsecS r (AxiomDef 'Parsed)
axiomDef _axiomBuiltin = do
kwAxiom
+ _axiomDoc <- getJudoc
_axiomName <- symbol
kwColon
_axiomType <- parseExpressionAtoms
@@ -349,17 +376,17 @@ axiomDef _axiomBuiltin = do
-- Function expression
--------------------------------------------------------------------------------
-implicitOpen :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r IsImplicit
+implicitOpen :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r IsImplicit
implicitOpen =
lbrace $> Implicit
<|> lparen $> Explicit
-implicitClose :: Members '[Reader ParserParams, InfoTableBuilder] r => IsImplicit -> ParsecS r ()
+implicitClose :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => IsImplicit -> ParsecS r ()
implicitClose = \case
Implicit -> rbrace
Explicit -> rparen
-functionParam :: forall r. Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (FunctionParameter 'Parsed)
+functionParam :: forall r. Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (FunctionParameter 'Parsed)
functionParam = do
(_paramName, _paramUsage, _paramImplicit) <- P.try $ do
impl <- implicitOpen
@@ -381,7 +408,7 @@ functionParam = do
<|> (Just UsageOmega <$ kwColonOmega)
<|> (Nothing <$ kwColon)
-function :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (Function 'Parsed)
+function :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (Function 'Parsed)
function = do
_funParameter <- functionParam
kwRightArrow
@@ -392,12 +419,12 @@ function = do
-- Where block clauses
--------------------------------------------------------------------------------
-whereBlock :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (WhereBlock 'Parsed)
+whereBlock :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (WhereBlock 'Parsed)
whereBlock = do
kwWhere
WhereBlock <$> braces (P.sepEndBy1 whereClause kwSemicolon)
-whereClause :: forall r. Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (WhereClause 'Parsed)
+whereClause :: forall r. Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (WhereClause 'Parsed)
whereClause =
(WhereOpenModule <$> openModule)
<|> sigOrFun
@@ -409,14 +436,14 @@ whereClause =
-- Lambda expression
--------------------------------------------------------------------------------
-lambdaClause :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (LambdaClause 'Parsed)
+lambdaClause :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (LambdaClause 'Parsed)
lambdaClause = do
lambdaParameters <- P.some patternAtom
kwMapsTo
lambdaBody <- parseExpressionAtoms
return LambdaClause {..}
-lambda :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (Lambda 'Parsed)
+lambda :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (Lambda 'Parsed)
lambda = do
kwLambda
_lambdaClauses <- braces (P.sepEndBy lambdaClause kwSemicolon)
@@ -426,45 +453,47 @@ lambda = do
-- Data type construction declaration
-------------------------------------------------------------------------------
-inductiveDef :: Members '[Reader ParserParams, InfoTableBuilder] r => Maybe BuiltinInductive -> ParsecS r (InductiveDef 'Parsed)
+inductiveDef :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => Maybe BuiltinInductive -> ParsecS r (InductiveDef 'Parsed)
inductiveDef _inductiveBuiltin = do
_inductivePositive <- isJust <$> optional kwPositive
kwInductive
+ _inductiveDoc <- getJudoc
_inductiveName <- symbol
_inductiveParameters <- P.many inductiveParam
_inductiveType <- optional (kwColon >> parseExpressionAtoms)
_inductiveConstructors <- braces $ P.sepEndBy constructorDef kwSemicolon
return InductiveDef {..}
-inductiveParam :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (InductiveParameter 'Parsed)
+inductiveParam :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (InductiveParameter 'Parsed)
inductiveParam = parens $ do
_inductiveParameterName <- symbol
kwColon
_inductiveParameterType <- parseExpressionAtoms
return InductiveParameter {..}
-constructorDef :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (InductiveConstructorDef 'Parsed)
+constructorDef :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (InductiveConstructorDef 'Parsed)
constructorDef = do
+ _constructorDoc <- optional judocBlock >> getJudoc
_constructorName <- symbol
kwColon
_constructorType <- parseExpressionAtoms
return InductiveConstructorDef {..}
-wildcard :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r Wildcard
+wildcard :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r Wildcard
wildcard = Wildcard . snd <$> interval kwWildcard
--------------------------------------------------------------------------------
-- Pattern section
--------------------------------------------------------------------------------
-patternAtom :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (PatternAtom 'Parsed)
+patternAtom :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (PatternAtom 'Parsed)
patternAtom =
PatternAtomIden <$> name
<|> PatternAtomWildcard <$> wildcard
<|> (PatternAtomParens <$> parens parsePatternAtoms)
<|> (PatternAtomBraces <$> braces parsePatternAtoms)
-parsePatternAtoms :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (PatternAtoms 'Parsed)
+parsePatternAtoms :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (PatternAtoms 'Parsed)
parsePatternAtoms = do
(_patternAtoms, _patternAtomsLoc) <- interval (P.some patternAtom)
return PatternAtoms {..}
@@ -473,7 +502,7 @@ parsePatternAtoms = do
-- Function binding declaration
--------------------------------------------------------------------------------
-functionClause :: Members '[Reader ParserParams, InfoTableBuilder] r => Symbol -> ParsecS r (FunctionClause 'Parsed)
+functionClause :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => Symbol -> ParsecS r (FunctionClause 'Parsed)
functionClause _clauseOwnerFunction = do
_clausePatterns <- P.many patternAtom
kwAssignment
@@ -485,14 +514,15 @@ functionClause _clauseOwnerFunction = do
-- Module declaration
--------------------------------------------------------------------------------
-pmodulePath :: forall t r. (SingI t, Members '[Reader ParserParams, InfoTableBuilder] r) => ParsecS r (ModulePathType 'Parsed t)
+pmodulePath :: forall t r. (SingI t, Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r) => ParsecS r (ModulePathType 'Parsed t)
pmodulePath = case sing :: SModuleIsTop t of
SModuleTop -> topModulePath
SModuleLocal -> symbol
-moduleDef :: (SingI t, Members '[Reader ParserParams, InfoTableBuilder] r) => ParsecS r (Module 'Parsed t)
+moduleDef :: (SingI t, Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r) => ParsecS r (Module 'Parsed t)
moduleDef = do
kwModule
+ _moduleDoc <- getJudoc
_modulePath <- pmodulePath
_moduleParameters <- many inductiveParam
kwSemicolon
@@ -501,7 +531,7 @@ moduleDef = do
return Module {..}
-- | An ExpressionAtom which is a valid expression on its own.
-atomicExpression :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (ExpressionAtoms 'Parsed)
+atomicExpression :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (ExpressionAtoms 'Parsed)
atomicExpression = do
(atom, loc) <- interval expressionAtom
case atom of
@@ -509,7 +539,7 @@ atomicExpression = do
_ -> return ()
return $ ExpressionAtoms (NonEmpty.singleton atom) loc
-openModule :: forall r. Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (OpenModule 'Parsed)
+openModule :: forall r. Members '[Reader ParserParams, InfoTableBuilder, JudocStash] r => ParsecS r (OpenModule 'Parsed)
openModule = do
kwOpen
_openModuleImport <- isJust <$> optional kwImport
diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index cfbb4f46c7..5283030418 100644
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@@ -278,19 +278,22 @@ infixl 7 <+?>
(<+?>) :: Doc ann -> Maybe (Doc ann) -> Doc ann
(<+?>) a = maybe a (a <+>)
-infixl 7
+infixr 7
() :: Maybe (Doc ann) -> Doc ann -> Doc ann
() = \case
Nothing -> id
Just a -> (a <+>)
-infixl 7
+infixr 7 ?<>
-() :: Semigroup m => m -> Maybe m -> m
-() a = maybe a (a <>)
+(?<>) :: Semigroup m => Maybe m -> m -> m
+(?<>) = maybe id (<>)
---------------------------------------------------------------------------------
+infixl 7 <>?
+
+(<>?) :: Semigroup m => m -> Maybe m -> m
+(<>?) a = maybe a (a <>)
data Indexed a = Indexed
{ _indexedIx :: Int,
diff --git a/src/Juvix/Prelude/Html.hs b/src/Juvix/Prelude/Html.hs
new file mode 100644
index 0000000000..232aac5cf8
--- /dev/null
+++ b/src/Juvix/Prelude/Html.hs
@@ -0,0 +1,28 @@
+module Juvix.Prelude.Html where
+
+import Juvix.Prelude
+import Text.Blaze.Html5 as Html hiding (map)
+import Text.Blaze.Html5.Attributes qualified as Attr
+
+cssLink :: AttributeValue -> Html
+cssLink css =
+ link
+ ! Attr.href css
+ ! Attr.rel "stylesheet"
+ ! Attr.type_ "text/css"
+
+ayuCss :: Html
+ayuCss = cssLink "assets/source-ayu-light.css"
+
+nordCss :: Html
+nordCss = cssLink "assets/source-nord.css"
+
+highlightJs :: Html
+highlightJs =
+ script
+ ! Attr.src "assets/highlight.js"
+ ! Attr.type_ "text/javascript"
+ $ mempty
+
+metaUtf8 :: Html
+metaUtf8 = meta ! Attr.charset "UTF-8"
diff --git a/src/Juvix/Prelude/Pretty.hs b/src/Juvix/Prelude/Pretty.hs
index 0d066b4e9f..3b8140551a 100644
--- a/src/Juvix/Prelude/Pretty.hs
+++ b/src/Juvix/Prelude/Pretty.hs
@@ -78,6 +78,9 @@ vsep2 = concatWith (\a b -> a <> line <> line <> b)
hsep :: Foldable f => f (Doc a) -> Doc a
hsep = PP.hsep . toList
+enclose1 :: Doc a -> Doc a -> Doc a
+enclose1 delim = enclose delim delim
+
vsepMaybe :: Foldable f => f (Doc a) -> Maybe (Doc a)
vsepMaybe l
| null l = Nothing
diff --git a/src/Juvix/Syntax/Abstract/Name.hs b/src/Juvix/Syntax/Abstract/Name.hs
index e012a77f9f..03f0a56542 100644
--- a/src/Juvix/Syntax/Abstract/Name.hs
+++ b/src/Juvix/Syntax/Abstract/Name.hs
@@ -51,7 +51,7 @@ prettyName :: HasNameKindAnn a => Bool -> Name -> Doc a
prettyName showNameId n =
annotate
(annNameKind (n ^. nameKind))
- (pretty (n ^. namePretty) uid)
+ (pretty (n ^. namePretty) <>? uid)
where
uid
| showNameId = Just ("@" <> pretty (n ^. nameId))
diff --git a/src/Juvix/Syntax/Abstract/Pretty/Ann.hs b/src/Juvix/Syntax/Abstract/Pretty/Ann.hs
index c894c221b7..a21a5607a7 100644
--- a/src/Juvix/Syntax/Abstract/Pretty/Ann.hs
+++ b/src/Juvix/Syntax/Abstract/Pretty/Ann.hs
@@ -16,6 +16,7 @@ fromScopedAnn s = case s of
S.AnnKind nk -> Just (AnnKind nk)
S.AnnKeyword -> Nothing
S.AnnDelimiter -> Nothing
+ S.AnnComment -> Nothing
S.AnnUnkindedSym -> Nothing
S.AnnDef {} -> Nothing
S.AnnRef {} -> Nothing
diff --git a/src/Juvix/Syntax/Concrete/Language.hs b/src/Juvix/Syntax/Concrete/Language.hs
index 60a2a2ed70..68a601e6a8 100644
--- a/src/Juvix/Syntax/Concrete/Language.hs
+++ b/src/Juvix/Syntax/Concrete/Language.hs
@@ -187,6 +187,7 @@ instance HasLoc OperatorSyntaxDef where
data TypeSignature (s :: Stage) = TypeSignature
{ _sigName :: FunctionName s,
_sigType :: ExpressionType s,
+ _sigDoc :: Maybe (Judoc s),
_sigBuiltin :: Maybe BuiltinFunction,
_sigTerminating :: Bool
}
@@ -202,7 +203,8 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Typ
-------------------------------------------------------------------------------
data AxiomDef (s :: Stage) = AxiomDef
- { _axiomName :: SymbolType s,
+ { _axiomDoc :: Maybe (Judoc s),
+ _axiomName :: SymbolType s,
_axiomBuiltin :: Maybe BuiltinAxiom,
_axiomType :: ExpressionType s
}
@@ -223,6 +225,7 @@ type InductiveName s = SymbolType s
data InductiveConstructorDef (s :: Stage) = InductiveConstructorDef
{ _constructorName :: InductiveConstructorName s,
+ _constructorDoc :: Maybe (Judoc s),
_constructorType :: ExpressionType s
}
@@ -245,6 +248,7 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Ind
data InductiveDef (s :: Stage) = InductiveDef
{ _inductiveBuiltin :: Maybe BuiltinInductive,
+ _inductiveDoc :: Maybe (Judoc s),
_inductiveName :: InductiveName s,
_inductiveParameters :: [InductiveParameter s],
_inductiveType :: Maybe (ExpressionType s),
@@ -383,6 +387,7 @@ type LocalModuleName s = SymbolType s
data Module (s :: Stage) (t :: ModuleIsTop) = Module
{ _modulePath :: ModulePathType s t,
_moduleParameters :: [InductiveParameter s],
+ _moduleDoc :: Maybe (Judoc s),
_moduleBody :: [Statement s]
}
@@ -897,7 +902,30 @@ data ExpressionAtoms (s :: Stage) = ExpressionAtoms
_expressionAtomsLoc :: Interval
}
+newtype Judoc (s :: Stage) = Judoc
+ { _block :: [JudocAtom s]
+ }
+ deriving newtype (Semigroup, Monoid)
+
+deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (Judoc s)
+
+deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (Judoc s)
+
+deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Judoc s)
+
+data JudocAtom (s :: Stage)
+ = JudocExpression (ExpressionType s)
+ | JudocText Text
+ | JudocNewline
+
+deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (JudocAtom s)
+
+deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (JudocAtom s)
+
+deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (JudocAtom s)
+
makeLenses ''PatternArg
+makeLenses ''Judoc
makeLenses ''Function
makeLenses ''InductiveDef
makeLenses ''PostfixApplication
diff --git a/src/Juvix/Syntax/Concrete/Name.hs b/src/Juvix/Syntax/Concrete/Name.hs
index 2d2c861e2c..bcfd4a41a1 100644
--- a/src/Juvix/Syntax/Concrete/Name.hs
+++ b/src/Juvix/Syntax/Concrete/Name.hs
@@ -2,7 +2,7 @@ module Juvix.Syntax.Concrete.Name where
import Data.List.NonEmpty.Extra qualified as NonEmpty
import Juvix.Prelude
-import Juvix.Prelude.Pretty
+import Juvix.Prelude.Pretty as Pretty
import Juvix.Syntax.Loc
type Symbol = WithLoc Text
@@ -70,6 +70,10 @@ data TopModulePath = TopModulePath
makeLenses ''TopModulePath
+instance Pretty TopModulePath where
+ pretty (TopModulePath path name) =
+ mconcat (punctuate Pretty.dot (map pretty (snoc path name)))
+
instance HasLoc TopModulePath where
getLoc TopModulePath {..} =
case _modulePathDir of
@@ -79,17 +83,28 @@ instance HasLoc TopModulePath where
topModulePathToFilePath :: FilePath -> TopModulePath -> FilePath
topModulePathToFilePath = topModulePathToFilePath' (Just ".juvix")
-topModulePathToFilePath' ::
- Maybe String -> FilePath -> TopModulePath -> FilePath
-topModulePathToFilePath' ext root mp = normalise absPath
+topModulePathToRelativeFilePath :: Maybe String -> String -> (FilePath -> FilePath -> FilePath) -> TopModulePath -> FilePath
+topModulePathToRelativeFilePath ext suffix joinpath mp = relFilePath
where
- relDirPath = foldr (() . toPath) mempty (mp ^. modulePathDir)
- relFilePath = relDirPath toPath (mp ^. modulePathName)
- absPath = case ext of
- Nothing -> root relFilePath
- Just e -> root relFilePath <.> e
+ relDirPath :: FilePath
+ relDirPath = foldr (joinpath . toPath) mempty (mp ^. modulePathDir)
+ relFilePath :: FilePath
+ relFilePath = addExt (relDirPath `joinpath'` toPath (mp ^. modulePathName) <> suffix)
+ joinpath' :: FilePath -> FilePath -> FilePath
+ joinpath' l r
+ | null l = r
+ | otherwise = joinpath l r
+ addExt = case ext of
+ Nothing -> id
+ Just e -> (<.> e)
toPath :: Symbol -> FilePath
- toPath s = unpack (s ^. withLocParam)
+ toPath s = unpack (s ^. symbolText)
+
+topModulePathToFilePath' ::
+ Maybe String -> FilePath -> TopModulePath -> FilePath
+topModulePathToFilePath' ext root mp =
+ normalise
+ (root topModulePathToRelativeFilePath ext "" () mp)
topModulePathToDottedPath :: IsString s => TopModulePath -> s
topModulePathToDottedPath (TopModulePath l r) =
diff --git a/src/Juvix/Syntax/Concrete/Scoped/Error/Types.hs b/src/Juvix/Syntax/Concrete/Scoped/Error/Types.hs
index d64b92652b..15417451b0 100644
--- a/src/Juvix/Syntax/Concrete/Scoped/Error/Types.hs
+++ b/src/Juvix/Syntax/Concrete/Scoped/Error/Types.hs
@@ -259,8 +259,9 @@ instance ToGenericError NotInScope where
}
where
msg =
- "Symbol not in scope:" <+> ppCode _notInScopeSymbol
- ((line <>) <$> suggestion)
+ "Symbol not in scope:"
+ <+> ppCode _notInScopeSymbol
+ <>? ((line <>) <$> suggestion)
suggestion :: Maybe (Doc a)
suggestion
| null suggestions = Nothing
diff --git a/src/Juvix/Syntax/Concrete/Scoped/Pretty/Ann.hs b/src/Juvix/Syntax/Concrete/Scoped/Pretty/Ann.hs
index 1f58d9dce0..b52b767d0c 100644
--- a/src/Juvix/Syntax/Concrete/Scoped/Pretty/Ann.hs
+++ b/src/Juvix/Syntax/Concrete/Scoped/Pretty/Ann.hs
@@ -6,6 +6,7 @@ import Juvix.Syntax.Concrete.Scoped.Name qualified as S
data Ann
= AnnKind S.NameKind
| AnnKeyword
+ | AnnComment
| AnnDelimiter
| AnnLiteralString
| AnnLiteralInteger
diff --git a/src/Juvix/Syntax/Concrete/Scoped/Pretty/Ansi.hs b/src/Juvix/Syntax/Concrete/Scoped/Pretty/Ansi.hs
index 89322b919a..db099b74f7 100644
--- a/src/Juvix/Syntax/Concrete/Scoped/Pretty/Ansi.hs
+++ b/src/Juvix/Syntax/Concrete/Scoped/Pretty/Ansi.hs
@@ -9,6 +9,7 @@ stylize :: Ann -> AnsiStyle
stylize a = case a of
AnnKind k -> nameKindAnsi k
AnnDelimiter -> colorDull White
+ AnnComment -> colorDull Cyan
AnnKeyword -> colorDull Blue
AnnDef {} -> mempty
AnnRef {} -> mempty
diff --git a/src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs b/src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs
index dca4110df2..0780904be0 100644
--- a/src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs
+++ b/src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs
@@ -319,7 +319,12 @@ instance PrettyCode BackendItem where
backend <+> kwMapsto <+> ppStringLit _backendItemCode
ppStringLit :: Text -> Doc Ann
-ppStringLit = annotate AnnLiteralString . doubleQuotes . pretty
+ppStringLit = annotate AnnLiteralString . doubleQuotes . escaped
+ where
+ showChar :: Char -> String
+ showChar c = showLitChar c ("" :: String)
+ escaped :: Text -> Doc a
+ escaped = mconcatMap (pretty . showChar) . unpack
ppTopModulePath ::
forall s r.
@@ -363,16 +368,18 @@ instance (SingI s, SingI t) => PrettyCode (Module s t) where
moduleBody' <- ppCode _moduleBody >>= indented
modulePath' <- ppModulePathType _modulePath
moduleParameters' <- ppInductiveParameters _moduleParameters
- return
- $ kwModule
+ moduleDoc' <- mapM ppCode _moduleDoc
+ return $
+ moduleDoc'
+ ?<> kwModule
<+> modulePath'
<+?> moduleParameters'
- <> kwSemicolon
- <> line
- <> moduleBody'
- <> line
- <> kwEnd
- lastSemicolon
+ <> kwSemicolon
+ <> line
+ <> moduleBody'
+ <> line
+ <> kwEnd
+ <>? lastSemicolon
where
lastSemicolon = case sing :: SModuleIsTop t of
SModuleLocal -> Nothing
@@ -408,7 +415,8 @@ instance SingI s => PrettyCode (InductiveConstructorDef s) where
ppCode InductiveConstructorDef {..} = do
constructorName' <- annDef _constructorName <$> ppSymbol _constructorName
constructorType' <- ppExpression _constructorType
- return $ constructorName' <+> kwColon <+> constructorType'
+ doc' <- mapM ppCode _constructorDoc
+ return $ doc' ?<> constructorName' <+> kwColon <+> constructorType'
instance PrettyCode BuiltinInductive where
ppCode i = return (kwBuiltin <+> keyword' i)
@@ -419,26 +427,34 @@ instance PrettyCode BuiltinFunction where
instance PrettyCode BuiltinAxiom where
ppCode i = return (kwBuiltin <+> keyword' i)
+ppInductiveSignature :: forall r s. (SingI s, Members '[Reader Options] r) => InductiveDef s -> Sem r (Doc Ann)
+ppInductiveSignature InductiveDef {..} = do
+ inductivebuiltin' <- traverse ppCode _inductiveBuiltin
+ inductiveName' <- annDef _inductiveName <$> ppSymbol _inductiveName
+ inductiveParameters' <- ppInductiveParameters _inductiveParameters
+ inductiveType' <- ppTypeType
+ return $
+ inductivebuiltin'
+ kwInductive
+ <+> inductiveName'
+ <+?> inductiveParameters'
+ <+?> inductiveType'
+ where
+ ppTypeType :: Sem r (Maybe (Doc Ann))
+ ppTypeType = case _inductiveType of
+ Nothing -> return Nothing
+ Just e -> Just . (kwColon <+>) <$> ppExpression e
+
+instance PrettyCode (Doc Ann) where
+ ppCode d = return d
+
instance SingI s => PrettyCode (InductiveDef s) where
ppCode :: forall r. Members '[Reader Options] r => InductiveDef s -> Sem r (Doc Ann)
- ppCode InductiveDef {..} = do
- inductiveName' <- annDef _inductiveName <$> ppSymbol _inductiveName
- inductiveParameters' <- ppInductiveParameters _inductiveParameters
- inductiveType' <- ppTypeType
+ ppCode d@InductiveDef {..} = do
+ doc' <- mapM ppCode _inductiveDoc
+ sig' <- ppInductiveSignature d
inductiveConstructors' <- ppBlock _inductiveConstructors
- inductivebuiltin' <- traverse ppCode _inductiveBuiltin
- return $
- inductivebuiltin'
- kwInductive
- <+> inductiveName'
- <+?> inductiveParameters'
- <+?> inductiveType'
- <+> inductiveConstructors'
- where
- ppTypeType :: Sem r (Maybe (Doc Ann))
- ppTypeType = case _inductiveType of
- Nothing -> return Nothing
- Just e -> Just . (kwColon <+>) <$> ppExpression e
+ return $ doc' ?<> sig' <+> inductiveConstructors'
dotted :: Foldable f => f (Doc Ann) -> Doc Ann
dotted = concatWith (surround kwDot)
@@ -487,7 +503,7 @@ instance PrettyCode n => PrettyCode (S.Name' n) where
ppCode S.Name' {..} = do
nameConcrete' <- annotateKind _nameKind <$> ppCode _nameConcrete
uid <- nameIdSuffix _nameId
- return $ annSRef (nameConcrete' uid)
+ return $ annSRef (nameConcrete' <>? uid)
where
annSRef :: Doc Ann -> Doc Ann
annSRef = annotate (AnnRef (_nameDefinedIn ^. S.absTopModulePath) _nameId)
@@ -505,7 +521,7 @@ instance SingI s => PrettyCode (OpenModule s) where
openParameters' <- ppOpenParams
let openPublic' = ppPublic
import_
- | _openModuleImport = Just Str.import_
+ | _openModuleImport = Just kwImport
| otherwise = Nothing
return $ kwOpen <+?> import_ <+> openModuleName' <+?> openParameters' <+?> openUsingHiding' <+?> openPublic'
where
@@ -531,13 +547,43 @@ instance SingI s => PrettyCode (OpenModule s) where
Public -> Just kwPublic
NoPublic -> Nothing
+instance SingI s => PrettyCode (Judoc s) where
+ ppCode :: forall r. Members '[Reader Options] r => Judoc s -> Sem r (Doc Ann)
+ ppCode (Judoc blck) =
+ mconcatMapM ppLine (linesBy isNewLine blck)
+ where
+ isNewLine :: JudocAtom s -> Bool
+ isNewLine = \case
+ JudocNewline -> True
+ _ -> False
+ ppLine :: [JudocAtom s] -> Sem r (Doc Ann)
+ ppLine atoms = do
+ atoms' <- mconcatMapM ppCode atoms
+ let prefix = pretty (Str.judocStart :: Text) :: Doc Ann
+ return $ prefix <> atoms' <> line
+
+instance SingI s => PrettyCode (JudocAtom s) where
+ ppCode :: forall r. (Members '[Reader Options] r) => JudocAtom s -> Sem r (Doc Ann)
+ ppCode = \case
+ JudocNewline -> return "\n"
+ JudocExpression e -> goExpression e
+ JudocText t -> return (annotate AnnComment (pretty t))
+ where
+ goExpression :: ExpressionType s -> Sem r (Doc Ann)
+ goExpression e = do
+ e' <- ppExpression e
+ return $ semiDelim e'
+ semiDelim :: Doc Ann -> Doc Ann
+ semiDelim = enclose1 (annotate AnnComment ";")
+
instance SingI s => PrettyCode (TypeSignature s) where
ppCode TypeSignature {..} = do
let sigTerminating' = if _sigTerminating then kwTerminating <> line else mempty
sigName' <- annDef _sigName <$> ppSymbol _sigName
sigType' <- ppExpression _sigType
builtin' <- traverse ppCode _sigBuiltin
- return $ builtin' sigTerminating' <> sigName' <+> kwColon <+> sigType'
+ doc' <- mapM ppCode _sigDoc
+ return $ doc' ?<> builtin' sigTerminating' <> sigName' <+> kwColon <+> sigType'
instance SingI s => PrettyCode (Function s) where
ppCode :: forall r. Members '[Reader Options] r => Function s -> Sem r (Doc Ann)
@@ -624,10 +670,11 @@ instance SingI s => PrettyCode (WhereClause s) where
instance SingI s => PrettyCode (AxiomDef s) where
ppCode AxiomDef {..} = do
- axiomName' <- ppSymbol _axiomName
+ axiomName' <- annDef _axiomName <$> ppSymbol _axiomName
+ axiomDoc' <- mapM ppCode _axiomDoc
axiomType' <- ppExpression _axiomType
builtin' <- traverse ppCode _axiomBuiltin
- return $ builtin' kwAxiom <+> axiomName' <+> kwColon <+> axiomType'
+ return $ axiomDoc' ?<> builtin' kwAxiom <+> axiomName' <+> kwColon <+> axiomType'
instance SingI s => PrettyCode (Import s) where
ppCode :: forall r. Members '[Reader Options] r => Import s -> Sem r (Doc Ann)
@@ -833,7 +880,7 @@ ppHole w = case sing :: SStage s of
instance PrettyCode Hole where
ppCode h = do
suff <- nameIdSuffix (h ^. holeId)
- return (kwWildcard suff)
+ return (kwWildcard <>? suff)
instance SingI s => PrettyCode (ExpressionAtom s) where
ppCode = \case
diff --git a/src/Juvix/Syntax/Concrete/Scoped/Pretty/Html.hs b/src/Juvix/Syntax/Concrete/Scoped/Pretty/Html.hs
index 46187a2961..6374e337a3 100644
--- a/src/Juvix/Syntax/Concrete/Scoped/Pretty/Html.hs
+++ b/src/Juvix/Syntax/Concrete/Scoped/Pretty/Html.hs
@@ -1,4 +1,4 @@
-module Juvix.Syntax.Concrete.Scoped.Pretty.Html (genHtml, Theme (..)) where
+module Juvix.Syntax.Concrete.Scoped.Pretty.Html where
import Data.ByteString qualified as BS
import Data.Text qualified as Text
@@ -7,6 +7,7 @@ import Data.Text.Lazy (toStrict)
import Data.Time.Clock
import Data.Time.Format
import Juvix.Prelude
+import Juvix.Prelude.Html
import Juvix.Syntax.Concrete.Language
import Juvix.Syntax.Concrete.Scoped.Name qualified as S
import Juvix.Syntax.Concrete.Scoped.Pretty.Base
@@ -25,6 +26,21 @@ data Theme
| Ayu
deriving stock (Show)
+data HtmlKind
+ = HtmlDoc
+ | HtmlSrc
+
+newtype HtmlOptions = HtmlOptions
+ { _htmlOptionsKind :: HtmlKind
+ }
+
+makeLenses ''HtmlOptions
+
+kindSuffix :: HtmlKind -> String
+kindSuffix = \case
+ HtmlDoc -> ""
+ HtmlSrc -> "-src"
+
genHtml :: Options -> Bool -> Theme -> FilePath -> Bool -> Module 'Scoped 'ModuleTop -> IO ()
genHtml opts recursive theme outputDir printMetadata entry = do
createDirectoryIfMissing True outputDir
@@ -58,26 +74,31 @@ genHtml opts recursive theme outputDir printMetadata entry = do
where
htmlFile = topModulePathToDottedPath (m ^. modulePath . S.nameConcrete) <.> ".html"
-genModule :: Options -> Bool -> UTCTime -> Theme -> Module 'Scoped 'ModuleTop -> Text
-genModule opts printMetadata utc theme m =
- toStrict $
- Html.renderHtml $
- docTypeHtml ! Attr.xmlns "http://www.w3.org/1999/xhtml" $
- mhead
- <> mbody
- <> if printMetadata then infoFooter else mempty
+genModuleHtml :: Options -> Bool -> UTCTime -> Theme -> Module 'Scoped 'ModuleTop -> Html
+genModuleHtml opts printMetadata utc theme m =
+ docTypeHtml ! Attr.xmlns "http://www.w3.org/1999/xhtml" $
+ mhead
+ <> mbody
+ <> if printMetadata then infoFooter else mempty
where
themeCss :: Html
themeCss = case theme of
Ayu -> ayuCss
Nord -> nordCss
+ htmlOpts :: HtmlOptions
+ htmlOpts =
+ HtmlOptions
+ { _htmlOptionsKind = HtmlSrc
+ }
+
+ pp :: PrettyCode a => a -> Html
+ pp = ppCodeHtml' htmlOpts opts
+
prettySrc :: Html
prettySrc =
(pre ! Attr.id "src-content") $
- renderTree $
- treeForm $
- docStream' opts m
+ pp m
mheader :: Html
mheader =
@@ -109,44 +130,69 @@ genModule opts printMetadata utc theme m =
formattedTime = formatTime defaultTimeLocale "%Y-%m-%d %-H:%M %Z" utc
-docStream' :: Options -> Module 'Scoped 'ModuleTop -> SimpleDocStream Ann
+genModule :: Options -> Bool -> UTCTime -> Theme -> Module 'Scoped 'ModuleTop -> Text
+genModule opts printMetadata utc theme =
+ toStrict
+ . Html.renderHtml
+ . genModuleHtml opts printMetadata utc theme
+
+docStream' :: PrettyCode a => Options -> a -> SimpleDocStream Ann
docStream' opts m = layoutPretty defaultLayoutOptions (runPrettyCode opts m)
-renderTree :: SimpleDocTree Ann -> Html
+renderTree :: Members '[Reader HtmlOptions] r => SimpleDocTree Ann -> Sem r Html
renderTree = go
-go :: SimpleDocTree Ann -> Html
+ppCodeHtml' :: PrettyCode a => HtmlOptions -> Options -> a -> Html
+ppCodeHtml' htmlOpts opts = run . runReader htmlOpts . renderTree . treeForm . docStream' opts
+
+ppCodeHtml :: (Members '[Reader HtmlOptions] r, PrettyCode a) => a -> Sem r Html
+ppCodeHtml x = do
+ o <- ask
+ return (ppCodeHtml' o defaultOptions x)
+
+go :: Members '[Reader HtmlOptions] r => SimpleDocTree Ann -> Sem r Html
go sdt = case sdt of
- STEmpty -> mempty
- STChar c -> toHtml c
- STText _ t -> toHtml t
- STLine s -> "\n" <> toHtml (textSpaces s)
- STAnn ann content -> putTag ann (go content)
+ STEmpty -> return mempty
+ STChar c -> return (toHtml c)
+ STText _ t -> return (toHtml t)
+ STLine s -> return ("\n" <> toHtml (textSpaces s))
+ STAnn ann content -> go content >>= putTag ann
STConcat l -> mconcatMap go l
where
textSpaces :: Int -> Text
textSpaces n = Text.replicate n (Text.singleton ' ')
-putTag :: Ann -> Html -> Html
+putTag :: forall r. Members '[Reader HtmlOptions] r => Ann -> Html -> Sem r Html
putTag ann x = case ann of
- AnnKind k -> tagKind k x
- AnnLiteralInteger -> Html.span ! Attr.class_ "ju-number" $ x
- AnnLiteralString -> Html.span ! Attr.class_ "ju-string" $ x
- AnnKeyword -> Html.span ! Attr.class_ "ju-keyword" $ x
- AnnUnkindedSym -> Html.span ! Attr.class_ "ju-var" $ x
- AnnDelimiter -> Html.span ! Attr.class_ "ju-delimiter" $ x
- AnnDef tmp ni -> tagDef tmp ni
+ AnnKind k -> return (tagKind k x)
+ AnnLiteralInteger -> return (Html.span ! Attr.class_ "ju-number" $ x)
+ AnnLiteralString -> return (Html.span ! Attr.class_ "ju-string" $ x)
+ AnnKeyword -> return (Html.span ! Attr.class_ "ju-keyword" $ x)
+ AnnUnkindedSym -> return (Html.span ! Attr.class_ "ju-var" $ x)
+ AnnComment -> return (Html.span ! Attr.class_ "ju-var" $ x) -- TODO add comment class
+ AnnDelimiter -> return (Html.span ! Attr.class_ "ju-delimiter" $ x)
+ AnnDef tmp ni -> boldDefine <*> tagDef tmp ni
AnnRef tmp ni -> tagRef tmp ni
where
- tagDef :: TopModulePath -> S.NameId -> Html
- tagDef tmp nid =
- Html.span ! Attr.id (nameIdAttr nid) $
- tagRef tmp nid
-
- tagRef tmp ni =
- Html.span ! Attr.class_ "annot" $
- a ! Attr.href (nameIdAttrRef tmp ni) $
- x
+ boldDefine :: Sem r (Html -> Html)
+ boldDefine =
+ asks (^. htmlOptionsKind) <&> \case
+ HtmlDoc -> Html.span ! Attr.class_ "ju-define"
+ HtmlSrc -> id
+
+ tagDef :: TopModulePath -> S.NameId -> Sem r Html
+ tagDef tmp nid = do
+ ref' <- tagRef tmp nid
+ return $ (Html.span ! Attr.id (nameIdAttr nid)) ref'
+
+ tagRef :: TopModulePath -> S.NameId -> Sem r Html
+ tagRef tmp ni = do
+ pth <- nameIdAttrRef tmp (Just ni)
+ return $
+ Html.span ! Attr.class_ "annot" $
+ a ! Attr.href pth $
+ x
+
tagKind k =
Html.span
! Attr.class_
@@ -163,29 +209,15 @@ putTag ann x = case ann of
nameIdAttr :: S.NameId -> AttributeValue
nameIdAttr (S.NameId k) = fromString . show $ k
-nameIdAttrRef :: TopModulePath -> S.NameId -> AttributeValue
-nameIdAttrRef tp s =
- topModulePathToDottedPath tp <> ".html" <> preEscapedToValue '#' <> nameIdAttr s
-
-cssLink :: AttributeValue -> Html
-cssLink css =
- link
- ! Attr.href css
- ! Attr.rel "stylesheet"
- ! Attr.type_ "text/css"
-
-ayuCss :: Html
-ayuCss = cssLink "assets/source-ayu-light.css"
-
-nordCss :: Html
-nordCss = cssLink "assets/source-nord.css"
-
-highlightJs :: Html
-highlightJs =
- script
- ! Attr.src "assets/highlight.js"
- ! Attr.type_ "text/javascript"
- $ mempty
+moduleDocRelativePath :: Members '[Reader HtmlOptions] r => TopModulePath -> Sem r FilePath
+moduleDocRelativePath m = do
+ suff <- kindSuffix <$> asks (^. htmlOptionsKind)
+ return (topModulePathToRelativeFilePath (Just "html") suff joinDot m)
+ where
+ joinDot :: FilePath -> FilePath -> FilePath
+ joinDot l r = l <.> r
-metaUtf8 :: Html
-metaUtf8 = meta ! Attr.charset "UTF-8"
+nameIdAttrRef :: Members '[Reader HtmlOptions] r => TopModulePath -> Maybe S.NameId -> Sem r AttributeValue
+nameIdAttrRef tp s = do
+ pth <- moduleDocRelativePath tp
+ return (fromString pth <> preEscapedToValue '#' <>? (nameIdAttr <$> s))
diff --git a/src/Juvix/Syntax/Concrete/Scoped/Utils.hs b/src/Juvix/Syntax/Concrete/Scoped/Utils.hs
index 560c8a6a02..e1a2481726 100644
--- a/src/Juvix/Syntax/Concrete/Scoped/Utils.hs
+++ b/src/Juvix/Syntax/Concrete/Scoped/Utils.hs
@@ -18,8 +18,7 @@ getAllModules' ::
Member (Output (S.NameId, Module 'Scoped 'ModuleTop)) r =>
Module 'Scoped 'ModuleTop ->
Sem r ()
-getAllModules' m = do
- recordModule m
+getAllModules' m = recordModule m
where
recordModule :: Module 'Scoped 'ModuleTop -> Sem r ()
recordModule n = do
diff --git a/src/Juvix/Syntax/MonoJuvix/Pretty/Base.hs b/src/Juvix/Syntax/MonoJuvix/Pretty/Base.hs
index 5d30dcd55b..9f4e22c97d 100644
--- a/src/Juvix/Syntax/MonoJuvix/Pretty/Base.hs
+++ b/src/Juvix/Syntax/MonoJuvix/Pretty/Base.hs
@@ -39,10 +39,10 @@ instance PrettyCode Name where
if
| showNameId -> Just . ("@" <>) <$> ppCode (n ^. nameId)
| otherwise -> return Nothing
- return
- $ annotate (AnnKind (n ^. nameKind))
- $ pretty (n ^. nameText)
- uid
+ return $
+ annotate (AnnKind (n ^. nameKind)) $
+ pretty (n ^. nameText)
+ <>? uid
instance PrettyCode Iden where
ppCode :: Member (Reader Options) r => Iden -> Sem r (Doc Ann)
diff --git a/src/Juvix/Translation/ScopedToAbstract.hs b/src/Juvix/Translation/ScopedToAbstract.hs
index 2d3b086f6d..2a6ed7a77b 100644
--- a/src/Juvix/Translation/ScopedToAbstract.hs
+++ b/src/Juvix/Translation/ScopedToAbstract.hs
@@ -65,7 +65,7 @@ goModule m = case sing :: SModuleIsTop t of
SModuleLocal -> goModule' m
where
goModule' :: Module 'Scoped t -> Sem r Abstract.Module
- goModule' (Module n par b) = case par of
+ goModule' (Module n par _ b) = case par of
[] -> Abstract.Module modName <$> goModuleBody b
_ -> unsupported "Module parameters"
where
@@ -265,7 +265,7 @@ goConstructorDef ::
Member (Error ScoperError) r =>
InductiveConstructorDef 'Scoped ->
Sem r Abstract.InductiveConstructorDef
-goConstructorDef (InductiveConstructorDef c ty) =
+goConstructorDef (InductiveConstructorDef c _ ty) =
Abstract.InductiveConstructorDef (goSymbol c) <$> goExpression ty
goExpression ::
diff --git a/tests/positive/Judoc.juvix b/tests/positive/Judoc.juvix
new file mode 100644
index 0000000000..1b7924f87f
--- /dev/null
+++ b/tests/positive/Judoc.juvix
@@ -0,0 +1,21 @@
+module Judoc;
+
+axiom A : Type;
+axiom b : Type;
+
+inductive T {
+
+};
+
+--- he ;id A; and ;A A id T A id; this is another ;id id id; example
+--- hahahah
+--- and another one ;T;
+id : {A : Type} → A → A;
+id a ≔ a;
+
+--- hellowww
+id2 : {A : Type} → A → A;
+id2 a ≔ a;
+
+
+end;