feat: add Deriving/Inhabited.lean

src/Lean/Elab/Deriving.lean

@@ -4,3 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Elab.Deriving.Basic
+import Lean.Elab.Deriving.Inhabited

src/Lean/Elab/Deriving/Basic.lean

@@ -41,4 +41,7 @@ def applyDerivingHandlers (className : Name) (typeNames : Array Name) : CommandE
          logException ex
   | _ => throwUnsupportedSyntax
 
+builtin_initialize
+  registerTraceClass `Elab.Deriving
+
 end Lean.Elab

src/Lean/Elab/Deriving/Inhabited.lean

@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Elab.Deriving.Basic
+
+namespace Lean.Elab
+open Command
+open Meta
+
+private abbrev IndexSet := Std.RBTree Nat (.<.)
+private abbrev LocalInst2Index := NameMap Nat
+
+private def implicitBinderF := Parser.Term.implicitBinder
+private def instBinderF     := Parser.Term.instBinder
+
+private def mkInhabitedInstanceUsing (inductiveTypeName : Name) (ctorName : Name) (addHypotheses : Bool) : CommandElabM Bool := do
+  match (← liftTermElabM none mkInstanceCmd?) with
+  | some cmd =>
+    elabCommand cmd
+    return true
+  | none =>
+    return false
+where
+  addLocalInstancesForParamsAux {α} (k : LocalInst2Index → TermElabM α) : List Expr → Nat → LocalInst2Index → TermElabM α
+    | [], i, map    => k map
+    | x::xs, i, map =>
+      try
+        let instType ← mkAppM `Inhabited #[x]
+        if (← isTypeCorrect instType) then
+          withLocalDeclD (← mkFreshUserName `inst) instType fun inst => do
+            trace[Elab.Deriving.inhabited]! "adding local instance {instType}"
+            addLocalInstancesForParamsAux k xs (i+1) (map.insert inst.fvarId! i)
+        else
+          addLocalInstancesForParamsAux k xs (i+1) map
+      catch _ =>
+        addLocalInstancesForParamsAux k xs (i+1) map
+
+  addLocalInstancesForParams {α} (xs : Array Expr) (k : LocalInst2Index → TermElabM α) : TermElabM α := do
+    if addHypotheses then
+      addLocalInstancesForParamsAux k xs.toList 0 {}
+    else
+      k {}
+
+  collectUsedLocalsInsts (usedInstIdxs : IndexSet) (localInst2Index : LocalInst2Index) (e : Expr) : IndexSet :=
+    if localInst2Index.isEmpty then
+      usedInstIdxs
+    else
+      let visit {ω} : StateRefT IndexSet (ST ω) Unit :=
+        e.forEach fun
+          | Expr.fvar fvarId _ =>
+            match localInst2Index.find? fvarId with
+            | some idx => modify (·.insert idx)
+            | none => pure ()
+          | _ => pure ()
+      runST (fun _ => visit |>.run usedInstIdxs) |>.2
+
+  /- Create an `instance` command using the constructor `ctorName` with a hypothesis `Inhabited α` when `α` is one of the inductive type parameters
+     at position `i` and `i ∈ assumingParamIdxs`. -/
+  mkInstanceCmdWith (assumingParamIdxs : IndexSet) : TermElabM Syntax := do
+    let indVal ← getConstInfoInduct inductiveTypeName
+    let ctorVal ← getConstInfoCtor ctorName
+    let mut indArgs := #[]
+    let mut binders := #[]
+    for i in [:indVal.nparams + indVal.nindices] do
+      let arg := mkIdent (← mkFreshUserName `a)
+      indArgs := indArgs.push arg
+      let binder ← `(implicitBinderF| { $arg:ident })
+      binders := binders.push binder
+      if assumingParamIdxs.contains i then
+        let binder ← `(instBinderF| [ Inhabited $arg:ident ])
+        binders := binders.push binder
+    let type ← `(Inhabited (@$(mkIdent inductiveTypeName):ident $indArgs:ident*))
+    let mut ctorArgs := #[]
+    for i in [:ctorVal.nparams] do
+      ctorArgs := ctorArgs.push (← `(_))
+    for i in [:ctorVal.nfields] do
+      ctorArgs := ctorArgs.push (← `(arbitrary))
+    let val ← `(⟨@$(mkIdent ctorName):ident $ctorArgs:ident*⟩)
+    `(instance $binders:explicitBinder* : $type := $val)
+
+  mkInstanceCmd? : TermElabM (Option Syntax) := do
+    let ctorVal ← getConstInfoCtor ctorName
+    forallTelescopeReducing ctorVal.type fun xs _ =>
+      addLocalInstancesForParams xs[:ctorVal.nparams] fun localInst2Index => do
+        let mut usedInstIdxs := {}
+        let mut ok := true
+        for i in [ctorVal.nparams:xs.size] do
+          let x := xs[i]
+          let instType ← mkAppM `Inhabited #[(← inferType x)]
+          trace[Elab.Deriving.inhabited]! "checking {instType} for '{ctorName}'"
+          match (← trySynthInstance instType) with
+          | LOption.some e =>
+            usedInstIdxs ← collectUsedLocalsInsts usedInstIdxs localInst2Index e
+          | _ =>
+            trace[Elab.Deriving.inhabited]! "failed to generate instance using '{ctorName}' {if addHypotheses then "(assuming parameters are inhabited)" else ""} because of field with type{indentExpr (← inferType x)}"
+            ok := false
+            break
+        if !ok then
+          return none
+        else
+          trace[Elab.Deriving.inhabited]! "inhabited instance using '{ctorName}' {if addHypotheses then "(assuming parameters are inhabited)" else ""} {usedInstIdxs.toList}"
+          let cmd ← mkInstanceCmdWith usedInstIdxs
+          trace[Elab.Deriving.inhabited]! "\n{cmd}"
+          return some cmd
+
+private def mkInhabitedInstance (declName : Name) : CommandElabM Unit := do
+  let indVal ← getConstInfoInduct declName
+  let doIt (addHypotheses : Bool) : CommandElabM Bool := do
+    for ctorName in indVal.ctors do
+      if (← mkInhabitedInstanceUsing declName ctorName addHypotheses) then
+        return true
+    return false
+  unless (← doIt false <||> doIt true) do
+    throwError! "failed to generate 'Inhabited' instance for '{declName}'"
+
+def mkInhabitedInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
+  if (← declNames.allM isInductive) then
+    declNames.forM mkInhabitedInstance
+    return true
+  else
+    return false
+
+builtin_initialize
+  registerBuiltinDerivingHandler `Inhabited mkInhabitedInstanceHandler
+  registerTraceClass `Elab.Deriving.inhabited
+
+end Lean.Elab

src/Lean/MonadEnv.lean

@@ -15,6 +15,11 @@ variables {m : Type → Type} [MonadEnv m]
 def setEnv (env : Environment) : m Unit :=
   modifyEnv fun _ => env
 
+def isInductive [Monad m] (declName : Name) : m Bool := do
+  match (← getEnv).find? declName with
+  | some (ConstantInfo.inductInfo ..) => return true
+  | _ => return false
+
 @[inline] def withoutModifyingEnv [Monad m] [MonadFinally m] {α : Type} (x : m α) : m α := do
   let env ← getEnv
   try x finally setEnv env