#!/usr/bin/ruby
# coding: utf-8

################################################################################
## CONFIG

Keyword = :keyword
Face    = Struct.new('Face', :name) do
  def inspect
    "Face(#{name})"
  end
end

def Face(x)
  Face.new(x)
end

def used?(cat)
  Keyword === cat || Face === cat
end

# Category types:
#   Keyword    - will be parsed for highlighting as a keyword
#   Face(name) - will be parsed for highlighting with the given face
#   :ignored   - lines in this section will be skipped
#   :done      - terminates parsing
CATEGORIES = { 'Edits'            => Keyword,
               'Coq terms'        => Face('font-lock-type-face'),
               'Coq commands'     => Face('font-lock-builtin-face'),
               
               'Coq punctuation'  => :ignored,
               'Ltac punctuation' => :ignored,
               'General'          => :ignored,
               
               'End'              => :done }

CUSTOM_KEYWORDS = { Face('font-lock-keyword-face') =>
                      ["^\\s-*\\<in\\>"],
                    Face('font-lock-builtin-face') =>
                      %w{Qed Defined Admitted}.map { |pe| "\\<#{pe}\\>" } }

################################################################################
## Output

def emacs_format_keywords(keywords)
  keywords = keywords.clone
  
  def face_keywords(fkws)
    fkws.flat_map { |face, kws| kws.map { |kw| "(#{quote(yield kw)} . #{face.name})" } }
  end

  plain_kws  = (keywords.delete(Keyword) || []).map { |kw| quote(kw) }
  face_kws   = face_keywords(keywords)        { |kw| "\\<#{regexp_quote(kw)}\\>" }
  custom_kws = face_keywords(CUSTOM_KEYWORDS) { |kw| kw }
  
  return [plain_kws, custom_kws + face_kws]
end

def emacs_mode_definition(directory, plain_kws, face_kws)
  def to_emacs(list)
    if !list || list.length == 0
      "nil"
    else
      "'(" + list.join(' ') + ")"
    end
  end
  
  <<ELISP
(define-generic-mode hs-to-coq-edits-mode
  '(?#)
  #{to_emacs(plain_kws)}
  #{to_emacs(face_kws)}
  '("[./]edits\\\\'")
  nil
  "Major mode for editing hs-to-coq edit files.

Automatically generated by `#{__FILE__}'.

\\{hs-to-coq-edits-mode-map}")
ELISP
end

def quote(s)
  '"' + s.gsub(/["\\]/) { |c| "\\#{c}" } + '"'
end

def regexp_quote(s)
  s.gsub(/[.*+?\[\]^$\\]/) { |c| "\\#{c}" }
end

################################################################################
## Utility functions

def die(*str)
  puts *str
  exit 1
end

################################################################################
## Parsing

module Token
  def self.start(line)
    !!/^%token\s*$/.match(line)
  end

  def self.category(line)
    match = /^ *-- Tokens: (.+)\s*$/.match(line)
    match and match[1]
  end

  def self.token(line)
    match = /^\s*(?:'((?:[^'\\]|\\.)+)'|(\S+))\s*{ Tok(Word|Op) +"((?:[^"\\]|\\.)+)" +}$/.match(line)
    
    name = if match[1] then match[1].gsub(/\\(.)/, '\1') else match[2] end
    type = match[3]
    tok  = match[4].gsub(/\\(.)/) { if '"\\'.includes? $1 then $1 else die "Unknown escape \\#{$1}" end }

    die "Token name and value differ: `#{name}' ≠ `#{tok}'" unless name == tok
    
    # Don't need type
    tok
  end

  def self.empty(line)
    !!/^\s*$/.match(line)
  end
end

################################################################################
## State machine

# :phase    -> :init, :tokens
# :category -> nil, CATEGORIES.keys
# :keywords -> {category => [String]}
class Parser
  attr_reader :phase, :category_type, :keywords
  
  def initialize
    @phase         = :init
    @category_type = nil
    @keywords      = {}
  end

  def to_s
    "#<Parser phase=#{@phase}, category_type=#{@category_type}, keywords=#{@keywords}>"
  end

  def self.parse_lines(lines)
    parser = self.new()
    lines.each { |line| parser.parse(line) or break }
    parser.keywords
  end
  
  def parse(line)
    case @phase
    when :init
      if Token.start(line)
        @phase = :tokens
      end
      return true
    when :tokens
      category = Token.category(line)
      if category then
        @category_type = CATEGORIES[category]
        case @category_type
        when :done
          return false
        when nil
          die "Unknown category #{category}"
        end
        @keywords[@category_type] ||= [] if used?(@category_type)
        return true
      end

      return true if @category_type == :ignored
      return true if Token.empty(line)

      token = Token.token(line)
      if token
        die "No token category specified" unless @category_type
        @keywords[@category_type] << token
        return true
      end

      die "Could not parse line:", line
    else
      die "INTERNAL ERROR: Unknown phase #{@phase}"
    end
  end
end

################################################################################
## Main

def main()
  die "#{$0} [INPUT]" if ARGV.length > 1
  keywords = Parser.parse_lines(ARGF.each_line)
  puts emacs_mode_definition(File.dirname(File.absolute_path(__FILE__)),
                             *emacs_format_keywords(keywords))
end

main() if __FILE__ == $0
