Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add a first version of indent support.
Browse files Browse the repository at this point in the history
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.
Julian committed Nov 30, 2024
1 parent d05e593 commit 2bf740c
Showing 8 changed files with 347 additions and 6 deletions.
15 changes: 15 additions & 0 deletions indent/lean.lua
Original file line number Diff line number Diff line change
@@ -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<',
}, ' ')
89 changes: 89 additions & 0 deletions lua/lean/indent.lua
Original file line number Diff line number Diff line change
@@ -0,0 +1,89 @@
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',
'=>',
':=',
}, [[\|]])))

---Check whether the given string is a goal focus dot.
---@param str string
---@param position? integer
---@return boolean
local function focuses_at(str, position)
position = position or 1
return str:sub(position, position + 1) == '·'
end

---Check whether the given line number is within a Lean enclosed bracket.
---@param linenr number
---@return boolean
local function is_enclosed(linenr)
local syntax = vim.inspect_pos(0, linenr, 0).syntax[1]
return syntax and syntax.hl_group == 'leanEncl'
end

---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 focuses_at(current:gsub('^%s*', '')) 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 focuses_at(last, last_indent + 1) then
return last_indent + #'·'
elseif INDENT_AFTER:match_str(last) and not INDENT_AFTER:match_str(current) then
return (last_indent or 0) + vim.bo.shiftwidth
elseif last_indent and is_enclosed(linenr - 1) then
return last_indent + vim.bo.shiftwidth
elseif last_indent and not is_block_comment(linenr - 2) then
local dedent_one = last_indent - vim.bo.shiftwidth

-- We could go backwards to check but that would involve looking back
-- repetaedly over lines backwards, so we cheat and just check whether the
-- previous line looks like it has a binder on it.
local is_end_of_binders = dedent_one > 0
and last:find '^%s*[({[]'
and INDENT_AFTER:match_str(current)
return is_end_of_binders and dedent_one or last_indent
end

return vim.fn.indent(linenr)
end

return M
35 changes: 29 additions & 6 deletions spec/fixtures.lua
Original file line number Diff line number Diff line change
@@ -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
19 changes: 19 additions & 0 deletions spec/fixtures/indent/declarations.in.lean
Original file line number Diff line number Diff line change
@@ -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
19 changes: 19 additions & 0 deletions spec/fixtures/indent/declarations.lean
Original file line number Diff line number Diff line change
@@ -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
8 changes: 8 additions & 0 deletions spec/fixtures/indent/with_comment.in.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
/-- foo
bar
baz -/
theorem quux : 0 = 0 := by
have : 0 = 0 := rfl
-- some comment
have : 1 = 1 := rfl
rfl
8 changes: 8 additions & 0 deletions spec/fixtures/indent/with_comment.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
/-- foo
bar
baz -/
theorem quux : 0 = 0 := by
have : 0 = 0 := rfl
-- some comment
have : 1 = 1 := rfl
rfl
160 changes: 160 additions & 0 deletions spec/indent_spec.lua
Original file line number Diff line number Diff line change
@@ -0,0 +1,160 @@
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)
)

it(
'indents inside braces',
helpers.clean_buffer(
[[
example : 2 = 2 ∧ 3 = 3 := by
exact ⟨rfl,
]],
function()
helpers.feed 'Gorfl⟩'
assert.current_line.is ' 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)

0 comments on commit 2bf740c

Please sign in to comment.