From 72c3411035574bd884e19eb261f5cda55c663ac4 Mon Sep 17 00:00:00 2001 From: whonore Date: Tue, 17 Sep 2024 10:01:32 -0700 Subject: [PATCH] Highlight and indent Rewrite Rule --- CHANGELOG.md | 4 ++++ indent/coq.vim | 4 +++- syntax/coq.vim | 5 ++++- tests/vim/indent.vader | 19 +++++++++++++++++++ 4 files changed, 30 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 74807899..c345e122 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,6 +2,10 @@ ## Unreleased ([main]) +### Added +- Basic support for `Rewrite Rule` syntax highlighting and indentation. + (PR #373) + ### Fixed - Correctly execute commands containing quotes (e.g., `Coq Check a'`). (PR #371) diff --git a/indent/coq.vim b/indent/coq.vim index 3be964aa..e0ad91ad 100644 --- a/indent/coq.vim +++ b/indent/coq.vim @@ -41,6 +41,8 @@ let s:bullet = '[-+*]\+)\@!' let s:bulletline = '^\s*' . s:bullet let s:match = '\<\%(lazy\|multi\)\?match\>' let s:inductive = '\%(\%(Co\)\?Inductive\|Variant\)' +let s:rewrite = '\' +let s:vbar_cmd = '\%(' . s:inductive . '\|' . s:rewrite . '\)' let s:lineend = '\s*$' " Match syntax groups. @@ -243,7 +245,7 @@ function! s:GetCoqIndent() abort if l:currentline =~# '^\s*|[|}]\@!' let l:match = s:indent_of_previous_pair(s:match, '', '\', 1, ['string', 'comment']) let l:off = get(g:, 'coqtail_inductive_shift', 1) * &sw - return l:match != -1 ? l:match : s:indent_of_previous('^\s*' . s:inductive) + l:off + return l:match != -1 ? l:match : s:indent_of_previous('^\s*' . s:vbar_cmd) + l:off endif " current line begins with terminating '|}', '}', or ')' diff --git a/syntax/coq.vim b/syntax/coq.vim index b912bf50..a8163f3a 100644 --- a/syntax/coq.vim +++ b/syntax/coq.vim @@ -267,7 +267,7 @@ syn region coqBinderTypeParen contained contains=@coqTerm matchgroup=coqVernac syn region coqBinderTypeCurly contained contains=@coqTerm matchgroup=coqVernacPunctuation start=":" end="}" " Declarations -syn region coqDecl contains=coqIdent,coqDeclTerm,coqBinder matchgroup=coqVernacCmd start="\<\%(Axioms\?\|Conjectures\?\|Hypothes[ie]s\|Parameters\?\|Variables\?\|Context\)\>" matchgroup=coqVernacCmd end="\.\_s" keepend +syn region coqDecl contains=coqIdent,coqDeclTerm,coqBinder matchgroup=coqVernacCmd start="\<\%(Axioms\?\|Conjectures\?\|Hypothes[ie]s\|Parameters\?\|Variables\?\|Context\|Symbols\?\)\>" matchgroup=coqVernacCmd end="\.\_s" keepend syn region coqDeclTerm contained contains=@coqTerm matchgroup=coqVernacPunctuation start=":" end=")" syn region coqDeclTerm contained contains=@coqTerm matchgroup=coqVernacPunctuation start=":" end="\.\_s" @@ -491,6 +491,9 @@ syn region elpiString contained start=+"+ skip=+\\"+ end=+"+ extend syn match elpiMode contained "\<[io]:" syn match elpiNumber contained "[0-9]\+" +" Rewrite Rules +syn region coqRewrite contains=coqIdent,coqVernacPunctuation,coqLtacContents matchgroup=coqVernacCmd start="\" end="\.\_s" keepend + " Various (High priority) syn region coqComment containedin=ALLBUT,coqString contains=coqComment,coqTodo,@Spell start="(\*" end="\*)" extend keepend syn keyword coqTodo contained TODO FIXME XXX NOTE diff --git a/tests/vim/indent.vader b/tests/vim/indent.vader index 7806a13d..dd670071 100644 --- a/tests/vim/indent.vader +++ b/tests/vim/indent.vader @@ -90,6 +90,25 @@ Expect coq (indented-inductive-shift): Execute (indent-inductive-shift-option-post): unlet g:coqtail_inductive_shift +Given coq (rewrite): + Rewrite Rule pplus_rewrite := + | ?n ++ 0 => ?n + | ?n ++ S ?m => + S (?n ++ ?m) + | 0 ++ ?n => ?n + | S ?n ++ ?m => S (?n ++ ?m). + +Do (indent-rewrite): + =ip + +Expect coq (indented-rewrite): + Rewrite Rule pplus_rewrite := + | ?n ++ 0 => ?n + | ?n ++ S ?m => + S (?n ++ ?m) + | 0 ++ ?n => ?n + | S ?n ++ ?m => S (?n ++ ?m). + Given coq (match): Definition f (b : bool) := match b with