Add a first version of indent support.

Handles some simple after-word indentation as well as focus dots.

Does not do anything particularly fancy to amke sure we're indenting
after the "real" use of the indentation words, but it's a start.

.luacheckrc

@@ -12,6 +12,8 @@ globals = {
     fields = {
       "contents",
       "message",
+      "are",
+      "is",
       "is_falsy",
       "is_truthy",
     }

indent/lean.lua

@@ -0,0 +1,15 @@
+if vim.b.did_indent then
+  return
+end
+---@diagnostic disable-next-line: inject-field
+vim.b.did_indent = true
+
+vim.bo.lisp = false
+vim.bo.indentexpr = [[v:lua.require('lean.indent').indentexpr()]]
+vim.bo.smartindent = false
+
+vim.b.undo_indent = table.concat({
+  'setlocal indentexpr<',
+  'lisp<',
+  'smartindent<',
+}, ' ')

lua/lean/indent.lua

@@ -0,0 +1,67 @@
+local M = {}
+
+-- Borrowed from the (not merged) https://github.com/leanprover/vscode-lean4/pull/329/
+local INDENT_AFTER = vim.regex(([[\<\(%s\)$]]):format(table.concat({
+  'by',
+  'do',
+  'try',
+  'finally',
+  'then',
+  'else',
+  'where',
+  'from',
+  'extends',
+  'deriving',
+  '=>',
+  ':=',
+}, [[\|]])))
+
+local FOCUS = '·'
+
+---Check whether the given line number is within a Lean block comment.
+---@param linenr number
+---@return boolean
+local function is_block_comment(linenr)
+  local syntax = vim.inspect_pos(0, linenr, 0).syntax[1]
+  return syntax and syntax.hl_group == 'leanBlockComment'
+end
+
+---A crude `:h indentexpr` for Lean.
+---@param linenr integer? the line number whose indent we are calculating
+---@return integer
+function M.indentexpr(linenr)
+  linenr = linenr or vim.v.lnum
+
+  if linenr == 1 then
+    return 0 -- Don't indent the first line, and now we can subtract from linenr.
+  end
+
+  local last, current = unpack(vim.api.nvim_buf_get_lines(0, linenr - 2, linenr, true))
+
+  -- Lua patterns are... seemingly broken with unicode and/or multibyte
+  -- characters. Specifically `('  foo'):find '^(%s+)([z]?)(.*)'` works fine to
+  -- match an optional `z`, but ('  foo'):find '^(%s+)([·]?)(.*)' does not.
+  local _, last_indent = last:find '^%s+'
+
+  if current:gsub('^%s*', ''):sub(1, 2) == FOCUS then
+    -- FIXME this seems wrong, and needs to check if the previous line is focused or not
+    return vim.bo.shiftwidth
+  elseif last:find ':%s*$' then
+    return vim.bo.shiftwidth * 2
+  elseif last:find ':=%s*$' then
+    return vim.bo.shiftwidth
+  elseif last_indent and last:sub(last_indent + 1, last_indent + 2) == FOCUS then
+    return last_indent + #FOCUS
+  elseif last_indent and not is_block_comment(linenr - 2) then
+    if INDENT_AFTER:match_str(current) then
+      return last_indent - vim.bo.shiftwidth
+    end
+    return last_indent
+  elseif INDENT_AFTER:match_str(last) and not INDENT_AFTER:match_str(current) then
+    return vim.bo.shiftwidth
+  end
+
+  return vim.fn.indent(linenr)
+end
+
+return M

spec/fixtures.lua

@@ -1,13 +1,34 @@
 local this_file = debug.getinfo(1).source:match '@(.*)$'
 
 local root = vim.fs.joinpath(vim.fs.dirname(this_file), 'fixtures')
+local indent = vim.fs.joinpath(root, 'indent')
 local project_root = vim.fs.normalize(vim.fs.joinpath(root, 'example-project'))
 
 local function child(name)
   return vim.fs.joinpath(project_root, name)
 end
 
 local fixtures = {
+  indent = function()
+    return vim.iter(vim.fs.dir(indent)):map(function(each)
+      local name, replaced = each:gsub('.in.lean$', '')
+      if replaced == 0 then
+        return
+      end
+
+      ---@class IndentFixture
+      ---@field description string the name of the fixture
+      ---@field unindented string the path to the unindented version
+      ---@field expected string[] the expected indented lines
+
+      ---@type IndentFixture
+      return {
+        description = name:gsub('_', ' '),
+        unindented = vim.fs.joinpath(indent, each),
+        expected = vim.fn.readfile(vim.fs.joinpath(indent, name .. '.lean')),
+      }
+    end)
+  end,
   project = {
     root = project_root,
     child = child,
@@ -21,12 +42,6 @@ local fixtures = {
   },
 }
 
-assert.is_truthy(vim.uv.fs_stat(fixtures.project.some_existing_file))
-assert.is_falsy(vim.uv.fs_stat(fixtures.project.some_nonexisting_file))
-assert.is_truthy(vim.uv.fs_stat(fixtures.project.some_nested_existing_file))
-assert.is_falsy(vim.uv.fs_stat(fixtures.project.some_nested_nonexisting_file))
-assert.is_truthy(vim.uv.fs_stat(fixtures.project.some_dependency_file))
-
 function fixtures.project:files()
   return vim.iter {
     ['existing'] = self.some_existing_file,
@@ -36,4 +51,12 @@ function fixtures.project:files()
   }
 end
 
+assert.is.truthy(vim.uv.fs_stat(fixtures.project.some_existing_file))
+assert.is.falsy(vim.uv.fs_stat(fixtures.project.some_nonexisting_file))
+assert.is.truthy(vim.uv.fs_stat(fixtures.project.some_nested_existing_file))
+assert.is.falsy(vim.uv.fs_stat(fixtures.project.some_nested_nonexisting_file))
+assert.is.truthy(vim.uv.fs_stat(fixtures.project.some_dependency_file))
+
+assert.is.truthy(vim.uv.fs_stat(indent))
+
 return fixtures

spec/fixtures/indent/declarations.in.lean

@@ -0,0 +1,19 @@
+structure foo where
+
+def spam := 37
+
+def eggs : Nat × Nat where
+fst := 3
+snd := 37
+
+def bar : foo where
+
+structure quux where
+foo := bar
+
+example : 2 = 2 := by
+  cases 2
+  · cases 2
+   rfl
+   rfl
+  · rfl

spec/fixtures/indent/declarations.lean

@@ -0,0 +1,19 @@
+structure foo where
+
+def spam := 37
+
+def eggs : Nat × Nat where
+  fst := 3
+  snd := 37
+
+def bar : foo where
+
+structure quux where
+  foo := bar
+
+example : 2 = 2 := by
+  cases 2
+  · cases 2
+    rfl
+    rfl
+  · rfl

spec/fixtures/indent/with_comment.in.lean

@@ -0,0 +1,8 @@
+/-- foo
+  bar
+  baz -/
+theorem quux : 0 = 0 := by
+have : 0 = 0 := rfl
+-- some comment
+have : 1 = 1 := rfl
+rfl

spec/fixtures/indent/with_comment.lean

@@ -0,0 +1,8 @@
+/-- foo
+  bar
+  baz -/
+theorem quux : 0 = 0 := by
+  have : 0 = 0 := rfl
+  -- some comment
+  have : 1 = 1 := rfl
+  rfl

spec/indent_spec.lua

@@ -0,0 +1,146 @@
+local fixtures = require 'spec.fixtures'
+local helpers = require 'spec.helpers'
+
+describe('indent', function()
+  it(
+    'indents after where',
+    helpers.clean_buffer([[structure foo where]], function()
+      helpers.feed 'Gofoo := 12'
+      assert.current_line.is '  foo := 12'
+    end)
+  )
+
+  it(
+    'maintains indentation level for fields',
+    helpers.clean_buffer(
+      [[
+      structure foo where
+        foo := 12
+    ]],
+      function()
+        helpers.feed 'Gobar := 37'
+        assert.current_line.is '  bar := 37'
+      end
+    )
+  )
+
+  it(
+    'aligns with focus dots',
+    helpers.clean_buffer(
+      [[
+      example {n : Nat} : n = n := by
+        cases n
+        · have : 0 = 0 := rfl
+    ]],
+      function()
+        helpers.feed 'Gorfl'
+        assert.current_line.is '    rfl'
+      end
+    )
+  )
+
+  it(
+    'indents after by',
+    helpers.clean_buffer([[example : 2 = 2 := by]], function()
+      helpers.feed 'Gorfl'
+      assert.current_line.is '  rfl'
+    end)
+  )
+
+  it(
+    'respects shiftwidth',
+    helpers.clean_buffer([[structure foo where]], function()
+      vim.bo.shiftwidth = 7
+      helpers.feed 'Gofoo := 12'
+      assert.current_line.is '       foo := 12'
+    end)
+  )
+
+  it(
+    'does not misindent the structure line itself',
+    helpers.clean_buffer([[structure foo where]], function()
+      vim.cmd.normal '=='
+      assert.current_line.is 'structure foo where'
+    end)
+  )
+
+  it(
+    'does not misindent successive structures',
+    helpers.clean_buffer(
+      [[
+      structure foo where
+      structure bar where
+      ]],
+      function()
+        vim.cmd.normal 'gg=G'
+        assert.are.same(
+          { 'structure foo where', 'structure bar where' },
+          vim.api.nvim_buf_get_lines(0, 0, -1, false)
+        )
+      end
+    )
+  )
+
+  it(
+    'does not misindent successive structures with whitespace',
+    helpers.clean_buffer(
+      [[
+      structure foo where
+
+      structure bar where
+      ]],
+      function()
+        vim.cmd.normal 'gg=G'
+        assert.are.same(
+          { 'structure foo where', '', 'structure bar where' },
+          vim.api.nvim_buf_get_lines(0, 0, -1, false)
+        )
+      end
+    )
+  )
+
+  it(
+    'does not mess with whitespace within structures with extra linebreaks',
+    helpers.clean_buffer(
+      [[
+      structure foo where
+        foo := 12
+        bar := 37
+
+        baz := 73
+        quux := 12
+      ]],
+      function()
+        vim.cmd.normal 'gg=G'
+        assert.are.same({
+          'structure foo where',
+          '  foo := 12',
+          '  bar := 37',
+          '',
+          '  baz := 73',
+          '  quux := 12',
+        }, vim.api.nvim_buf_get_lines(0, 0, -1, false))
+      end
+    )
+  )
+
+  it(
+    'dedents after double indented type',
+    helpers.clean_buffer([[example :]], function()
+      helpers.feed 'o2 = 2 :=<CR>rfl'
+      assert.contents.are [[
+        example :
+            2 = 2 :=
+          rfl
+      ]]
+    end)
+  )
+
+  for each in fixtures.indent() do
+    it(each.description, function()
+      vim.cmd.edit { each.unindented, bang = true }
+      vim.cmd.normal 'gg=G'
+      assert.are.same(each.expected, vim.api.nvim_buf_get_lines(0, 0, -1, false))
+    end)
+  end
+end)