From bbd3a394e3854e27d3a344063d3f03baea16b8e8 Mon Sep 17 00:00:00 2001 From: lecopivo Date: Thu, 7 Mar 2024 18:11:53 -0500 Subject: [PATCH] continue simplifying after autodiff --- SciLean/Tactic/Autodiff.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/SciLean/Tactic/Autodiff.lean b/SciLean/Tactic/Autodiff.lean index 945f38b0..deb2c760 100644 --- a/SciLean/Tactic/Autodiff.lean +++ b/SciLean/Tactic/Autodiff.lean @@ -15,7 +15,9 @@ simproc_decl lift_lets_simproc (_) := fun e => do -- todo: add option, discharger, only and [...] syntax macro "autodiff" : conv => - `(conv| fun_trans (config:={zeta:=false,singlePass:=true}) (disch:=sorry) only [ftrans_simp,lift_lets_simproc]) + `(conv| (fun_trans (config:={zeta:=false,singlePass:=true}) (disch:=sorry) only [ftrans_simp,lift_lets_simproc]; + simp (config:={zeta:=false,failIfUnchanged:=false}) only [ftrans_simp,lift_lets_simproc])) macro "autodiff" : tactic => - `(tactic| fun_trans (config:={zeta:=false,singlePass:=true}) (disch:=sorry) only [ftrans_simp,lift_lets_simproc]) + `(tactic| (fun_trans (config:={zeta:=false,singlePass:=true}) (disch:=sorry) only [ftrans_simp,lift_lets_simproc]; + simp (config:={zeta:=false,failIfUnchanged:=false}) only [ftrans_simp,lift_lets_simproc]))