FormatSpec.hs

{-|
Module      : FormatterSpec
Description : Tests related to the formatter module
-}
{-# LANGUAGE OverloadedStrings #-}
module Rzk.FormatSpec where

import qualified Data.Text.IO as T
import           Test.Hspec

import           Rzk.Format   (format, formatDocument, isWellFormatted)

formatsTo :: FilePath -> FilePath -> Expectation
formatsTo beforePath afterPath = do
  beforeSrc <- T.readFile ("test/files/" ++ beforePath)
  afterSrc <- T.readFile ("test/files/" ++ afterPath)
  format beforeSrc `shouldBe` afterSrc
  isWellFormatted afterSrc `shouldBe` True -- idempotency

formats :: FilePath -> Expectation
formats path = (path ++ "-bad.rzk") `formatsTo` (path ++ "-good.rzk")


spec :: Spec
spec = do
  describe "Formatter" $ do
    it "Puts definition assumptions, conclusion, and construction on separate lines" $ do
      -- formats "definition-structure"
      pendingWith "Doesn't currently place assumptions on a new line"

    it "Replaces common ASCII sequences with their unicode equivalent" $ do
      formats "unicode"

    it "Formats Rzk blocks in Literate Rzk Markdown" $ do
      "literate-bad.rzk.md" `formatsTo` "literate-good.rzk.md"

    it "Preserves comments" $ do
      formats "comments"

    it "Moves trailing binary operators to next line (except lambda arrow)" $ do
      formats "bin-ops"

    it "Keeps both canonical #data layouts (inline and multi-line)" $ do
      formats "data-decl"

    it "Adds relevant spaces to structure constructions like a tree" $ do
      formats "tree-structure"

    it "Aligns colons in split context with parameter name (issue #215)" $ do
      formats "context-colon-align"

    it "Inserts newline after =_{ ... }" $ do
      formats "identity-type-eq-brace"

    it "Doesn't fail on empty inputs" $ do
      formats "empty"

    it "Normalizes tabs to spaces" $ do
      formats "tabs"

    it "Let bindings formatting differs from defenitions" $ do
      formats "let"

    it "Spaces the match-branch arrow and converts it to unicode, keeping it at line ends" $ do
      formats "match"

    it "Fixes indentation" pending

    it "Wraps long lines" pending

  -- The language server replaces the whole document, and used to send it with
  -- every trailing newline stripped: saving deleted the file's final newline,
  -- which then failed the .editorconfig and Prettier checks that sHoTT's CI
  -- runs, with no formatting able to satisfy both.
  describe "formatDocument" $ do
    it "Keeps the final newline" $ do
      formatDocument "#lang rzk-1\n" `shouldBe` "#lang rzk-1\n"

    it "Keeps a document that ends without a newline as it was" $ do
      formatDocument "#lang rzk-1" `shouldBe` "#lang rzk-1"

    it "Keeps the trailing blank lines the source had" $ do
      formatDocument "#lang rzk-1\n\n\n" `shouldBe` "#lang rzk-1\n\n\n"

    it "Is idempotent on the final newline" $ do
      let src = "#lang rzk-1\n\n#define id (A : U)\n  : A → A\n  := \\ x → x\n"
      formatDocument src `shouldBe` src