Create pp::unicode option. The idea is to be able to disable unicode characters, but still be able to use mixfix notation.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
e031d7bc10
commit
544229e5d3
28 changed files with 227 additions and 59 deletions
|
@ -27,7 +27,7 @@ struct frontend::imp {
|
|||
// Remark: only named objects are stored in the dictionary.
|
||||
typedef std::unordered_map<name, operator_info, name_hash, name_eq> operator_table;
|
||||
typedef std::unordered_map<name, implicit_info, name_hash, name_eq> implicit_table;
|
||||
typedef std::unordered_map<expr, operator_info, expr_hash, std::equal_to<expr>> expr_to_operator;
|
||||
typedef std::unordered_map<expr, list<operator_info>, expr_hash, std::equal_to<expr>> expr_to_operators;
|
||||
typedef std::unordered_map<expr_pair, expr, expr_pair_hash, expr_pair_eq> coercion_map;
|
||||
typedef std::unordered_set<expr, expr_hash, std::equal_to<expr>> coercion_set;
|
||||
|
||||
|
@ -36,7 +36,7 @@ struct frontend::imp {
|
|||
environment m_env;
|
||||
operator_table m_nud; // nud table for Pratt's parser
|
||||
operator_table m_led; // led table for Pratt's parser
|
||||
expr_to_operator m_expr_to_operator; // map denotations to operators (this is used for pretty printing)
|
||||
expr_to_operators m_expr_to_operators; // map denotations to operators (this is used for pretty printing)
|
||||
implicit_table m_implicit_table; // track the number of implicit arguments for a symbol.
|
||||
coercion_map m_coercion_map; // mapping from (given_type, expected_type) -> coercion
|
||||
coercion_set m_coercion_set; // Set of coercions
|
||||
|
@ -95,12 +95,18 @@ struct frontend::imp {
|
|||
}
|
||||
|
||||
/** \brief Find the operator that is used as notation for the given expression. */
|
||||
operator_info find_op_for(expr const & e) const {
|
||||
auto it = m_expr_to_operator.find(e);
|
||||
if (it != m_expr_to_operator.end())
|
||||
return it->second;
|
||||
else if (has_parent())
|
||||
return m_parent->find_op_for(e);
|
||||
operator_info find_op_for(expr const & e, bool unicode) const {
|
||||
auto it = m_expr_to_operators.find(e);
|
||||
if (it != m_expr_to_operators.end()) {
|
||||
auto l = it->second;
|
||||
for (auto op : l) {
|
||||
if (unicode || op.is_safe_ascii())
|
||||
return op;
|
||||
}
|
||||
}
|
||||
|
||||
if (has_parent())
|
||||
return m_parent->find_op_for(e, unicode);
|
||||
else
|
||||
return operator_info();
|
||||
}
|
||||
|
@ -108,20 +114,26 @@ struct frontend::imp {
|
|||
/** \brief Remove all internal denotations that are associated with the given operator symbol (aka notation) */
|
||||
void remove_bindings(operator_info const & op) {
|
||||
for (expr const & d : op.get_denotations()) {
|
||||
if (has_parent() && m_parent->find_op_for(d)) {
|
||||
if (has_parent() && m_parent->find_op_for(d, true)) {
|
||||
// parent has an association for d... we must hide it.
|
||||
insert(m_expr_to_operator, d, operator_info());
|
||||
insert(m_expr_to_operators, d, list<operator_info>(operator_info()));
|
||||
} else {
|
||||
m_expr_to_operator.erase(d);
|
||||
m_expr_to_operators.erase(d);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/** \brief Add a new entry d -> op in the mapping m_expr_to_operators */
|
||||
void insert_expr_to_operator_entry(expr const & d, operator_info const & op) {
|
||||
list<operator_info> & l = m_expr_to_operators[d];
|
||||
l = cons(op, l);
|
||||
}
|
||||
|
||||
/** \brief Register the new operator in the tables for parsing and pretty printing. */
|
||||
void register_new_op(operator_info new_op, expr const & d, bool led) {
|
||||
new_op.add_expr(d);
|
||||
insert_op(new_op, led);
|
||||
insert(m_expr_to_operator, d, new_op);
|
||||
insert_expr_to_operator_entry(d, new_op);
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -173,7 +185,7 @@ struct frontend::imp {
|
|||
// overload
|
||||
if (defined_here(old_op, led)) {
|
||||
old_op.add_expr(d);
|
||||
insert(m_expr_to_operator, d, old_op);
|
||||
insert_expr_to_operator_entry(d, old_op);
|
||||
} else {
|
||||
// we must copy the operator because it was defined in
|
||||
// a parent frontend.
|
||||
|
@ -391,7 +403,7 @@ void frontend::add_mixfixl(unsigned sz, name const * opns, unsigned p, expr cons
|
|||
void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixr(sz, opns, p, d); }
|
||||
void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixc(sz, opns, p, d); }
|
||||
void frontend::add_mixfixo(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixo(sz, opns, p, d); }
|
||||
operator_info frontend::find_op_for(expr const & n) const { return m_imp->find_op_for(n); }
|
||||
operator_info frontend::find_op_for(expr const & n, bool unicode) const { return m_imp->find_op_for(n, unicode); }
|
||||
operator_info frontend::find_nud(name const & n) const { return m_imp->find_nud(n); }
|
||||
operator_info frontend::find_led(name const & n) const { return m_imp->find_led(n); }
|
||||
|
||||
|
|
|
@ -93,8 +93,11 @@ public:
|
|||
return the null operator.
|
||||
|
||||
\remark This is used for pretty printing.
|
||||
|
||||
\remark If unicode is false, then only operators containing
|
||||
safe ASCII chars are considered.
|
||||
*/
|
||||
operator_info find_op_for(expr const & e) const;
|
||||
operator_info find_op_for(expr const & e, bool unicode) const;
|
||||
/**
|
||||
\brief Return the operator (if one exists) that can appear at
|
||||
the beginning of a language construct.
|
||||
|
|
|
@ -65,6 +65,11 @@ name const & operator_info::get_op_name() const { lean_assert(m_ptr); return car
|
|||
|
||||
list<name> const & operator_info::get_op_name_parts() const { lean_assert(m_ptr); return m_ptr->m_op_parts; }
|
||||
|
||||
bool operator_info::is_safe_ascii() const {
|
||||
auto l = get_op_name_parts();
|
||||
return std::all_of(l.begin(), l.end(), [](name const & p) { return p.is_safe_ascii(); });
|
||||
}
|
||||
|
||||
operator_info operator_info::copy() const { return operator_info(new imp(*m_ptr)); }
|
||||
|
||||
bool operator==(operator_info const & op1, operator_info const & op2) {
|
||||
|
|
|
@ -83,6 +83,9 @@ public:
|
|||
/** \brief Return the operators parts. */
|
||||
list<name> const & get_op_name_parts() const;
|
||||
|
||||
/** \brief Return true if all parts of the operator use only safe ASCII characters */
|
||||
bool is_safe_ascii() const;
|
||||
|
||||
/** \brief Return a copy of the operator. */
|
||||
operator_info copy() const;
|
||||
|
||||
|
|
|
@ -1137,7 +1137,7 @@ class parser::imp {
|
|||
regular(m_frontend) << m_frontend << endl;
|
||||
}
|
||||
} else if (opt_id == g_options_kwd) {
|
||||
regular(m_frontend) << m_frontend.get_state().get_options() << endl;
|
||||
regular(m_frontend) << pp(m_frontend.get_state().get_options()) << endl;
|
||||
} else {
|
||||
throw parser_error("invalid Show command, expression, 'Options' or 'Environment' expected", m_last_cmd_pos);
|
||||
}
|
||||
|
|
|
@ -145,6 +145,7 @@ class pp_fn {
|
|||
unsigned m_max_depth;
|
||||
unsigned m_max_steps;
|
||||
bool m_implict; //!< if true show implicit arguments
|
||||
bool m_unicode; //!< if true use unicode chars
|
||||
bool m_coercion; //!< if true show coercions
|
||||
bool m_notation; //!< if true use notation
|
||||
bool m_extra_lets; //!< introduce extra let-expression to cope with sharing.
|
||||
|
@ -197,7 +198,7 @@ class pp_fn {
|
|||
}
|
||||
|
||||
result pp_ellipsis() {
|
||||
return mk_result(m_notation ? g_ellipsis_n_fmt : g_ellipsis_fmt, 1);
|
||||
return mk_result(m_unicode ? g_ellipsis_n_fmt : g_ellipsis_fmt, 1);
|
||||
}
|
||||
|
||||
result pp_var(expr const & e) {
|
||||
|
@ -223,14 +224,14 @@ class pp_fn {
|
|||
}
|
||||
|
||||
result pp_value(expr const & e) {
|
||||
return mk_result(to_value(e).pp(m_notation), 1);
|
||||
return mk_result(to_value(e).pp(m_unicode), 1);
|
||||
}
|
||||
|
||||
result pp_type(expr const & e) {
|
||||
if (e == Type()) {
|
||||
return mk_result(g_Type_fmt, 1);
|
||||
} else {
|
||||
return mk_result(format{g_Type_fmt, space(), ::lean::pp(ty_level(e))}, 1);
|
||||
return mk_result(format{g_Type_fmt, space(), ::lean::pp(ty_level(e), m_unicode)}, 1);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -312,7 +313,7 @@ class pp_fn {
|
|||
local_names::mk_scope mk(m_local_names);
|
||||
expr b = collect_nested_quantifiers(e, is_forall, nested);
|
||||
format head;
|
||||
if (m_notation)
|
||||
if (m_unicode)
|
||||
head = is_forall ? g_forall_n_fmt : g_exists_n_fmt;
|
||||
else
|
||||
head = is_forall ? g_forall_fmt : g_exists_fmt;
|
||||
|
@ -369,7 +370,7 @@ class pp_fn {
|
|||
if (is_constant(e) && m_local_names.find(const_name(e)) != m_local_names.end())
|
||||
return operator_info();
|
||||
else
|
||||
return m_frontend.find_op_for(e);
|
||||
return m_frontend.find_op_for(e, m_unicode);
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -760,7 +761,7 @@ class pp_fn {
|
|||
lean_assert(!T);
|
||||
result p_lhs = pp_child(abst_domain(e), depth);
|
||||
result p_rhs = pp_arrow_body(abst_body(e), depth);
|
||||
format r_format = group(format{p_lhs.first, space(), m_notation ? g_arrow_n_fmt : g_arrow_fmt, line(), p_rhs.first});
|
||||
format r_format = group(format{p_lhs.first, space(), m_unicode ? g_arrow_n_fmt : g_arrow_fmt, line(), p_rhs.first});
|
||||
return mk_result(r_format, p_lhs.second + p_rhs.second + 1);
|
||||
} else {
|
||||
buffer<std::pair<name, expr>> nested;
|
||||
|
@ -770,7 +771,7 @@ class pp_fn {
|
|||
unsigned head_indent = m_indent;
|
||||
format head;
|
||||
if (!T && !implicit_args) {
|
||||
if (m_notation) {
|
||||
if (m_unicode) {
|
||||
head = is_lambda(e) ? g_lambda_n_fmt : g_Pi_n_fmt;
|
||||
head_indent = 2;
|
||||
} else {
|
||||
|
@ -987,6 +988,7 @@ class pp_fn {
|
|||
m_max_depth = get_pp_max_depth(opts);
|
||||
m_max_steps = get_pp_max_steps(opts);
|
||||
m_implict = get_pp_implicit(opts);
|
||||
m_unicode = get_pp_unicode(opts);
|
||||
m_coercion = get_pp_coercion(opts);
|
||||
m_notation = get_pp_notation(opts);
|
||||
m_extra_lets = get_pp_extra_lets(opts);
|
||||
|
@ -1146,7 +1148,8 @@ class pp_formatter_cell : public formatter_cell {
|
|||
}
|
||||
|
||||
format pp_uvar_decl(object const & obj, options const & opts) {
|
||||
return format{highlight_command(format(obj.keyword())), space(), format(obj.get_name()), space(), format("\u2265"), space(), ::lean::pp(obj.get_cnstr_level())};
|
||||
bool unicode = get_pp_unicode(opts);
|
||||
return format{highlight_command(format(obj.keyword())), space(), format(obj.get_name()), space(), format(unicode ? "\u2265" : ">="), space(), ::lean::pp(obj.get_cnstr_level(), unicode)};
|
||||
}
|
||||
|
||||
format pp_postulate(object const & obj, options const & opts) {
|
||||
|
|
|
@ -33,7 +33,7 @@ static char g_normalized[256];
|
|||
|
||||
/** \brief Auxiliary class for initializing global variable \c g_normalized. */
|
||||
class init_normalized_table {
|
||||
void set(int i, char v) { g_normalized[static_cast<unsigned>(i)] = v; }
|
||||
void set(int i, char v) { g_normalized[static_cast<unsigned char>(i)] = v; }
|
||||
public:
|
||||
init_normalized_table() {
|
||||
// by default all characters are in group c,
|
||||
|
|
|
@ -195,7 +195,7 @@ std::ostream & operator<<(std::ostream & out, level const & l) {
|
|||
return out;
|
||||
}
|
||||
|
||||
format pp(level const & l) {
|
||||
format pp(level const & l, bool unicode) {
|
||||
switch (kind(l)) {
|
||||
case level_kind::UVar:
|
||||
if (l.is_bottom())
|
||||
|
@ -206,19 +206,30 @@ format pp(level const & l) {
|
|||
if (lift_of(l).is_bottom())
|
||||
return format(lift_offset(l));
|
||||
else
|
||||
return format{pp(lift_of(l)), format("+"), format(lift_offset(l))};
|
||||
return format{pp(lift_of(l), unicode), format("+"), format(lift_offset(l))};
|
||||
case level_kind::Max: {
|
||||
format r = pp(max_level(l, 0));
|
||||
for (unsigned i = 1; i < max_size(l); i++) {
|
||||
r += format{space(), format("\u2294"), space()};
|
||||
r += pp(max_level(l, i));
|
||||
if (unicode) {
|
||||
format r = pp(max_level(l, 0), unicode);
|
||||
for (unsigned i = 1; i < max_size(l); i++) {
|
||||
r += format{space(), format("\u2294"), line()};
|
||||
r += pp(max_level(l, i), unicode);
|
||||
}
|
||||
return group(r);
|
||||
} else {
|
||||
format r = format("max");
|
||||
for (unsigned i = 0; i < max_size(l); i++)
|
||||
r += format{line(), pp(max_level(l, i), unicode)};
|
||||
return group(nest(1, format{lp(), r, rp()}));
|
||||
}
|
||||
return r;
|
||||
}}
|
||||
lean_unreachable();
|
||||
return format();
|
||||
}
|
||||
|
||||
format pp(level const & l, options const & opts) {
|
||||
return pp(l, get_pp_unicode(opts));
|
||||
}
|
||||
|
||||
level max(std::initializer_list<level> const & l) {
|
||||
if (l.size() == 1)
|
||||
return *(l.begin());
|
||||
|
|
|
@ -8,6 +8,7 @@ Author: Leonardo de Moura
|
|||
#include <iostream>
|
||||
#include "name.h"
|
||||
#include "format.h"
|
||||
#include "options.h"
|
||||
|
||||
namespace lean {
|
||||
class environment;
|
||||
|
@ -65,6 +66,7 @@ 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);
|
||||
format pp(level const & l, bool unicode);
|
||||
format pp(level const & l, options const & opts = options());
|
||||
}
|
||||
void print(lean::level const & l);
|
||||
|
|
|
@ -108,11 +108,21 @@ static void tst5() {
|
|||
lean_assert(name(name("foo"), 0u).get_prefix().is_string());
|
||||
}
|
||||
|
||||
static void tst6() {
|
||||
lean_assert(name({"foo", "bla"}).is_safe_ascii());
|
||||
lean_assert(name(123u).is_safe_ascii());
|
||||
lean_assert(name(name(name(230u), "bla"), "foo").is_safe_ascii());
|
||||
lean_assert(!name({"foo", "b\u2200aaa"}).is_safe_ascii());
|
||||
lean_assert(!name({"\u2200", "boo"}).is_safe_ascii());
|
||||
lean_assert(!name(name(name(230u), "bla\u2200"), "foo").is_safe_ascii());
|
||||
}
|
||||
|
||||
int main() {
|
||||
tst1();
|
||||
tst2();
|
||||
tst3();
|
||||
tst4();
|
||||
tst5();
|
||||
tst6();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
|
|
|
@ -1,2 +1,2 @@
|
|||
add_library(util trace.cpp debug.cpp name.cpp exception.cpp
|
||||
hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp)
|
||||
hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp ascii.cpp)
|
||||
|
|
44
src/util/ascii.cpp
Normal file
44
src/util/ascii.cpp
Normal file
|
@ -0,0 +1,44 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <initializer_list>
|
||||
namespace lean {
|
||||
static char g_safe_ascii[256];
|
||||
|
||||
class init_safe_ascii {
|
||||
void set(int i, bool v) { g_safe_ascii[static_cast<unsigned char>(i)] = v; }
|
||||
public:
|
||||
init_safe_ascii() {
|
||||
for (int i = 0; i <= 255; i++)
|
||||
set(i, false);
|
||||
// digits and characters are safe
|
||||
for (int i = '0'; i <= '9'; i++) set(i, true);
|
||||
for (int i = 'a'; i <= 'z'; i++) set(i, true);
|
||||
for (int i = 'A'; i <= 'Z'; i++) set(i, true);
|
||||
// the following characters are also safe
|
||||
for (unsigned char b : {'_', ' ', '\t', '\r', '\n', '(', ')', '{', '}', ':', '.', ',', '\"', '\'', '`', '!', '#',
|
||||
'=', '<', '>', '@', '^', '|', '&', '~', '+', '-', '*', '/', '\\', '$', '%', '?', ';', '[', ']'})
|
||||
set(b, true);
|
||||
}
|
||||
};
|
||||
|
||||
static init_safe_ascii g_init_safe_ascii;
|
||||
|
||||
bool is_safe_ascii(char c) {
|
||||
return g_safe_ascii[static_cast<unsigned char>(c)];
|
||||
}
|
||||
|
||||
bool is_safe_ascii(char const * str) {
|
||||
if (str) {
|
||||
while (*str != 0) {
|
||||
if (!is_safe_ascii(*str))
|
||||
return false;
|
||||
str++;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
}
|
19
src/util/ascii.h
Normal file
19
src/util/ascii.h
Normal file
|
@ -0,0 +1,19 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
namespace lean {
|
||||
/**
|
||||
\brief Return true iff \c c is a "safe" ASCII characters.
|
||||
It is a "keyboard" character.
|
||||
*/
|
||||
bool is_safe_ascii(char c);
|
||||
/**
|
||||
\brief Return true iff the given string contains only "safe"
|
||||
ASCII character.
|
||||
*/
|
||||
bool is_safe_ascii(char const * str);
|
||||
}
|
|
@ -28,6 +28,7 @@ class list {
|
|||
public:
|
||||
list():m_ptr(nullptr) {}
|
||||
list(T const & h, list const & t):m_ptr(new cell(h, t)) {}
|
||||
list(T const & h):m_ptr(new cell(h, list())) {}
|
||||
list(list const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
||||
list(list&& s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
|
||||
list(std::initializer_list<T> const & l):list() {
|
||||
|
|
|
@ -14,6 +14,7 @@ Author: Leonardo de Moura
|
|||
#include "buffer.h"
|
||||
#include "hash.h"
|
||||
#include "trace.h"
|
||||
#include "ascii.h"
|
||||
|
||||
namespace lean {
|
||||
constexpr char const * anonymous_str = "[anonymous]";
|
||||
|
@ -302,6 +303,18 @@ unsigned name::hash() const {
|
|||
return m_ptr ? m_ptr->m_hash : 11;
|
||||
}
|
||||
|
||||
bool name::is_safe_ascii() const {
|
||||
imp * i = m_ptr;
|
||||
while (i) {
|
||||
if (i->m_is_string) {
|
||||
if (!::lean::is_safe_ascii(i->m_str))
|
||||
return false;
|
||||
}
|
||||
i = i->m_prefix;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
std::string name::to_string() const {
|
||||
std::ostringstream s;
|
||||
imp::display(s, m_ptr);
|
||||
|
|
|
@ -55,11 +55,11 @@ public:
|
|||
\brief Convert this hierarchical name into a string.
|
||||
*/
|
||||
std::string to_string() const;
|
||||
/**
|
||||
\brief Size of the this name (in characters).
|
||||
*/
|
||||
/** \brief Size of the this name (in characters). */
|
||||
size_t size() const;
|
||||
unsigned hash() const;
|
||||
/** \brief Return true iff the name contains only safe ASCII chars */
|
||||
bool is_safe_ascii() const;
|
||||
friend std::ostream & operator<<(std::ostream & out, name const & n);
|
||||
};
|
||||
struct name_hash { unsigned operator()(name const & n) const { return n.hash(); } };
|
||||
|
|
|
@ -15,6 +15,10 @@
|
|||
#define LEAN_DEFAULT_PP_INDENTATION 4
|
||||
#endif
|
||||
|
||||
#ifndef LEAN_DEFAULT_PP_UNICODE
|
||||
#define LEAN_DEFAULT_PP_UNICODE true
|
||||
#endif
|
||||
|
||||
#ifndef LEAN_DEFAULT_PP_WIDTH
|
||||
#define LEAN_DEFAULT_PP_WIDTH 120
|
||||
#endif
|
||||
|
@ -37,10 +41,12 @@
|
|||
|
||||
namespace lean {
|
||||
static name g_pp_indent{"pp", "indent"};
|
||||
static name g_pp_unicode{"pp", "unicode"};
|
||||
static name g_pp_colors{"pp", "colors"};
|
||||
static name g_pp_width{"pp", "width"};
|
||||
|
||||
RegisterUnsignedOption(g_pp_indent, LEAN_DEFAULT_PP_INDENTATION, "(pretty printer) default indentation");
|
||||
RegisterBoolOption(g_pp_unicode, LEAN_DEFAULT_PP_UNICODE, "(pretty printer) use unicode characters");
|
||||
RegisterBoolOption(g_pp_colors, LEAN_DEFAULT_PP_COLORS, "(pretty printer) use colors");
|
||||
RegisterUnsignedOption(g_pp_width, LEAN_DEFAULT_PP_WIDTH, "(pretty printer) line width");
|
||||
|
||||
|
@ -48,6 +54,10 @@ unsigned get_pp_indent(options const & o) {
|
|||
return o.get_unsigned(g_pp_indent, LEAN_DEFAULT_PP_INDENTATION);
|
||||
}
|
||||
|
||||
bool get_pp_unicode(options const & o) {
|
||||
return o.get_bool(g_pp_unicode, LEAN_DEFAULT_PP_UNICODE);
|
||||
}
|
||||
|
||||
bool get_pp_colors(options const & o) {
|
||||
return o.get_bool(g_pp_colors, LEAN_DEFAULT_PP_COLORS);
|
||||
}
|
||||
|
|
|
@ -305,6 +305,8 @@ inline format fillwords(std::initializer_list<std::string> const & l) {
|
|||
class options;
|
||||
/** \brief Extract indentation from options */
|
||||
unsigned get_pp_indent(options const & o);
|
||||
/** \brief Return unicode characters flag */
|
||||
bool get_pp_unicode(options const & o);
|
||||
|
||||
/** \brief Format a hierarchical name */
|
||||
format pp(name const & n);
|
||||
|
|
|
@ -117,6 +117,7 @@ char const * options::get_string(char const * n, char const * default_value) con
|
|||
static char const * g_left_angle_bracket = "\u27E8";
|
||||
static char const * g_right_angle_bracket = "\u27E9";
|
||||
static char const * g_arrow = "\u21a6";
|
||||
static char const * g_assign = ":=";
|
||||
|
||||
options options::update(name const & n, sexpr const & v) const {
|
||||
if (contains(n)) {
|
||||
|
@ -141,25 +142,31 @@ options join(options const & opts1, options const & opts2) {
|
|||
}
|
||||
|
||||
format pp(options const & o) {
|
||||
bool unicode = get_pp_unicode(o);
|
||||
format r;
|
||||
bool first = true;
|
||||
char const * arrow = unicode ? g_arrow : g_assign;
|
||||
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();
|
||||
r += group(nest(sz+3, format{pp(head(p)), space(), format(g_arrow), space(), pp(tail(p))}));
|
||||
unsigned indent = unicode ? sz+3 : sz+4;
|
||||
r += group(nest(indent, format{pp(head(p)), space(), format(arrow), space(), pp(tail(p))}));
|
||||
});
|
||||
return group(nest(1, format{format(g_left_angle_bracket), r, format(g_right_angle_bracket)}));
|
||||
format open = unicode ? format(g_left_angle_bracket) : lp();
|
||||
format close = unicode ? format(g_right_angle_bracket) : rp();
|
||||
return group(nest(1, format{open, r, close}));
|
||||
}
|
||||
|
||||
std::ostream & operator<<(std::ostream & out, options const & o) {
|
||||
out << g_left_angle_bracket;
|
||||
bool unicode = get_pp_unicode(o);
|
||||
out << (unicode ? g_left_angle_bracket : "(");
|
||||
bool first = true;
|
||||
for_each(o.m_value, [&](sexpr const & p) {
|
||||
if (first) first = false; else out << ", ";
|
||||
out << head(p) << " " << g_arrow << " " << tail(p);
|
||||
out << head(p) << " " << (unicode ? g_arrow : g_assign) << " " << tail(p);
|
||||
});
|
||||
out << g_right_angle_bracket;
|
||||
out << (unicode ? g_right_angle_bracket : ")");
|
||||
return out;
|
||||
}
|
||||
}
|
||||
|
|
|
@ -70,7 +70,7 @@ struct mk_option_declaration {
|
|||
#define LEAN_MAKE_OPTION_NAME_CORE(LINE) LEAN_OPTION_ ## LINE
|
||||
#define LEAN_MAKE_OPTION_NAME(LINE) LEAN_MAKE_OPTION_NAME_CORE(LINE)
|
||||
#define LEAN_OPTION_UNIQUE_NAME LEAN_MAKE_OPTION_NAME(__LINE__)
|
||||
#define RegisterOption(N,K,D,DESC) ::lean::mk_option_declaration LEAN_OPTION_UNIQUE_NAME(N,K,D,DESC)
|
||||
#define RegisterOption(N,K,D,DESC) static ::lean::mk_option_declaration LEAN_OPTION_UNIQUE_NAME(N,K,D,DESC)
|
||||
#define RegisterOptionCore(N,K,D,DESC) RegisterOption(N,K,#D,DESC)
|
||||
#define RegisterBoolOption(N,D,DESC) RegisterOptionCore(N, BoolOption, D, DESC);
|
||||
#define RegisterUnsignedOption(N,D,DESC) RegisterOptionCore(N, UnsignedOption, D, DESC);
|
||||
|
|
|
@ -4,6 +4,8 @@ Set pp::colors false
|
|||
Show true
|
||||
Set lean::pp::notation false
|
||||
Show true && false
|
||||
Set pp::unicode false
|
||||
Show true && false
|
||||
Variable a : Bool
|
||||
Variable a : Bool
|
||||
Variable b : Bool
|
||||
|
|
|
@ -1,13 +1,15 @@
|
|||
Set: pp::colors
|
||||
⊤
|
||||
Set: lean::pp::notation
|
||||
and ⊤ ⊥
|
||||
Set: pp::unicode
|
||||
and true false
|
||||
Assumed: a
|
||||
Error (line: 8, pos: 0) invalid object declaration, environment already has an object named 'a'
|
||||
Error (line: 10, pos: 0) invalid object declaration, environment already has an object named 'a'
|
||||
Assumed: b
|
||||
and a b
|
||||
Assumed: A
|
||||
Error (line: 12, pos: 11) type mismatch at application
|
||||
Error (line: 14, pos: 11) type mismatch at application
|
||||
and a A
|
||||
Function type:
|
||||
Bool -> Bool -> Bool
|
||||
|
@ -15,8 +17,8 @@ Arguments types:
|
|||
Bool
|
||||
Type
|
||||
Variable A : Type
|
||||
⟨lean::pp::notation ↦ false, pp::colors ↦ false⟩
|
||||
Error (line: 15, pos: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
|
||||
Error (line: 16, pos: 23) invalid option value, given option is not an integer
|
||||
(pp::unicode := false, lean::pp::notation := false, pp::colors := false)
|
||||
Error (line: 17, pos: 4) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
|
||||
Error (line: 18, pos: 23) invalid option value, given option is not an integer
|
||||
Set: lean::pp::notation
|
||||
a ∧ b
|
||||
a /\ b
|
||||
|
|
|
@ -3,8 +3,8 @@
|
|||
Assumed: g
|
||||
⊤ ++ ⊥ ++ ⊤
|
||||
Set: lean::pp::notation
|
||||
f (f true false) true
|
||||
f (f ⊤ ⊥) ⊤
|
||||
Assumed: a
|
||||
Assumed: b
|
||||
g (g a b) a
|
||||
f (f true false) false
|
||||
f (f ⊤ ⊥) ⊥
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
Set pp::colors false
|
||||
Show 1 + true
|
||||
|
||||
Variable R : Type
|
||||
Variable T : Type
|
||||
Variable r2t : R -> T
|
||||
|
|
|
@ -1,8 +1,9 @@
|
|||
Error (line: 1, pos: 10) application type mismatch, none of the overloads can be used
|
||||
Set: pp::colors
|
||||
Error (line: 2, pos: 9) application type mismatch, none of the overloads can be used
|
||||
Candidates:
|
||||
Real::add : Real [33m→[0m Real [33m→[0m Real
|
||||
Int::add : Int [33m→[0m Int [33m→[0m Int
|
||||
Nat::add : Nat [33m→[0m Nat [33m→[0m Nat
|
||||
Real::add : Real → Real → Real
|
||||
Int::add : Int → Int → Int
|
||||
Nat::add : Nat → Nat → Nat
|
||||
Arguments:
|
||||
1 : Nat
|
||||
⊤ : Bool
|
||||
|
@ -23,8 +24,8 @@ f (r2t b) (t2r a)
|
|||
f a b
|
||||
Error (line: 20, pos: 10) ambiguous overloads
|
||||
Candidates:
|
||||
g : R [33m->[0m T [33m->[0m R
|
||||
f : T [33m->[0m R [33m->[0m T
|
||||
g : R → T → R
|
||||
f : T → R → T
|
||||
Arguments:
|
||||
b : R
|
||||
a : T
|
||||
|
|
|
@ -2,7 +2,7 @@
|
|||
Notation 10 if _ then _ : implies
|
||||
if ⊤ then ⊥
|
||||
if ⊤ then (if a then ⊥)
|
||||
implies true (implies a false)
|
||||
implies ⊤ (implies a ⊥)
|
||||
Notation 100 _ |- _ ; _ : f
|
||||
f c d e
|
||||
c |- d ; e
|
||||
|
|
9
tests/lean/unicode.lean
Normal file
9
tests/lean/unicode.lean
Normal file
|
@ -0,0 +1,9 @@
|
|||
Set pp::colors false
|
||||
Show true /\ false
|
||||
Set pp::unicode false
|
||||
Show true /\ false
|
||||
Set pp::unicode true
|
||||
Set lean::pp::notation false
|
||||
Show true /\ false
|
||||
Set pp::unicode false
|
||||
Show true /\ false
|
9
tests/lean/unicode.lean.expected.out
Normal file
9
tests/lean/unicode.lean.expected.out
Normal file
|
@ -0,0 +1,9 @@
|
|||
Set: pp::colors
|
||||
⊤ ∧ ⊥
|
||||
Set: pp::unicode
|
||||
true /\ false
|
||||
Set: pp::unicode
|
||||
Set: lean::pp::notation
|
||||
and ⊤ ⊥
|
||||
Set: pp::unicode
|
||||
and true false
|
Loading…
Reference in a new issue