why3.vim 8.19 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
" Vim syntax file
" Language:     Why3
" Filenames:    *.why *.mlw
"
" Adapted from syntax file for Ocaml

" For version 5.x: Clear all syntax items
" For version 6.x: Quit when a syntax file was already loaded
if version < 600
  syntax clear
elseif exists("b:current_syntax") && b:current_syntax == "why3"
  finish
endif

" Why3 is case sensitive.
syn case match

" " Script headers highlighted like comments
" syn match    whyComment   "^#!.*"

" lowercase identifier - the standard way to match
syn match    whyLCIdentifier /\<\(\l\|_\)\(\w\|'\)*\>/

syn match    whyKeyChar    "|"

" Errors
syn match    whyBraceErr   "}"
syn match    whyBrackErr   "\]"
syn match    whyParenErr   ")"

31
syn match    whyCommentErr "\*)"
Andrei Paskevich's avatar
Andrei Paskevich committed
32 33 34 35 36 37 38 39 40 41 42 43

syn match    whyCountErr   "\<downto\>"
syn match    whyCountErr   "\<to\>"

syn match    whyDoErr      "\<do\>"
syn match    whyDoneErr    "\<done\>"
syn match    whyThenErr    "\<then\>"
syn match    whyTheoryErr  "\<theory\>"
syn match    whyModuleErr  "\<module\>"
syn match    whyEndErr     "\<end\>"

" Some convenient clusters
44
syn cluster  whyAllErrs contains=whyBraceErr,whyBrackErr,whyParenErr,whyCommentErr,whyCountErr,whyDoErr,whyDoneErr,whyEndErr,whyThenErr,whyTheoryErr,whyModuleErr
Andrei Paskevich's avatar
Andrei Paskevich committed
45

46
syn cluster  whyContained contains=whyTodo,whyImport,whyExport,whyTheoryContents,whyModuleContents,whyScopeContents,whyModuleKeyword
Andrei Paskevich's avatar
Andrei Paskevich committed
47 48 49
" ,whyPreDef,whyModParam,whyModParam1,whyPreMPRestr,whyMPRestr,whyMPRestr1,whyMPRestr2,whyMPRestr3,whyModRHS,whyFuncWith,whyFuncStruct,whyModTypeRestr,whyModTRWith,whyWith,whyWithRest,whyModType,whyFullMod,whyVal

" Enclosing delimiters
Andrei Paskevich's avatar
Andrei Paskevich committed
50 51 52
syn region   whyEncl transparent matchgroup=whyKeyChar start="(" matchgroup=whyKeyChar end=")" contains=ALLBUT,@whyContained,whyParenErr
syn region   whyEncl transparent matchgroup=whyKeyChar start="{" matchgroup=whyKeyChar end="}"  contains=ALLBUT,@whyContained,whyBraceErr
syn region   whyEncl transparent start="\[" end="\]" contains=ALLBUT,@whyContained,whyBrackErr
Andrei Paskevich's avatar
Andrei Paskevich committed
53 54

" Comments
55 56 57
syn region   whyComment start="(\*" end="\*)" contains=whyComment,whyTodo
syn match    whyOperator "(\*)"

Andrei Paskevich's avatar
Andrei Paskevich committed
58 59 60 61 62 63 64 65 66 67 68 69 70 71
syn keyword  whyTodo contained TODO FIXME XXX NOTE

" Blocks
" FIXME? match and try should detect the absence of "with" ?
syn region   whyEnd matchgroup=whyKeyword start="\<begin\>" matchgroup=whyKeyword end="\<end\>" contains=ALLBUT,@whyContained,whyEndErr
syn region   whyEnd matchgroup=whyKeyword start="\<match\>" matchgroup=whyKeyword end="\<end\>" contains=ALLBUT,@whyContained,whyEndErr
syn region   whyEnd matchgroup=whyKeyword start="\<loop\>" matchgroup=whyKeyword end="\<end\>" contains=ALLBUT,@whyContained,whyEndErr
syn region   whyEnd matchgroup=whyKeyword start="\<try\>" matchgroup=whyKeyword end="\<end\>" contains=ALLBUT,@whyContained,whyEndErr
syn region   whyNone matchgroup=whyKeyword start="\<for\>" matchgroup=whyKeyword end="\<\(to\|downto\)\>" contains=ALLBUT,@whyContained,whyCountErr
syn region   whyDo matchgroup=whyKeyword start="\<do\>" matchgroup=whyKeyword end="\<done\>" contains=ALLBUT,@whyContained,whyDoneErr
syn region   whyNone matchgroup=whyKeyword start="\<if\>" matchgroup=whyKeyword end="\<then\>" contains=ALLBUT,@whyContained,whyThenErr

" Theories and modules

72
syn region   whyTheory matchgroup=whyKeyword start="\<theory\>" matchgroup=whyModSpec end="\<\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment skipwhite skipempty nextgroup=whyModuleContents
Andrei Paskevich's avatar
Andrei Paskevich committed
73
syn region   whyModule matchgroup=whyKeyword start="\<module\>" matchgroup=whyModSpec end="\<\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment skipwhite skipempty nextgroup=whyModuleContents
74
syn region   whyScope matchgroup=whyKeyword start="\<scope\>" matchgroup=whyModSpec end="\<\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment,whyImport skipwhite skipempty nextgroup=whyModuleContents
Andrei Paskevich's avatar
Andrei Paskevich committed
75

76
syn region   whyModuleContents start="" matchgroup=whyModSpec end="\<end\>" contained contains=ALLBUT,@whyContained,whyEndErr,whyTheory,whyModule
Andrei Paskevich's avatar
Andrei Paskevich committed
77

78
syn region   whyNone matchgroup=whyKeyword start="\<\(use\|clone\)\>" matchgroup=whyModSpec end="\<\(\w\+\.\)*\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment,whyString,whyImport,whyExport
Andrei Paskevich's avatar
Andrei Paskevich committed
79 80 81
syn keyword  whyExport contained export
syn keyword  whyImport contained import

82
syn region   whyNone matchgroup=whyKeyword start="\<\(axiom\|lemma\|goal\)\>" matchgroup=whyNone end="\<\w\(\w\|'\)*\>" contains=@whyAllErrs,whyComment
Andrei Paskevich's avatar
Andrei Paskevich committed
83

Martin Clochard's avatar
Martin Clochard committed
84
syn keyword  whyKeyword  as by constant
Andrei Paskevich's avatar
Andrei Paskevich committed
85
syn keyword  whyKeyword  else epsilon exists
86
syn keyword  whyKeyword  forall function
87
syn keyword  whyKeyword  if in inductive coinductive
Andrei Paskevich's avatar
Andrei Paskevich committed
88
syn keyword  whyKeyword  let meta
Martin Clochard's avatar
Martin Clochard committed
89
syn keyword  whyKeyword  not predicate so
90
syn keyword  whyKeyword  then type with
Andrei Paskevich's avatar
Andrei Paskevich committed
91

92
syn keyword  whyKeyword  abstract any
93
syn keyword  whyKeyword  exception fun ghost label
94 95 96 97
syn keyword  whyKeyword  model mutable private
syn keyword  whyKeyword  raise rec val while

syn keyword  whyBoolean  true false
Andrei Paskevich's avatar
Andrei Paskevich committed
98 99 100 101

syn keyword  whyType     bool int list map option real
syn keyword  whyType     array ref unit

102
syn keyword  whySpec     absurd assert assume check diverges ensures invariant
103
syn keyword  whySpec     pure raises reads requires returns variant writes at old
104

Andrei Paskevich's avatar
Andrei Paskevich committed
105 106 107 108 109 110 111 112 113
syn match    whyConstructor  "(\s*)"
syn match    whyConstructor  "\u\(\w\|'\)*\>"
syn match    whyModPath      "\u\(\w\|'\)*\."he=e-1

syn region   whyString       start=+"+ skip=+\\\\\|\\"+ end=+"+

syn match    whyOperator     "->"
syn match    whyOperator     "<->\?"
syn match    whyOperator     "/\\"
Andrei Paskevich's avatar
Andrei Paskevich committed
114
syn match    whyOperator     "\\/"
Andrei Paskevich's avatar
Andrei Paskevich committed
115 116
syn match    whyOperator     "&&"
syn match    whyOperator     "<>"
117
syn match    whyKeyChar      "|"
Andrei Paskevich's avatar
Andrei Paskevich committed
118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140
syn match    whyKeyChar      ";"
" FIXME? is this too inefficient?
syn match    whyOperator     "[^<>~=:+*/%$&@^.|#!?]=[^<>~=:+*/%$&@^.|#!?]"ms=s+1,me=e-1
syn match    whyOperator                         "^=[^<>~=:+*/%$&@^.|#!?]"me=e-1
syn match    whyOperator     "[^<>~=:+*/%$&@^.|#!?]=$"ms=s+1

syn match    whyAnyVar       "\<_\>"

syn match    whyNumber        "\<-\=\d\(_\|\d\)*\>"
syn match    whyNumber        "\<-\=0[x|X]\(\x\|_\)\+\>"
syn match    whyNumber        "\<-\=0[o|O]\(\o\|_\)\+\>"
syn match    whyNumber        "\<-\=0[b|B]\([01]\|_\)\+\>"
syn match    whyFloat         "\<-\=\d\+[eE][-+]\=\d\+\>"
syn match    whyFloat         "\<-\=\d\+\.\d*\([eE][-+]\=\d\+\)\=\>"
syn match    whyFloat         "\<-\=0[x|X]\x\+\.\?\x*[pP][-+]\=\d\+\>"

" Synchronization
syn sync minlines=50
syn sync maxlines=500

syn sync match whyDoSync      grouphere  whyDo      "\<do\>"
syn sync match whyDoSync      groupthere whyDo      "\<done\>"

141
syn sync match whyEndSync     grouphere  whyEnd     "\<\(begin\|match\|loop\|try\)\>"
Andrei Paskevich's avatar
Andrei Paskevich committed
142 143 144 145 146 147 148 149
syn sync match whyEndSync     groupthere whyEnd     "\<end\>"

syn sync match whyTheorySync  grouphere  whyTheory  "\<theory\>"
syn sync match whyTheorySync  groupthere whyTheory  "\<end\>"

syn sync match whyModuleSync  grouphere  whyModule  "\<module\>"
syn sync match whyModuleSync  groupthere whyModule  "\<end\>"

150 151
syn sync match whyScopeSync   grouphere  whyScope   "\<scope\>"
syn sync match whyScopeSync   groupthere whyScope   "\<end\>"
Andrei Paskevich's avatar
Andrei Paskevich committed
152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186

" Define the default highlighting.
" For version 5.7 and earlier: only when not done already
" For version 5.8 and later: only when an item doesn't have highlighting yet
if version >= 508 || !exists("did_why_syntax_inits")
  if version < 508
    let did_why_syntax_inits = 1
    command -nargs=+ HiLink hi link <args>
  else
    command -nargs=+ HiLink hi def link <args>
  endif

  HiLink whyBraceErr	   Error
  HiLink whyBrackErr	   Error
  HiLink whyParenErr	   Error
  HiLink whyCommentErr     Error
  HiLink whyCountErr	   Error
  HiLink whyDoErr	   Error
  HiLink whyDoneErr	   Error
  HiLink whyEndErr	   Error
  HiLink whyThenErr	   Error
  HiLink whyTheoryErr	   Error
  HiLink whyModuleErr	   Error

  HiLink whyComment	   Comment

  HiLink whyModPath	   Include
  HiLink whyModSpec	   Include
  HiLink whyImport	   Keyword
  HiLink whyExport	   Keyword
  HiLink whyModuleKeyword  Keyword

  HiLink whyConstructor    Constant

  HiLink whyKeyword	   Keyword
Andrei Paskevich's avatar
Andrei Paskevich committed
187 188 189
  HiLink whyKeyChar	   Operator
  HiLink whyAnyVar	   Operator
  HiLink whyOperator	   Operator
190
  HiLink whySpec	   Identifier
Andrei Paskevich's avatar
Andrei Paskevich committed
191 192 193 194

  HiLink whyNumber	   Number
  HiLink whyFloat	   Float
  HiLink whyString	   String
195
  HiLink whyBoolean	   Boolean
Andrei Paskevich's avatar
Andrei Paskevich committed
196 197 198 199 200 201 202 203 204 205 206 207 208

  HiLink whyType	   Type

  HiLink whyTodo	   Todo

  HiLink whyEncl	   Keyword

  delcommand HiLink
endif

let b:current_syntax = "why3"

" vim: ts=8