coq-elpi.lang

<?xml version="1.0" encoding="UTF-8"?>
<language id="coq-elpi" _name="Coq + ELPI" version="2.0" _section="Scientific">
  <metadata>
    <property name="globs">*.v</property>
    <property name="block-comment-start">\(\*</property>
    <property name="block-comment-stop">\*\)</property>
  </metadata>
  
  <styles>
    <style id="comment" _name="Comment" map-to="def:comment"/>
    <style id="coqdoc" _name="Coqdoc text" map-to="def:note"/>
    <style id="vernac-keyword" _name="Vernacular keyword" map-to="def:keyword"/>
    <style id="gallina-keyword" _name="Gallina keyword" map-to="def:keyword"/>
    <style id="identifier" _name="Identifier" map-to="def:identifier"/>
    <style id="constr-keyword" _name="Cic keyword" map-to="def:keyword"/>
    <style id="constr-sort" _name="Cic sort" map-to="def:builtin"/>
    <style id="string" _name="String" map-to="def:string"/>
    <style id="escape" _name="Escaped Character" map-to="def:special-char"/>
    <style id="error" _name="Error" map-to="def:error"/>
    <style id="safe" _name="Checked Part"/>
    <style id="sentence" _name="Sentence terminator"/>
    <style id="tactic" _name="Tactic"/>
    <style id="endtactic" _name="Tactic terminator"/>
    <style id="iterator" _name="Tactic iterator"/>
  </styles>
  
  <definitions>
    <define-regex id="space">\s</define-regex>
    <define-regex id="first_ident_char">[_\p{L}]</define-regex>
    <define-regex id="ident_char">[_\p{L}'\pN]</define-regex>
    <define-regex id="ident">\%{first_ident_char}\%{ident_char}*</define-regex>
    <define-regex id="qualit">(\%{ident}*\.)*\%{ident}</define-regex>
    <define-regex id="undotted_sep">[-+*{}]</define-regex>
    <define-regex id="dot_sep">\.(\s|\z)</define-regex>
    <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Canonical)|(Coercion)</define-regex>
    <define-regex id="mult_decl">(Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)</define-regex>
    <define-regex id="locality">(((Local)|(Global))\%{space}+)?</define-regex>
    <define-regex id="begin_proof">(Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)</define-regex>
    <define-regex id="end_proof">(Qed)|(Defined)|(Admitted)|(Abort)</define-regex>
    <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))</define-regex>
    <define-regex id="lp-var">[A-Z_][A-Za-z-+_0-9?]*</define-regex>
    <define-regex id="lp-name">[a-z][A-Za-z-+_>0-9?\.]*</define-regex>
    <define-regex id="lp-symb">(:-|\\|,|=>|\]|\[)</define-regex>
    <define-regex id="lp-comment">%.*\z</define-regex>

    <context id="escape-seq" style-ref="escape">
      <match>""</match>
    </context>
    <context id="string" style-ref="string">
      <start>"</start>
      <end>"</end>
      <include>
	<context ref="escape-seq"/>
      </include>
    </context>
    <context id="ssr-iter" style-ref="iterator">
      <keyword>do</keyword>
      <keyword>last</keyword>
      <keyword>first</keyword>
    </context>
    <context id="ssr-tac" style-ref="tactic">
      <keyword>apply</keyword>
      <keyword>auto</keyword>
      <keyword>case</keyword>
      <keyword>case</keyword>
      <keyword>congr</keyword>
      <keyword>elim</keyword>
      <keyword>exists</keyword>
      <keyword>have</keyword>
      <keyword>gen have</keyword>
      <keyword>generally have</keyword>
      <keyword>move</keyword>
      <keyword>pose</keyword>
      <keyword>rewrite</keyword>
      <keyword>set</keyword>
      <keyword>split</keyword>
      <keyword>suffices</keyword>
      <keyword>suff</keyword>
      <keyword>transitivity</keyword>
      <keyword>without loss</keyword>
      <keyword>wlog</keyword>
    </context>
    <context id="ssr-endtac" style-ref="endtactic">
      <keyword>by</keyword>
      <keyword>exact</keyword>
      <keyword>reflexivity</keyword>
    </context>
    <context id="coq-elpi" class="no-spell-check">
      <include>
       <context ref="string"/> 
	<context id="coqdoc" style-ref="coqdoc" class-disabled="no-spell-check">
	  <start>\(\*\*(\s|\z)</start>
	  <end>\*\)</end>
	  <include>
	    <context ref="comment-in-comment"/>
	    <context ref="string"/>
	    <context ref="escape-seq"/>
	  </include>
	</context>
	<context id="comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
	  <start>\(\*</start>
	  <end>\*\)</end>
	  <include>
	    <context id="comment-in-comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
	      <start>\(\*</start>
	      <end>\*\)</end>
	      <include>
		<context ref="comment-in-comment"/>
		<context ref="string"/>
		<context ref="escape-seq"/>
	      </include>
	    </context>
	    <context ref="string"/>
	    <context ref="escape-seq"/>
	  </include>
	</context>
	<context id="declaration">
	  <start>\%{decl_head}</start>
	  <end>\%{dot_sep}</end>
	  <include>
	    <context sub-pattern="id" where="start" style-ref="identifier"/>
	    <context sub-pattern="gal" where="start" style-ref="gallina-keyword"/>
	    <context sub-pattern="id_list" where="start" style-ref="identifier"/>
	    <context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/>
	    <context id="constr-keyword" style-ref="constr-keyword">
	      <keyword>forall</keyword>
	      <keyword>fun</keyword>
	      <keyword>match</keyword>
	      <keyword>fix</keyword>
	      <keyword>cofix</keyword>
	      <keyword>with</keyword>
	      <keyword>for</keyword>
	      <keyword>end</keyword>
	      <keyword>as</keyword>
	      <keyword>let</keyword>
	      <keyword>in</keyword>
	      <keyword>if</keyword>
	      <keyword>then</keyword>
	      <keyword>else</keyword>
	      <keyword>return</keyword>
	      <keyword>using</keyword>
	    </context>
	    <context id="constr-sort" style-ref="constr-keyword">
	      <keyword>Prop</keyword>
	      <keyword>Set</keyword>
	      <keyword>Type</keyword>
	    </context>
	    <context id="dot-nosep">
	      <match>\.\.</match>
	    </context>
	    <context ref="comment"/>
	    <context ref="string"/>
	    <context ref="coqdoc"/>
	  </include>
	</context>
	<context id="proof">
	  <start>Proof</start>
	  <end>\%{end_proof}\%{dot_sep}</end>
	  <include>
	    <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
	    <context sub-pattern="0" where="end" style-ref="vernac-keyword"/>
	    <context ref="command"/>
	    <context ref="scope-command"/>
	    <context ref="hint-command"/>
	    <context ref="command-for-qualit"/>
	    <context ref="declaration"/>
	    <context ref="comment"/>
	    <context ref="string"/>
	    <context ref="coqdoc"/>
	    <context ref="proof"/>
	    <context ref="undotted-sep"/>
	    <context id="tactic" extend-parent="false">
              <start></start>
              <end>\%{dot_sep}</end>
	      <include>
	        <context ref="ssr-tac"/>
	        <context ref="ssr-endtac"/>
	        <context ref="ssr-iter"/>
		<context ref="dot-nosep"/>
		<context ref="constr-keyword"/>
		<context ref="constr-sort"/>
	        <context ref="comment"/>
	        <context ref="string"/>
	      </include>
	    </context>
	  </include>
	</context>
	<context id="undotted-sep" style-ref="vernac-keyword">
	  <match>\%{undotted_sep}</match>
	</context>
	<context id="elpi">
		<start>(Elpi\%{space}+Accumulate\%{space}+lp:{{|Elpi\%{space}+Db\%{space}+\%{qualit}\%{space}+lp:{{|Elpi\%{space}+Query\%{space}+lp:{{|Elpi\%{space}+Query\%{space}+\%{qualit}\%{space}+lp:{{|Elpi\%{space}+Command\%{space}+\%{qualit}\%{space}+lp:{{|Elpi\%{space}+Tactic\%{space}+\%{qualit}\%{space}+lp:{{|Elpi\%{space}+Program\%{space}+\%{qualit}\%{space}+lp:{{)</start>
	  <end>}}\%{dot_sep}</end>
	  <include>
	    <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
	    <context sub-pattern="0" where="end" style-ref="vernac-keyword"/>
		<context id="HOAS" style-ref="escape">
		  <keyword>fun</keyword>
		  <keyword>prod</keyword>
		  <keyword>sort</keyword>
		  <keyword>let</keyword>
		  <keyword>match</keyword>
		  <keyword>fix</keyword>
		  <keyword>indc</keyword>
		  <keyword>indt</keyword>
		  <keyword>const</keyword>
		  <keyword>prop</keyword>
		  <keyword>app</keyword>
		  <keyword>global</keyword>
		</context>
		<context id="typing-keyword" style-ref="vernac-keyword">
			<keyword>type</keyword>
			<keyword>kind</keyword>
			<keyword>pi</keyword>
			<keyword>sigma</keyword>
			<keyword>rule</keyword>
			<keyword>constraint</keyword>
			<keyword>namespace</keyword>
		</context>
		  <context id="lp-var" style-ref="constr-keyword">
			  <match>\%{lp-var}</match>
		  </context>
		  <context id="lp-name" style-ref="identifier">
			  <match>\%{lp-name}</match>
		  </context>
                <context id="nested-string" style-ref="string">
                 <start>""</start>
                 <end>""</end>
	        </context>
		<context id="symbols" style-ref="def:special-char">
			<match>\%{lp-symb}</match>
		</context>
		<context id="lp-comment" style-ref="comment">
			<match>\%{lp-comment}</match>
		</context>
       </include>
        </context>
	<context id="command" style-ref="vernac-keyword">
	  <keyword>Add</keyword>
	  <keyword>Check</keyword>
	  <keyword>Eval</keyword>
	  <keyword>Load</keyword>
	  <keyword>Undo</keyword>
          <keyword>Restart</keyword>
	  <keyword>Goal</keyword>
	  <keyword>Print</keyword>
	  <keyword>Save</keyword>
	  <keyword>Comments</keyword>
	  <keyword>Solve\%{space}+Obligation</keyword>
	  <keyword>((Uns)|(S))et(\%{space}+\%{ident})+</keyword>
	  <keyword>(\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation</keyword>
	  <keyword>\%{locality}Infix</keyword>
	  <keyword>(Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist)</keyword>
	  <keyword>(Elpi\%{space}+Trace)|(Elpi\%{space}+Accumulate\%{space}+File)|(Elpi\%{space}+Accumulate\%{space}+Db)|(Elpi\%{space}+Accumulate)|(Elpi\%{space}+Query)|(Elpi\%{space}+Bound\%{space}+Steps)|(Elpi\%{space}+Program)|(Elpi\%{space}+\%{qualit})</keyword>
	</context>
	<context id="hint-command" style-ref="vernac-keyword">
	  <prefix>\%{locality}Hint\%{space}+</prefix>
	  <keyword>Resolve</keyword>
	  <keyword>Immediate</keyword>
	  <keyword>Constructors</keyword>
	  <keyword>unfold</keyword>
	  <keyword>Opaque</keyword>
	  <keyword>Transparent</keyword>
	  <keyword>Extern</keyword>
	</context>
	<context id="scope-command" style-ref="vernac-keyword">
	  <suffix>\%{space}+Scope</suffix>
	  <keyword>\%{locality}Open</keyword>
	  <keyword>\%{locality}Close</keyword>
	  <keyword>Bind</keyword>
	  <keyword>Delimit</keyword>
	</context>
	<context id="command-for-qualit">
	  <suffix>\%{space}+(?'qua'\%{qualit})</suffix>
	  <keyword>Chapter</keyword>
	  <keyword>Combined\%{space}+Scheme</keyword>
	  <keyword>End</keyword>
	  <keyword>Section</keyword>
	  <keyword>Arguments</keyword>
	  <keyword>Implicit\%{space}+Arguments</keyword>
	  <keyword>(Import)|(Include)</keyword>
	  <keyword>Require(\%{space}+((Import)|(Export)))?</keyword>
	  <keyword>(Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))?</keyword>
	  <keyword>Extract\%{space}+(Inlined\%{space}+)?(Constant)|(Inductive)</keyword>
	  <include>
	    <context sub-pattern="1" style-ref="vernac-keyword"/>
	  </include>
	</context>
	<context id="command-for-qualit-list" style-ref="vernac-keyword">
	  <suffix>(?'qua_list'(\%{space}+\%{qualit})+)</suffix>
	  <keyword>Typeclasses (Transparent)|(Opaque)</keyword>
	  <include>
	    <context sub-pattern="qua_list" style-ref="identifier"/>
	  </include>
	</context>
      </include>
    </context>
  </definitions>
</language>