max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: rename lowerEnumToScalarType to lowerEnumToScalarType? (#9063)

Browse source
This commit is contained in:
Cameron Zwarich 2025-06-28 08:52:11 -07:00 • committed by GitHub
parent 5ca6eadd50
commit 5144a3bf74
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Compiler/IR/ToIR.lean
View file

@ -75,7 +75,7 @@ def lowerLitValue (v : LCNF.LitValue) : LitVal :=
builtin_initialize scalarTypeExt : LCNF.CacheExtension Name (Option IRType) ←
LCNF.CacheExtension.register
def lowerEnumToScalarType (name : Name) : M (Option IRType) := do
def lowerEnumToScalarType? (name : Name) : M (Option IRType) := do
match (← scalarTypeExt.find? name) with
| some info? => return info?
| none =>
@ -114,14 +114,14 @@ def lowerType (e : Lean.Expr) : M IRType := do
| ``Float32 => return .float32
| ``lcErased => return .irrelevant
| _ =>
if let some scalarType ← lowerEnumToScalarType name then
if let some scalarType ← lowerEnumToScalarType? name then
return scalarType
else
return .object
| .app f _ =>
-- All mono types are in headBeta form.
if let .const name _ := f then
if let some scalarType ← lowerEnumToScalarType name then
if let some scalarType ← lowerEnumToScalarType? name then
return scalarType
else
return .object
@ -288,7 +288,7 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
return code
else
mkExpr (.fap name irArgs)
else if let some scalarType ← lowerEnumToScalarType ctorVal.name then
else if let some scalarType ← lowerEnumToScalarType? ctorVal.name then
assert! args.isEmpty
let var ← bindVar decl.fvarId
return .vdecl var scalarType (.lit (.num ctorVal.cidx)) (← lowerCode k)