//===-- Lexer.h -------------------------------------------------*- C++ -*-===//
//
//                     The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//

#ifndef KLEE_EXPR_LEXER_H
#define KLEE_EXPR_LEXER_H

#include <string>

namespace llvm {
  class MemoryBuffer;
}

namespace klee {
namespace expr {
  struct Token {
    enum Kind {
      At,                       /// '@'
      Arrow,                    /// '->'
      Colon,                    /// ':'
      Comma,                    /// ','
      Comment,                  /// #[^\n]+
      EndOfFile,                /// <end of file>
      Equals,                   /// ' = '
      Identifier,               /// [a-zA-Z_][a-zA-Z0-9._]*
      KWArray,                  /// 'array'
      KWFalse,                  /// 'false'
      KWQuery,                  /// 'query'
      KWReserved,               /// fp[0-9]+([.].*)?, i[0-9]+
      KWSymbolic,               /// 'symbolic'
      KWTrue,                   /// 'true'
      KWWidth,                  /// w[0-9]+
      LBrace,                   /// '{'
      LParen,                   /// '('
      LSquare,                  /// '['
      Number,                   /// [+-]?[0-9][a-zA-Z0-9_]+
      RBrace,                   /// '}'
      RParen,                   /// ')'
      RSquare,                  /// ']'
      Semicolon,                /// ';'
      Unknown,                   /// <other>
      
      KWKindFirst=KWArray,
      KWKindLast=KWWidth
    };

    Kind        kind;           /// The token kind.
    const char *start;          /// The beginning of the token string. 
    unsigned    length;         /// The length of the token.
    unsigned    line;           /// The line number of the start of this token.
    unsigned    column;         /// The column number at the start of
                                /// this token.

    /// getKindName - The name of this token's kind.
    const char *getKindName() const;

    /// getString - The string spanned by this token. This is not
    /// particularly efficient, use start and length when reasonable.
    std::string getString() const { return std::string(start, length); }

    /// isKeyword - True if this token is a keyword.
    bool isKeyword() const { 
      return kind >= KWKindFirst && kind <= KWKindLast; 
    }

    // dump - Dump the token to stderr.
    void dump();
  };

  /// Lexer - Interface for lexing tokens from a .pc language file.
  class Lexer {
    const char *BufferPos;      /// The current lexer position.
    const char *BufferEnd;      /// The buffer end position.
    unsigned    LineNumber;     /// The current line.
    unsigned    ColumnNumber;   /// The current column.

    /// GetNextChar - Eat a character or -1 from the stream.
    int GetNextChar();

    /// PeekNextChar - Return the next character without consuming it
    /// from the stream. This does not perform newline
    /// canonicalization.
    int PeekNextChar();

    /// SetTokenKind - Set the token kind and length (using the
    /// token's start pointer, which must have been initialized).
    Token &SetTokenKind(Token &Result, Token::Kind k);

    /// SetTokenKind - Set an identifiers token kind. This has the
    /// same requirements as SetTokenKind and additionally takes care
    /// of keyword recognition.
    Token &SetIdentifierTokenKind(Token &Result);
  
    void SkipToEndOfLine();

    /// LexNumber - Lex a number which does not have a base specifier.
    Token &LexNumber(Token &Result);

    /// LexIdentifier - Lex an identifier.
    Token &LexIdentifier(Token &Result);

  public:
    explicit Lexer(const llvm::MemoryBuffer *_buf);
    ~Lexer();

    /// Lex - Return the next token from the file or EOF continually
    /// when the end of the file is reached. The input argument is
    /// used as the result, for convenience.
    Token &Lex(Token &Result);
  };
}
}

#endif