chore(library/rewriter): remove lean-0.1 files
This commit is contained in:
Soonho Kong
parent
5ff200c516
commit
0f5d88517d
5 changed files with 0 additions and 1719 deletions
|
|
@ -1,2 +0,0 @@
|
|||
add_library(rewriter rewriter.cpp fo_match.cpp)
|
||||
target_link_libraries(rewriter ${LEAN_LIBS})
|
||||
|
|
@ -1,192 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Soonho Kong
|
||||
*/
|
||||
#include <utility>
|
||||
#include "util/trace.h"
|
||||
#include "kernel/expr.h"
|
||||
#include "library/printer.h"
|
||||
#include "library/arith/nat.h"
|
||||
#include "library/arith/arith.h"
|
||||
#include "library/rewriter/fo_match.h"
|
||||
#include "library/rewriter/rewriter.h"
|
||||
|
||||
using std::cout;
|
||||
using std::endl;
|
||||
|
||||
namespace lean {
|
||||
|
||||
bool fo_match::match_var(expr const & p, expr const & t, unsigned o, subst_map & s) {
|
||||
lean_trace("fo_match", tout << "match_var : (" << p << ", " << t << ", " << o << ", " << s << ")" << endl;); // LCOV_EXCL_LINE
|
||||
|
||||
unsigned idx = var_idx(p);
|
||||
if (idx < o) {
|
||||
// Current variable is the one created by lambda inside of pattern
|
||||
// and it is *not* a target of pattern matching.
|
||||
return p == t;
|
||||
} else {
|
||||
auto it = s.find(idx - o);
|
||||
if (it != s.end()) {
|
||||
// This variable already has an entry in the substitution
|
||||
// map. We need to make sure that 't' and s[idx] are the
|
||||
// same
|
||||
lean_trace("fo_match", tout << "match_var exist:" << idx - o << " |-> " << it->second << endl;); // LCOV_EXCL_LINE
|
||||
return it->second == t;
|
||||
}
|
||||
// This variable has no entry in the substituition map. Let's
|
||||
// add one.
|
||||
s.insert(idx - o, t);
|
||||
lean_trace("fo_match", tout << "match_var MATCHED : " << s << endl;); // LCOV_EXCL_LINE
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
bool fo_match::match_constant(expr const & p, expr const & t, unsigned, subst_map &) {
|
||||
lean_trace("fo_match", tout << "match_constant : (" << p << ", " << t << ")" << endl;); // LCOV_EXCL_LINE
|
||||
return p == t;
|
||||
}
|
||||
|
||||
bool fo_match::match_value(expr const & p, expr const & t, unsigned, subst_map &) {
|
||||
lean_trace("fo_match", tout << "match_value : (" << p << ", " << t << ")" << endl;); // LCOV_EXCL_LINE
|
||||
return p == t;
|
||||
}
|
||||
|
||||
bool fo_match::match_app(expr const & p, expr const & t, unsigned o, subst_map & s) {
|
||||
lean_trace("fo_match", tout << "match_app : (" << p << ", " << t << ", " << o << ", " << s << ")" << endl;); // LCOV_EXCL_LINE
|
||||
if (!is_app(t)) {
|
||||
lean_trace("fo_match", tout << "match_app : " << t << " is not app." << endl;); // LCOV_EXCL_LINE
|
||||
return false;
|
||||
}
|
||||
unsigned num_p = num_args(p);
|
||||
unsigned num_t = num_args(t);
|
||||
if (num_p != num_t) {
|
||||
lean_trace("fo_match", tout << "match_app : number of arguments does not match"
|
||||
<< "(" << num_p << " <> " << num_t << ")" << endl;); // LCOV_EXCL_LINE
|
||||
return false;
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < num_p; i++) {
|
||||
if (!match_main(arg(p, i), arg(t, i), o, s))
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool fo_match::match_lambda(expr const & p, expr const & t, unsigned o, subst_map & s) {
|
||||
lean_trace("fo_match", tout << "match_lambda : (" << p << ", " << t << ", " << o << ", " << s << ")" << endl;); // LCOV_EXCL_LINE
|
||||
lean_trace("fo_match", tout << "fun (" << abst_name(p) << " : " << abst_domain(p) << "), " << abst_body(p) << endl;); // LCOV_EXCL_LINE
|
||||
if (!is_lambda(t)) {
|
||||
return false;
|
||||
} else {
|
||||
// First match the domain part
|
||||
auto p_domain = abst_domain(p);
|
||||
auto t_domain = abst_domain(t);
|
||||
if (!match_main(p_domain, t_domain, o, s))
|
||||
return false;
|
||||
|
||||
// Then match the body part, increase offset by 1.
|
||||
auto p_body = abst_body(p);
|
||||
auto t_body = abst_body(t);
|
||||
return match_main(p_body, t_body, o + 1, s);
|
||||
}
|
||||
}
|
||||
|
||||
bool fo_match::match_pi(expr const & p, expr const & t, unsigned o, subst_map & s) {
|
||||
lean_trace("fo_match", tout << "match_pi : (" << p << ", " << t << ", " << o << ", " << s << ")" << endl;); // LCOV_EXCL_LINE
|
||||
lean_trace("fo_match", tout << "Pi (" << abst_name(p) << " : " << abst_domain(p) << "), " << abst_body(p) << endl;); // LCOV_EXCL_LINE
|
||||
if (!is_pi(t)) {
|
||||
return false;
|
||||
} else {
|
||||
// First match the domain part
|
||||
auto p_domain = abst_domain(p);
|
||||
auto t_domain = abst_domain(t);
|
||||
if (!match_main(p_domain, t_domain, o, s))
|
||||
return false;
|
||||
|
||||
// Then match the body part, increase offset by 1.
|
||||
auto p_body = abst_body(p);
|
||||
auto t_body = abst_body(t);
|
||||
return match_main(p_body, t_body, o + 1, s);
|
||||
}
|
||||
}
|
||||
|
||||
bool fo_match::match_type(expr const & p, expr const & t, unsigned, subst_map &) {
|
||||
lean_trace("fo_match", tout << "match_type : (" << p << ", " << t << ")" << endl;); // LCOV_EXCL_LINE
|
||||
return p == t;
|
||||
}
|
||||
|
||||
bool fo_match::match_let(expr const & p, expr const & t, unsigned o, subst_map & s) {
|
||||
lean_trace("fo_match", tout << "match_let : (" << p << ", " << t << ", " << o << ", " << s << ")" << endl;); // LCOV_EXCL_LINE
|
||||
if (!is_let(t)) {
|
||||
return false;
|
||||
} else {
|
||||
// First match the type part
|
||||
auto p_type = let_type(p);
|
||||
auto t_type = let_type(t);
|
||||
if (!match_main(p_type, t_type, o, s))
|
||||
return false;
|
||||
|
||||
// then match the value part
|
||||
auto p_value = let_value(p);
|
||||
auto t_value = let_value(t);
|
||||
if (!match_main(p_value, t_value, o, s))
|
||||
return false;
|
||||
|
||||
// then match the value part
|
||||
auto p_body = let_body(p);
|
||||
auto t_body = let_body(t);
|
||||
return match_main(p_body, t_body, o + 1, s);
|
||||
}
|
||||
}
|
||||
bool fo_match::match_metavar(expr const & p, expr const & t, unsigned, subst_map &) {
|
||||
lean_trace("fo_match", tout << "match_meta : (" << p << ", " << t << ")" << endl;); // LCOV_EXCL_LINE
|
||||
return p == t;
|
||||
}
|
||||
|
||||
bool fo_match::match_main(optional<expr> const & p, optional<expr> const & t, unsigned o, subst_map & s) {
|
||||
if (p && t)
|
||||
return match_main(*p, *t, o, s);
|
||||
else
|
||||
return !p && !t;
|
||||
}
|
||||
|
||||
bool fo_match::match_main(expr const & p, expr const & t, unsigned o, subst_map & s) {
|
||||
lean_trace("fo_match", tout << "match : (" << p << ", " << t << ", " << o << ", " << s << ")" << endl;); // LCOV_EXCL_LINE
|
||||
switch (p.kind()) {
|
||||
case expr_kind::Var:
|
||||
return match_var(p, t, o, s);
|
||||
case expr_kind::Constant:
|
||||
return match_constant(p, t, o, s);
|
||||
case expr_kind::Value:
|
||||
return match_value(p, t, o, s);
|
||||
case expr_kind::App:
|
||||
return match_app(p, t, o, s);
|
||||
case expr_kind::Lambda:
|
||||
return match_lambda(p, t, o, s);
|
||||
case expr_kind::Pi:
|
||||
return match_pi(p, t, o, s);
|
||||
case expr_kind::Type:
|
||||
return match_type(p, t, o, s);
|
||||
case expr_kind::Let:
|
||||
return match_let(p, t, o, s);
|
||||
case expr_kind::MetaVar:
|
||||
return match_metavar(p, t, o, s);
|
||||
case expr_kind::Proj: case expr_kind::Pair: case expr_kind::Sigma: case expr_kind::HEq:
|
||||
// TODO(Leo):
|
||||
break;
|
||||
}
|
||||
lean_unreachable(); // LCOV_EXCL_LINE
|
||||
}
|
||||
|
||||
bool fo_match::match(expr const & p, expr const & t, unsigned o, subst_map & s) {
|
||||
s.push();
|
||||
if (match_main(p, t, o, s)) {
|
||||
return true;
|
||||
} else {
|
||||
s.pop();
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1,33 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Soonho Kong
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/scoped_map.h"
|
||||
#include "kernel/expr.h"
|
||||
#include "kernel/context.h"
|
||||
#include "library/printer.h"
|
||||
|
||||
namespace lean {
|
||||
using subst_map = scoped_map<unsigned, expr>;
|
||||
|
||||
class fo_match {
|
||||
private:
|
||||
bool match_var(expr const & p, expr const & t, unsigned o, subst_map & s);
|
||||
bool match_constant(expr const & p, expr const & t, unsigned o, subst_map & s);
|
||||
bool match_value(expr const & p, expr const & t, unsigned o, subst_map & s);
|
||||
bool match_app(expr const & p, expr const & t, unsigned o, subst_map & s);
|
||||
bool match_lambda(expr const & p, expr const & t, unsigned o, subst_map & s);
|
||||
bool match_pi(expr const & p, expr const & t, unsigned o, subst_map & s);
|
||||
bool match_type(expr const & p, expr const & t, unsigned o, subst_map & s);
|
||||
bool match_let(expr const & p, expr const & t, unsigned o, subst_map & s);
|
||||
bool match_metavar(expr const & p, expr const & t, unsigned o, subst_map & s);
|
||||
bool match_main(expr const & p, expr const & t, unsigned o, subst_map & s);
|
||||
bool match_main(optional<expr> const & p, optional<expr> const & t, unsigned o, subst_map & s);
|
||||
|
||||
public:
|
||||
bool match(expr const & p, expr const & t, unsigned o, subst_map & s);
|
||||
};
|
||||
}
|
||||
|
|
@ -1,968 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation.
|
||||
Copyright (c) 2013 Carnegie Mellon University.
|
||||
All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Soonho Kong
|
||||
*/
|
||||
#include "kernel/abstract.h"
|
||||
#include "kernel/kernel.h"
|
||||
#include "kernel/context.h"
|
||||
#include "kernel/environment.h"
|
||||
#include "kernel/expr.h"
|
||||
#include "kernel/replace_fn.h"
|
||||
#include "kernel/type_checker.h"
|
||||
#include "library/printer.h"
|
||||
#include "library/rewriter/fo_match.h"
|
||||
#include "library/rewriter/rewriter.h"
|
||||
#include "util/buffer.h"
|
||||
#include "util/trace.h"
|
||||
|
||||
using std::cout;
|
||||
using std::endl;
|
||||
using std::initializer_list;
|
||||
using std::make_pair;
|
||||
using std::ostream;
|
||||
|
||||
namespace lean {
|
||||
|
||||
/**
|
||||
\brief For a lambda term v = \f$(\lambda n : ty. body)\f$ and the rewriting result
|
||||
for ty, it constructs a new rewriting result for v' = \f$(\lambda n : ty'.
|
||||
body)\f$ with the proof of v = v'.
|
||||
|
||||
\param env environment
|
||||
\param ctx context
|
||||
\param v \f$(\lambda n : ty. body)\f$
|
||||
\param result_ty rewriting result of ty -- pair of ty'
|
||||
rewritten type of ty and pf_ty the proof of (ty = ty')
|
||||
\return pair of v' = \f$(\lambda n : ty'. body)\f$, and proof of v = v'
|
||||
*/
|
||||
pair<expr, expr> rewrite_lambda_type(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_ty) {
|
||||
lean_assert(is_lambda(v));
|
||||
type_inferer ti(env);
|
||||
expr const & ty = abst_domain(v);
|
||||
expr const & new_ty = result_ty.first;
|
||||
expr const & ty_v = ti(v, ctx);
|
||||
if (ty == new_ty) {
|
||||
return make_pair(v, mk_refl_th(ty_v, v));
|
||||
} else {
|
||||
name const & n = abst_name(v);
|
||||
expr const & body = abst_body(v);
|
||||
// expr const & pf_ty = result_ty.second;
|
||||
expr const & new_v = mk_lambda(n, new_ty, body);
|
||||
// expr const & ty_ty = ti(ty, ctx);
|
||||
// lean_assert_eq(ty_ty, ti(new_ty, ctx)); // TODO(soonhok): generalize for hetreogeneous types
|
||||
expr proof;
|
||||
#if 0 // TODO(Leo): we don't have heterogeneous equality anymore
|
||||
= mk_subst_th(ty_ty, ty, new_ty,
|
||||
Fun({Const("T"), ty_ty},
|
||||
mk_heq(v, mk_lambda(n, Const("T"), body))),
|
||||
mk_refl_th(ty_v, v), pf_ty);
|
||||
#endif
|
||||
return make_pair(new_v, proof);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief For a lambda term v = \f$(\lambda n : ty. body)\f$ and the rewriting result
|
||||
for body, it constructs a new rewriting result for v' = \f$(\lambda n : ty.
|
||||
body')\f$ with the proof of v = v'.
|
||||
|
||||
\param env environment
|
||||
\param ctx context
|
||||
\param v \f$(\lambda n : ty. body)\f$
|
||||
\param result_body rewriting result of body -- pair of \c body'
|
||||
rewritten term of body and \c pf_body the proof of (body =
|
||||
body')
|
||||
\return pair of v' = \f$(\lambda n : ty. body')\f$, and proof of v = v'
|
||||
*/
|
||||
pair<expr, expr> rewrite_lambda_body(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_body) {
|
||||
lean_assert(is_lambda(v));
|
||||
type_inferer ti(env);
|
||||
expr const & body = abst_body(v);
|
||||
expr const & new_body = result_body.first;
|
||||
expr const & ty_v = ti(v, ctx);
|
||||
if (body == new_body) {
|
||||
return make_pair(v, mk_refl_th(ty_v, v));
|
||||
} else {
|
||||
name const & n = abst_name(v);
|
||||
expr const & ty = abst_domain(v);
|
||||
expr const & pf_body = result_body.second;
|
||||
expr const & new_v = mk_lambda(n, ty, new_body);
|
||||
expr const & ty_body = ti(body, extend(ctx, n, ty));
|
||||
lean_assert_eq(ty_body, ti(new_body, ctx)); // TODO(soonhok): generalize for hetreogeneous types
|
||||
expr const & proof = mk_funext_th(ty, mk_lambda(n, ty, ty_body), v, new_v, mk_lambda(n, ty, pf_body));
|
||||
return make_pair(new_v, proof);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief For a lambda term v = \f$(\lambda n : ty. body)\f$ and the rewriting
|
||||
result for ty and body, it constructs a new rewriting result for v'
|
||||
= \f$(\lambda n : ty'. body')\f$ with the proof of v = v'.
|
||||
|
||||
\param env environment
|
||||
\param ctx context
|
||||
\param v \f$(\lambda n : ty. body)\f$
|
||||
\param result_ty rewriting result of ty -- pair of ty'
|
||||
rewritten type of ty and pf_ty the proof of (ty = ty')
|
||||
\param result_body rewriting result of body -- pair of body'
|
||||
rewritten term of body and \c pf_body the proof of (body =
|
||||
body')
|
||||
\return pair of v' = \f$(\lambda n : ty'. body')\f$, and proof of v = v'
|
||||
*/
|
||||
pair<expr, expr> rewrite_lambda(environment const & env, context & /* ctx */, expr const & v, pair<expr, expr> const & result_ty, pair<expr, expr> const & result_body) {
|
||||
lean_assert(is_lambda(v));
|
||||
type_inferer ti(env);
|
||||
name const & n = abst_name(v);
|
||||
// expr const & ty = abst_domain(v);
|
||||
// expr const & body = abst_body(v);
|
||||
expr const & new_ty = result_ty.first;
|
||||
// expr const & pf_ty = result_ty.second;
|
||||
expr const & new_body = result_body.first;
|
||||
// expr const & pf_body = result_body.second;
|
||||
// expr const & ty_ty = ti(ty, ctx);
|
||||
// expr const & ty_body = ti(body, ctx);
|
||||
// expr const & ty_v = ti(v, ctx);
|
||||
// expr const & new_v1 = mk_lambda(n, new_ty, body);
|
||||
// expr const & ty_new_v1 = ti(v, ctx);
|
||||
expr const & new_v2 = mk_lambda(n, new_ty, new_body);
|
||||
// proof1 : v = new_v1
|
||||
|
||||
expr proof;
|
||||
#if 0 // TODO(Leo): we don't have heterogeneous equality anymore
|
||||
expr proof1 = mk_subst_th(ty_ty, ty, new_ty,
|
||||
Fun({Const("T"), ty_ty},
|
||||
mk_heq(v, mk_lambda(n, Const("T"), body))),
|
||||
mk_refl_th(ty_v, v),
|
||||
pf_ty);
|
||||
expr proof2 = mk_subst_th(ty_body, body, new_body,
|
||||
Fun({Const("e"), ty_body},
|
||||
mk_heq(new_v1, mk_lambda(n, new_ty, Const("e")))),
|
||||
mk_refl_th(ty_new_v1, new_v1),
|
||||
pf_body);
|
||||
expr const & proof = mk_trans_th(ty_v, v, new_v1, new_v2, proof1, proof2);
|
||||
#endif
|
||||
return make_pair(new_v2, proof);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief For a Pi term v = \f$(\Pi n : ty. body)\f$ and the rewriting
|
||||
result for ty, it constructs a new rewriting result for v'
|
||||
= \f$(\Pi n : ty'. body)\f$ with the proof of v = v'.
|
||||
|
||||
\param env environment
|
||||
\param ctx context
|
||||
\param v \f$(\Pi n : ty. body)\f$
|
||||
\param result_ty rewriting result of ty -- pair of ty'
|
||||
rewritten type of ty and pf_ty the proof of (ty = ty')
|
||||
\return pair of v' = \f$(\Pi n : ty'. body)\f$, and proof of v = v'
|
||||
*/
|
||||
pair<expr, expr> rewrite_pi_type(environment const & env, context & /* ctx */, expr const & v, pair<expr, expr> const & result_ty) {
|
||||
lean_assert(is_pi(v));
|
||||
type_inferer ti(env);
|
||||
name const & n = abst_name(v);
|
||||
// expr const & ty = abst_domain(v);
|
||||
expr const & body = abst_body(v);
|
||||
expr const & new_ty = result_ty.first;
|
||||
// expr const & pf = result_ty.second;
|
||||
expr const & new_v = mk_pi(n, new_ty, body);
|
||||
// expr const & ty_ty = ti(ty, ctx);
|
||||
// expr const & ty_v = ti(v, ctx);
|
||||
expr proof;
|
||||
#if 0 // TODO(Leo): HEq is gone
|
||||
= mk_subst_th(ty_ty, ty, new_ty,
|
||||
Fun({Const("T"), ty_ty},
|
||||
mk_heq(v, mk_pi(n, Const("T"), body))),
|
||||
mk_refl_th(ty_v, v),
|
||||
pf);
|
||||
#endif
|
||||
return make_pair(new_v, proof);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief For a Pi term v = \f$(\Pi n : ty. body)\f$ and the rewriting
|
||||
result for body, it constructs a new rewriting result for v'
|
||||
= \f$(\Pi n : ty. body')\f$ with the proof of v = v'.
|
||||
|
||||
\param env environment
|
||||
\param ctx context
|
||||
\param v \f$(\Pi n : ty. body)\f$
|
||||
\param result_body rewriting result of body -- pair of body'
|
||||
rewritten term of body and \c pf_body the proof of (body =
|
||||
body')
|
||||
\return pair of v' = \f$(\Pi n : ty. body')\f$, and proof of v = v'
|
||||
*/
|
||||
pair<expr, expr> rewrite_pi_body(environment const & env, context & /* ctx */, expr const & v, pair<expr, expr> const & result_body) {
|
||||
lean_assert(is_pi(v));
|
||||
type_inferer ti(env);
|
||||
name const & n = abst_name(v);
|
||||
expr const & ty = abst_domain(v);
|
||||
// expr const & body = abst_body(v);
|
||||
expr const & new_body = result_body.first;
|
||||
// expr const & pf = result_body.second;
|
||||
expr const & new_v = mk_pi(n, ty, new_body);
|
||||
// expr const & ty_body = ti(body, extend(ctx, n, ty));
|
||||
// expr const & ty_v = ti(v, ctx);
|
||||
expr proof;
|
||||
#if 0 // TODO(Leo): HEq is gone
|
||||
expr const & proof = mk_subst_th(ty_body, body, new_body,
|
||||
Fun({Const("e"), ty_body},
|
||||
mk_heq(v, mk_pi(n, ty, Const("e")))),
|
||||
mk_refl_th(ty_v, v),
|
||||
pf);
|
||||
#endif
|
||||
return make_pair(new_v, proof);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief For a Pi term v = \f$(\Pi n : ty. body)\f$ and the rewriting
|
||||
result for ty and body, it constructs a new rewriting result for v'
|
||||
= \f$(\Pi n : ty'. body')\f$ with the proof of v = v'.
|
||||
|
||||
\param env environment
|
||||
\param ctx context
|
||||
\param v \f$(\Pi n : ty. body)\f$
|
||||
\param result_ty rewriting result of ty -- pair of ty'
|
||||
rewritten type of ty and pf_ty the proof of (ty = ty')
|
||||
\param result_body rewriting result of body -- pair of body'
|
||||
rewritten term of body and \c pf_body the proof of (body =
|
||||
body')
|
||||
\return pair of v' = \f$(\Pi n : ty'. body')\f$, and proof of v = v'
|
||||
*/
|
||||
pair<expr, expr> rewrite_pi(environment const & env, context & /*ctx*/, expr const & v, pair<expr, expr> const & result_ty, pair<expr, expr> const & result_body) {
|
||||
lean_assert(is_pi(v));
|
||||
type_inferer ti(env);
|
||||
name const & n = abst_name(v);
|
||||
// expr const & ty = abst_domain(v);
|
||||
// expr const & body = abst_body(v);
|
||||
expr const & new_ty = result_ty.first;
|
||||
// expr const & pf_ty = result_ty.second;
|
||||
expr const & new_body = result_body.first;
|
||||
// expr const & pf_body = result_body.second;
|
||||
// expr const & ty_ty = ti(ty, ctx);
|
||||
// expr const & ty_body = ti(body, ctx);
|
||||
// expr const & ty_v = ti(v, ctx);
|
||||
// expr const & new_v1 = mk_pi(n, new_ty, body);
|
||||
// expr const & ty_new_v1 = ti(v, ctx);
|
||||
expr const & new_v2 = mk_pi(n, new_ty, new_body);
|
||||
expr proof;
|
||||
#if 0 // TODO(Leo): HEq is gone
|
||||
expr const & proof1 = mk_subst_th(ty_ty, ty, new_ty,
|
||||
Fun({Const("T"), ty_ty},
|
||||
mk_heq(v, mk_pi(n, Const("T"), body))),
|
||||
mk_refl_th(ty_v, v),
|
||||
pf_ty);
|
||||
expr const & proof2 = mk_subst_th(ty_body, body, new_body,
|
||||
Fun({Const("e"), ty_body},
|
||||
mk_heq(new_v1, mk_pi(n, new_ty, Const("e")))),
|
||||
mk_refl_th(ty_new_v1, new_v1),
|
||||
pf_body);
|
||||
expr const & proof = mk_trans_th(ty_v, v, new_v1, new_v2, proof1, proof2);
|
||||
#endif
|
||||
return make_pair(new_v2, proof);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief For a lambda term v = (let n : ty = val in body) and the rewriting result
|
||||
for ty, it constructs a new rewriting result for v' = (let n : ty'
|
||||
= val in body) with the proof of v = v'.
|
||||
|
||||
\param env environment
|
||||
\param ctx context
|
||||
\param v (let n : ty = val in body)
|
||||
\param result_ty rewriting result of ty -- pair of ty'
|
||||
rewritten type of ty and \c pf_ty the proof of (ty = ty')
|
||||
\return pair of v' = (let n : ty' = val in body), and proof of v = v'
|
||||
*/
|
||||
pair<expr, expr> rewrite_let_type(environment const & env, context & /* ctx */, expr const & v, pair<expr, expr> const & result_ty) {
|
||||
lean_assert(is_let(v));
|
||||
type_inferer ti(env);
|
||||
if (!let_type(v)) {
|
||||
name const & n = let_name(v);
|
||||
// expr const & ty = *let_type(v);
|
||||
expr const & val = let_value(v);
|
||||
expr const & body = let_body(v);
|
||||
expr const & new_ty = result_ty.first;
|
||||
// expr const & pf = result_ty.second;
|
||||
expr const & new_v = mk_let(n, new_ty, val, body);
|
||||
// expr const & ty_ty = ti(ty, ctx);
|
||||
// expr const & ty_v = ti(v, ctx);
|
||||
expr proof;
|
||||
#if 0 // TODO(Leo): HEq is gone
|
||||
expr const & proof = mk_subst_th(ty_ty, ty, new_ty,
|
||||
Fun({Const("x"), ty_ty},
|
||||
mk_heq(v, mk_let(n, Const("x"), val, body))),
|
||||
mk_refl_th(ty_v, v),
|
||||
pf);
|
||||
#endif
|
||||
return make_pair(new_v, proof);
|
||||
} else {
|
||||
throw rewriter_exception();
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief For a lambda term v = (let n : ty = val in body) and the rewriting result
|
||||
for val, it constructs a new rewriting result for v' = (let n : ty
|
||||
= val' in body) with the proof of v = v'.
|
||||
|
||||
\param env environment
|
||||
\param ctx context
|
||||
\param v (let n : ty = val in body)
|
||||
\param result_value rewriting result of val -- pair of val'
|
||||
rewritten term of val and \c pf_val the proof of (val = val')
|
||||
\return pair of v' = (let n : ty = val' in body), and proof of v = v'
|
||||
*/
|
||||
pair<expr, expr> rewrite_let_value(environment const & env, context & /* ctx */, expr const & v, pair<expr, expr> const & result_value) {
|
||||
lean_assert(is_let(v));
|
||||
type_inferer ti(env);
|
||||
name const & n = let_name(v);
|
||||
optional<expr> const & ty = let_type(v);
|
||||
// expr const & val = let_value(v);
|
||||
expr const & body = let_body(v);
|
||||
expr const & new_val = result_value.first;
|
||||
// expr const & pf = result_value.second;
|
||||
expr const & new_v = mk_let(n, ty, new_val, body);
|
||||
// expr const & ty_val = ti(val, ctx);
|
||||
// expr const & ty_v = ti(v, ctx);
|
||||
expr proof;
|
||||
#if 0 // TODO(Leo): HEq is gone
|
||||
expr const & proof = mk_subst_th(ty_val, val, new_val,
|
||||
Fun({Const("x"), ty_val},
|
||||
mk_heq(v, mk_let(n, ty, Const("x"), body))),
|
||||
mk_refl_th(ty_v, v),
|
||||
pf);
|
||||
#endif
|
||||
return make_pair(new_v, proof);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief For a lambda term v = (let n : ty = val in body) and the rewriting result
|
||||
for body, it constructs a new rewriting result for v' = (let n : ty
|
||||
= val in body') with the proof of v = v'.
|
||||
|
||||
\param env environment
|
||||
\param ctx context
|
||||
\param v (let n : ty = val in body)
|
||||
\param result_body rewriting result of body -- pair of \c body'
|
||||
rewritten term of body and \c pf_body the proof of (body =
|
||||
body')
|
||||
\return pair of v' = (let n : ty = val in body'), and proof of v = v'
|
||||
*/
|
||||
pair<expr, expr> rewrite_let_body(environment const & env, context & /* ctx */, expr const & v, pair<expr, expr> const & result_body) {
|
||||
lean_assert(is_let(v));
|
||||
type_inferer ti(env);
|
||||
name const & n = let_name(v);
|
||||
optional<expr> const & ty = let_type(v);
|
||||
expr const & val = let_value(v);
|
||||
// expr const & body = let_body(v);
|
||||
expr const & new_body = result_body.first;
|
||||
// expr const & pf = result_body.second;
|
||||
expr const & new_v = mk_let(n, ty, val, new_body);
|
||||
// expr const & ty_body = ti(body, extend(ctx, n, ty, body));
|
||||
// expr const & ty_v = ti(v, ctx);
|
||||
expr proof;
|
||||
#if 0 // TODO(Leo): HEq is gone
|
||||
expr const & proof = mk_subst_th(ty_body, body, new_body,
|
||||
Fun({Const("e"), ty_body},
|
||||
mk_heq(v, mk_let(n, ty, val, Const("e")))),
|
||||
mk_refl_th(ty_v, v),
|
||||
pf);
|
||||
#endif
|
||||
return make_pair(new_v, proof);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief For a lambda term v = (e_0 e_1 ... e_n) and the rewriting results
|
||||
for each e_i, it constructs a new rewriting result for v' = (e'_0
|
||||
e'_1 ... e'_n) with the proof of v = v'.
|
||||
|
||||
\param env environment
|
||||
\param ctx context
|
||||
\param v (e_0 e_1 ... e_n)
|
||||
\param results rewriting result foe each e_i -- pair of e'_i
|
||||
rewritten term of e_i and \c pf_e_i the proof of (e_i = e'_i)
|
||||
\return pair of v' = (e'_0 e'_1 ... e'_n), and proof of v = v'
|
||||
*/
|
||||
pair<expr, expr> rewrite_app(environment const & env, context & ctx, expr const & v, buffer<pair<expr, expr>> const & results ) {
|
||||
type_inferer ti(env);
|
||||
expr f = arg(v, 0);
|
||||
expr new_f = results[0].first;
|
||||
expr pf = results[0].second;
|
||||
for (unsigned i = 1; i < results.size(); i++) {
|
||||
expr const & f_ty = ti(f, ctx);
|
||||
lean_assert(is_pi(f_ty));
|
||||
expr const & f_ty_domain = abst_domain(f_ty); // A
|
||||
expr f_ty_body = mk_lambda(abst_name(f_ty), f_ty_domain, abst_body(f_ty)); // B
|
||||
expr const & e_i = arg(v, i);
|
||||
expr const & new_e_i = results[i].first;
|
||||
expr const & pf_e_i = results[i].second;
|
||||
bool f_changed = f != new_f;
|
||||
if (f_changed) {
|
||||
if (arg(v, i) != results[i].first) {
|
||||
// congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi
|
||||
// (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f
|
||||
// a = g b
|
||||
pf = mk_congr_th(f_ty_domain, f_ty_body, f, new_f, e_i, new_e_i, pf, pf_e_i);
|
||||
} else {
|
||||
// congr1 : Pi (A : Type u) (B : A -> Type u) (f g: Pi
|
||||
// (x : A) B x) (a : A) (H : f = g), f a = g a
|
||||
pf = mk_congr1_th(f_ty_domain, f_ty_body, f, new_f, e_i, pf);
|
||||
}
|
||||
} else {
|
||||
if (arg(v, i) != results[i].first) {
|
||||
// congr2 : Pi (A : Type u) (B : A -> Type u) (a b : A) (f : Pi (x : A) B x) (H : a = b), f a = f b
|
||||
pf = mk_congr2_th(f_ty_domain, f_ty_body, e_i, new_e_i, f, pf_e_i);
|
||||
} else {
|
||||
// refl
|
||||
pf = mk_refl_th(ti(f(e_i), ctx), f(e_i));
|
||||
}
|
||||
}
|
||||
f = f (e_i);
|
||||
new_f = new_f (new_e_i);
|
||||
}
|
||||
return make_pair(new_f, pf);
|
||||
}
|
||||
|
||||
void rewriter_cell::dealloc() {
|
||||
delete this;
|
||||
}
|
||||
rewriter_cell::rewriter_cell(rewriter_kind k):m_kind(k), m_rc(1) { }
|
||||
rewriter_cell::~rewriter_cell() {
|
||||
}
|
||||
|
||||
// Theorem Rewriter
|
||||
theorem_rewriter_cell::theorem_rewriter_cell(expr const & type, expr const & body)
|
||||
: rewriter_cell(rewriter_kind::Theorem), m_type(type), m_body(body), m_num_args(0) {
|
||||
lean_trace("rewriter", tout << "Type = " << m_type << endl;);
|
||||
lean_trace("rewriter", tout << "Body = " << m_body << endl;);
|
||||
|
||||
// We expect the theorem is in the form of
|
||||
// Pi (x_1 : t_1 ... x_n : t_n), pattern = rhs
|
||||
m_pattern = m_type;
|
||||
while (is_pi(m_pattern)) {
|
||||
m_pattern = abst_body(m_pattern);
|
||||
m_num_args++;
|
||||
}
|
||||
#if 0 // HEq is gone
|
||||
if (!is_heq(m_pattern)) {
|
||||
lean_trace("rewriter", tout << "Theorem " << m_type << " is not in the form of "
|
||||
<< "Pi (x_1 : t_1 ... x_n : t_n), pattern = rhs" << endl;);
|
||||
}
|
||||
m_rhs = heq_rhs(m_pattern);
|
||||
m_pattern = heq_lhs(m_pattern);
|
||||
|
||||
lean_trace("rewriter", tout << "Number of Arg = " << m_num_args << endl;);
|
||||
#endif
|
||||
}
|
||||
theorem_rewriter_cell::~theorem_rewriter_cell() { }
|
||||
pair<expr, expr> theorem_rewriter_cell::operator()(environment const &, context &, expr const & v) const throw(rewriter_exception) {
|
||||
// lean_trace("rewriter", tout << "Context = " << ctx << endl;);
|
||||
lean_trace("rewriter", tout << "Term = " << v << endl;);
|
||||
lean_trace("rewriter", tout << "Pattern = " << m_pattern << endl;);
|
||||
lean_trace("rewriter", tout << "Num Args = " << m_num_args << endl;);
|
||||
|
||||
fo_match fm;
|
||||
subst_map s;
|
||||
if (!fm.match(m_pattern, v, 0, s)) {
|
||||
throw rewriter_exception();
|
||||
}
|
||||
lean_trace("rewriter", tout << "Subst = " << s << endl;);
|
||||
|
||||
// apply s to rhs
|
||||
auto f = [&s](expr const & e, unsigned offset) -> expr {
|
||||
if (!is_var(e)) {
|
||||
return e;
|
||||
}
|
||||
unsigned idx = var_idx(e);
|
||||
if (idx < offset) {
|
||||
return e;
|
||||
}
|
||||
|
||||
lean_trace("rewriter", tout << "Inside of apply : offset = " << offset
|
||||
<< ", e = " << e
|
||||
<< ", idx = " << var_idx(e) << endl;);
|
||||
auto it = s.find(idx);
|
||||
if (it != s.end()) {
|
||||
lean_trace("rewriter", tout << "Inside of apply : s[" << idx << "] = " << it->second << endl;);
|
||||
return it->second;
|
||||
}
|
||||
return e;
|
||||
};
|
||||
|
||||
expr new_rhs = replace_fn<decltype(f)>(f)(m_rhs);
|
||||
lean_trace("rewriter", tout << "New RHS = " << new_rhs << endl;);
|
||||
|
||||
expr proof = m_body;
|
||||
for (int i = m_num_args -1 ; i >= 0; i--) {
|
||||
auto it = s.find(i);
|
||||
lean_assert(it != s.end());
|
||||
proof = proof(it->second);
|
||||
lean_trace("rewriter", tout << "proof: " << i << "\t" << it->second << "\t" << proof << endl;);
|
||||
}
|
||||
lean_trace("rewriter", tout << "Proof = " << proof << endl;);
|
||||
return make_pair(new_rhs, proof);
|
||||
}
|
||||
ostream & theorem_rewriter_cell::display(ostream & out) const {
|
||||
out << "Thm_RW(" << m_type << ", " << m_body << ")";
|
||||
return out;
|
||||
}
|
||||
|
||||
// OrElse Rewriter
|
||||
orelse_rewriter_cell::orelse_rewriter_cell(rewriter const & rw1, rewriter const & rw2)
|
||||
:rewriter_cell(rewriter_kind::OrElse), m_rwlist({rw1, rw2}) { }
|
||||
orelse_rewriter_cell::orelse_rewriter_cell(initializer_list<rewriter> const & l)
|
||||
:rewriter_cell(rewriter_kind::OrElse), m_rwlist(l) {
|
||||
lean_assert(l.size() >= 2);
|
||||
}
|
||||
orelse_rewriter_cell::~orelse_rewriter_cell() { }
|
||||
pair<expr, expr> orelse_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
for (rewriter const & rw : m_rwlist) {
|
||||
try {
|
||||
return rw(env, ctx, v);
|
||||
} catch (rewriter_exception & ) {
|
||||
// Do nothing
|
||||
}
|
||||
}
|
||||
// If the execution reaches here, it means every rewriter failed.
|
||||
throw rewriter_exception();
|
||||
}
|
||||
ostream & orelse_rewriter_cell::display(ostream & out) const {
|
||||
out << "Or_RW({";
|
||||
for (rewriter const & rw : m_rwlist) { out << rw << "; "; }
|
||||
out << "})";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Then Rewriter
|
||||
then_rewriter_cell::then_rewriter_cell(rewriter const & rw1, rewriter const & rw2)
|
||||
:rewriter_cell(rewriter_kind::Then), m_rwlist({rw1, rw2}) { }
|
||||
then_rewriter_cell::then_rewriter_cell(initializer_list<rewriter> const & l)
|
||||
:rewriter_cell(rewriter_kind::Then), m_rwlist(l) {
|
||||
lean_assert(l.size() >= 2);
|
||||
}
|
||||
then_rewriter_cell::~then_rewriter_cell() { }
|
||||
pair<expr, expr> then_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
pair<expr, expr> result = car(m_rwlist)(env, ctx, v);
|
||||
pair<expr, expr> new_result = result;
|
||||
for (rewriter const & rw : cdr(m_rwlist)) {
|
||||
new_result = rw(env, ctx, result.first);
|
||||
expr const & ty = type_inferer(env)(v, ctx);
|
||||
if (v != new_result.first) {
|
||||
result = make_pair(new_result.first,
|
||||
mk_trans_th(ty, v, result.first, new_result.first, result.second, new_result.second));
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
ostream & then_rewriter_cell::display(ostream & out) const {
|
||||
out << "Then_RW({";
|
||||
for (rewriter const & rw : m_rwlist) { out << rw << "; "; }
|
||||
out << "})";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Try Rewriter
|
||||
try_rewriter_cell::try_rewriter_cell(rewriter const & rw1, rewriter const & rw2)
|
||||
:rewriter_cell(rewriter_kind::Try), m_rwlist({rw1, rw2}) { }
|
||||
try_rewriter_cell::try_rewriter_cell(initializer_list<rewriter> const & l)
|
||||
:rewriter_cell(rewriter_kind::Try), m_rwlist(l) {
|
||||
lean_assert(l.size() >= 1);
|
||||
}
|
||||
try_rewriter_cell::~try_rewriter_cell() { }
|
||||
pair<expr, expr> try_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
for (rewriter const & rw : m_rwlist) {
|
||||
try {
|
||||
return rw(env, ctx, v);
|
||||
} catch (rewriter_exception & ) {
|
||||
// Do nothing
|
||||
}
|
||||
}
|
||||
// If the execution reaches here, it means every rewriter failed.
|
||||
expr const & t = type_inferer(env)(v, ctx);
|
||||
return make_pair(v, mk_refl_th(t, v));
|
||||
}
|
||||
ostream & try_rewriter_cell::display(ostream & out) const {
|
||||
out << "Try_RW({";
|
||||
for (rewriter const & rw : m_rwlist) { out << rw << "; "; }
|
||||
out << "})";
|
||||
return out;
|
||||
}
|
||||
|
||||
// App Rewriter
|
||||
app_rewriter_cell::app_rewriter_cell(rewriter const & rw)
|
||||
:rewriter_cell(rewriter_kind::App), m_rw(rw) { }
|
||||
app_rewriter_cell::~app_rewriter_cell() { }
|
||||
pair<expr, expr> app_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
if (!is_app(v))
|
||||
throw rewriter_exception();
|
||||
|
||||
buffer<pair<expr, expr>> results;
|
||||
for (unsigned i = 0; i < num_args(v); i++) {
|
||||
results.push_back(m_rw(env, ctx, arg(v, i)));
|
||||
}
|
||||
return rewrite_app(env, ctx, v, results);
|
||||
}
|
||||
|
||||
ostream & app_rewriter_cell::display(ostream & out) const {
|
||||
out << "App_RW(" << m_rw << ")";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Lambda Type Rewriter
|
||||
lambda_type_rewriter_cell::lambda_type_rewriter_cell(rewriter const & rw)
|
||||
:rewriter_cell(rewriter_kind::LambdaType), m_rw(rw) { }
|
||||
lambda_type_rewriter_cell::~lambda_type_rewriter_cell() { }
|
||||
|
||||
pair<expr, expr> lambda_type_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
if (!is_lambda(v))
|
||||
throw rewriter_exception();
|
||||
expr const & ty = abst_domain(v);
|
||||
type_inferer ti(env);
|
||||
pair<expr, expr> result_ty = m_rw(env, ctx, ty);
|
||||
if (ty != result_ty.first) {
|
||||
return rewrite_lambda_type(env, ctx, v, result_ty);
|
||||
} else {
|
||||
// nothing changed
|
||||
return make_pair(v, mk_refl_th(ti(v, ctx), v));
|
||||
}
|
||||
}
|
||||
ostream & lambda_type_rewriter_cell::display(ostream & out) const {
|
||||
out << "Lambda_Type_RW(" << m_rw << ")";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Lambda Body Rewriter
|
||||
lambda_body_rewriter_cell::lambda_body_rewriter_cell(rewriter const & rw)
|
||||
:rewriter_cell(rewriter_kind::LambdaBody), m_rw(rw) { }
|
||||
lambda_body_rewriter_cell::~lambda_body_rewriter_cell() { }
|
||||
|
||||
pair<expr, expr> lambda_body_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
if (!is_lambda(v))
|
||||
throw rewriter_exception();
|
||||
|
||||
name const & n = abst_name(v);
|
||||
expr const & ty = abst_domain(v);
|
||||
expr const & body = abst_body(v);
|
||||
context new_ctx = extend(ctx, n, ty);
|
||||
pair<expr, expr> result_body = m_rw(env, new_ctx, body);
|
||||
if (body != result_body.first) {
|
||||
// body changed
|
||||
return rewrite_lambda_body(env, ctx, v, result_body);
|
||||
} else {
|
||||
// nothing changed
|
||||
type_inferer ti(env);
|
||||
return make_pair(v, mk_refl_th(ti(v, ctx), v));
|
||||
}
|
||||
}
|
||||
ostream & lambda_body_rewriter_cell::display(ostream & out) const {
|
||||
out << "Lambda_Body_RW(" << m_rw << ")";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Lambda Rewriter
|
||||
lambda_rewriter_cell::lambda_rewriter_cell(rewriter const & rw)
|
||||
:rewriter_cell(rewriter_kind::Lambda), m_rw(rw) { }
|
||||
lambda_rewriter_cell::~lambda_rewriter_cell() { }
|
||||
|
||||
pair<expr, expr> lambda_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
if (!is_lambda(v))
|
||||
throw rewriter_exception();
|
||||
rewriter rw = mk_then_rewriter(mk_lambda_type_rewriter(m_rw),
|
||||
mk_lambda_body_rewriter(m_rw));
|
||||
return rw(env, ctx, v);
|
||||
}
|
||||
ostream & lambda_rewriter_cell::display(ostream & out) const {
|
||||
out << "Lambda_RW(" << m_rw << ")";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Pi Type Rewriter
|
||||
pi_type_rewriter_cell::pi_type_rewriter_cell(rewriter const & rw)
|
||||
:rewriter_cell(rewriter_kind::PiType), m_rw(rw) { }
|
||||
pi_type_rewriter_cell::~pi_type_rewriter_cell() { }
|
||||
|
||||
pair<expr, expr> pi_type_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
if (!is_pi(v))
|
||||
throw rewriter_exception();
|
||||
|
||||
expr const & ty = abst_domain(v);
|
||||
pair<expr, expr> result_ty = m_rw(env, ctx, ty);
|
||||
if (ty != result_ty.first) {
|
||||
return rewrite_pi_type(env, ctx, v, result_ty);
|
||||
} else {
|
||||
// nothing changed
|
||||
type_inferer ti(env);
|
||||
return make_pair(v, mk_refl_th(ti(v, ctx), v));
|
||||
}
|
||||
}
|
||||
ostream & pi_type_rewriter_cell::display(ostream & out) const {
|
||||
out << "Pi_Type_RW(" << m_rw << ")";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Pi Body Rewriter
|
||||
pi_body_rewriter_cell::pi_body_rewriter_cell(rewriter const & rw)
|
||||
:rewriter_cell(rewriter_kind::PiBody), m_rw(rw) { }
|
||||
pi_body_rewriter_cell::~pi_body_rewriter_cell() { }
|
||||
|
||||
pair<expr, expr> pi_body_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
if (!is_pi(v))
|
||||
throw rewriter_exception();
|
||||
|
||||
name const & n = abst_name(v);
|
||||
expr const & ty = abst_domain(v);
|
||||
expr const & body = abst_body(v);
|
||||
context new_ctx = extend(ctx, n, ty);
|
||||
pair<expr, expr> result_body = m_rw(env, new_ctx, body);
|
||||
if (body != result_body.first) {
|
||||
// body changed
|
||||
return rewrite_pi_body(env, ctx, v, result_body);
|
||||
} else {
|
||||
// nothing changed
|
||||
type_inferer ti(env);
|
||||
return make_pair(v, mk_refl_th(ti(v, ctx), v));
|
||||
}
|
||||
}
|
||||
ostream & pi_body_rewriter_cell::display(ostream & out) const {
|
||||
out << "Pi_Body_RW(" << m_rw << ")";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Pi Rewriter
|
||||
pi_rewriter_cell::pi_rewriter_cell(rewriter const & rw)
|
||||
:rewriter_cell(rewriter_kind::Pi), m_rw(rw) { }
|
||||
pi_rewriter_cell::~pi_rewriter_cell() { }
|
||||
pair<expr, expr> pi_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
if (!is_pi(v))
|
||||
throw rewriter_exception();
|
||||
rewriter rw = mk_then_rewriter(mk_pi_type_rewriter(m_rw),
|
||||
mk_pi_body_rewriter(m_rw));
|
||||
return rw(env, ctx, v);
|
||||
}
|
||||
ostream & pi_rewriter_cell::display(ostream & out) const {
|
||||
out << "Pi_RW(" << m_rw << ")";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Let Type rewriter
|
||||
let_type_rewriter_cell::let_type_rewriter_cell(rewriter const & rw)
|
||||
:rewriter_cell(rewriter_kind::LetType), m_rw(rw) { }
|
||||
let_type_rewriter_cell::~let_type_rewriter_cell() { }
|
||||
pair<expr, expr> let_type_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
if (!is_let(v) || !let_type(v))
|
||||
throw rewriter_exception();
|
||||
|
||||
expr const & ty = *let_type(v);
|
||||
|
||||
pair<expr, expr> result_ty = m_rw(env, ctx, ty);
|
||||
if (ty != result_ty.first) {
|
||||
// ty changed
|
||||
return rewrite_let_type(env, ctx, v, result_ty);
|
||||
} else {
|
||||
type_inferer ti(env);
|
||||
return make_pair(v, mk_refl_th(ti(v, ctx), v));
|
||||
}
|
||||
}
|
||||
ostream & let_type_rewriter_cell::display(ostream & out) const {
|
||||
out << "Let_Type_RW(" << m_rw << ")";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Let Value rewriter
|
||||
let_value_rewriter_cell::let_value_rewriter_cell(rewriter const & rw)
|
||||
:rewriter_cell(rewriter_kind::LetValue), m_rw(rw) { }
|
||||
let_value_rewriter_cell::~let_value_rewriter_cell() { }
|
||||
pair<expr, expr> let_value_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
if (!is_let(v))
|
||||
throw rewriter_exception();
|
||||
|
||||
expr const & val = let_value(v);
|
||||
pair<expr, expr> result_val = m_rw(env, ctx, val);
|
||||
if (val != result_val.first) {
|
||||
// ty changed
|
||||
return rewrite_let_value(env, ctx, v, result_val);
|
||||
} else {
|
||||
type_inferer ti(env);
|
||||
return make_pair(v, mk_refl_th(ti(v, ctx), v));
|
||||
}
|
||||
}
|
||||
ostream & let_value_rewriter_cell::display(ostream & out) const {
|
||||
out << "Let_Value_RW(" << m_rw << ")";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Let Body rewriter
|
||||
let_body_rewriter_cell::let_body_rewriter_cell(rewriter const & rw)
|
||||
:rewriter_cell(rewriter_kind::LetBody), m_rw(rw) { }
|
||||
let_body_rewriter_cell::~let_body_rewriter_cell() { }
|
||||
pair<expr, expr> let_body_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
if (!is_let(v))
|
||||
throw rewriter_exception();
|
||||
|
||||
name const & n = let_name(v);
|
||||
optional<expr> const & ty = let_type(v);
|
||||
expr const & body = let_body(v);
|
||||
context new_ctx = extend(ctx, n, ty, let_value(v));
|
||||
pair<expr, expr> result_body = m_rw(env, new_ctx, body);
|
||||
if (body != result_body.first) {
|
||||
return rewrite_let_body(env, ctx, v, result_body);
|
||||
} else {
|
||||
type_inferer ti(env);
|
||||
return make_pair(v, mk_refl_th(ti(v, ctx), v));
|
||||
}
|
||||
}
|
||||
ostream & let_body_rewriter_cell::display(ostream & out) const {
|
||||
out << "Let_Body_RW(" << m_rw << ")";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Let rewriter
|
||||
let_rewriter_cell::let_rewriter_cell(rewriter const & rw)
|
||||
:rewriter_cell(rewriter_kind::Let), m_rw(rw) { }
|
||||
let_rewriter_cell::~let_rewriter_cell() { }
|
||||
pair<expr, expr> let_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
if (!is_let(v))
|
||||
throw rewriter_exception();
|
||||
rewriter rw = mk_then_rewriter({mk_let_type_rewriter(m_rw),
|
||||
mk_let_value_rewriter(m_rw),
|
||||
mk_let_body_rewriter(m_rw)});
|
||||
return rw(env, ctx, v);
|
||||
}
|
||||
ostream & let_rewriter_cell::display(ostream & out) const {
|
||||
out << "Let_RW(" << m_rw << ")";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Fail rewriter
|
||||
fail_rewriter_cell::fail_rewriter_cell():rewriter_cell(rewriter_kind::Fail) { }
|
||||
fail_rewriter_cell::~fail_rewriter_cell() { }
|
||||
pair<expr, expr> fail_rewriter_cell::operator()(environment const &, context &, expr const &) const throw(rewriter_exception) {
|
||||
throw rewriter_exception();
|
||||
}
|
||||
ostream & fail_rewriter_cell::display(ostream & out) const {
|
||||
out << "Fail_RW()";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Success rewriter (trivial)
|
||||
success_rewriter_cell::success_rewriter_cell():rewriter_cell(rewriter_kind::Success) { }
|
||||
success_rewriter_cell::~success_rewriter_cell() { }
|
||||
pair<expr, expr> success_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
expr const & t = type_inferer(env)(v, ctx);
|
||||
return make_pair(v, mk_refl_th(t, v));
|
||||
}
|
||||
ostream & success_rewriter_cell::display(ostream & out) const {
|
||||
out << "Success_RW()";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Repeat rewriter
|
||||
repeat_rewriter_cell::repeat_rewriter_cell(rewriter const & rw):rewriter_cell(rewriter_kind::Repeat), m_rw(rw) { }
|
||||
repeat_rewriter_cell::~repeat_rewriter_cell() { }
|
||||
pair<expr, expr> repeat_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
pair<expr, expr> result = mk_success_rewriter()(env, ctx, v);
|
||||
type_inferer ti(env);
|
||||
try {
|
||||
while (true) {
|
||||
pair<expr, expr> new_result = m_rw(env, ctx, result.first);
|
||||
if (result.first == new_result.first)
|
||||
break;
|
||||
expr const & ty = ti(v, ctx);
|
||||
result = make_pair(new_result.first,
|
||||
mk_trans_th(ty, v, result.first, new_result.first, result.second, new_result.second));
|
||||
}
|
||||
} catch (rewriter_exception &) {
|
||||
return result;
|
||||
}
|
||||
return result;
|
||||
}
|
||||
ostream & repeat_rewriter_cell::display(ostream & out) const {
|
||||
out << "Repeat_RW(" << m_rw << ")";
|
||||
return out;
|
||||
}
|
||||
|
||||
// Depth rewriter
|
||||
depth_rewriter_cell::depth_rewriter_cell(rewriter const & rw):rewriter_cell(rewriter_kind::Depth), m_rw(rw) { }
|
||||
depth_rewriter_cell::~depth_rewriter_cell() { }
|
||||
pair<expr, expr> depth_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
|
||||
return apply_rewriter_fn<decltype(m_rw)>(m_rw)(env, ctx, v);
|
||||
}
|
||||
ostream & depth_rewriter_cell::display(ostream & out) const {
|
||||
out << "Depth_RW(" << m_rw << ")";
|
||||
return out;
|
||||
}
|
||||
|
||||
rewriter mk_theorem_rewriter(expr const & type, expr const & body) {
|
||||
return rewriter(new theorem_rewriter_cell(type, body));
|
||||
}
|
||||
rewriter mk_then_rewriter(rewriter const & rw1, rewriter const & rw2) {
|
||||
return rewriter(new then_rewriter_cell(rw1, rw2));
|
||||
}
|
||||
rewriter mk_then_rewriter(initializer_list<rewriter> const & l) {
|
||||
return rewriter(new then_rewriter_cell(l));
|
||||
}
|
||||
rewriter mk_try_rewriter(rewriter const & rw) {
|
||||
return rewriter(new try_rewriter_cell({rw}));
|
||||
}
|
||||
rewriter mk_try_rewriter(rewriter const & rw1, rewriter const & rw2) {
|
||||
return rewriter(new try_rewriter_cell(rw1, rw2));
|
||||
}
|
||||
rewriter mk_try_rewriter(initializer_list<rewriter> const & l) {
|
||||
return rewriter(new try_rewriter_cell(l));
|
||||
}
|
||||
rewriter mk_orelse_rewriter(rewriter const & rw1, rewriter const & rw2) {
|
||||
return rewriter(new orelse_rewriter_cell(rw1, rw2));
|
||||
}
|
||||
rewriter mk_orelse_rewriter(initializer_list<rewriter> const & l) {
|
||||
return rewriter(new orelse_rewriter_cell(l));
|
||||
}
|
||||
rewriter mk_app_rewriter(rewriter const & rw) {
|
||||
return rewriter(new app_rewriter_cell(rw));
|
||||
}
|
||||
rewriter mk_lambda_type_rewriter(rewriter const & rw) {
|
||||
return rewriter(new lambda_type_rewriter_cell(rw));
|
||||
}
|
||||
rewriter mk_lambda_body_rewriter(rewriter const & rw) {
|
||||
return rewriter(new lambda_body_rewriter_cell(rw));
|
||||
}
|
||||
rewriter mk_lambda_rewriter(rewriter const & rw) {
|
||||
return rewriter(new lambda_rewriter_cell(rw));
|
||||
}
|
||||
rewriter mk_pi_type_rewriter(rewriter const & rw) {
|
||||
return rewriter(new pi_type_rewriter_cell(rw));
|
||||
}
|
||||
rewriter mk_pi_body_rewriter(rewriter const & rw) {
|
||||
return rewriter(new pi_body_rewriter_cell(rw));
|
||||
}
|
||||
rewriter mk_pi_rewriter(rewriter const & rw) {
|
||||
return rewriter(new pi_rewriter_cell(rw));
|
||||
}
|
||||
rewriter mk_let_type_rewriter(rewriter const & rw) {
|
||||
return rewriter(new let_type_rewriter_cell(rw));
|
||||
}
|
||||
rewriter mk_let_value_rewriter(rewriter const & rw) {
|
||||
return rewriter(new let_value_rewriter_cell(rw));
|
||||
}
|
||||
rewriter mk_let_body_rewriter(rewriter const & rw) {
|
||||
return rewriter(new let_body_rewriter_cell(rw));
|
||||
}
|
||||
rewriter mk_let_rewriter(rewriter const & rw) {
|
||||
return rewriter(new let_rewriter_cell(rw));
|
||||
}
|
||||
rewriter mk_fail_rewriter() {
|
||||
return rewriter(new fail_rewriter_cell());
|
||||
}
|
||||
rewriter mk_success_rewriter() {
|
||||
return rewriter(new success_rewriter_cell());
|
||||
}
|
||||
rewriter mk_repeat_rewriter(rewriter const & rw) {
|
||||
return rewriter(new repeat_rewriter_cell(rw));
|
||||
}
|
||||
rewriter mk_depth_rewriter(rewriter const & rw) {
|
||||
return rewriter(new depth_rewriter_cell(rw));
|
||||
}
|
||||
}
|
||||
|
|
@ -1,524 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation.
|
||||
Copyright (c) 2013 Carnegie Mellon University.
|
||||
All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Soonho Kong
|
||||
*/
|
||||
#pragma once
|
||||
#include <algorithm>
|
||||
#include <utility>
|
||||
#include "kernel/abstract.h"
|
||||
#include "kernel/context.h"
|
||||
#include "kernel/environment.h"
|
||||
#include "kernel/expr.h"
|
||||
#include "kernel/replace_fn.h"
|
||||
#include "kernel/type_checker.h"
|
||||
#include "kernel/kernel.h"
|
||||
#include "library/rewriter/rewriter.h"
|
||||
#include "util/exception.h"
|
||||
#include "util/scoped_map.h"
|
||||
// TODO(soonhok)
|
||||
// FORALL
|
||||
// FAIL_IF
|
||||
|
||||
namespace lean {
|
||||
|
||||
class rewriter_exception : public exception {
|
||||
public:
|
||||
virtual exception * clone() const { return new rewriter_exception(); }
|
||||
virtual void rethrow() const { throw *this; }
|
||||
};
|
||||
|
||||
enum class rewriter_kind { Theorem, OrElse, Then, Try, App,
|
||||
LambdaType, LambdaBody, Lambda,
|
||||
PiType, PiBody, Pi,
|
||||
LetType, LetValue, LetBody, Let,
|
||||
Fail, Success, Repeat, Depth };
|
||||
|
||||
std::pair<expr, expr> rewrite_lambda_type(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_ty);
|
||||
std::pair<expr, expr> rewrite_lambda_body(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_body);
|
||||
std::pair<expr, expr> rewrite_lambda(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_ty, std::pair<expr, expr> const & result_body);
|
||||
std::pair<expr, expr> rewrite_pi_type(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_ty);
|
||||
std::pair<expr, expr> rewrite_pi_body(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_body);
|
||||
std::pair<expr, expr> rewrite_pi(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_ty, std::pair<expr, expr> const & result_body);
|
||||
std::pair<expr, expr> rewrite_let_type(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_ty);
|
||||
std::pair<expr, expr> rewrite_let_value(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_value);
|
||||
std::pair<expr, expr> rewrite_let_body(environment const & env, context & ctx, expr const & v, std::pair<expr, expr> const & result_body);
|
||||
std::pair<expr, expr> rewrite_app(environment const & env, context & ctx, expr const & v, buffer<std::pair<expr, expr>> const & results );
|
||||
|
||||
class rewriter;
|
||||
|
||||
class rewriter_cell {
|
||||
protected:
|
||||
rewriter_kind m_kind;
|
||||
MK_LEAN_RC();
|
||||
void dealloc();
|
||||
virtual std::ostream & display(std::ostream & out) const = 0;
|
||||
public:
|
||||
rewriter_cell(rewriter_kind k);
|
||||
virtual ~rewriter_cell();
|
||||
rewriter_kind kind() const { return m_kind; }
|
||||
// unsigned hash() const { return m_hash; }
|
||||
virtual std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) = 0;
|
||||
friend std::ostream & operator<<(std::ostream & out, rewriter_cell const & rw);
|
||||
};
|
||||
|
||||
class rewriter {
|
||||
private:
|
||||
rewriter_cell * m_ptr;
|
||||
public:
|
||||
explicit rewriter(rewriter_cell * ptr):m_ptr(ptr) {}
|
||||
rewriter():m_ptr(nullptr) {}
|
||||
rewriter(rewriter const & r):m_ptr(r.m_ptr) {
|
||||
if (m_ptr) m_ptr->inc_ref();
|
||||
}
|
||||
rewriter(rewriter && r):m_ptr(r.m_ptr) { r.m_ptr = nullptr; }
|
||||
~rewriter() { if (m_ptr) m_ptr->dec_ref(); }
|
||||
void release() { if (m_ptr) m_ptr->dec_ref(); m_ptr = nullptr; }
|
||||
friend void swap(rewriter & a, rewriter & b) { std::swap(a.m_ptr, b.m_ptr); }
|
||||
rewriter_kind kind() const { return m_ptr->kind(); }
|
||||
rewriter & operator=(rewriter const & s) { LEAN_COPY_REF(s); }
|
||||
rewriter & operator=(rewriter && s) { LEAN_MOVE_REF(s); }
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const {
|
||||
return (*m_ptr)(env, ctx, v);
|
||||
}
|
||||
friend std::ostream & operator<<(std::ostream & out, rewriter const & rw);
|
||||
};
|
||||
|
||||
class theorem_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
expr const & m_type;
|
||||
expr const & m_body;
|
||||
expr m_pattern;
|
||||
expr m_rhs;
|
||||
unsigned m_num_args;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
|
||||
public:
|
||||
theorem_rewriter_cell(expr const & type, expr const & body);
|
||||
~theorem_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class orelse_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
list<rewriter> m_rwlist;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
orelse_rewriter_cell(rewriter const & rw1, rewriter const & rw2);
|
||||
orelse_rewriter_cell(std::initializer_list<rewriter> const & l);
|
||||
~orelse_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class then_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
list<rewriter> m_rwlist;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
then_rewriter_cell(rewriter const & rw1, rewriter const & rw2);
|
||||
then_rewriter_cell(std::initializer_list<rewriter> const & l);
|
||||
~then_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class try_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
list<rewriter> m_rwlist;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
try_rewriter_cell(rewriter const & rw1, rewriter const & rw2);
|
||||
try_rewriter_cell(std::initializer_list<rewriter> const & l);
|
||||
~try_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class app_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
rewriter m_rw;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
app_rewriter_cell(rewriter const & rw);
|
||||
~app_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class lambda_type_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
rewriter m_rw;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
lambda_type_rewriter_cell(rewriter const & rw);
|
||||
~lambda_type_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class lambda_body_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
rewriter m_rw;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
lambda_body_rewriter_cell(rewriter const & rw);
|
||||
~lambda_body_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class lambda_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
rewriter m_rw;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
lambda_rewriter_cell(rewriter const & rw);
|
||||
~lambda_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class pi_type_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
rewriter m_rw;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
pi_type_rewriter_cell(rewriter const & rw);
|
||||
~pi_type_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class pi_body_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
rewriter m_rw;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
pi_body_rewriter_cell(rewriter const & rw);
|
||||
~pi_body_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class pi_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
rewriter m_rw;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
pi_rewriter_cell(rewriter const & rw);
|
||||
~pi_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
|
||||
class let_type_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
rewriter m_rw;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
let_type_rewriter_cell(rewriter const & rw);
|
||||
~let_type_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class let_value_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
rewriter m_rw;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
let_value_rewriter_cell(rewriter const & rw);
|
||||
~let_value_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class let_body_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
rewriter m_rw;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
let_body_rewriter_cell(rewriter const & rw);
|
||||
~let_body_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class let_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
rewriter m_rw;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
let_rewriter_cell(rewriter const & rw);
|
||||
~let_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class fail_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
fail_rewriter_cell();
|
||||
~fail_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class success_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
success_rewriter_cell();
|
||||
~success_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class repeat_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
rewriter m_rw;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
repeat_rewriter_cell(rewriter const & rw);
|
||||
~repeat_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
class depth_rewriter_cell : public rewriter_cell {
|
||||
private:
|
||||
rewriter m_rw;
|
||||
std::ostream & display(std::ostream & out) const;
|
||||
public:
|
||||
depth_rewriter_cell(rewriter const & rw);
|
||||
~depth_rewriter_cell();
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception);
|
||||
};
|
||||
|
||||
/** \brief (For debugging) Display the content of this rewriter */
|
||||
inline std::ostream & operator<<(std::ostream & out, rewriter_cell const & rc) { rc.display(out); return out; }
|
||||
inline std::ostream & operator<<(std::ostream & out, rewriter const & rw) { out << *(rw.m_ptr); return out; }
|
||||
|
||||
rewriter mk_theorem_rewriter(expr const & type, expr const & body);
|
||||
rewriter mk_then_rewriter(rewriter const & rw1, rewriter const & rw2);
|
||||
rewriter mk_then_rewriter(std::initializer_list<rewriter> const & l);
|
||||
rewriter mk_try_rewriter(rewriter const & rw);
|
||||
rewriter mk_try_rewriter(rewriter const & rw1, rewriter const & rw2);
|
||||
rewriter mk_try_rewriter(std::initializer_list<rewriter> const & l);
|
||||
rewriter mk_orelse_rewriter(rewriter const & rw1, rewriter const & rw2);
|
||||
rewriter mk_orelse_rewriter(std::initializer_list<rewriter> const & l);
|
||||
rewriter mk_app_rewriter(rewriter const & rw);
|
||||
rewriter mk_lambda_type_rewriter(rewriter const & rw);
|
||||
rewriter mk_lambda_body_rewriter(rewriter const & rw);
|
||||
rewriter mk_lambda_rewriter(rewriter const & rw);
|
||||
rewriter mk_pi_type_rewriter(rewriter const & rw);
|
||||
rewriter mk_pi_body_rewriter(rewriter const & rw);
|
||||
rewriter mk_pi_rewriter(rewriter const & rw);
|
||||
rewriter mk_let_type_rewriter(rewriter const & rw);
|
||||
rewriter mk_let_value_rewriter(rewriter const & rw);
|
||||
rewriter mk_let_body_rewriter(rewriter const & rw);
|
||||
rewriter mk_let_rewriter(rewriter const & rw);
|
||||
rewriter mk_fail_rewriter();
|
||||
rewriter mk_success_rewriter();
|
||||
rewriter mk_repeat_rewriter(rewriter const & rw);
|
||||
rewriter mk_depth_rewriter(rewriter const & rw);
|
||||
|
||||
/**
|
||||
\brief Functional for applying <tt>F</tt> to the subexpressions of a given expression.
|
||||
|
||||
The signature of \c F is
|
||||
expr const &, context const & ctx, unsigned n -> expr
|
||||
|
||||
F is invoked for each subexpression \c s of the input expression e.
|
||||
In a call <tt>F(s, c, n)</tt>, \c c is the context where \c s occurs,
|
||||
and \c n is the size of \c c.
|
||||
|
||||
P is a "post-processing" functional object that is applied to each
|
||||
pair (old, new)
|
||||
*/
|
||||
template<typename RW, typename P = default_replace_postprocessor>
|
||||
class apply_rewriter_fn {
|
||||
// the return type of RW()(env, ctx, e) should be std::pair<expr, expr>
|
||||
static_assert(std::is_same<typename std::result_of<decltype(std::declval<RW>())(environment const &, context &, expr const &)>::type,
|
||||
std::pair<expr, expr>>::value,
|
||||
"apply_rewriter_fn: the return type of RW()(env, ctx, e) should be std::pair<expr, expr>");
|
||||
// the return type of P()(e1, e2) should be void
|
||||
static_assert(std::is_same<typename std::result_of<decltype(std::declval<P>())(expr const &, expr const &)>::type,
|
||||
void>::value,
|
||||
"apply_rewriter_fn: the return type of P()(e1, e2) is not void");
|
||||
|
||||
typedef scoped_map<expr, std::pair<expr, expr>, expr_hash, expr_eqp> cache;
|
||||
cache m_cache;
|
||||
RW m_rw;
|
||||
P m_post;
|
||||
|
||||
std::pair<expr, expr> apply(environment const & env, context & ctx, expr const & v) {
|
||||
bool shared = false;
|
||||
if (is_shared(v)) {
|
||||
shared = true;
|
||||
auto it = m_cache.find(v);
|
||||
if (it != m_cache.end())
|
||||
return it->second;
|
||||
}
|
||||
|
||||
std::pair<expr, expr> result; // m_rw(env, ctx, v);
|
||||
// if (is_eqp(v, result.first))
|
||||
type_inferer ti(env);
|
||||
expr ty_v = ti(v, ctx);
|
||||
|
||||
switch (v.kind()) {
|
||||
case expr_kind::Type:
|
||||
result = m_rw(env, ctx, v);
|
||||
break;
|
||||
case expr_kind::Value:
|
||||
result = m_rw(env, ctx, v);
|
||||
break;
|
||||
case expr_kind::Constant:
|
||||
result = m_rw(env, ctx, v);
|
||||
break;
|
||||
case expr_kind::Var:
|
||||
result = m_rw(env, ctx, v);
|
||||
break;
|
||||
case expr_kind::MetaVar:
|
||||
result = m_rw(env, ctx, v);
|
||||
break;
|
||||
case expr_kind::App: {
|
||||
buffer<std::pair<expr, expr>> results;
|
||||
for (unsigned i = 0; i < num_args(v); i++) {
|
||||
results.push_back(apply(env, ctx, arg(v, i)));
|
||||
}
|
||||
result = rewrite_app(env, ctx, v, results);
|
||||
std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
|
||||
if (result.first != tmp.first) {
|
||||
tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second);
|
||||
result = tmp;
|
||||
}
|
||||
}
|
||||
break;
|
||||
case expr_kind::HEq: case expr_kind::Proj: case expr_kind::Pair: case expr_kind::Sigma:
|
||||
// TODO(Leo):
|
||||
break;
|
||||
case expr_kind::Lambda: {
|
||||
name const & n = abst_name(v);
|
||||
expr const & ty = abst_domain(v);
|
||||
expr const & body = abst_body(v);
|
||||
context new_ctx = extend(ctx, n, ty);
|
||||
std::pair<expr, expr> result_ty = apply(env, ctx, ty);
|
||||
std::pair<expr, expr> result_body = apply(env, new_ctx, body);
|
||||
if (ty != result_ty.first) {
|
||||
if (body != result_body.first) {
|
||||
// ty and body changed
|
||||
result = rewrite_lambda(env, ctx, v, result_ty, result_body);
|
||||
} else {
|
||||
// ty changed
|
||||
result = rewrite_lambda_type(env, ctx, v, result_ty);
|
||||
}
|
||||
} else {
|
||||
if (body != result_body.first) {
|
||||
// body changed
|
||||
result = rewrite_lambda_body(env, ctx, v, result_body);
|
||||
} else {
|
||||
// nothing changed
|
||||
result = std::make_pair(v, mk_refl_th(ti(v, ctx), v));
|
||||
}
|
||||
}
|
||||
std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
|
||||
if (result.first != tmp.first) {
|
||||
tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second);
|
||||
result = tmp;
|
||||
}
|
||||
}
|
||||
break;
|
||||
|
||||
case expr_kind::Pi: {
|
||||
name const & n = abst_name(v);
|
||||
expr const & ty = abst_domain(v);
|
||||
expr const & body = abst_body(v);
|
||||
context new_ctx = extend(ctx, n, ty);
|
||||
std::pair<expr, expr> result_ty = apply(env, ctx, ty);
|
||||
std::pair<expr, expr> result_body = apply(env, new_ctx, body);
|
||||
if (ty != result_ty.first) {
|
||||
if (body != result_body.first) {
|
||||
// ty and body changed
|
||||
result = rewrite_pi(env, ctx, v, result_ty, result_body);
|
||||
} else {
|
||||
// ty changed
|
||||
result = rewrite_pi_type(env, ctx, v, result_ty);
|
||||
}
|
||||
} else {
|
||||
if (body != result_body.first) {
|
||||
// body changed
|
||||
result = rewrite_pi_body(env, ctx, v, result_body);
|
||||
} else {
|
||||
// nothing changed
|
||||
result = std::make_pair(v, mk_refl_th(ti(v, ctx), v));
|
||||
}
|
||||
}
|
||||
std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
|
||||
if (result.first != tmp.first) {
|
||||
tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second);
|
||||
result = tmp;
|
||||
}
|
||||
}
|
||||
break;
|
||||
case expr_kind::Let: {
|
||||
name const & n = let_name(v);
|
||||
optional<expr> const & ty = let_type(v);
|
||||
expr const & val = let_value(v);
|
||||
expr const & body = let_body(v);
|
||||
|
||||
expr new_v = v;
|
||||
expr ty_v = ti(v, ctx);
|
||||
expr pf = mk_refl_th(ty_v, v);
|
||||
bool changed = false;
|
||||
|
||||
if (ty) {
|
||||
std::pair<expr, expr> result_ty = apply(env, ctx, *ty);
|
||||
if (*ty != result_ty.first) {
|
||||
// ty changed
|
||||
result = rewrite_let_type(env, ctx, new_v, result_ty);
|
||||
new_v = result.first;
|
||||
pf = result.second;
|
||||
changed = true;
|
||||
}
|
||||
}
|
||||
|
||||
std::pair<expr, expr> result_val = apply(env, ctx, val);
|
||||
if (val != result_val.first) {
|
||||
result = rewrite_let_value(env, ctx, new_v, result_val);
|
||||
if (changed) {
|
||||
pf = mk_trans_th(ty_v, v, new_v, result.first, pf, result.second);
|
||||
} else {
|
||||
pf = result.second;
|
||||
}
|
||||
new_v = result.first;
|
||||
changed = true;
|
||||
}
|
||||
|
||||
context new_ctx = extend(ctx, n, ty, val);
|
||||
std::pair<expr, expr> result_body = apply(env, new_ctx, body);
|
||||
if (body != result_body.first) {
|
||||
result = rewrite_let_body(env, ctx, new_v, result_body);
|
||||
if (changed) {
|
||||
pf = mk_trans_th(ty_v, v, new_v, result.first, pf, result.second);
|
||||
} else {
|
||||
pf = result.second;
|
||||
}
|
||||
new_v = result.first;
|
||||
changed = true;
|
||||
}
|
||||
result = std::make_pair(new_v, pf);
|
||||
|
||||
std::pair<expr, expr> tmp = m_rw(env, ctx, result.first);
|
||||
if (result.first != tmp.first) {
|
||||
tmp.second = mk_trans_th(ty_v, v, result.first, tmp.first, result.second, tmp.second);
|
||||
result = tmp;
|
||||
}
|
||||
}
|
||||
break;
|
||||
}
|
||||
if (shared)
|
||||
m_cache.insert(std::make_pair(v, result));
|
||||
return result;
|
||||
}
|
||||
|
||||
public:
|
||||
apply_rewriter_fn(RW const & rw, P const & p = P()):
|
||||
m_rw(rw),
|
||||
m_post(p) {
|
||||
}
|
||||
std::pair<expr, expr> operator()(environment const & env, context & ctx, expr const & v) {
|
||||
return apply(env, ctx, v);
|
||||
}
|
||||
};
|
||||
|
||||
}
|
||||
Loading…
Reference in a new issue