Understanding evalConst in aesop tacgen

Stream: general

[Frederick Pu]

I'm having trouble understanding what evalConst is actually doing in tacGenImpl

-- Precondition: `decl` has type `TacGen`.
unsafe def tacGenImpl (decl : Name) : RuleTac := λ input => do
  let tacGen ← evalConst TacGen decl
  let initialState ← saveState
  let suggestions ← tacGen input.goal
  let mut apps := Array.mkEmpty suggestions.size
  ...

[Aaron Liu]

It's getting the TacGen from an name.

[Frederick Pu]

so does it run a compiler on the string?

[Aaron Liu]

It looks up the definition and evaluates it. Use like

def foo : TacGen := bar
-- evalConst TacGen `foo
-- works here

[Kyle Miller]

Yeah, my understanding is that evalConst TacGen decl looks up the declaration whose name is given by decl, which has already been compiled, and then uses the interpreter to evaluate the compiled code, returning some runtime value, which must be a TacGen. If it's not actually a TacGen, then unspecified behavior occurs.