why3.lang 7.63 KB
Newer Older
1
<?xml version="1.0" encoding="UTF-8"?>
2
<!--
3

4 5
The Why3 Verification Platform   /   The Why3 Development Team
Copyright 2010-2013   -    INRIA - CNRS - Paris-Sud University
6

7 8 9
This software is distributed under the terms of the GNU Lesser
General Public License version 2.1, with the special exception
on linking described in file LICENSE.
10

11 12
-->
<!--
13
 This file was based on ocaml.lang by
14 15 16
 Copyright (C) 2007 Eric Cooper <ecc@cmu.edu>
 Copyright (C) 2007 Eric Norige <thelema314@gmail.com>
-->
17
<language id="why3" _name="Why3" version="2.0" _section="Sources">
18
  <metadata>
19
    <property name="mimetypes">text/x-why3</property>
20
    <property name="globs">*.mlw;*.why</property>
21 22 23
    <property name="block-comment-start">(*</property>
    <property name="block-comment-end">*)</property>
  </metadata>
24

25 26 27 28 29 30 31 32 33 34 35
  <styles>
    <style id="comment" _name="Comment" map-to="def:comment"/>
    <style id="base-n-integer" _name="Base-N Integer" map-to="def:base-n-integer"/>
    <style id="floating-point" _name="Floating Point number" map-to="def:floating-point"/>
    <style id="decimal" _name="Decimal number" map-to="def:decimal"/>
    <style id="string" _name="String" map-to="def:string"/>
    <style id="keyword" _name="Keyword" map-to="def:keyword"/>
    <style id="meta-keyword" _name="Type, module or object keyword" map-to="def:keyword"/>
    <style id="fun-keyword" _name="Builtin-function keyword" map-to="def:keyword"/>
    <style id="type" _name="Data Type" map-to="def:type"/>
    <style id="label" _name="Labeled argument" map-to="def:type"/>
36
<!--
37
    <style id="poly-variant" _name="Polymorphic Variant" map-to="def:type"/>
38
-->
39 40 41 42 43
    <style id="variant" _name="Variant Constructor" map-to="def:type"/>
    <style id="type-var" _name="Type Variable" map-to="def:type"/>
    <style id="module" _name="Module Path" map-to="def:type"/>
    <style id="escape" _name="Escaped Character" map-to="def:special-char"/>
    <style id="boolean" _name="Boolean value" map-to="def:boolean"/>
44
    <style id="spec-keyword" _name="Specification keyword" map-to="def:shebang"/>
45 46
    <style id="error" _name="Error" map-to="def:error"/>
  </styles>
47

48 49 50 51
  <definitions>
    <define-regex id="cap-ident">\b[A-Z][A-Za-z0-9_']*</define-regex>
    <define-regex id="low-ident">\b[a-z][A-Za-z0-9_']*</define-regex>
    <define-regex id="char-esc">\\((\\|"|'|n|t|b|r)|[0-9]{3}|x[0-9a-fA-F]{2})</define-regex>
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
52
    <!-- " -->
53 54 55 56
    <context id="escape-seq" style-ref="escape">
      <match>\%{char-esc}</match>
    </context>
    <!-- here's the main context -->
57
    <context id="why3">
58
      <include>
Andrei Paskevich's avatar
Andrei Paskevich committed
59
	<context id="symbol-star">
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
60 61 62 63
	  <match>\(\*\)</match>
	</context>
	<context id="comment" style-ref="comment">
	  <start>\(\*</start>
64 65
	  <end>\*\)</end>
	  <include>
Andrei Paskevich's avatar
Andrei Paskevich committed
66
	    <context ref="symbol-star"/>
67 68 69 70 71
	    <context id="comment-in-comment" style-ref="comment">
	      <start>\(\*</start>
	      <end>\*\)</end>
	      <include>
		<context ref="string"/>
Andrei Paskevich's avatar
Andrei Paskevich committed
72
		<context ref="symbol-star"/>
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
		<context ref="comment-in-comment"/>
		<context ref="def:in-comment:*"/>
	      </include>
	    </context>
	    <context ref="string"/>
	    <context ref="def:in-comment:*"/>
	  </include>
	</context>
	<context id="decimal" style-ref="decimal">
	  <match>[-]?[0-9][0-9_]*[lLn]?</match>
	</context>
	<context id="hex-number" style-ref="base-n-integer">
	  <match>[-]?0[xX][0-9A-Fa-f][0-9A-Fa-f_]*[lL]?</match>
	</context>
	<context id="octal-number" style-ref="base-n-integer">
	  <match>[-]?0[oO][0-7][0-7_]*[lL]?</match>
	</context>
	<context id="binary-number" style-ref="base-n-integer">
	  <match>[-]?0[bB][01][01_]*[lL]?</match>
	</context>
	<context id="floating-point-number" style-ref="floating-point">
	  <match>[-]?[0-9][0-9_]*(\.[0-9_]*)?([Ee][+-]?[0-9][0-9_]*)?</match>
	</context>
96
<!--
97 98 99 100 101 102
	<context id="label" style-ref="label">
	  <match>[~?]\%{low-ident}</match>
	</context>
	<context id="poly-variant" style-ref="poly-variant">
	  <match>`\%{cap-ident}</match>
	</context>
103
-->
104 105 106 107 108 109 110 111 112 113 114 115 116 117
	<context id="modpath" style-ref="module">
	  <!-- include final '.'?  At the moment, no.  -->
	  <match>\%{cap-ident}(\.\%{cap-ident})*(?=\.)</match>
	</context>
	<context id="variant" style-ref="variant">
	  <match>\%{cap-ident}</match>
	</context>
	<context id="string" style-ref="string">
	  <start>"</start>
	  <end>"</end>
	  <include>
	    <context ref="escape-seq"/>
	  </include>
	</context>
118
<!--
119 120 121
	<context id="character-constant" style-ref="string">
	  <match>('\%{char-esc}')|('[^\\']')</match>
	</context>
122
-->
123 124 125
	<context id="type-var" style-ref="type-var">
	  <match>'\%{low-ident}</match>
	</context>
126 127 128 129
	<context id="recordlit">
	  <start>\{</start>
	  <end>\}</end>
	  <include>
130
	    <context ref="why3"/>
131 132 133 134 135 136
	  </include>
	</context>
	<context id="badrecord" style-ref="error" extend-parent="false">
	  <match>}</match>
	</context>
<!--
137 138 139 140
	<context id="arraylit">
	  <start>\[\|</start>
	  <end>\|\]</end>
	  <include>
141
	    <context ref="why3"/>
142 143 144 145 146 147 148 149 150
	  </include>
	</context>
	<context id="badarray" style-ref="error" extend-parent="false">
	  <match>\|\]</match>
	</context>
	<context id="listlit">
	  <start>\[</start>
	  <end>(?&lt;!\|)\]</end>
	  <include>
151
	    <context ref="why3"/>
152 153 154 155 156
	  </include>
	</context>
	<context id="badlist" style-ref="error" extend-parent="false">
	  <match>\]</match>
	</context>
157
-->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
158
	<context id="keywords" style-ref="meta-keyword">
159
          <keyword>abstract</keyword>
160 161
          <keyword>axiom</keyword>
          <keyword>clone</keyword>
162 163
          <keyword>coinductive</keyword>
          <keyword>constant</keyword>
164 165 166 167 168
          <keyword>end</keyword>
          <keyword>exception</keyword>
          <keyword>export</keyword>
          <keyword>function</keyword>
          <keyword>goal</keyword>
169
          <keyword>ghost</keyword>
170 171 172 173 174 175
          <keyword>import</keyword>
          <keyword>inductive</keyword>
          <keyword>lemma</keyword>
          <keyword>module</keyword>
          <keyword>namespace</keyword>
          <keyword>predicate</keyword>
176
          <keyword>private</keyword>
177 178 179 180 181
          <keyword>theory</keyword>
          <keyword>type</keyword>
          <keyword>use</keyword>
          <keyword>val</keyword>
          <keyword>with</keyword>
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
182 183
	</context>
	<context id="meta-words" style-ref="keyword">
184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201
          <keyword>begin</keyword>
          <keyword>do</keyword>
          <keyword>done</keyword>
          <keyword>downto</keyword>
          <keyword>else</keyword>
          <keyword>exists</keyword>
          <keyword>for</keyword>
          <keyword>forall</keyword>
          <keyword>if</keyword>
          <keyword>in</keyword>
          <keyword>let</keyword>
          <keyword>match</keyword>
          <keyword>raise</keyword>
          <keyword>rec</keyword>
          <keyword>then</keyword>
          <keyword>to</keyword>
          <keyword>try</keyword>
          <keyword>while</keyword>
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
202
	  <keyword>-&gt;</keyword>
203
	</context>
204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221
	<context id="spec" style-ref="spec-keyword">
          <keyword>absurd</keyword>
          <keyword>assert</keyword>
          <keyword>assume</keyword>
	  <keyword>ensures</keyword>
	  <keyword>check</keyword>
	  <keyword>invariant</keyword>
	  <keyword>raises</keyword>
	  <keyword>reads</keyword>
	  <keyword>requires</keyword>
	  <keyword>returns</keyword>
	  <keyword>variant</keyword>
	  <keyword>writes</keyword>
	</context>
	<context id="bool-const" style-ref="boolean">
	  <keyword>true</keyword>
	  <keyword>false</keyword>
	</context>
222
	<context id="types" style-ref="type">
223 224
	  <keyword>array</keyword>
	  <keyword>bool</keyword>
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
225
	  <keyword>int</keyword>
226 227 228
	  <keyword>list</keyword>
	  <keyword>map</keyword>
	  <keyword>option</keyword>
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
229
 	  <keyword>real</keyword>
230 231
	  <keyword>ref</keyword>
	  <keyword>unit</keyword>
232
	</context>
233 234 235
	<context id="var">
	  <match>\%{low-ident}</match>
	</context>
236 237 238
      </include>
    </context>
  </definitions>
239
</language>