From 790d4a4447a82a1285bed42facd2e9dacb2edebe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 Aug 2013 18:54:01 -0700 Subject: [PATCH] Move pretty printer to frontend. Add support for mixfix pretty printing Signed-off-by: Leonardo de Moura --- src/exprlib/CMakeLists.txt | 2 + src/frontend/CMakeLists.txt | 2 +- src/frontend/builtin_notation.cpp | 19 ++ src/frontend/builtin_notation.h | 11 + src/frontend/frontend.cpp | 84 ++--- src/frontend/frontend.h | 15 +- src/frontend/operator_info.cpp | 6 +- src/frontend/operator_info.h | 6 +- src/frontend/pp.cpp | 539 ++++++++++++++++++++++++++++++ src/{kernel => frontend}/pp.h | 7 +- src/kernel/CMakeLists.txt | 2 +- src/kernel/environment.cpp | 1 - src/kernel/expr_formatter.h | 2 +- src/kernel/object.cpp | 18 +- src/kernel/pp.cpp | 213 ------------ src/tests/kernel/expr.cpp | 34 +- src/util/sexpr/format.cpp | 4 +- src/util/sexpr/options.cpp | 10 + src/util/sexpr/options.h | 2 + 19 files changed, 654 insertions(+), 323 deletions(-) create mode 100644 src/exprlib/CMakeLists.txt create mode 100644 src/frontend/builtin_notation.cpp create mode 100644 src/frontend/builtin_notation.h create mode 100644 src/frontend/pp.cpp rename src/{kernel => frontend}/pp.h (59%) delete mode 100644 src/kernel/pp.cpp diff --git a/src/exprlib/CMakeLists.txt b/src/exprlib/CMakeLists.txt new file mode 100644 index 0000000000..c75b2d23dd --- /dev/null +++ b/src/exprlib/CMakeLists.txt @@ -0,0 +1,2 @@ +add_library(exprlib basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp) +target_link_libraries(exprlib ${LEAN_LIBS}) diff --git a/src/frontend/CMakeLists.txt b/src/frontend/CMakeLists.txt index b44b9dc3b0..9347235f90 100644 --- a/src/frontend/CMakeLists.txt +++ b/src/frontend/CMakeLists.txt @@ -1,2 +1,2 @@ -add_library(frontend frontend.cpp operator_info.cpp scanner.cpp) +add_library(frontend frontend.cpp operator_info.cpp scanner.cpp pp.cpp builtin_notation.cpp) target_link_libraries(frontend ${LEAN_LIBS}) diff --git a/src/frontend/builtin_notation.cpp b/src/frontend/builtin_notation.cpp new file mode 100644 index 0000000000..c4a9d4ad86 --- /dev/null +++ b/src/frontend/builtin_notation.cpp @@ -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 +*/ +#include "frontend.h" +#include "builtin.h" + +namespace lean { +/** + \brief Initialize builtin notation. +*/ +void init_builtin_notation(frontend & f) { + f.add_infixl("\u2227", 13, const_name(mk_and_fn())); + f.add_infixl("\u2228", 14, const_name(mk_or_fn())); + f.add_prefix("\u00ac", 3, const_name(mk_not_fn())); +} +} diff --git a/src/frontend/builtin_notation.h b/src/frontend/builtin_notation.h new file mode 100644 index 0000000000..81f399f29c --- /dev/null +++ b/src/frontend/builtin_notation.h @@ -0,0 +1,11 @@ +/* +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 { +class frontend; +void init_builtin_notation(frontend & fe); +} diff --git a/src/frontend/frontend.cpp b/src/frontend/frontend.cpp index 64ae4e408f..d722e8b55c 100644 --- a/src/frontend/frontend.cpp +++ b/src/frontend/frontend.cpp @@ -9,6 +9,9 @@ Author: Leonardo de Moura #include "frontend.h" #include "environment.h" #include "operator_info.h" +#include "toplevel.h" +#include "builtin_notation.h" +#include "pp.h" namespace lean { /** @@ -26,9 +29,10 @@ public: virtual format pp(environment const &) const { char const * cmd; switch (m_op.get_fixity()) { - case fixity::Infixl: cmd = "Infixl"; break; - case fixity::Infixr: cmd = "Infixr"; break; - case fixity::Prefix: cmd = "Prefix"; break; + case fixity::Infix: cmd = "Infix"; break; + case fixity::Infixl: cmd = "Infixl"; break; + case fixity::Infixr: cmd = "Infixr"; break; + case fixity::Prefix: cmd = "Prefix"; break; case fixity::Postfix: cmd = "Postfix"; break; case fixity::Mixfixl: cmd = "Mixfixl"; break; case fixity::Mixfixr: cmd = "Mixfixr"; break; @@ -132,7 +136,7 @@ struct frontend::imp { /** \brief Remove all internal operators that are associated with the given operator symbol (aka notation) */ void remove_bindings(operator_info const & op) { for (name const & n : op.get_internal_names()) { - if (has_parent() && !is_nil(m_parent->find_op_for(n))) { + if (has_parent() && m_parent->find_op_for(n)) { // parent has a binding for n... we must hide it. insert(m_name_to_operator, n, operator_info()); } else { @@ -162,7 +166,7 @@ struct frontend::imp { void add_op(operator_info new_op, name const & n, bool led) { name const & opn = new_op.get_op_name(); operator_info old_op = find_op(opn, led); - if (is_nil(old_op)) { + if (!old_op) { register_new_op(new_op, n, led); } else if (old_op == new_op) { // overload @@ -182,24 +186,17 @@ struct frontend::imp { m_env.add_anonymous_object(new notation_declaration(new_op, n)); } - void add_infixl(name const & opn, unsigned precedence, name const & n) { - add_op(infixl(opn, precedence), n, true); - } + void add_infixl(name const & opn, unsigned p, name const & n) { add_op(infixl(opn, p), n, true); } + void add_infixr(name const & opn, unsigned p, name const & n) { add_op(infixr(opn, p), n, true); } + void add_prefix(name const & opn, unsigned p, name const & n) { add_op(prefix(opn, p), n, false); } + void add_postfix(name const & opn, unsigned p, name const & n) { add_op(postfix(opn, p), n, true); } + void add_mixfixl(unsigned sz, name const * opns, unsigned p, name const & n) { add_op(mixfixl(sz, opns, p), n, false); } + void add_mixfixr(unsigned sz, name const * opns, unsigned p, name const & n) { add_op(mixfixr(sz, opns, p), n, true); } + void add_mixfixc(unsigned sz, name const * opns, unsigned p, name const & n) { add_op(mixfixc(sz, opns, p), n, false); } - void add_infixr(name const & opn, unsigned precedence, name const & n) { - add_op(infixr(opn, precedence), n, true); - } - - void add_prefix(name const & opn, unsigned precedence, name const & n) { - add_op(prefix(opn, precedence), n, false); - } - - void add_postfix(name const & opn, unsigned precedence, name const & n) { - add_op(postfix(opn, precedence), n, true); - } - - imp(): - m_num_children(0) { + imp(frontend & fe): + m_num_children(0), + m_env(mk_toplevel()) { } explicit imp(std::shared_ptr const & parent): @@ -215,37 +212,18 @@ struct frontend::imp { } }; -frontend::frontend(): - m_imp(new imp()) { +frontend::frontend():m_imp(new imp(*this)) { + init_builtin_notation(*this); + m_imp->m_env.set_formatter(mk_pp_expr_formatter(*this, options())); } +frontend::frontend(imp * new_ptr):m_imp(new_ptr) {} +frontend::frontend(std::shared_ptr const & ptr):m_imp(ptr) {} +frontend::~frontend() {} -frontend::frontend(imp * new_ptr): - m_imp(new_ptr) { -} - -frontend::frontend(std::shared_ptr const & ptr): - m_imp(ptr) { -} - -frontend::~frontend() { -} - -frontend frontend::mk_child() const { - return frontend(new imp(m_imp)); -} - -bool frontend::has_children() const { - return m_imp->has_children(); -} - -bool frontend::has_parent() const { - return m_imp->has_parent(); -} - -frontend frontend::parent() const { - lean_assert(has_parent()); - return frontend(m_imp->m_parent); -} +frontend frontend::mk_child() const { return frontend(new imp(m_imp)); } +bool frontend::has_children() const { return m_imp->has_children(); } +bool frontend::has_parent() const { return m_imp->has_parent(); } +frontend frontend::parent() const { lean_assert(has_parent()); return frontend(m_imp->m_parent); } environment const & frontend::env() const { return m_imp->m_env; } @@ -257,6 +235,10 @@ void frontend::add_infixl(name const & opn, unsigned p, name const & n) { m_imp void frontend::add_infixr(name const & opn, unsigned p, name const & n) { m_imp->add_infixr(opn, p, n); } void frontend::add_prefix(name const & opn, unsigned p, name const & n) { m_imp->add_prefix(opn, p, n); } void frontend::add_postfix(name const & opn, unsigned p, name const & n) { m_imp->add_postfix(opn, p, n); } +void frontend::add_mixfixl(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixl(sz, opns, p, n); } +void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixr(sz, opns, p, n); } +void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixc(sz, opns, p, n); } +operator_info frontend::find_op_for(name const & n) const { return m_imp->find_op_for(n); } void frontend::display(std::ostream & out) const { m_imp->m_env.display(out); } } diff --git a/src/frontend/frontend.h b/src/frontend/frontend.h index 6479e66ab4..fa0b3d8fc8 100644 --- a/src/frontend/frontend.h +++ b/src/frontend/frontend.h @@ -6,10 +6,10 @@ Author: Leonardo de Moura */ #pragma once #include -#include "level.h" +#include "environment.h" +#include "operator_info.h" namespace lean { -class environment; /** \brief Object for managing the environment, parser, pretty printer, elaborator, etc. @@ -56,6 +56,17 @@ public: void add_infixr(name const & opn, unsigned precedence, name const & n); void add_prefix(name const & opn, unsigned precedence, name const & n); void add_postfix(name const & opn, unsigned precedence, name const & n); + void add_mixfixl(unsigned sz, name const * opns, unsigned precedence, name const & n); + void add_mixfixr(unsigned sz, name const * opns, unsigned precedence, name const & n); + void add_mixfixc(unsigned sz, name const * opns, unsigned precedence, name const & n); + /** + \brief Return the operator (if it exists) associated with the + given internal name. + + \remark If an operator is not associated with \c n, then + return the nil operator. + */ + operator_info find_op_for(name const & n) const; // ======================================= /** \brief Display universal variable constraints and objects stored in this environment and its parents. */ diff --git a/src/frontend/operator_info.cpp b/src/frontend/operator_info.cpp index 588525c190..c63436621f 100644 --- a/src/frontend/operator_info.cpp +++ b/src/frontend/operator_info.cpp @@ -76,6 +76,9 @@ bool operator==(operator_info const & op1, operator_info const & op2) { return true; } +operator_info infix(name const & op, unsigned precedence) { + return operator_info(new operator_info::imp(op, fixity::Infix, precedence)); +} operator_info infixr(name const & op, unsigned precedence) { return operator_info(new operator_info::imp(op, fixity::Infixr, precedence)); } @@ -103,6 +106,7 @@ static char const * g_arrow = "\u21a6"; format pp(operator_info const & o) { format r; switch (o.get_fixity()) { + case fixity::Infix: r = format("Infix"); break; case fixity::Infixl: r = format("Infixl"); break; case fixity::Infixr: r = format("Infixr"); break; case fixity::Prefix: r = format("Prefix"); break; @@ -118,7 +122,7 @@ format pp(operator_info const & o) { r += format{format(o.get_precedence()), space()}; switch (o.get_fixity()) { - case fixity::Infixl: case fixity::Infixr: case fixity::Prefix: case fixity::Postfix: + case fixity::Infix: case fixity::Infixl: case fixity::Infixr: case fixity::Prefix: case fixity::Postfix: r += pp(o.get_op_name()); break; case fixity::Mixfixl: for (auto p : o.get_op_name_parts()) r += format{pp(p), format(" _")}; diff --git a/src/frontend/operator_info.h b/src/frontend/operator_info.h index 60d26ab481..53e3715c49 100644 --- a/src/frontend/operator_info.h +++ b/src/frontend/operator_info.h @@ -20,7 +20,7 @@ namespace lean { Mixfixr: _ ID _ ID ... _ ID (has at least two parts) Mixfixc: ID _ ID _ ... ID _ ID (has at least two parts) */ -enum class fixity { Prefix, Infixl, Infixr, Postfix, Mixfixl, Mixfixr, Mixfixc }; +enum class fixity { Prefix, Infix, Infixl, Infixr, Postfix, Mixfixl, Mixfixr, Mixfixc }; /** \brief Data-structure for storing user defined operator @@ -43,8 +43,9 @@ public: friend void swap(operator_info & o1, operator_info & o2) { std::swap(o1.m_ptr, o2.m_ptr); } - friend bool is_nil(operator_info const & o) { return o.m_ptr == nullptr; } + operator bool() const { return m_ptr != nullptr; } + friend operator_info infix(name const & op, unsigned precedence); friend operator_info infixl(name const & op, unsigned precedence); friend operator_info infixr(name const & op, unsigned precedence); friend operator_info prefix(name const & op, unsigned precedence); @@ -86,6 +87,7 @@ public: friend bool operator==(operator_info const & op1, operator_info const & op2); friend bool operator!=(operator_info const & op1, operator_info const & op2) { return !(op1 == op2); } }; +operator_info infix(name const & op, unsigned precedence); operator_info infixl(name const & op, unsigned precedence); operator_info infixr(name const & op, unsigned precedence); operator_info prefix(name const & op, unsigned precedence); diff --git a/src/frontend/pp.cpp b/src/frontend/pp.cpp new file mode 100644 index 0000000000..4c81876c17 --- /dev/null +++ b/src/frontend/pp.cpp @@ -0,0 +1,539 @@ +/* +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 +#include +#include "frontend.h" +#include "context.h" +#include "scoped_map.h" +#include "expr_formatter.h" +#include "occurs.h" +#include "instantiate.h" +#include "options.h" + +#ifndef LEAN_DEFAULT_PP_MAX_DEPTH +#define LEAN_DEFAULT_PP_MAX_DEPTH std::numeric_limits::max() +#endif + +#ifndef LEAN_DEFAULT_PP_MAX_STEPS +#define LEAN_DEFAULT_PP_MAX_STEPS std::numeric_limits::max() +#endif + +#ifndef LEAN_DEFAULT_PP_IMPLICIT +#define LEAN_DEFAULT_PP_IMPLICIT false +#endif + +#ifndef LEAN_DEFAULT_PP_NOTATION +#define LEAN_DEFAULT_PP_NOTATION true +#endif + +#ifndef LEAN_DEFAULT_PP_EXTRA_LETS +#define LEAN_DEFAULT_PP_EXTRA_LETS true +#endif + +#ifndef LEAN_DEFAULT_PP_ALIAS_MIN_DEPTH +#define LEAN_DEFAULT_PP_ALIAS_MIN_DEPTH 1000 //TODO: fix to reasonable value +#endif + +namespace lean { +static format g_Type_fmt = highlight_builtin(format("Type")); +static unsigned g_eq_prec = 20; +static format g_eq_fmt = format("="); +static char const * g_eq_sym = "eq"; +static unsigned g_eq_sz = strlen(g_eq_sym); +static format g_eq_sym_fmt = format(g_eq_sym); +static format g_lambda_fmt = highlight_keyword(format("\u03BB")); +static format g_Pi_fmt = highlight_keyword(format("\u03A0")); +static format g_arrow_fmt = highlight_keyword(format("\u2192")); +static format g_ellipsis_fmt = highlight(format("\u2026")); +static format g_let_fmt = highlight_keyword(format("let")); +static format g_in_fmt = highlight_keyword(format("in")); + +static name g_pp_max_depth {"pp", "max_depth"}; +static name g_pp_max_steps {"pp", "max_steps"}; +static name g_pp_implicit {"pp", "implicit"}; +static name g_pp_notation {"pp", "notation"}; +static name g_pp_extra_lets {"pp", "extra_lets"}; +static name g_pp_alias_min_depth {"pp", "alias_min_depth"}; + +unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); } +unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); } +bool get_pp_implicit(options const & opts) { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); } +bool get_pp_notation(options const & opts) { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); } +bool get_pp_extra_lets(options const & opts) { return opts.get_bool(g_pp_extra_lets, LEAN_DEFAULT_PP_EXTRA_LETS); } +unsigned get_pp_alias_min_depth(options const & opts) { return opts.get_unsigned(g_pp_alias_min_depth, LEAN_DEFAULT_PP_ALIAS_MIN_DEPTH); } + +/** \brief Functional object for pretty printing expressions */ +struct pp_fn { + typedef scoped_map aliases; + typedef std::vector> aliases_defs; + frontend const & m_frontend; + context const & m_context; + // State + aliases m_aliases; + aliases_defs m_aliases_defs; + unsigned m_num_steps; + name m_aux; + // Configuration + unsigned m_indent; + unsigned m_max_depth; + unsigned m_max_steps; + bool m_implict; + bool m_notation; //!< if true use notation + bool m_extra_lets; //!< introduce extra let-expression to cope with sharing. + unsigned m_alias_min_depth; //!< minimal depth to create an alias + + // Create a scope for local definitions + struct mk_scope { + pp_fn & m_fn; + unsigned m_old_size; + mk_scope(pp_fn & fn):m_fn(fn), m_old_size(fn.m_aliases_defs.size()) { + m_fn.m_aliases.push(); + } + ~mk_scope() { + lean_assert(m_old_size <= m_fn.m_aliases_defs.size()); + m_fn.m_aliases.pop(); + m_fn.m_aliases_defs.resize(m_old_size); + } + }; + + format nest(unsigned i, format const & f) { return ::lean::nest(i, f); } + + typedef std::pair result; + + /** + \brief Return true iff \c e is an atomic operation. + */ + bool is_atomic(expr const & e) { + switch (e.kind()) { + case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: case expr_kind::Type: + return true; + case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Eq: case expr_kind::Let: + return false; + } + return false; + } + + result mk_result(format const & fmt, unsigned depth) { + return mk_pair(fmt, depth); + } + + result pp_ellipsis() { + return mk_result(g_ellipsis_fmt, 1); + } + + result pp_var(expr const & e) { + unsigned vidx = var_idx(e); + return mk_result(compose(format("#"), format(vidx)), 1); + } + + result pp_constant(expr const & e) { + return mk_result(::lean::pp(const_name(e)), 1); + } + + result pp_value(expr const & e) { + return mk_result(to_value(e).pp(), 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); + } + } + + /** + \brief Return the operator associated with \c e. + Return the nil operator if there is none. + + We say \c e has an operator associated with it, if: + + 1) It is a constant and there is an operator associated with it. + + 2) It is an application, and the function is a constant \c c with an + operator associated with \c c. + */ + operator_info get_operator(expr const & e) { + if (is_constant(e)) + return m_frontend.find_op_for(const_name(e)); + else if (is_app(e) && is_constant(arg(e, 0))) + return m_frontend.find_op_for(const_name(arg(e, 0))); + else + return operator_info(); + } + + /** \brief Return true if the application \c e has the number of arguments expected by the operator \c op. */ + bool has_expected_num_args(expr const & e, operator_info const & op) { + switch (op.get_fixity()) { + case fixity::Infix: case fixity::Infixl: case fixity::Infixr: + return num_args(e) == 3; + case fixity::Prefix: case fixity::Postfix: + return num_args(e) == 2; + case fixity::Mixfixl: case fixity::Mixfixr: + return num_args(e) == length(op.get_op_name_parts()) + 1; + case fixity::Mixfixc: + return num_args(e) == length(op.get_op_name_parts()); + } + lean_unreachable(); + return false; + } + + /** + \brief Pretty print given expression and put parenthesis around it. + */ + result pp_child_with_paren(expr const & e, unsigned depth) { + result r = pp(e, depth + 1); + return mk_result(format{lp(), r.first, rp()}, r.second); + } + + /** + \brief Pretty print given expression and put parenthesis around + it if it is not atomic. + */ + result pp_child(expr const & e, unsigned depth) { + if (is_atomic(e)) + return pp(e, depth + 1); + else + return pp_child_with_paren(e, depth); + } + + /** + \brief Pretty print the child of an infix, prefix, postfix or + mixfix operator. It will add parethesis when needed. + */ + result pp_mixfix_child(operator_info const & op, expr const & e, unsigned depth) { + if (is_atomic(e)) { + return pp(e, depth + 1); + } else { + operator_info op_child = get_operator(e); + if (op_child && op.get_precedence() < op_child.get_precedence()) + return pp(e, depth + 1); + else + return pp_child_with_paren(e, depth); + } + } + + /** + \brief Pretty print the child of an associative infix + operator. It will add parethesis when needed. + */ + result pp_infix_child(operator_info const & op, expr const & e, unsigned depth) { + if (is_atomic(e)) { + return pp(e, depth + 1); + } else { + operator_info op_child = get_operator(e); + if (op_child && (op == op_child || op.get_precedence() < op_child.get_precedence())) + return pp(e, depth + 1); + else + return pp_child_with_paren(e, depth); + } + } + + result mk_infix(operator_info const & op, result const & lhs, result const & rhs) { + unsigned r_depth = std::max(lhs.second, rhs.second) + 1; + format r_format = group(format{lhs.first, space(), format(op.get_op_name()), line(), rhs.first}); + return mk_result(r_format, r_depth); + } + + /** + \brief Pretty print an application. + */ + result pp_app(expr const & e, unsigned depth) { + operator_info op; + if (m_notation && (op = get_operator(e)) && has_expected_num_args(e, op)) { + result p_arg; + format r_format; + unsigned sz; + unsigned r_depth = 0; + switch (op.get_fixity()) { + case fixity::Infix: + return mk_infix(op, pp_mixfix_child(op, arg(e, 1), depth), pp_mixfix_child(op, arg(e, 2), depth)); + case fixity::Infixr: + return mk_infix(op, pp_mixfix_child(op, arg(e, 1), depth), pp_infix_child(op, arg(e, 2), depth)); + case fixity::Infixl: + return mk_infix(op, pp_infix_child(op, arg(e, 1), depth), pp_mixfix_child(op, arg(e, 2), depth)); + case fixity::Prefix: + p_arg = pp_infix_child(op, arg(e, 1), depth); + sz = op.get_op_name().size(); + return mk_result(group(format{format(op.get_op_name()), nest(sz+1, format{line(), p_arg.first})}), + p_arg.second + 1); + case fixity::Postfix: + p_arg = pp_mixfix_child(op, arg(e, 1), depth); + return mk_result(group(format{p_arg.first, space(), format(op.get_op_name())}), + p_arg.second + 1); + case fixity::Mixfixr: { + // _ ID ... _ ID + list parts = op.get_op_name_parts(); + auto it = parts.begin(); + for (unsigned i = 1; i < num_args(e); i++) { + result p_arg = pp_mixfix_child(op, arg(e, i), depth); + r_format += format{p_arg.first, space(), format(*it), line()}; + r_depth = std::max(r_depth, p_arg.second); + ++it; + } + return mk_result(group(r_format), r_depth + 1); + } + case fixity::Mixfixl: case fixity::Mixfixc: { + // ID _ ... _ + // ID _ ... _ ID + list parts = op.get_op_name_parts(); + auto it = parts.begin(); + for (unsigned i = 1; i < num_args(e); i++) { + result p_arg = pp_mixfix_child(op, arg(e, i), depth); + unsigned sz = (*it).size(); + r_format += format{format(*it), nest(sz+1, format{line(), p_arg.first})}; + r_depth = std::max(r_depth, p_arg.second); + ++it; + } + if (it != parts.end()) { + // it is Mixfixc + r_format += format{space(), format(*it)}; + } + return mk_result(group(r_format), r_depth + 1); + }} + lean_unreachable(); + return mk_result(format(), 0); + } else { + // standard function application + result p = pp_child(arg(e, 0), depth); + format r_format = p.first; + unsigned r_depth = p.second; + for (unsigned i = 1; i < num_args(e); i++) { + result p_arg = pp_child(arg(e, i), depth); + r_format += format{line(), p_arg.first}; + r_depth = std::max(r_depth, p_arg.second); + } + return mk_result(group(nest(m_indent, r_format)), r_depth + 1); + } + } + + /** + \brief Collect nested Lambdas (or Pis), and instantiate + variables with unused names. Store in \c r the selected names + and associated domains. Return the body of the sequence of + Lambda (of Pis). + */ + expr collect_nested(expr const & e, expr_kind k, buffer> & r) { + if (e.kind() == k) { + name const & n = abst_name(e); + name n1 = n; + unsigned i = 1; + while (occurs(n1, abst_body(e))) { + n1 = name(n, i); + i++; + } + r.push_back(mk_pair(n1, abst_domain(e))); + expr b = instantiate_with_closed(abst_body(e), mk_constant(n1)); + return collect_nested(b, k, r); + } else { + return e; + } + } + + result pp_scoped_child(expr const & e, unsigned depth) { + if (is_atomic(e)) { + return pp(e, depth + 1); + } else { + mk_scope s(*this); + // TODO: create Let with new aliases + return pp(e, depth+1); + } + } + + result pp_arrow_body(expr const & e, unsigned depth) { + if (is_atomic(e) || is_arrow(e)) { + return pp(e, depth + 1); + } else { + return pp_child_with_paren(e, depth); + } + } + + template + format pp_bnames(It const & begin, It const & end, bool use_line) { + auto it = begin; + format r = format(it->first); + ++it; + for (; it != end; ++it) { + r += compose(use_line ? line() : space(), format(it->first)); + } + return r; + } + + result pp_abstraction(expr const & e, unsigned depth) { + if (is_arrow(e)) { + 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(), g_arrow_fmt, line(), p_rhs.first}); + return mk_result(r_format, std::max(p_lhs.second, p_rhs.second) + 1); + } else { + buffer> nested; + expr b = collect_nested(e, e.kind(), nested); + lean_assert(b.kind() != e.kind()); + format head = is_lambda(e) ? g_lambda_fmt : g_Pi_fmt; + format body_sep = comma(); + + expr domain0 = nested[0].second; + if (std::all_of(nested.begin() + 1, nested.end(), [&](std::pair const & p) { return p.second == domain0; })) { + // Domain of all binders is the same + format names = pp_bnames(nested.begin(), nested.end(), false); + result p_domain = pp_scoped_child(domain0, depth); + result p_body = pp_scoped_child(b, depth); + format r_format = group(nest(m_indent, format{head, space(), names, space(), colon(), space(), p_domain.first, body_sep, line(), p_body.first})); + return mk_result(r_format, std::max(p_domain.second, p_body.second)+1); + } else { + auto it = nested.begin(); + auto end = nested.end(); + unsigned r_depth; + // PP binders in blocks (names ... : type) + bool first = true; + format bindings; + while (it != end) { + auto it2 = it; + ++it2; + while (it2 != end && it2->second == it->second) { + ++it2; + } + result p_domain = pp_scoped_child(it->second, depth); + r_depth = std::max(r_depth, p_domain.second); + format block = group(nest(m_indent, format{lp(), pp_bnames(it, it2, true), space(), colon(), space(), p_domain.first, rp()})); + if (first) { + bindings = block; + first = false; + } else { + bindings += compose(line(), block); + } + it = it2; + } + result p_body = pp_scoped_child(b, depth); + format r_format = group(nest(m_indent, format{head, space(), group(bindings), body_sep, line(), p_body.first})); + return mk_result(r_format, std::max(r_depth, p_body.second)+1); + } + } + } + + result pp_let(expr const & e, unsigned depth) { + // TODO + return mk_result(format("TODO"), 1); + } + + /** \brief Pretty print the child of an equality. */ + result pp_eq_child(expr const & e, unsigned depth) { + if (is_atomic(e)) { + return pp(e, depth + 1); + } else { + operator_info op_child = get_operator(e); + if (op_child && g_eq_prec < op_child.get_precedence()) + return pp(e, depth + 1); + else + return pp_child_with_paren(e, depth); + } + } + + /** \brief Pretty print an equality */ + result pp_eq(expr const & e, unsigned depth) { + result p_arg1, p_arg2; + format r_format; + if (m_notation) { + p_arg1 = pp_eq_child(eq_lhs(e), depth); + p_arg2 = pp_eq_child(eq_rhs(e), depth); + r_format = group(format{p_arg1.first, space(), g_eq_fmt, line(), p_arg2.first}); + + } else { + p_arg1 = pp_child(eq_lhs(e), depth); + p_arg2 = pp_child(eq_rhs(e), depth); + r_format = group(format{g_eq_sym_fmt, nest(g_eq_sz + 1, + format{line(), p_arg1.first, + line(), p_arg2.first})}); + } + return mk_result(r_format, std::max(p_arg1.second, p_arg2.second) + 1); + } + + result pp(expr const & e, unsigned depth) { + if (m_num_steps > m_max_steps || depth > m_max_depth) { + return pp_ellipsis(); + } else { + m_num_steps++; + if (m_extra_lets && is_shared(e)) { + auto it = m_aliases.find(e); + if (it != m_aliases.end()) + return mk_result(format(it->second), 1); + } + result r; + switch (e.kind()) { + case expr_kind::Var: r = pp_var(e); break; + case expr_kind::Constant: r = pp_constant(e); break; + case expr_kind::Value: r = pp_value(e); break; + case expr_kind::App: r = pp_app(e, depth); break; + case expr_kind::Lambda: + case expr_kind::Pi: r = pp_abstraction(e, depth); break; + case expr_kind::Type: r = pp_type(e); break; + case expr_kind::Eq: r = pp_eq(e, depth); break; + case expr_kind::Let: r = pp_let(e, depth); break; + } + if (m_extra_lets && is_shared(e) && r.second > m_alias_min_depth) { + std::cout << "DEPTH: " << r.second << "\n"; + name new_aux = name(m_aux, m_aliases.size()); + m_aliases.insert(e, new_aux); + return mk_result(format(new_aux), 1); + } + return r; + } + } + + void set_options(options const & opts) { + m_indent = get_pp_indent(opts); + m_max_depth = get_pp_max_depth(opts); + m_max_steps = get_pp_max_steps(opts); + m_implict = get_pp_implicit(opts); + m_notation = get_pp_notation(opts); + m_extra_lets = get_pp_extra_lets(opts); + m_alias_min_depth = get_pp_alias_min_depth(opts); + } + + pp_fn(frontend const & fe, context const & ctx, options const & opts): + m_frontend(fe), + m_context(ctx) { + set_options(opts); + } + + format operator()(expr const & e) { + m_aliases.clear(); + m_aliases_defs.clear(); + m_num_steps = 0; + m_aux = name("aux"); // TODO: find non used prefix + return pp(e, 0).first; + } +}; + +class pp_expr_formatter : public expr_formatter { + frontend const & m_frontend; + options m_options; +public: + pp_expr_formatter(frontend const & fe, options const & opts): + m_frontend(fe), + m_options(opts) { + } + + virtual ~pp_expr_formatter() { + } + + virtual options get_options() const { + return m_options; + } + + // TODO: remove context parameter from expr_formatter + // The context pretty printer must open the expression + // before pretty-printing it. + virtual format operator()(expr const & e, context const & c) { + return pp_fn(m_frontend, c, m_options)(e); + } +}; + +std::shared_ptr mk_pp_expr_formatter(frontend const & fe, options const & opts) { + return std::shared_ptr(new pp_expr_formatter(fe, opts)); +} +} diff --git a/src/kernel/pp.h b/src/frontend/pp.h similarity index 59% rename from src/kernel/pp.h rename to src/frontend/pp.h index 36e495fd02..e470038b6e 100644 --- a/src/kernel/pp.h +++ b/src/frontend/pp.h @@ -5,11 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "expr.h" -#include "format.h" +#include "expr_formatter.h" namespace lean { -class environment; -format pp(expr const & n); -format pp(expr const & n, environment const & env); +std::shared_ptr mk_pp_expr_formatter(frontend const & fe, options const & opts); } diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 98582fd6f5..3ea2bbee69 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,6 +1,6 @@ add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp normalize.cpp context.cpp level.cpp object.cpp environment.cpp type_check.cpp builtin.cpp expr_formatter.cpp expr_locator.cpp - occurs.cpp pp.cpp) + occurs.cpp) target_link_libraries(kernel ${LEAN_LIBS}) diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index ef6978d3ab..6b0735cc32 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -13,7 +13,6 @@ Author: Leonardo de Moura #include "safe_arith.h" #include "type_check.h" #include "exception.h" -#include "pp.h" #include "debug.h" namespace lean { diff --git a/src/kernel/expr_formatter.h b/src/kernel/expr_formatter.h index e5188bd9b0..c075cf6024 100644 --- a/src/kernel/expr_formatter.h +++ b/src/kernel/expr_formatter.h @@ -15,7 +15,7 @@ class expr_formatter { public: virtual ~expr_formatter() {} /** \brief Convert expression in the given context into a format object. */ - virtual format operator()(expr const & e, context const & c) = 0; + virtual format operator()(expr const & e, context const & c = context()) = 0; /** \brief Return options for pretty printing. */ virtual options get_options() const = 0; diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp index c9a2ce1ed1..18df9c48ea 100644 --- a/src/kernel/object.cpp +++ b/src/kernel/object.cpp @@ -6,14 +6,8 @@ Author: Leonardo de Moura */ #include "object.h" #include "environment.h" -#include "pp.h" // TODO: move to front-end namespace lean { -// TODO: delete hardcoded -format pp_object_kind(char const * n) { return highlight_command(format(n)); } -constexpr unsigned indentation = 2; // TODO: must be option -// - object::~object() {} void object::display(std::ostream & out, environment const & env) const { out << pp(env); } @@ -41,9 +35,10 @@ bool definition::is_definition() const { return true; } bool definition::is_opaque() const { return m_opaque; } expr const & definition::get_value() const { return m_value; } format definition::pp(environment const & env) const { - return nest(indentation, - format{pp_object_kind(keyword()), format(" "), format(get_name()), format(" : "), ::lean::pp(get_type(), env), format(" :="), - line(), ::lean::pp(get_value()), format(".")}); + expr_formatter & fmt = env.get_formatter(); + format def = format{highlight_command(format(keyword())), space(), format(get_name()), space(), colon(), space(), + fmt(get_type()), format(" :="), line(), fmt(get_value())}; + return group(fmt.nest(def)); } char const * theorem::g_keyword = "Theorem"; @@ -57,8 +52,9 @@ bool fact::is_definition() const { return false; } bool fact::is_opaque() const { lean_unreachable(); return false; } expr const & fact::get_value() const { lean_unreachable(); return expr::null(); } format fact::pp(environment const & env) const { - return nest(indentation, - format{pp_object_kind(keyword()), format(" "), format(get_name()), format(" : "), ::lean::pp(get_type(), env), format(".")}); + expr_formatter & fmt = env.get_formatter(); + format def = format{highlight_command(format(keyword())), space(), format(get_name()), space(), colon(), space(), fmt(get_type())}; + return group(fmt.nest(def)); } char const * axiom::g_keyword = "Axiom"; diff --git a/src/kernel/pp.cpp b/src/kernel/pp.cpp deleted file mode 100644 index 6af9498ed6..0000000000 --- a/src/kernel/pp.cpp +++ /dev/null @@ -1,213 +0,0 @@ -/* -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 "pp.h" -#include "environment.h" -#include "scoped_set.h" -#include "for_each.h" -#include "instantiate.h" - -namespace lean { -struct pp_fn { - environment const * m_env; - - pp_fn(environment const * env):m_env(env) {} - - unsigned indent() const { return 2; } - format pp_keyword(char const * k) { return highlight_keyword(format(k)); } - format pp_type_kwd() { return highlight_builtin(format("Type")); } - format pp_eq_kwd() { return format(" = "); } - format pp_lambda_kwd() { return pp_keyword("\u03BB "); } - format pp_lambda_sep() { return format(","); } - format pp_pi_kwd() { return pp_keyword("\u03A0 "); } - format pp_pi_sep() { return format(","); } - format pp_type_arrow() { return format(" \u2192 "); } - format pp_colon() { return format(" : "); } - format pp_space() { return format(" "); } - format pp_lp() { return format("("); } - format pp_rp() { return format(")"); } - - bool is_atomic(expr const & e) { - switch (e.kind()) { - case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: case expr_kind::Type: - return true; - case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Eq: case expr_kind::Let: - return false; - } - return false; - } - - format pp_var(expr const & e) { - unsigned vidx = var_idx(e); - return compose(format("#"), format(vidx)); - } - - format pp_constant(expr const & e) { - return ::lean::pp(const_name(e)); - } - - format pp_value(expr const & e) { - return to_value(e).pp(); - } - - format pp_type(expr const & e) { - if (e == Type()) { - return pp_type_kwd(); - } else { - return format{pp_type_kwd(), pp_space(), ::lean::pp(ty_level(e))}; - } - } - - format pp_child(expr const & c) { - if (is_atomic(c)) - return pp(c); - else - return format{pp_lp(), pp(c), pp_rp()}; - } - - format pp_eq(expr const & e) { - return format{pp_child(eq_lhs(e)), pp_eq_kwd(), pp_child(eq_rhs(e))}; - } - - format pp_app(expr const & e) { - // TODO: infix operators, implicit arguments - - // Prefix case - format r = pp_child(arg(e, 0)); - for (unsigned i = 1; i < num_args(e); i++) { - r += compose(line(), pp_child(arg(e, i))); - } - return group(nest(indent(), r)); - } - - format pp_arrow_body(expr const & e) { - if (is_atomic(e) || is_arrow(e)) - return pp(e); - else - return pp_child(e); - } - - struct is_used {}; - - /** \brief Return true iff \c n is already used in body */ - bool used(name const & n, expr const & body) { - auto visitor = [&](expr const & e, unsigned offset) -> void { - if (is_constant(e)) { - if (const_name(e) == n) - throw is_used(); - } - }; - - try { - for_each_fn f(visitor); - f(body); - return false; - } catch (is_used) { - return true; - } - } - - format pp_bname(expr const & binder) { - return ::lean::pp(abst_name(binder)); - } - - template - format pp_bnames(It const & begin, It const & end, bool use_line) { - static_assert(std::is_same::value_type, expr>::value, - "pp_bnames takes an argument which is not an iterator containing expr."); - auto it = begin; - format r = pp_bname(*it); - ++it; - for (; it != end; ++it) { - r += compose(use_line ? line() : pp_space(), pp_bname(*it)); - } - return r; - } - - expr collect_nested(expr const & e, expr_kind k, buffer & r) { - if (e.kind() == k) { - r.push_back(e); - name const & n = abst_name(e); - name n1 = n; - unsigned i = 1; - while (used(n1, abst_body(e))) { - n1 = name(n, i); - i++; - } - expr b = instantiate_with_closed(abst_body(e), mk_constant(n1)); - return collect_nested(b, k, r); - } else { - return e; - } - } - - format pp_abstraction(expr const & e) { - if (is_arrow(e)) { - return format{pp_child(abst_domain(e)), pp_type_arrow(), pp_arrow_body(abst_body(e))}; - } else { - buffer nested; - expr b = collect_nested(e, e.kind(), nested); - lean_assert(b.kind() != e.kind()); - format head = is_lambda(e) ? pp_lambda_kwd() : pp_pi_kwd(); - format body_sep = is_lambda(e) ? pp_lambda_sep() : pp_pi_sep(); - - if (std::all_of(nested.begin(), nested.end(), [&](expr const & a) { return abst_domain(a) == abst_domain(e); })) { - // Domain of all binders is the same - format names = pp_bnames(nested.begin(), nested.end(), false); - return group(nest(indent(), format{head, names, pp_colon(), pp(abst_domain(e)), body_sep, line(), pp(b)})); - } else { - auto it = nested.begin(); - auto end = nested.end(); - // PP binders in blocks (names ... : type) - bool first = true; - format bindings; - while (it != end) { - auto it2 = it; - ++it2; - while (it2 != end && abst_domain(*it2) == abst_domain(*it)) { - ++it2; - } - format block = group(nest(indent(), format{pp_lp(), pp_bnames(it, it2, true), pp_colon(), pp(abst_domain(*it)), pp_rp()})); - if (first) { - bindings = block; - first = false; - } else { - bindings += compose(line(), block); - } - it = it2; - } - return group(nest(indent(), format{head, group(bindings), body_sep, line(), pp(b)})); - } - } - } - - format pp_let(expr const & e) { - return format("TODO"); - } - - format pp(expr const & e) { - switch (e.kind()) { - case expr_kind::Var: return pp_var(e); - case expr_kind::Constant: return pp_constant(e); - case expr_kind::Value: return pp_value(e); - case expr_kind::App: return pp_app(e); - case expr_kind::Lambda: - case expr_kind::Pi: return pp_abstraction(e); - case expr_kind::Type: return pp_type(e); - case expr_kind::Eq: return pp_eq(e); - case expr_kind::Let: return pp_let(e); - } - lean_unreachable(); - return format(); - } - - format operator()(expr const & e) { - return pp(e); - } -}; -format pp(expr const & n) { return pp_fn(0)(n); } -format pp(expr const & n, environment const & env) { return pp_fn(&env)(n); } -} diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 076b0607c5..83539853fb 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -15,7 +15,6 @@ Author: Leonardo de Moura #include "instantiate.h" #include "deep_copy.h" #include "arith.h" -#include "pp.h" using namespace lean; void tst1() { @@ -39,23 +38,6 @@ void tst1() { std::cout << mk_pi("x", ty, Var(0)) << "\n"; } -void tst1_pp() { - std::cerr << "=============== PP =====================\n"; - expr a; - a = Const("a"); - expr f; - f = Var(0); - expr fa = f(a); - expr ty = Type(); - std::cout << pp(fa(a)) << "\n"; - std::cout << pp(fa(fa, fa)) << "\n"; - std::cout << pp(mk_lambda("x", ty, Var(0))) << "\n"; - std::cout << pp(mk_pi("x", ty, Var(0))) << "\n"; - std::cout << pp(mk_pi("x", ty, mk_lambda("y", ty, Var(0)))) << "\n"; - std::cerr << "=============== PP =====================\n"; -} - - expr mk_dag(unsigned depth, bool _closed = false) { expr f = Const("f"); expr a = _closed ? Const("a") : Var(0); @@ -214,9 +196,9 @@ void tst5() { std::cout << "count(r1): " << count(r1) << "\n"; std::cout << "count(r2): " << count(r2) << "\n"; std::cout << "r1 = " << std::endl; - std::cout << pp(r1) << std::endl; + std::cout << r1 << std::endl; std::cout << "r2 = " << std::endl; - std::cout << pp(r2) << std::endl; + std::cout << r2 << std::endl; lean_assert(r1 == r2); } { @@ -278,10 +260,6 @@ void tst8() { r = mk_lambda("y", p, mk_app({mk_lambda("x", p, Var(0)), Var(1)})); lean_assert(!closed(r)); lean_assert(closed(mk_lambda("z", p, r))); - - std::cout << pp(mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(0)}))) << std::endl; - std::cout << pp(mk_pi("x", p, f(f(f(a))))) << std::endl; - } void tst9() { @@ -371,18 +349,11 @@ void tst15() { lean_assert(closed(l)); } -void tst16() { - std::cout << pp(Type() >> ((Int >> Int) >> (Int >> Bool))) << "\n"; - expr x = Const("x"); expr y = Const("y"); expr f = Const("f"); - std::cout << pp(Fun({{x, Int}, {y, Int}, {x, Bool}, {f, Pi({x,Bool}, x)}}, f(x, f(Eq(y,Var(3)), iVal(10))))) << "\n"; -} - int main() { std::cout << "sizeof(expr): " << sizeof(expr) << "\n"; std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n"; std::cout << "sizeof(expr_cell): " << sizeof(expr_cell) << "\n"; tst1(); - tst1_pp(); tst2(); tst3(); tst4(); @@ -397,7 +368,6 @@ int main() { tst13(); tst14(); tst15(); - tst16(); std::cout << "done" << "\n"; return has_violations() ? 1 : 0; } diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 2deac2474f..f24264403a 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -41,7 +41,7 @@ static name g_pp_colors{"pp", "colors"}; static name g_pp_width{"pp", "width"}; unsigned get_pp_indent(options const & o) { - return o.get_int(g_pp_indent, LEAN_DEFAULT_PP_INDENTATION); + return o.get_unsigned(g_pp_indent, LEAN_DEFAULT_PP_INDENTATION); } bool get_pp_colors(options const & o) { @@ -49,7 +49,7 @@ bool get_pp_colors(options const & o) { } unsigned get_pp_width(options const & o) { - return o.get_int(g_pp_width, LEAN_DEFAULT_PP_WIDTH); + return o.get_unsigned(g_pp_width, LEAN_DEFAULT_PP_WIDTH); } std::ostream & layout(std::ostream & out, bool colors, sexpr const & s) { diff --git a/src/util/sexpr/options.cpp b/src/util/sexpr/options.cpp index 036757412e..a3450da684 100644 --- a/src/util/sexpr/options.cpp +++ b/src/util/sexpr/options.cpp @@ -35,6 +35,11 @@ int options::get_int(name const & n, int default_value) const { return !is_nil(r) && is_int(r) ? to_int(r) : default_value; } +unsigned options::get_unsigned(name const & n, unsigned default_value) const { + sexpr const & r = get_sexpr(n); + return !is_nil(r) && is_int(r) ? static_cast(to_int(r)) : default_value; +} + bool options::get_bool(name const & n, bool default_value) const { sexpr const & r = get_sexpr(n); return !is_nil(r) && is_bool(r) ? to_bool(r) != 0 : default_value; @@ -60,6 +65,11 @@ int options::get_int(char const * n, int default_value) const { return !is_nil(r) && is_int(r) ? to_int(r) : default_value; } +unsigned options::get_unsigned(char const * n, unsigned default_value) const { + sexpr const & r = get_sexpr(n); + return !is_nil(r) && is_int(r) ? static_cast(to_int(r)) : default_value; +} + bool options::get_bool(char const * n, bool default_value) const { sexpr const & r = get_sexpr(n); return !is_nil(r) && is_bool(r) ? to_bool(r) != 0 : default_value; diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h index 847bf619d1..33c5126045 100644 --- a/src/util/sexpr/options.h +++ b/src/util/sexpr/options.h @@ -31,12 +31,14 @@ public: bool get_bool(name const & n, bool default_value=false) const; int get_int(name const & n, int default_value=0) const; + unsigned get_unsigned(name const & n, unsigned default_value=0) const; double get_double(name const & n, double default_value=0.0) const; char const * get_string(name const & n, char const * default_value=nullptr) const; sexpr get_sexpr(name const & n, sexpr const & default_value=sexpr()) const; bool get_bool(char const * n, bool default_value=false) const; int get_int(char const * n, int default_value=0) const; + unsigned get_unsigned(char const * n, unsigned default_value=0) const; double get_double(char const * n, double default_value=0.0) const; char const * get_string(char const * n, char const * default_value=nullptr) const; sexpr get_sexpr(char const * n, sexpr const & default_value=sexpr()) const;