From fc62e8f3a43a94d99e2d8987cfd5f1c577476af7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Oct 2018 17:10:35 -0700 Subject: [PATCH] chore(library/compiler): `cdecl` ==> `comp_decl` --- src/library/compiler/compiler.cpp | 14 +++++++------- src/library/compiler/util.h | 6 +++--- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index 8531531fcf..64567dda96 100644 --- a/src/library/compiler/compiler.cpp +++ b/src/library/compiler/compiler.cpp @@ -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(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(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 -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 -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); diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h index 6ed66990fa..dce2c15a5e 100644 --- a/src/library/compiler/util.h +++ b/src/library/compiler/util.h @@ -13,9 +13,9 @@ Author: Leonardo de Moura #include "library/util.h" namespace lean { -/* A "compiler" declaration `v := e` */ -typedef pair_ref cdecl; -typedef list_ref cdecls; +/* A "compiler" declaration `x := e` */ +typedef pair_ref comp_decl; +typedef list_ref 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]` */