Suppress unchecked datatype fact previews

HTML currently has only raw datatype syntax, while checked facts may use canonical domains. Omit derived facts until checked semantic context reaches the renderer.

2 files changed, 11 insertions, 292 deletions

diff --git a/source/Render/Html.hs b/source/Render/Html.hs
index 71f1668..1c3bcda 100644
--- a/source/Render/Html.hs
+++ b/source/Render/Html.hs
@@ -341,24 +341,16 @@ pageStyles = Text.unlines
     , "proof- > details > :not(summary) {"
     , "  margin-top: 0.5rem;"
     , "}"
-    , "datatype- > details,"
     , "inductive- > details {"
     , "  margin-top: 0.75rem;"
     , "}"
-    , "datatype- > details > summary,"
     , "inductive- > details > summary {"
     , "  cursor: pointer;"
     , "  font-weight: 700;"
     , "}"
-    , "datatype- > details > :not(summary),"
     , "inductive- > details > :not(summary) {"
     , "  margin-top: 0.5rem;"
     , "}"
-    , ".datatype-derived-facts {"
-    , "  margin: 0;"
-    , "  padding-left: 1.5rem;"
-    , "}"
-    , ".datatype-derived-facts > li,"
     , ".inductive-derived-facts > li {"
     , "  margin: 0.35rem 0;"
     , "}"
@@ -366,9 +358,6 @@ pageStyles = Text.unlines
     , "  margin: 0;"
     , "  padding-left: 1.5rem;"
     , "}"
-    , ".datatype-derived-facts > li {"
-    , "  margin: 0.35rem 0;"
-    , "}"
     , ".reference-preview-store {"
     , "  display: none;"
     , "}"
@@ -1847,14 +1836,7 @@ renderDatatype hints Datatype{..} = do
     toHtml ("." :: Text)
     ul_ do
         traverse_ renderDatatypeClause (toList datatypeClauses)
-    case datatypeDerivedFacts (Datatype{..}) of
-        [] ->
-            skip
-        derivedFacts ->
-            details_ do
-                summary_ (toHtml ("Derived facts" :: Text))
-                ul_ [class_ "datatype-derived-facts"] do
-                    traverse_ (renderDatatypeDerivedFact hints) derivedFacts
+    -- Derived facts require checked semantic context.
     where
         renderDatatypeClause :: DatatypeClause -> Html ()
         renderDatatypeClause DatatypeClause{..} = li_ do
@@ -1872,217 +1854,6 @@ renderDatatype hints Datatype{..} = do
         renderDatatypePremise (x, domain) =
             inlineMath (renderRelationApplication hints Positive [ExprVar x] (Relation Nowhere ElementSymbol []) [domain])
 
-renderDatatypeDerivedFact :: HintMap -> DatatypeDerivedFact -> Html ()
-renderDatatypeDerivedFact hints DatatypeDerivedFact{datatypeDerivedFactMarker, datatypeDerivedFactFormula} =
-    li_ (id_ (markerText datatypeDerivedFactMarker) : previewTargetAttributes "Datatype Fact" (Just datatypeDerivedFactMarker) Nothing) do
-        term "head-" do
-            code_ (toHtml (markerText datatypeDerivedFactMarker))
-            toHtml (": " :: Text)
-        inlineMath (renderFormulaMath hints datatypeDerivedFactFormula)
-        toHtml ("." :: Text)
-
-data DatatypeDerivedFact = DatatypeDerivedFact
-    { datatypeDerivedFactMarker :: Marker
-    , datatypeDerivedFactFormula :: Formula
-    }
-
-data DatatypeRenderInfo = DatatypeRenderInfo
-    { datatypeFactBaseText :: Text
-    , datatypeCarrierExpr :: Expr
-    , datatypeRenderClauses :: NonEmpty DatatypeRenderClause
-    }
-
-data DatatypeRenderClause = DatatypeRenderClause
-    { datatypeRenderClauseSymbolText :: Text
-    , datatypeRenderClauseExpr :: Expr
-    , datatypeRenderClauseArgs :: [VarSymbol]
-    , datatypeRenderClausePremises :: [(VarSymbol, Expr)]
-    }
-
-datatypeDerivedFacts :: Datatype -> [DatatypeDerivedFact]
-datatypeDerivedFacts datatype = case datatypeRenderInfo datatype of
-    Nothing ->
-        []
-    Just info ->
-        datatypeIntroFacts info
-            <> datatypeDistinctFacts info
-            <> datatypeInjectiveFacts info
-            <> [ DatatypeDerivedFact (datatypeCasesMarker info) (datatypeCasesFormula info)
-               , DatatypeDerivedFact (datatypeInductMarker info) (datatypeInductFormula info)
-               ]
-
-datatypeRenderInfo :: Datatype -> Maybe DatatypeRenderInfo
-datatypeRenderInfo Datatype{datatypeHeadExpr, datatypeClauses} = do
-    datatypeFactBaseText <- datatypeFactBase datatypeHeadExpr
-    datatypeRenderClauses <- traverse datatypeRenderClause datatypeClauses
-    pure DatatypeRenderInfo{datatypeFactBaseText, datatypeCarrierExpr = datatypeHeadExpr, datatypeRenderClauses}
-
-datatypeRenderClause :: DatatypeClause -> Maybe DatatypeRenderClause
-datatypeRenderClause DatatypeClause{datatypeClauseConstructorExpr, datatypeClausePremises} = do
-    (constructorSymbol, constructorArgs) <- exprOp datatypeClauseConstructorExpr
-    datatypeRenderClauseArgs <- traverse exprVar constructorArgs
-    let datatypeRenderClauseSymbolText = markerText (mixfixMarker constructorSymbol)
-    pure DatatypeRenderClause
-        { datatypeRenderClauseSymbolText
-        , datatypeRenderClauseExpr = datatypeClauseConstructorExpr
-        , datatypeRenderClauseArgs
-        , datatypeRenderClausePremises = datatypeClausePremises
-        }
-
-datatypeIntroFacts :: DatatypeRenderInfo -> [DatatypeDerivedFact]
-datatypeIntroFacts info =
-    [ DatatypeDerivedFact (datatypeIntroMarker info clause) (datatypeIntroFormula info clause)
-    | clause <- NonEmpty.toList (datatypeRenderClauses info)
-    ]
-
-datatypeDistinctFacts :: DatatypeRenderInfo -> [DatatypeDerivedFact]
-datatypeDistinctFacts info =
-    [ DatatypeDerivedFact (datatypeDistinctMarker info leftClause rightClause) (datatypeDistinctFormula leftClause rightClause)
-    | (leftClause, rightClause) <- unorderedPairs (NonEmpty.toList (datatypeRenderClauses info))
-    ]
-
-datatypeInjectiveFacts :: DatatypeRenderInfo -> [DatatypeDerivedFact]
-datatypeInjectiveFacts info =
-    [ DatatypeDerivedFact (datatypeInjectiveMarker info clause) (datatypeInjectiveFormula clause)
-    | clause <- NonEmpty.toList (datatypeRenderClauses info)
-    , not (null (datatypeRenderClauseArgs clause))
-    ]
-
-datatypeIntroMarker :: DatatypeRenderInfo -> DatatypeRenderClause -> Marker
-datatypeIntroMarker info clause =
-    Marker (datatypeFactBaseText info <> "_" <> datatypeRenderClauseSymbolText clause <> "_intro")
-
-datatypeDistinctMarker :: DatatypeRenderInfo -> DatatypeRenderClause -> DatatypeRenderClause -> Marker
-datatypeDistinctMarker info leftClause rightClause =
-    Marker
-        ( datatypeFactBaseText info
-            <> "_"
-            <> datatypeRenderClauseSymbolText leftClause
-            <> "_"
-            <> datatypeRenderClauseSymbolText rightClause
-            <> "_distinct"
-        )
-
-datatypeInjectiveMarker :: DatatypeRenderInfo -> DatatypeRenderClause -> Marker
-datatypeInjectiveMarker info clause =
-    Marker (datatypeFactBaseText info <> "_" <> datatypeRenderClauseSymbolText clause <> "_injective")
-
-datatypeCasesMarker :: DatatypeRenderInfo -> Marker
-datatypeCasesMarker info =
-    Marker (datatypeFactBaseText info <> "_cases")
-
-datatypeInductMarker :: DatatypeRenderInfo -> Marker
-datatypeInductMarker info =
-    Marker (datatypeFactBaseText info <> "_induct")
-
-datatypeFactBase :: Expr -> Maybe Text
-datatypeFactBase expr = do
-    (datatypeSymbol, datatypeArgs) <- exprOp expr
-    guard (null datatypeArgs)
-    pure (markerText (mixfixMarker datatypeSymbol))
-
-datatypeIntroFormula :: DatatypeRenderInfo -> DatatypeRenderClause -> Formula
-datatypeIntroFormula info clause =
-    forallIfNeeded premiseVars (impliesFrom premiseFormulas conclusion)
-    where
-        premiseVars = datatypeClausePremiseVars clause
-        premiseFormulas = datatypeClausePremiseFormulas clause
-        conclusion = elementOfFormula (datatypeRenderClauseExpr clause) (datatypeCarrierExpr info)
-
-datatypeDistinctFormula :: DatatypeRenderClause -> DatatypeRenderClause -> Formula
-datatypeDistinctFormula leftClause rightClause =
-    forallIfNeeded (leftVars <> rightVars) (notEqualsFormula (datatypeRenderClauseExpr leftClause) rightTerm)
-    where
-        leftVars = datatypeRenderClauseArgs leftClause
-        rightVars = renameDatatypeVars (Set.fromList leftVars) (datatypeRenderClauseArgs rightClause)
-        rightTerm = substituteExpr (Map.fromList (zip (datatypeRenderClauseArgs rightClause) (ExprVar <$> rightVars))) (datatypeRenderClauseExpr rightClause)
-
-datatypeInjectiveFormula :: DatatypeRenderClause -> Formula
-datatypeInjectiveFormula clause =
-    forallIfNeeded (leftVars <> rightVars) (impliesFormula (equalsFormula leftTerm rightTerm) (formulaConjunction equalities))
-    where
-        leftVars = datatypeRenderClauseArgs clause
-        rightVars = renameDatatypeVars (Set.fromList leftVars) leftVars
-        leftTerm = datatypeRenderClauseExpr clause
-        rightTerm = substituteExpr (Map.fromList (zip leftVars (ExprVar <$> rightVars))) leftTerm
-        equalities =
-            zipWith (\leftVar rightVar -> equalsFormula (ExprVar leftVar) (ExprVar rightVar)) leftVars rightVars
-
-datatypeCasesFormula :: DatatypeRenderInfo -> Formula
-datatypeCasesFormula info =
-    forallIfNeeded [witnessVar] (impliesFormula (elementOfFormula (ExprVar witnessVar) (datatypeCarrierExpr info)) (formulaDisjunction disjuncts))
-    where
-        usedVars = datatypeUsedVars info
-        witnessVar = freshDatatypeVar usedVars "x"
-        disjuncts = datatypeCaseDisjunct witnessVar <$> NonEmpty.toList (datatypeRenderClauses info)
-        datatypeCaseDisjunct x clause =
-            existsIfNeeded premiseVars (formulaConjunction (premises <> [equalsFormula (ExprVar x) (datatypeRenderClauseExpr clause)]))
-            where
-                premiseVars = datatypeClausePremiseVars clause
-                premises = datatypeClausePremiseFormulas clause
-
-datatypeInductFormula :: DatatypeRenderInfo -> Formula
-datatypeInductFormula info =
-    forallIfNeeded [subsetVar] (impliesFrom closureAssumptions conclusion)
-    where
-        usedVars = datatypeUsedVars info
-        subsetVar = freshDatatypeVar usedVars "S"
-        witnessVar = freshDatatypeVar (Set.insert subsetVar usedVars) "x"
-        conclusion =
-            forallIfNeeded [witnessVar]
-                (impliesFormula
-                    (elementOfFormula (ExprVar witnessVar) (datatypeCarrierExpr info))
-                    (elementOfFormula (ExprVar witnessVar) (ExprVar subsetVar))
-                )
-        closureAssumptions = datatypeInductionClosure info subsetVar <$> NonEmpty.toList (datatypeRenderClauses info)
-
-datatypeInductionClosure :: DatatypeRenderInfo -> VarSymbol -> DatatypeRenderClause -> Formula
-datatypeInductionClosure info subsetVar clause =
-    forallIfNeeded premiseVars (impliesFrom inductionPremises conclusion)
-    where
-        premiseVars = datatypeClausePremiseVars clause
-        inductionPremises = datatypeInductionPremise info subsetVar <$> datatypeRenderClausePremises clause
-        conclusion = elementOfFormula (datatypeRenderClauseExpr clause) (ExprVar subsetVar)
-
-datatypeInductionPremise :: DatatypeRenderInfo -> VarSymbol -> (VarSymbol, Expr) -> Formula
-datatypeInductionPremise info subsetVar (x, domain)
-    | sameDatatypeCarrier domain (datatypeCarrierExpr info) =
-        elementOfFormula (ExprVar x) (ExprVar subsetVar)
-    | otherwise =
-        elementOfFormula (ExprVar x) domain
-
-datatypeClausePremiseVars :: DatatypeRenderClause -> [VarSymbol]
-datatypeClausePremiseVars DatatypeRenderClause{datatypeRenderClausePremises} =
-    fst <$> datatypeRenderClausePremises
-
-datatypeClausePremiseFormulas :: DatatypeRenderClause -> [Formula]
-datatypeClausePremiseFormulas DatatypeRenderClause{datatypeRenderClausePremises} =
-    [ elementOfFormula (ExprVar x) domain
-    | (x, domain) <- datatypeRenderClausePremises
-    ]
-
-datatypeUsedVars :: DatatypeRenderInfo -> Set VarSymbol
-datatypeUsedVars info =
-    Set.fromList
-        [ var
-        | clause <- NonEmpty.toList (datatypeRenderClauses info)
-        , var <- datatypeRenderClauseArgs clause <> datatypeClausePremiseVars clause
-        ]
-
-sameDatatypeCarrier :: Expr -> Expr -> Bool
-sameDatatypeCarrier left right = case (exprOp left, exprOp right) of
-    (Just (leftSymbol, []), Just (rightSymbol, [])) ->
-        leftSymbol == rightSymbol
-    _ ->
-        False
-
-exprOp :: Expr -> Maybe (MixfixItem, [Expr])
-exprOp = \case
-    ExprOp _loc symbol args ->
-        Just (symbol, args)
-    _ ->
-        Nothing
-
 exprVar :: Expr -> Maybe VarSymbol
 exprVar = \case
     ExprVar x ->
@@ -2126,10 +1897,6 @@ equalsFormula :: Expr -> Expr -> Formula
 equalsFormula left right =
     FormulaChain (ChainBase (left :| []) Positive (Relation Nowhere EqSymbol []) (right :| []))
 
-notEqualsFormula :: Expr -> Expr -> Formula
-notEqualsFormula left right =
-    FormulaChain (ChainBase (left :| []) Positive (Relation Nowhere NeqSymbol []) (right :| []))
-
 impliesFormula :: Formula -> Formula -> Formula
 impliesFormula left right =
     Connected Nowhere Implication left right
@@ -2162,24 +1929,6 @@ impliesFrom :: [Formula] -> Formula -> Formula
 impliesFrom [] conclusion = conclusion
 impliesFrom premises conclusion = impliesFormula (formulaConjunction premises) conclusion
 
-unorderedPairs :: [a] -> [(a, a)]
-unorderedPairs = \case
-    [] -> []
-    x : xs -> [(x, y) | y <- xs] <> unorderedPairs xs
-
-renameDatatypeVars :: Set VarSymbol -> [VarSymbol] -> [VarSymbol]
-renameDatatypeVars _ [] = []
-renameDatatypeVars used (x:xs) =
-    let x' = freshDatatypeLikeVar used x
-    in x' : renameDatatypeVars (Set.insert x' used) xs
-
-freshDatatypeLikeVar :: Set VarSymbol -> VarSymbol -> VarSymbol
-freshDatatypeLikeVar used = \case
-    NamedVar name ->
-        freshDatatypeVar used (name <> "_rhs")
-    FreshVar n ->
-        freshDatatypeVar used ("_" <> Text.pack (show n) <> "_rhs")
-
 freshDatatypeVar :: Set VarSymbol -> Text -> VarSymbol
 freshDatatypeVar used base =
     List.head
@@ -2722,7 +2471,7 @@ blockLocationOf = \case
 
 referenceTargetsOfBlockRenderInfo :: BlockRenderInfo -> [ReferenceTarget]
 referenceTargetsOfBlockRenderInfo (_index, block, blockId) =
-    maybeToList blockTarget <> datatypeTargets <> inductiveTargets
+    maybeToList blockTarget <> inductiveTargets
     where
         sourceFile = locFile (blockLocationOf block)
 
@@ -2737,21 +2486,6 @@ referenceTargetsOfBlockRenderInfo (_index, block, blockId) =
                 , targetBody = \hints -> renderPreviewBlockBody hints block
                 }
 
-        datatypeTargets = case block of
-            BlockData _loc _title _marker datatype ->
-                [ ReferenceTarget
-                    { targetMarker = datatypeDerivedFactMarker
-                    , targetAnchorId = markerText datatypeDerivedFactMarker
-                    , targetKind = "Datatype Fact"
-                    , targetTitle = Nothing
-                    , targetSourceFile = sourceFile
-                    , targetBody = \hints -> previewStatement (inlineMath (renderFormulaMath hints datatypeDerivedFactFormula))
-                    }
-                | DatatypeDerivedFact{datatypeDerivedFactMarker, datatypeDerivedFactFormula} <- datatypeDerivedFacts datatype
-                ]
-            _ ->
-                []
-
         inductiveTargets = case block of
             BlockInductive _loc _title marker inductive ->
                 [ ReferenceTarget
diff --git a/source/Test/Unit/Html.hs b/source/Test/Unit/Html.hs
index e379c77..8b91f23 100644
--- a/source/Test/Unit/Html.hs
+++ b/source/Test/Unit/Html.hs
@@ -18,8 +18,7 @@ unitTests = testGroup "HTML renderer"
     , testCase "imported references inherit the page route namespace" libraryPrefixedImportedRoutes
     , testCase "nested library pages load the shared script asset relatively" nestedLibraryScriptAsset
     , testCase "missing reference preview data falls back to readable text" missingReferenceFallback
-    , testCase "datatype derived facts render as collapsed local reference targets" datatypeDerivedFactTargets
-    , testCase "imported datatype derived facts get hidden preview templates" importedDatatypeDerivedFactPreviews
+    , testCase "datatype rendering omits unchecked derived facts" datatypeDerivedFactsAreOmitted
     ]
 
 referencePreviews :: Assertion
@@ -87,32 +86,18 @@ missingReferenceFallback = do
     assertContains "missing references remain visible" "missing_ref" html
     assertNotContains "missing references do not claim preview content" "data-preview-id=" html
 
-datatypeDerivedFactTargets :: Assertion
-datatypeDerivedFactTargets = do
+datatypeDerivedFactsAreOmitted :: Assertion
+datatypeDerivedFactsAreOmitted = do
     let blocks =
             [ propformDatatypeBlock Nowhere
-            , referenceClaimBlock "uses_local_datatype_fact"
-            , referenceProofBlock "propform_propbot_intro"
+            , referenceClaimBlock "uses_datatype_fact"
+            , referenceProofBlock "propform_induct"
             ]
         html = Html.renderDocument "synthetic.tex" "" blocks []
-    assertContains "datatype blocks render derived facts inside a details element" "<summary>Derived facts</summary>" html
-    assertContains "local datatype fact refs keep page anchors" "href=\"#propform_propbot_intro\"" html
-    assertContains "local datatype fact refs point previews at the derived fact target" "data-reference-label=\"propform_propbot_intro\" data-preview-target-id=\"propform_propbot_intro\"" html
-    assertContains "derived fact targets expose preview metadata" "id=\"propform_propbot_intro\" data-preview-kind=\"Datatype Fact\" data-preview-label=\"propform_propbot_intro\"" html
-    assertContains "local hash navigation opens collapsed ancestors before scrolling" "revealTarget(target);" Html.supportScriptAssetContents
-
-importedDatatypeDerivedFactPreviews :: Assertion
-importedDatatypeDerivedFactPreviews = do
-    importedLoc <- fileLocation "test/html-fixtures/imported-datatype.tex"
-    let rootBlocks =
-            [ referenceClaimBlock "uses_imported_datatype_fact"
-            , referenceProofBlock "propform_propbot_intro"
-            ]
-        html = Html.renderDocument "test/html-fixtures/root-datatype.tex" "" rootBlocks [propformDatatypeBlock importedLoc]
-    assertContains "imported datatype fact refs link to the imported theory route" "href=\"/test/html-fixtures/imported-datatype#propform_propbot_intro\"" html
-    assertContains "imported datatype fact refs use hidden preview ids" "data-reference-label=\"propform_propbot_intro\" data-preview-id=\"reference-preview-" html
-    assertContains "imported datatype fact previews identify their kind" "Datatype Fact <code>propform_propbot_intro</code>" html
-    assertContains "imported datatype fact previews record their source file" "test/html-fixtures/imported-datatype.tex" html
+    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
 
 fileLocation :: FilePath -> IO Location
 fileLocation path = do