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

feat(frontends/lean): add pretty printer configuration options

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-08 09:24:56 -07:00
parent 435a582bb0
commit 2fa2589220
3 changed files with 86 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/CMakeLists.txt
View file

@ -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})

68
src/frontends/lean/pp_options.cpp Normal file
View file

@ -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<unsigned>::max()
#endif
#ifndef LEAN_DEFAULT_PP_MAX_STEPS
#define LEAN_DEFAULT_PP_MAX_STEPS std::numeric_limits<unsigned>::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); }
}

17
src/frontends/lean/pp_options.h Normal file
View file

@ -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);
}