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

feat: apply csimp attribute constant replacements

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-21 12:22:15 -07:00
parent 347710204a
commit 6cfdfe9942
3 changed files with 30 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -159,6 +159,12 @@ bool is_main_fn_type(expr const & type) {
#define trace_compiler(k, ds) lean_trace(k, trace_comp_decls(ds););
extern "C" object* lean_csimp_replace_constants(object* env, object* n);
expr csimp_replace_constants(environment const & env, expr const & e) {
return expr(lean_csimp_replace_constants(env.to_obj_arg(), e.to_obj_arg()));
}
environment compile(environment const & env, options const & opts, names cs) {
if (!is_codegen_enabled(opts))
return env;
@ -206,6 +212,7 @@ environment compile(environment const & env, options const & opts, names cs) {
// trace(ds);
ds = apply(cce, env, ds);
trace_compiler(name({"compiler", "cce"}), ds);
ds = apply(csimp_replace_constants, env, ds);
ds = apply(simp, env, ds);
trace_compiler(name({"compiler", "simp"}), ds);
// trace(ds);

17
tests/lean/csimpAttr.lean Normal file
View file

@ -0,0 +1,17 @@
def foo (x : Nat) :=
2*x
def boo (x : Nat) :=
x + x
@[csimp] theorem foo_eq_boo1 (x : Nat) : foo x = boo x := by -- Error
simp [foo, boo, Nat.mul_comm]
show (x * 1) + x = x + x
simp
@[csimp] theorem foo_eq_boo2 : foo = boo :=
funext foo_eq_boo1
set_option trace.compiler.ir.init true
def f (x : Nat) : Nat :=
foo (foo x)

6
tests/lean/csimpAttr.lean.expected.out Normal file
View file

@ -0,0 +1,6 @@
[init]
def f (x_1 : obj) : obj :=
let x_2 : obj := Nat.add x_1 x_1;
let x_3 : obj := Nat.add x_2 x_2;
ret x_3csimpAttr.lean:7:17-7:28: error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported.