Persistent interactive data?

Stream: general

[Niels Voss]

Python has an interactive mode where you can do something like

>>> name = input("Enter your name: ")
Enter your name: Bob
>>> print(name)
Bob
>>> n = len(name)
>>> n
3

I'm wondering if such a thing would be possible for Lean (e.g. if we were to attach a proper non-JSON-based CLI to the Lean REPL). Suppose I wanted to create a random list and refer to it in several different #eval commands. I was wondering if there was some way to store the results of #eval in a variable.

def n : IO Nat := IO.rand 0 100
def myList : IO (List Nat) := do
  return [← IO.rand 0 100, ← IO.rand 0 100, ← IO.rand 0 100]

-- How do I store the result of the following two commands?
#eval n -- 54
#eval myList -- [18, 66, 41]

#eval /- What do I put here to refer to 54 or 66? -/

For n I can do something like

import Lean
open Lean

def n : IO Nat := IO.rand 0 100

#eval show CoreM Unit from do
  let realizationOfN ← n
  addAndCompile (.defnDecl {
    name := `m, levelParams := [], type := mkConst ``Nat,
    value := mkNatLit realizationOfN, hints := .regular 0, safety := .safe
  })

-- m is a fixed value, so it will always be the same
#eval m -- 54
#eval m -- 54

but this is not easy to do for lists. (I managed to do the same thing by using toExpr, but this seems very inefficient). And in any case, I want to be storing the actual value, not some Expr which represents it.

My mental model is that the Lean environment is basically a giant hashmap of names to Exprs + a bunch of environment extensions. So if I understand correctly, what I propose would require the realization of myList to be stored in an environment extension, not in the expression hashmap. Is this possible, and how do I do this?

My motivation for this question is just to get a better understanding of Lean as a system because I am trying to learn metaprogramming and might have to do something using this later. This is also relevant to #Computer algebra > What would interactive use of a simplifier look like?

[Malvin Gattinger]

Just to check - have you seen https://github.com/leanprover-community/repl before?

[Niels Voss]

Yes I have, but for the reasons stated above, this doesn't actually let me have persistent interactive data.

I'm essentially looking for a way to

• Create a random natural number n : Nat (or an IO.Ref)
• Define two functions f : Nat -> Nat and g : Nat -> Nat (or two functions that consume an IO.Ref)
• Call f and g on the same random natural number, in two different #eval commands

[Robin Arnez]

I have a little prototype with a special #eval command:

def f (n : Nat) : Nat :=
  n * n + 3

def g (n : Nat) : Nat :=
  n + 7

#eval_set n : Nat ← IO.rand 3 10

#eval_set a : Nat ← pure (f n)
#eval_set b : Nat ← pure (g n)

#eval_set x : Fin (n + 1) ← do
  return Fin.ofNat _ (← IO.rand 0 n)

#eval_set _a : Unit ←
  IO.println s!"{n}, {a}, {b}, {x}"

Here's the prototype (which will need to be imported as a separate file):

Prototype for #eval_set

import Lean

open Lean
structure DataEntry where
  decl : LocalDecl
  value : NonScalar

initialize dataExt : Lean.EnvExtension (Array DataEntry) ←
  registerEnvExtension (pure #[])

open Lean Parser Meta Elab Command

unsafe def getNthDataValue {α : Sort u} (data : Array DataEntry) (i : Nat) : α :=
  unsafeCast (data[i]'lcProof).value

elab tk:"#eval_set " nm:ident type:(Term.typeSpec)? " ← " code:term : command => do
  liftTermElabM do
  let dataEntries := dataExt.getState (← getEnv)
  withExistingLocalDecls (dataEntries.map (·.decl)).toList do
  let exTy : Expr ←
    if let some spec := type then
      let `(Term.typeSpec| : $ty) := spec | throwUnsupportedSyntax
      let type : Expr ← Term.elabTermEnsuringType ty (some <| .sort 1)
      pure type
    else
      let mvar ← mkFreshExprMVar (some <| .sort 1)
      pure mvar
  let actType := .app (mkConst ``TermElabM) exTy
  let act ← Term.elabTermEnsuringType code (some actType)
  Term.synthesizeSyntheticMVarsNoPostponing
  let act ← instantiateMVars act
  let actType ← instantiateMVars actType
  let exTy ← instantiateMVars exTy
  if (← Term.logUnassignedUsingErrorInfos (← getMVars act)) then throwAbortTerm
  if (← Term.logUnassignedUsingErrorInfos (← getMVars actType)) then throwAbortTerm
  let fvars := (← getLCtx).getFVars
  let lambda ← mkLambdaFVars fvars act
  let type ← mkForallFVars fvars actType
  let dataType := .app (.const ``Array [0]) (mkConst ``DataEntry)
  withLocalDeclD `data dataType fun data => do
    let mut lambda := lambda
    let mut type := type
    for i in *...fvars.size do
      let .forallE _ t b _ := type | unreachable!
      let u ← getLevel t
      let val := mkApp3 (.const ``getNthDataValue [u]) t data (toExpr i)
      lambda := .app lambda val
      type := b.instantiate1 val
    let name ← mkAuxDeclName `eval_set
    addAndCompile <| .defnDecl {
      name := name
      levelParams := []
      type := ← mkForallFVars #[data] type
      value := ← mkLambdaFVars #[data] lambda
      hints := .opaque
      safety := .unsafe
    }
    let res : Array DataEntry → TermElabM NonScalar ← unsafe evalConst _ name
    let val ← withRef tk <| res dataEntries
    withLocalDeclD nm.getId exTy fun value => do
      let decl ← value.fvarId!.getDecl
      Term.addTermInfo' nm value
      modifyEnv (dataExt.modifyState · fun entries => entries.push ⟨decl, val⟩)

[Niels Voss]

Woah, this is pretty cool. I'm having a bit of difficulty understanding what it actually does though. Is my understanding correct that:

1. It registers an environment extension, which contains a list of definitions and associated values. (Don't we want this to only contain cdecls and not ldecls?) I'm not familiar with the initialize command; do you know where it is documented?
2. It uses withExistingLocalDecls to add the types of everything registered previously using #eval_set to the local context. Then it elaborates the type and term within this context.
3. It then abstracts away all the custom variables, so e.g. in this example a becomes fun n => pure (f n) of type forall n, Nat, and b becomes fun n a => pure (g n) of type forall n a, Nat.
4. fun n => pure (f n) is then replaced with (fun n => pure (f n)) (getNthDataValue data 0) and fun n a => pure (g n) is replaced with (fun n a => pure (g n)) (getNthDataValue data 0) (getNthDataValue data 1), where data is a free variable of type Array DataEntry. During this process, one level of forall is also peeled off of the type and substituted like a beta-reduction.
5. A new unsafe auxillary declaration is created and compiled, with e.g. value fun data : Array DataEntry => (fun n => pure (f n)) (getNthDataValue data 0)
6. This is evaluated somehow? I don't really understand the let res line.
7. Somehow the new value is appended to the environment extension?

[Chris Henson]

The reference manual has some docs about initialization.

[Robin Arnez]

Yes, pretty much.
For 1.: Yes, we only want cdecls but LocalDecl is the most convenient way to store them.
For 3.: Of type forall n, TermElabM Nat but otherwise yes
For 6.: We end up with a declaration Array DataEntry → TermElabM ... after all these steps. Using the interpreter we can evaluate this into an actual function Array DataEntry → TermElabM .... The ... bothers us here but we can sneakily cast into NonScalar without anyone noticing!
For 7.: After we evaluate the constant and run the code with res dataEntries we end up with the result of the computation in val (here as a NonScalar but that's just a placeholder for "any type"). Then we create our cdecl and add it together with the value to the list of entries in the environment extension.