Support options with type ``Lean.Name``

Stream: lean4

[Yicheng Qian]

Is it possible to support options with type Lean.Name? I need this type of options in lean-auto. Currently we can register options of type Lean.Name

register_option foo : Lean.Name := {
  defValue := ""
}

But cannot set_option:

set_option foo ``Nat.add

Seems like the parser is not supporting Name literals

-- Lean/Parser/Command.lean
def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
@[builtin_command_parser] def «set_option»   := leading_parser
  "set_option " >> ident >> ppSpace >> optionValue

[Yicheng Qian]

Currently I'm using a workaround: register options of type String and use name_str.foldl (fun acc s => Name.str acc s) .anonymous.

[Kyle Miller]

There's a possibility. There are some questions about the implementation.

There are two options:

1. Have set_option foo `name and set_option foo ``name, where single vs double backquote work like how they do for normal names (the latter would do name resolution)
2. Have set_option foo name, where either (a) name is not resolved or (b) name always attempts to resolve and either b.1 doesn't throw an error if it doesn't or b.2 throws an error if it does.

Could you mention the use case for name-valued options in lean-auto? Could you also evaluate the difference between this proposed set_option feature and using an attribute?

[Yicheng Qian]

In lean-auto, I sometimes want to leave "hole"s in the code using Lean.evalConst:

• I want users to be able to customize e.g. the translation from lean-auto's internal representation to Lean. This can be done by leaving a hole in the code.
• I need to debug code deep in the import tree (long compilation time), and testing lean-auto might require importing mathlib (long loading time). Sometimes I have to make several attempts to get the code right. So, I leave a hole in the code deep in the import tree, and fill the hole directly in the test file.

[Yicheng Qian]

I think set_option foo `name and set_option foo ``name is better within the two options.

[Yicheng Qian]

Using attributes would also be ok, but set_option seems more convenient?

[Kyle Miller]

Is it more convenient than writing something like the following?

@[rebind myFn]
def newFn : ...

That would be rather than

def newFn : ...

setOption myFn ``newFn

[Yicheng Qian]

I'm a bit confused. My intended set_option approach looks like this overall:

register_option hole_func_name : Name := ...

unsafe def foo := do
  ...
  let hole_func ← hole_func_name.get (← getOptions)
  <check that hole_func have the correct type>
  let hole ← evalConst <expected_type> hole_func
  ...

-- In another Lean file
def newFn := ...
set_option hole_func_name ``newFn

If I understand correctly, the rebind approach only replaces

-- In another Lean file
def newFn := ...
set_option hole_func_name ``newFn

with

@[rebind hole_func_name]
def newFn := ...

[Yicheng Qian]

That would be a little more convenient.

[Yicheng Qian]

However, the set_option approach will allow def newFn := ... and set_option hole_func_name ``newFn to reside in different Lean files, while the rebind approach won't.

[Kyle Miller]

You could use the attribute [rebind hole_func_name] newFn syntax from a different file just fine

[Kyle Miller]

code: Rebind.lean

import Lean

open Lean

structure RebindDescr where
  fnName : Name
  type : Expr
  impl? : Option Name
  deriving Inhabited

abbrev RebindState := NameMap RebindDescr

abbrev RebindExtension := SimpleScopedEnvExtension RebindDescr RebindState

def RebindState.addEntry (s : NameMap RebindDescr) (r : RebindDescr) : NameMap RebindDescr :=
  s.insert r.fnName r

initialize rebindExtension : RebindExtension ←
  registerSimpleScopedEnvExtension {
    initial := {}
    addEntry := RebindState.addEntry
  }

def getRebinds (env : Environment) : NameMap RebindDescr := rebindExtension.getState env

def getRebind? (env : Environment) (fnName : Name) : Option RebindDescr :=
  (getRebinds env).find? fnName

syntax (name := rebindAttr) "rebind " ident : attr

initialize
  registerBuiltinAttribute {
    name := `rebindAttr
    descr := "add a rebind"
    add   := fun decl stx kind => do
      match stx with
      | `(attr| rebind $fnName) => withRef stx[0] do
        let fnName := fnName.getId.eraseMacroScopes
        let some r := getRebind? (← getEnv) fnName
          | throwError "No such rebindable function {fnName}"
        let some info := (← getEnv).find? decl | unreachable!
        unless info.levelParams.isEmpty do
          throwError "Declaration has level parameters, which is not supported."
        unless ← Meta.MetaM.run' <| Meta.isDefEq info.type r.type do
          throwError "Type is{indentD info.type}\nbut it must be{indentD r.type}"
        let r' := {r with impl? := decl}
        rebindExtension.add r' kind
      | _  => throwError "invalid `[rebind]` attribute"
  }

unsafe def RebindExtension.eval {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m]
    (α : Type) (n : Name) : m α := do
  let some c := getRebind? (← getEnv) n
    | throwError "No such rebindable function {n}"
  let some impl := c.impl?
    | throwError "No implementation exists for rebind {n}"
  evalConst α impl

elab "declare_rebindable " fnName:ident " : " type:term : command => do
  Elab.Command.runTermElabM fun args => do
    let type ← Elab.Term.elabType type
    Elab.Term.synthesizeSyntheticMVarsUsingDefault
    let type ← Meta.mkForallFVars (usedOnly := true) args type
    let type ← instantiateMVars type
    if type.hasMVar then
      throwError "Type contains metavariables{indentD type}"
    if type.hasLevelParam then
      throwError "Type contains level parameters{indentD type}"
    let r : RebindDescr :=
      { fnName := fnName.getId
        type := type
        impl? := none }
    rebindExtension.add r .global

syntax (name := evalRebindStx) "eval_rebind% " ident : term

@[term_elab evalRebindStx]
def elabEvalRebindStx : Elab.Term.TermElab
  | `(eval_rebind% $fnName) => fun expectedType? => do
    let some c := getRebind? (← getEnv) fnName.getId
      | throwError "No such rebindable function {fnName}"
    let stx ← `(unsafe RebindExtension.eval $(← Elab.Term.exprToSyntax c.type) $(quote fnName.getId))
    Elab.Term.elabTerm stx expectedType?
  | _ => fun _ => Elab.throwUnsupportedSyntax

Example usage (you need to fix the import first):

import /-packagename-/.Rebind

declare_rebindable foo : Nat

def test : Lean.MetaM Nat :=
  eval_rebind% foo

#eval test
-- No implementation exists for rebind foo

@[rebind foo]
def myFoo : Nat := 22

#eval test
-- 22

section
@[local rebind foo]
def myFoo' : Nat := 37

#eval test
-- 37

end

#eval test
-- 22

[Kyle Miller]

Extending the examples:

declare_rebindable f : Nat → Nat
declare_rebindable a : Nat

def test2 : Lean.MetaM Nat := do
  return (← eval_rebind% f) (← eval_rebind% a)

attribute [rebind a] myFoo

@[rebind f]
def myF := (· * 2)

#eval test2
-- 44

[Kyle Miller]

Note that the type of eval_rebind% f in this example is m (Nat -> Nat), for m some monad that supports what evalConst requires.

Note also that since this is being done with a term elaborator like this, we can safely omit unsafe because we can ensure it has the right type.

[Yicheng Qian]

Thanks! I'm using rebind in lean-auto now.