From 2fa25892202fcd409c2e398c780aff3aebd62285 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 8 Jul 2014 09:24:56 -0700 Subject: [PATCH] feat(frontends/lean): add pretty printer configuration options Signed-off-by: Leonardo de Moura --- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/pp_options.cpp | 68 +++++++++++++++++++++++++++++++ src/frontends/lean/pp_options.h | 17 ++++++++ 3 files changed, 86 insertions(+), 1 deletion(-) create mode 100644 src/frontends/lean/pp_options.cpp create mode 100644 src/frontends/lean/pp_options.h diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 7ef781ef4a..c73b1ec495 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -4,6 +4,6 @@ parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp interactive.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp proof_qed_ext.cpp -class.cpp) +class.cpp pp_options.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp new file mode 100644 index 0000000000..caf939908d --- /dev/null +++ b/src/frontends/lean/pp_options.cpp @@ -0,0 +1,68 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "frontends/lean/pp_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_NOTATION +#define LEAN_DEFAULT_PP_NOTATION true +#endif + +#ifndef LEAN_DEFAULT_PP_IMPLICIT +#define LEAN_DEFAULT_PP_IMPLICIT false +#endif + +#ifndef LEAN_DEFAULT_PP_COERCION +#define LEAN_DEFAULT_PP_COERCION false +#endif + +#ifndef LEAN_DEFAULT_PP_EXTRA_LETS +#define LEAN_DEFAULT_PP_EXTRA_LETS true +#endif + +#ifndef LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT +#define LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT 20 +#endif + +namespace lean { +static name g_pp_max_depth {"lean", "pp", "max_depth"}; +static name g_pp_max_steps {"lean", "pp", "max_steps"}; +static name g_pp_notation {"lean", "pp", "notation"}; +static name g_pp_implicit {"lean", "pp", "implicit"}; +static name g_pp_coercion {"lean", "pp", "coercion"}; +static name g_pp_extra_lets {"lean", "pp", "extra_lets"}; +static name g_pp_alias_min_weight {"lean", "pp", "alias_min_weight"}; + +RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, + "(lean pretty printer) maximum expression depth, after that it will use ellipsis"); +RegisterUnsignedOption(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS, + "(lean pretty printer) maximum number of visited expressions, after that it will use ellipsis"); +RegisterBoolOption(g_pp_notation, LEAN_DEFAULT_PP_NOTATION, + "(lean pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)"); +RegisterBoolOption(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT, + "(lean pretty printer) display implicit parameters"); +RegisterBoolOption(g_pp_coercion, LEAN_DEFAULT_PP_COERCION, + "(lean pretty printer) display coercions"); +RegisterBoolOption(g_pp_extra_lets, LEAN_DEFAULT_PP_EXTRA_LETS, + "(lean pretty printer) introduce extra let expressions when displaying shared terms"); +RegisterUnsignedOption(g_pp_alias_min_weight, LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT, + "(lean pretty printer) mimimal weight (approx. size) of a term to be considered a shared term"); + +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_notation(options const & opts) { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); } +bool get_pp_implicit(options const & opts) { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); } +bool get_pp_coercion(options const & opts) { return opts.get_bool(g_pp_coercion, LEAN_DEFAULT_PP_COERCION); } +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_weight(options const & opts) { return opts.get_unsigned(g_pp_alias_min_weight, LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT); } +} diff --git a/src/frontends/lean/pp_options.h b/src/frontends/lean/pp_options.h new file mode 100644 index 0000000000..470a0a9b7e --- /dev/null +++ b/src/frontends/lean/pp_options.h @@ -0,0 +1,17 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/sexpr/options.h" +namespace lean { +unsigned get_pp_max_depth(options const & opts); +unsigned get_pp_max_steps(options const & opts); +bool get_pp_notation(options const & opts); +bool get_pp_implicit(options const & opts); +bool get_pp_coercion(options const & opts); +bool get_pp_extra_lets(options const & opts); +unsigned get_pp_alias_min_weight(options const & opts); +}