# -*- coding: utf-8 -*- #
# frozen_string_literal: true
module Rouge
module Lexers
class Coq < RegexLexer
title "Coq"
desc 'Coq (coq.inria.fr)'
tag 'coq'
mimetypes 'text/x-coq'
def self.gallina
@gallina ||= Set.new %w(
as fun if in let match then else return end Type Set Prop
forall
)
end
def self.coq
@coq ||= Set.new %w(
Definition Theorem Lemma Remark Example Fixpoint CoFixpoint
Record Inductive CoInductive Corollary Goal Proof
Ltac Require Import Export Module Section End Variable
Context Polymorphic Monomorphic Universe Universes
Variables Class Instance Global Local Include
Printing Notation Infix Arguments Hint Rewrite Immediate
Qed Defined Opaque Transparent Existing
Compute Eval Print SearchAbout Search About Check Admitted
)
end
def self.ltac
@ltac ||= Set.new %w(
apply eapply auto eauto rewrite setoid_rewrite
with in as at destruct split inversion injection
intro intros unfold fold cbv cbn lazy subst
clear symmetry transitivity etransitivity erewrite
edestruct constructor econstructor eexists exists
f_equal refine instantiate revert simpl
specialize generalize dependent red induction
beta iota zeta delta exfalso autorewrite setoid_rewrite
compute vm_compute native_compute
)
end
def self.tacticals
@tacticals ||= Set.new %w(
repeat first try
)
end
def self.terminators
@terminators ||= Set.new %w(
omega solve congruence reflexivity exact
assumption eassumption
)
end
def self.classify(x)
if self.coq.include? x
return Keyword
elsif self.gallina.include? x
return Keyword::Reserved
elsif self.ltac.include? x
return Keyword::Pseudo
elsif self.terminators.include? x
return Name::Exception
elsif self.tacticals.include? x
return Keyword::Pseudo
else
return Name::Constant
end
end
# https://github.com/coq/coq/blob/110921a449fcb830ec2a1cd07e3acc32319feae6/clib/unicode.ml#L67
# https://coq.inria.fr/refman/language/core/basic.html#grammar-token-ident
id_first = /\p{L}/
id_first_underscore = /(?:\p{L}|_)/
id_subsequent = /(?:\p{L}|\p{N}|_|')/ # a few missing? some mathematical ' primes and subscripts
id = /(?:#{id_first}#{id_subsequent}*)|(?:#{id_first_underscore}#{id_subsequent}+)/i
dot_id = /\.(#{id})/i
dot_space = /\.(\s+)/
state :root do
mixin :begin_proof
mixin :sentence
end
state :sentence do
mixin :comment_whitespace
mixin :module_setopts
# After parsing the id, end up in sentence_postid
rule id do |m|
@name = m[0]
@id_dotted = false
push :sentence_postid
push :continue_id
end
end
state :begin_proof do
rule %r/(Proof)(\s*)(\.)(\s+)/i do
groups Keyword, Text::Whitespace, Punctuation::Indicator, Text::Whitespace
push :proof_mode
end
end
state :proof_mode do
mixin :comment_whitespace
mixin :module_setopts
mixin :begin_proof
rule %r/(Qed|Defined|Save|Admitted)(\s*)(\.)(\s+)/i do
groups Keyword, Text::Whitespace, Punctuation::Indicator, Text::Whitespace
pop!
end
# the whole point of parsing Proof/Qed, normally some of these will be operators
rule %r/(?:\-+|\++|\*+)/, Punctuation
rule %r/[{}]/, Punctuation
# toplevel_selector
rule %r/(!|all|par)(:)/ do
groups Keyword::Pseudo, Punctuation
end
# numbered goals 1: {} 1,2: {}
rule %r/\d+/, Num::Integer, :numeric_labels
# [named_goal]: { ... }
rule %r/(\[)(\s*)(#{id})(\s*)(\])(\s*)(:)/ do
groups Punctuation, Text::Whitespace, Name::Constant, Text::Whitespace, Punctuation, Text::Whitespace, Punctuation
end
# After parsing the id, end up in sentence_postid
rule id do |m|
@name = m[0]
@id_dotted = false
push :sentence_postid
push :continue_id
end
end
state :numeric_labels do
mixin :whitespace
rule %r/(,)(\s*)(\d+)/ do
groups Punctuation, Text::Whitespace, Num::Integer
end
rule %r(:), Punctuation, :pop!
end
state :whitespace do
rule %r/\s+/m, Text::Whitespace
end
state :comment_whitespace do
rule %r/[(][*](?![)])/, Comment, :comment
mixin :whitespace
end
state :module_setopts do
rule %r/(Module)(\s+)(Type)(\s+)/ do
groups Keyword, Text::Whitespace, Keyword, Text::Whitespace
end
rule %r(
(Set|Unset)(\s+)
(Universe|Printing|Implicit|Strict)(\s+)
(Polymorphism|All|Notations|Arguments|Universes|Implicit)?(\s*)(\.)
)x do
groups Keyword, Text::Whitespace, Keyword, Text::Whitespace, Keyword, Text::Whitespace, Punctuation::Indicator
end
end
state :sentence_postid do
mixin :comment_whitespace
mixin :module_setopts
# up here to beat the id rule for lambda
rule %r(:=|=>|;|:>|:|::|_), Punctuation
rule %r(->|/\\|\\/|;|:>|[⇒→↔⇔≔≡∀∃∧∨¬⊤⊥⊢⊨∈λ]), Operator
rule id do |m|
@name = m[0]
@id_dotted = false
push :continue_id
end
# must be followed by whitespace, so that we don't match notations like sym.(a + b)
rule %r/\.(?=\s)/, Punctuation::Indicator, :pop! # :sentence_postid
rule %r/-?\d[\d_]*(.[\d_]*)?(e[+-]?\d[\d_]*)/i, Num::Float
rule %r/-?\d[\d_]*/, Num::Integer
rule %r/'(?:(\\[\\"'ntbr ])|(\\[0-9]{3})|(\\x\h{2}))'/, Str::Char
rule %r/'/, Keyword
rule %r/"/, Str::Double, :string
rule %r/[~?]#{id}/, Name::Variable
rule %r(`{|[{}\[\]()?|;,.]), Punctuation
rule %r([!@^|~#.%/]+), Operator
# any other combo of S (symbol), P (punctuation) and some extras just to be sure
rule %r((?:\p{S}|\p{Pc}|[./\:\<=>\-+*])+), Operator
rule %r/./, Error
end
state :comment do
rule %r/[^(*)]+/, Comment
rule(/[(][*]/) { token Comment; push }
rule %r/[*][)]/, Comment, :pop!
rule %r/[(*)]/, Comment
end
state :string do
rule %r/[^"]+/, Str::Double
rule %r/""/, Str::Double
rule %r/"/, Str::Double, :pop!
end
state :continue_id do
# the stream starts with an id (stored in @name) and continues here
rule dot_id do |m|
token Name::Namespace, @name
token Punctuation, '.'
@id_dotted = true
@name = m[1]
end
rule dot_space do |m|
if @id_dotted
token Name::Constant, @name
else
token self.class.classify(@name), @name
end
token Punctuation::Indicator, '.'
token Text::Whitespace, m[1]
@name = false
@id_dotted = false
pop! # :continue_id
pop! # :sentence_postid
end
rule %r// do
if @id_dotted
token Name::Constant, @name
else
token self.class.classify(@name), @name
end
@name = false
@id_dotted = false
# we finished parsing an id, drop back into the sentence_postid that was pushed first.
pop! # :continue_id
end
end
end
end
end