From 4ec2101b06e20f0fef223e95cb631edbfec1a109 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 28 Nov 2014 14:49:00 -0800
Subject: [PATCH] feat(frontends/lean): add option 'pp.purify_locals'

---
 src/frontends/lean/pp.cpp         |  3 +++
 src/frontends/lean/pp.h           |  1 +
 src/frontends/lean/pp_options.cpp | 11 +++++++++++
 src/frontends/lean/pp_options.h   |  1 +
 4 files changed, 16 insertions(+)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index c40a53438..07da5e544 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -148,6 +148,8 @@ name pretty_fn::mk_metavar_name(name const & m) {
 }
 
 name pretty_fn::mk_local_name(name const & n, name const & suggested) {
+    if (!m_purify_locals)
+        return suggested;
     if (auto it = m_purify_local_table.find(n))
         return *it;
     unsigned i = 1;
@@ -212,6 +214,7 @@ void pretty_fn::set_options_core(options const & o) {
     m_private_names   = get_pp_private_names(o);
     m_metavar_args    = get_pp_metavar_args(o);
     m_purify_metavars = get_pp_purify_metavars(o);
+    m_purify_locals   = get_pp_purify_locals(o);
     m_beta            = get_pp_beta(o);
 }
 
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index 0441cbe5a..a87721ca4 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -62,6 +62,7 @@ private:
     bool                m_private_names;
     bool                m_metavar_args;
     bool                m_purify_metavars;
+    bool                m_purify_locals;
     bool                m_beta;
 
     name mk_metavar_name(name const & m);
diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp
index 3d722c44f..130aa0070 100644
--- a/src/frontends/lean/pp_options.cpp
+++ b/src/frontends/lean/pp_options.cpp
@@ -47,6 +47,10 @@ Author: Leonardo de Moura
 #define LEAN_DEFAULT_PP_PURIFY_METAVARS true
 #endif
 
+#ifndef LEAN_DEFAULT_PP_PURIFY_LOCALS
+#define LEAN_DEFAULT_PP_PURIFY_LOCALS true
+#endif
+
 #ifndef LEAN_DEFAULT_PP_BETA
 #define LEAN_DEFAULT_PP_BETA false
 #endif
@@ -62,6 +66,7 @@ static name * g_pp_full_names      = nullptr;
 static name * g_pp_private_names   = nullptr;
 static name * g_pp_metavar_args    = nullptr;
 static name * g_pp_purify_metavars = nullptr;
+static name * g_pp_purify_locals   = nullptr;
 static name * g_pp_beta            = nullptr;
 static list<options> * g_distinguishing_pp_options = nullptr;
 
@@ -76,6 +81,7 @@ void initialize_pp_options() {
     g_pp_private_names   = new name{"pp", "private_names"};
     g_pp_metavar_args    = new name{"pp", "metavar_args"};
     g_pp_purify_metavars = new name{"pp", "purify_metavars"};
+    g_pp_purify_locals   = new name{"pp", "purify_locals"};
     g_pp_beta            = new name{"pp", "beta"};
     register_unsigned_option(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH,
                              "(pretty printer) maximum expression depth, after that it will use ellipsis");
@@ -98,6 +104,9 @@ void initialize_pp_options() {
     register_bool_option(*g_pp_purify_metavars, LEAN_DEFAULT_PP_PURIFY_METAVARS,
                          "(pretty printer) rename internal metavariable names (with \"user-friendly\" ones) "
                          "before pretty printing");
+    register_bool_option(*g_pp_purify_locals, LEAN_DEFAULT_PP_PURIFY_LOCALS,
+                         "(pretty printer) rename local names to avoid name capture, "
+                         "before pretty printing");
     register_bool_option(*g_pp_beta,  LEAN_DEFAULT_PP_BETA,
                          "(pretty printer) apply beta-reduction when pretty printing");
 
@@ -124,6 +133,7 @@ void finalize_pp_options() {
     delete g_pp_private_names;
     delete g_pp_metavar_args;
     delete g_pp_purify_metavars;
+    delete g_pp_purify_locals;
     delete g_pp_beta;
     delete g_distinguishing_pp_options;
 }
@@ -146,6 +156,7 @@ bool     get_pp_full_names(options const & opts)      { return opts.get_bool(*g_
 bool     get_pp_private_names(options const & opts)   { return opts.get_bool(*g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); }
 bool     get_pp_metavar_args(options const & opts)    { return opts.get_bool(*g_pp_metavar_args, LEAN_DEFAULT_PP_METAVAR_ARGS); }
 bool     get_pp_purify_metavars(options const & opts) { return opts.get_bool(*g_pp_purify_metavars, LEAN_DEFAULT_PP_PURIFY_METAVARS); }
+bool     get_pp_purify_locals(options const & opts)   { return opts.get_bool(*g_pp_purify_locals, LEAN_DEFAULT_PP_PURIFY_LOCALS); }
 bool     get_pp_beta(options const & opts)            { return opts.get_bool(*g_pp_beta, LEAN_DEFAULT_PP_BETA); }
 list<options> const & get_distinguishing_pp_options() { return *g_distinguishing_pp_options; }
 }
diff --git a/src/frontends/lean/pp_options.h b/src/frontends/lean/pp_options.h
index 5c46c0d06..4287cae64 100644
--- a/src/frontends/lean/pp_options.h
+++ b/src/frontends/lean/pp_options.h
@@ -26,6 +26,7 @@ bool     get_pp_private_names(options const & opts);
 bool     get_pp_metavar_args(options const & opts);
 bool     get_pp_beta(options const & opts);
 bool     get_pp_purify_metavars(options const & opts);
+bool     get_pp_purify_locals(options const & opts);
 list<options> const & get_distinguishing_pp_options();
 
 void initialize_pp_options();