From 4ae0c4c4456e5490be342ca1ada3777e217f0153 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Jul 2013 00:34:44 -0700 Subject: [PATCH] Remove dead code Signed-off-by: Leonardo de Moura --- src/kernel/var_changer.cpp | 141 ------------------------------------- src/kernel/var_changer.h | 49 ------------- 2 files changed, 190 deletions(-) delete mode 100644 src/kernel/var_changer.cpp delete mode 100644 src/kernel/var_changer.h diff --git a/src/kernel/var_changer.cpp b/src/kernel/var_changer.cpp deleted file mode 100644 index 297e4cd62..000000000 --- a/src/kernel/var_changer.cpp +++ /dev/null @@ -1,141 +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 -#include -#include "var_changer.h" -#include "free_vars.h" -#include "maps.h" - -namespace lean { - -template -class var_changer_proc { - expr_cell_offset_map m_cache; - FV m_fv; - FS m_fs; -public: - var_changer_proc(FV const & fv, FS const & fs): - m_fv(fv), - m_fs(fs) { - } - - expr apply(expr const & e, unsigned offset) { - if (is_shared(e)) { - expr_cell_offset p(e.raw(), offset); - auto it = m_cache.find(p); - if (it != m_cache.end()) - return it->second; - } - - expr r = m_fs(e, offset); - if (eqp(e, r)) { - switch (e.kind()) { - case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Constant: - break; - case expr_kind::Var: - r = m_fv(e, offset); - break; - case expr_kind::App: { - std::vector new_args; - bool modified = false; - for (expr const & a : args(e)) { - new_args.push_back(apply(a, offset)); - if (!eqp(a, new_args.back())) - modified = true; - } - if (modified) - r = app(new_args.size(), new_args.data()); - else - r = e; - break; - } - case expr_kind::Lambda: - case expr_kind::Pi: { - expr const & old_t = abst_type(e); - expr const & old_b = abst_body(e); - expr t = apply(old_t, offset); - expr b = apply(old_b, offset+1); - if (!eqp(t, old_t) || !eqp(b, old_b)) { - name const & n = abst_name(e); - r = is_pi(e) ? pi(n, t, b) : lambda(n, t, b); - } - else { - r = e; - } - break; - }} - } - - if (is_shared(e)) - m_cache.insert(std::make_pair(expr_cell_offset(e.raw(), offset), r)); - - return r; - } -}; - -expr abstract(unsigned n, expr const * s, expr const & e) { - lean_assert(std::all_of(s, s+n, closed)); - - auto fv = [](expr const & x, unsigned offset) { return x; }; - - auto fs = [=](expr const & e, unsigned offset) { - unsigned i = n; - while (i > 0) { - --i; - if (s[i] == e) - return var(offset + n - i - 1); - } - return e; - }; - - var_changer_proc proc(fv, fs); - return proc.apply(e, 0); -} - -expr abstract_p(unsigned n, expr const * s, expr const & e) { - lean_assert(std::all_of(s, s+n, closed)); - - auto fv = [](expr const & x, unsigned offset) { return x; }; - - auto fs = [=](expr const & e, unsigned offset) { - unsigned i = n; - while (i > 0) { - --i; - if (eqp(s[i], e)) - return var(offset + n - i - 1); - } - return e; - }; - - var_changer_proc proc(fv, fs); - return proc.apply(e, 0); -} - -expr instantiate(unsigned n, expr const * s, expr const & e) { - lean_assert(std::all_of(s, s+n, closed)); - - auto fv = [=](expr const & x, unsigned offset) { - lean_assert(is_var(x)); - unsigned vidx = var_idx(x); - if (vidx >= offset) { - if (vidx < offset + n) - return s[n - (vidx - offset) - 1]; - else - return var(vidx - n); - } - else { - return x; - } - }; - - auto fs = [](expr const & c, unsigned offset) { return c; }; - - var_changer_proc proc(fv, fs); - return proc.apply(e, 0); -} - -} diff --git a/src/kernel/var_changer.h b/src/kernel/var_changer.h deleted file mode 100644 index c86b38179..000000000 --- a/src/kernel/var_changer.h +++ /dev/null @@ -1,49 +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 -*/ -#pragma once -#include "expr.h" - -namespace lean { - -/** - \brief Replace the expressions s[0], ..., s[n-1] in e with var(n-1), ..., var(0). - - Structural equality is used to compare subexpressions of e with the s[i]'s. - - \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables). -*/ -expr abstract(unsigned n, expr const * s, expr const & e); -inline expr abstract(expr const & s, expr const & e) { return abstract(1, &s, e); } - -/** - \brief Replace the expressions s[0], ..., s[n-1] in e with var(n-1), ..., var(0). - - Pointer comparison is used to compare subexpressions of e with the s[i]'s. - - \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables). -*/ -expr abstract_p(unsigned n, expr const * s, expr const & e); -inline expr abstract_p(expr const & s, expr const & e) { return abstract_p(1, &s, e); } - -/** - \brief Replace the free variables with indices 0,...,n-1 with s[n-1],...,s[0] in e. - - \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables). -*/ -expr instantiate(unsigned n, expr const * s, expr const & e); -inline expr instantiate(expr const & s, expr const & e) { return instantiate(1, &s, e); } - -/** - \brief Substitute s with t in e. - - \pre s and t must be closed expressions (i.e., no free variables) -*/ -inline expr substitute(expr const & s, expr const & t, expr const & e) { - return instantiate(t, abstract(s, e)); -} - -}