<?xml version="1.0" encoding="UTF-8"?>
<!--

 Author: Alain Mebsout

-->
<language id="alt-ergo" _name="Alt-Ergo" version="2.0" _section="Sources">
  <metadata>
    <property name="mimetypes">text/x-alt-ergo</property>
    <!-- Conflict with Why3 -->
    <!-- <property name="globs">*.mlw;*.why</property> -->
    <property name="block-comment-start">(*</property>
    <property name="block-comment-end">*)</property>
  </metadata>

  <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="real" _name="Real" map-to="def:floating-point"/>
    <style id="integer" _name="Interger" map-to="def:decimal"/>
    <style id="keyword" _name="Keyword" map-to="def:keyword"/>
    <style id="toplevel" _name="Toplevel"  map-to="def:identifier"/>
    <style id="operator" _name="Operator" map-to="def:operator"/>
    <style id="type" _name="Data Type" map-to="def:type"/>
    <style id="label" _name="Labeled argument" map-to="def:type"/>
    <style id="poly-variant" _name="Polymorphic Variant" map-to="def:type"/>
    <style id="variant" _name="Variant Constructor" map-to="def:type"/>
    <style id="type-var" _name="Type Variable" map-to="def:type"/>
    <style id="boolean" _name="Boolean value" map-to="def:boolean"/>
    <style id="error" _name="Error" map-to="def:error"/>
    <style id="trigger" _name="Trigger" map-to="def:doc-comment-element"/>
  </styles>

  <definitions>
    <define-regex id="digit">[0-9]</define-regex>
    <define-regex id="hexa">[0-9a-fA-F]</define-regex>
    <define-regex id="ident">[A-Za-z][A-Za-z0-9_']*</define-regex>
    <define-regex id="exponent">[pP][-+]?[0-9][0-9]*</define-regex>
    <!-- here's the main context -->
    <context id="alt-ergo">
      <include>

	<context id="comment" style-ref="comment">
	  <start>\(\*</start>
	  <end>\*\)</end>
	  <include>
	    <context ref="def:in-comment:*"/>
	  </include>
	</context>


	<context id="boolean-constant" style-ref="boolean">
	  <keyword>true</keyword>
	  <keyword>false</keyword>
	  <keyword>void</keyword>
	</context>
	<!-- Flow control & common keywords -->
	<context id="keywords" style-ref="keyword">
	  <keyword>and</keyword>
	  <keyword>distinct</keyword>
	  <keyword>else</keyword>
	  <keyword>exists</keyword>
	  <keyword>forall</keyword>
	  <keyword>if</keyword>
	  <keyword>not</keyword>
	  <keyword>or</keyword>
	  <keyword>reach</keyword>
	  <keyword>then</keyword>
	  <keyword>with</keyword>
	</context>
	<context id="toplevel" style-ref="toplevel">
	  <keyword>ac</keyword>
	  <keyword>axiom</keyword>
	  <keyword>check</keyword>
	  <keyword>cut</keyword>
	  <keyword>function</keyword>
	  <keyword>goal</keyword>
	  <keyword>hypothesis</keyword>
	  <keyword>include</keyword>
	  <keyword>instance</keyword>
	  <keyword>inversion</keyword>
	  <keyword>logic</keyword>
	  <keyword>predicate</keyword>
	  <keyword>rewriting</keyword>
	  <keyword>type</keyword>	
        </context>
	<context id="types" style-ref="type">
	  <!-- pervasives types -->
	  <keyword>bool</keyword>
	  <keyword>int</keyword>
	  <keyword>bitv</keyword>
	  <keyword>prop</keyword>
	  <keyword>real</keyword>
	  <keyword>unit</keyword>
	  <!-- note: Some and None are highlighted as variants -->
	</context>	
	
	<context id="integer" style-ref="integer">
	  <match>\%{digit}(\%{digit})*</match>
	</context>
	
	<context id="real" style-ref="real">
	  <match>\%{digit}(\%{digit})*\.(\%{digit})*</match>
	</context>
	<context id="hex-number" style-ref="real">
	  <match>0x\%{hexa}(\%{hexa})*(\.(\%{hexa})*)?\%{exponent}</match>
	</context>

	<context id="poly-variant" style-ref="poly-variant">
	  <match>`\%{ident}</match>
	</context>

	<context id="type-var" style-ref="type-var">
	  <match>'\%{ident}</match>
	</context>

	<context id="ident">
	  <match>\%{ident}</match>
	</context>
	
	<context id="bitv" style-ref="integer">
	  <match>\[[01][01]*\]</match>
	</context>

	<context id="op" style-ref="operator">
	  <match>[\%\*+-]</match>
	</context>

	<context id="trigger" style-ref="trigger">
	  <match>\[.*\]\.</match>
	</context>
<!--
	<context id="badtrigger" style-ref="error" extend-parent="false">
	  <match>\]</match>
	</context>
-->
      </include>
    </context>
  </definitions>
</language>