333f7573d7
This PR fixes an issue where uses of 'noncomputable' definitions can get incorrectly compiled, while also removing the use of 'noncomputable' definitions altogether. Some uses of 'noncomputable' definitions (e.g. Classical.propDecidable) do not get compiled correctly by type erasure. Running the optimizer on the result can lead to them being optimized away, eluding the later IR-level check for uses of noncomputable definitions. To fix this, we add a 'noncomputable' check earlier in the erase_irrelevant pass.
24 lines
778 B
Text
24 lines
778 B
Text
/-
|
|
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura
|
|
-/
|
|
prelude
|
|
import Lean.EnvExtension
|
|
|
|
namespace Lean
|
|
|
|
builtin_initialize noncomputableExt : TagDeclarationExtension ← mkTagDeclarationExtension
|
|
|
|
/-- Mark in the environment extension that the given declaration has been declared by the user as `noncomputable`. -/
|
|
def addNoncomputable (env : Environment) (declName : Name) : Environment :=
|
|
noncomputableExt.tag env declName
|
|
|
|
/--
|
|
Return true iff the user has declared the given declaration as `noncomputable`.
|
|
-/
|
|
@[export lean_is_noncomputable]
|
|
def isNoncomputable (env : Environment) (declName : Name) : Bool :=
|
|
noncomputableExt.isTagged env declName
|
|
|
|
end Lean
|