feat: ToExpr deriving handler (#3215)

Add a deriving handler for `ToExpr` loosely modeled off the  `Repr` one. Supports mutually recursive inductive types.

Introduces a `ToLevel` typeclass for creating `Level` expressions that represent universe levels. This is used in the derived `ToExpr` instances to support some universe polymorphism.

Mathlib.lean

@@ -1586,6 +1586,7 @@ import Mathlib.Tactic.Contrapose
 import Mathlib.Tactic.Conv
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.Core
+import Mathlib.Tactic.DeriveToExpr
 import Mathlib.Tactic.Elementwise
 import Mathlib.Tactic.Eqns
 import Mathlib.Tactic.Existsi
@@ -1672,6 +1673,8 @@ import Mathlib.Tactic.SwapVar
 import Mathlib.Tactic.TFAE
 import Mathlib.Tactic.Tauto
 import Mathlib.Tactic.ToAdditive
+import Mathlib.Tactic.ToExpr
+import Mathlib.Tactic.ToLevel
 import Mathlib.Tactic.Trace
 import Mathlib.Tactic.TypeCheck
 import Mathlib.Tactic.UnsetOption

Mathlib/Tactic/DeriveToExpr.lean

@@ -0,0 +1,197 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+import Lean
+import Mathlib.Tactic.ToLevel
+
+/-!
+# A `ToExpr` derive handler
+
+This module defines a `ToExpr` derive handler for inductive types. It supports mutually inductive
+types as well.
+
+The `ToExpr` derive handlers support universe level polymorphism. This is implemented using the
+`Lean.ToLevel` class. To use `ToExpr` in places where there is universe polymorphism, make sure
+to have a `[ToLevel.{u}]` instance available.
+
+**Warning:** Import `Mathlib.Tactic.ToExpr` instead of this one. This ensures that you are using
+the universe polymorphic `ToExpr` instances that override the ones from Lean 4 core.
+
+Implementation note: this derive handler was originally modeled after the `Repr` derive handler.
+-/
+
+namespace Mathlib.Deriving.ToExpr
+
+open Lean Elab Lean.Parser.Term
+open Meta Command Deriving
+
+def mkToExprHeader (indVal : InductiveVal) : TermElabM Header := do
+  -- The auxiliary functions we produce are `indtype -> Expr`.
+  let header ← mkHeader ``ToExpr 1 indVal
+  return header
+
+/-- Give a term that is equivalent to `(term|mkAppN $f #[$args,*])`.
+As an optimization, `mkAppN` is pre-expanded out to use `Expr.app` directly. -/
+def mkAppNTerm (f : Term) (args : Array Term) : MetaM Term :=
+  args.foldlM (fun a b => `(Expr.app $a $b)) f
+
+def mkToExprBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) :
+    TermElabM Term := do
+  let discrs ← mkDiscrs header indVal
+  let alts ← mkAlts
+  `(match $[$discrs],* with $alts:matchAlt*)
+where
+  mkAlts : TermElabM (Array (TSyntax ``matchAlt)) := do
+    let mut alts := #[]
+    for ctorName in indVal.ctors do
+      let ctorInfo ← getConstInfoCtor ctorName
+      let alt ← forallTelescopeReducing ctorInfo.type fun xs _ => do
+        let mut patterns := #[]
+        -- add `_` pattern for indices
+        for _ in [:indVal.numIndices] do
+          patterns := patterns.push (← `(_))
+        let mut ctorArgs := #[]
+        let mut rhsArgs : Array Term := #[]
+        let mkArg (x : Expr) (a : Term) : TermElabM Term := do
+          if (← inferType x).isAppOf indVal.name then
+            `($(mkIdent auxFunName) $a)
+          else if ← Meta.isType x then
+            `(toTypeExpr $a)
+          else
+            `(toExpr $a)
+        -- add `_` pattern for inductive parameters, which are inaccessible
+        for i in [:ctorInfo.numParams] do
+          let a := mkIdent header.argNames[i]!
+          ctorArgs := ctorArgs.push (← `(_))
+          rhsArgs := rhsArgs.push <| ← mkArg xs[i]! a
+        for i in [:ctorInfo.numFields] do
+          let a := mkIdent (← mkFreshUserName `a)
+          ctorArgs := ctorArgs.push a
+          rhsArgs := rhsArgs.push <| ← mkArg xs[ctorInfo.numParams + i]! a
+        patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs:term*))
+        let levels ← indVal.levelParams.toArray.mapM (fun u => `(toLevel.{$(mkIdent u)}))
+        let rhs : Term ←
+          mkAppNTerm (← `(Expr.const $(quote ctorInfo.name) [$levels,*])) rhsArgs
+        `(matchAltExpr| | $[$patterns:term],* => $rhs)
+      alts := alts.push alt
+    return alts
+
+def mkToTypeExpr (argNames : Array Name) (indVal : InductiveVal) : TermElabM Term := do
+  let levels ← indVal.levelParams.toArray.mapM (fun u => `(toLevel.{$(mkIdent u)}))
+  forallTelescopeReducing indVal.type fun xs _ => do
+    let mut args : Array Term := #[]
+    for i in [:xs.size] do
+      let x := xs[i]!
+      let a := mkIdent argNames[i]!
+      if ← Meta.isType x then
+        args := args.push <| ← `(toTypeExpr $a)
+      else
+        args := args.push <| ← `(toExpr $a)
+    mkAppNTerm (← `((Expr.const $(quote indVal.name) [$levels,*]))) args
+
+def mkLocalInstanceLetDecls (ctx : Deriving.Context) (argNames : Array Name) :
+    TermElabM (Array (TSyntax ``Parser.Term.letDecl)) := do
+  let mut letDecls := #[]
+  for i in [:ctx.typeInfos.size] do
+    let indVal       := ctx.typeInfos[i]!
+    let auxFunName   := ctx.auxFunNames[i]!
+    let currArgNames ← mkInductArgNames indVal
+    let numParams    := indVal.numParams
+    let currIndices  := currArgNames[numParams:]
+    let binders      ← mkImplicitBinders currIndices
+    let argNamesNew  := argNames[:numParams] ++ currIndices
+    let indType      ← mkInductiveApp indVal argNamesNew
+    let instName     ← mkFreshUserName `localinst
+    let toTypeExpr   ← mkToTypeExpr argNames indVal
+    let letDecl      ← `(Parser.Term.letDecl| $(mkIdent instName):ident $binders:implicitBinder* :
+                            ToExpr $indType :=
+                          { toExpr := $(mkIdent auxFunName), toTypeExpr := $toTypeExpr })
+    letDecls := letDecls.push letDecl
+  return letDecls
+
+/-- Fix the output of `mkInductiveApp` to explicitly reference universe levels. -/
+def fixIndType (indVal : InductiveVal) (t : Term) : TermElabM Term :=
+  match t with
+  | `(@$f $args*) =>
+    let levels := indVal.levelParams.toArray.map mkIdent
+    `(@$f.{$levels,*} $args*)
+  | _ => throwError "(internal error) expecting output of `mkInductiveApp`"
+
+/-- Make `ToLevel` instance binders for all the level variables. -/
+def mkToLevelBinders (indVal : InductiveVal) : TermElabM (TSyntaxArray ``instBinderF) := do
+  indVal.levelParams.toArray.mapM (fun u => `(instBinderF| [ToLevel.{$(mkIdent u)}]))
+
+open TSyntax.Compat in
+def mkAuxFunction (ctx : Deriving.Context) (i : Nat) : TermElabM Command := do
+  let auxFunName := ctx.auxFunNames[i]!
+  let indVal     := ctx.typeInfos[i]!
+  let header     ← mkToExprHeader indVal
+  let mut body   ← mkToExprBody header indVal auxFunName
+  if ctx.usePartial then
+    let letDecls ← mkLocalInstanceLetDecls ctx header.argNames
+    body ← mkLet letDecls body
+  -- We need to alter the last binder (the one for the "target") to have explicit universe levels
+  -- so that the `ToLevel` instance arguments can use them.
+  let addLevels binder :=
+    match binder with
+    | `(bracketedBinderF| ($a : $ty)) => do `(bracketedBinderF| ($a : $(← fixIndType indVal ty)))
+    | _ => throwError "(internal error) expecting inst binder"
+  let binders := header.binders.pop
+    ++ (← mkToLevelBinders indVal)
+    ++ #[← addLevels header.binders.back]
+  let levels := indVal.levelParams.toArray.map mkIdent
+  if ctx.usePartial then
+    `(private partial def $(mkIdent auxFunName):ident.{$levels,*} $binders:bracketedBinder* :
+        Expr := $body:term)
+  else
+    `(private def $(mkIdent auxFunName):ident.{$levels,*} $binders:bracketedBinder* :
+        Expr := $body:term)
+
+def mkMutualBlock (ctx : Deriving.Context) : TermElabM Syntax := do
+  let mut auxDefs := #[]
+  for i in [:ctx.typeInfos.size] do
+    auxDefs := auxDefs.push (← mkAuxFunction ctx i)
+  `(mutual $auxDefs:command* end)
+
+open TSyntax.Compat in
+def mkInstanceCmds (ctx : Deriving.Context) (typeNames : Array Name) :
+    TermElabM (Array Command) := do
+  let mut instances := #[]
+  for i in [:ctx.typeInfos.size] do
+    let indVal       := ctx.typeInfos[i]!
+    if typeNames.contains indVal.name then
+      let auxFunName   := ctx.auxFunNames[i]!
+      let argNames     ← mkInductArgNames indVal
+      let binders      ← mkImplicitBinders argNames
+      let binders      := binders ++ (← mkInstImplicitBinders ``ToExpr indVal argNames)
+      let binders      := binders ++ (← mkToLevelBinders indVal)
+      let indType      ← fixIndType indVal (← mkInductiveApp indVal argNames)
+      let toTypeExpr   ← mkToTypeExpr argNames indVal
+      let levels       := indVal.levelParams.toArray.map mkIdent
+      let instCmd ← `(instance $binders:implicitBinder* : ToExpr $indType where
+                        toExpr := $(mkIdent auxFunName).{$levels,*}
+                        toTypeExpr := $toTypeExpr)
+      instances := instances.push instCmd
+  return instances
+
+def mkToExprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
+  let ctx ← mkContext "toExpr" declNames[0]!
+  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx declNames)
+  trace[Elab.Deriving.toExpr] "\n{cmds}"
+  return cmds
+
+def mkToExprInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
+  if (← declNames.allM isInductive) && declNames.size > 0 then
+    let cmds ← liftTermElabM <| mkToExprInstanceCmds declNames
+    cmds.forM elabCommand
+    return true
+  else
+    return false
+
+initialize
+  registerDerivingHandler `Lean.ToExpr mkToExprInstanceHandler
+  registerTraceClass `Elab.Deriving.toExpr
+
+end Mathlib.Deriving.ToExpr

Mathlib/Tactic/ToExpr.lean

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+import Mathlib.Tactic.DeriveToExpr
+
+/-! # `ToExpr` instances for Mathlib
+
+This module should be imported by any module that intends to define `ToExpr` instances.
+It provides necessary dependencies (the `Lean.ToLevel` class) and it also overrides the instances
+that come from core Lean 4 that do not handle universe polymorphism.
+(See the module `Lean.ToExpr` for the instances that are overridden.)
+
+In addition, we provide some additional `ToExpr` instances for core definitions.
+-/
+
+section override
+namespace Lean
+
+attribute [-instance] Lean.instToExprOption
+
+deriving instance ToExpr for Option
+
+attribute [-instance] Lean.instToExprList
+
+deriving instance ToExpr for List
+
+attribute [-instance] Lean.instToExprArray
+
+instance {α : Type u} [ToExpr α] [ToLevel.{u}] : ToExpr (Array α) :=
+  let type := toTypeExpr α
+  { toExpr     := fun as => mkApp2 (mkConst ``List.toArray [toLevel.{u}]) type (toExpr as.toList)
+    toTypeExpr := mkApp (mkConst ``Array [toLevel.{u}]) type }
+
+attribute [-instance] Lean.instToExprProd
+
+deriving instance ToExpr for Prod
+
+end Lean
+end override
+
+namespace Mathlib
+open Lean
+
+deriving instance ToExpr for Int
+
+deriving instance ToExpr for ULift
+
+/-- Hand-written instance since `PUnit` is a `Sort` rather than a `Type`. -/
+instance [ToLevel.{u}] : ToExpr PUnit.{u+1} where
+  toExpr _ := mkConst ``PUnit.unit [toLevel.{u+1}]
+  toTypeExpr := mkConst ``PUnit [toLevel.{u+1}]
+
+deriving instance ToExpr for String.Pos
+deriving instance ToExpr for Substring
+deriving instance ToExpr for SourceInfo
+deriving instance ToExpr for Syntax.Preresolved
+deriving instance ToExpr for Syntax
+
+open DataValue in
+private def toExprMData (md : MData) : Expr := Id.run do
+  let mut e := mkConst ``MData.empty
+  for (k, v) in md do
+    let k := toExpr k
+    e := match v with
+          | ofString v => mkApp3 (mkConst ``KVMap.setString) e k (mkStrLit v)
+          | ofBool v   => mkApp3 (mkConst ``KVMap.setBool) e k (toExpr v)
+          | ofName v   => mkApp3 (mkConst ``KVMap.setName) e k (toExpr v)
+          | ofNat v    => mkApp3 (mkConst ``KVMap.setNat) e k (mkNatLit v)
+          | ofInt v    => mkApp3 (mkConst ``KVMap.setInt) e k (toExpr v)
+          | ofSyntax v => mkApp3 (mkConst ``KVMap.setSyntax) e k (toExpr v)
+  return e
+
+instance : ToExpr MData where
+  toExpr := toExprMData
+  toTypeExpr := mkConst ``MData
+
+deriving instance ToExpr for FVarId
+deriving instance ToExpr for MVarId
+deriving instance ToExpr for LevelMVarId
+deriving instance ToExpr for Level
+deriving instance ToExpr for BinderInfo
+deriving instance ToExpr for Literal
+deriving instance ToExpr for Expr
+
+end Mathlib

Mathlib/Tactic/ToLevel.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+import Lean
+import Mathlib.Init.Align
+
+/-! # `ToLevel` class
+
+This module defines `Lean.ToLevel`, which is the `Lean.Level` analogue to `Lean.ToExpr`.
+
+**Warning:** Import `Mathlib.Tactic.ToExpr` instead of this one if you are writing `ToExpr`
+instances. This ensures that you are using the universe polymorphic `ToExpr` instances that
+override the ones from Lean 4 core.
+
+-/
+
+namespace Lean
+
+/-- A class to create `Level` expressions that denote particular universe levels in Lean.
+`Lean.ToLevel.toLevel.{u}` evaluates to a `Lean.Level` term representing `u` -/
+class ToLevel.{u} where
+  /-- A `Level` that represents the universe level `u`. -/
+  toLevel : Level
+  /-- The universe itself. This is only here to avoid the "unused universe parameter" error. -/
+  univ : Type u := Sort u
+export ToLevel (toLevel)
+#align reflected_univ Lean.ToLevel
+#align reflected_univ.lvl Lean.ToLevel.toLevel
+
+instance : ToLevel.{0} where
+  toLevel := .zero
+
+instance [ToLevel.{u}] : ToLevel.{u+1} where
+  toLevel := .succ toLevel.{u}
+
+/-- `ToLevel` for `max u v`. This is not an instance since it causes divergence. -/
+def ToLevel.max [ToLevel.{u}] [ToLevel.{v}] : ToLevel.{max u v} where
+  toLevel := .max toLevel.{u} toLevel.{v}
+
+/-- `ToLevel` for `imax u v`. This is not an instance since it causes divergence. -/
+def ToLevel.imax [ToLevel.{u}] [ToLevel.{v}] : ToLevel.{imax u v} where
+  toLevel := .imax toLevel.{u} toLevel.{v}
+
+end Lean