Declutter infoview tests.

lua/tests/helpers.lua

@@ -1,4 +1,5 @@
 local assert = require('luassert')
+local infoview = require('lean.infoview')
 
 local lean = require('lean')
 
@@ -95,9 +96,6 @@ function helpers.wait_for_line_diagnostics()
   assert.message("Waited for line diagnostics but none came.").True(succeeded)
 end
 
---- The number of current windows.
-function helpers.get_num_wins() return #vim.api.nvim_list_wins() end
-
 --- Assert about the entire buffer contents.
 local function has_buf_contents(_, arguments)
   local buf = table.concat(vim.api.nvim_buf_get_lines(0, 0, -1, false), '\n')
@@ -116,11 +114,226 @@ local function has_all(_, arguments)
   return true
 end
 
+--- The number of current windows.
+function helpers.get_num_wins() return #vim.api.nvim_list_wins() end
+
+local last_wins = {}
+local last_win = nil
+local last_win_max = -1
+
+local function get_wins()
+  local wins = {}
+  for _, win in pairs(vim.api.nvim_list_wins()) do
+    wins[win] = true
+  end
+
+  return wins
+end
+
+local function update_wins(_, arguments)
+  -- inductive hypothesis: last_wins is accurate to immediately before creating/closing any of the given windows
+  local expected_wins = vim.deepcopy(last_wins)
+
+  local opened_wins = arguments[1] or {}
+  local closed_wins = arguments[2] or {}
+
+  -- for ensuring no collisions
+  local opened_win_set = {}
+
+  for _, opened_win in pairs(opened_wins) do
+    -- should be an actual window
+    assert.is_truthy(vim.api.nvim_win_is_valid(opened_win))
+
+    -- should be brand new
+    assert.is_truthy(opened_win > last_win_max)
+    assert.is_falsy(opened_win_set[opened_win])
+
+    expected_wins[opened_win] = true
+    opened_win_set[opened_win] = true
+  end
+
+  for _, closed_win in pairs(closed_wins) do
+    -- should not be a window
+    assert.is_falsy(vim.api.nvim_win_is_valid(closed_win))
+
+    -- should have previously existed (should not pass a random previously/never closed window)
+    assert.is_truthy(expected_wins[closed_win])
+
+    expected_wins[closed_win] = nil
+  end
+
+  assert.message("expected: " .. vim.inspect(expected_wins) .. "\n got: " .. vim.inspect(get_wins())).is_truthy(
+    vim.deep_equal(expected_wins, get_wins()))
+
+  for _, opened_win in pairs(opened_wins) do
+    if opened_win > last_win_max then last_win_max = opened_win end
+  end
+
+  -- maintain IH
+  last_wins = get_wins()
+
+  -- also maintain IH for closed_win
+  last_win = vim.api.nvim_get_current_win()
+
+  return true
+end
+
+local function created_win(_, arguments)
+  local new_wins = arguments[1]
+  if new_wins then
+    assert.update_wins(arguments[1], nil)
+  else
+    assert.changed_win()
+    assert.update_wins({vim.api.nvim_get_current_win()}, nil)
+  end
+
+  return true
+end
+
+local function closed_win(_, arguments)
+  local closed_wins = arguments[1]
+  if closed_wins then
+    assert.update_wins(nil, arguments[1])
+  else
+    -- inductive hypothesis: in addition to that of update_wins,
+    -- last_win must be the window we were in immediately before closing
+    assert.changed_win()
+    assert.update_wins(nil, {last_win})
+  end
+
+  return true
+end
+
+local function changed_win(_, _)
+  -- no nested assertion to allow for negation
+  return last_win ~= vim.api.nvim_get_current_win()
+end
+
+
+local function opened_infoview(_, arguments)
+  local this_info = arguments[1]
+
+  assert.is_truthy(this_info.is_open)
+  assert.is_truthy(this_info.bufnr)
+  assert.is_truthy(this_info.window)
+  assert.is_falsy(this_info.prev_buf)
+  assert.is_falsy(this_info.prev_win)
+
+  return true
+end
+
+local function opened_infoview_kept(_, arguments)
+  local this_info = arguments[1]
+
+  assert.is_truthy(this_info.is_open)
+  assert.is_truthy(this_info.bufnr)
+  assert.is_truthy(this_info.window)
+  assert.is_truthy(this_info.bufnr == this_info.prev_buf)
+  assert.is_truthy(this_info.window == this_info.prev_win)
+
+  return true
+end
+
+local function closed_infoview(_, arguments)
+  local this_info = arguments[1]
+
+  assert.is_falsy(this_info.is_open)
+  assert.is_falsy(this_info.bufnr)
+  assert.is_falsy(this_info.window)
+  assert.is_truthy(this_info.prev_buf)
+  assert.is_truthy(this_info.prev_win)
+
+  return true
+end
+
+local function closed_infoview_kept(_, arguments)
+  local this_info = arguments[1]
+
+  assert.is_falsy(this_info.is_open)
+  assert.is_falsy(this_info.bufnr)
+  assert.is_falsy(this_info.window)
+  assert.is_falsy(this_info.prev_buf)
+  assert.is_falsy(this_info.prev_win)
+
+  return true
+end
+
+local function infoview_check(list)
+  local opened_wins = {}
+  local closed_wins = {}
+
+  for _, id in pairs(vim.api.nvim_list_tabpages()) do
+    local check = list[id]
+
+    local this_info = infoview._by_id[id]
+
+    -- infer check
+    if not check then
+      if this_info.prev_check == "opened" then
+        check = "opened_kept"
+      elseif this_info.prev_check == "opened_kept" then
+        check = "opened_kept"
+      elseif this_info.prev_check == "closed" then
+        check = "closed_kept"
+      elseif this_info.prev_check == "closed_kept" then
+        check = "closed_kept"
+      end
+    end
+
+    if check == "opened" then
+      vim.list_extend(opened_wins, {this_info.window})
+      assert.opened_infoview_state(this_info)
+    elseif check == "opened_kept" then
+      assert.opened_infoview_kept_state(this_info)
+    elseif check == "closed" then
+      vim.list_extend(closed_wins, {this_info.prev_win})
+      assert.closed_infoview_state(this_info)
+    elseif check == "closed_kept" then
+      assert.closed_infoview_kept_state(this_info)
+    end
+
+    this_info.prev_buf = this_info.bufnr
+    this_info.prev_win = this_info.window
+    this_info.prev_check = check
+  end
+
+  assert.update_wins(opened_wins, closed_wins)
+
+  return true
+end
+
 assert:register("assertion", "has_all", has_all)
-assert:register(
-  "assertion",
-  "open_infoview",
-  function() return require('lean.infoview').get_current_infoview().is_open end
-)
+assert:register("assertion", "updated_infoviews", function(_, arguments)
+  return infoview_check(arguments[1] or {})
+end)
+assert:register("assertion", "opened_infoview", function(_, arguments)
+  return infoview_check(arguments[1] or {[vim.api.nvim_win_get_tabpage(0)] = "opened"})
+end)
+assert:register("assertion", "opened_infoview_kept", function(_, arguments)
+  return infoview_check(arguments[1] or {[vim.api.nvim_win_get_tabpage(0)] = "opened_kept"})
+end)
+assert:register("assertion", "closed_infoview", function(_, arguments)
+  return infoview_check(arguments[1] or {[vim.api.nvim_win_get_tabpage(0)] = "closed"})
+end)
+assert:register("assertion", "closed_infoview_kept", function(_, arguments)
+  return infoview_check(arguments[1] or {[vim.api.nvim_win_get_tabpage(0)] = "closed_kept"})
+end)
+assert:register("assertion", "unopened_infoview", function(_, arguments)
+  return infoview_check(arguments[1] or {[vim.api.nvim_win_get_tabpage(0)] = "closed_kept"})
+end)
+
+-- internal state checks
+assert:register("assertion", "opened_infoview_state", opened_infoview)
+assert:register("assertion", "opened_infoview_kept_state", opened_infoview_kept)
+assert:register("assertion", "closed_infoview_state", closed_infoview)
+assert:register("assertion", "closed_infoview_kept_state", closed_infoview_kept)
+
+assert:register("assertion", "update_wins", update_wins)
+assert:register("assertion", "closed_win", closed_win)
+assert:register("assertion", "created_win", created_win)
+assert:register("assertion", "changed_win", changed_win)
+
+-- initialize on very first nvim window (base case satisfied pretty trivially)
+assert.created_win()
 
 return helpers

lua/tests/infoview/autoopen_false_spec.lua

@@ -5,17 +5,15 @@ require('tests.helpers').setup {
   infoview = { autoopen = false },
 }
 describe('infoview', function()
-  vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-
   it('does not automatically open',
     function(_)
       vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-      assert.is_not.open_infoview()
+      assert.unopened_infoview()
     end)
 
   it('can be opened after no autoopen',
     function(_)
       infoview.get_current_infoview():open()
-      assert.open_infoview()
+      assert.opened_infoview()
     end)
 end)

lua/tests/infoview/autoopen_spec.lua

@@ -1,63 +1,67 @@
 local infoview = require('lean.infoview')
 local fixtures = require('tests.fixtures')
+local helpers = require('tests.helpers')
 
-require('tests.helpers').setup {
+helpers.setup {
   infoview = { autoopen = true },
 }
 describe('infoview', function()
-  vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-
   it('automatically opens',
     function(_)
       vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-      assert.open_infoview()
+      assert.opened_infoview()
     end)
 
   it('new tab automatically opens',
     function(_)
-      vim.api.nvim_command('tabedit ' .. fixtures.lean3_project.some_existing_file)
-      assert.open_infoview()
+      vim.api.nvim_command('tabnew')
+      assert.created_win()
+      vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
+      assert.opened_infoview()
     end)
 
   it('can be closed after autoopen',
     function(_)
       infoview.get_current_infoview():close()
-      assert.is_not.open_infoview()
+      assert.closed_infoview()
     end)
 
-  vim.api.nvim_command("tabnew")
   it('opens automatically after having closen previous infoviews',
   function(_)
+    vim.api.nvim_command("tabnew")
+    assert.created_win()
     vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
-    assert.open_infoview()
+    assert.opened_infoview()
   end)
 
-  vim.api.nvim_command("tabnew")
-  infoview.set_autoopen(false)
   it('auto-open disable',
   function(_)
+    vim.api.nvim_command("tabnew")
+    infoview.set_autoopen(false)
+    assert.created_win()
     vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
-    assert.is_not.open_infoview()
+    assert.unopened_infoview()
   end)
 
   it('open after auto-open disable',
   function(_)
     infoview.get_current_infoview():open()
-    assert.open_infoview()
+    assert.opened_infoview()
   end)
 
   it('close after auto-open disable',
   function(_)
     infoview.get_current_infoview():close()
-    assert.is_not.open_infoview()
+    assert.closed_infoview()
   end)
 
-  vim.api.nvim_command("tabnew")
-  infoview.set_autoopen(true)
   it('auto-open re-enable',
   function(_)
+    vim.api.nvim_command("tabnew")
+    infoview.set_autoopen(true)
+    assert.created_win()
     vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
-    assert.open_infoview()
+    assert.opened_infoview()
   end)
 
   it('no auto-open for irrelevant file',