diff --git a/src/frontends/lean/lean_frontend.cpp b/src/frontends/lean/lean_frontend.cpp index 0805eac5b..25b2aa219 100644 --- a/src/frontends/lean/lean_frontend.cpp +++ b/src/frontends/lean/lean_frontend.cpp @@ -27,7 +27,7 @@ struct frontend::imp { // Remark: only named objects are stored in the dictionary. typedef std::unordered_map operator_table; typedef std::unordered_map implicit_table; - typedef std::unordered_map> expr_to_operator; + typedef std::unordered_map, expr_hash, std::equal_to> expr_to_operators; typedef std::unordered_map coercion_map; typedef std::unordered_set> 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())); } 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 & 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); } diff --git a/src/frontends/lean/lean_frontend.h b/src/frontends/lean/lean_frontend.h index 984256751..12ae8ebdd 100644 --- a/src/frontends/lean/lean_frontend.h +++ b/src/frontends/lean/lean_frontend.h @@ -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. diff --git a/src/frontends/lean/lean_operator_info.cpp b/src/frontends/lean/lean_operator_info.cpp index 2433255a7..3af1d4687 100644 --- a/src/frontends/lean/lean_operator_info.cpp +++ b/src/frontends/lean/lean_operator_info.cpp @@ -65,6 +65,11 @@ name const & operator_info::get_op_name() const { lean_assert(m_ptr); return car list 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) { diff --git a/src/frontends/lean/lean_operator_info.h b/src/frontends/lean/lean_operator_info.h index b21c68900..b51c51515 100644 --- a/src/frontends/lean/lean_operator_info.h +++ b/src/frontends/lean/lean_operator_info.h @@ -83,6 +83,9 @@ public: /** \brief Return the operators parts. */ list 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; diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index 34a2408b2..9c8cfb08f 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -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); } diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/lean_pp.cpp index fb6c26855..7aaf7bccc 100644 --- a/src/frontends/lean/lean_pp.cpp +++ b/src/frontends/lean/lean_pp.cpp @@ -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> 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) { diff --git a/src/frontends/lean/lean_scanner.cpp b/src/frontends/lean/lean_scanner.cpp index 7de134870..d17475720 100644 --- a/src/frontends/lean/lean_scanner.cpp +++ b/src/frontends/lean/lean_scanner.cpp @@ -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(i)] = v; } + void set(int i, char v) { g_normalized[static_cast(i)] = v; } public: init_normalized_table() { // by default all characters are in group c, diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index fcbbdc82f..c886bc051 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -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 const & l) { if (l.size() == 1) return *(l.begin()); diff --git a/src/kernel/level.h b/src/kernel/level.h index e37d61c1d..2eb1f4800 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #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); diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp index 4f10f7b66..4a95cfdd1 100644 --- a/src/tests/util/name.cpp +++ b/src/tests/util/name.cpp @@ -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; } diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 4ad2db9e1..62e5f5750 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -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) diff --git a/src/util/ascii.cpp b/src/util/ascii.cpp new file mode 100644 index 000000000..5072be9a7 --- /dev/null +++ b/src/util/ascii.cpp @@ -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 +namespace lean { +static char g_safe_ascii[256]; + +class init_safe_ascii { + void set(int i, bool v) { g_safe_ascii[static_cast(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(c)]; +} + +bool is_safe_ascii(char const * str) { + if (str) { + while (*str != 0) { + if (!is_safe_ascii(*str)) + return false; + str++; + } + } + return true; +} +} diff --git a/src/util/ascii.h b/src/util/ascii.h new file mode 100644 index 000000000..33f9c0c31 --- /dev/null +++ b/src/util/ascii.h @@ -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); +} diff --git a/src/util/list.h b/src/util/list.h index 0752a2170..e950851f6 100644 --- a/src/util/list.h +++ b/src/util/list.h @@ -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 const & l):list() { diff --git a/src/util/name.cpp b/src/util/name.cpp index dd239cdc5..321b06003 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -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); diff --git a/src/util/name.h b/src/util/name.h index 968c1ad21..0859c3f7c 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -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(); } }; diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 45dfdae06..79c908fd3 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -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); } diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h index 779b02684..d96b23210 100644 --- a/src/util/sexpr/format.h +++ b/src/util/sexpr/format.h @@ -305,6 +305,8 @@ inline format fillwords(std::initializer_list 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); diff --git a/src/util/sexpr/options.cpp b/src/util/sexpr/options.cpp index 3a680f9f1..0e60af26e 100644 --- a/src/util/sexpr/options.cpp +++ b/src/util/sexpr/options.cpp @@ -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; } } diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h index e4b782856..d8a583262 100644 --- a/src/util/sexpr/options.h +++ b/src/util/sexpr/options.h @@ -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); diff --git a/tests/lean/ex2.lean b/tests/lean/ex2.lean index 15a869c74..7651075b6 100644 --- a/tests/lean/ex2.lean +++ b/tests/lean/ex2.lean @@ -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 diff --git a/tests/lean/ex2.lean.expected.out b/tests/lean/ex2.lean.expected.out index bc49806d4..b49c8fd43 100644 --- a/tests/lean/ex2.lean.expected.out +++ b/tests/lean/ex2.lean.expected.out @@ -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 diff --git a/tests/lean/overload1.lean.expected.out b/tests/lean/overload1.lean.expected.out index b2bb13990..d06cf117b 100644 --- a/tests/lean/overload1.lean.expected.out +++ b/tests/lean/overload1.lean.expected.out @@ -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 ⊤ ⊥) ⊥ diff --git a/tests/lean/overload2.lean b/tests/lean/overload2.lean index 06a9b21ef..f75cf84e8 100644 --- a/tests/lean/overload2.lean +++ b/tests/lean/overload2.lean @@ -1,5 +1,5 @@ +Set pp::colors false Show 1 + true - Variable R : Type Variable T : Type Variable r2t : R -> T diff --git a/tests/lean/overload2.lean.expected.out b/tests/lean/overload2.lean.expected.out index 21026b1c6..41b0ea603 100644 --- a/tests/lean/overload2.lean.expected.out +++ b/tests/lean/overload2.lean.expected.out @@ -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 → Real → Real - Int::add : Int → Int → Int - Nat::add : Nat → Nat → 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 -> T -> R - f : T -> R -> T + g : R → T → R + f : T → R → T Arguments: b : R a : T diff --git a/tests/lean/tst3.lean.expected.out b/tests/lean/tst3.lean.expected.out index ae0ffe1d4..68ec51d4d 100644 --- a/tests/lean/tst3.lean.expected.out +++ b/tests/lean/tst3.lean.expected.out @@ -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 diff --git a/tests/lean/unicode.lean b/tests/lean/unicode.lean new file mode 100644 index 000000000..c24432cf2 --- /dev/null +++ b/tests/lean/unicode.lean @@ -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 diff --git a/tests/lean/unicode.lean.expected.out b/tests/lean/unicode.lean.expected.out new file mode 100644 index 000000000..a0da64bc2 --- /dev/null +++ b/tests/lean/unicode.lean.expected.out @@ -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