max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/compiler): cdecl ==> comp_decl

Browse source
This commit is contained in:
Leonardo de Moura 2018-10-05 17:10:35 -07:00
parent d75b1c57bf
commit fc62e8f3a4
2 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/library/compiler/compiler.cpp
View file

@ -22,8 +22,8 @@ bool is_codegen_enabled(options const & opts) {
return opts.get_bool(*g_codegen, true);
}
static cdecls to_cdecls(environment const & env, names const & cs) {
return map2<cdecl>(cs, [&](name const & n) { return cdecl(n, env.get(n).get_value()); });
static comp_decls to_comp_decls(environment const & env, names const & cs) {
return map2<comp_decl>(cs, [&](name const & n) { return comp_decl(n, env.get(n).get_value()); });
}
static expr eta_expand(environment const & env, expr const & e) {
@ -31,13 +31,13 @@ static expr eta_expand(environment const & env, expr const & e) {
}
template<typename F>
cdecls apply(F && f, environment const & env, cdecls const & ds) {
return map(ds, [&](cdecl const & d) { return cdecl(d.fst(), f(env, d.snd())); });
comp_decls apply(F && f, environment const & env, comp_decls const & ds) {
return map(ds, [&](comp_decl const & d) { return comp_decl(d.fst(), f(env, d.snd())); });
}
template<typename F>
cdecls apply(F && f, cdecls const & ds) {
return map(ds, [&](cdecl const & d) { return cdecl(d.fst(), f(d.snd())); });
comp_decls apply(F && f, comp_decls const & ds) {
return map(ds, [&](comp_decl const & d) { return comp_decl(d.fst(), f(d.snd())); });
}
environment compile(environment const & env, options const & opts, names const & cs) {
@ -49,7 +49,7 @@ environment compile(environment const & env, options const & opts, names const &
return env;
}
cdecls ds = to_cdecls(env, cs);
comp_decls ds = to_comp_decls(env, cs);
auto simp = [&](environment const & env, expr const & e) { return csimp(env, e, csimp_cfg(opts)); };
ds = apply(eta_expand, env, ds);

6
src/library/compiler/util.h
View file

@ -13,9 +13,9 @@ Author: Leonardo de Moura
#include "library/util.h"
namespace lean {
/* A "compiler" declaration `v := e` */
typedef pair_ref<name, expr> cdecl;
typedef list_ref<cdecl> cdecls;
/* A "compiler" declaration `x := e` */
typedef pair_ref<name, expr> comp_decl;
typedef list_ref<comp_decl> comp_decls;
/* If `e` is of the form `(fun x, t) a` return `head_beta_const_fn(t)` if `t` does not depend on `x`,
and `e` otherwise. We also reduce `(fun x_1 ... x_n, x_i) a_1 ... a_n` into `a_[n-i-1]` */