Skip to content

Commit

Permalink
Add a switch for swapping the rewrite direction of lemmas.
Browse files Browse the repository at this point in the history
I have no idea why I can't get all these tests to pass, somehow the
regex isn't matching only all previous elements.
  • Loading branch information
Julian committed Sep 4, 2024
1 parent 45a3a5b commit 34fd70e
Show file tree
Hide file tree
Showing 2 changed files with 71 additions and 3 deletions.
13 changes: 10 additions & 3 deletions ftplugin/lean/switch.lua
Original file line number Diff line number Diff line change
Expand Up @@ -41,15 +41,22 @@ vim.b.switch_definitions = {
{ '', '', '', '' },

{
[ [=[\<simp\(?\?\)\(\s\+only\s\+\[[^\]]*]\)\?]=] ] = function(original)
[ [=[\<rw \[\%(\s*←\?\s*\i\+\s*,\s*\)*\zs\s*\(←\?\s*\)\(\i\+\)]=] ] = function (original)
local arrow = original[2]
local lemma = original[3]
return (arrow == '' and '' or '') .. lemma
end
},

{
[ [=[\<simp\(?\?\)\(\s\+only\s\+\[[^\]]*]\)\?]=] ] = function (original)
if original[2] == '' and original[3] == '' then
return 'simp?'
else
return 'simp'
end
end,
end
},

{ [segment 'bot'] = 'top', [segment 'top'] = 'bot' },
{ [segment 'inl'] = 'inr', [segment 'inr'] = 'inl' },
{ [segment 'left'] = 'right', [segment 'right'] = 'left' },
Expand Down
61 changes: 61 additions & 0 deletions spec/switch_spec.lua
Original file line number Diff line number Diff line change
Expand Up @@ -86,4 +86,65 @@ describe('tactics', function()
assert.contents.are [=[simp? [foo, bar, baz]]=]
end)
)

it(
'switch between rw [foo] and rw [← foo]',
clean_buffer([=[rw [foo]]=], function()
vim.cmd.normal { '1gg5|', bang = true }
vim.cmd.Switch()
assert.contents.are [=[rw [← foo]]=]
end)
)

it(
'switch between rw [← foo] and rw [foo]',
clean_buffer([=[rw [← foo]]=], function()
vim.cmd.normal { '1gg5|', bang = true }
vim.cmd.Switch()
assert.contents.are [=[rw [foo]]=]
end)
)

it(
'switch between rw [foo, bar] and rw [← foo, bar]',
clean_buffer([=[rw [foo, bar]]=], function()
vim.cmd.normal { '1gg5|', bang = true }
vim.cmd.Switch()
assert.contents.are [=[rw [← foo, bar]]=]
end)
)

it(
'switch between rw [foo, bar, baz] and rw [foo, ← bar, baz]',
clean_buffer([=[rw [foo, bar, baz]]=], function()
vim.cmd.normal { '1gg11|', bang = true }

vim.cmd.Switch()
assert.contents.are [=[rw [foo, ← bar, baz]]=]

vim.cmd.Switch()
assert.contents.are [=[rw [foo, bar, baz]]=]

vim.cmd.normal { '1gg16|', bang = true }
assert.contents.are [=[rw [foo, bar, ← baz]]=]
end)
)

it(
'switch between rw [foo, bar] and rw [foo, ← bar]',
clean_buffer([=[rw [foo, bar]]=], function()
vim.cmd.normal { '1gg11|', bang = true }
vim.cmd.Switch()
assert.contents.are [=[rw [foo, ← bar]]=]
end)
)

it(
'switch between rw [foo _ bar, baz] and rw [← foo _ bar, baz]',
clean_buffer([=[rw [foo _ bar, baz]]=], function()
vim.cmd.normal { '1gg5|', bang = true }
vim.cmd.Switch()
assert.contents.are [=[rw [← foo _ bar, baz]]=]
end)
)
end)

0 comments on commit 34fd70e

Please sign in to comment.