phino-0.0.0.55: test/LaTeXSpec.hs

-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
-- SPDX-License-Identifier: MIT

{- | Tests for the LaTeX module that provides conversion of phi-calculus
programs and rules to LaTeX format for academic documents.
Attention! Most of the tests are generated by LLM. Consider that when refactoring
-}
module LaTeXSpec where

import AST
import Control.Monad (forM_)
import LaTeX (LatexContext (..), defaultLatexContext, explainRules, meetInProgram, programToLaTeX, rewrittensToLatex)
import LaTeX qualified as L
import Lining (LineFormat (MULTILINE, SINGLELINE))
import Parser (parseExpressionThrows, parseProgramThrows)
import Sugar (SugarType (SALTY, SWEET))
import Test.Hspec (Spec, describe, it, shouldBe, shouldContain, shouldNotContain)
import Yaml qualified as Y

spec :: Spec
spec = do
  describe "meet program in program" $
    forM_
      [ ("Q.x.y", "{Q.x.y}", "{[[ x -> Q.x.y ]]}", ["Q.x.y"])
      , ("Q.x.y twice", "{Q.x.y}", "{[[ x -> Q.x.y, y -> Q.x.y.z ]]}", ["Q.x.y", "Q.x.y"])
      , ("Q.x.y.z.a and Q.x.y", "{Q.x.y.z.a}", "{[[ x -> Q.x.y, y -> Q.x.y.z ]]}", ["Q.x.y.z", "Q.x.y", "Q.x.y"])
      , ("Ignore data objects", "{[[ x -> \"foo\" ]]}", "{Q.x( y -> \"foo\" )}", [])
      , ("Not found [[ t -> 42 ]]", "{⟦ ex ↦ ⟦ x ↦ ⟦ t ↦ 42 ⟧.t ⟧.x ⟧}", "{⟦ ex ↦ ⟦ x ↦ 42 ⟧.x ⟧}", [])
      , ("Missed [[ t -> 42 ]]", "{⟦ ex ↦ ⟦ x ↦ ⟦ t ↦ 42 ⟧.t ⟧.x ⟧}", "{⟦ ex ↦ 42 ⟧}", [])
      ]
      ( \(desc, first, second, exprs) -> it desc $ do
          ptn <- parseProgramThrows first
          tgt <- parseProgramThrows second
          res <- traverse parseExpressionThrows exprs
          meetInProgram ptn tgt `shouldBe` res
      )

  describe "programToLaTeX with nonumber=True" $
    it "uses phiquation* environment" $ do
      prog <- parseProgramThrows "{Q}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "\\begin{phiquation*}"

  describe "programToLaTeX with nonumber=False" $
    it "uses phiquation environment" $ do
      prog <- parseProgramThrows "{Q}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = False}
          result = programToLaTeX prog ctx
      result `shouldContain` "\\begin{phiquation}"

  describe "programToLaTeX output structure" $
    it "contains begin and end tags" $ do
      prog <- parseProgramThrows "{Q}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "\\end{phiquation*}"

  describe "programToLaTeX with SWEET sugar" $
    it "renders sweet syntax with braces" $ do
      prog <- parseProgramThrows "{Q}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "\\Big\\{"

  describe "programToLaTeX with SALTY sugar" $
    it "renders salty syntax with arrow" $ do
      prog <- parseProgramThrows "{Q}"
      let ctx = defaultLatexContext{sugar = SALTY, line = SINGLELINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "->"

  describe "programToLaTeX with MULTILINE format" $
    it "renders multiline format" $ do
      prog <- parseProgramThrows "{[[ x -> Q ]]}"
      let ctx = defaultLatexContext{line = MULTILINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "|x|"

  describe "rewrittensToLatex with empty list" $
    it "generates valid latex structure" $ do
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = rewrittensToLatex [] ctx
      result `shouldContain` "\\begin{phiquation*}"

  describe "rewrittensToLatex with single program" $
    it "renders single program without rule" $ do
      prog <- parseProgramThrows "{Q}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = rewrittensToLatex [(prog, Nothing)] ctx
      result `shouldContain` "\\Big\\{"

  describe "rewrittensToLatex with rule name" $
    it "includes nameref for rule" $ do
      prog <- parseProgramThrows "{Q}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = rewrittensToLatex [(prog, Just "myrule")] ctx
      result `shouldContain` "\\nameref{r:myrule}"

  describe "rewrittensToLatex with label" $
    it "includes label command" $ do
      prog <- parseProgramThrows "{Q}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True, label = Just "myeq"}
          result = rewrittensToLatex [(prog, Nothing)] ctx
      result `shouldContain` "\\label{myeq}"

  describe "rewrittensToLatex without label" $
    it "excludes label command" $ do
      prog <- parseProgramThrows "{Q}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = rewrittensToLatex [(prog, Nothing)] ctx
      result `shouldNotContain` "\\label"

  describe "rewrittensToLatex with expression" $
    it "includes phiExpression command" $ do
      prog <- parseProgramThrows "{Q}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True, expression = Just "myexpr"}
          result = rewrittensToLatex [(prog, Nothing)] ctx
      result `shouldContain` "\\phiExpression{myexpr}"

  describe "rewrittensToLatex without expression" $
    it "excludes phiExpression command" $ do
      prog <- parseProgramThrows "{Q}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = rewrittensToLatex [(prog, Nothing)] ctx
      result `shouldNotContain` "\\phiExpression"

  describe "rewrittensToLatex with multiple programs" $
    it "joins with leadsto" $ do
      prog1 <- parseProgramThrows "{Q.x}"
      prog2 <- parseProgramThrows "{Q.y}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = rewrittensToLatex [(prog1, Nothing), (prog2, Nothing)] ctx
      result `shouldContain` "\\leadsto"

  describe "rewrittensToLatex ends with period" $
    it "adds period before end tag" $ do
      prog <- parseProgramThrows "{Q}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = rewrittensToLatex [(prog, Nothing)] ctx
      result `shouldContain` ".\n\\end"

  describe "rewrittensToLatex with nonumber=False" $
    it "uses phiquation without asterisk" $ do
      prog <- parseProgramThrows "{Q}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = False}
          result = rewrittensToLatex [(prog, Nothing)] ctx
      result `shouldContain` "\\begin{phiquation}"

  describe "escapeUnprintedChars escapes dollar" $
    it "replaces $ with char36 in label via AST" $ do
      let prog = Program (ExFormation [BiTau (AtLabel "$my") ExGlobal])
          ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "\\char36{}"

  describe "escapeUnprintedChars escapes at sign" $
    it "replaces @ with char64 in label via AST" $ do
      let prog = Program (ExFormation [BiTau (AtLabel "@my") ExGlobal])
          ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "\\char64{}"

  describe "escapeUnprintedChars escapes caret" $
    it "replaces ^ with char94 in label via AST" $ do
      let prog = Program (ExFormation [BiTau (AtLabel "^my") ExGlobal])
          ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "\\char94{}"

  describe "escapeUnprintedChars escapes underscore" $
    it "replaces _ in label with char95" $ do
      prog <- parseProgramThrows "{Q.my_label}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "\\char95{}"

  describe "escapeUnprintedChars preserves regular chars" $
    it "keeps alphanumeric chars unchanged" $ do
      prog <- parseProgramThrows "{Q.abc123}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "abc123"

  describe "explainRules with empty list" $
    it "generates document structure" $ do
      let result = explainRules []
      result `shouldContain` "\\documentclass{article}"

  describe "explainRules document has amsmath" $
    it "includes amsmath package" $ do
      let result = explainRules []
      result `shouldContain` "\\usepackage{amsmath}"

  describe "explainRules document structure" $
    it "has begin and end document" $ do
      let result = explainRules []
      result `shouldContain` "\\begin{document}"

  describe "explainRules document ends correctly" $
    it "has end document tag" $ do
      let result = explainRules []
      result `shouldContain` "\\end{document}"

  describe "explainRules with named rule" $
    it "includes rule name" $ do
      let rule = Y.Rule (Just "DOT") Nothing ExGlobal ExGlobal Nothing Nothing Nothing
          result = explainRules [rule]
      result `shouldContain` "\\rule{DOT}"

  describe "explainRules with unnamed rule" $
    it "uses unnamed as fallback" $ do
      let rule = Y.Rule Nothing Nothing ExGlobal ExGlobal Nothing Nothing Nothing
          result = explainRules [rule]
      result `shouldContain` "\\rule{unnamed}"

  describe "explainRules with multiple rules" $
    it "includes all rule names" $ do
      let rule1 = Y.Rule (Just "RULE1") Nothing ExGlobal ExGlobal Nothing Nothing Nothing
          rule2 = Y.Rule (Just "RULE2") Nothing ExGlobal ExGlobal Nothing Nothing Nothing
          result = explainRules [rule1, rule2]
      result `shouldContain` "\\rule{RULE1}"

  describe "explainRules with multiple rules second" $
    it "includes second rule name" $ do
      let rule1 = Y.Rule (Just "FIRST") Nothing ExGlobal ExGlobal Nothing Nothing Nothing
          rule2 = Y.Rule (Just "SECOND") Nothing ExGlobal ExGlobal Nothing Nothing Nothing
          result = explainRules [rule1, rule2]
      result `shouldContain` "\\rule{SECOND}"

  describe "LatexContext sugar field" $
    it "stores sugar type correctly" $ do
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = False}
      sugar ctx `shouldBe` SWEET

  describe "LatexContext line field" $
    it "stores line format correctly" $ do
      let ctx = defaultLatexContext{line = MULTILINE, nonumber = True}
      line ctx `shouldBe` MULTILINE

  describe "LatexContext nonumber field" $
    it "stores nonumber flag correctly" $ do
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = False}
      nonumber ctx `shouldBe` False

  describe "LatexContext expression field" $
    it "stores expression correctly" $ do
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True, expression = Just "expr"}
      L.expression ctx `shouldBe` Just "expr"

  describe "LatexContext label field" $
    it "stores label correctly" $ do
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True, label = Just "lbl"}
      L.label ctx `shouldBe` Just "lbl"

  describe "programToLaTeX handles formation" $
    it "renders formation with bindings" $ do
      prog <- parseProgramThrows "{[[ x -> Q, y -> $ ]]}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "|x|"

  describe "programToLaTeX handles dispatch" $
    it "renders dispatch expression" $ do
      prog <- parseProgramThrows "{Q.x.y.z}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "|z|"

  describe "programToLaTeX handles application" $
    it "renders application expression" $ do
      prog <- parseProgramThrows "{Q.f(x -> Q)}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "|f|"

  describe "programToLaTeX handles void binding" $
    it "renders void in formation" $ do
      prog <- parseProgramThrows "{[[ x -> ? ]]}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "|x|"

  describe "programToLaTeX handles nested formations" $
    it "renders nested structures" $ do
      prog <- parseProgramThrows "{[[ x -> [[ y -> Q ]] ]]}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = programToLaTeX prog ctx
      result `shouldContain` "|y|"

  describe "rewrittensToLatex with label and expression" $
    it "includes both label and expression" $ do
      prog <- parseProgramThrows "{Q}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True, expression = Just "expr", label = Just "lbl"}
          result = rewrittensToLatex [(prog, Nothing)] ctx
      result `shouldContain` "\\label{lbl}"

  describe "rewrittensToLatex with complex rewrite chain" $
    it "shows rewrite sequence" $ do
      prog1 <- parseProgramThrows "{Q.x}"
      prog2 <- parseProgramThrows "{Q.y}"
      prog3 <- parseProgramThrows "{Q.z}"
      let ctx = defaultLatexContext{line = SINGLELINE, nonumber = True}
          result = rewrittensToLatex [(prog1, Just "r1"), (prog2, Just "r2"), (prog3, Nothing)] ctx
      result `shouldContain` "\\nameref{r:r1}"