Is there a way to convert `MetaM String` to `IO String`?

Stream: general

[Zihao Zhang]

Is there a way to convert MetaM String to IO String?

[Zihao Zhang]

import TrainingData.Frontend
import TrainingData.InfoTree.ToJson
import Mathlib.Data.String.Defs
import Mathlib.Lean.CoreM
import Batteries.Data.String.Basic
import Cli

open Lean Elab IO Meta Tactic Term
open Cli System

def fun1 : MetaM String := do
  return "hello"

def fun2 : IO String := do
  return fun1

Like this, how to solve the error?

[Damiano Testa]

There is a monad map in the mathlib4 wiki page: I'm on mobile and find it hard to give a link, though.

[Damiano Testa]

There you can probably find a path of lift and run that might take you from one monad to the other.

[Zihao Zhang]

This? https://github.com/leanprover-community/mathlib4/wiki/Monad-map

[Damiano Testa]

Yes, that's what I had in mind!

[Zihao Zhang]

@Damiano Testa It is still difficult for me :joy:

[Paul Lezeau]

This topic was also discussed here: #lean4 > MetaM String -> IO String

[Paul Lezeau]

One way of doing this would be to use docs#Lean.Meta.MetaM.toIO

[Adam Topaz]

Using Meta.toIO probably won’t get you far because you need the core state and context. I suggest using withImports… as mentioned in the discussion in the first link Paul mentioned.

[Zihao Zhang]

@Paul Lezeau @Adam Topaz It is solved, thank you!

import TrainingData.Frontend
import TrainingData.InfoTree.ToJson
import Mathlib.Data.String.Defs
import Mathlib.Lean.CoreM
import Batteries.Data.String.Basic
import Cli

open Lean Elab IO Meta Tactic Term
open Cli System
def foo (m : MetaM α) : IO α := CoreM.withImportModules #[`Mathlib] <| m.run'

-- #eval foo <| show MetaM Unit from do
--   let env ← getEnv
--   println! env.constants.toList.length

def fun1 : MetaM String := do
  return "hello"

def fun2 : IO String := do
  let s ← foo fun1
  return s

[Notification Bot]

Zihao Zhang has marked this topic as resolved.

[Notification Bot]

Zihao Zhang has marked this topic as unresolved.

[Zihao Zhang]

@Paul Lezeau @Adam Topaz By the way, Is there a way to convert TacticM String to IO String?

[Paul Lezeau]

As Kyle mentionned in the other thread, there are ways to run TacticM from within MetaM, but it’s possible those aren’t exactly what you’re looking for - would you mind saying a little more about what you’re trying to do?