f0a11b8864
types like
```
inductive Many (α : Type u) where
| none : Many α
| more : α → (Unit → Many α) → Many α
```
have a `.brecOn` only supports motives producing `Type u`, but not `Sort
u`, but our induction principles produce `Prop`. So the previous
implementation of functional induction would fail for functions that
structurally recurse over such types.
We recognize this case now and, rather hazardously, replace `.brecOn`
with `.binductionOn` (and thus `.below ` with `.ibelow` and `PProd` with
`And`). This assumes that these definitions are highly analogous.
This also improves the error message when realizing a reserved name
fails with an exception, by prepending
```
Failed to realize constant {id}:
```
to the error message.
Fixes #4320
86 lines
2.9 KiB
Text
86 lines
2.9 KiB
Text
/-
|
||
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Leonardo de Moura
|
||
-/
|
||
prelude
|
||
import Lean.CoreM
|
||
|
||
namespace Lean
|
||
|
||
/--
|
||
When trying to resolve a reserved name, an action can be executed to generate the actual definition/theorem.
|
||
The action returns `true` if it "handled" the given name.
|
||
|
||
Remark: usually when one install a reserved name predicate, an associated action is also installed.
|
||
-/
|
||
def ReservedNameAction := Name → CoreM Bool
|
||
|
||
private builtin_initialize reservedNameActionsRef : IO.Ref (Array ReservedNameAction) ← IO.mkRef #[]
|
||
|
||
/--
|
||
Register a new function that is invoked when trying to resolve a reserved name.
|
||
-/
|
||
def registerReservedNameAction (act : ReservedNameAction) : IO Unit := do
|
||
unless (← initializing) do
|
||
throw (IO.userError "failed to register reserved name action, this kind of extension can only be registered during initialization")
|
||
reservedNameActionsRef.modify (·.push act)
|
||
|
||
/--
|
||
Execute a registered reserved action for the given reserved name.
|
||
Note that the handler can throw an exception.
|
||
-/
|
||
def executeReservedNameAction (name : Name) : CoreM Unit := do
|
||
for act in (← reservedNameActionsRef.get) do
|
||
if (← act name) then
|
||
return ()
|
||
|
||
/--
|
||
Similar to `resolveGlobalName`, but also executes reserved name actions.
|
||
-/
|
||
def realizeGlobalName (id : Name) : CoreM (List (Name × List String)) := do
|
||
let cs ← resolveGlobalName id
|
||
cs.filterM fun (c, _) => do
|
||
if (← getEnv).contains c then
|
||
return true
|
||
else
|
||
try
|
||
executeReservedNameAction c
|
||
return (← getEnv).contains c
|
||
catch ex =>
|
||
-- We record the error produced by the reserved name action generator
|
||
logError m!"Failed to realize constant {id}:{indentD ex.toMessageData}"
|
||
return false
|
||
|
||
/--
|
||
Similar to `resolveGlobalConstCore`, but also executes reserved name actions.
|
||
-/
|
||
def realizeGlobalConstCore (n : Name) : CoreM (List Name) := do
|
||
let cs ← realizeGlobalName n
|
||
filterFieldList n cs
|
||
|
||
/--
|
||
Similar to `realizeGlobalConstNoOverloadCore`, but also executes reserved name actions.
|
||
-/
|
||
def realizeGlobalConstNoOverloadCore (n : Name) : CoreM Name := do
|
||
ensureNoOverload n (← realizeGlobalConstCore n)
|
||
|
||
/--
|
||
Similar to `resolveGlobalConst`, but also executes reserved name actions.
|
||
|
||
Consider using `realizeGlobalConstWithInfo` if you want the syntax to show the resulting name's info
|
||
on hover.
|
||
-/
|
||
def realizeGlobalConst (stx : Syntax) : CoreM (List Name) :=
|
||
withRef stx do preprocessSyntaxAndResolve stx realizeGlobalConstCore
|
||
|
||
/--
|
||
Similar to `realizeGlobalConstNoOverload`, but also executes reserved name actions.
|
||
|
||
Consider using `realizeGlobalConstNoOverloadWithInfo` if you want the syntax to show the resulting
|
||
name's info on hover.
|
||
-/
|
||
def realizeGlobalConstNoOverload (id : Syntax) : CoreM Name := do
|
||
ensureNonAmbiguous id (← realizeGlobalConst id)
|
||
|
||
end Lean
|