0a2d121e45
closes #5333 This PR tries to address issue #5333. My conjecture is that the binder annotations for `C.toB` and `Algebra.toSMul` are not ideal. `Algebra.toSMul` is one of declarations where the new command `set_synth_order` was used. Both classes, `C` and `Algebra`, are parametric over instances, and in both cases, the issue arises due to projection instances: `C.toB` and `Algebra.toSMul`. Let's focus on the binder annotations for `C.toB`. They are as follows: ``` C.toB [inst : A 20000] [self : @C inst] : @B ... ``` As a projection, it seems odd that `inst` is an instance-implicit argument instead of an implicit one, given that its value is fixed by `self`. We observe the same issue in `Algebra.toSMul`: ``` Algebra.toSMul {R : Type u} {A : Type v} [inst1 : CommSemiring R] [inst2 : Semiring A] [self : @Algebra R A inst1 inst2] : SMul R A ``` The PR changes the binder annotations as follows: ``` C.toB {inst : A 20000} [self : @C inst] : @B ... ``` and ``` Algebra.toSMul {R : Type u} {A : Type v} {inst1 : CommSemiring R} {inst2 : Semiring A} [self : @Algebra R A inst1 inst2] : SMul R A ``` In both cases, the `set_synth_order` is used to force `self` to be processed first. In the MWE, there is no instance for `C ...`, and `C.toB` is quickly discarded. I suspect a similar issue occurs when trying to use `Algebra.toSMul`, where there is no `@Algebra R A ... ...`, but Lean spends unnecessary time trying to synthesize `CommSemiring R` and `Semiring A` instances. I believe the new binder annotations make sense, as if there is a way to synthesize `Algebra R A ... ...`, it will tell us how to retrieve the instance-implicit arguments. TODO: - Impact on Mathlib. - Document changes. --------- Co-authored-by: Kim Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
65 lines
2.4 KiB
Text
65 lines
2.4 KiB
Text
/-
|
|
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura
|
|
-/
|
|
prelude
|
|
import Lean.Environment
|
|
|
|
namespace Lean
|
|
|
|
/--
|
|
Given a structure `S`, Lean automatically creates an auxiliary definition (projection function)
|
|
for each field. This structure caches information about these auxiliary definitions.
|
|
-/
|
|
structure ProjectionFunctionInfo where
|
|
/-- Constructor associated with the auxiliary projection function. -/
|
|
ctorName : Name
|
|
/-- Number of parameters in the structure -/
|
|
numParams : Nat
|
|
/-- The field index associated with the auxiliary projection function. -/
|
|
i : Nat
|
|
/-- `true` if the structure is a class. -/
|
|
fromClass : Bool
|
|
deriving Inhabited, Repr
|
|
|
|
@[export lean_mk_projection_info]
|
|
def mkProjectionInfoEx (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : ProjectionFunctionInfo :=
|
|
{ ctorName, numParams, i, fromClass }
|
|
@[export lean_projection_info_from_class]
|
|
def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool :=
|
|
info.fromClass
|
|
|
|
builtin_initialize projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo ← mkMapDeclarationExtension
|
|
|
|
@[export lean_add_projection_info]
|
|
def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : Environment :=
|
|
projectionFnInfoExt.insert env projName { ctorName, numParams, i, fromClass }
|
|
|
|
namespace Environment
|
|
|
|
@[export lean_get_projection_info]
|
|
def getProjectionFnInfo? (env : Environment) (projName : Name) : Option ProjectionFunctionInfo :=
|
|
projectionFnInfoExt.find? env projName
|
|
|
|
def isProjectionFn (env : Environment) (declName : Name) : Bool :=
|
|
projectionFnInfoExt.contains env declName
|
|
|
|
/-- If `projName` is the name of a projection function, return the associated structure name -/
|
|
def getProjectionStructureName? (env : Environment) (projName : Name) : Option Name :=
|
|
match env.getProjectionFnInfo? projName with
|
|
| none => none
|
|
| some projInfo =>
|
|
match env.find? projInfo.ctorName with
|
|
| some (ConstantInfo.ctorInfo val) => some val.induct
|
|
| _ => none
|
|
|
|
end Environment
|
|
|
|
def isProjectionFn [MonadEnv m] [Monad m] (declName : Name) : m Bool :=
|
|
return (← getEnv).isProjectionFn declName
|
|
|
|
def getProjectionFnInfo? [MonadEnv m] [Monad m] (declName : Name) : m (Option ProjectionFunctionInfo) :=
|
|
return (← getEnv).getProjectionFnInfo? declName
|
|
|
|
end Lean
|