<?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:preprocessor"/>
    <style id="toplevel" _name="Toplevel"  map-to="def:keyword"/>
    <style id="operator" _name="Operator" map-to="def:preprocessor"/>
    <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:comment"/>
    <style id="special" _name="Special" map-to="def:special-char"/>
    <!-- <style id="axiom" _name="Axiom" map-to="def:function"/> -->
    <style id="definition-name" _name="Name" map-to="def:function"/>
    <style id="theory-name" _name="Theory" map-to="def:string"/>
  </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>in</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>check</keyword>
	  <keyword>cut</keyword>
	  <keyword>include</keyword>
	  <keyword>end</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="special" style-ref="special">
	  <match>\?</match>
	</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>\|-&gt;|&lt;-&gt;|-&gt;|[\%\*+-]</match>
	</context>

        <context id="type" style-ref="toplevel">
          <match>type\s+((('\%{ident}|\('\%{ident}(, '\%{ident})*\)) )?\%{ident})</match>
          <include>
            <context id="type-name" sub-pattern="1"
                     style-ref="type"/>
          </include>
        </context>

        <context id="logic">
          <match>(logic)\s+(\%{ident})(\s*,\s*(\%{ident}))*</match>
          <include>
            <context id="logic-name" sub-pattern="1"
                     style-ref="toplevel"/>
            <context id="logic-name" sub-pattern="2"
                     style-ref="definition-name"/>
            <context id="logic-name" sub-pattern="4"
                     style-ref="definition-name"/>
          </include>
        </context>

        <context id="axiom" style-ref="toplevel">
          <match>axiom\s+(\%{ident})</match>
          <include>
            <context id="axiom-name" sub-pattern="1"
                     style-ref="definition-name"/>
          </include>
        </context>

        <context id="hypothesis" style-ref="toplevel">
          <match>hypothesis\s+(\@?_?\%{ident})</match>
          <include>
            <context id="hyp-name" sub-pattern="1"
                     style-ref="definition-name"/>
          </include>
        </context>

        <context id="goal" style-ref="toplevel">
          <match>goal\s+(\%{ident})</match>
          <include>
            <context id="goal-name" sub-pattern="1"
                     style-ref="definition-name"/>
          </include>
        </context>

        <context id="theory_ext" style-ref="toplevel">
          <match>theory\s+(\%{ident})\s+extends\s+(\%{ident})</match>
          <include>
            <context id="theory-name" sub-pattern="1"
                     style-ref="theory-name"/>
            <context id="theoey-extend-name" sub-pattern="2"
                     style-ref="theory-name"/>
          </include>
        </context>

        <context id="theory" style-ref="toplevel">
          <match>theory\s+(\%{ident})</match>
          <include>
            <context id="theory-name" sub-pattern="1"
                     style-ref="theory-name"/>
          </include>
        </context>

        <context id="function" style-ref="toplevel">
          <match>(function|predicate|inversion|rewriting|instance)\s+(\%{ident})</match>
          <include>
            <context id="function-k" sub-pattern="1"
                     style-ref="toplevel"/>
            <context id="function-name" sub-pattern="2"
                     style-ref="definition-name"/>
          </include>
        </context>

	<context id="trigger" style-ref="trigger">
	  <!-- <match>\[.*\]({.*})?(\s|\n)*\.</match> -->
	  <start> \[</start>
	  <end>(\]|})\.</end>
	  <include>
	    <context ref="boolean-constant"/>
	    <context ref="keywords"/>
	    <context ref="types"/>
	    <context ref="special"/>
	    <context ref="integer"/>
	    <context ref="real"/>
	    <context ref="hex-number"/>
	    <context ref="poly-variant"/>
	    <context ref="op"/>
	    <context ref="type-var"/>
	    <context ref="bitv"/>
	  </include>
	</context>
<!--
	<context id="badtrigger" style-ref="error" extend-parent="false">
	  <match>\]</match>
	</context>
-->
      </include>
    </context>
  </definitions>
</language>