256 lines
7.7 KiB
Ruby
256 lines
7.7 KiB
Ruby
# -*- 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
|