Working with mutable monad

Stream: lean4

[Tomas Skrivan]

I would like to have a function that replaces a subexpression, but it should be monadic so I can e.g. store the expression being replaced. However, I'm having hard time doing this using the mut notation.

My partial attempt that does not typecheck.

import Lean
open Lean

partial def replaceSubExpression {m : Type _ → Type _} [Monad m] [MonadLift m MetaM]
            (e : Expr) (test : Expr → Bool) (replace : Expr → m Expr) : MetaM Expr := do
if (test e) then
  (replace e)
else
match e with
  | Expr.app f x d => do (mkApp (← (replaceSubExpression f test replace)) (← (replaceSubExpression x test replace)))
  | Expr.lam n x b d => Expr.lam n x (← replaceSubExpression b test replace) d
  -- this is incomplete and should use lambda telescope
  | _ => e


def getfvar (e : Expr) : MetaM Expr := do
  let mut sub : Expr := arbitrary
  let replace := (λ e : Expr =>
                    do -- invalid 'do' notation, expected type is not available
                      sub := e
                      e)
  let e' : Expr ← replaceSubExpression e (λ e => e.isFVar) replace
  e'

The problem is with the definition of replace, I'm expecting I should explicitly state what monad it should use.

[Sebastian Ullrich]

You cannot use mut across lambdas. Use the state monad or an IO.Ref.

[Tomas Skrivan]

That is a shame that it cannot be used, but I will look into IO.Ref.

[Sebastian Ullrich]

In that case you don't need to change the monad, so I would remove m completely

[Tomas Skrivan]

Any example on how to use IO.Ref ?

[Tomas Skrivan]

Never mind, it looks pretty straight forward :) It does not stop to amaze me how incredibly readable the code of Lean 4 is and if things typecheck they usually work.

[Sebastian Ullrich]

Great excuse to avoid writing docs :grimacing:

[Tomas Skrivan]

I have noticed :D I know very little about formal methods, programming language design etc. but for example I was able to understand the role of local contex of an expression just from reading the Lean code and successfully use it to do some expression transformations.