Make fields of a class evaluate only once

Stream: general

[Yuyang Zhao]

I'm trying to make something like pre-processed global constants using typeclass. But I ran into some problems

class foo /- may have some parameters -/ where
  x : Nat :=
    dbg_trace "!"
    1 -- may be some calculations
  x_def : x = 1 := by rfl
open foo

def z (n : Nat) [foo] : Nat := n + x

def bar : Nat :=
  let _ : foo := {}
  z 0 + z 1 + z 2 + z 3 + z 4

#eval bar

dbg_trace prints 5 !s, does this mean that x is evaluated 5 times? How can I make it only evaluated once?

[Yuyang Zhao]

It seems that it will only be evaluated once if not using instance parameter... I don't know what's happening

class foo /- may have some parameters -/ where
  x : Nat :=
    dbg_trace "!"
    1 -- may be some calculations
  x_def : x = 1 := by rfl
open foo

def z (n : Nat) (s : foo) : Nat := n + s.x

def bar : Nat :=
  let s : foo := {}
  z 0 s + z 1 s + z 2 s + z 3 s + z 4 s

#eval bar

[Mario Carneiro]

z is automatically specialized for instance arguments, and the specialized instance of z n ({} : foo) evaluates the dbg_trace

[Mario Carneiro]

You normally don't have to do anything special to get constants to evaluate only once, lean automatically hoists them into globals

[Mario Carneiro]

extracting dbg_trace "!"; 1 into a definition makes it evaluate only once