Deriving Add

Stream: lean4

[Tomas Skrivan]

I would like to derive Add for any structure that has elements equipped with Add. My ultimate goal is to automatically derive that a structure is a vector space if all its elements form a vectors space. What is the best way to approach this?

[Tomas Skrivan]

My attempt at registering new deriving Add but it does not seem to do anything

import Lean.Meta.Inductive
import Lean.Elab.Deriving.Basic
import Lean.Elab.Deriving.Util

namespace Lean.Elab.Deriving

open Command
open Lean.Parser.Term
open Meta

def mkAddHandler (declNames : Array Name) : CommandElabM Bool := do
  if (← declNames.allM isInductive) && declNames.size > 0 then
    IO.println "Calling Add Handler!"
    return true
  else
    return false

builtin_initialize
  registerDerivingHandler ``Add mkAddHandler

structure Float2 where
  (x y : Float)
deriving Add

[Mario Carneiro]

you should use initialize instead of builtin_initialize, and you should put Float2 in another file

[Tomas Skrivan]

Ahh it is being registered correctly now! Thanks!

[Tomas Skrivan]

If anyone is interested here is the solution:

import Lean.Elab.Deriving.Basic

open Lean Elab Command

private def mkAddInstanceCmd (declName : Name) : TermElabM (TSyntax "command") := do
  let env ← getEnv
  match getStructureInfo? env declName with
  | some info => do
    let xName : Name := "x"
    let yName : Name := "y"
    let args : TSyntaxArray "term" ← info.fieldNames.mapM (λ name => `(($(mkIdent <| xName.append name) + $(mkIdent <| yName.append name))))
    let addFun : TSyntax "term" ← `(λ $(mkIdent xName) $(mkIdent yName) => $(mkIdent (declName.append "mk")) $args*)
    let cmd ← `(instance : Add $(mkIdent declName) := ⟨$addFun⟩)
    return cmd
  | none =>
    pure default


def mkAddHandler (declNames : Array Name) : CommandElabM Bool := do
  let env ← getEnv
  if (← declNames.allM (λ name => pure (isStructure env name))) && declNames.size > 0 then
    declNames.forM λ name => do
      let cmd ← liftTermElabM <| mkAddInstanceCmd name
      elabCommand cmd
    return true
  else
    return false

initialize
  registerDerivingHandler ``Add mkAddHandler

It works but I'm really not sure if I got the macro hygiene correct. Creating names and identifiers is still a bit of a mystery to me.

[Mario Carneiro]

macro hygiene is generally as simple as using identifiers directly in the syntax quotation

[Mario Carneiro]

what you are doing is manually creating unhygienic identifiers

[Tomas Skrivan]

That was my suspicion that the arguments x and y in the lambda are not hygienic. But I wasnt sure how can I create the array args e.g. #[(x.x + y.x), (x.y + y.y)]

[Tomas Skrivan]

This works, but not sure if it is the intended way:

    let x : TSyntax "ident" ← `(x)
    let y : TSyntax "ident" ← `(y)
    let args : TSyntaxArray "term" ← info.fieldNames.mapM (λ name => `(( $x.$(mkIdent name) + $y.$(mkIdent name))))
    let addFun : TSyntax "term" ← `(λ $x $y => $(mkIdent (declName.append "mk")) $args*)

[Mario Carneiro]

private def mkAddInstanceCmd (declName : Name) : TermElabM (TSyntax "command") := do
  let env ← getEnv
  match getStructureInfo? env declName with
  | some info => do
    let mk := (getStructureCtor env declName).name
    let args : TSyntaxArray `term ← info.fieldNames.mapM fun name =>
      `((x.$(mkIdent name) + y.$(mkIdent name)))
    let addFun : Term ← `(λ x y => $(mkIdent mk) $args*)
    `(instance : Add $(mkIdent declName) := ⟨$addFun⟩)
  | none =>
    pure default

[Tomas Skrivan]

Interesting, I thought that this way the x and y would end up being different identifiers in args and addFun.

[Mario Carneiro]

the identifiers depend on the current "macro scope", which is a ReaderT argument so it can't change unless you use a combinator like withFreshMacroScope

[Mario Carneiro]

it gets incremented when you call back into the macro system or do one step of macro expansion

[Mario Carneiro]

and you can also use that function directly if you want lots of variables

[Mario Carneiro]

The (mkIdent mk) $args* still isn't quite correct because the constructor could have implicit arguments. It's probably better to use a structure literal

[Mario Carneiro]

    let fields : Array Ident := info.fieldNames.map mkIdent
    let fields1 := fields; let fields2 := fields
    `(instance : Add $(mkIdent declName) := ⟨λ x y => {
      $[$fields:ident := x.$fields1 + y.$fields2]*
    }⟩)

[Mario Carneiro]

cc: @Sebastian Ullrich any particular reason that you can't reuse variables in a syntax quotation?

[Sebastian Ullrich]

No particular reason, just an edge case in the implementation

[Mario Carneiro]

ooh, if you use $(id fields) you get an even weirder error

[Tomas Skrivan]

I would like to generalize it to user specified binary operation, but for className := ``Add and opName := ``Add.add, this breaks:

    let fields : Array Ident := info.fieldNames.map mkIdent
    let fields1 := fields; let fields2 := fields
    `(instance : $(mkIdent className) $(mkIdent declName) := ⟨λ x y => {
      $[$fields:ident := $(mkIdent opName):ident x.$fields1 y.$fields2]*}⟩)

[Mario Carneiro]

:sad: I guess the implementation isn't that great at mixing variables with different repetitions. You can still do the original thing:

    let className := ``Add
    let opName := ``Add.add
    let fields ← info.fieldNames.map mkIdent |>.mapM fun field =>
      `(Lean.Parser.Term.structInstField|
        $field:ident := $(mkIdent opName):ident x.$field y.$field)
    `(instance : $(mkIdent className) $(mkIdent declName) := ⟨λ x y => { $fields* }⟩)

[Tomas Skrivan]

Unfortunately this totally fails for parameterized structures such as:

structure Pair2 (α : Type) [Add α] where
  (x y : α)
deriving Add

[Tomas Skrivan]

Horray, I can do it even for parameterized structures! I could not figure it out by manipulating Syntax so I had to get my hands dirty and manipulate Expr directly and create Declaration

private def mkBinaryOpInstance (className opName : Name) (declName : Name) : TermElabM Unit := do
  let env ← getEnv
  match getStructureInfo? env declName with
  | some info => do
    IO.println s!"{info.structName}"
    let structType ← Meta.inferType (mkConst info.structName)
    let instValue ← Meta.forallTelescope structType λ xs b =>
    do
      let strct ← Meta.mkAppOptM info.structName (xs.map some)
      let binOp ←
        Meta.withLocalDecl `x default strct λ x =>
        Meta.withLocalDecl `y default strct λ y =>
         do
           let mut fields := #[]
           for i in [0:info.fieldNames.size] do
             fields := fields.push (← Meta.mkAppM opName #[x.proj info.structName i, y.proj info.structName i])
           (Meta.mkLambdaFVars #[x,y] (← Meta.mkAppM (info.structName.append "mk") fields))

      Meta.mkLambdaFVars xs (← Meta.mkAppM (className.append "mk") #[binOp])

    let instType ← Meta.inferType instValue

    let instName : Name := s!"inst{className}{declName}"
    let instDecl : Declaration := .defnDecl
      {levelParams := [],
       hints := .abbrev,
       safety := .safe,
       type := instType,
       value := instValue,
       name := instName,
       }
    addAndCompile instDecl
    Attribute.add instName "instance" default
  | none =>
    pure default


def mkBinaryOpHandler (className opName : Name) (declNames : Array Name) : CommandElabM Bool := do
  let env ← getEnv
  if (← declNames.allM (λ name => pure (isStructure env name))) && declNames.size > 0 then
    declNames.forM λ name => do
      liftTermElabM <| mkBinaryOpInstance className opName name
    return true
  else
    return false

initialize
  registerDerivingHandler ``Add (mkBinaryOpHandler ``Add ``Add.add)