Zulip Chat Archive

Stream: lean4

Topic: Code generation


view this post on Zulip Calvin Lee (Mar 11 2021 at 01:25):

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

view this post on Zulip Mario Carneiro (Mar 11 2021 at 05:55):

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

view this post on Zulip Mario Carneiro (Mar 11 2021 at 06:12):

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

view this post on Zulip Calvin Lee (Mar 11 2021 at 22:26):

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

view this post on Zulip Leonardo de Moura (Mar 11 2021 at 22:52):

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

view this post on Zulip Calvin Lee (Mar 17 2021 at 20:40):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:05):

It looks like no

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:05):

macros live in the MacroM monad which is pure

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:10):

Although you might not need it since MacroM implements MonadRef

view this post on Zulip Calvin Lee (Mar 17 2021 at 21:10):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:11):

No, all macros live in MacroM

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:12):

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

view this post on Zulip Calvin Lee (Mar 17 2021 at 21:14):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:14):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:16):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:17):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:17):

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"?

view this post on Zulip Mario Carneiro (Mar 17 2021 at 21:18):

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

view this post on Zulip Calvin Lee (Mar 17 2021 at 21:36):

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)


Last updated: May 18 2021 at 22:15 UTC