Class: Rouge::Lexers::Coq

Inherits:
RegexLexer show all
Defined in:
lib/rouge/lexers/coq.rb

Constant Summary

Constants inherited from RegexLexer

RegexLexer::MAX_NULL_SCANS

Constants included from Token::Tokens

Token::Tokens::Num, Token::Tokens::Str

Instance Attribute Summary

Attributes inherited from Rouge::Lexer

#options

Class Method Summary collapse

Methods inherited from RegexLexer

append, #delegate, get_state, #get_state, #goto, #group, #groups, #in_state?, #pop!, prepend, #push, #recurse, replace_state, #reset!, #reset_stack, #stack, start, start_procs, #state, state, #state?, state_definitions, states, #step, #stream_tokens, #token

Methods inherited from Rouge::Lexer

aliases, all, #as_bool, #as_lexer, #as_list, #as_string, #as_token, assert_utf8!, #bool_option, debug_enabled?, demo, demo_file, desc, detect?, disable_debug!, enable_debug!, filenames, find, find_fancy, guess, guess_by_filename, guess_by_mimetype, guess_by_source, guesses, #hash_option, #initialize, lex, #lex, #lexer_option, #list_option, mimetypes, option, option_docs, #reset!, #stream_tokens, #string_option, tag, #tag, title, #token_option

Methods included from Token::Tokens

token

Constructor Details

This class inherits a constructor from Rouge::Lexer

Class Method Details

.classify(x) ⇒ Object 



68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
 
# File 'lib/rouge/lexers/coq.rb', line 68

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

.coq ⇒ Object 



18
19
20
21
22
23
24
25
26
27
28
29
 
# File 'lib/rouge/lexers/coq.rb', line 18

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
  )
end

.end_sentence ⇒ Object 



64
65
66
 
# File 'lib/rouge/lexers/coq.rb', line 64

def self.end_sentence
  @end_sentence ||= Punctuation::Indicator
end

.gallina ⇒ Object 



11
12
13
14
15
16
 
# File 'lib/rouge/lexers/coq.rb', line 11

def self.gallina
  @gallina ||= Set.new %w(
    as fun if in let match then else return end Type Set Prop
    forall
  )
end

.keyopts ⇒ Object 



58
59
60
61
62
 
# File 'lib/rouge/lexers/coq.rb', line 58

def self.keyopts
  @keyopts ||= Set.new %w(
    := => -> /\\ \\/ _ ; :> :
  )
end

.ltac ⇒ Object 



31
32
33
34
35
36
37
38
39
40
41
42
43
 
# File 'lib/rouge/lexers/coq.rb', line 31

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

.tacticals ⇒ Object 



45
46
47
48
49
 
# File 'lib/rouge/lexers/coq.rb', line 45

def self.tacticals
  @tacticals ||= Set.new %w(
    repeat first try
  )
end

.terminators ⇒ Object 



51
52
53
54
55
56
 
# File 'lib/rouge/lexers/coq.rb', line 51

def self.terminators
  @terminators ||= Set.new %w(
    omega solve congruence reflexivity exact
    assumption eassumption
  )
end