Highlight and indent Rewrite Rule

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)

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 = '\<Rewrite\_s\+Rule\>'
+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, '', '\<end\>', 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 ')'

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="\<Rewrite\_s\+Rule\>" 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

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