michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Remove option name::separator, it can't be configured during runtime

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-13 08:18:01 -07:00
parent 27b3ac19a7
commit 0a4e03efc5
12 changed files with 34 additions and 97 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/frontend/operator_info.cpp
View file

@ -7,7 +7,6 @@ Author: Leonardo de Moura
*/
#include "operator_info.h"
#include "rc.h"
#include "options.h"
namespace lean {
@ -87,7 +86,7 @@ operator_info mixfixc(unsigned num_parts, name const * parts, unsigned precedenc
static char const * g_arrow = "\u21a6";
format pp(operator_info const & o, options const & opt) {
format pp(operator_info const & o) {
format r;
switch (o.get_fixity()) {
case fixity::Infix: r = format(o.get_associativity() == associativity::Left ? "Infixl" : "Infixr"); break;
@ -105,36 +104,31 @@ format pp(operator_info const & o, options const & opt) {
switch (o.get_fixity()) {
case fixity::Infix: case fixity::Prefix: case fixity::Postfix:
r += pp(o.get_op_name(), opt); break;
r += pp(o.get_op_name()); break;
case fixity::Mixfixl:
for (auto p : o.get_op_name_parts()) r += format{pp(p, opt), format(" _")};
for (auto p : o.get_op_name_parts()) r += format{pp(p), format(" _")};
break;
case fixity::Mixfixr:
for (auto p : o.get_op_name_parts()) r += format{format("_ "), pp(p, opt)};
for (auto p : o.get_op_name_parts()) r += format{format("_ "), pp(p)};
break;
case fixity::Mixfixc: {
bool first = true;
for (auto p : o.get_op_name_parts()) {
if (first) first = false; else r += format(" _ ");
r += pp(p, opt);
r += pp(p);
}
}}
list<name> const & l = o.get_internal_names();
if (!is_nil(l)) {
r += format{space(), format(g_arrow)};
for (auto n : l) r += format{space(), pp(n, opt)};
for (auto n : l) r += format{space(), pp(n)};
}
return r;
}
format pp(operator_info const & o) {
return pp(o, options());
}
std::ostream & operator<<(std::ostream & out, operator_info const & o) {
out << pp(o);
return out;
}
}

2
src/frontend/operator_info.h
View file

@ -95,8 +95,6 @@ inline operator_info mixfixl(std::initializer_list<name> const & l, unsigned pre
inline operator_info mixfixr(std::initializer_list<name> const & l, unsigned precedence) { return mixfixr(l.size(), l.begin(), precedence); }
inline operator_info mixfixc(std::initializer_list<name> const & l, unsigned precedence) { return mixfixc(l.size(), l.begin(), precedence); }
class options;
format pp(operator_info const & o, options const &);
format pp(operator_info const & o);
std::ostream & operator<<(std::ostream & out, operator_info const & o);
}

10
src/kernel/level.cpp
View file

@ -192,23 +192,23 @@ std::ostream & operator<<(std::ostream & out, level const & l) {
return out;
}
format pp(level const & l, char const * sep) {
format pp(level const & l) {
switch (kind(l)) {
case level_kind::UVar:
if (l.is_bottom())
return format(0);
else
return format(uvar_name(l).to_string(sep));
return pp(uvar_name(l));
case level_kind::Lift:
if (lift_of(l).is_bottom())
return format(lift_offset(l));
else
return format{pp(lift_of(l), sep), format(" + "), format(lift_offset(l))};
return format{pp(lift_of(l)), format(" + "), format(lift_offset(l))};
case level_kind::Max: {
format r = pp(max_level(l, 0), sep);
format r = pp(max_level(l, 0));
for (unsigned i = 1; i < max_size(l); i++) {
r += format(" \u2293 ");
r += pp(max_level(l, i), sep);
r += pp(max_level(l, i));
}
return r;
}}

2
src/kernel/level.h
View file

@ -65,5 +65,5 @@ inline bool is_max (level const & l) { return kind(l) == level_kind::Max; }
inline level const * max_begin_levels(level const & l) { return &max_level(l, 0); }
inline level const * max_end_levels(level const & l) { return max_begin_levels(l) + max_size(l); }
format pp(level const & l, char const * sep = LEAN_NAME_SEPARATOR);
format pp(level const & l);
}

7
src/kernel/pp.cpp
View file

@ -17,7 +17,6 @@ struct pp_fn {
pp_fn(environment const * env):m_env(env) {}
unsigned indent() const { return 2; }
char const * sep() const { return LEAN_NAME_SEPARATOR; }
format pp_keyword(char const * k) { return highlight(format(k), format::format_color::ORANGE); }
format pp_type_kwd() { return highlight(format("Type"), format::format_color::PINK); }
format pp_eq_kwd() { return highlight(format(" = "), format::format_color::BLUE); }
@ -47,7 +46,7 @@ struct pp_fn {
}
format pp_constant(expr const & e) {
return format(const_name(e).to_string(sep()));
return ::lean::pp(const_name(e));
}
format pp_value(expr const & e) {
@ -58,7 +57,7 @@ struct pp_fn {
if (e == Type()) {
return pp_type_kwd();
} else {
return format{pp_type_kwd(), pp_space(), ::lean::pp(ty_level(e), sep())};
return format{pp_type_kwd(), pp_space(), ::lean::pp(ty_level(e))};
}
}
@ -112,7 +111,7 @@ struct pp_fn {
}
format pp_bname(expr const & binder) {
return format(abst_name(binder).to_string(sep()));
return ::lean::pp(abst_name(binder));
}
template<typename It>

1
src/tests/util/sexpr.cpp
View file

@ -168,7 +168,6 @@ static void tst7() {
sexpr s = sexpr{ sexpr(1,2), sexpr(2,3), sexpr(0,1) };
std::cout << pp(sexpr{s, s, s, s, s}) << "\n";
std::cout << pp(sexpr{sexpr(name{"test","name"}), sexpr(10), sexpr(10.20)}) << "\n";
std::cout << pp(sexpr{sexpr(name{"test","name"}), sexpr(10), sexpr(10.20)}, options(name{"name","separator"}, "-->")) << "\n";
}
int main() {

35
src/util/name.cpp
View file

@ -47,11 +47,11 @@ struct name::imp {
imp(bool s, imp * p):m_rc(1), m_is_string(s), m_hash(0), m_prefix(p) { if (p) p->inc_ref(); }
static void display_core(std::ostream & out, char const * sep, imp * p) {
static void display_core(std::ostream & out, imp * p) {
lean_assert(p != nullptr);
if (p->m_prefix) {
display_core(out, sep, p->m_prefix);
out << sep;
display_core(out, p->m_prefix);
out << lean_name_separator;
}
if (p->m_is_string)
out << p->m_str;
@ -59,11 +59,11 @@ struct name::imp {
out << p->m_k;
}
static void display(std::ostream & out, char const * sep, imp * p) {
static void display(std::ostream & out, imp * p) {
if (p == nullptr)
out << anonymous_str;
else
display_core(out, sep, p);
display_core(out, p);
}
friend void copy_limbs(imp * p, std::vector<name::imp *> & limbs) {
@ -238,12 +238,12 @@ static unsigned num_digits(unsigned k) {
return r;
}
size_t name::size(char const * sep) const {
size_t name::size() const {
if (m_ptr == nullptr) {
return strlen(anonymous_str);
} else {
imp * i = m_ptr;
size_t sep_sz = strlen(sep);
size_t sep_sz = strlen(lean_name_separator);
size_t r = 0;
while (true) {
if (i->m_is_string) {
@ -262,33 +262,18 @@ size_t name::size(char const * sep) const {
}
}
size_t name::size() const {
return size(LEAN_NAME_SEPARATOR);
}
unsigned name::hash() const {
return m_ptr ? m_ptr->m_hash : 11;
}
std::string name::to_string(char const * sep) const {
std::string name::to_string() const {
std::ostringstream s;
imp::display(s, sep, m_ptr);
imp::display(s, m_ptr);
return s.str();
}
std::string name::to_string() const {
return to_string(LEAN_NAME_SEPARATOR);
}
std::ostream & operator<<(std::ostream & out, name const & n) {
name::imp::display(out, LEAN_NAME_SEPARATOR, n.m_ptr);
return out;
}
name::sep::sep(name const & n, char const * s):m_name(n), m_sep(s) {}
std::ostream & operator<<(std::ostream & out, name::sep const & s) {
name::imp::display(out, s.m_sep, s.m_name.m_ptr);
name::imp::display(out, n.m_ptr);
return out;
}
}

19
src/util/name.h
View file

@ -7,11 +7,8 @@ Author: Leonardo de Moura
#pragma once
#include <iostream>
#ifndef LEAN_NAME_SEPARATOR
#define LEAN_NAME_SEPARATOR "::"
#endif
namespace lean {
constexpr char const * lean_name_separator = "::";
enum class name_kind { ANONYMOUS, STRING, NUMERAL };
/**
\brief Hierarchical names.
@ -52,25 +49,15 @@ public:
bool is_atomic() const;
name get_prefix() const;
/**
\brief Convert this hierarchical name into a string using the given separator to "glue" the different limbs.
\brief Convert this hierarchical name into a string.
*/
std::string to_string(char const * sep) const;
std::string to_string() const;
/**
\brief Size of the this name (in characters) when using the given separator.
\brief Size of the this name (in characters).
*/
size_t size(char const * sep) const;
size_t size() const;
unsigned hash() const;
friend std::ostream & operator<<(std::ostream & out, name const & n);
class sep {
name const & m_name;
char const * m_sep;
public:
sep(name const & n, char const * s);
friend std::ostream & operator<<(std::ostream & out, sep const & s);
};
friend std::ostream & operator<<(std::ostream & out, sep const & s);
};
struct name_hash { unsigned operator()(name const & n) const { return n.hash(); } };
struct name_eq { bool operator()(name const & n1, name const & n2) const { return n1 == n2; } };

24
src/util/sexpr/format.cpp
View file

@ -302,21 +302,11 @@ unsigned get_pp_indent(options const & o) {
return o.get_int(g_pp_indent, LEAN_DEFAULT_INDENTATION);
}
format pp(name const & n, char const * sep) {
return format(n.to_string(sep));
}
format pp(name const & n, options const & o) {
return pp(n, get_name_separator(o));
}
format pp(name const & n) {
return pp(n, get_name_separator(options()));
return format(n.to_string());
}
struct sexpr_pp_fn {
char const * m_sep;
format apply(sexpr const & s) {
switch (s.kind()) {
case sexpr_kind::NIL: return format("nil");
@ -328,7 +318,7 @@ struct sexpr_pp_fn {
case sexpr_kind::BOOL: return format(to_bool(s) ? "true" : "false");
case sexpr_kind::INT: return format(to_int(s));
case sexpr_kind::DOUBLE: return format(to_double(s));
case sexpr_kind::NAME: return pp(to_name(s), m_sep);
case sexpr_kind::NAME: return pp(to_name(s));
case sexpr_kind::MPZ: return format(to_mpz(s));
case sexpr_kind::MPQ: return format(to_mpq(s));
case sexpr_kind::CONS: {
@ -350,18 +340,12 @@ struct sexpr_pp_fn {
return format();
}
format operator()(sexpr const & s, options const & o) {
m_sep = get_name_separator(o);
format operator()(sexpr const & s) {
return apply(s);
}
};
format pp(sexpr const & s, options const & o) {
return sexpr_pp_fn()(s, o);
}
format pp(sexpr const & s) {
return pp(s, options());
return sexpr_pp_fn()(s);
}
}

2
src/util/sexpr/format.h
View file

@ -286,8 +286,6 @@ class options;
unsigned get_pp_indent(options const & o);
/** \brief Format a hierarchical name */
format pp(name const & n, char const * s);
format pp(name const & n, options const & o);
format pp(name const & n);
/** \brief Format a S-expression */

9
src/util/sexpr/options.cpp
View file

@ -84,14 +84,13 @@ options options::update(name const & n, sexpr const & v) const {
}
format pp(options const & o) {
char const * sep = get_name_separator(o);
format r;
bool first = true;
for_each(o.m_value, [&](sexpr const & p) {
if (first) { first = false; } else { r += comma(); r += line(); }
name const & n = to_name(head(p));
unsigned sz = n.size(sep);
r += group(nest(sz+3, format{pp(head(p), o), space(), format(g_arrow), space(), pp(tail(p), o)}));
unsigned sz = n.size();
r += group(nest(sz+3, format{pp(head(p)), space(), format(g_arrow), space(), pp(tail(p))}));
});
return group(nest(1, format{format(g_left_angle_bracket), r, format(g_right_angle_bracket)}));
}
@ -106,8 +105,4 @@ std::ostream & operator<<(std::ostream & out, options const & o) {
out << g_right_angle_bracket;
return out;
}
static name g_name_separator{"name", "separator"};
char const * get_name_separator(options const & o) {
return o.get_string(g_name_separator, "::");
}
}

2
src/util/sexpr/options.h
View file

@ -51,6 +51,4 @@ public:
};
template<typename T> options update(options const & o, name const & n, T const & v) { return o.update(n, sexpr(v)); }
template<typename T> options update(options const & o, char const * n, T const & v) { return o.update(name(n), sexpr(v)); }
/** \brief Return the separator for hierarchical names */
char const * get_name_separator(options const & o);
}