Running CommandElabM inside IO and installing instances

Stream: lean4

[Gauvain Devillez]

Hello,

I am trying to reuse a function from a command_elab which creates an instance of Cow and installs an instance of the type class Age through metaprogramming. Because I want the function to be used in main, I would like to convert the CommandElabM into IO. I can obtain the constructed instance, but the type classes are lost.

In the example below, the age function works and the Age instance is found when using the command, but the Age is not found when using the function convertCow.

I suspect it has to do with the Enviroment but could not find how to obtain the current Enviroment from IO. Is there a way?

Sorry if it is unclear.

import Lean
import Qq

open Qq Lean Elab Command

-- A structure
structure Cow where
  name : String

-- A typeclass
class Age (c : Cow) : Type :=
  age : Nat

-- Some function using the typeclass
def Cow.age (c : Cow) [b : Age c] : Nat :=
  b.age

-- Function from Mario Carneiro on zulip : https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/read.20term.20from.20file/near/400316661
-- I do not know if it will preserve the side-effects of installing the instances.
def runCommandElabM (env : Environment) (x : CommandElabM α) : IO α := do
  let cmdCtx := {
    fileName     := "<empty>"
    fileMap      := .ofString ""
    tacticCache? := none
  }
  match (← liftM <| EIO.toIO' <| (x cmdCtx).run { env, maxRecDepth := maxRecDepth.defValue }) with
  | .ok (a, _) => return a
  | .error e =>
    throw <| IO.Error.userError s!"unexpected internal error: {← e.toMessageData.toString}"

-- Function to construct a Cow and install an Age instance in metaprogramming.
unsafe def makeCowAux (ident : Name) (name : String) (age : Nat) : Elab.Command.CommandElabM Cow := do
   -- We create the Cow
   have cowQ : Q(Cow) := q({name := $name})
   Elab.Command.liftCoreM <| addAndCompile <| .defnDecl {
     name := ident
     levelParams := []
     type := q(Cow)
     value := q($cowQ)
     hints := .regular 0
     safety := .safe
   }
   setReducibleAttribute ident
   have cow : Q(Cow) := mkConst ident []

   -- We create the Age object
   have ageQ : Q(Age $cow) := q({age := $age})
   have ageName : Name := Name.mkStr ident "ageClass"
   Elab.Command.liftCoreM <| addAndCompile <| .defnDecl {
       name := ageName
       levelParams := []
       type := q(Age $cow)
       value := ageQ
       hints := .regular 0
       safety := .safe
   }
   -- We install the instance
   Elab.Command.liftTermElabM <| Meta.addInstance ageName .global 42
   -- We want the object registered under the Name
   evalConst Cow ident

-- We want to get out of CommandElabM and into IO
unsafe def convertCow (ident : String) (name : String) (age : Nat) : IO Cow := do
  -- This part might be wrong. I did not find a way to get the current environment from outside the CommandElabM monad.
  -- Also, I do not know what I should import exactly.
  let env ← importModules #[`Init] {}
  let cmdCow := makeCowAux ident name age
  runCommandElabM env cmdCow

-- We want to be able to use the function in a command
syntax (name := makeCow) "make_cow" ident str num : command

@[command_elab makeCow]
unsafe def makeCowImpl : Elab.Command.CommandElab
  | `(make_cow $ident $name $age) => do
    let _ ← makeCowAux ident.getId name.getString age.getNat
  | _ => Elab.throwUnsupportedSyntax


make_cow bessy "Bessy" 10

-- Used as a command, it works
#check bessy.ageClass
#eval bessy.age

unsafe def myFunction : IO Unit := do
  let newBessy : Cow ← convertCow "newBessy" "newBessy" 42
  IO.println newBessy.name
  -- Used in a function, the instances are missing/not found.
  IO.println newBessy.ageClass.age
  IO.println newBessy.age

[Sebastian Ullrich]

What you try to do in myFunction is not possible. You run convertCow at run time of the function but somehow expect it to influence the compile time of the function, which would be time travel. Can you say more about what you're trying to achieve?

[Sebastian Ullrich]

It may be the case that you want to move the computation convertCow "newBessy" "newBessy" 42 to compile time by introducing a term elaborator that does something very similar to makeCowAux but the context is not sufficiently clear

[Gauvain Devillez]

Thank you for the reply! I did not think about the compile time.

To give more context, we are trying to build graphs from json files along with their properties. For example, a graph and the property that it is connected. We do so using elab to have good performances (there will be tens of thousands of files).

What I want to do now is to be able to create an exe that would go through a list of json files and verify those properties for the graphs in each of them. I was hoping I would not have to duplicate the code.

[Eric Wieser]

I think you're looking for withImportModules, which starts an interpreter/compiler within your runtime