feat(library): add token set
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
5a5d66edc8
commit
7dba2c29d2
3 changed files with 89 additions and 1 deletions
|
@ -3,7 +3,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
|
|||
resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp
|
||||
normalize.cpp shared_environment.cpp module.cpp coercion.cpp
|
||||
private.cpp placeholder.cpp aliases.cpp scope.cpp level_names.cpp
|
||||
update_declaration.cpp)
|
||||
update_declaration.cpp token_set.cpp)
|
||||
# fo_unify.cpp hop_match.cpp)
|
||||
|
||||
target_link_libraries(library ${LEAN_LIBS})
|
||||
|
|
47
src/library/token_set.cpp
Normal file
47
src/library/token_set.cpp
Normal file
|
@ -0,0 +1,47 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "library/token_set.h"
|
||||
|
||||
namespace lean {
|
||||
token_set token_set::add_command_token(char const * token) const { return token_set(insert(m_tokens, token, info(token))); }
|
||||
token_set token_set::add_token(char const * token, unsigned prec) const { return token_set(insert(m_tokens, token, info(token, prec))); }
|
||||
token_set token_set::add_token(char const * token, char const * val, unsigned prec) const {
|
||||
return token_set(insert(m_tokens, token, info(val, prec)));
|
||||
}
|
||||
token_set token_set::merge(token_set const & s) const { return token_set(::lean::merge(m_tokens, s.m_tokens)); }
|
||||
optional<token_set> token_set::find(char c) const {
|
||||
auto r = m_tokens.find(c);
|
||||
return r ? optional<token_set>(token_set(*r)) : optional<token_set>();
|
||||
}
|
||||
optional<token_set::info> token_set::value() const { return m_tokens.value(); }
|
||||
|
||||
static char const * g_lambda_unicode = "\u03BB";
|
||||
static char const * g_pi_unicode = "\u03A0";
|
||||
static char const * g_forall_unicode = "\u2200";
|
||||
static char const * g_arrow_unicode = "\u2192";
|
||||
|
||||
// Auxiliary class for creating the initial token set
|
||||
class init_token_set_fn {
|
||||
public:
|
||||
token_set m_token_set;
|
||||
init_token_set_fn():m_token_set(true) {
|
||||
char const * builtin[] = {"fun", "forall", "let", "in", "have", "show", "by", "from", "(", ")", "{", "}",
|
||||
".{", "Type", "...", ",", ".", ":", "calc", ":=", "--", "(*", "(--", "->", 0};
|
||||
char const ** it = builtin;
|
||||
while (*it) {
|
||||
m_token_set = m_token_set.add_token(*it);
|
||||
it++;
|
||||
}
|
||||
m_token_set = m_token_set.add_token(g_lambda_unicode, "fun");
|
||||
m_token_set = m_token_set.add_token(g_forall_unicode, "forall");
|
||||
m_token_set = m_token_set.add_token(g_pi_unicode, "forall");
|
||||
m_token_set = m_token_set.add_token(g_arrow_unicode, "->");
|
||||
}
|
||||
};
|
||||
static init_token_set_fn g_init;
|
||||
token_set::token_set():token_set(g_init.m_token_set) {}
|
||||
}
|
41
src/library/token_set.h
Normal file
41
src/library/token_set.h
Normal file
|
@ -0,0 +1,41 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include <utility>
|
||||
#include <string>
|
||||
#include "util/trie.h"
|
||||
|
||||
namespace lean {
|
||||
|
||||
/** \brief Set of tokens and their precedences. This information is used by the scanner. */
|
||||
class token_set {
|
||||
class info {
|
||||
bool m_command;
|
||||
std::string m_value;
|
||||
unsigned m_precedence;
|
||||
public:
|
||||
info():m_command(true) {}
|
||||
info(char const * val):m_command(true), m_value(val), m_precedence(0) {}
|
||||
info(char const * val, unsigned prec):m_command(false), m_value(val), m_precedence(prec) {}
|
||||
bool is_command() const { return m_command; }
|
||||
std::string const & value() const { return m_value; }
|
||||
unsigned precedence() const { return m_precedence; }
|
||||
};
|
||||
ctrie<info> m_tokens;
|
||||
explicit token_set(ctrie<info> const & t):m_tokens(t) {}
|
||||
friend class init_token_set_fn;
|
||||
token_set(bool) {} // NOLINT
|
||||
public:
|
||||
token_set();
|
||||
token_set add_command_token(char const * token) const;
|
||||
token_set add_token(char const * token, unsigned prec = 0) const;
|
||||
token_set add_token(char const * token, char const * val, unsigned prec = 0) const;
|
||||
token_set merge(token_set const & s) const;
|
||||
optional<token_set> find(char c) const;
|
||||
optional<info> value() const;
|
||||
};
|
||||
}
|
Loading…
Reference in a new issue