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

fix(frontends/lean/elaborator): pretty print placeholders as '_'

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-25 08:46:03 -07:00
parent e7c7d5718a
commit 736b219e65
1 changed files with 18 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/frontends/lean/pp.cpp
View file

@ -11,24 +11,26 @@ Author: Leonardo de Moura
#include "library/scoped_ext.h" #include "library/scoped_ext.h"
#include "library/coercion.h" #include "library/coercion.h"
#include "library/expr_pair.h" #include "library/expr_pair.h"
#include "library/placeholder.h"
#include "frontends/lean/pp.h" #include "frontends/lean/pp.h"
#include "frontends/lean/pp_options.h" #include "frontends/lean/pp_options.h"
#include "frontends/lean/token_table.h" #include "frontends/lean/token_table.h"
namespace lean { namespace lean {
static format g_ellipsis_n_fmt= highlight(format("\u2026")); static format g_ellipsis_n_fmt = highlight(format("\u2026"));
static format g_ellipsis_fmt = highlight(format("...")); static format g_ellipsis_fmt = highlight(format("..."));
static format g_lambda_n_fmt = highlight_keyword(format("\u03BB")); static format g_placeholder_fmt = highlight(format("_"));
static format g_lambda_fmt = highlight_keyword(format("fun")); static format g_lambda_n_fmt = highlight_keyword(format("\u03BB"));
static format g_forall_n_fmt = highlight_keyword(format("\u2200")); static format g_lambda_fmt = highlight_keyword(format("fun"));
static format g_forall_fmt = highlight_keyword(format("forall")); static format g_forall_n_fmt = highlight_keyword(format("\u2200"));
static format g_pi_n_fmt = highlight_keyword(format("Π")); static format g_forall_fmt = highlight_keyword(format("forall"));
static format g_pi_fmt = highlight_keyword(format("Pi")); static format g_pi_n_fmt = highlight_keyword(format("Π"));
static format g_arrow_n_fmt = highlight_keyword(format("\u2192")); static format g_pi_fmt = highlight_keyword(format("Pi"));
static format g_arrow_fmt = highlight_keyword(format("->")); static format g_arrow_n_fmt = highlight_keyword(format("\u2192"));
static format g_let_fmt = highlight_keyword(format("let")); static format g_arrow_fmt = highlight_keyword(format("->"));
static format g_in_fmt = highlight_keyword(format("in")); static format g_let_fmt = highlight_keyword(format("let"));
static format g_assign_fmt = highlight_keyword(format(":=")); static format g_in_fmt = highlight_keyword(format("in"));
static format g_assign_fmt = highlight_keyword(format(":="));
name pretty_fn::mk_metavar_name(name const & m) { name pretty_fn::mk_metavar_name(name const & m) {
if (auto it = m_purify_meta_table.find(m)) if (auto it = m_purify_meta_table.find(m))
@ -342,6 +344,9 @@ auto pretty_fn::pp(expr const & e) -> result {
flet<unsigned> let_d(m_depth, m_depth+1); flet<unsigned> let_d(m_depth, m_depth+1);
m_num_steps++; m_num_steps++;
if (is_placeholder(e))
return mk_result(g_placeholder_fmt);
switch (e.kind()) { switch (e.kind()) {
case expr_kind::Var: return pp_var(e); case expr_kind::Var: return pp_var(e);
case expr_kind::Sort: return pp_sort(e); case expr_kind::Sort: return pp_sort(e);