cornelis-0.2.0.0: test/TestSpec.hs

{-# LANGUAGE NumDecimals       #-}
{-# LANGUAGE OverloadedStrings #-}

module TestSpec where

import           Control.Concurrent (threadDelay)
import           Control.Monad (void)
import           Cornelis.Subscripts (decNextDigitSeq, incNextDigitSeq)
import           Cornelis.Types
import           Cornelis.Types.Agda (Rewrite (..))
import           Cornelis.Utils (withBufferStuff)
import           Cornelis.Vim
import qualified Data.Text as T
import qualified Data.Vector as V
import           Neovim (liftIO)
import           Neovim.API.Text
import           Neovim.Test
import           Plugin
import           Test.Hspec
import           Utils


broken :: String -> SpecWith a -> SpecWith a
broken = before_ . pendingWith

spec :: Spec
spec = focus $ do
  let timeout = Seconds 60
  diffSpec "should refine" timeout "test/Hello.agda"
      [ Swap "unit = ?" "unit = one"] $ \w _ -> do
    goto w 11 8
    refine

  broken "Times out in CI for unknown reasons" $ diffSpec "should support helper functions" timeout "test/Hello.agda"
      [ Swap "" "help_me : Unit"] $ \w _ -> do
    goto w 11 8
    helperFunc Normalised "help_me"
    liftIO $ threadDelay 5e5
    void $ vim_command "normal! G\"\"p"

  diffSpec "should case split (unicode lambda)" timeout "test/Hello.agda"
      [ Add                       "slap = λ { true → {! !}"
      , Swap "slap = λ { x → ? }" "         ; false → {! !} }"
      ] $ \w _ -> do
    goto w 20 16
    caseSplit "x"

  diffSpec "should preserve indents when doing case split" timeout "test/Hello.agda"
      [ Add                       "  testIndent true = {! !}"
      , Swap "  testIndent b = ?" "  testIndent false = {! !}"
      ] $ \w _ -> do
    goto w 24 18
    caseSplit "b"

  diffSpec "should refine with hints" timeout "test/Hello.agda"
      [ Swap "isEven∘ (suc n) = {! isEven∘ !}" "isEven∘ (suc n) = isEven∘ {! !}"] $ \w _ -> do
    goto w 28 24
    refine

  let case_split_test name row col =
        diffSpec ("should case split (" <> T.unpack name <> ")") timeout "test/Hello.agda"
            (fmap (fmap (name <>))
              [ Add           " true = {! !}"
              , Swap " x = ?" " false = {! !}"
              ]
            ) $ \w _ -> do
          goto w row col
          caseSplit "x"

  case_split_test "test" 14 10

  case_split_test "unicodeTest₁" 17 18

  vimSpec "should support why in scope" timeout "test/Hello.agda" $ \_ b -> do
    withBufferStuff b $ \bs -> do
      whyInScope "zero"
      liftIO $ threadDelay 5e5
      res <- buffer_get_lines (iw_buffer $ bs_info_win bs) vimFirstLine vimLastLine False
      liftIO $ V.toList res `shouldContain` ["zero is in scope as"]

  vimSpec "should support goto definition across modules"
          timeout "test/Hello.agda" $ \w _ -> do
    goto w 2 18
    gotoDefinition
    liftIO $ threadDelay 5e5
    b' <- nvim_get_current_buf
    res <- buffer_get_lines b' vimFirstLine vimLastLine False
    liftIO $ V.toList res `shouldContain` ["module Agda.Builtin.Nat where"]

  diffSpec "work with multiple" timeout "test/Hello.agda"
      [ Add                  "copattern true = {! !}"
      , Swap "copattern = ?" "copattern false = {! !}"
      ] $ \w _ -> do
    goto w 31 13
    caseSplit ""
    liftIO $ threadDelay 5e5
    goto w 31 15
    liftIO $ threadDelay 5e5
    caseSplit "x"

  diffSpec "work with ? in names" timeout "test/Hello.agda"
      [ Swap "foo? ?f = {! !}" "foo? ?f x = {! !}"
      ] $ \w _ -> do
    goto w 34 13
    caseSplit ""

  diffSpec "question to meta" timeout "test/Hello.agda"
       [ Swap "unit = ?" "unit = {! !}"
       , Swap "test x = ?" "test x = {! !}"
       , Swap "unicodeTest\8321 x = ?" "unicodeTest\8321 x = {! !}"
       , Swap "slap = \955 { x \8594 ? }" "slap = \955 { x \8594 {! !} }"
       , Swap "  testIndent b = ?" "  testIndent b = {! !}"
       , Swap "copattern = ?" "copattern = {! !}"
       ] $ \_ b -> do
    questionToMeta b

  diffSpec "give" timeout "test/Hello.agda"
        [ Swap "give = {! true !}" "give = true"
        ] $ \w _ -> do
    goto w 37 11
    give

  let elaborate_test rw changes row column =
        let title = maybe "default mode" show rw in
        diffSpec ("elaborate (" <> title <> ")") timeout "test/Hello.agda" changes $
            \w _ -> do
                goto w row column
                withNormalizationMode rw elaborate

  elaborate_test (Just "AsIs")
    [Swap "elaborate = {! 3 !}" "elaborate = 3"]
    40 16

  diffSpec "should dec subscripts" timeout "test/Hello.agda"
      [ Swap "sub₀and-super⁹ : Nat" "sub₋₁and-super⁹ : Nat"] $ \w _ -> do
    goto w 42 1
    decNextDigitSeq

  diffSpec "should inc subscripts" timeout "test/Hello.agda"
      [ Swap "sub₀and-super⁹ : Nat" "sub₁and-super⁹ : Nat"] $ \w _ -> do
    goto w 42 1
    incNextDigitSeq

  diffSpec "should dec superscripts" timeout "test/Hello.agda"
      [ Swap "sub₀and-super⁹ : Nat" "sub₀and-super⁸ : Nat"] $ \w _ -> do
    goto w 42 6
    decNextDigitSeq

  diffSpec "should inc superscripts" timeout "test/Hello.agda"
      [ Swap "sub₀and-super⁹ : Nat" "sub₀and-super¹⁰ : Nat"] $ \w _ -> do
    goto w 42 6
    incNextDigitSeq

  diffSpec "should dec digits" timeout "test/Hello.agda"
      [ Swap "sub₀and-super⁹ = 15" "sub₀and-super⁹ = 14"] $ \w _ -> do
    goto w 43 16
    decNextDigitSeq

  diffSpec "should inc digits" timeout "test/Hello.agda"
      [ Swap "sub₀and-super⁹ = 15" "sub₀and-super⁹ = 16"] $ \w _ -> do
    goto w 43 16
    incNextDigitSeq

  vimSpec "should infer type of local variable" timeout "test/Hello.agda" $ \w b -> do
    withBufferStuff b $ \bs -> do
        goto w 46 14
        inferType AsIs
        liftIO $ threadDelay 5e5
        res <- buffer_get_lines (iw_buffer $ bs_info_win bs) vimFirstLine vimLastLine False
        liftIO $ V.toList res `shouldContain` ["Inferred Type: Bool"]