Migrate to `Felix` namespaceHEADhotg

1 files changed, 225 insertions, 0 deletions

diff --git a/source/Felix/Test/Unit/Html.hs b/source/Felix/Test/Unit/Html.hs
new file mode 100644
index 0000000..c8395ec
--- /dev/null
+++ b/source/Felix/Test/Unit/Html.hs
@@ -0,0 +1,225 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Felix.Test.Unit.Html (unitTests) where
+
+import Base
+import Felix.Parse qualified as Parse
+import Felix.Source
+import Felix.Source.Graph
+import Felix.Workspace qualified as Workspace
+import Felix.Render.Html qualified as Html
+import Felix.Render.Html.Context
+import Felix.Render.Html.Layout
+import Felix.Report.Location (Location, pattern Nowhere)
+import Felix.Syntax.Abstract
+
+import Data.Text qualified as Text
+import Data.Text.IO qualified as TextIO
+import Data.List.NonEmpty qualified as NonEmpty
+import System.Directory qualified as Directory
+import Test.Tasty
+import Test.Tasty.HUnit
+
+unitTests :: TestTree
+unitTests = testGroup "HTML renderer"
+    [ testCase "one shared index resolves local and cross-page previews" referencePreviews
+    , testCase "missing reference preview data falls back to readable text" missingReferenceFallback
+    , testCase "datatype rendering omits unchecked derived facts" datatypeDerivedFactsAreOmitted
+    ]
+
+referencePreviews :: Assertion
+referencePreviews = do
+    environment <- expectRight =<< Workspace.prepareDefaultWorkspaceEnvironment
+    graph <-
+        expectRight =<<
+            Workspace.prepareDefaultSourceGraph
+                "test/html-fixtures/root-preview.tex"
+    workspace <-
+        expectRight =<< Parse.parseResolvedSourceGraph graph
+    hints <- TextIO.readFile "library/lexicon.tsv"
+    layout <-
+        expectRight
+            (layoutHtmlSourceGraph
+                (Workspace.workspaceHtmlMountPrefixes environment)
+                graph)
+    let nodes = Parse.parsedWorkspaceImportedBeforeImporter workspace
+        sourceBlocks =
+            (\node ->
+                ( Parse.parsedModuleResolved node
+                , Parse.parsedModuleBlocks node
+                ))
+                <$> nodes
+        (renderIndex, pages) =
+            Html.buildRenderIndex sourceBlocks
+        rootPage = NonEmpty.last pages
+    context <-
+        expectRight
+            (htmlRenderContext
+                layout
+                (Html.htmlPagePresentationSource rootPage))
+    html <-
+        expectRight
+            (Html.renderDocument
+                context
+                hints
+                renderIndex
+                rootPage)
+    let supportScript = Html.supportScriptAssetContents
+    assertContains "local references keep page anchors" "href=\"#local_prop\"" html
+    assertContains "local references point previews at the visible target block" "data-reference-label=\"local_prop\" data-preview-target-id=\"local_prop\"" html
+    assertNotContains "local references do not use hidden preview ids" "data-reference-label=\"local_prop\" data-preview-id=\"" html
+    assertContains "visible target blocks expose preview metadata" "id=\"local_prop\" data-preview-kind=\"Proposition\" data-preview-label=\"local_prop\"" html
+    assertContains "imported references get preview metadata" "data-reference-label=\"imported_prop\"" html
+    assertContains "imported references link to their relative encoded theory route" "href=\"imported-preview#imported_prop\"" html
+    assertContains "imported references still use hidden preview templates" "data-reference-label=\"imported_prop\" data-preview-id=\"reference-preview-" html
+    assertNotContains "imported references do not get broken page anchors" "href=\"#imported_prop\"" html
+    assertNotContains "imported references are not non-clickable spans" "<span class=\"ref-badge has-preview\" data-reference-label=\"imported_prop\"" html
+    assertCount "hidden preview store only contains the imported fixture preview" 1 "class=\"reference-preview-template\"" html
+    assertContains "page grid is scoped to an explicit shell" "class=\"page-layout\"" html
+    assertNotContains "page grid does not apply to every body div" "body > div" html
+    assertContains "page heading uses the selected mounted source" "<h1>project:test/html-fixtures/root-preview.tex</h1>" html
+    assertContains "imported preview records its mounted source" "project:test/html-fixtures/imported-preview.tex" html
+    assertContains "imported preview source links to the same route" "href=\"imported-preview\"><code>project:test/html-fixtures/imported-preview.tex</code>" html
+    assertContains "imported source renders on its own line" "class=\"reference-preview-source\"" html
+    assertContains "multi-reference rendering preserves the comma separator" ", <a href=\"imported-preview#imported_prop\" class=\"ref-badge has-preview\" data-reference-label=\"imported_prop\"" html
+    assertContains "calculation justifications also use target previews" "Step 2: by <a href=\"#local_prop\" class=\"ref-badge has-preview\" data-reference-label=\"local_prop\" data-preview-target-id=\"local_prop\"" html
+    assertContains "large reference lists collapse to an ellipsis trigger" "Follows by <span class=\"ref-badge has-preview ref-badge-group\" data-preview-group=\"true\" data-reference-label=\"5 references\"" html
+    assertContains "collapsed references keep current-page item metadata" "data-reference-label=\"group_source\" data-preview-link=\"#group_source\" data-preview-target-id=\"group_source\"" html
+    assertContains "collapsed references keep imported item metadata" "data-reference-label=\"imported_prop\" data-preview-link=\"imported-preview#imported_prop\" data-preview-id=\"reference-preview-" html
+    assertNotContains "collapsed references do not inline the long list" "Follows by <a href=\"#local_prop\" class=\"ref-badge has-preview\" data-reference-label=\"local_prop\" data-preview-target-id=\"local_prop\" aria-describedby=\"reference-preview-popup\">local_prop</a>, <a href=\"#uses_refs\"" html
+    assertContains "collapsed tooltips compose full preview templates" "const preview = cloneHiddenPreview(item) || buildCurrentPreview(item) || buildMissingPreview(item);" supportScript
+    assertContains "collapsed tooltip labels become links" "template.append(linkGroupHeading(item, preview));" supportScript
+    assertContains "collapsed tooltip labels use generated reference links" "link.href = href;" supportScript
+    assertContains "collapsed tooltip heading links have hover affordance" ".reference-preview-heading a:hover," html
+    assertContains "collapsed tooltips use stacked preview sections" "className = 'reference-preview-group-template'" supportScript
+    assertContains "visible preview popup accepts pointer interaction" "pointer-events: auto;" html
+    assertContains "preview popup uses a wider bounded layout" "width: 44rem;" html
+    assertContains "preview popup uses a taller bounded layout" "max-height: min(34rem, calc(100vh - 2rem));" html
+    assertContains "behavior loads from the shared external script asset" "src=\"../../_static/naproche-html.js\"" html
+    assertNotContains "inline script bundles are not emitted" "<script type=\"text/javascript\">" html
+    assertContains "preview popup cancels delayed hide on pointer entry" "popup.addEventListener('pointerenter', clearHideTimer);" supportScript
+    assertContains "preview popup schedules delayed hide on pointer exit" "popup.addEventListener('pointerleave', scheduleHide);" supportScript
+    assertContains "group click pins the preview popup" "showPreview(trigger, event, true);" supportScript
+    assertContains "group keyboard activation pins the preview popup" "showPreview(trigger, null, true);" supportScript
+    assertContains "preview statements use a full-width paragraph" "class=\"reference-preview-statement\"" html
+    assertContains "preview popup is emitted once" "id=\"reference-preview-popup\"" html
+
+missingReferenceFallback :: Assertion
+missingReferenceFallback = do
+    let proof = Qed (Just Nowhere) (JustificationRef ("missing_ref" :| []))
+        blocks = [BlockProof Nowhere proof Nowhere]
+    html <- renderSynthetic blocks
+    assertContains "missing references remain visible" "missing_ref" html
+    assertNotContains "missing references do not claim preview content" "data-preview-id=" html
+
+datatypeDerivedFactsAreOmitted :: Assertion
+datatypeDerivedFactsAreOmitted = do
+    let blocks =
+            [ propformDatatypeBlock Nowhere
+            , referenceClaimBlock "uses_datatype_fact"
+            , referenceProofBlock "propform_induct"
+            ]
+    html <- renderSynthetic blocks
+    assertContains "datatype declarations remain visible" "Datatype of " html
+    assertContains "derived fact references remain readable" "propform_induct" html
+    assertNotContains "unchecked datatype facts are not rendered" "<summary>Derived facts</summary>" html
+    assertNotContains "unchecked datatype facts do not become preview targets" "data-preview-label=\"propform_induct\"" html
+
+renderSynthetic :: [Block] -> IO Text
+renderSynthetic blocks = do
+    currentDirectory <- Directory.getCurrentDirectory
+    mounts <-
+        expectRight =<<
+            prepareSourceMounts
+                [(sourceMountId "project", currentDirectory)]
+    request <-
+        expectRight
+            (searchedRoot "test/html-fixtures/root-preview.tex")
+    graph <-
+        expectRight =<<
+            buildResolvedSourceGraph mounts request
+    layout <-
+        expectRight
+            (layoutHtmlSourceGraph
+                [(sourceMountId "project", [])]
+                graph)
+    context <-
+        expectRight
+            (htmlRenderContext
+                layout
+                (sourceGraphRootSource graph))
+    let (renderIndex, page :| _remainingPages) =
+            Html.buildRenderIndex
+                ((sourceGraphRootSource graph, blocks) :| [])
+    expectRight
+        (Html.renderDocument
+            context
+            ""
+            renderIndex
+            page)
+
+expectRight :: (Show e, HasCallStack) => Either e a -> IO a
+expectRight = \case
+    Left err ->
+        assertFailure ("expected Right, got Left " <> show err)
+    Right value ->
+        pure value
+
+propformDatatypeBlock :: Location -> Block
+propformDatatypeBlock blockLoc =
+    BlockData blockLoc Nothing "propform" propformDatatype
+
+propformDatatype :: Datatype
+propformDatatype =
+    Datatype
+        { datatypeHeadExpr = ExprOp Nowhere (constSymbol "propform") []
+        , datatypeClauses =
+            DatatypeClause (ExprOp Nowhere (constSymbol "propbot") []) (ExprOp Nowhere (constSymbol "propform") []) [] :|
+                [ DatatypeClause (ExprOp Nowhere (unarySymbol "propvar") [ExprVar "n"]) (ExprOp Nowhere (constSymbol "propform") []) [("n", ExprOp Nowhere (constSymbol "naturals") [])]
+                , DatatypeClause
+                    (ExprOp Nowhere (infixSymbol "propto") [ExprVar "p", ExprVar "q"])
+                    (ExprOp Nowhere (constSymbol "propform") [])
+                    [ ("p", ExprOp Nowhere (constSymbol "propform") [])
+                    , ("q", ExprOp Nowhere (constSymbol "propform") [])
+                    ]
+                ]
+        }
+
+referenceClaimBlock :: Marker -> Block
+referenceClaimBlock marker =
+    BlockClaim Proposition Nowhere Nothing marker (Claim [] (StmtFormula (PropositionalConstant Nowhere IsTop)))
+
+referenceProofBlock :: Marker -> Block
+referenceProofBlock marker =
+    BlockProof Nowhere (Qed (Just Nowhere) (JustificationRef (marker :| []))) Nowhere
+
+constSymbol :: Text -> FunctionSymbol
+constSymbol name =
+    mkMixfixItem [Just (Command name)] (Marker name) NonAssoc
+
+unarySymbol :: Text -> FunctionSymbol
+unarySymbol name =
+    mkMixfixItem [Just (Command name), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] (Marker name) NonAssoc
+
+infixSymbol :: Text -> FunctionSymbol
+infixSymbol name =
+    mkMixfixItem [Nothing, Just (Command name), Nothing] (Marker name) NonAssoc
+
+assertContains :: HasCallStack => String -> Text -> Text -> Assertion
+assertContains label needle haystack =
+    assertBool
+        (label <> "\nExpected to find: " <> Text.unpack needle)
+        (needle `Text.isInfixOf` haystack)
+
+assertNotContains :: HasCallStack => String -> Text -> Text -> Assertion
+assertNotContains label needle haystack =
+    assertBool
+        (label <> "\nDid not expect to find: " <> Text.unpack needle)
+        (not (needle `Text.isInfixOf` haystack))
+
+assertCount :: HasCallStack => String -> Int -> Text -> Text -> Assertion
+assertCount label expected needle haystack =
+    assertEqual
+        (label <> "\nExpected count for: " <> Text.unpack needle)
+        expected
+        (Text.count needle haystack)