Code generation

Stream: lean4

[Calvin Lee]

Would there be any easy way to generate a lot of constants automatically at once with random values?

[Mario Carneiro]

In lean 3 you can do that by calling add_decl to create new definitions, where the definition is a random value turned into a literal expression

[Mario Carneiro]

Here's some code that should work, and currently works in the command line but crashes the server for me:

import Lean

open Lean

def test : CoreM Unit := do
  let decl := Declaration.defnDecl {
    name        := `foo,
    levelParams := [],
    value       := toExpr (← IO.rand 0 100),
    type        := mkConst ``Nat,
    hints       := ReducibilityHints.regular 0,
    safety      := DefinitionSafety.safe
  }
  match (← getEnv).addAndCompile {} decl with
  | Except.ok    env => setEnv env
  | Except.error kex => pure ()

#eval test

#print foo
-- def foo : Nat :=
-- 77

[Calvin Lee]

Hmm, is there any way to do this without the #eval?

[Leonardo de Moura]

Here is an example using the macro system.

/- Helper syntax for defining the real macro. -/
syntax "gen_random_defs%" ident num num num : command

/-
`gen_random_defs id n s` creates `n` declarations of the form
``
def id_<idx> : Nat := <random value>
``
The "random values" are generated using the function `stdNext` and "seed" `s`
-/
macro "gen_random_defs" id:ident n:num s:num : command =>
  `(gen_random_defs% $id $n $s 1) -- s and 1 are the "seeds" for the random number generator

macro_rules
  | `(gen_random_defs% $id $n $s1 $s2) =>
    open Lean in
      let (val, ⟨s1, s2⟩) := stdNext ⟨s1.toNat, s2.toNat⟩
      let n      := n.toNat
      let currId := id.getId.appendIndexAfter n
      if n == 0 then
        return mkNullNode
      else
        `(def $(mkIdentFrom id currId) := $(quote val)
          gen_random_defs% $id $(quote (n-1)) $(quote s1) $(quote s2))

gen_random_defs foo 4 10 -- Creates `foo_1` ... `foo_4` using random seed 10

#print foo_1
#print foo_2
#print foo_3
#print foo_4

[Calvin Lee]

Is there any way to access IO in term or command macros in order to get rid of the seed argument here? I'm trying to write something like

/- `rand_nat_const` creates a random `Nat` in the StdGen range -/
macro "rand_nat_const" : term => do
  `($(quote (<-(IO.rand (stdRange.fst) (stdRange.snd)))))

but it seems I can only use the reader monad here

[Mario Carneiro]

It looks like no

[Mario Carneiro]

macros live in the MacroM monad which is pure

[Mario Carneiro]

Although you might not need it since MacroM implements MonadRef

[Calvin Lee]

I see, if I have : command does it live in CommandM instead? and does that include IO?

[Mario Carneiro]

No, all macros live in MacroM

[Mario Carneiro]

but that just means that it is pure during macro expansion, you can just do your computation after macro expansion

[Calvin Lee]

Indeed
the issue is I would like to avoid the randomness on runtime

[Mario Carneiro]

I'm not sure what you mean. It's the same either way

[Mario Carneiro]

It's not really clear what counts as "runtime" here

[Mario Carneiro]

If you have a command-like that adds definitions to the environment, that will run when the lean file is processed. The olean files will contain the resulting definitions

[Mario Carneiro]

if this is then used in a dependent lean file, it will be as if you wrote all those definitions, so I guess it's "compile time"?

[Mario Carneiro]

That said, a lean file that elaborates differently depending on the phase of the moon seems like a bad idea

[Calvin Lee]

indeed but it's awfully convenient for this case where I want an algorithm to have some random parameters (for efficiency reasons) but I don't want it to be random on runtime (I don't want one of my runs to get some bad seed)
Also it's nice because I don't have to worry about threading a reader through everything, especially if I want to prove things about this (which I want to be immutable)