fix to lsimp, call reduce instead of full dsimp in post pass, fixes #26

lecopivo · Oct 31, 2023 · a4797fb · a4797fb
1 parent 4ac0357
commit a4797fb
Show file tree

Hide file tree

Showing 3 changed files with 32 additions and 40 deletions.
diff --git a/SciLean/Core/FunctionPropositions/HasAdjDiffAt.lean b/SciLean/Core/FunctionPropositions/HasAdjDiffAt.lean
@@ -322,7 +322,7 @@ theorem HSMul.hSMul.arg_a1.HasAdjDiffAt_rule
   : HasAdjDiffAt K (fun x => c • g x) x :=
 by 
   have ⟨_,_⟩ := hg
-  constructor; fprop; ftrans; simp; fprop
+  constructor; fprop; ftrans; fprop
 
 
 

diff --git a/SciLean/Tactic/LSimp2/Main.lean b/SciLean/Tactic/LSimp2/Main.lean
@@ -249,34 +249,33 @@ private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
   | none => return e
 
 private partial def dsimp (e : Expr) : M Expr := do
-  return e
-  -- let cfg ← Simp.getConfig
-  -- withTraceNode `ldsimp (fun _ => pure s!"ldsimp {cfg.dsimp}") do
-  -- unless cfg.dsimp do
-  --   return e
-  -- let pre (e : Expr) : M TransformStep := do
-  --   withTraceNode `ldsimp (fun _ => pure "ldsimp pre") do
-  --   if let Step.visit r ← rewritePre e (fun _ => pure none) (rflOnly := true) then
-  --     if r.expr != e then
-  --       return .visit r.expr
-  --   return .continue
-  -- let post (e : Expr) : M TransformStep := do
-  --   withTraceNode `ldsimp (fun _ => pure "ldsimp post") do
-  --   -- lsimp modification               
-  --   -- remove unsued let bindings
-  --   let e := 
-  --     if e.isLet && ¬e.letBody!.hasLooseBVars then
-  --       e.letBody!
-  --     else
-  --       e
-  --   if let Step.visit r ← rewritePost e (fun _ => pure none) (rflOnly := true) then
-  --     if r.expr != e then
-  --       return .visit r.expr
-  --   let mut eNew ← reduce e
-  --   if cfg.zeta && eNew.isFVar then
-  --     eNew ← reduceFVar cfg eNew
-  --   if eNew != e then return .visit eNew else return .done e
-  -- transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
+  let cfg ← Simp.getConfig
+  withTraceNode `ldsimp (fun _ => pure s!"ldsimp {cfg.dsimp}") do
+  unless cfg.dsimp do
+    return e
+  let pre (e : Expr) : M TransformStep := do
+    withTraceNode `ldsimp (fun _ => pure "ldsimp pre") do
+    if let Step.visit r ← rewritePre e (fun _ => pure none) (rflOnly := true) then
+      if r.expr != e then
+        return .visit r.expr
+    return .continue
+  let post (e : Expr) : M TransformStep := do
+    withTraceNode `ldsimp (fun _ => pure "ldsimp post") do
+    -- lsimp modification               
+    -- remove unsued let bindings
+    let e := 
+      if e.isLet && ¬e.letBody!.hasLooseBVars then
+        e.letBody!
+      else
+        e
+    if let Step.visit r ← rewritePost e (fun _ => pure none) (rflOnly := true) then
+      if r.expr != e then
+        return .visit r.expr
+    let mut eNew ← reduce e
+    if cfg.zeta && eNew.isFVar then
+      eNew ← reduceFVar cfg eNew
+    if eNew != e then return .visit eNew else return .done e
+  transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
 
 instance : Inhabited (M α) where
   default := fun _ _ _ => default
@@ -468,7 +467,7 @@ where
           let r ← mkEqTrans r r'
           -- lsimp modification
           -- clean up expressions after rewrites
-          let r ← mkEqTrans r { expr := ← dsimp r.expr }
+          let r ← mkEqTrans r { expr := ← reduce r.expr }
           if cfg.singlePass || init == r.expr then
             cacheResult cfg r
           else

diff --git a/test/issues/26.lean b/test/issues/26.lean
@@ -1,22 +1,15 @@
 import SciLean
 
-
 variable (a : Nat)
 
-/- expected
+/--
 info: let x := a + a;
 a + (a + x) : ℕ
 -/
-
-/--
-info: a +
-  let x := a + a;
-  a + x : ℕ
--/
 #guard_msgs in
 #check 
-  (a + 
-    (a + 
+  (a +
+    (a +
     let x := a + a
     x))
   rewrite_by