From 4b191f797e7c94f490c159df7339211e45754fb0 Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Sun, 17 Nov 2024 16:12:42 -0500 Subject: [PATCH] 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 | 2 + indent/lean.lua | 15 +++ lua/lean/indent.lua | 68 ++++++++++ spec/fixtures.lua | 35 +++++- spec/fixtures/indent/declarations.in.lean | 19 +++ spec/fixtures/indent/declarations.lean | 19 +++ spec/fixtures/indent/with_comment.in.lean | 8 ++ spec/fixtures/indent/with_comment.lean | 8 ++ spec/indent_spec.lua | 146 ++++++++++++++++++++++ 9 files changed, 314 insertions(+), 6 deletions(-) create mode 100644 indent/lean.lua create mode 100644 lua/lean/indent.lua create mode 100644 spec/fixtures/indent/declarations.in.lean create mode 100644 spec/fixtures/indent/declarations.lean create mode 100644 spec/fixtures/indent/with_comment.in.lean create mode 100644 spec/fixtures/indent/with_comment.lean create mode 100644 spec/indent_spec.lua diff --git a/.luacheckrc b/.luacheckrc index 21c181c3..8cd8ac49 100644 --- a/.luacheckrc +++ b/.luacheckrc @@ -12,6 +12,8 @@ globals = { fields = { "contents", "message", + "are", + "is", "is_falsy", "is_truthy", } diff --git a/indent/lean.lua b/indent/lean.lua new file mode 100644 index 00000000..1029a41c --- /dev/null +++ b/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<', +}, ' ') diff --git a/lua/lean/indent.lua b/lua/lean/indent.lua new file mode 100644 index 00000000..97a73ab2 --- /dev/null +++ b/lua/lean/indent.lua @@ -0,0 +1,68 @@ +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 + local one_less = last_indent - vim.bo.shiftwidth + if one_less > 0 and INDENT_AFTER:match_str(current) then + return one_less + 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 diff --git a/spec/fixtures.lua b/spec/fixtures.lua index 5532f7cf..ff9df99d 100644 --- a/spec/fixtures.lua +++ b/spec/fixtures.lua @@ -1,6 +1,7 @@ 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) @@ -8,6 +9,26 @@ local function child(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 diff --git a/spec/fixtures/indent/declarations.in.lean b/spec/fixtures/indent/declarations.in.lean new file mode 100644 index 00000000..da180b3f --- /dev/null +++ b/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 diff --git a/spec/fixtures/indent/declarations.lean b/spec/fixtures/indent/declarations.lean new file mode 100644 index 00000000..bbaf51be --- /dev/null +++ b/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 diff --git a/spec/fixtures/indent/with_comment.in.lean b/spec/fixtures/indent/with_comment.in.lean new file mode 100644 index 00000000..d9879100 --- /dev/null +++ b/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 diff --git a/spec/fixtures/indent/with_comment.lean b/spec/fixtures/indent/with_comment.lean new file mode 100644 index 00000000..d2805280 --- /dev/null +++ b/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 diff --git a/spec/indent_spec.lua b/spec/indent_spec.lua new file mode 100644 index 00000000..09708eff --- /dev/null +++ b/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 :=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)