本文整理汇总了C++中name类的典型用法代码示例。如果您正苦于以下问题:C++ name类的具体用法?C++ name怎么用?C++ name使用的例子?那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。
在下文中一共展示了name类的17个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: add_namespace
environment add_namespace(environment const & env, name const & ns) {
scope_mng_ext ext = get_extension(env);
if (!ext.m_namespace_set.contains(ns)) {
ext.m_namespace_set.insert(ns);
environment r = update(env, ext);
r = module::add(r, *g_new_namespace_key, [=](environment const &, serializer & s) { s << ns; });
if (ns.is_atomic())
return r;
else
return add_namespace(r, ns.get_prefix());
} else {
return env;
}
}
开发者ID:soonhokong,项目名称:lean-osx,代码行数:14,代码来源:scoped_ext.cpp
示例2: add_alias
environment add_alias(parser & p, environment env, bool composite,
name const & full_id, levels const & ctx_levels, buffer<expr> const & ctx_params) {
name id;
if (composite)
id = name(name(full_id.get_prefix().get_string()), full_id.get_string());
else
id = name(full_id.get_string());
if (!empty(ctx_levels) || !ctx_params.empty()) {
expr r = mk_local_ref(full_id, ctx_levels, ctx_params);
env = p.add_local_ref(env, id, r);
}
if (full_id != id)
env = add_expr_alias_rec(env, id, full_id);
return env;
}
开发者ID:GallagherCommaJack,项目名称:lean,代码行数:15,代码来源:type_util.cpp
示例3: serialize_decl
json serialize_decl(name const & short_name, name const & long_name, environment const & env, options const & o) {
declaration const & d = env.get(long_name);
type_context_old tc(env);
auto fmter = mk_pretty_formatter_factory()(env, o, tc);
expr type = d.get_type();
if (LEAN_COMPLETE_CONSUME_IMPLICIT) {
while (true) {
if (!is_pi(type))
break;
if (!binding_info(type).is_implicit() && !binding_info(type).is_inst_implicit())
break;
std::string q("?");
q += binding_name(type).to_string();
expr m = mk_constant(name(q.c_str()));
type = instantiate(binding_body(type), m);
}
}
json completion;
completion["text"] = short_name.to_string();
interactive_report_type(env, o, type, completion);
add_source_info(env, long_name, completion);
if (auto doc = get_doc_string(env, long_name))
completion["doc"] = *doc;
return completion;
}
开发者ID:fpvandoorn,项目名称:lean,代码行数:25,代码来源:json.cpp
示例4: collect
level collect(level const & l) {
return replace(l, [&](level const & l) {
if (is_meta(l)) {
name const & id = meta_id(l);
if (auto r = m_univ_meta_to_param.find(id)) {
return some_level(*r);
} else {
name n = m_prefix.append_after(m_next_idx);
m_next_idx++;
level new_r = mk_param_univ(n);
m_univ_meta_to_param.insert(id, new_r);
m_univ_meta_to_param_inv.insert(n, l);
m_level_params.push_back(n);
return some_level(new_r);
}
} else if (is_param(l)) {
name const & id = param_id(l);
if (!m_found_univ_params.contains(id)) {
m_found_univ_params.insert(id);
m_level_params.push_back(id);
}
}
return none_level();
});
}
开发者ID:sakas--,项目名称:lean,代码行数:25,代码来源:aux_definition.cpp
示例5: find_file
std::string find_file(search_path const & paths, std::string const & base, optional<unsigned> const & rel, name const & fname,
std::initializer_list<char const *> const & extensions) {
if (!rel) {
return find_file(paths, fname.to_string(get_dir_sep()), extensions);
} else {
auto path = base;
for (unsigned i = 0; i < *rel; i++) {
path += get_dir_sep();
path += "..";
}
for (auto ext : extensions) {
if (auto r = check_file(path, fname.to_string(get_dir_sep()), ext))
return *r;
}
throw lean_file_not_found_exception(fname.to_string());
}
}
开发者ID:avigad,项目名称:lean,代码行数:17,代码来源:lean_path.cpp
示例6: find_file
std::string find_file(std::string const & base, optional<unsigned> const & rel, name const & fname,
std::initializer_list<char const *> const & extensions) {
if (!rel) {
return find_file(fname.to_string(g_sep_str.c_str()), extensions);
} else {
auto path = base;
for (unsigned i = 0; i < *rel; i++) {
path += g_sep;
path += "..";
}
for (auto ext : extensions) {
if (auto r = check_file(path, fname.to_string(g_sep_str.c_str()), ext))
return *r;
}
throw exception(sstream() << "file '" << fname << "' not found at '" << path << "'");
}
}
开发者ID:codyroux,项目名称:lean,代码行数:17,代码来源:lean_path.cpp
示例7: get_unused_name
name get_unused_name(name const & prefix, unsigned & idx, buffer<expr> const & locals) {
while (true) {
name curr = prefix.append_after(idx);
idx++;
if (!uses_name(curr, locals))
return curr;
}
}
开发者ID:GallagherCommaJack,项目名称:lean,代码行数:8,代码来源:goal.cpp
示例8: mk_fresh_name
static name mk_fresh_name(environment const & env, buffer<name> const & names, name const & s) {
unsigned i = 1;
name c = s;
while (true) {
if (!env.find(c) &&
std::find(names.begin(), names.end(), c) == names.end())
return c;
c = s.append_after(i);
i++;
}
}
开发者ID:bmalehorn,项目名称:lean,代码行数:11,代码来源:projection.cpp
示例9: get_precedence
static unsigned get_precedence(environment const & env, buffer<token_entry> const & new_tokens, name const & token) {
std::string token_str = token.to_string();
for (auto const & e : new_tokens) {
if (e.m_token == token_str)
return e.m_prec;
}
auto prec = get_expr_precedence(get_token_table(env), token_str.c_str());
if (prec)
return *prec;
else
return 0;
}
开发者ID:GallagherCommaJack,项目名称:lean,代码行数:12,代码来源:notation_cmd.cpp
示例10: BOOST_LOG_SEV
void merger::check_name(const std::string& model_name, const name& key,
const name& value) const {
if (key.location().original_model_name() != model_name) {
std::ostringstream s;
s << "Type does not belong to this model. Model name: '"
<< model_name << "'. Type name: "
<< key.qualified();
BOOST_LOG_SEV(lg, error) << s.str();
BOOST_THROW_EXCEPTION(merging_error(s.str()));
}
if (key != value) {
std::ostringstream s;
s << "Inconsistency between key and value names: "
<< " key: " << key.qualified()
<< " value: " << value.qualified();
BOOST_LOG_SEV(lg, error) << s.str();
BOOST_THROW_EXCEPTION(merging_error(s.str()));
}
}
开发者ID:Niam99,项目名称:dogen,代码行数:21,代码来源:merger.cpp
示例11: switch
/// This feature does not define names.
bool
eq_algo::operator()(const name& a, const name& b) const
{
switch (a.get_kind()) {
case basic_name_kind:
return eq_basic_name(cast<basic_name>(a), cast<basic_name>(b));
case internal_name_kind:
return eq_internal_name(cast<internal_name>(a), cast<internal_name>(b));
default:
break;
}
assert(false && "not a core name");
}
开发者ID:asutton,项目名称:beaker,代码行数:14,代码来源:eq.cpp
示例12: switch
/// Hash the name `n` into `h`.
void
hash_algo::operator()(hasher& h, const name& n) const
{
switch (n.get_kind()) {
case basic_name_kind:
return hash(h, cast<basic_name>(n).get_symbol());
case internal_name_kind:
return hash(h, cast<internal_name>(n).get_id());
default:
break;
}
assert(false && "name not a core name");
}
开发者ID:asutton,项目名称:beaker,代码行数:14,代码来源:hash.cpp
示例13: mk_name_for
name mk_name_for(expr const & e) {
lean_assert(is_nested_declaration(e));
if (auto n = get_nested_declaration_name(e)) {
return *n;
} else {
name ns = get_namespace(m_env);
while (true) {
name aux = m_dname.append_after(m_idx);
m_idx++;
if (!m_env.find(ns + aux))
return aux;
}
}
}
开发者ID:cpehle,项目名称:lean,代码行数:14,代码来源:nested_declaration.cpp
示例14: switch
void
print_algo::operator()(std::ostream& os, const name& n) const
{
switch (n.get_kind()) {
case basic_name_kind:
os << cast<basic_name>(n).get_symbol().get_spelling();
return;
case internal_name_kind:
os << "<internal>";
return;
default:
break;
}
assert(false && "not a core name");
}
开发者ID:asutton,项目名称:beaker,代码行数:15,代码来源:print.cpp
示例15: visit_cases_on
expr visit_cases_on(name const & fn, buffer<expr> & args) {
name const & I_name = fn.get_prefix();
if (is_inductive_predicate(env(), I_name))
throw exception(sstream() << "code generation failed, inductive predicate '" << I_name << "' is not supported");
bool is_builtin = is_vm_builtin_function(fn);
buffer<name> cnames;
get_intro_rule_names(env(), I_name, cnames);
lean_assert(args.size() >= cnames.size() + 1);
if (args.size() > cnames.size() + 1)
distribute_extra_args_over_minors(I_name, cnames, args);
lean_assert(args.size() == cnames.size() + 1);
/* Process major premise */
args[0] = visit(args[0]);
unsigned num_reachable = 0;
optional<expr> reachable_case;
/* Process minor premises */
for (unsigned i = 0; i < cnames.size(); i++) {
buffer<bool> rel_fields;
get_constructor_info(cnames[i], rel_fields);
auto p = visit_minor_premise(args[i+1], rel_fields);
expr new_minor = p.first;
if (i == 0 && has_trivial_structure(I_name, rel_fields)) {
/* Optimization for an inductive datatype that has a single constructor with only one relevant field */
return beta_reduce(mk_app(new_minor, args[0]));
}
args[i+1] = new_minor;
if (!p.second) {
num_reachable++;
reachable_case = p.first;
}
}
if (num_reachable == 0) {
return mk_unreachable_expr();
} else if (num_reachable == 1 && !is_builtin) {
/* Use _cases.1 */
return mk_app(mk_cases(1), args[0], *reachable_case);
} else if (is_builtin) {
return mk_app(mk_constant(fn), args);
} else {
return mk_app(mk_cases(cnames.size()), args);
}
}
开发者ID:soonhokong,项目名称:lean-osx,代码行数:43,代码来源:simp_inductive.cpp
示例16: name_to_file
std::string name_to_file(name const & fname) {
return fname.to_string(get_dir_sep());
}
开发者ID:avigad,项目名称:lean,代码行数:3,代码来源:lean_path.cpp
示例17: report
virtual void report(io_state_stream const & ios, json & record) const override {
record["full-id"] = m_full_id.to_string();
add_source_info(ios.get_environment(), m_full_id, record);
if (auto doc = get_doc_string(ios.get_environment(), m_full_id))
record["doc"] = *doc;
}
开发者ID:fpvandoorn,项目名称:lean,代码行数:6,代码来源:info_manager.cpp
注:本文中的name类示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论