diff options
Diffstat (limited to 'source/Felix/Render/Html.hs')
| -rw-r--r-- | source/Felix/Render/Html.hs | 3964 |
1 files changed, 3964 insertions, 0 deletions
diff --git a/source/Felix/Render/Html.hs b/source/Felix/Render/Html.hs new file mode 100644 index 0000000..7081e52 --- /dev/null +++ b/source/Felix/Render/Html.hs @@ -0,0 +1,3964 @@ +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} + +module Felix.Render.Html + ( HtmlRenderIndex + , HtmlPagePresentation + , buildRenderIndex + , htmlPagePresentationSource + , renderDocument + , supportScriptAssetContents + ) where + +import Felix.Syntax.Abstract + +import Base +import Felix.Source (ResolvedSource) +import Lucid hiding (Term, for_) +import Lucid.Base (makeAttributes) +import Lucid.Math +import Felix.Render.Html.Context + ( HtmlRenderContext + , HtmlRenderContextError + , htmlCurrentPageLabel + , htmlCurrentSource + , htmlSourceFragmentHref + , htmlSourceLabel + , htmlSourcePageHref + , htmlSupportScriptHref + ) +import Felix.Render.Html.Layout (renderUrlFragment) +import Felix.Report.Location (Location, pattern Nowhere) +import Felix.Syntax.Token (VariableDisplay(..), VariableSuffix(..), displayVariable, tokToText) + +import Control.Monad (unless, when) +import Data.Char (digitToInt, isAlphaNum, isDigit, isSpace, toUpper) +import Data.List qualified as List +import Data.List.NonEmpty qualified as NonEmpty +import Data.Map.Strict qualified as Map +import Data.Set qualified as Set +import Data.Text qualified as Text +import Data.Text.Lazy qualified as LazyText + + + +data HintCategory + = OperatorHint + | RelationHint + | PredicateHint + | StructOpHint + deriving (Show, Eq, Ord) + +data TemplatePiece + = Literal Text + | Slot Int + deriving (Show, Eq, Ord) + +data RenderHint = RenderHint + { renderHintArity :: Int + , renderHintTemplate :: [TemplatePiece] + } deriving (Show, Eq, Ord) + +type HintMap = Map (HintCategory, Marker, Int) RenderHint +type AnchorMap = Map Marker Text +type BlockRenderInfo = (Int, Block, Text) +type PreviewMap = Map Marker PreviewEntry + +data HtmlRenderIndex = HtmlRenderIndex + !(Map Marker IndexedReferenceTarget) + +data HtmlPagePresentation = HtmlPagePresentation + { htmlPagePresentationSource :: !ResolvedSource + , pagePresentationBlockInfos :: ![BlockRenderInfo] + , pagePresentationAnchors :: !AnchorMap + , pagePresentationReferencedMarkers :: !(Set Marker) + } + +data IndexedReferenceTarget = IndexedReferenceTarget + !Int + !ResolvedSource + !ReferenceTarget + +data ReferenceContext = ReferenceContext + { referenceAnchors :: AnchorMap + , referencePreviews :: PreviewMap + } + +data PreviewEntry = PreviewEntry + { previewMarker :: Marker + , previewKind :: Text + , previewTitle :: Maybe Text + , previewSourceLabel :: Text + , previewSourceHref :: Text + , previewReferenceHref :: Text + , previewId :: Text + , previewBody :: HintMap -> Html () + } + +data ReferenceTarget = ReferenceTarget + { targetMarker :: Marker + , targetAnchorId :: Text + , targetKind :: Text + , targetTitle :: Maybe Text + , targetBody :: HintMap -> Html () + } + +data StmtMathFragment + = StmtMathProse Text + | StmtMathNode (Html ()) + +type StmtMathFragments = [StmtMathFragment] + +newtype MissingHintMap = MissingHintMap + { unMissingHintMap :: Map HintCategory (Set Marker) + } deriving (Show, Eq) + +instance Semigroup MissingHintMap where + MissingHintMap left <> MissingHintMap right = + MissingHintMap (Map.unionWith (<>) left right) + +instance Monoid MissingHintMap where + mempty = MissingHintMap mempty + +proofCollapseThreshold :: Int +proofCollapseThreshold = 10 + +referenceGroupThreshold :: Int +referenceGroupThreshold = 5 + + +renderDocument + :: HtmlRenderContext + -> Text + -> HtmlRenderIndex + -> HtmlPagePresentation + -> Either HtmlRenderContextError Text +renderDocument + context + hintsSource + renderIndex + HtmlPagePresentation + { pagePresentationBlockInfos = blockInfos + , pagePresentationAnchors = anchors + , pagePresentationReferencedMarkers = referencedMarkers + } = do + previews <- + buildPreviewMap + context + referencedMarkers + anchors + renderIndex + let result = + case formatMissingHintWarning missingHints of + Nothing -> rendered + Just warningText -> + trace (Text.unpack warningText) rendered + hints = parseHints hintsSource + missingHints = + collectMissingHints + hints + [ block + | (_index, block, _blockId) <- blockInfos + ] + rendered = LazyText.toStrict (renderText (renderPage hints)) + pageLabel = htmlCurrentPageLabel context + tocBlocks = [(index, blockId, block) | (index, block, blockId) <- blockInfos, includeInToc block] + referenceContext = ReferenceContext anchors previews + + renderPage :: HintMap -> Html () + renderPage hintMap = doctypehtml_ do + head_ do + meta_ [charset_ "utf-8"] + title_ (toHtml pageLabel) + style_ pageStyles + body_ do + div_ [class_ "page-layout"] do + aside_ [class_ "toc-column"] do + nav_ [class_ "toc"] do + h2_ [class_ "toc-heading"] "Contents" + input_ + [ class_ "toc-filter" + , type_ "search" + , placeholder_ "Filter labels" + , makeAttributes "aria-label" "Filter TOC by label" + ] + ol_ [class_ "toc-list"] do + traverse_ renderTocEntry tocBlocks + main_ do + h1_ (toHtml pageLabel) + traverse_ (renderBlock hintMap referenceContext) blockInfos + renderPreviewStore hintMap previews + div_ + [ id_ "reference-preview-popup" + , class_ "reference-preview-popup" + , makeAttributes "role" "tooltip" + , makeAttributes "aria-hidden" "true" + ] + skip + script_ + [src_ (htmlSupportScriptHref context)] + ("" :: Text) + Right result + +-- | Index every block target and every page's referenced markers once in +-- deterministic source order. Rendering a page subsequently performs only +-- marker lookups in the shared index. +buildRenderIndex + :: NonEmpty (ResolvedSource, [Block]) + -> (HtmlRenderIndex, NonEmpty HtmlPagePresentation) +buildRenderIndex sourceBlocks = + ( HtmlRenderIndex + (Map.fromList + [ ( targetMarker target + , IndexedReferenceTarget ordinal source target + ) + | (ordinal, (source, target)) <- + zip [1 :: Int ..] orderedTargets + ]) + , pages + ) + where + analysedPages = + uncurry analysePage <$> sourceBlocks + pages = + fst <$> analysedPages + orderedTargets = + [ (htmlPagePresentationSource page, target) + | (page, targets) <- NonEmpty.toList analysedPages + , target <- targets + ] + + analysePage source blocks = + ( HtmlPagePresentation + { htmlPagePresentationSource = source + , pagePresentationBlockInfos = blockInfos + , pagePresentationAnchors = + Map.fromList + [ (targetMarker, targetAnchorId) + | ReferenceTarget + { targetMarker + , targetAnchorId + } <- targets + ] + , pagePresentationReferencedMarkers = + foldMap + (\(_blockInfo, _targets, references) -> references) + analysedBlocks + } + , targets + ) + where + analysedBlocks = + [ ( blockInfo + , referenceTargetsOfBlockRenderInfo blockInfo + , collectReferencedMarkersOfBlock block + ) + | (index, block) <- zip [1 :: Int ..] blocks + , let blockInfo = + (index, block, blockAnchorId index block) + ] + blockInfos = + [ blockInfo + | (blockInfo, _targets, _references) <- analysedBlocks + ] + targets = + concat + [ blockTargets + | (_blockInfo, blockTargets, _references) <- analysedBlocks + ] + + +pageStyles :: Text +pageStyles = Text.unlines + [ ":root {" + , " color-scheme: light dark;" + , " font-family: Georgia, \"Times New Roman\", serif;" + , " --page-bg: #ffffff;" + , " --page-fg: #111111;" + , " --muted-fg: #666666;" + , " --subtle-fg: #444444;" + , " --badge-bg: #f1f1f1;" + , " --badge-border: #dddddd;" + , " --badge-fg: #555555;" + , " --rule-color: #d9d2c2;" + , " --error-fg: #9f1d1d;" + , " --error-bg: #fff1f1;" + , " --toc-active-bg: #f3efe6;" + , " --toc-active-fg: #1b1b1b;" + , " --toc-active-accent: #b9aa7a;" + , " --preview-bg: #fffdf8;" + , " --preview-border: #cfc3a3;" + , " --preview-shadow: rgba(0, 0, 0, 0.18);" + , "}" + , "html {" + , " height: 100%;" + , "}" + , "body {" + , " margin: 0;" + , " height: 100vh;" + , " overflow: hidden;" + , " line-height: 1.5;" + , " background: var(--page-bg);" + , " color: var(--page-fg);" + , "}" + , ".page-layout {" + , " display: grid;" + , " grid-template-columns: minmax(16rem, 24rem) minmax(0, 1fr);" + , " grid-template-rows: minmax(0, 1fr);" + , " gap: 2rem;" + , " align-items: stretch;" + , " box-sizing: border-box;" + , " margin: 0 auto;" + , " max-width: 84rem;" + , " height: 100vh;" + , " padding: 2rem 1.25rem 3rem;" + , "}" + , ".toc-column {" + , " display: block;" + , " min-height: 0;" + , "}" + , ".toc {" + , " display: flex;" + , " flex-direction: column;" + , " height: 100%;" + , " min-height: 0;" + , "}" + , ".toc-heading {" + , " margin: 0 0 0.75rem;" + , " color: var(--muted-fg);" + , " font-size: 0.9rem;" + , " letter-spacing: 0.04em;" + , " text-transform: uppercase;" + , "}" + , ".toc-filter {" + , " box-sizing: border-box;" + , " width: 100%;" + , " margin: 0 0 0.9rem;" + , " padding: 0.45rem 0.55rem;" + , " border: 1px solid var(--badge-border);" + , " border-radius: 0.35rem;" + , " background: var(--page-bg);" + , " color: var(--page-fg);" + , " font: inherit;" + , "}" + , ".toc-filter::placeholder {" + , " color: var(--muted-fg);" + , "}" + , ".toc-list {" + , " flex: 1 1 auto;" + , " min-height: 0;" + , " overflow-y: auto;" + , " list-style: none;" + , " margin: 0;" + , " padding: 0 0.5rem 0 0;" + , "}" + , ".toc-list > li {" + , " margin: 0 0 0.8rem;" + , "}" + , ".toc-list > li > a {" + , " display: block;" + , " margin: -0.15rem -0.35rem;" + , " padding: 0.15rem 0.35rem;" + , " border-radius: 0.35rem;" + , " color: inherit;" + , " text-decoration: none;" + , " transition: background-color 120ms ease, box-shadow 120ms ease, color 120ms ease;" + , "}" + , ".toc-list > li > a:hover," + , ".toc-list > li > a:focus-visible {" + , " text-decoration: underline;" + , "}" + , ".toc-list > li > a.is-active {" + , " background: var(--toc-active-bg);" + , " box-shadow: inset 0.2rem 0 0 var(--toc-active-accent);" + , " color: var(--toc-active-fg);" + , "}" + , ".toc-list > li > a.is-active > code {" + , " color: var(--toc-active-fg);" + , "}" + , ".toc-list > li > a > span:first-child {" + , " display: block;" + , " font-weight: 700;" + , "}" + , ".toc-list > li > a > code {" + , " display: block;" + , " margin-top: 0.15rem;" + , " color: var(--muted-fg);" + , " font-size: 0.9em;" + , " overflow-wrap: anywhere;" + , "}" + , "main {" + , " min-width: 0;" + , " min-height: 0;" + , " overflow-y: auto;" + , "}" + , "main > *[id] {" + , " display: block;" + , " margin: 0 0 1rem;" + , " scroll-margin-top: 1rem;" + , "}" + , "head- {" + , " font-weight: 700;" + , "}" + , "title- {" + , " font-weight: 400;" + , "}" + , "id-," + , "main a[href^=\"#\"]," + , ".ref-badge {" + , " display: inline-block;" + , " padding: 0.02rem 0.35rem;" + , " border: 1px solid var(--badge-border);" + , " border-radius: 0.2rem;" + , " background: var(--badge-bg);" + , " color: var(--badge-fg);" + , " font-family: \"SFMono-Regular\", Menlo, Consolas, \"Liberation Mono\", monospace;" + , " font-size: 0.82em;" + , " text-decoration: none;" + , "}" + , "head- > id- {" + , " margin-left: 0.45rem;" + , "}" + , "main a[href^=\"#\"]:hover," + , "main a[href^=\"#\"]:focus-visible," + , ".ref-badge.has-preview:hover," + , ".ref-badge.has-preview:focus-visible {" + , " text-decoration: underline;" + , "}" + , ".ref-badge.has-preview {" + , " cursor: help;" + , "}" + , ".ref-badge-group {" + , " user-select: none;" + , "}" + , "proof- > p:first-child," + , "proof- > details > summary + p {" + , " display: inline;" + , " margin: 0;" + , "}" + , "proof- proof- {" + , " display: block;" + , " margin: 0.5rem 0 0.5rem 1rem;" + , " padding-left: 0.75rem;" + , " border-left: 1px solid var(--rule-color);" + , "}" + , "proof- > details {" + , " margin: 0;" + , "}" + , "proof- > details > summary {" + , " cursor: pointer;" + , " font-weight: 700;" + , "}" + , "proof- > details > summary title- {" + , " font-weight: 400;" + , "}" + , "proof- > details > :not(summary) {" + , " margin-top: 0.5rem;" + , "}" + , "inductive- > details {" + , " margin-top: 0.75rem;" + , "}" + , "inductive- > details > summary {" + , " cursor: pointer;" + , " font-weight: 700;" + , "}" + , "inductive- > details > :not(summary) {" + , " margin-top: 0.5rem;" + , "}" + , ".inductive-derived-facts > li {" + , " margin: 0.35rem 0;" + , "}" + , ".inductive-derived-facts {" + , " margin: 0;" + , " padding-left: 1.5rem;" + , "}" + , ".reference-preview-store {" + , " display: none;" + , "}" + , ".reference-preview-popup {" + , " position: fixed;" + , " z-index: 1000;" + , " box-sizing: border-box;" + , " width: 44rem;" + , " max-width: calc(100vw - 2rem);" + , " max-height: 34rem;" + , " max-height: min(34rem, calc(100vh - 2rem));" + , " overflow: auto;" + , " overscroll-behavior: contain;" + , " padding: 0.75rem 0.9rem;" + , " border: 1px solid var(--preview-border);" + , " border-radius: 0.45rem;" + , " background: var(--preview-bg);" + , " color: var(--page-fg);" + , " box-shadow: 0 0.75rem 2.25rem var(--preview-shadow);" + , " opacity: 0;" + , " pointer-events: none;" + , " transform: translateY(0.2rem);" + , " transition: opacity 90ms ease, transform 90ms ease;" + , "}" + , ".reference-preview-popup[aria-hidden=\"true\"] {" + , " visibility: hidden;" + , "}" + , ".reference-preview-popup.is-visible {" + , " opacity: 1;" + , " pointer-events: auto;" + , " transform: translateY(0);" + , "}" + , ".reference-preview-popup * {" + , " box-sizing: border-box;" + , "}" + , ".reference-preview-template {" + , " display: flex;" + , " flex-direction: column;" + , " gap: 0.45rem;" + , " width: 100%;" + , "}" + , ".reference-preview-heading {" + , " display: block;" + , " margin: 0;" + , " width: 100%;" + , " color: var(--muted-fg);" + , " font-size: 0.82rem;" + , " letter-spacing: 0.035em;" + , " text-transform: uppercase;" + , "}" + , ".reference-preview-heading code {" + , " color: var(--page-fg);" + , " font-family: \"SFMono-Regular\", Menlo, Consolas, \"Liberation Mono\", monospace;" + , " letter-spacing: 0;" + , " text-transform: none;" + , "}" + , ".reference-preview-heading a {" + , " color: inherit;" + , " text-decoration: none;" + , "}" + , ".reference-preview-heading a:hover," + , ".reference-preview-heading a:focus-visible {" + , " text-decoration: underline;" + , "}" + , ".reference-preview-source {" + , " display: block;" + , " margin: 0;" + , " color: var(--subtle-fg);" + , " font-size: 0.78rem;" + , " letter-spacing: 0;" + , " text-transform: none;" + , "}" + , ".reference-preview-body {" + , " display: block;" + , " clear: both;" + , " margin: 0;" + , " width: 100%;" + , "}" + , ".reference-preview-body p {" + , " margin: 0.35rem 0 0;" + , "}" + , ".reference-preview-body p:first-child {" + , " margin-top: 0;" + , "}" + , ".reference-preview-group-template {" + , " display: flex;" + , " flex-direction: column;" + , " gap: 1rem;" + , " margin: 0;" + , " width: 100%;" + , "}" + , ".reference-preview-group-template > .reference-preview-template + .reference-preview-template {" + , " padding-top: 1rem;" + , " border-top: 1px solid var(--badge-border);" + , "}" + , ".reference-preview-statement {" + , " display: block;" + , " width: 100%;" + , " white-space: normal;" + , " overflow-wrap: break-word;" + , "}" + , ".reference-preview-statement math {" + , " max-width: 100%;" + , " overflow-x: auto;" + , " overflow-y: hidden;" + , " vertical-align: middle;" + , "}" + , "math[display=\"block\"] {" + , " display: block;" + , " margin: 0.5rem 0;" + , "}" + , "merror {" + , " color: var(--error-fg);" + , " background: var(--error-bg);" + , "}" + , "@media (prefers-color-scheme: dark) {" + , " :root {" + , " --page-bg: #161616;" + , " --page-fg: #e9e6df;" + , " --muted-fg: #b7b0a4;" + , " --subtle-fg: #cfc8bc;" + , " --badge-bg: #2a2a2a;" + , " --badge-border: #444444;" + , " --badge-fg: #d8d3ca;" + , " --rule-color: #5b5348;" + , " --error-fg: #ffb0b0;" + , " --error-bg: #3b1f1f;" + , " --toc-active-bg: #2b271f;" + , " --toc-active-fg: #f0ebe1;" + , " --toc-active-accent: #99865a;" + , " --preview-bg: #211f1a;" + , " --preview-border: #776a50;" + , " --preview-shadow: rgba(0, 0, 0, 0.55);" + , " }" + , "}" + , "@media (max-width: 900px) {" + , " body {" + , " height: auto;" + , " overflow: auto;" + , " }" + , " .page-layout {" + , " grid-template-columns: 1fr;" + , " grid-template-rows: auto;" + , " gap: 1.5rem;" + , " height: auto;" + , " }" + , " .toc-column {" + , " display: none;" + , " }" + , " main {" + , " min-height: auto;" + , " overflow: visible;" + , " }" + , "}" + ] + +supportScriptAssetContents :: Text +supportScriptAssetContents = tocScript <> "\n" <> referencePreviewScript + + +tocScript :: Text +tocScript = Text.unlines + [ "(function () {" + , " const toc = document.querySelector('.toc');" + , " const tocList = toc ? toc.querySelector('.toc-list') : null;" + , " const filterInput = toc ? toc.querySelector('.toc-filter') : null;" + , " const content = document.querySelector('main');" + , " if (!toc || !tocList || !content) return;" + , " const links = Array.from(tocList.querySelectorAll(':scope > li > a[href^=\"#\"]'));" + , " const blocks = Array.from(content.querySelectorAll(':scope > *[id]'));" + , " if (!links.length || !blocks.length) return;" + , " const linkByTarget = new Map(links.map((link) => [decodeURIComponent(link.hash.slice(1)), link]));" + , " const tocEntries = links.map((link) => ({" + , " item: link.parentElement," + , " link," + , " label: ((link.querySelector('code') || link.lastElementChild || link).textContent || '').trim().toLowerCase()" + , " }));" + , " let activeTarget = null;" + , " let rafId = 0;" + , " let suspendUntil = 0;" + , "" + , " const keepActiveLinkVisible = (link) => {" + , " if (!link || performance.now() < suspendUntil) return;" + , " const item = link.parentElement;" + , " if (item && item.hidden) return;" + , " const tocRect = tocList.getBoundingClientRect();" + , " const linkRect = link.getBoundingClientRect();" + , " const comfortTop = tocRect.top + tocRect.height * 0.2;" + , " const comfortBottom = tocRect.bottom - tocRect.height * 0.2;" + , " if (linkRect.top < comfortTop || linkRect.bottom > comfortBottom) {" + , " link.scrollIntoView({ block: 'nearest', inline: 'nearest' });" + , " }" + , " };" + , "" + , " const applyFilter = () => {" + , " const query = filterInput ? filterInput.value.trim().toLowerCase() : '';" + , " for (const { item, label } of tocEntries) {" + , " if (!item) continue;" + , " item.hidden = query !== '' && !label.includes(query);" + , " }" + , " if (activeTarget) {" + , " keepActiveLinkVisible(linkByTarget.get(activeTarget));" + , " }" + , " };" + , "" + , " const setActiveTarget = (target) => {" + , " if (!target || target === activeTarget) return;" + , " const previous = activeTarget ? linkByTarget.get(activeTarget) : null;" + , " if (previous) {" + , " previous.classList.remove('is-active');" + , " previous.removeAttribute('aria-current');" + , " }" + , " activeTarget = target;" + , " const next = linkByTarget.get(target);" + , " if (!next) return;" + , " next.classList.add('is-active');" + , " next.setAttribute('aria-current', 'location');" + , " keepActiveLinkVisible(next);" + , " };" + , "" + , " const firstTarget = blocks[0].id;" + , "" + , " const findActiveTarget = () => {" + , " const contentRect = content.getBoundingClientRect();" + , " const topSnapThreshold = 40;" + , " for (const block of blocks) {" + , " const target = block.id;" + , " const rect = block.getBoundingClientRect();" + , " if (rect.top >= contentRect.top - 4 && rect.top <= contentRect.top + topSnapThreshold) {" + , " return target;" + , " }" + , " }" + , " const activationLine = contentRect.top + contentRect.height * 0.22;" + , " let candidate = firstTarget;" + , " for (const block of blocks) {" + , " const target = block.id;" + , " if (block.getBoundingClientRect().top <= activationLine) {" + , " candidate = target;" + , " continue;" + , " }" + , " break;" + , " }" + , " return candidate;" + , " };" + , "" + , " const scheduleUpdate = () => {" + , " if (rafId) return;" + , " rafId = window.requestAnimationFrame(() => {" + , " rafId = 0;" + , " setActiveTarget(findActiveTarget());" + , " });" + , " };" + , "" + , " const suspendAutofollow = () => {" + , " suspendUntil = performance.now() + 1500;" + , " };" + , "" + , " const revealTarget = (target) => {" + , " let parent = target.parentElement;" + , " while (parent) {" + , " if (parent.localName === 'details') {" + , " parent.open = true;" + , " }" + , " parent = parent.parentElement;" + , " }" + , " };" + , "" + , " const scrollToTarget = (targetId) => {" + , " const target = document.getElementById(targetId);" + , " if (!target || !content.contains(target)) return false;" + , " revealTarget(target);" + , " target.scrollIntoView({ block: 'start', inline: 'nearest' });" + , " setActiveTarget(targetId);" + , " return true;" + , " };" + , "" + , " content.addEventListener('scroll', scheduleUpdate, { passive: true });" + , " window.addEventListener('resize', scheduleUpdate);" + , " tocList.addEventListener('wheel', suspendAutofollow, { passive: true });" + , " tocList.addEventListener('touchstart', suspendAutofollow, { passive: true });" + , " toc.addEventListener('pointerdown', suspendAutofollow);" + , " toc.addEventListener('focusin', suspendAutofollow);" + , " if (filterInput) {" + , " filterInput.addEventListener('input', applyFilter);" + , " }" + , " for (const details of content.querySelectorAll('details')) {" + , " details.addEventListener('toggle', scheduleUpdate);" + , " }" + , "" + , " toc.addEventListener('click', (event) => {" + , " const link = event.target.closest('a[href^=\"#\"]');" + , " if (!link || !tocList.contains(link)) return;" + , " const targetId = decodeURIComponent(link.hash.slice(1));" + , " if (!scrollToTarget(targetId)) return;" + , " event.preventDefault();" + , " suspendUntil = 0;" + , " if (location.hash !== '#' + targetId) {" + , " try {" + , " history.pushState(null, '', '#' + targetId);" + , " } catch (_error) {" + , " location.hash = targetId;" + , " }" + , " }" + , " });" + , "" + , " window.addEventListener('hashchange', () => {" + , " if (location.hash.length <= 1) return;" + , " const hashTarget = decodeURIComponent(location.hash.slice(1));" + , " if (!scrollToTarget(hashTarget)) scheduleUpdate();" + , " });" + , "" + , " if (location.hash.length > 1) {" + , " const hashTarget = decodeURIComponent(location.hash.slice(1));" + , " window.requestAnimationFrame(() => {" + , " applyFilter();" + , " if (!scrollToTarget(hashTarget)) scheduleUpdate();" + , " });" + , " return;" + , " }" + , "" + , " applyFilter();" + , " scheduleUpdate();" + , "})();" + ] + +referencePreviewScript :: Text +referencePreviewScript = Text.unlines + [ "(function () {" + , " const content = document.querySelector('main');" + , " const popup = document.getElementById('reference-preview-popup');" + , " if (!content || !popup) return;" + , " let activeTrigger = null;" + , " let lastPointer = null;" + , " let isPinned = false;" + , " let hideTimer = 0;" + , " const offset = 14;" + , " const margin = 12;" + , " const hideDelay = 180;" + , "" + , " const cloneHiddenPreview = (trigger) => {" + , " const previewId = trigger.getAttribute('data-preview-id');" + , " const template = previewId ? document.getElementById(previewId) : null;" + , " if (!template) return null;" + , " const clone = template.cloneNode(true);" + , " clone.removeAttribute('id');" + , " return clone;" + , " };" + , "" + , " const buildCurrentPreview = (trigger) => {" + , " const targetId = trigger.getAttribute('data-preview-target-id');" + , " const target = targetId ? document.getElementById(targetId) : null;" + , " if (!target || !content.contains(target)) return null;" + , " const template = document.createElement('div');" + , " template.className = 'reference-preview-template';" + , " const heading = document.createElement('div');" + , " heading.className = 'reference-preview-heading';" + , " const kind = target.getAttribute('data-preview-kind') || 'Reference';" + , " const label = target.getAttribute('data-preview-label') || targetId;" + , " const title = target.getAttribute('data-preview-title');" + , " heading.append(document.createTextNode(kind + ' '));" + , " const code = document.createElement('code');" + , " code.textContent = label;" + , " heading.append(code);" + , " if (title) {" + , " heading.append(document.createTextNode(' (' + title + ')'));" + , " }" + , " template.append(heading);" + , " const body = document.createElement('div');" + , " body.className = 'reference-preview-body';" + , " const statement = document.createElement('div');" + , " statement.className = 'reference-preview-statement';" + , " const head = Array.from(target.children).find((child) => child.localName === 'head-');" + , " const nodes = Array.from(target.childNodes);" + , " const start = head ? nodes.indexOf(head) + 1 : 0;" + , " for (const node of nodes.slice(start)) {" + , " statement.append(node.cloneNode(true));" + , " }" + , " if (!statement.childNodes.length) return null;" + , " body.append(statement);" + , " template.append(body);" + , " return template;" + , " };" + , "" + , " const buildMissingPreview = (item) => {" + , " const label = item.getAttribute('data-reference-label') || '';" + , " const template = document.createElement('div');" + , " template.className = 'reference-preview-template';" + , " const heading = document.createElement('div');" + , " heading.className = 'reference-preview-heading';" + , " heading.append(document.createTextNode('Reference '));" + , " const code = document.createElement('code');" + , " code.textContent = label;" + , " heading.append(code);" + , " template.append(heading);" + , " const body = document.createElement('div');" + , " body.className = 'reference-preview-body';" + , " const statement = document.createElement('p');" + , " statement.className = 'reference-preview-statement';" + , " statement.textContent = 'Preview unavailable.';" + , " body.append(statement);" + , " template.append(body);" + , " return template;" + , " };" + , "" + , " const linkGroupHeading = (item, template) => {" + , " const href = item.getAttribute('data-preview-link');" + , " if (!href) return template;" + , " const heading = template.querySelector('.reference-preview-heading');" + , " const code = heading ? heading.querySelector('code') : null;" + , " if (!heading || !code || code.closest('a')) return template;" + , " const link = document.createElement('a');" + , " link.href = href;" + , " link.append(code.cloneNode(true));" + , " code.replaceWith(link);" + , " return template;" + , " };" + , "" + , " const buildGroupPreview = (trigger) => {" + , " if (!trigger.hasAttribute('data-preview-group')) return null;" + , " const items = Array.from(trigger.querySelectorAll('.reference-preview-group-items > [data-reference-label]'));" + , " if (!items.length) return null;" + , " const template = document.createElement('div');" + , " template.className = 'reference-preview-group-template';" + , " for (const item of items) {" + , " const preview = cloneHiddenPreview(item) || buildCurrentPreview(item) || buildMissingPreview(item);" + , " template.append(linkGroupHeading(item, preview));" + , " }" + , " return template;" + , " };" + , "" + , " const previewFor = (trigger) => buildGroupPreview(trigger) || cloneHiddenPreview(trigger) || buildCurrentPreview(trigger);" + , "" + , " const clamp = (value, min, max) => Math.min(Math.max(value, min), max);" + , " const findTrigger = (target) => target instanceof Element ? target.closest('[data-preview-group], [data-preview-id], [data-preview-target-id]') : null;" + , " const clearHideTimer = () => {" + , " if (!hideTimer) return;" + , " window.clearTimeout(hideTimer);" + , " hideTimer = 0;" + , " };" + , "" + , " const hidePreview = () => {" + , " clearHideTimer();" + , " activeTrigger = null;" + , " lastPointer = null;" + , " isPinned = false;" + , " popup.classList.remove('is-visible');" + , " popup.setAttribute('aria-hidden', 'true');" + , " popup.replaceChildren();" + , " };" + , "" + , " const scheduleHide = () => {" + , " if (isPinned) return;" + , " clearHideTimer();" + , " hideTimer = window.setTimeout(() => {" + , " hideTimer = 0;" + , " if (!isPinned) hidePreview();" + , " }, hideDelay);" + , " };" + , "" + , " const placePreview = () => {" + , " if (!activeTrigger) return;" + , " const triggerRect = activeTrigger.getBoundingClientRect();" + , " const popupRect = popup.getBoundingClientRect();" + , " const fallbackWidth = Math.min(704, Math.max(0, window.innerWidth - margin * 2));" + , " const popupWidth = popupRect.width || fallbackWidth;" + , " const popupHeight = popupRect.height || 0;" + , " const pointer = lastPointer;" + , " const anchorX = pointer ? pointer.clientX : triggerRect.left;" + , " const anchorY = pointer ? pointer.clientY : triggerRect.bottom;" + , " let left = anchorX + (pointer ? offset : 0);" + , " let top = anchorY + offset;" + , " if (top + popupHeight + margin > window.innerHeight) {" + , " const upperAnchor = pointer ? pointer.clientY : triggerRect.top;" + , " top = Math.max(margin, upperAnchor - popupHeight - offset);" + , " }" + , " left = clamp(left, margin, Math.max(margin, window.innerWidth - popupWidth - margin));" + , " popup.style.left = `${left}px`;" + , " popup.style.top = `${top}px`;" + , " };" + , "" + , " const showPreview = (trigger, pointerEvent, pinned = false) => {" + , " const source = previewFor(trigger);" + , " if (!source) {" + , " hidePreview();" + , " return;" + , " }" + , " const wasPinned = isPinned && trigger === activeTrigger;" + , " clearHideTimer();" + , " activeTrigger = trigger;" + , " lastPointer = pointerEvent ? { clientX: pointerEvent.clientX, clientY: pointerEvent.clientY } : null;" + , " isPinned = pinned || wasPinned;" + , " popup.replaceChildren(source);" + , " popup.scrollTop = 0;" + , " popup.setAttribute('aria-hidden', 'false');" + , " popup.classList.add('is-visible');" + , " placePreview();" + , " };" + , "" + , " content.addEventListener('pointerover', (event) => {" + , " const trigger = findTrigger(event.target);" + , " if (!trigger || !content.contains(trigger) || trigger === activeTrigger) return;" + , " showPreview(trigger, event);" + , " });" + , "" + , " content.addEventListener('pointermove', (event) => {" + , " const trigger = findTrigger(event.target);" + , " if (!trigger || trigger !== activeTrigger) return;" + , " if (isPinned) return;" + , " lastPointer = { clientX: event.clientX, clientY: event.clientY };" + , " placePreview();" + , " });" + , "" + , " content.addEventListener('pointerout', (event) => {" + , " const trigger = findTrigger(event.target);" + , " if (!trigger || trigger !== activeTrigger) return;" + , " if (isPinned) return;" + , " const related = event.relatedTarget;" + , " if (related instanceof Node && trigger.contains(related)) return;" + , " if (related instanceof Node && popup.contains(related)) return;" + , " scheduleHide();" + , " });" + , "" + , " content.addEventListener('focusin', (event) => {" + , " const trigger = findTrigger(event.target);" + , " if (!trigger || !content.contains(trigger)) return;" + , " showPreview(trigger, null);" + , " });" + , "" + , " content.addEventListener('focusout', (event) => {" + , " const trigger = findTrigger(event.target);" + , " if (trigger && trigger === activeTrigger && !isPinned) scheduleHide();" + , " });" + , "" + , " content.addEventListener('click', (event) => {" + , " const trigger = findTrigger(event.target);" + , " if (!trigger || !trigger.hasAttribute('data-preview-group') || !content.contains(trigger)) return;" + , " event.preventDefault();" + , " showPreview(trigger, event, true);" + , " });" + , "" + , " popup.addEventListener('pointerenter', clearHideTimer);" + , " popup.addEventListener('pointerleave', scheduleHide);" + , "" + , " document.addEventListener('click', (event) => {" + , " if (!isPinned) return;" + , " const target = event.target;" + , " if (target instanceof Node && popup.contains(target)) return;" + , " if (activeTrigger && target instanceof Node && activeTrigger.contains(target)) return;" + , " hidePreview();" + , " });" + , "" + , " content.addEventListener('scroll', hidePreview, { passive: true });" + , " window.addEventListener('resize', hidePreview);" + , " window.addEventListener('hashchange', hidePreview);" + , " document.addEventListener('keydown', (event) => {" + , " if (event.key === 'Escape') {" + , " hidePreview();" + , " return;" + , " }" + , " if (event.key !== 'Enter' && event.key !== ' ') return;" + , " const trigger = findTrigger(document.activeElement);" + , " if (!trigger || !trigger.hasAttribute('data-preview-group')) return;" + , " event.preventDefault();" + , " showPreview(trigger, null, true);" + , " });" + , "})();" + ] + +collectReferencedMarkersOfBlock :: Block -> Set Marker +collectReferencedMarkersOfBlock = + collectBlock + where + collectBlock :: Block -> Set Marker + collectBlock = \case + BlockProof _start proof _end -> + collectProof proof + _ -> + mempty + + collectProof :: Proof -> Set Marker + collectProof = \case + Omitted _loc -> + mempty + Qed _loc justification -> + collectJustification justification + Contradiction _loc justification -> + collectJustification justification + ByCase _loc cases -> + foldMap collectCase cases + ByContradiction _loc proof -> + collectProof proof + BySetInduction _loc _term proof -> + collectProof proof + ByOrdInduction _loc proof -> + collectProof proof + Assume _loc _stmt proof -> + collectProof proof + FixSymbolic _loc _vars _bound proof -> + collectProof proof + FixSuchThat _loc _vars _stmt proof -> + collectProof proof + Calc _loc _maybeQuant calc proof -> + collectCalc calc <> collectProof proof + TakeVar _loc _vars _bound _stmt justification proof -> + collectJustification justification <> collectProof proof + TakeNoun _loc _np justification proof -> + collectJustification justification <> collectProof proof + Have _loc _maybeStmt _stmt justification proof -> + collectJustification justification <> collectProof proof + Suffices _loc _stmt justification proof -> + collectJustification justification <> collectProof proof + Subclaim _loc _stmt subproof proof -> + collectProof subproof <> collectProof proof + Define _loc _var _expr proof -> + collectProof proof + DefineFunction _loc _fun _arg _value _boundVar _boundExpr proof -> + collectProof proof + DefineFunctionLocal _loc _fun _arg _target _domVar _codVar _rules proof -> + collectProof proof + + collectCase :: Case -> Set Marker + collectCase Case{caseProof} = + collectProof caseProof + + collectCalc :: Calc -> Set Marker + collectCalc = \case + Equation _expr steps -> + foldMap (collectJustification . snd) steps + Biconditionals _formula steps -> + foldMap (collectJustification . snd) steps + + collectJustification :: Justification -> Set Marker + collectJustification = \case + JustificationRef markers -> + Set.fromList (toList markers) + JustificationSetExt -> + mempty + JustificationEmpty -> + mempty + JustificationLocal -> + mempty + +collectMissingHints :: HintMap -> [Block] -> MissingHintMap +collectMissingHints hints = foldMap collectBlock + where + noteMissingHint :: HintCategory -> Marker -> Int -> MissingHintMap + noteMissingHint category marker arity = + if Map.member (category, marker, arity) hints + then mempty + else MissingHintMap (Map.singleton category (Set.singleton marker)) + + collectBlock :: Block -> MissingHintMap + collectBlock = \case + BlockAxiom _loc _title _marker axiom -> + collectAxiom axiom + BlockClaim _kind _loc _title _marker claim -> + collectClaim claim + BlockProof _start proof _end -> + collectProof proof + BlockDefn _loc _title _marker defn -> + collectDefn defn + BlockAbbr _loc _title _marker abbr -> + collectAbbreviation abbr + BlockData _loc _title _marker datatype -> + collectDatatype datatype + BlockInductive _loc _title _marker ind -> + collectInductive ind + BlockSig _loc _title _marker asms sig -> + collectAsms asms + <> collectSignature sig + BlockStruct _loc _title _marker structDefn -> + collectStructDefn structDefn + + collectAxiom :: Axiom -> MissingHintMap + collectAxiom (Axiom asms stmt) = + collectAsms asms <> collectStmt stmt + + collectClaim :: Claim -> MissingHintMap + collectClaim (Claim asms stmt) = + collectAsms asms <> collectStmt stmt + + collectDefn :: Defn -> MissingHintMap + collectDefn = \case + Defn asms defnHead stmt -> + collectAsms asms + <> collectDefnHead defnHead + <> collectStmt stmt + DefnFun asms _fun maybeTerm resultTerm -> + collectAsms asms + <> foldMap collectTerm maybeTerm + <> collectTerm resultTerm + DefnOp symb expr -> + collectSymbolPattern symb + <> collectExpr expr + + collectDefnHead :: DefnHead -> MissingHintMap + collectDefnHead = \case + DefnAdj maybeNp _var _adj -> + foldMap collectNounPhraseMaybe maybeNp + DefnVerb maybeNp _var _verb -> + foldMap collectNounPhraseMaybe maybeNp + DefnNoun _var noun -> + collectVarNoun noun + DefnSymbolicPredicate _predi marker vars -> + noteMissingHint PredicateHint marker (length vars) + <> foldMap (collectExpr . ExprVar) vars + DefnRel _x rel params _y -> + noteMissingHint RelationHint (relationSymbolMarker rel) (length params) + + collectAbbreviation :: Abbreviation -> MissingHintMap + collectAbbreviation = \case + AbbreviationAdj _var _adj stmt -> + collectStmt stmt + AbbreviationVerb _var _verb stmt -> + collectStmt stmt + AbbreviationNoun _var _noun stmt -> + collectStmt stmt + AbbreviationRel _x rel params _y stmt -> + noteMissingHint RelationHint (relationSymbolMarker rel) (length params) + <> collectStmt stmt + AbbreviationFun _fun bodyTerm -> + collectTerm bodyTerm + AbbreviationEq symb expr -> + collectSymbolPattern symb + <> collectExpr expr + + collectDatatype :: Datatype -> MissingHintMap + collectDatatype Datatype{..} = + collectExpr datatypeHeadExpr + <> foldMap collectDatatypeClause datatypeClauses + + collectDatatypeClause :: DatatypeClause -> MissingHintMap + collectDatatypeClause DatatypeClause{..} = + collectExpr datatypeClauseConstructorExpr + <> collectExpr datatypeClauseTargetExpr + <> foldMap (collectExpr . snd) datatypeClausePremises + + collectInductive :: Inductive -> MissingHintMap + collectInductive Inductive{..} = + collectSymbolPattern inductiveSymbolPattern + <> collectExpr inductiveDomain + <> foldMap collectIntroRule inductiveIntros + + collectIntroRule :: IntroRule -> MissingHintMap + collectIntroRule IntroRule{..} = + foldMap collectFormula introConditions + <> collectFormula introResult + + collectSignature :: Signature -> MissingHintMap + collectSignature = \case + SignatureAdj _var adj -> + collectVarAdj adj + SignatureVerb _var verb -> + collectVarVerb verb + SignatureNoun _var noun -> + collectVarNoun noun + SignatureSymbolic symb np -> + collectSymbolPattern symb + <> collectNounPhraseMaybe np + + collectStructDefn :: StructDefn -> MissingHintMap + collectStructDefn StructDefn{structAssumes} = + foldMap (collectStmt . snd) structAssumes + + collectProof :: Proof -> MissingHintMap + collectProof = \case + Omitted _loc -> + mempty + Qed{} -> + mempty + Contradiction{} -> + mempty + ByCase _loc cases -> + foldMap collectCase cases + ByContradiction _loc proof -> + collectProof proof + BySetInduction _loc maybeTerm proof -> + foldMap collectTerm maybeTerm + <> collectProof proof + ByOrdInduction _loc proof -> + collectProof proof + Assume _loc stmt proof -> + collectStmt stmt + <> collectProof proof + FixSymbolic _loc _vars bound proof -> + collectBound bound + <> collectProof proof + FixSuchThat _loc _vars stmt proof -> + collectStmt stmt + <> collectProof proof + Calc _loc maybeQuant calc proof -> + foldMap collectCalcQuantifier maybeQuant + <> collectCalc calc + <> collectProof proof + TakeVar _loc _vars bound stmt _justification proof -> + collectBound bound + <> collectStmt stmt + <> collectProof proof + TakeNoun _loc np _justification proof -> + collectNounPhraseList np + <> collectProof proof + Have _loc maybeStmt stmt _justification proof -> + foldMap collectStmt maybeStmt + <> collectStmt stmt + <> collectProof proof + Suffices _loc stmt _justification proof -> + collectStmt stmt + <> collectProof proof + Subclaim _loc stmt subproof proof -> + collectStmt stmt + <> collectProof subproof + <> collectProof proof + Define _loc _var expr proof -> + collectExpr expr + <> collectProof proof + DefineFunction _loc _fun _arg value _boundVar boundExpr proof -> + collectExpr value + <> collectExpr boundExpr + <> collectProof proof + DefineFunctionLocal _loc _fun _arg _target _domVar _codVar rules proof -> + foldMap collectLocalFunctionRule rules + <> collectProof proof + + collectLocalFunctionRule :: (Expr, Formula) -> MissingHintMap + collectLocalFunctionRule (ruleTerm, formula) = + collectExpr ruleTerm + <> collectFormula formula + + collectCase :: Case -> MissingHintMap + collectCase Case{caseOf, caseProof} = + collectStmt caseOf + <> collectProof caseProof + + collectCalcQuantifier :: CalcQuantifier -> MissingHintMap + collectCalcQuantifier (CalcQuantifier _vars bound maybeStmt) = + collectBound bound + <> foldMap collectStmt maybeStmt + + collectCalc :: Calc -> MissingHintMap + collectCalc = \case + Equation expr steps -> + collectExpr expr + <> foldMap (collectExpr . fst) steps + Biconditionals phi steps -> + collectFormula phi + <> foldMap (collectFormula . fst) steps + + collectStmt :: Stmt -> MissingHintMap + collectStmt = \case + StmtFormula phi -> + collectFormula phi + StmtVerbPhrase terms verbPhrase -> + collectTerms terms + <> collectVerbPhrase verbPhrase + StmtNoun terms np -> + collectTerms terms + <> collectNounPhraseMaybe np + StmtStruct stmtTerm _structPhrase -> + collectTerm stmtTerm + StmtNeg _loc stmt -> + collectStmt stmt + StmtExists _loc np -> + collectNounPhraseList np + StmtConnected _conn _loc stmt1 stmt2 -> + collectStmt stmt1 + <> collectStmt stmt2 + StmtQuantPhrase _loc qp stmt -> + collectQuantPhrase qp + <> collectStmt stmt + SymbolicQuantified _loc _quant _vars bound suchThat stmt -> + collectBound bound + <> foldMap collectStmt suchThat + <> collectStmt stmt + + collectQuantPhrase :: QuantPhrase -> MissingHintMap + collectQuantPhrase (QuantPhrase _quant np) = + collectNounPhraseList np + + collectAsm :: Asm -> MissingHintMap + collectAsm = \case + AsmSuppose stmt -> + collectStmt stmt + AsmLetNoun _vars np -> + collectNounPhraseMaybe np + AsmLetIn _vars expr -> + collectExpr expr + AsmLetThe _var fun -> + collectFun fun + AsmLetEq _var expr -> + collectExpr expr + AsmLetStruct{} -> + mempty + + collectTerm :: Term -> MissingHintMap + collectTerm = \case + TermExpr expr -> + collectExpr expr + TermFun fun -> + collectFun fun + TermIota _loc _var stmt -> + collectStmt stmt + TermQuantified _quant _loc np -> + collectNounPhraseMaybe np + + collectNounPhraseMaybe :: NounPhrase Maybe -> MissingHintMap + collectNounPhraseMaybe (NounPhrase ls noun _maybeName rs maybeSuchThat) = + collectAdjLs ls + <> collectNoun noun + <> collectAdjRs rs + <> foldMap collectStmt maybeSuchThat + + collectNounPhraseList :: NounPhrase [] -> MissingHintMap + collectNounPhraseList (NounPhrase ls noun _names rs maybeSuchThat) = + collectAdjLs ls + <> collectNoun noun + <> collectAdjRs rs + <> foldMap collectStmt maybeSuchThat + + collectAdjL :: AdjLOf Term -> MissingHintMap + collectAdjL (AdjL _loc _item args) = + collectTerms args + + collectAdjR :: AdjROf Term -> MissingHintMap + collectAdjR = \case + AdjR _loc _item args -> + collectTerms args + AttrRThat verbPhrase -> + collectVerbPhrase verbPhrase + + collectAdj :: AdjOf Term -> MissingHintMap + collectAdj (Adj _loc _item args) = + collectTerms args + + collectVarAdj :: AdjOf VarSymbol -> MissingHintMap + collectVarAdj _adj = + mempty + + collectVerb :: VerbOf Term -> MissingHintMap + collectVerb (Verb _loc _item args) = + collectTerms args + + collectVarVerb :: VerbOf VarSymbol -> MissingHintMap + collectVarVerb _verb = + mempty + + collectVerbPhrase :: VerbPhrase -> MissingHintMap + collectVerbPhrase = \case + VPVerb verb -> + collectVerb verb + VPAdj adjs -> + foldMap collectAdj adjs + VPVerbNot verb -> + collectVerb verb + VPAdjNot adjs -> + foldMap collectAdj adjs + + collectNoun :: NounOf Term -> MissingHintMap + collectNoun (Noun _loc _item args) = + collectTerms args + + collectVarNoun :: NounOf VarSymbol -> MissingHintMap + collectVarNoun _noun = + mempty + + collectFun :: FunOf Term -> MissingHintMap + collectFun Fun{funArgs} = + collectTerms funArgs + + collectBound :: Bound -> MissingHintMap + collectBound = \case + Unbounded -> + mempty + Bounded _loc _sign rel expr -> + collectRelation rel + <> collectExpr expr + + collectFormula :: Formula -> MissingHintMap + collectFormula = \case + FormulaChain chain -> + collectChain chain + FormulaPredicate _loc _predi marker exprs -> + noteMissingHint PredicateHint marker (length exprs) + <> collectExprs exprs + Connected _loc _conn phi psi -> + collectFormula phi + <> collectFormula psi + FormulaNeg _loc phi -> + collectFormula phi + FormulaQuantified _loc _quant _vars bound phi -> + collectBound bound + <> collectFormula phi + PropositionalConstant{} -> + mempty + + collectChain :: Chain -> MissingHintMap + collectChain = \case + ChainBase lhs _sign rel rhs -> + collectExprs lhs + <> collectRelation rel + <> collectExprs rhs + ChainCons lhs _sign rel chain -> + collectExprs lhs + <> collectRelation rel + <> collectChain chain + + collectRelation :: Relation -> MissingHintMap + collectRelation = \case + Relation _loc symbol relParams -> + noteMissingHint RelationHint (relationSymbolMarker symbol) (length relParams) + <> collectExprs relParams + RelationExpr _loc expr -> + collectExpr expr + + collectExpr :: Expr -> MissingHintMap + collectExpr = \case + ExprVar{} -> + mempty + ExprInteger{} -> + mempty + ExprOp _loc item args -> + noteMissingHint OperatorHint (mixfixMarker item) (length args) + <> collectExprs args + ExprStructOp _loc symb maybeExpr -> + noteMissingHint StructOpHint (structMarker symb) (length (maybeToList maybeExpr)) + <> foldMap collectExpr maybeExpr + ExprFiniteSet _loc exprs -> + collectExprs exprs + ExprSep _loc _var boundExpr stmt -> + collectExpr boundExpr + <> collectStmt stmt + ExprReplace _loc expr bounds maybeStmt -> + collectExpr expr + <> foldMap (collectExpr . snd) bounds + <> foldMap collectStmt maybeStmt + ExprReplacePred _loc _rangeVar _domVar domExpr stmt -> + collectExpr domExpr + <> collectStmt stmt + + collectSymbolPattern :: SymbolPattern -> MissingHintMap + collectSymbolPattern (SymbolPattern symbol vars) = + noteMissingHint OperatorHint (mixfixMarker symbol) (length vars) + + collectAsms :: [Asm] -> MissingHintMap + collectAsms = + foldMap collectAsm + + collectTerms :: Foldable t => t Term -> MissingHintMap + collectTerms = + foldMap collectTerm + + collectAdjLs :: [AdjLOf Term] -> MissingHintMap + collectAdjLs = + foldMap collectAdjL + + collectAdjRs :: [AdjROf Term] -> MissingHintMap + collectAdjRs = + foldMap collectAdjR + + collectExprs :: Foldable t => t Expr -> MissingHintMap + collectExprs = + foldMap collectExpr + +formatMissingHintWarning :: MissingHintMap -> Maybe Text +formatMissingHintWarning missingHints + | null parts = Nothing + | otherwise = Just ("WARNING: missing render hints: " <> Text.intercalate "; " parts) + where + missingHintMap = unMissingHintMap missingHints + + parts = + [ label <> "(" <> Text.intercalate ", " (markerText <$> Set.toAscList markers) <> ")" + | (category, label) <- categoryLabels + , Just markers <- [Map.lookup category missingHintMap] + , not (Set.null markers) + ] + + categoryLabels :: [(HintCategory, Text)] + categoryLabels = + [ (OperatorHint, "operators") + , (RelationHint, "relations") + , (PredicateHint, "predicates") + , (StructOpHint, "structops") + ] + + +parseHints :: Text -> HintMap +parseHints source = Map.fromList (parseLine <$> zip [1 :: Int ..] relevantLines) + where + relevantLines = [line | line <- Text.lines source, not (Text.all isSpace line)] + + parseLine :: (Int, Text) -> ((HintCategory, Marker, Int), RenderHint) + parseLine (lineNo, line) = case Text.splitOn "\t" line of + [categoryText, markerName, arityText, templateText] -> + let category = parseCategory lineNo categoryText + marker = Marker markerName + arity = parseArity lineNo arityText + template = parseTemplate lineNo templateText + in ((category, marker, arity), RenderHint arity template) + _ -> + error ("Malformed render hint at line " <> show lineNo <> ": expected exactly 4 tab-separated columns") + +parseCategory :: Int -> Text -> HintCategory +parseCategory lineNo = \case + "operator" -> OperatorHint + "relation" -> RelationHint + "predicate" -> PredicateHint + "structop" -> StructOpHint + other -> error ("Unknown render hint category at line " <> show lineNo <> ": " <> Text.unpack other) + +parseArity :: Int -> Text -> Int +parseArity lineNo text = case reads (Text.unpack text) of + [(n, "")] -> n + _ -> error ("Malformed render-hint arity at line " <> show lineNo <> ": " <> Text.unpack text) + +parseTemplate :: Int -> Text -> [TemplatePiece] +parseTemplate lineNo template = reverse (flush mempty (go mempty [] template)) + where + go :: Text -> [TemplatePiece] -> Text -> [TemplatePiece] + go literal acc rest = case parseSlot rest of + Just (slot, rest') -> + go mempty (Slot slot : flush literal acc) rest' + Nothing -> case Text.uncons rest of + Nothing -> flush literal acc + Just (c, rest') -> go (Text.snoc literal c) acc rest' + + flush :: Text -> [TemplatePiece] -> [TemplatePiece] + flush literal acc + | Text.null literal = acc + | otherwise = Literal literal : acc + + parseSlot :: Text -> Maybe (Int, Text) + parseSlot text = do + text' <- Text.stripPrefix "<x" text + (digit, rest) <- Text.uncons text' + guard (isDigit digit) + rest' <- Text.stripPrefix "/>" rest + let slot = digitToInt digit + guard (slot > 0 && slot <= 9) + pure (slot, rest') + + _unusedLineNo = lineNo + + +renderBlock :: HintMap -> ReferenceContext -> BlockRenderInfo -> Html () +renderBlock hints references (_index, block, blockId) = case block of + BlockAxiom _loc title marker axiom -> + renderCustomBlock blockId "axiom-" "Axiom" (Just marker) title (renderAxiom hints axiom) + BlockClaim kind _loc title marker claim -> + renderCustomBlock blockId (claimKindElement kind) (claimKindPrefix kind) (Just marker) title (renderClaim hints claim) + BlockProof _start proof _end -> + renderProofBlock hints references proof + BlockDefn _loc title marker defn -> + renderCustomBlock blockId "definition-" "Definition" (Just marker) title (renderDefn hints defn) + BlockAbbr _loc title marker abbr -> + renderCustomBlock blockId "abbreviation-" "Abbreviation" (Just marker) title (renderAbbreviation hints abbr) + BlockData _loc title marker datatype -> + renderCustomBlock blockId "datatype-" "Datatype" (Just marker) title (renderDatatype hints datatype) + BlockInductive _loc title marker ind -> + renderCustomBlock blockId "inductive-" "Inductive" (Just marker) title (renderInductive hints marker ind) + BlockSig _loc title marker asms sig -> + renderCustomBlock blockId "signature-" "Signature" (Just marker) title (renderSignatureBlock hints asms sig) + BlockStruct _loc title marker structDefn -> + renderCustomBlock blockId "struct-" "Structure" (Just marker) title (renderStructDefn hints structDefn) + +renderTocEntry :: (Int, Text, Block) -> Html () +renderTocEntry (index, blockId, block) = + li_ do + a_ [href_ (renderUrlFragment blockId)] do + span_ (toHtml (blockPrefixText block)) + case formatMarker (blockMarkerOf block) of + Nothing -> + when (blockNeedsIndexLabel block) do + code_ (toHtml (Text.pack (show index))) + Just marker -> + code_ (toHtml marker) + +includeInToc :: Block -> Bool +includeInToc = \case + BlockProof{} -> False + _ -> True + +renderCustomBlock :: Text -> Text -> Text -> Maybe Marker -> Maybe BlockTitle -> Html () -> Html () +renderCustomBlock blockId name prefix mmarker mtitle body = + term name (id_ blockId : previewTargetAttributes prefix mmarker mtitle) do + renderBlockLead prefix mmarker mtitle True + body + +previewTargetAttributes :: Text -> Maybe Marker -> Maybe BlockTitle -> [Attributes] +previewTargetAttributes prefix mmarker mtitle = + case formatMarker mmarker of + Nothing -> + [] + Just marker -> + [ makeAttributes "data-preview-kind" prefix + , makeAttributes "data-preview-label" marker + ] + <> case formatBlockTitle mtitle of + Nothing -> + [] + Just title -> + [makeAttributes "data-preview-title" title] + +renderProofBlock :: HintMap -> ReferenceContext -> Proof -> Html () +renderProofBlock hints references proof + | proofStepCount proof >= proofCollapseThreshold = + term "proof-" do + details_ do + summary_ (renderBlockLead "Proof" Nothing Nothing False) + renderProof hints references proof + | otherwise = + term "proof-" do + renderBlockLead "Proof" Nothing Nothing True + renderProof hints references proof + +blockAnchorId :: Int -> Block -> Text +blockAnchorId index block = + case formatMarker (blockMarkerOf block) of + Just marker -> marker + Nothing -> sanitizeIdFragment (Text.toLower (blockPrefixText block) <> "-" <> Text.pack (show index)) + +sanitizeIdFragment :: Text -> Text +sanitizeIdFragment = + Text.dropWhile (== '-') . Text.map sanitize . Text.toLower + where + sanitize c + | isAlphaNum c = c + | c == '-' || c == '_' = c + | otherwise = '-' + +blockPrefixText :: Block -> Text +blockPrefixText = \case + BlockAxiom{} -> "Axiom" + BlockClaim kind _ _ _ _ -> claimKindPrefix kind + BlockProof{} -> "Proof" + BlockDefn{} -> "Definition" + BlockAbbr{} -> "Abbreviation" + BlockData{} -> "Datatype" + BlockInductive{} -> "Inductive" + BlockSig{} -> "Signature" + BlockStruct{} -> "Structure" + +blockMarkerOf :: Block -> Maybe Marker +blockMarkerOf = \case + BlockAxiom _ _ marker _ -> Just marker + BlockClaim _ _ _ marker _ -> Just marker + BlockProof{} -> Nothing + BlockDefn _ _ marker _ -> Just marker + BlockAbbr _ _ marker _ -> Just marker + BlockData _ _ marker _ -> Just marker + BlockInductive _ _ marker _ -> Just marker + BlockSig _ _ marker _ _ -> Just marker + BlockStruct _ _ marker _ -> Just marker + +blockTitleOf :: Block -> Maybe BlockTitle +blockTitleOf = \case + BlockAxiom _ title _ _ -> title + BlockClaim _ _ title _ _ -> title + BlockProof{} -> Nothing + BlockDefn _ title _ _ -> title + BlockAbbr _ title _ _ -> title + BlockData _ title _ _ -> title + BlockInductive _ title _ _ -> title + BlockSig _ title _ _ _ -> title + BlockStruct _ title _ _ -> title + +blockNeedsIndexLabel :: Block -> Bool +blockNeedsIndexLabel block = case (formatMarker (blockMarkerOf block), formatBlockTitle (blockTitleOf block)) of + (Nothing, Nothing) -> True + _ -> False + +renderBlockLead :: Text -> Maybe Marker -> Maybe BlockTitle -> Bool -> Html () +renderBlockLead prefix mmarker mtitle withTrailingSpace = + term "head-" do + toHtml prefix + case formatMarker mmarker of + Nothing -> skip + Just marker -> + term "id-" (toHtml marker) + case formatBlockTitle mtitle of + Nothing -> + toHtml ("." <> suffix) + Just title -> do + toHtml (" (" :: Text) + term "title-" (toHtml title) + toHtml (")." <> suffix) + where + suffix :: Text + suffix + | withTrailingSpace = " " + | otherwise = "" + +formatMarker :: Maybe Marker -> Maybe Text +formatMarker = \case + Nothing -> Nothing + Just marker -> + let text = Text.strip (markerText marker) + in if Text.null text then Nothing else Just text + +formatBlockTitle :: Maybe BlockTitle -> Maybe Text +formatBlockTitle = + fmap capitalizeTitle . nonEmptyTitle + where + nonEmptyTitle = \case + Nothing -> Nothing + Just toks -> + let text = Text.strip (Text.unwords (tokToText <$> toks)) + in if Text.null text then Nothing else Just text + +capitalizeTitle :: Text -> Text +capitalizeTitle text = case Text.uncons text of + Nothing -> text + Just (c, rest) -> Text.cons (toUpper c) rest + +claimKindElement :: ClaimKind -> Text +claimKindElement = \case + Proposition -> "proposition-" + Theorem -> "theorem-" + Lemma -> "lemma-" + Corollary -> "corollary-" + PlainClaim -> "claim-" + +claimKindPrefix :: ClaimKind -> Text +claimKindPrefix = \case + Proposition -> "Proposition" + Theorem -> "Theorem" + Lemma -> "Lemma" + Corollary -> "Corollary" + PlainClaim -> "Claim" + + +renderAxiom :: HintMap -> Axiom -> Html () +renderAxiom hints (Axiom asms stmt) = + renderWithAssumptions hints asms stmt + +renderClaim :: HintMap -> Claim -> Html () +renderClaim hints (Claim asms stmt) = + renderWithAssumptions hints asms stmt + +renderWithAssumptions :: HintMap -> [Asm] -> Stmt -> Html () +renderWithAssumptions hints asms stmt = do + case asms of + [] -> renderStmtInline hints stmt + _ -> do + toHtml ("Suppose " :: Text) + renderAsmList hints asms + toHtml (". Then " :: Text) + renderStmtInline hints stmt + toHtml ("." :: Text) + +renderDefn :: HintMap -> Defn -> Html () +renderDefn hints = \case + Defn asms headStmt stmt -> + do + when (not (null asms)) do + toHtml ("If " :: Text) + renderAsmList hints asms + toHtml (", then " :: Text) + renderDefnHead hints headStmt + toHtml (" iff " :: Text) + renderStmtInline hints stmt + toHtml ("." :: Text) + DefnFun asms fun maybeSymbol resultTerm -> + do + when (not (null asms)) do + toHtml ("If " :: Text) + renderAsmList hints asms + toHtml (", then " :: Text) + renderFunInline renderVarInline fun + case maybeSymbol of + Nothing -> skip + Just symbolicTerm -> do + toHtml (", " :: Text) + renderTermInline hints symbolicTerm + toHtml (" is " :: Text) + renderTermInline hints resultTerm + toHtml ("." :: Text) + DefnOp symb expr -> + do + inlineMath do + renderSymbolPatternMath hints symb + moText "=" + renderExprMathRow hints expr + toHtml ("." :: Text) + +renderDefnHead :: HintMap -> DefnHead -> Html () +renderDefnHead hints = \case + DefnAdj maybeNp var adj -> do + renderTypedVar hints maybeNp var + toHtml (" is " :: Text) + renderAdjInline renderVarInline adj + DefnVerb maybeNp var verb -> do + renderTypedVar hints maybeNp var + toHtml (" " :: Text) + renderVerbInline False renderVarInline verb + DefnNoun var noun -> do + renderVarInline var + toHtml (" is a " :: Text) + renderNounInline False renderVarInline noun + DefnSymbolicPredicate predi marker vars -> + inlineMath + ( renderHintedMathRow + hints + PredicateHint + marker + (ExprVar <$> toList vars) + (renderPrefixPredicateFallback predi (renderVarMath <$> toList vars)) + ) + DefnRel x rel params y -> + inlineMath (renderRelationApplication hints Positive [ExprVar x] (Relation Nowhere rel [ExprVar p | p <- params]) [ExprVar y]) + +renderTypedVar :: HintMap -> Maybe (NounPhrase Maybe) -> VarSymbol -> Html () +renderTypedVar hints = \case + Nothing -> renderVarInline + Just np -> \var -> do + renderNounPhraseMaybe hints np + toHtml (" " :: Text) + renderVarInline var + + +renderAbbreviation :: HintMap -> Abbreviation -> Html () +renderAbbreviation hints = \case + AbbreviationAdj var adj stmt -> + do + renderVarInline var + toHtml (" is " :: Text) + renderAdjInline renderVarInline adj + toHtml (" stands for " :: Text) + renderStmtInline hints stmt + toHtml ("." :: Text) + AbbreviationVerb var verb stmt -> + do + renderVarInline var + toHtml (" " :: Text) + renderVerbInline False renderVarInline verb + toHtml (" stands for " :: Text) + renderStmtInline hints stmt + toHtml ("." :: Text) + AbbreviationNoun var noun stmt -> + do + renderVarInline var + toHtml (" is a " :: Text) + renderNounInline False renderVarInline noun + toHtml (" stands for " :: Text) + renderStmtInline hints stmt + toHtml ("." :: Text) + AbbreviationRel x rel params y stmt -> + do + inlineMath (renderRelationApplication hints Positive [ExprVar x] (Relation Nowhere rel [ExprVar p | p <- params]) [ExprVar y]) + toHtml (" stands for " :: Text) + renderStmtInline hints stmt + toHtml ("." :: Text) + AbbreviationFun fun bodyTerm -> + do + renderFunInline renderVarInline fun + toHtml (" stands for " :: Text) + renderTermInline hints bodyTerm + toHtml ("." :: Text) + AbbreviationEq symb expr -> + do + renderSymbolPatternInline hints symb + toHtml (" stands for " :: Text) + inlineMath (renderExprMathRow hints expr) + toHtml ("." :: Text) + +renderDatatype :: HintMap -> Datatype -> Html () +renderDatatype hints Datatype{..} = do + toHtml ("Datatype of " :: Text) + inlineMath (renderExprMathRow hints datatypeHeadExpr) + toHtml ("." :: Text) + ul_ do + traverse_ renderDatatypeClause (toList datatypeClauses) + -- Derived facts require checked semantic context. + where + renderDatatypeClause :: DatatypeClause -> Html () + renderDatatypeClause DatatypeClause{..} = li_ do + inlineMath do + renderRelationApplication hints Positive [datatypeClauseConstructorExpr] (Relation Nowhere ElementSymbol []) [datatypeClauseTargetExpr] + case datatypeClausePremises of + [] -> + toHtml ("." :: Text) + premises -> do + toHtml (" for " :: Text) + joinHtml (toHtml (" and " :: Text)) (renderDatatypePremise <$> premises) + toHtml ("." :: Text) + + renderDatatypePremise :: (VarSymbol, Expr) -> Html () + renderDatatypePremise (x, domain) = + inlineMath (renderRelationApplication hints Positive [ExprVar x] (Relation Nowhere ElementSymbol []) [domain]) + +exprVar :: Expr -> Maybe VarSymbol +exprVar = \case + ExprVar x -> + Just x + _ -> + Nothing + +substituteExpr :: Map.Map VarSymbol Expr -> Expr -> Expr +substituteExpr env = \case + ExprVar x -> + fromMaybe (ExprVar x) (Map.lookup x env) + ExprInteger loc n -> + ExprInteger loc n + ExprOp loc symbol args -> + ExprOp loc symbol (substituteExpr env <$> args) + ExprStructOp loc symbol expr -> + ExprStructOp loc symbol (substituteExpr env <$> expr) + ExprFiniteSet loc exprs -> + ExprFiniteSet loc (substituteExpr env <$> exprs) + ExprSep loc x bound stmt -> + ExprSep loc x (substituteExpr env bound) stmt + ExprReplace loc expr bounds maybeStmt -> + ExprReplace loc (substituteExpr env expr) ((\(x, bound) -> (x, substituteExpr env bound)) <$> bounds) maybeStmt + ExprReplacePred loc x y expr stmt -> + ExprReplacePred loc x y (substituteExpr env expr) stmt + +elementOfFormula :: Expr -> Expr -> Formula +elementOfFormula left right = + FormulaChain (ChainBase (left :| []) Positive (Relation Nowhere ElementSymbol []) (right :| [])) + +semanticSubsetFormula :: Set VarSymbol -> Expr -> Expr -> Formula +semanticSubsetFormula reserved left right = + forallIfNeeded [witnessVar] + (impliesFormula + (elementOfFormula (ExprVar witnessVar) left) + (elementOfFormula (ExprVar witnessVar) right)) + where + witnessVar = freshDatatypeVar (reserved <> Set.fromList (exprVars left <> exprVars right)) "x" + +equalsFormula :: Expr -> Expr -> Formula +equalsFormula left right = + FormulaChain (ChainBase (left :| []) Positive (Relation Nowhere EqSymbol []) (right :| [])) + +impliesFormula :: Formula -> Formula -> Formula +impliesFormula left right = + Connected Nowhere Implication left right + +formulaConjunction :: [Formula] -> Formula +formulaConjunction = \case + [] -> + PropositionalConstant Nowhere IsTop + phi : rest -> + foldl' (\left right -> Connected Nowhere Conjunction left right) phi rest + +formulaDisjunction :: [Formula] -> Formula +formulaDisjunction = \case + [] -> + PropositionalConstant Nowhere IsBottom + phi : rest -> + foldl' (\left right -> Connected Nowhere Disjunction left right) phi rest + +forallIfNeeded :: [VarSymbol] -> Formula -> Formula +forallIfNeeded [] phi = phi +forallIfNeeded vars phi = + FormulaQuantified Nowhere Universally (NonEmpty.fromList vars) Unbounded phi + +existsIfNeeded :: [VarSymbol] -> Formula -> Formula +existsIfNeeded [] phi = phi +existsIfNeeded vars phi = + FormulaQuantified Nowhere Existentially (NonEmpty.fromList vars) Unbounded phi + +impliesFrom :: [Formula] -> Formula -> Formula +impliesFrom [] conclusion = conclusion +impliesFrom premises conclusion = impliesFormula (formulaConjunction premises) conclusion + +freshDatatypeVar :: Set VarSymbol -> Text -> VarSymbol +freshDatatypeVar used base = + List.head + [ NamedVar candidate + | candidate <- base : [base <> Text.pack (show n) | n <- [(1 :: Int) ..]] + , NamedVar candidate `Set.notMember` used + ] + +renderInductive :: HintMap -> Marker -> Inductive -> Html () +renderInductive hints marker Inductive{..} = do + toHtml ("Inductive definition of " :: Text) + renderSymbolPatternInline hints inductiveSymbolPattern + toHtml (" over " :: Text) + inlineMath (renderExprMathRow hints inductiveDomain) + toHtml ("." :: Text) + ul_ do + traverse_ renderIntro (toList inductiveIntros) + case inductiveDerivedFacts marker Inductive{..} of + [] -> + skip + derivedFacts -> + details_ do + summary_ (toHtml ("Derived facts" :: Text)) + ul_ [class_ "inductive-derived-facts"] do + traverse_ (renderInductiveDerivedFact hints) derivedFacts + where + renderIntro :: IntroRule -> Html () + renderIntro IntroRule{..} = li_ do + case introConditions of + [] -> skip + _ -> do + toHtml ("If " :: Text) + joinHtml (toHtml (" and " :: Text)) (inlineMath . renderFormulaMath hints <$> introConditions) + toHtml (", then " :: Text) + inlineMath (renderFormulaMath hints introResult) + toHtml ("." :: Text) + +renderInductiveDerivedFact :: HintMap -> InductiveDerivedFact -> Html () +renderInductiveDerivedFact hints InductiveDerivedFact{inductiveDerivedFactMarker, inductiveDerivedFactFormula} = + li_ (id_ (markerText inductiveDerivedFactMarker) : previewTargetAttributes "Inductive Fact" (Just inductiveDerivedFactMarker) Nothing) do + term "head-" do + code_ (toHtml (markerText inductiveDerivedFactMarker)) + toHtml (": " :: Text) + inlineMath (renderFormulaMath hints inductiveDerivedFactFormula) + toHtml ("." :: Text) + +data InductiveDerivedFact = InductiveDerivedFact + { inductiveDerivedFactMarker :: Marker + , inductiveDerivedFactFormula :: Formula + } + +data InductiveRenderInfo = InductiveRenderInfo + { inductiveFactBaseMarker :: Marker + , inductiveRenderParams :: [VarSymbol] + , inductiveRenderCarrierExpr :: Expr + , inductiveRenderDomainExpr :: Expr + , inductiveRenderClauses :: NonEmpty InductiveRenderClause + } + +data InductiveRenderClause = InductiveRenderClause + { inductiveRenderClauseVars :: [VarSymbol] + , inductiveRenderClauseConditions :: [InductiveRenderCondition] + , inductiveRenderClauseResultExpr :: Expr + } + +data InductiveRenderCondition + = InductiveRenderSideCondition Formula + | InductiveRenderRecursiveCondition Expr Expr + +inductiveDerivedFacts :: Marker -> Inductive -> [InductiveDerivedFact] +inductiveDerivedFacts marker inductive = case inductiveRenderInfo marker inductive of + Nothing -> + [] + Just info -> + inductiveIntroFacts info + <> [ InductiveDerivedFact (inductiveDomSubsetMarker info) (inductiveDomSubsetFormula info) + , InductiveDerivedFact (inductiveCasesMarker info) (inductiveCasesFormula info) + , InductiveDerivedFact (inductiveInductMarker info) (inductiveInductFormula info) + ] + +inductiveRenderInfo :: Marker -> Inductive -> Maybe InductiveRenderInfo +inductiveRenderInfo marker Inductive{inductiveSymbolPattern = SymbolPattern inductiveSymbol inductiveParams, inductiveDomain, inductiveIntros} = do + inductiveRenderClauses <- traverse (inductiveRenderClause inductiveSymbol inductiveParams) inductiveIntros + pure InductiveRenderInfo + { inductiveFactBaseMarker = marker + , inductiveRenderParams = inductiveParams + , inductiveRenderCarrierExpr = ExprOp Nowhere inductiveSymbol (ExprVar <$> inductiveParams) + , inductiveRenderDomainExpr = inductiveDomain + , inductiveRenderClauses + } + where + inductiveRenderClause :: MixfixItem -> [VarSymbol] -> IntroRule -> Maybe InductiveRenderClause + inductiveRenderClause symbol params IntroRule{introConditions, introResult} = do + inductiveRenderClauseResultExpr <- inductiveRenderResultExpr symbol params introResult + inductiveRenderClauseConditions <- traverse (inductiveRenderCondition symbol params) introConditions + let paramSet = Set.fromList params + inductiveRenderClauseVars = + List.filter (`Set.notMember` paramSet) + (orderedRenderVars (concatMap formulaVars introConditions <> exprVars inductiveRenderClauseResultExpr)) + pure InductiveRenderClause + { inductiveRenderClauseVars + , inductiveRenderClauseConditions + , inductiveRenderClauseResultExpr + } + +inductiveRenderResultExpr :: MixfixItem -> [VarSymbol] -> Formula -> Maybe Expr +inductiveRenderResultExpr symbol params = \case + FormulaChain (ChainBase (resultExpr :| []) Positive (Relation _ ElementSymbol []) (carrierExpr :| [])) + | sameInductiveCarrierExpr symbol params carrierExpr -> + Just resultExpr + _ -> + Nothing + +inductiveRenderCondition :: MixfixItem -> [VarSymbol] -> Formula -> Maybe InductiveRenderCondition +inductiveRenderCondition symbol params phi + | not (formulaMentionsFunction symbol phi) = + Just (InductiveRenderSideCondition phi) + | otherwise = case phi of + FormulaChain (ChainBase (recursiveTerm :| []) Positive (Relation _ ElementSymbol []) (recursiveCarrier :| [])) + | not (exprMentionsFunction symbol recursiveTerm) -> + InductiveRenderRecursiveCondition recursiveTerm <$> replaceCarrierExpr symbol params recursiveCarrier + _ -> + Nothing + where + replaceCarrierExpr :: MixfixItem -> [VarSymbol] -> Expr -> Maybe Expr + replaceCarrierExpr target targetParams = + replaceInductiveCarrierExpr target targetParams (ExprVar "__inductive") + +inductiveIntroFacts :: InductiveRenderInfo -> [InductiveDerivedFact] +inductiveIntroFacts info = + [ InductiveDerivedFact (inductiveIntroMarker info index) (inductiveIntroFormula info clause) + | (index, clause) <- zip [(1 :: Int) ..] (NonEmpty.toList (inductiveRenderClauses info)) + ] + +inductiveIntroMarker :: InductiveRenderInfo -> Int -> Marker +inductiveIntroMarker info index = + Marker (markerText (inductiveFactBaseMarker info) <> "_intro_" <> Text.pack (show index)) + +inductiveDomSubsetMarker :: InductiveRenderInfo -> Marker +inductiveDomSubsetMarker info = + Marker (markerText (inductiveFactBaseMarker info) <> "_dom_subset") + +inductiveCasesMarker :: InductiveRenderInfo -> Marker +inductiveCasesMarker info = + Marker (markerText (inductiveFactBaseMarker info) <> "_cases") + +inductiveInductMarker :: InductiveRenderInfo -> Marker +inductiveInductMarker info = + Marker (markerText (inductiveFactBaseMarker info) <> "_induct") + +inductiveIntroFormula :: InductiveRenderInfo -> InductiveRenderClause -> Formula +inductiveIntroFormula info clause = + forallIfNeeded (orderedRenderVars (inductiveRenderParams info <> inductiveRenderClauseVars clause)) + (impliesFrom premises conclusion) + where + premises = inductiveRenderConditionFormula info <$> inductiveRenderClauseConditions clause + conclusion = elementOfFormula (inductiveRenderClauseResultExpr clause) (inductiveRenderCarrierExpr info) + +inductiveDomSubsetFormula :: InductiveRenderInfo -> Formula +inductiveDomSubsetFormula info = + forallIfNeeded (inductiveRenderParams info) + (semanticSubsetFormula (inductiveUsedVars info) (inductiveRenderCarrierExpr info) (inductiveRenderDomainExpr info)) + +inductiveCasesFormula :: InductiveRenderInfo -> Formula +inductiveCasesFormula info = + forallIfNeeded (orderedRenderVars (inductiveRenderParams info <> [witnessVar])) + (impliesFormula (elementOfFormula (ExprVar witnessVar) (inductiveRenderCarrierExpr info)) (formulaDisjunction disjuncts)) + where + witnessVar = freshDatatypeVar (inductiveUsedVars info) "x" + disjuncts = inductiveCaseDisjunct witnessVar <$> NonEmpty.toList (inductiveRenderClauses info) + inductiveCaseDisjunct x clause = + existsIfNeeded (inductiveRenderClauseVars clause) + (formulaConjunction (premises <> [equalsFormula (ExprVar x) (inductiveRenderClauseResultExpr clause)])) + where + premises = inductiveRenderConditionFormula info <$> inductiveRenderClauseConditions clause + +inductiveInductFormula :: InductiveRenderInfo -> Formula +inductiveInductFormula info = + forallIfNeeded (orderedRenderVars (inductiveRenderParams info <> [subsetVar])) + (impliesFrom closures conclusion) + where + subsetVar = freshDatatypeVar (inductiveUsedVars info) "S" + closures = inductiveInductionClosure subsetVar <$> NonEmpty.toList (inductiveRenderClauses info) + conclusion = + semanticSubsetFormula + (Set.insert subsetVar (inductiveUsedVars info)) + (inductiveRenderCarrierExpr info) + (ExprVar subsetVar) + +inductiveInductionClosure :: VarSymbol -> InductiveRenderClause -> Formula +inductiveInductionClosure subsetVar clause = + forallIfNeeded (inductiveRenderClauseVars clause) (impliesFrom premises conclusion) + where + premises = inductiveRenderConditionFormulaAt (ExprVar subsetVar) <$> inductiveRenderClauseConditions clause + conclusion = elementOfFormula (inductiveRenderClauseResultExpr clause) (ExprVar subsetVar) + +inductiveRenderConditionFormula :: InductiveRenderInfo -> InductiveRenderCondition -> Formula +inductiveRenderConditionFormula info = + inductiveRenderConditionFormulaAt (inductiveRenderCarrierExpr info) + +inductiveRenderConditionFormulaAt :: Expr -> InductiveRenderCondition -> Formula +inductiveRenderConditionFormulaAt replacement = \case + InductiveRenderSideCondition phi -> + phi + InductiveRenderRecursiveCondition recursiveTerm recursiveCarrierTemplate -> + elementOfFormula recursiveTerm (substituteExpr (Map.singleton "__inductive" replacement) recursiveCarrierTemplate) + +inductiveUsedVars :: InductiveRenderInfo -> Set VarSymbol +inductiveUsedVars info = + Set.fromList + ( inductiveRenderParams info + <> [ var + | clause <- NonEmpty.toList (inductiveRenderClauses info) + , var <- inductiveRenderClauseVars clause + ] + ) + +sameInductiveCarrierExpr :: MixfixItem -> [VarSymbol] -> Expr -> Bool +sameInductiveCarrierExpr symbol params = \case + ExprOp _ symbol' args -> + symbol == symbol' + && length params == length args + && and (zipWith (\param arg -> exprVar arg == Just param) params args) + _ -> + False + +replaceInductiveCarrierExpr :: MixfixItem -> [VarSymbol] -> Expr -> Expr -> Maybe Expr +replaceInductiveCarrierExpr symbol params replacement = go + where + go = \case + ExprVar x -> + Just (ExprVar x) + ExprInteger loc n -> + Just (ExprInteger loc n) + ExprOp loc symbol' args + | sameInductiveCarrierExpr symbol params (ExprOp loc symbol' args) -> + Just replacement + | symbol == symbol' -> + Nothing + | otherwise -> + ExprOp loc symbol' <$> traverse go args + ExprStructOp loc structSymbol expr -> + ExprStructOp loc structSymbol <$> traverse go expr + ExprFiniteSet loc exprs -> + ExprFiniteSet loc <$> traverse go exprs + ExprSep{} -> + Nothing + ExprReplace{} -> + Nothing + ExprReplacePred{} -> + Nothing + +formulaMentionsFunction :: MixfixItem -> Formula -> Bool +formulaMentionsFunction symbol = \case + FormulaChain chain -> + chainMentionsFunction symbol chain + FormulaPredicate _loc _predicate _marker exprs -> + any (exprMentionsFunction symbol) exprs + Connected _loc _conn left right -> + formulaMentionsFunction symbol left || formulaMentionsFunction symbol right + FormulaNeg _loc phi -> + formulaMentionsFunction symbol phi + FormulaQuantified _loc _quant _vars _bound phi -> + formulaMentionsFunction symbol phi + PropositionalConstant{} -> + False + +chainMentionsFunction :: MixfixItem -> Chain -> Bool +chainMentionsFunction symbol = \case + ChainBase left _sign relation right -> + any (exprMentionsFunction symbol) left || relationMentionsFunction symbol relation || any (exprMentionsFunction symbol) right + ChainCons left _sign relation rest -> + any (exprMentionsFunction symbol) left || relationMentionsFunction symbol relation || chainMentionsFunction symbol rest + +relationMentionsFunction :: MixfixItem -> Relation -> Bool +relationMentionsFunction symbol = \case + Relation _loc _relationSymbol exprs -> + any (exprMentionsFunction symbol) exprs + RelationExpr _loc expr -> + exprMentionsFunction symbol expr + +exprMentionsFunction :: MixfixItem -> Expr -> Bool +exprMentionsFunction symbol = \case + ExprVar{} -> + False + ExprInteger{} -> + False + ExprOp _loc symbol' args -> + symbol == symbol' || any (exprMentionsFunction symbol) args + ExprStructOp _loc _structSymbol expr -> + maybe False (exprMentionsFunction symbol) expr + ExprFiniteSet _loc exprs -> + any (exprMentionsFunction symbol) exprs + ExprSep _loc _var bound _stmt -> + exprMentionsFunction symbol bound + ExprReplace _loc expr bounds _maybeStmt -> + exprMentionsFunction symbol expr || any (exprMentionsFunction symbol . snd) bounds + ExprReplacePred _loc _x _y expr _stmt -> + exprMentionsFunction symbol expr + +formulaVars :: Formula -> [VarSymbol] +formulaVars = \case + FormulaChain chain -> + chainVars chain + FormulaPredicate _loc _predicate _marker exprs -> + concatMap exprVars exprs + Connected _loc _conn left right -> + formulaVars left <> formulaVars right + FormulaNeg _loc phi -> + formulaVars phi + FormulaQuantified _loc _quant vars _bound phi -> + List.filter (`notElem` toList vars) (formulaVars phi) + PropositionalConstant{} -> + [] + +chainVars :: Chain -> [VarSymbol] +chainVars = \case + ChainBase left _sign relation right -> + concatMap exprVars (toList left) <> relationVars relation <> concatMap exprVars (toList right) + ChainCons left _sign relation rest -> + concatMap exprVars (toList left) <> relationVars relation <> chainVars rest + +relationVars :: Relation -> [VarSymbol] +relationVars = \case + Relation _loc _relationSymbol exprs -> + concatMap exprVars exprs + RelationExpr _loc expr -> + exprVars expr + +exprVars :: Expr -> [VarSymbol] +exprVars = \case + ExprVar x -> + [x] + ExprInteger{} -> + [] + ExprOp _loc _symbol args -> + concatMap exprVars args + ExprStructOp _loc _structSymbol expr -> + maybe [] exprVars expr + ExprFiniteSet _loc exprs -> + concatMap exprVars exprs + ExprSep _loc x bound _stmt -> + List.filter (/= x) (exprVars bound) + ExprReplace _loc expr bounds _maybeStmt -> + let boundVars = fst <$> toList bounds + free = exprVars expr <> concatMap (exprVars . snd) (toList bounds) + in List.filter (`notElem` boundVars) free + ExprReplacePred _loc x y expr _stmt -> + List.filter (\var -> var /= x && var /= y) (exprVars expr) + +orderedRenderVars :: [VarSymbol] -> [VarSymbol] +orderedRenderVars = + reverse . snd . foldl' step (Set.empty, []) + where + step (seen, acc) x + | x `Set.member` seen = (seen, acc) + | otherwise = (Set.insert x seen, x : acc) + +renderSignatureBlock :: HintMap -> [Asm] -> Signature -> Html () +renderSignatureBlock hints asms sig = do + case asms of + [] -> skip + _ -> do + toHtml ("Assumptions: " :: Text) + renderAsmList hints asms + toHtml ("." :: Text) + when (not (null asms)) do + p_ do + renderSignature hints sig + toHtml ("." :: Text) + when (null asms) do + renderSignature hints sig + toHtml ("." :: Text) + +renderSignature :: HintMap -> Signature -> Html () +renderSignature hints = \case + SignatureAdj var adj -> do + renderVarInline var + toHtml (" can be " :: Text) + renderAdjInline renderVarInline adj + SignatureVerb var verb -> do + renderVarInline var + toHtml (" can " :: Text) + renderVerbInline False renderVarInline verb + SignatureNoun var noun -> do + renderVarInline var + toHtml (" is a " :: Text) + renderNounInline False renderVarInline noun + SignatureSymbolic symb np -> do + renderSymbolPatternInline hints symb + toHtml (" is a " :: Text) + renderNounPhraseMaybe hints np + +renderStructDefn :: HintMap -> StructDefn -> Html () +renderStructDefn hints StructDefn{..} = do + toHtml ("Structure phrase: " :: Text) + renderStructPhraseInline structPhrase + toHtml ("." :: Text) + p_ do + toHtml ("Label: " :: Text) + renderVarInline structLabel + toHtml ("." :: Text) + when (not (null structParents)) do + p_ do + toHtml ("Parents: " :: Text) + joinHtml (toHtml (", " :: Text)) (renderStructPhraseInline <$> structParents) + toHtml ("." :: Text) + when (not (null structFixes)) do + p_ do + toHtml ("Fixes: " :: Text) + inlineMath (joinHtml (moText ",") (renderStructSymbolName <$> structFixes)) + toHtml ("." :: Text) + when (not (null structAssumes)) do + ul_ do + for_ structAssumes \(marker, stmt) -> li_ do + toHtml (markerText marker) + toHtml (": " :: Text) + renderStmtInline hints stmt + toHtml ("." :: Text) + + +buildPreviewMap + :: HtmlRenderContext + -> Set Marker + -> AnchorMap + -> HtmlRenderIndex + -> Either HtmlRenderContextError PreviewMap +buildPreviewMap + context + referencedMarkers + anchors + (HtmlRenderIndex targetIndex) = + Map.fromList <$> traverse makePreviewEntry indexedTargets + where + targets = + List.sortOn targetOrdinal + [ indexed + | marker <- Set.toList referencedMarkers + , marker `Map.notMember` anchors + , Just indexed@(IndexedReferenceTarget _ source _target) <- + [Map.lookup marker targetIndex] + , source /= htmlCurrentSource context + ] + targetOrdinal (IndexedReferenceTarget ordinal _source _target) = + ordinal + sourceTarget (IndexedReferenceTarget _ordinal source target) = + (source, target) + indexedTargets = + zip [1 :: Int ..] (sourceTarget <$> targets) + + makePreviewEntry (index, (source, target)) = do + previewSourceLabel <- + htmlSourceLabel context source + previewSourceHref <- + htmlSourcePageHref context source + previewReferenceHref <- + htmlSourceFragmentHref + context + source + (targetAnchorId target) + let marker = targetMarker target + previewMarker = marker + previewKind = targetKind target + previewTitle = targetTitle target + previewId = + "reference-preview-" <> Text.pack (show index) + previewBody = targetBody target + Right (marker, PreviewEntry{..}) + +renderPreviewStore :: HintMap -> PreviewMap -> Html () +renderPreviewStore hints previews = + div_ [class_ "reference-preview-store", makeAttributes "aria-hidden" "true"] do + traverse_ (renderPreviewEntry hints) (Map.elems previews) + +renderPreviewEntry :: HintMap -> PreviewEntry -> Html () +renderPreviewEntry hints PreviewEntry{..} = + div_ [id_ previewId, class_ "reference-preview-template"] do + div_ [class_ "reference-preview-heading"] do + toHtml previewKind + toHtml (" " :: Text) + code_ (toHtml (markerText previewMarker)) + case previewTitle of + Nothing -> + skip + Just title -> do + toHtml (" (" :: Text) + toHtml title + toHtml (")" :: Text) + div_ [class_ "reference-preview-source"] do + toHtml ("from " :: Text) + a_ [href_ previewSourceHref] do + code_ (toHtml previewSourceLabel) + div_ [class_ "reference-preview-body"] do + previewBody hints + +renderPreviewBlockBody :: HintMap -> Block -> Html () +renderPreviewBlockBody hints = \case + BlockAxiom _loc _title _marker axiom -> + previewStatement (renderAxiom hints axiom) + BlockClaim _kind _loc _title _marker claim -> + previewStatement (renderClaim hints claim) + BlockDefn _loc _title _marker defn -> + previewStatement (renderDefn hints defn) + BlockAbbr _loc _title _marker abbr -> + previewStatement (renderAbbreviation hints abbr) + BlockData _loc _title _marker datatype -> + renderDatatype hints datatype + BlockInductive _loc _title marker ind -> + renderInductive hints marker ind + BlockSig _loc _title _marker asms sig -> + renderSignatureBlock hints asms sig + BlockStruct _loc _title _marker structDefn -> + renderStructDefn hints structDefn + BlockProof{} -> + skip + +previewStatement :: Html () -> Html () +previewStatement = + p_ [class_ "reference-preview-statement"] + +referenceTargetsOfBlockRenderInfo :: BlockRenderInfo -> [ReferenceTarget] +referenceTargetsOfBlockRenderInfo (_index, block, blockId) = + maybeToList blockTarget <> inductiveTargets + where + blockTarget = do + marker <- blockMarkerOf block + pure ReferenceTarget + { targetMarker = marker + , targetAnchorId = blockId + , targetKind = blockPrefixText block + , targetTitle = formatBlockTitle (blockTitleOf block) + , targetBody = \hints -> renderPreviewBlockBody hints block + } + + inductiveTargets = case block of + BlockInductive _loc _title marker inductive -> + [ ReferenceTarget + { targetMarker = inductiveDerivedFactMarker + , targetAnchorId = markerText inductiveDerivedFactMarker + , targetKind = "Inductive Fact" + , targetTitle = Nothing + , targetBody = \hints -> previewStatement (inlineMath (renderFormulaMath hints inductiveDerivedFactFormula)) + } + | InductiveDerivedFact{inductiveDerivedFactMarker, inductiveDerivedFactFormula} <- inductiveDerivedFacts marker inductive + ] + _ -> + [] + + +renderProof :: HintMap -> ReferenceContext -> Proof -> Html () +renderProof hints references = \case + Omitted _loc -> + p_ "Omitted." + Qed mloc justification -> + renderProofTerminal mloc justification + Contradiction _loc justification -> + p_ do + toHtml ("Contradiction" :: Text) + renderJustificationSuffix references justification + toHtml ("." :: Text) + ByCase _loc cases -> do + p_ "Proof by cases." + term "proof-" (traverse_ (renderCase hints references) cases) + ByContradiction _loc proof -> do + p_ "Proof by contradiction." + term "proof-" (renderProof hints references proof) + BySetInduction _loc maybeTerm proof -> do + p_ do + toHtml ("Proof by set induction" :: Text) + case maybeTerm of + Nothing -> skip + Just targetTerm -> do + toHtml (" on " :: Text) + renderTermInline hints targetTerm + toHtml ("." :: Text) + term "proof-" (renderProof hints references proof) + ByOrdInduction _loc proof -> do + p_ "Proof by ordinal induction." + term "proof-" (renderProof hints references proof) + Assume _loc stmt proof -> do + p_ do + toHtml ("Assume " :: Text) + renderStmtInline hints stmt + toHtml ("." :: Text) + renderProofContinuation hints references proof + FixSymbolic _loc vars bound proof -> do + p_ do + toHtml ("Fix " :: Text) + renderVarListInline vars + renderBoundInline hints vars bound + toHtml ("." :: Text) + renderProofContinuation hints references proof + FixSuchThat _loc vars stmt proof -> do + p_ do + toHtml ("Fix " :: Text) + renderVarListInline vars + toHtml (" such that " :: Text) + renderStmtInline hints stmt + toHtml ("." :: Text) + renderProofContinuation hints references proof + Calc _loc maybeQuant calc proof -> do + renderCalc hints references maybeQuant calc + renderProofContinuation hints references proof + TakeVar _loc vars bound stmt justification proof -> do + p_ do + toHtml ("Take " :: Text) + renderVarListInline vars + renderBoundInline hints vars bound + toHtml (" such that " :: Text) + renderStmtInline hints stmt + renderJustificationSuffix references justification + toHtml ("." :: Text) + renderProofContinuation hints references proof + TakeNoun _loc np justification proof -> do + p_ do + toHtml ("Take " :: Text) + renderNounPhraseList hints np + renderJustificationSuffix references justification + toHtml ("." :: Text) + renderProofContinuation hints references proof + Have _loc maybeStmt stmt justification proof -> do + p_ do + case maybeStmt of + Nothing + | isImplicitProofEnd proof -> + skip + | otherwise -> + toHtml ("We have " :: Text) + Just premise -> do + toHtml ("Since " :: Text) + renderStmtInline hints premise + toHtml (", we have " :: Text) + renderStmtInline hints stmt + renderJustificationSuffix references justification + toHtml ("." :: Text) + renderProofContinuation hints references proof + Suffices _loc stmt justification proof -> do + p_ do + toHtml ("It suffices to show that " :: Text) + renderStmtInline hints stmt + renderJustificationSuffix references justification + toHtml ("." :: Text) + renderProofContinuation hints references proof + Subclaim _loc stmt subproof proof -> do + p_ do + toHtml ("Show " :: Text) + renderStmtInline hints stmt + toHtml ("." :: Text) + term "proof-" (renderProof hints references subproof) + renderProofContinuation hints references proof + Define _loc var expr proof -> do + p_ do + toHtml ("Let " :: Text) + renderVarEqInline hints var expr + toHtml ("." :: Text) + renderProofContinuation hints references proof + DefineFunction _loc fun arg value boundVar boundExpr proof -> do + p_ do + toHtml ("Let " :: Text) + renderFunctionEqInline hints fun arg value + toHtml (" for " :: Text) + renderVarInline boundVar + toHtml (" in " :: Text) + inlineMath (renderExprMathRow hints boundExpr) + toHtml ("." :: Text) + renderProofContinuation hints references proof + DefineFunctionLocal _loc fun arg _target domVar codVar rules proof -> do + p_ do + toHtml ("Let " :: Text) + renderFunctionCallInline fun arg + toHtml (" be locally defined from " :: Text) + renderVarInline domVar + toHtml (" to " :: Text) + renderVarInline codVar + toHtml ("." :: Text) + ul_ do + for_ (toList rules) \(ruleTerm, formula) -> li_ do + inlineMath (renderExprMathRow hints ruleTerm) + toHtml (" if " :: Text) + inlineMath (renderFormulaMath hints formula) + toHtml ("." :: Text) + renderProofContinuation hints references proof + + where + renderProofTerminal :: Maybe Location -> Justification -> Html () + renderProofTerminal mloc justification = case (mloc, justification) of + (Nothing, JustificationEmpty) -> + skip + (Just _, JustificationEmpty) -> + p_ "Trivial." + _ -> + p_ do + toHtml ("Follows" :: Text) + renderJustificationSuffix references justification + toHtml ("." :: Text) + +renderProofContinuation :: HintMap -> ReferenceContext -> Proof -> Html () +renderProofContinuation hints references proof = + unless (isImplicitProofEnd proof) (renderProof hints references proof) + +isImplicitProofEnd :: Proof -> Bool +isImplicitProofEnd = \case + Qed Nothing JustificationEmpty -> True + _ -> False + +proofStepCount :: Proof -> Int +proofStepCount = \case + Omitted _loc -> 1 + Qed{} -> 1 + Contradiction{} -> 1 + ByCase _loc cases -> 1 + sum (caseStepCount <$> cases) + ByContradiction _loc proof -> 1 + proofStepCount proof + BySetInduction _loc _maybeTerm proof -> 1 + proofStepCount proof + ByOrdInduction _loc proof -> 1 + proofStepCount proof + Assume _loc _stmt proof -> 1 + proofStepCount proof + FixSymbolic _loc _vars _bound proof -> 1 + proofStepCount proof + FixSuchThat _loc _vars _stmt proof -> 1 + proofStepCount proof + Calc _loc _maybeQuant calc proof -> 1 + calcStepCount calc + proofStepCount proof + TakeVar _loc _vars _bound _stmt _justification proof -> 1 + proofStepCount proof + TakeNoun _loc _np _justification proof -> 1 + proofStepCount proof + Have _loc _maybeStmt _stmt _justification proof -> 1 + proofStepCount proof + Suffices _loc _stmt _justification proof -> 1 + proofStepCount proof + Subclaim _loc _stmt subproof proof -> 1 + proofStepCount subproof + proofStepCount proof + Define _loc _var _expr proof -> 1 + proofStepCount proof + DefineFunction _loc _fun _arg _value _boundVar _boundExpr proof -> 1 + proofStepCount proof + DefineFunctionLocal _loc _fun _arg _target _domVar _codVar rules proof -> + 1 + length rules + proofStepCount proof + +caseStepCount :: Case -> Int +caseStepCount Case{caseProof} = 1 + proofStepCount caseProof + +calcStepCount :: Calc -> Int +calcStepCount = \case + Equation _ steps -> length steps + Biconditionals _ steps -> length steps + +renderCase :: HintMap -> ReferenceContext -> Case -> Html () +renderCase hints references Case{..} = + term "proof-" do + p_ do + toHtml ("Case " :: Text) + renderStmtInline hints caseOf + toHtml ("." :: Text) + renderProof hints references caseProof + +renderCalc :: HintMap -> ReferenceContext -> Maybe CalcQuantifier -> Calc -> Html () +renderCalc hints references maybeQuant calc = do + p_ do + toHtml ("Calculation" :: Text) + case maybeQuant of + Nothing -> skip + Just quant -> do + toHtml (" for " :: Text) + renderCalcQuantifierInline hints quant + toHtml ("." :: Text) + blockMath (renderCalcMath hints calc) + let justifications = calcJustifications calc + when (not (null justifications)) do + ul_ do + traverse_ renderStepJustification justifications + where + renderStepJustification :: (Int, Justification) -> Html () + renderStepJustification (_idx, JustificationEmpty) = skip + renderStepJustification (idx, jst) = li_ do + toHtml ("Step " <> Text.pack (show idx) <> ": " :: Text) + renderJustification references jst + toHtml ("." :: Text) + +renderCalcQuantifierInline :: HintMap -> CalcQuantifier -> Html () +renderCalcQuantifierInline hints (CalcQuantifier vars bound maybeStmt) = do + renderVarListInline vars + renderBoundInline hints vars bound + case maybeStmt of + Nothing -> skip + Just stmt -> do + toHtml (" such that " :: Text) + renderStmtInline hints stmt + +renderCalcMath :: HintMap -> Calc -> Html () +renderCalcMath hints = \case + Equation expr steps -> do + renderExprMathRow hints expr + for_ (toList steps) \(nextExpr, _jst) -> do + moText "=" + renderExprMathRow hints nextExpr + Biconditionals phi steps -> do + renderFormulaMath hints phi + for_ (toList steps) \(nextPhi, _jst) -> do + moText "⇔" + renderFormulaMath hints nextPhi + +calcJustifications :: Calc -> [(Int, Justification)] +calcJustifications = \case + Equation _ steps -> + zip [1..] (snd <$> toList steps) + Biconditionals _ steps -> + zip [1..] (snd <$> toList steps) + + +renderStmtInline :: HintMap -> Stmt -> Html () +renderStmtInline hints = \case + StmtFormula phi -> + inlineMath (renderFormulaMath hints phi) + StmtVerbPhrase ts vp -> do + renderTermList hints ts + toHtml (" " :: Text) + renderVerbPhraseInline hints (length ts > 1) vp + StmtNoun ts np -> do + renderTermList hints ts + toHtml (if length ts > 1 then " are a " else " is a " :: Text) + renderNounPhraseMaybe hints np + StmtStruct t structPhrase -> do + renderTermInline hints t + toHtml (" is a " :: Text) + renderStructPhraseInline structPhrase + StmtNeg _loc stmt -> do + toHtml ("it is not the case that " :: Text) + renderStmtInline hints stmt + StmtExists _loc np -> do + toHtml ("there exists " :: Text) + renderNounPhraseList hints np + StmtConnected conn _loc stmt1 stmt2 -> do + renderConnectedStmtInline hints conn stmt1 stmt2 + StmtQuantPhrase _loc qp stmt -> do + renderQuantPhraseInline hints qp + toHtml (" " :: Text) + renderStmtInline hints stmt + SymbolicQuantified _loc quant vars bound suchThat stmt -> do + toHtml (quantifierWord quant) + toHtml (" " :: Text) + renderBoundSubjectInline hints vars bound + renderQuantifiedTailInline hints quant suchThat stmt + +renderQuantPhraseInline :: HintMap -> QuantPhrase -> Html () +renderQuantPhraseInline hints (QuantPhrase quant np) = do + toHtml (quantifierWord quant) + toHtml (" " :: Text) + renderNounPhraseList hints np + +quantifierWord :: Quantifier -> Text +quantifierWord = \case + Universally -> "for every" + Existentially -> "there exists" + Nonexistentially -> "there exists no" + +connectiveWord :: Connective -> Text +connectiveWord = \case + Conjunction -> "and" + Disjunction -> "or" + Implication -> "implies" + Equivalence -> "iff" + ExclusiveOr -> "xor" + NegatedDisjunction -> "nor" + +renderConnectedStmtInline :: HintMap -> Connective -> Stmt -> Stmt -> Html () +renderConnectedStmtInline hints conn stmt1 stmt2 = case conn of + ExclusiveOr -> do + toHtml ("either " :: Text) + renderStmtInline hints stmt1 + toHtml (" or " :: Text) + renderStmtInline hints stmt2 + NegatedDisjunction -> do + toHtml ("neither " :: Text) + renderStmtInline hints stmt1 + toHtml (" nor " :: Text) + renderStmtInline hints stmt2 + _ -> do + renderStmtInline hints stmt1 + toHtml (" " :: Text) + toHtml (connectiveWord conn) + toHtml (" " :: Text) + renderStmtInline hints stmt2 + +renderQuantifiedTailInline :: HintMap -> Quantifier -> Maybe Stmt -> Stmt -> Html () +renderQuantifiedTailInline hints quant suchThat stmt = + case quant of + Universally -> do + for_ suchThat \suchStmt -> do + toHtml (" such that " :: Text) + renderStmtInline hints suchStmt + toHtml (" we have " :: Text) + renderStmtInline hints stmt + Existentially -> + renderExistentialTailInline hints suchThat stmt + Nonexistentially -> + renderExistentialTailInline hints suchThat stmt + +renderExistentialTailInline :: HintMap -> Maybe Stmt -> Stmt -> Html () +renderExistentialTailInline hints suchThat stmt = do + toHtml (" such that " :: Text) + case suchThat of + Nothing -> + renderStmtInline hints stmt + Just suchStmt -> do + renderStmtInline hints suchStmt + toHtml (" and " :: Text) + renderStmtInline hints stmt + + +renderAsmList :: HintMap -> [Asm] -> Html () +renderAsmList hints asms = + joinHtml (toHtml ("; " :: Text)) (renderAsm hints <$> asms) + +renderAsm :: HintMap -> Asm -> Html () +renderAsm hints = \case + AsmSuppose stmt -> + renderStmtInline hints stmt + AsmLetNoun vars np -> do + renderVarListInline vars + toHtml (" be " :: Text) + renderNounPhraseMaybe hints np + AsmLetIn vars expr -> do + renderVarListInline vars + toHtml (" be in " :: Text) + inlineMath (renderExprMathRow hints expr) + AsmLetThe var fun -> do + renderVarInline var + toHtml (" be " :: Text) + renderFunInline renderTermInline' fun + where renderTermInline' = renderTermInline hints + AsmLetEq var expr -> do + renderVarEqInline hints var expr + AsmLetStruct var structPhrase -> do + renderVarInline var + toHtml (" be a " :: Text) + renderStructPhraseInline structPhrase + + +renderTermInline :: HintMap -> Term -> Html () +renderTermInline hints = \case + TermExpr expr -> + inlineMath (renderExprMathRow hints expr) + TermFun fun -> do + toHtml ("the " :: Text) + renderFunInline (renderTermInline hints) fun + TermIota _loc var stmt -> do + toHtml ("the " :: Text) + renderVarInline var + toHtml (" such that " :: Text) + renderStmtInline hints stmt + TermQuantified quant _loc np -> do + toHtml (termQuantifierWord quant) + toHtml (" " :: Text) + renderNounPhraseMaybe hints np + +termQuantifierWord :: Quantifier -> Text +termQuantifierWord = \case + Universally -> "every" + Existentially -> "some" + Nonexistentially -> "no" + +renderTermList :: HintMap -> NonEmpty Term -> Html () +renderTermList hints = + joinHtml (toHtml (" and " :: Text)) . fmap (renderTermInline hints) . toList + +renderNounPhraseMaybe :: HintMap -> NounPhrase Maybe -> Html () +renderNounPhraseMaybe hints (NounPhrase ls noun maybeName rs maybeSuchThat) = do + renderAdjListInline renderTermInline' ls + renderNounInline False renderTermInline' noun + case maybeName of + Nothing -> skip + Just name -> do + toHtml (" " :: Text) + renderVarInline name + renderAdjRListInline hints rs + case maybeSuchThat of + Nothing -> skip + Just stmt -> do + toHtml (" such that " :: Text) + renderStmtInline hints stmt + where + renderTermInline' = renderTermInline hints + +renderNounPhraseList :: HintMap -> NounPhrase [] -> Html () +renderNounPhraseList hints (NounPhrase ls noun names rs maybeSuchThat) = do + renderAdjListInline renderTermInline' ls + renderNounInline (length names > 1) renderTermInline' noun + when (not (null names)) do + toHtml (" " :: Text) + renderVarListInline (NonEmpty.fromList names) + renderAdjRListInline hints rs + case maybeSuchThat of + Nothing -> skip + Just stmt -> do + toHtml (" such that " :: Text) + renderStmtInline hints stmt + where + renderTermInline' = renderTermInline hints + +renderAdjListInline :: (a -> Html ()) -> [AdjLOf a] -> Html () +renderAdjListInline renderArg adjs = + unless (null adjs) do + joinHtml (toHtml (" " :: Text)) (renderAdjLInline renderArg <$> adjs) + toHtml (" " :: Text) + +renderAdjRListInline :: HintMap -> [AdjROf Term] -> Html () +renderAdjRListInline hints adjs = + unless (null adjs) do + toHtml (" " :: Text) + joinHtml (toHtml (" and " :: Text)) (renderAdjRInline hints <$> adjs) + +renderAdjLInline :: (a -> Html ()) -> AdjLOf a -> Html () +renderAdjLInline renderArg (AdjL _loc item args) = + renderLexicalItemInline renderArg item args + +renderAdjRInline :: HintMap -> AdjROf Term -> Html () +renderAdjRInline hints = \case + AdjR _loc item args -> + renderLexicalItemInline (renderTermInline hints) item args + AttrRThat verbPhrase -> do + toHtml ("that " :: Text) + renderVerbPhraseInline hints False verbPhrase + +renderAdjInline :: (a -> Html ()) -> AdjOf a -> Html () +renderAdjInline renderArg (Adj _loc item args) = + renderLexicalItemInline renderArg item args + +renderVerbInline :: Bool -> (a -> Html ()) -> VerbOf a -> Html () +renderVerbInline isPlural renderArg (Verb _loc item args) = + renderLexicalItemSgPlInline isPlural renderArg item args + +renderVerbPhraseInline :: HintMap -> Bool -> VerbPhrase -> Html () +renderVerbPhraseInline hints isPlural = \case + VPVerb verb -> + renderVerbInline isPlural (renderTermInline hints) verb + VPAdj adjs -> do + toHtml (if isPlural then "are " else "is " :: Text) + joinHtml (toHtml (" and " :: Text)) (renderAdjInline (renderTermInline hints) <$> toList adjs) + VPVerbNot verb -> do + toHtml (if isPlural then "do not " else "does not " :: Text) + renderVerbInline True (renderTermInline hints) verb + VPAdjNot adjs -> do + toHtml (if isPlural then "are not " else "is not " :: Text) + joinHtml (toHtml (" and " :: Text)) (renderAdjInline (renderTermInline hints) <$> toList adjs) + +renderNounInline :: Bool -> (a -> Html ()) -> NounOf a -> Html () +renderNounInline isPlural renderArg (Noun _loc item args) = + renderLexicalItemSgPlInline isPlural renderArg item args + +renderFunInline :: (a -> Html ()) -> FunOf a -> Html () +renderFunInline renderArg Fun{phrase, funArgs} = + renderLexicalItemSgPlInline False renderArg phrase funArgs + +renderStructPhraseInline :: StructPhrase -> Html () +renderStructPhraseInline item = + renderLexicalItemSgPlInline False renderTermInlinePlaceholder item [] + +renderTermInlinePlaceholder :: a -> Html () +renderTermInlinePlaceholder _ = toHtml ("?" :: Text) + +renderLexicalItemInline :: (a -> Html ()) -> LexicalItem -> [a] -> Html () +renderLexicalItemInline renderArg item args = + renderPatternInline renderArg (lexicalItemPhrase item) args + +renderLexicalItemSgPlInline :: Bool -> (a -> Html ()) -> LexicalItemSgPl -> [a] -> Html () +renderLexicalItemSgPlInline isPlural renderArg item args = + renderPatternInline renderArg phrase args + where + phrase = if isPlural then pl (lexicalItemSgPlPhrase item) else sg (lexicalItemSgPlPhrase item) + +renderPatternInline :: (a -> Html ()) -> [Maybe Token] -> [a] -> Html () +renderPatternInline renderArg patternParts args = + joinHtml (toHtml (" " :: Text)) (go patternParts args) + where + go [] [] = [] + go [] (_ : _) = error "renderPatternInline: too many arguments" + go (Nothing : rest) (arg : restArgs) = renderArg arg : go rest restArgs + go (Nothing : _) [] = error "renderPatternInline: not enough arguments" + go (Just tok : rest) restArgs = tokenTextHtml tok : go rest restArgs + +renderStmtMath :: HintMap -> Stmt -> Html () +renderStmtMath hints = + renderStmtMathFragments . stmtMathFragments hints + +renderStmtMathFragments :: StmtMathFragments -> Html () +renderStmtMathFragments = + go "" + where + go :: Text -> StmtMathFragments -> Html () + go pending = \case + [] -> + flush pending + StmtMathProse text : rest -> + go (pending <> text) rest + StmtMathNode node : rest -> do + flush pending + node + go "" rest + + flush :: Text -> Html () + flush text = + let renderedText = preserveBoundarySpaces text + in unless (Text.null renderedText) (mtextText renderedText) + + preserveBoundarySpaces :: Text -> Text + preserveBoundarySpaces text = + Text.replicate leadingCount nbsp + <> middleText + <> Text.replicate trailingCount nbsp + where + leadingCount = Text.length (Text.takeWhile (== ' ') text) + textAfterLeading = Text.drop leadingCount text + trailingCount = Text.length (Text.takeWhileEnd (== ' ') textAfterLeading) + middleText = Text.dropEnd trailingCount textAfterLeading + nbsp = Text.singleton '\160' + +stmtMathProse :: Text -> StmtMathFragments +stmtMathProse text + | Text.null text = [] + | otherwise = [StmtMathProse text] + +stmtMathNode :: Html () -> StmtMathFragments +stmtMathNode html = + [StmtMathNode html] + +joinStmtMathFragments :: StmtMathFragments -> [StmtMathFragments] -> StmtMathFragments +joinStmtMathFragments _ [] = [] +joinStmtMathFragments separator (first : rest) = + first <> foldMap (separator <>) rest + +stmtMathFragments :: HintMap -> Stmt -> StmtMathFragments +stmtMathFragments hints = \case + StmtFormula phi -> + stmtMathNode (renderFormulaMath hints phi) + StmtVerbPhrase ts vp -> do + termListMathFragments hints ts + <> stmtMathProse " " + <> verbPhraseMathFragments hints (length ts > 1) vp + StmtNoun ts np -> do + termListMathFragments hints ts + <> stmtMathProse (if length ts > 1 then " are a " else " is a ") + <> nounPhraseMaybeMathFragments hints np + StmtStruct t structPhrase -> do + termMathFragments hints t + <> stmtMathProse " is a " + <> structPhraseMathFragments structPhrase + StmtNeg _loc stmt -> do + stmtMathProse "it is not the case that " + <> stmtMathFragments hints stmt + StmtExists _loc np -> do + stmtMathProse "there exists " + <> nounPhraseListMathFragments hints np + StmtConnected conn _loc stmt1 stmt2 -> do + connectedStmtMathFragments hints conn stmt1 stmt2 + StmtQuantPhrase _loc qp stmt -> do + quantPhraseMathFragments hints qp + <> stmtMathProse " " + <> stmtMathFragments hints stmt + SymbolicQuantified _loc quant vars bound suchThat stmt -> do + stmtMathProse (quantifierWord quant <> " ") + <> boundSubjectMathFragments hints vars bound + <> quantifiedTailMathFragments hints quant suchThat stmt + +quantPhraseMathFragments :: HintMap -> QuantPhrase -> StmtMathFragments +quantPhraseMathFragments hints (QuantPhrase quant np) = + stmtMathProse (quantifierWord quant <> " ") + <> nounPhraseListMathFragments hints np + +connectedStmtMathFragments :: HintMap -> Connective -> Stmt -> Stmt -> StmtMathFragments +connectedStmtMathFragments hints conn stmt1 stmt2 = case conn of + ExclusiveOr -> + stmtMathProse "either " + <> stmtMathFragments hints stmt1 + <> stmtMathProse " or " + <> stmtMathFragments hints stmt2 + NegatedDisjunction -> + stmtMathProse "neither " + <> stmtMathFragments hints stmt1 + <> stmtMathProse " nor " + <> stmtMathFragments hints stmt2 + _ -> + stmtMathFragments hints stmt1 + <> stmtMathProse (" " <> connectiveWord conn <> " ") + <> stmtMathFragments hints stmt2 + +quantifiedTailMathFragments :: HintMap -> Quantifier -> Maybe Stmt -> Stmt -> StmtMathFragments +quantifiedTailMathFragments hints quant suchThat stmt = + case quant of + Universally -> + foldMap + (\suchStmt -> stmtMathProse " such that " <> stmtMathFragments hints suchStmt) + suchThat + <> stmtMathProse " we have " + <> stmtMathFragments hints stmt + Existentially -> + existentialTailMathFragments hints suchThat stmt + Nonexistentially -> + existentialTailMathFragments hints suchThat stmt + +existentialTailMathFragments :: HintMap -> Maybe Stmt -> Stmt -> StmtMathFragments +existentialTailMathFragments hints suchThat stmt = + stmtMathProse " such that " + <> case suchThat of + Nothing -> + stmtMathFragments hints stmt + Just suchStmt -> + stmtMathFragments hints suchStmt + <> stmtMathProse " and " + <> stmtMathFragments hints stmt + +termMathFragments :: HintMap -> Term -> StmtMathFragments +termMathFragments hints = \case + TermExpr expr -> + stmtMathNode (renderExprMathRow hints expr) + TermFun fun -> do + stmtMathProse "the " + <> funMathFragments (termMathFragments hints) fun + TermIota _loc var stmt -> do + stmtMathProse "the " + <> stmtMathNode (renderVarMath var) + <> stmtMathProse " such that " + <> stmtMathFragments hints stmt + TermQuantified quant _loc np -> do + stmtMathProse (termQuantifierWord quant <> " ") + <> nounPhraseMaybeMathFragments hints np + +termListMathFragments :: HintMap -> NonEmpty Term -> StmtMathFragments +termListMathFragments hints = + joinStmtMathFragments (stmtMathProse " and ") . fmap (termMathFragments hints) . toList + +nounPhraseMaybeMathFragments :: HintMap -> NounPhrase Maybe -> StmtMathFragments +nounPhraseMaybeMathFragments hints (NounPhrase ls noun maybeName rs maybeSuchThat) = + adjListMathFragments renderTermMath' ls + <> nounMathFragments False renderTermMath' noun + <> foldMap (\name -> stmtMathProse " " <> stmtMathNode (renderVarMath name)) maybeName + <> adjRListMathFragments hints rs + <> foldMap (\stmt -> stmtMathProse " such that " <> stmtMathFragments hints stmt) maybeSuchThat + where + renderTermMath' = termMathFragments hints + +nounPhraseListMathFragments :: HintMap -> NounPhrase [] -> StmtMathFragments +nounPhraseListMathFragments hints (NounPhrase ls noun names rs maybeSuchThat) = + adjListMathFragments renderTermMath' ls + <> nounMathFragments (length names > 1) renderTermMath' noun + <> if null names + then [] + else stmtMathProse " " <> stmtMathNode (renderVarListMath (NonEmpty.fromList names)) + <> adjRListMathFragments hints rs + <> foldMap (\stmt -> stmtMathProse " such that " <> stmtMathFragments hints stmt) maybeSuchThat + where + renderTermMath' = termMathFragments hints + +adjListMathFragments :: (a -> StmtMathFragments) -> [AdjLOf a] -> StmtMathFragments +adjListMathFragments renderArg adjs = + if null adjs + then [] + else joinStmtMathFragments (stmtMathProse " ") (renderAdjLMathFragments renderArg <$> adjs) + <> stmtMathProse " " + +adjRListMathFragments :: HintMap -> [AdjROf Term] -> StmtMathFragments +adjRListMathFragments hints adjs = + if null adjs + then [] + else stmtMathProse " " + <> joinStmtMathFragments (stmtMathProse " and ") (renderAdjRMathFragments hints <$> adjs) + +renderAdjLMathFragments :: (a -> StmtMathFragments) -> AdjLOf a -> StmtMathFragments +renderAdjLMathFragments renderArg (AdjL _loc item args) = + lexicalItemStmtMathFragments renderArg item args + +renderAdjRMathFragments :: HintMap -> AdjROf Term -> StmtMathFragments +renderAdjRMathFragments hints = \case + AdjR _loc item args -> + lexicalItemStmtMathFragments (termMathFragments hints) item args + AttrRThat verbPhrase -> + stmtMathProse "that " + <> verbPhraseMathFragments hints False verbPhrase + +adjMathFragments :: (a -> StmtMathFragments) -> AdjOf a -> StmtMathFragments +adjMathFragments renderArg (Adj _loc item args) = + lexicalItemStmtMathFragments renderArg item args + +verbMathFragments :: Bool -> (a -> StmtMathFragments) -> VerbOf a -> StmtMathFragments +verbMathFragments isPlural renderArg (Verb _loc item args) = + lexicalItemSgPlStmtMathFragments isPlural renderArg item args + +verbPhraseMathFragments :: HintMap -> Bool -> VerbPhrase -> StmtMathFragments +verbPhraseMathFragments hints isPlural = \case + VPVerb verb -> + verbMathFragments isPlural (termMathFragments hints) verb + VPAdj adjs -> + stmtMathProse (if isPlural then "are " else "is ") + <> joinStmtMathFragments (stmtMathProse " and ") (adjMathFragments (termMathFragments hints) <$> toList adjs) + VPVerbNot verb -> + stmtMathProse (if isPlural then "do not " else "does not ") + <> verbMathFragments True (termMathFragments hints) verb + VPAdjNot adjs -> + stmtMathProse (if isPlural then "are not " else "is not ") + <> joinStmtMathFragments (stmtMathProse " and ") (adjMathFragments (termMathFragments hints) <$> toList adjs) + +nounMathFragments :: Bool -> (a -> StmtMathFragments) -> NounOf a -> StmtMathFragments +nounMathFragments isPlural renderArg (Noun _loc item args) = + lexicalItemSgPlStmtMathFragments isPlural renderArg item args + +funMathFragments :: (a -> StmtMathFragments) -> FunOf a -> StmtMathFragments +funMathFragments renderArg Fun{phrase, funArgs} = + lexicalItemSgPlStmtMathFragments False renderArg phrase funArgs + +structPhraseMathFragments :: StructPhrase -> StmtMathFragments +structPhraseMathFragments item = + lexicalItemSgPlStmtMathFragments False termMathPlaceholderFragments item [] + +termMathPlaceholderFragments :: a -> StmtMathFragments +termMathPlaceholderFragments _ = + stmtMathProse "?" + +lexicalItemStmtMathFragments :: (a -> StmtMathFragments) -> LexicalItem -> [a] -> StmtMathFragments +lexicalItemStmtMathFragments renderArg item args = + patternStmtMathFragments renderArg (lexicalItemPhrase item) args + +lexicalItemSgPlStmtMathFragments :: Bool -> (a -> StmtMathFragments) -> LexicalItemSgPl -> [a] -> StmtMathFragments +lexicalItemSgPlStmtMathFragments isPlural renderArg item args = + patternStmtMathFragments renderArg phrase args + where + phrase = if isPlural then pl (lexicalItemSgPlPhrase item) else sg (lexicalItemSgPlPhrase item) + +patternStmtMathFragments :: (a -> StmtMathFragments) -> [Maybe Token] -> [a] -> StmtMathFragments +patternStmtMathFragments renderArg patternParts args = + joinStmtMathFragments (stmtMathProse " ") (go patternParts args) + where + go [] [] = [] + go [] (_ : _) = error "renderPatternStmtMath: too many arguments" + go (Nothing : rest) (arg : restArgs) = renderArg arg : go rest restArgs + go (Nothing : _) [] = error "renderPatternStmtMath: not enough arguments" + go (Just tok : rest) restArgs = renderStmtToken tok : go rest restArgs + + renderStmtToken :: Token -> StmtMathFragments + renderStmtToken = \case + Word w -> stmtMathProse w + tok -> stmtMathNode (renderMathToken tok) + + +renderFormulaMath :: HintMap -> Formula -> Html () +renderFormulaMath hints = \case + FormulaChain chain -> + renderChainMathRow hints chain + FormulaPredicate _loc predi marker exprs -> + renderHintedMathRow hints PredicateHint marker (toList exprs) (renderPrefixPredicateFallback predi (renderExprMath hints <$> toList exprs)) + Connected _loc conn phi psi -> do + renderFormulaMath hints phi + moText (connectiveSymbol conn) + renderFormulaMath hints psi + FormulaNeg _loc phi -> do + moText "¬" + renderFormulaMath hints phi + FormulaQuantified _loc quant vars bound phi -> do + moText (quantifierSymbol quant) + renderVarListMath vars + renderBoundMath hints vars bound + moText "." + renderFormulaMath hints phi + PropositionalConstant _loc pc -> + moText (propositionalConstantSymbol pc) + +connectiveSymbol :: Connective -> Text +connectiveSymbol = \case + Conjunction -> "∧" + Disjunction -> "∨" + Implication -> "⇒" + Equivalence -> "⇔" + ExclusiveOr -> "⊕" + NegatedDisjunction -> "↓" + +quantifierSymbol :: Quantifier -> Text +quantifierSymbol = \case + Universally -> "∀" + Existentially -> "∃" + Nonexistentially -> "∄" + +propositionalConstantSymbol :: PropositionalConstant -> Text +propositionalConstantSymbol = \case + IsBottom -> "⊥" + IsTop -> "⊤" + +renderChainMathRow :: HintMap -> Chain -> Html () +renderChainMathRow hints chain = + joinHtml (moText "∧") (renderLink <$> splatChain chain) + where + renderLink (lhs, sign, rel, rhs) = + renderRelationApplication hints sign (toList lhs) rel (toList rhs) + + splatChain :: Chain -> [(NonEmpty Expr, Sign, Relation, NonEmpty Expr)] + splatChain = \case + ChainBase es sign rel es' -> + [(es, sign, rel, es')] + ChainCons es sign rel ch'@(ChainBase es' _ _ _) -> + (es, sign, rel, es') : splatChain ch' + ChainCons es sign rel ch'@(ChainCons es' _ _ _) -> + (es, sign, rel, es') : splatChain ch' + +renderBoundMath :: HintMap -> NonEmpty VarSymbol -> Bound -> Html () +renderBoundMath hints vars = \case + Unbounded -> skip + Bounded _loc sign rel expr -> do + moText "," + renderRelationApplication hints sign (ExprVar <$> toList vars) rel [expr] + +renderRelationApplication :: HintMap -> Sign -> [Expr] -> Relation -> [Expr] -> Html () +renderRelationApplication hints sign lhs rel rhs = case (sign, rel) of + (Negative, Relation _loc symbol []) + | Just negated <- negatedRelationSymbol (relationSymbolToken symbol) -> do + renderExprListMath hints lhs + moText negated + renderExprListMath hints rhs + _ -> + applySign sign (renderRelationCore hints lhs rel rhs) + +applySign :: Sign -> Html () -> Html () +applySign sign html = case sign of + Positive -> html + Negative -> do + mo_ "¬" + html + +renderRelationCore :: HintMap -> [Expr] -> Relation -> [Expr] -> Html () +renderRelationCore hints lhs rel rhs = case rel of + Relation _loc symbol relParams -> do + renderExprListMath hints lhs + renderRelationSymbolCore hints symbol relParams + renderExprListMath hints rhs + RelationExpr _loc expr -> do + renderExprListMath hints lhs + renderExprMath hints expr + renderExprListMath hints rhs + +renderRelationSymbolCore :: HintMap -> RelationSymbol -> [Expr] -> Html () +renderRelationSymbolCore hints symbol relParams = + renderHintedMathRow + hints + RelationHint + (relationSymbolMarker symbol) + relParams + (renderRelationFallback hints symbol relParams) + +renderRelationFallback :: HintMap -> RelationSymbol -> [Expr] -> Html () +renderRelationFallback hints symbol relParams = + merror_ (renderRelationFallbackCore hints symbol relParams) + +renderRelationFallbackCore :: HintMap -> RelationSymbol -> [Expr] -> Html () +renderRelationFallbackCore hints symbol relParams + | null relParams = renderRelationToken (relationSymbolToken symbol) + | otherwise = msub_ do + renderRelationToken (relationSymbolToken symbol) + mrow_ (renderExprListMath hints relParams) + +renderRelationToken :: Token -> Html () +renderRelationToken = \case + Command "in" -> moText "∈" + Command "ni" -> moText "∋" + Command "notin" -> moText "∉" + Command "meets" -> moText "⋈" + Command "notmeets" -> moText "⋈̸" + Command "subset" -> moText "⊂" + Command "subseteq" -> moText "⊆" + Command "supset" -> moText "⊃" + Command "supseteq" -> moText "⊇" + Command "neq" -> moText "≠" + tok -> renderMathToken tok + +negatedRelationSymbol :: Token -> Maybe Text +negatedRelationSymbol = \case + Command "in" -> Just "∉" + Command "ni" -> Just "∌" + Command "subset" -> Just "⊄" + Command "subseteq" -> Just "⊈" + Command "supset" -> Just "⊅" + Command "supseteq" -> Just "⊉" + Command "meets" -> Just "⋈̸" + Symbol "=" -> Just "≠" + Symbol "<" -> Just "≮" + Symbol ">" -> Just "≯" + Symbol "≤" -> Just "≰" + Symbol "≥" -> Just "≱" + _ -> Nothing + + +renderExprMath :: HintMap -> Expr -> Html () +renderExprMath hints expr = case expr of + ExprVar var -> + renderVarMath var + ExprInteger _loc n -> + mnText (Text.pack (show n)) + ExprOp _loc item args -> + renderHintedMath hints OperatorHint (mixfixMarker item) args (renderPatternFallback (mixfixPattern item) (renderExprMath hints <$> args)) + ExprStructOp _loc symb maybeExpr -> + let marker = structMarker symb + args = maybeToList maybeExpr + in renderHintedMath hints StructOpHint marker args (renderStructFallback symb (renderExprMath hints <$> args)) + ExprFiniteSet{} -> + mrow_ (renderExprMathRow hints expr) + ExprSep{} -> + mrow_ (renderExprMathRow hints expr) + ExprReplace{} -> + mrow_ (renderExprMathRow hints expr) + ExprReplacePred{} -> + mrow_ (renderExprMathRow hints expr) + +renderExprMathRow :: HintMap -> Expr -> Html () +renderExprMathRow hints = \case + ExprVar var -> + renderVarMath var + ExprInteger _loc n -> + mnText (Text.pack (show n)) + ExprOp _loc item args -> + renderHintedMathRow hints OperatorHint (mixfixMarker item) args (renderPatternFallback (mixfixPattern item) (renderExprMath hints <$> args)) + ExprStructOp _loc symb maybeExpr -> + let marker = structMarker symb + args = maybeToList maybeExpr + in renderHintedMathRow hints StructOpHint marker args (renderStructFallback symb (renderExprMath hints <$> args)) + ExprFiniteSet _loc exprs -> + renderFiniteSetMath hints (toList exprs) + ExprSep _loc var bound stmt -> do + moText "{" + renderVarMath var + moText "∈" + renderExprMathRow hints bound + moText "|" + renderStmtMath hints stmt + moText "}" + ExprReplace _loc expr bounds maybeStmt -> do + moText "{" + renderExprMathRow hints expr + moText "|" + renderReplaceBoundsMath hints (toList bounds) + for_ maybeStmt \stmt -> do + moText "|" + renderStmtMath hints stmt + moText "}" + ExprReplacePred _loc rangeVar domVar domExpr stmt -> do + moText "{" + renderVarMath rangeVar + moText "|" + moText "∃" + renderVarMath domVar + moText "∈" + renderExprMathRow hints domExpr + moText "." + renderStmtMath hints stmt + moText "}" + +renderReplaceBoundsMath :: HintMap -> [(VarSymbol, Expr)] -> Html () +renderReplaceBoundsMath hints = + joinHtml (moText ",") . fmap renderBound + where + renderBound (var, expr) = do + renderVarMath var + moText "∈" + renderExprMathRow hints expr + +renderExprListMath :: HintMap -> [Expr] -> Html () +renderExprListMath hints = + joinHtml (moText ",") . fmap (renderExprMath hints) + +renderFiniteSetMath :: HintMap -> [Expr] -> Html () +renderFiniteSetMath hints exprs = + do + moText "{" + renderExprListMath hints exprs + moText "}" + +renderHintedMath :: HintMap -> HintCategory -> Marker -> [Expr] -> Html () -> Html () +renderHintedMath hints category marker args fallback = + case Map.lookup (category, marker, length args) hints of + Nothing -> + fallback + Just RenderHint{..} + | renderHintArity /= length args -> + error ("Render hint arity mismatch for " <> show category <> " " <> show marker <> ": expected " <> show renderHintArity <> ", got " <> show (length args)) + | otherwise -> + renderTemplateAsNode renderHintTemplate + where + renderedArgs = renderExprMath hints <$> args + + renderTemplateAsNode :: [TemplatePiece] -> Html () + renderTemplateAsNode = \case + [piece] -> + renderPiece piece + pieces -> + mrow_ (traverse_ renderPiece pieces) + + renderPiece :: TemplatePiece -> Html () + renderPiece = \case + Literal text -> toHtmlRaw text + Slot ix -> case nth (ix - 1) renderedArgs of + Just html -> html + Nothing -> error ("Render hint slot out of bounds for " <> show marker <> ": <x" <> show ix <> "/>") + +renderHintedMathRow :: HintMap -> HintCategory -> Marker -> [Expr] -> Html () -> Html () +renderHintedMathRow hints category marker args fallback = + case Map.lookup (category, marker, length args) hints of + Nothing -> + fallback + Just RenderHint{..} + | renderHintArity /= length args -> + error ("Render hint arity mismatch for " <> show category <> " " <> show marker <> ": expected " <> show renderHintArity <> ", got " <> show (length args)) + | otherwise -> + traverse_ renderPiece renderHintTemplate + where + renderedArgs = renderExprMath hints <$> args + + renderPiece :: TemplatePiece -> Html () + renderPiece = \case + Literal text -> toHtmlRaw text + Slot ix -> case nth (ix - 1) renderedArgs of + Just html -> html + Nothing -> error ("Render hint slot out of bounds for " <> show marker <> ": <x" <> show ix <> "/>") + +renderPatternFallback :: Pattern -> [Html ()] -> Html () +renderPatternFallback patternParts renderedArgs = + merror_ (renderPatternMath patternParts renderedArgs) + +renderPatternMath :: Pattern -> [Html ()] -> Html () +renderPatternMath patternParts renderedArgs = + traverse_ id (go patternParts renderedArgs) + where + go End [] = [] + go End (_ : _) = error "renderPatternMath: too many arguments" + go (HoleCons rest) (arg : args) = arg : go rest args + go (HoleCons _) [] = error "renderPatternMath: not enough arguments" + go (TokenCons tok rest) args = renderMathToken tok : go rest args + +renderPrefixPredicateFallback :: PrefixPredicate -> [Html ()] -> Html () +renderPrefixPredicateFallback (PrefixPredicate command _arity) renderedArgs = + merror_ do + miText command + when (not (null renderedArgs)) do + moText "(" + joinHtml (moText ",") renderedArgs + moText ")" + +renderStructFallback :: StructSymbol -> [Html ()] -> Html () +renderStructFallback symb renderedArgs = + merror_ do + renderStructSymbolName symb + when (not (null renderedArgs)) do + moText "(" + joinHtml (moText ",") renderedArgs + moText ")" + +renderStructSymbolName :: StructSymbol -> Html () +renderStructSymbolName (StructSymbol name) = miText name + +structMarker :: StructSymbol -> Marker +structMarker (StructSymbol name) = Marker name + +renderMathToken :: Token -> Html () +renderMathToken = \case + Word w -> miText w + Variable v -> renderNamedVariableMath v + Symbol s -> moText s + Integer n -> mnText (Text.pack (show n)) + Command cmd -> miText cmd + Label m -> mtextText ("label:" <> m) + Ref ms -> mtextText ("ref:" <> Text.intercalate "," (toList ms)) + BeginEnv env -> mtextText ("begin:" <> env) + EndEnv env -> mtextText ("end:" <> env) + ParenL -> moText "(" + ParenR -> moText ")" + BracketL -> moText "[" + BracketR -> moText "]" + VisibleBraceL -> moText "{" + VisibleBraceR -> moText "}" + InvisibleBraceL -> moText "(" + InvisibleBraceR -> moText ")" + + +inlineMath :: Html () -> Html () +inlineMath inner = math_ inner + +blockMath :: Html () -> Html () +blockMath inner = math_ [displayblock_] inner + +renderVarInline :: VarSymbol -> Html () +renderVarInline = inlineMath . renderVarMath + +renderVarMath :: VarSymbol -> Html () +renderVarMath = \case + NamedVarAt _loc name -> + renderNamedVariableMath name + FreshVarAt _loc n -> + miText ("_" <> Text.pack (show n)) + +renderNamedVariableMath :: Text -> Html () +renderNamedVariableMath rawName = + case displayVariable rawName of + VariableDisplay baseText Nothing -> + miText baseText + VariableDisplay baseText (Just (VariableTicks tickCount)) -> + msup_ do + miText baseText + renderPrimeSuperscript tickCount + VariableDisplay baseText (Just (VariableSubscript subscriptText)) -> + msub_ do + miText baseText + renderVariableSubscriptMath subscriptText + +renderPrimeSuperscript :: Int -> Html () +renderPrimeSuperscript tickCount + | tickCount <= 1 = + moText "′" + | otherwise = + mrow_ (foldMap (const (moText "′")) [1 .. tickCount]) + +renderVariableSubscriptMath :: Text -> Html () +renderVariableSubscriptMath subscriptText + | Text.all isDigit subscriptText = + mnText subscriptText + | otherwise = + miText subscriptText + +renderVarEqInline :: HintMap -> VarSymbol -> Expr -> Html () +renderVarEqInline hints var expr = + inlineMath do + renderVarMath var + moText "=" + renderExprMathRow hints expr + +renderFunctionCallInline :: VarSymbol -> VarSymbol -> Html () +renderFunctionCallInline fun arg = + inlineMath (renderFunctionCallMath fun arg) + +renderFunctionEqInline :: HintMap -> VarSymbol -> VarSymbol -> Expr -> Html () +renderFunctionEqInline hints fun arg expr = + inlineMath do + renderFunctionCallMath fun arg + moText "=" + renderExprMathRow hints expr + +renderFunctionCallMath :: VarSymbol -> VarSymbol -> Html () +renderFunctionCallMath fun arg = do + renderVarMath fun + moText "(" + renderVarMath arg + moText ")" + +renderVarListInline :: NonEmpty VarSymbol -> Html () +renderVarListInline vars = + inlineMath (renderVarListMath vars) + +renderVarListMath :: NonEmpty VarSymbol -> Html () +renderVarListMath vars = + joinHtml (moText ",") (renderVarMath <$> toList vars) + +renderBoundInline :: HintMap -> NonEmpty VarSymbol -> Bound -> Html () +renderBoundInline hints vars = \case + Unbounded -> skip + bound -> do + toHtml (" with " :: Text) + inlineMath (renderBoundPhraseMath hints vars bound) + +renderBoundSubjectInline :: HintMap -> NonEmpty VarSymbol -> Bound -> Html () +renderBoundSubjectInline hints vars = \case + Unbounded -> + renderVarListInline vars + bound -> + inlineMath (renderBoundSubjectMath hints vars bound) + +renderBoundPhraseMath :: HintMap -> NonEmpty VarSymbol -> Bound -> Html () +renderBoundPhraseMath hints vars = \case + Unbounded -> mrow_ skip + Bounded _loc sign rel expr -> + renderRelationApplication hints sign (ExprVar <$> toList vars) rel [expr] + +renderBoundSubjectMath :: HintMap -> NonEmpty VarSymbol -> Bound -> Html () +renderBoundSubjectMath hints vars = \case + Unbounded -> + renderVarListMath vars + Bounded _loc sign rel expr -> + renderRelationApplication hints sign (ExprVar <$> toList vars) rel [expr] + +boundSubjectMathFragments :: HintMap -> NonEmpty VarSymbol -> Bound -> StmtMathFragments +boundSubjectMathFragments hints vars = \case + Unbounded -> + stmtMathNode (renderVarListMath vars) + bound -> + stmtMathNode (renderBoundSubjectMath hints vars bound) + +renderSymbolPatternInline :: HintMap -> SymbolPattern -> Html () +renderSymbolPatternInline hints = + inlineMath . renderSymbolPatternMath hints + +renderSymbolPatternMath :: HintMap -> SymbolPattern -> Html () +renderSymbolPatternMath hints (SymbolPattern symbol vars) = + renderHintedMathRow hints OperatorHint (mixfixMarker symbol) (ExprVar <$> vars) (renderPatternFallback (mixfixPattern symbol) (renderVarMath <$> vars)) + +renderJustification :: ReferenceContext -> Justification -> Html () +renderJustification references = \case + JustificationRef markers -> do + toHtml ("by " :: Text) + renderMarkerReferences references (toList markers) + JustificationSetExt -> + toHtml ("by set extensionality" :: Text) + JustificationEmpty -> + skip + JustificationLocal -> + toHtml ("by local assumptions" :: Text) + +renderJustificationSuffix :: ReferenceContext -> Justification -> Html () +renderJustificationSuffix _ JustificationEmpty = skip +renderJustificationSuffix references justification = do + toHtml (" " :: Text) + renderJustification references justification + +renderMarkerReferences :: ReferenceContext -> [Marker] -> Html () +renderMarkerReferences references markers + | length markers >= referenceGroupThreshold = + renderMarkerReferenceGroup references markers + | otherwise = + joinHtml (toHtml (", " :: Text)) (renderMarkerReference references <$> markers) + +renderMarkerReferenceGroup :: ReferenceContext -> [Marker] -> Html () +renderMarkerReferenceGroup references markers = + span_ groupAttributes do + toHtml ("[...]" :: Text) + span_ [class_ "reference-preview-group-items", makeAttributes "hidden" "hidden"] do + traverse_ (renderMarkerReferenceGroupItem references) markers + where + referenceCountLabel = Text.pack (show (length markers)) <> " references" + + groupAttributes = + [ class_ "ref-badge has-preview ref-badge-group" + , makeAttributes "data-preview-group" "true" + , makeAttributes "data-reference-label" referenceCountLabel + , makeAttributes "aria-describedby" "reference-preview-popup" + , makeAttributes "tabindex" "0" + , makeAttributes "role" "button" + , makeAttributes "aria-label" ("Show " <> referenceCountLabel) + ] + +renderMarkerReferenceGroupItem :: ReferenceContext -> Marker -> Html () +renderMarkerReferenceGroupItem ReferenceContext{..} marker = + span_ itemAttributes skip + where + label = markerText marker + baseAttributes = + [ class_ "reference-preview-group-item" + , makeAttributes "data-reference-label" label + ] + + itemAttributes = + baseAttributes <> case Map.lookup marker referenceAnchors of + Just anchor -> + [ makeAttributes + "data-preview-link" + (renderUrlFragment anchor) + , makeAttributes "data-preview-target-id" anchor + ] + Nothing -> + case Map.lookup marker referencePreviews of + Nothing -> + [] + Just preview -> + [ makeAttributes + "data-preview-link" + (previewReferenceHref preview) + , makeAttributes "data-preview-id" (previewId preview) + ] + +renderMarkerReference :: ReferenceContext -> Marker -> Html () +renderMarkerReference ReferenceContext{..} marker = + case Map.lookup marker referenceAnchors of + Just anchor -> + a_ + ( href_ (renderUrlFragment anchor) + : referenceAttributes + (Just (currentPreviewAttributes anchor)) + ) + (toHtml label) + Nothing -> + case Map.lookup marker referencePreviews of + Nothing -> + span_ (referenceAttributes Nothing) (toHtml label) + Just preview -> + a_ + ( href_ (previewReferenceHref preview) + : referenceAttributes (Just (importedPreviewAttributes preview)) + ) + (toHtml label) + where + label = markerText marker + + referenceAttributes preview = + [ class_ (if hasPreview preview then "ref-badge has-preview" else "ref-badge") + , makeAttributes "data-reference-label" label + ] + <> foldMap id preview + + hasPreview = + \case + Nothing -> False + Just _ -> True + + currentPreviewAttributes anchor = + [ makeAttributes "data-preview-target-id" anchor + , makeAttributes "aria-describedby" "reference-preview-popup" + ] + + importedPreviewAttributes entry = + [ makeAttributes "data-preview-id" (previewId entry) + , makeAttributes "aria-describedby" "reference-preview-popup" + ] + + +markerText :: Marker -> Text +markerText (Marker text) = text + +tokenTextHtml :: Token -> Html () +tokenTextHtml = toHtml . tokToText + +joinHtml :: Html () -> [Html ()] -> Html () +joinHtml _ [] = mempty +joinHtml separator (x : xs) = x <> foldMap (separator <>) xs + +miText :: Text -> Html () +miText = mi_ . toHtml + +moText :: Text -> Html () +moText = mo_ . toHtml + +mnText :: Text -> Html () +mnText = mn_ . toHtml + +mtextText :: Text -> Html () +mtextText = mtext_ . toHtml |