Zulip Chat Archive

Stream: lean4

Topic: CommitIfNoEx not reversing all side effects?

Jeremy Salwen (May 13 2023 at 16:59):

I know that this is not a MWE, but I just want to understand if this behavior of commitIfNoEx. This is the structure of my command:

elab "#markSimpLemmas" : command => Elab.Command.liftTermElabM do
  let allSimpDecls ← getAllSimpDecls `simp
  for lem in allSimpDecls do
    try
      if ... then
        -- Do something
      else
        commitIfNoEx do
          -- Do something else
          logInfo "WTF"
    catch _ =>
      if lem == ``Array.map_data then
        logInfo "Crashed"
      continue

When I run it, it logs "Crashed", but never logs "WTF", because the commitIfNoEx gets rolled back every time it is executed. This is normal.

HOWEVER, if I remove the commitIfNoEx block, then it no longer prints out "Crashed". To me this seems like the commitIfNoEx block is having side effects, despite always being rolled back. Is this a bug, or is commitIfNoEx not as powerful as I expected?

Kyle Miller (May 13 2023 at 17:06):

When you say "remove the commitIfNoEx block, you mean just that you remove commitIfNoEx, right?

The definition is pretty simple:

def commitIfNoEx [Monad m] [MonadBacktrack s m] [MonadExcept ε m] (x : m α) : m α := do
  let s ← saveState
  try
    x
  catch ex =>
    restoreState s
    throw ex

The only way you could see crashed is if x throws an exception, so I want to be sure you're still throwing the exception in your test!

Kyle Miller (May 13 2023 at 17:07):

Something you could also do is try using dbg_trace instead of logInfo to see messages immediately without worrying about what state is being restored or not

Jeremy Salwen (May 13 2023 at 17:19):

Kyle Miller said:

When you say "remove the commitIfNoEx block, you mean just that you remove commitIfNoEx, right?

The definition is pretty simple:

def commitIfNoEx [Monad m] [MonadBacktrack s m] [MonadExcept ε m] (x : m α) : m α := do
  let s ← saveState
  try
    x
  catch ex =>
    restoreState s
    throw ex

The only way you could see crashed is if x throws an exception, so I want to be sure you're still throwing the exception in your test!

No, see that's what's weird, when I remove the whole block, it doesn't log "Crashed":

elab "#markSimpLemmas" : command => Elab.Command.liftTermElabM do
  let allSimpDecls ← getAllSimpDecls `simp
  for lem in allSimpDecls do
    try
      if ... then
        -- Do something
    catch _ =>
      if lem == ``Array.map_data then
        logInfo "Crashed"
      continue

Kyle Miller (May 13 2023 at 17:21):

What's -- Do something else then? It must be throwing an exception

Jeremy Salwen (May 13 2023 at 17:22):

Yes, I think it is throwing an exception, but the exception should have no side effect, right?

Kyle Miller (May 13 2023 at 17:22):

You can see from the code that if the block in commitIfNoEx throws an exception then that exception will be re-thrown

Jeremy Salwen (May 13 2023 at 17:22):

Ohh, I see, it is rethrowing

Jeremy Salwen (May 13 2023 at 17:23):

ahh, so I need to wrap it in try catch to really make it have zero side effects.

Kyle Miller (May 13 2023 at 17:23):

It's worth skimming through the file that defines commitIfNoEx to see if there's anything in there that gives you what you want

Notification Bot (May 13 2023 at 17:23):

Jeremy Salwen has marked this topic as resolved.

Jeremy Salwen (May 13 2023 at 17:24):

withoutModifyingState Seems to be what I was looking for.

Kyle Miller (May 13 2023 at 17:24):

(I always have tor re-read the source for these functions to remember what they do exactly!)

Jeremy Salwen (May 13 2023 at 17:24):

Wait, not quite, as it won't ever commit.

Kyle Miller (May 13 2023 at 17:25):

I frequently use observing? for committing and also not throwing an exception on failure.

Jeremy Salwen (May 13 2023 at 17:26):

Yeah, that seems to be equivalent to commitIfNoEx that doesn't throw.

Notification Bot (May 13 2023 at 17:30):

Jeremy Salwen has marked this topic as unresolved.

Kyle Miller (May 13 2023 at 17:30):

Sometimes it also turns out to be easier to manage the state yourself, so don't be afraid to use saveState/restoreState and try/catch(/finally)

Jeremy Salwen (May 13 2023 at 17:32):

Hmm, realizing that I didn't actually include all of the relevant details. Theif condition should rule out the if condition in the catch from triggering:

elab "#markSimpLemmas" : command => Elab.Command.liftTermElabM do
  let allSimpDecls ← getAllSimpDecls `simp

  for lem in allSimpDecls do
    try
      if lem == ``Array.map_data ||  lem == ``Array.append_data ||  lem == ``Array.data_pop ||  lem == ``Array.pop_data ||  lem == ``Array.data_set ||  lem == ``Array.toListAppend_eq ||  lem == ``Array.appendList_data then
        -- Do something
      else
        commitIfNoEx do
          -- Do something else
          logInfo "WTF"
    catch _ =>
      if lem == ``Array.map_data then
        logInfo "Crashed"
      continue

Again, If I remove the else branch, Crashed no longer prints.

Jeremy Salwen (May 13 2023 at 17:35):

I'm going to try rewriting it without the commitIfNoEx to see if I can get a better understanding.

Kyle Miller (May 13 2023 at 17:36):

If you just delete commitIfNoEx but leave the do block, does it still do the same thing?

Jeremy Salwen (May 13 2023 at 17:38):

yes, in fact WTF is not printed out?

Jeremy Salwen (May 13 2023 at 17:40):

(The reason I came up with this code was to try to isolate the effects of the commitIfNoEx's that were succeeding from the ones that were failing, so I expect the else block to always throw an exception.)

Jeremy Salwen (May 13 2023 at 17:48):

Ok, an even more clear example using observing?:

elab "#markSimpLemmas" : command => Elab.Command.liftTermElabM do
  let allSimpDecls ← getAllSimpDecls `simp

  for lem in allSimpDecls do
    try
      if ... now irrelevant again... then
        -- Do something
      else
        let b := ← observing? do
          -- Do something else
        if b.isSome then
          logInfo "Committed"
    catch _ =>
      if lem == ``Array.map_data then
        logInfo "Crashed"
      continue

It will never log "Committed", but removing the else block changes whether "Crashed" is logged.

Kyle Miller (May 13 2023 at 17:52):

Can you give a #mwe? It doesn't have to be minimal -- it's just hard to say anything without seeing (and maybe testing out) some working code.

Jeremy Salwen (May 13 2023 at 17:59):

Ok, apologies for the code dump:

import Lean
import Std.Data.Array.Init.Lemmas
import Std.Data.Array.Lemmas
import Mathlib.Tactic.Find
import Mathlib.Tactic.Simps.Basic
import Lean.Elab.Term

open Lean Meta Elab Term Lean.Meta Tactic

def transformEtaReduce (e : Expr) : MetaM Expr := do
  transform e fun node => pure <| TransformStep.continue node.etaExpanded?

def betaReduceHead (e:Expr): Expr :=
  if e.isHeadBetaTarget then e.headBeta else e

lemma List.toArray_data (a:Array α): (List.toArray a.data) = a := sorry

lemma Array.ext_iff' (a: Array α) (b:Array α):  a = b ↔ a.data = b.data  := sorry


def lhsSimp (e : Expr) : MetaM Simp.Result :=
  simpOnlyNames [``Array.data_toArray, ``List.toArray_data, ``funext, ``funext₂, ``funext₃] e
    (config := { decide := false })

def onlySimp (e:Expr): MetaM Simp.Result :=
    simpOnlyNames [] e
    (config := { decide := false })

-- The same as in mathlib addRelatedDef, except we don't look up the defintion,
-- but pass a const to the construct function.  Also we don't apply attrs to source definition :D
def addRelatedThm (src : Name) (suffix : String) (ref : Syntax)
    (attrs? : Option (Syntax.TSepArray `Lean.Parser.Term.attrInstance ","))
    (construct : Expr → Expr → List Name → MetaM (Expr × List Name)) :
    MetaM Unit := do
  let tgt := match src with
    | Name.str n s => Name.mkStr n $ s ++ suffix
    | x => x
  addDeclarationRanges tgt {
    range := ← getDeclarationRange (← getRef)
    selectionRange := ← getDeclarationRange ref }
  let info ← getConstInfo src
  let (newValue, newLevels) ← construct info.type (← mkConstWithLevelParams @src) info.levelParams
  let newValue ← instantiateMVars newValue
  let newType ← instantiateMVars (← inferType newValue)
  match info with
  | ConstantInfo.thmInfo info =>
    addAndCompile <| .thmDecl
      { info with levelParams := newLevels, type := newType, name := tgt, value := newValue }
  | ConstantInfo.defnInfo info =>
    -- Structure fields are created using `def`, even when they are propositional,
    -- so we don't rely on this to decided whether we should be constructing a `theorem` or a `def`.
    addAndCompile <| if ← isProp newType then .thmDecl
      { info with levelParams := newLevels, type := newType, name := tgt, value := newValue }
      else .defnDecl
      { info with levelParams := newLevels, type := newType, name := tgt, value := newValue }
  | _ => throwError "Constant {src} is not a theorem or definition."
  if isProtected (← getEnv) src then
    setEnv $ addProtected (← getEnv) tgt
  let attrs := match attrs? with | some attrs => attrs | none => #[]
  _ ← Term.TermElabM.run' <| do
    let attrs ← elabAttrs attrs
    Term.applyAttributes tgt attrs


def upLemmaAttrs : MetaM (Syntax.TSepArray `Lean.Parser.Term.attrInstance ",") := do
  let arr : Syntax.TSepArray `Lean.Parser.Term.attrInstance "," := ∅
  return arr


def countFnsFromTypeAux (e : Expr) (ty: Expr) (exclude: List Name) : StateT ℕ MetaM Unit := do
  e.forEach fun subExpr => do
    match subExpr.getAppFnArgs with
    | (f, args ) =>
      if f ∉ exclude then
        args.forM (λ arg => do
          let (mvars, _, _) ← forallMetaTelescope (← inferType ty)
          if ← withoutModifyingEnv (isDefEq (mkAppN ty mvars) (← inferType arg)) then
            modify Nat.succ
        )

def countFnCallsAux (e : Expr) (fns: List Name) : StateT ℕ MetaM Unit := do
  e.forEach fun subExpr => do
    match subExpr.getAppFnArgs with
    | (f, _) =>
      if f ∈  fns then
        modify Nat.succ

def countFnsFromType(e: Expr) (ty: Expr) (exclude: List Name) : MetaM ℕ  := do
  let initialState := 0
  let (_, finalState) ← (countFnsFromTypeAux e ty exclude).run initialState
  return finalState

def countFnCalls (e : Expr) (fns: List Name) : MetaM ℕ := do
  let initialState := 0
  let (_, finalState) ← (countFnCallsAux e fns).run initialState
  return finalState

def fillImplicitArgsWithMVars (e: Expr): MetaM Expr := do
  forallTelescope (← inferType e) (fun xs _ => do
    let mut result := e
    for x in xs do
      if ¬ (← x.fvarId!.getBinderInfo).isExplicit then
        result := mkApp result (← mkFreshExprMVar (← x.fvarId!.getType))
    pure result
  )

def upLemma (srcType: Name) (f:Name) (r: Name) (lem: Name) : MetaM Unit := do
  addRelatedThm lem "_up" (← getRef) (← upLemmaAttrs)
    fun t value levels => do
      let transformed ←  forallTelescope t (fun xs ty => do
        match ty.getAppFnArgs with
          | (``Eq, #[α, lhs, rhs]) => do
            if (← countFnsFromType lhs (← mkConst' srcType) [f]) > (← countFnsFromType rhs (← mkConst' srcType) [f]) && (← countFnCalls ty [f]) > 0 then
              let mut e := (mkAppN value xs)
              if lhs.isAppOf f then
                let r ← fillImplicitArgsWithMVars (← mkConst' r)
                if (← isDefEq (← inferType r) (← mkArrow α (← mkFreshTypeMVar))) then
                  e ← mkCongrArg r e
                  e ← simpType lhsSimp e

              for x in xs.reverse do
                e ← mkLambdaFVars #[x] e
                if (← x.fvarId!.getBinderInfo).isExplicit then
                  e ← mkFunExt e

              e ← transformEtaReduce e
              e ← simpType onlySimp e
              pure e
            else
              throwError "Does not reduce operations on the source type: {(← countFnsFromType lhs (← mkConst' ``Array) [f])} {← countFnsFromType rhs (← mkConst' ``Array) [f]}"
          | _ => throwError "Can only handle hypotheses of the form `a = b`"
      )
      pure (transformed, levels)

elab "#upLemma" srcType:ident " x " f:ident " x " r:ident " x " e:ident: command => Elab.Command.liftTermElabM do
  upLemma srcType.getId f.getId r.getId e.getId

elab "#markSimpLemmas" : command => Elab.Command.liftTermElabM do
  Term.applyAttributes ``List.toArray_data (← elabAttrs (← upLemmaAttrs))
  Term.applyAttributes ``Array.data_toArray (← elabAttrs (← upLemmaAttrs))
  Term.applyAttributes ``Array.ext_iff' (← elabAttrs (← upLemmaAttrs))
  let allSimpDecls ← getAllSimpDecls `simp

  for lem in allSimpDecls do
    try
      if lem == ``Array.map_data ||  lem == ``Array.append_data ||  lem == ``Array.data_pop ||  lem == ``Array.pop_data ||  lem == ``Array.data_set ||  lem == ``Array.toListAppend_eq ||  lem == ``Array.appendList_data then
        logInfo "FOUNDIT"
        commitIfNoEx do
          upLemma ``Array ``Array.data ``List.toArray lem
          logInfo lem
      else
        let b := ← observing? do
          upLemma ``Array ``Array.data ``List.toArray lem
          logInfo "WTF"
          logInfo lem
        if b.isSome then
          logInfo "Committed"
    catch _ =>
      if lem == ``Array.map_data then
        logInfo "Ded"
      continue

#markSimpLemmas

Jeremy Salwen (May 13 2023 at 18:09):

Trying to implement it with nested try/catch for an even clearer example, but the syntax doesn't seem to allow nesting try/catch.

Kyle Miller (May 13 2023 at 18:09):

I'm seeing a panic at #markSimpLemmas. If there's a panic, then I'm not sure we can really reason about the code.

Kyle Miller (May 13 2023 at 18:10):

PANIC at Lean.MapDeclarationExtension.insert Lean.Environment:594:2: assertion violation: env.getModuleIdxFor? declName |>.isNone -- See comment at MapDeclarationExtension

Jeremy Salwen (May 13 2023 at 18:10):

How are you seeing a panic? Like in the info bar?

Jeremy Salwen (May 13 2023 at 18:10):

OOOH there is a message in the output window.

Kyle Miller (May 13 2023 at 18:10):

I get a popup in the lower right corner of VS Code, and it also shows up in stderr

Jeremy Salwen (May 13 2023 at 18:14):

Ok, so what is happening is I am panicking inside the CommitIfNoEx, but it is "recovering" from the panic and continuing to execute, despite it not actually undoing the side-effects of the panic?

Kyle Miller (May 13 2023 at 18:15):

Panics are not recoverable

Kyle Miller (May 13 2023 at 18:16):

They're not exceptions -- they're sort of a special Inhabited.default that prints out an error message

Jeremy Salwen (May 13 2023 at 18:16):

But my code continues to execute, and more messages appear on the info bar, after the panic?

Kyle Miller (May 13 2023 at 18:17):

Yes, they don't halt execution, just like Inhabited.default doesn't

Kyle Miller (May 13 2023 at 18:18):

It might not be the cause of your errors, but it's definitely worth looking into. Here's where the panic is coming from: https://github.com/leanprover/lean4/blob/445fd417be4df8f69f1b97b5426bd5ef97d28138/src/Lean/Environment.lean#L592

Henrik Böving (May 13 2023 at 18:19):

You can make them halt execution by setting LEAN_PANIC=abort in your environment variables

Jeremy Salwen (May 13 2023 at 18:30):

Ok, thanks. Maybe I think this because I was just bitten, but this does seem like an area where the UI could be improved. It's really not clear based on the log message in the "Output" tab (which is usually hidden since it contains no information) that all other information displayed to the user (in the Lean InfoView, the Problems window, and the editor itself) is invalid. It is also not clear if a panic is currently affecting what is displayed, vs just something which happened in the past, and is no longer affecting the validity of the information displayed.

Jeremy Salwen (May 13 2023 at 18:35):

Hmm LEAN_ABORT_ON_PANIC=1 seems to just kill the server entirely, rather than just stopping the execution of the current code.

Henrik Böving (May 13 2023 at 18:38):

That is expected behaviour yes

Henrik Böving (May 13 2023 at 18:38):

The Server is a Lean process, it will simply jump to the bytecode interpreter upon meeting a #eval, if you now panic within that section of code the process gets killed so you of course never end up returning to the server code.

Henrik Böving (May 13 2023 at 18:40):

There does of course exist a solution here which would be forking and having some IPC between the server and the execution unit, I do not know why it is not done like this though.

Jeremy Salwen (May 13 2023 at 18:44):

So if the server panics, and then I delete all my code, is the server still potentially in an invalid state due to the panic?

Henrik Böving (May 13 2023 at 18:45):

The server process for your file is dead, it does not exist anymore. What you can do is comment out the eval statement that murdered it and tell it to reload the file, in emacs that would be via C-c C-d

Jeremy Salwen (May 13 2023 at 18:47):

Sorry, I mean if I don't have LEAN_ABORT_ON_PANIC=1.

Henrik Böving (May 13 2023 at 18:52):

Well then the same thing applies really^^

Jeremy Salwen (May 13 2023 at 19:41):

Hmm, I'm not sure I understand. When I don't have LEAN_ABORT_ON_PANIC=1, the server process for the file does not die when it encounters the panic, instead it continues to process my lean code, and continues to generate messages for the lean infoview, which it then sends to VS Code.

If I delete the code which caused the panic, and write fresh code in the same file, does that same server still remain in an invalid state, where it will process my new code, and update the lean infoview, but its internal state is corrupted, such that I cannot trust the output any more?

Henrik Böving (May 13 2023 at 19:43):

Right, sorry that was expressed wrongly by me: Yes the server should not die, generally speaking the procedure above helps for "my server is in a weird state what can I do"

if you do nnot have abort on panic on the server state should remain perfectly fine at all times.

Mario Carneiro (May 13 2023 at 19:44):

unless your panicked code pollutes lean's state, of course

Max Nowak 🐉 (May 15 2023 at 10:14):

Semantically a panic just returns the default value and logs an error message. Then execution continues using that default value, which may or may not be catastrophic. But this way, panics are "sound", in a way... at least as far as I understand it.

Max Nowak 🐉 (May 15 2023 at 10:15):

example: (panic! "" : Nat) = 0 := by simp

Jeremy Salwen (May 17 2023 at 05:32):

Would it be technically simple to either

  1. Stop execution of user code on a panic
  2. Stop sending new messages and errors to the lean infoview on a panic
  3. Send a special message to the lean infoview on a panic

and would you accept a PR that does one of the above?

Mario Carneiro (May 17 2023 at 05:33):

no, all three of those are not technically simple

Jeremy Salwen (May 17 2023 at 05:40):

I see, is there a clear connection between the panic and a particular piece of code, or is it more like you have to look at stderr, and try to match it up based on the timing?

Mario Carneiro (May 17 2023 at 05:41):

the panic is not an effect as far as lean is concerned, which makes it difficult for the server to know that it has happened

Mario Carneiro (May 17 2023 at 05:42):

You might be able to look at stderr (if you captured it), but you wouldn't be able to distinguish it from other stderr printouts that are not about panicking

Mario Carneiro (May 17 2023 at 05:55):

Here's a demonstration:

#eval show IO Unit from do
  let bOut ← IO.mkRef {}
  IO.withStderr (IO.FS.Stream.ofBuffer bOut) <| do
    println! (panic! s!"{← (← IO.mkRef 1).get}" : Nat)
  println! "isEmpty: {(← bOut.get).data.isEmpty}"

It appears that even if you capture stderr, there is still nothing the surrounding lean code can do to observe that a panic has happened

Jeremy Salwen (May 17 2023 at 06:00):

yeah I am just thinking about how to make it clear the distinction between a valid state and an invalid state.

Mario Carneiro (May 17 2023 at 06:00):

I'm not saying that it wouldn't be nice to be able to do better, I'm saying it is not technically simple

Jeremy Salwen (May 17 2023 at 06:01):

Yeah I get it :cry: . I was hoping you might have a creative idea of how to get that information.

Mario Carneiro (May 17 2023 at 06:02):

you would need to modify the C++ code (probably the interpreter or the runtime) to log panics somewhere

Jeremy Salwen (May 18 2023 at 15:57):

So, I've got some bad news. I have fixed the panic, but it seems like the same issue is present. withoutModifyingState seems to definitely be modifying the state. Again, removing the else changes whether "Crashed" is print, despite it entirely being inside "withoutModifyingState"

import Lean
import Std.Data.Array.Init.Lemmas
import Std.Data.Array.Lemmas
import Mathlib.Tactic.Find
import Mathlib.Tactic.Simps.Basic
import Lean.Elab.Term

open Lean Meta Elab Term Lean.Meta Tactic

def transformEtaReduce (e : Expr) : MetaM Expr := do
  transform e fun node => pure <| TransformStep.continue node.etaExpanded?

syntax "eta_reduce" (ppSpace Parser.Tactic.location)? : tactic

elab_rules : tactic
  | `(tactic| eta_reduce $[$loc?]?) =>
  withLocation (expandOptLocation (Lean.mkOptionalNode loc?))
    (atLocal := fun h => liftMetaTactic1 fun mvarId => do
      let ty ← instantiateMVars (← h.getType)
      mvarId.changeLocalDecl' h (← transformEtaReduce ty))
    (atTarget := liftMetaTactic1 fun mvarId => do
      let ty ← instantiateMVars (← mvarId.getType)
      mvarId.change (← transformEtaReduce ty))
    (failed := fun _ => throwError "eta_reduce failed")


lemma List.toArray_data (a:Array α): (List.toArray a.data) = a := sorry

lemma Array.ext_iff' (a: Array α) (b:Array α):  a = b ↔ a.data = b.data  := sorry


def lhsSimp (e : Expr) : MetaM Simp.Result :=
  simpOnlyNames [``Array.data_toArray, ``List.toArray_data, ``funext, ``funext₂, ``funext₃] e
    (config := { decide := false })

def onlySimp (e:Expr): MetaM Simp.Result :=
    simpOnlyNames [] e
    (config := { decide := false })

-- The same as in mathlib addRelatedDef, except we don't look up the defintion,
-- but pass a const to the construct function.  Also we don't apply attrs to source definition :D
def addRelatedThm (src : Name) (suffix : String) (ref : Syntax)
    (attrs? : Option (Syntax.TSepArray `Lean.Parser.Term.attrInstance ","))
    (construct : Expr → Expr → List Name → MetaM (Expr × List Name)) :
    MetaM Unit := do
  let tgt := match src with
    | Name.str n s =>
      Name.mkStr n $ s ++ suffix
    | x =>
      .str x suffix

  addDeclarationRanges tgt {
    range := ← getDeclarationRange (← getRef)
    selectionRange := ← getDeclarationRange ref }
  let info ← getConstInfo src
  let (newValue, newLevels) ← construct info.type (← mkConstWithLevelParams @src) info.levelParams
  let newValue ← instantiateMVars newValue
  let newType ← instantiateMVars (← inferType newValue)
  match info with
  | ConstantInfo.thmInfo info =>
    addAndCompile <| .thmDecl
      { info with levelParams := newLevels, type := newType, name := tgt, value := newValue }
  | ConstantInfo.defnInfo info =>
    -- Structure fields are created using `def`, even when they are propositional,
    -- so we don't rely on this to decided whether we should be constructing a `theorem` or a `def`.
    addAndCompile <| if ← isProp newType then .thmDecl
      { info with levelParams := newLevels, type := newType, name := tgt, value := newValue }
      else .defnDecl
      { info with levelParams := newLevels, type := newType, name := tgt, value := newValue }
  | _ => throwError "Constant {src} is not a theorem or definition."
  if isProtected (← getEnv) src then
    setEnv $ addProtected (← getEnv) tgt
  let attrs := match attrs? with | some attrs => attrs | none => #[]
  _ ← Term.TermElabM.run' <| do
    let attrs ← elabAttrs attrs
    Term.applyAttributes tgt attrs


def upLemmaAttrs : MetaM (Syntax.TSepArray `Lean.Parser.Term.attrInstance ",") := do
  let arr : Syntax.TSepArray `Lean.Parser.Term.attrInstance "," := ∅
  return arr


def countFnsFromTypeAux (e : Expr) (ty: Expr) (exclude: List Name) : StateT ℕ MetaM Unit := do
  e.forEach fun subExpr => do
    match subExpr.getAppFnArgs with
    | (f, args ) =>
      if f ∉ exclude then
        args.forM (λ arg => do
          let (mvars, _, _) ← forallMetaTelescope (← inferType ty)
          if ← withoutModifyingEnv (isDefEq (mkAppN ty mvars) (← inferType arg)) then
            modify Nat.succ
        )

def countFnCallsAux (e : Expr) (fns: List Name) : StateT ℕ MetaM Unit := do
  e.forEach fun subExpr => do
    match subExpr.getAppFnArgs with
    | (f, _) =>
      if f ∈  fns then
        modify Nat.succ

def countFnsFromType(e: Expr) (ty: Expr) (exclude: List Name) : MetaM ℕ  := do
  let initialState := 0
  let (_, finalState) ← (countFnsFromTypeAux e ty exclude).run initialState
  return finalState

def countFnCalls (e : Expr) (fns: List Name) : MetaM ℕ := do
  let initialState := 0
  let (_, finalState) ← (countFnCallsAux e fns).run initialState
  return finalState

def fillImplicitArgsWithMVars (e: Expr): MetaM Expr := do
  forallTelescope (← inferType e) (fun xs _ => do
    let mut result := e
    for x in xs do
      if ¬ (← x.fvarId!.getBinderInfo).isExplicit then
        result := mkApp result (← mkFreshExprMVar (← x.fvarId!.getType))
    pure result
  )

def upLemma (srcType: Name) (f:Name) (r: Name) (lem: Name) : MetaM Unit := do
  addRelatedThm lem "_up" (← getRef) (← upLemmaAttrs)
    fun t value levels => do
      let transformed ←  forallTelescope t (fun xs ty => do
        match ty.getAppFnArgs with
          | (``Eq, #[α, lhs, rhs]) => do
            if (← countFnsFromType lhs (← mkConst' srcType) [f]) > (← countFnsFromType rhs (← mkConst' srcType) [f]) && (← countFnCalls ty [f]) > 0 then
              let mut e := (mkAppN value xs)
              if lhs.isAppOf f then
                let r ← fillImplicitArgsWithMVars (← mkConst' r)
                if (← isDefEq (← inferType r) (← mkArrow α (← mkFreshTypeMVar))) then
                  e ← mkCongrArg r e
                  e ← simpType lhsSimp e

              for x in xs.reverse do
                e ← mkLambdaFVars #[x] e
                if (← x.fvarId!.getBinderInfo).isExplicit then
                  e ← mkFunExt e

              e ← transformEtaReduce e
              e ← simpType onlySimp e
              pure e
            else
              throwError "Does not reduce operations on the source type: {(← countFnsFromType lhs (← mkConst' ``Array) [f])} {← countFnsFromType rhs (← mkConst' ``Array) [f]}"
          | _ => throwError "Can only handle hypotheses of the form `a = b`"
      )
      pure (transformed, levels)

elab "#upLemma" srcType:ident " x " f:ident " x " r:ident " x " e:ident: command => Elab.Command.liftTermElabM do
  upLemma srcType.getId f.getId r.getId e.getId

elab "#markSimpLemmas" : command => Elab.Command.liftTermElabM do
  Term.applyAttributes ``List.toArray_data (← elabAttrs (← upLemmaAttrs))
  Term.applyAttributes ``Array.data_toArray (← elabAttrs (← upLemmaAttrs))
  Term.applyAttributes ``Array.ext_iff' (← elabAttrs (← upLemmaAttrs))
  let allSimpDecls ← getAllSimpDecls `simp

  for lem in allSimpDecls do
    try
      if lem == ``Array.map_data ||  lem == ``Array.append_data ||  lem == ``Array.data_pop ||  lem == ``Array.pop_data ||  lem == ``Array.data_set ||  lem == ``Array.toListAppend_eq ||  lem == ``Array.appendList_data then
        commitIfNoEx do
          upLemma ``Array ``Array.data ``List.toArray lem
          logInfo lem
      else
        withoutModifyingState do
          upLemma ``Array ``Array.data ``List.toArray lem
          logInfo "WTF"
          logInfo lem
    catch _ =>
      if lem == ``Array.map_data then
        logInfo "Crashed"
      continue
  logInfo "DONE"


#markSimpLemmas

Jeremy Salwen (May 18 2023 at 22:32):

Ok, after further debugging, I found another strange behavior (or maybe the root cause?). In this case, if I remove an interpolated value from the throwError string argument (see the "DELETE AFTER THE COLON" string), then the "Crashed" is no longer printed, i.e. it seems like withoutModifyingState is actually able to do its job of preventing modification of the state.

This at least seems plausible as an area for a bug/ambiguity, since maybe the interpolation is lazily evaluated or something?

Here is the MWE:

import Lean
import Std.Data.Array.Init.Lemmas
import Std.Data.Array.Lemmas
import Mathlib.Tactic.Find
import Mathlib.Tactic.Simps.Basic
import Lean.Elab.Term

open Lean Meta Elab Term Lean.Meta Tactic

def lhsSimp (e : Expr) : MetaM Simp.Result :=
  simpOnlyNames [``funext, ``funext₂, ``funext₃] e
    (config := { decide := false })

def addRelatedThm (src : Name) (suffix : String) (ref : Syntax)
    (construct : Expr → Expr → List Name → MetaM (Expr × List Name)) :
    MetaM Unit := do
  let tgt := .str src suffix
  addDeclarationRanges tgt {
    range := ← getDeclarationRange (← getRef)
    selectionRange := ← getDeclarationRange ref }
  let info ← getConstInfo src
  let (newValue, newLevels) ← construct info.type (← mkConstWithLevelParams @src) info.levelParams
  let newValue ← instantiateMVars newValue
  let newType ← instantiateMVars (← inferType newValue)
  match info with
  | ConstantInfo.thmInfo info =>
    addAndCompile <| .thmDecl
      { info with levelParams := newLevels, type := newType, name := tgt, value := newValue }
  | _ => throwError "Constant {src} is not a theorem or definition."

def countFnsFromTypeAux (e : Expr) (ty: Expr) (exclude: List Name) : StateT ℕ MetaM Unit := do
  e.forEach fun subExpr => do
    match subExpr.getAppFnArgs with
    | (f, args ) =>
      if f ∉ exclude then
        args.forM (λ arg => do
          let (mvars, _, _) ← forallMetaTelescope (← inferType ty)
          if ← withoutModifyingEnv (isDefEq (mkAppN ty mvars) (← inferType arg)) then
            modify Nat.succ
        )

def countFnCallsAux (e : Expr) (fns: List Name) : StateT ℕ MetaM Unit := do
  e.forEach fun subExpr => do
    match subExpr.getAppFnArgs with
    | (f, _) =>
      if f ∈  fns then
        modify Nat.succ

def countFnsFromType(e: Expr) (ty: Expr) (exclude: List Name) : MetaM ℕ  := do
  let initialState := 0
  let (_, finalState) ← (countFnsFromTypeAux e ty exclude).run initialState
  return finalState

def countFnCalls (e : Expr) (fns: List Name) : MetaM ℕ := do
  let initialState := 0
  let (_, finalState) ← (countFnCallsAux e fns).run initialState
  return finalState

def fillImplicitArgsWithMVars (e: Expr): MetaM Expr := do
  forallTelescope (← inferType e) (fun xs _ => do
    let mut result := e
    for x in xs do
      if ¬ (← x.fvarId!.getBinderInfo).isExplicit then
        result := mkApp result (← mkFreshExprMVar (← x.fvarId!.getType))
    pure result
  )

def upLemma (srcType: Name) (f:Name) (r: Name) (lem: Name) : MetaM Unit := do
  addRelatedThm lem "_up" (← getRef)
    fun t value levels => do
      let transformed ←  forallTelescope t (fun xs ty => do
        match ty.getAppFnArgs with
          | (``Eq, #[α, lhs, rhs]) => do
            if (← countFnsFromType lhs (← mkConst' srcType) [f]) > (← countFnsFromType rhs (← mkConst' srcType) [f]) && (← countFnCalls ty [f]) > 0 then
              let mut e := (mkAppN value xs)
              if lhs.isAppOf f then
                let r ← fillImplicitArgsWithMVars (← mkConst' r)
                if (← isDefEq (← inferType r) (← mkArrow α (← mkFreshTypeMVar))) then
                  e ← mkCongrArg r e
                  e ← simpType lhsSimp e

              mkLambdaFVars xs e
            else
              throwError "DELETE AFTER THE COLON: {(← countFnsFromType lhs (← mkConst' ``Array) [f])} {← countFnsFromType rhs (← mkConst' ``Array) [f]}"
          | _ => throwError ""
      )
      pure (transformed, levels)

elab "#markSimpLemmas" : command => Elab.Command.liftTermElabM do
  let allSimpDecls ← getAllSimpDecls `simp

  for lem in allSimpDecls do
    try
      if lem == ``Array.map_data then
        commitIfNoEx do
          upLemma ``Array ``Array.data ``List.toArray lem
          logInfo lem
      else
        withoutModifyingState do
          upLemma ``Array ``Array.data ``List.toArray lem
          logInfo "WTF"
          logInfo lem
    catch _ =>
      if lem == ``Array.map_data then
        logError "Crashed"
      continue
  logInfo "DONE"

#markSimpLemmas

Last updated: Dec 20 2023 at 11:08 UTC