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

perf: make function types object rather than tobject (#9461)

Browse source
This commit is contained in:
Cameron Zwarich 2025-07-21 18:16:45 -07:00 • committed by GitHub
parent 30ca6c82e0
commit 6f5532f069
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Compiler/IR/ToIRType.lean
View file

@ -82,7 +82,7 @@ def toIRType (type : Lean.Expr) : CoreM IRType := do
-- All mono types are in headBeta form.
let .const name _ := type.getAppFn | unreachable!
nameToIRType name
| .forallE .. => return .tobject
| .forallE .. => return .object
| .mdata _ b => toIRType b
| _ => unreachable!

8
tests/lean/computedFieldsCode.lean.expected.out
View file

@ -1,5 +1,5 @@
[Compiler.IR] [result]
def Exp.casesOn._override._redArg (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : @& tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) : tobj :=
def Exp.casesOn._override._redArg (x_1 : tobj) (x_2 : obj) (x_3 : obj) (x_4 : @& tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) : tobj :=
case x_1 : tobj of
Exp.var._impl →
dec x_3;
@ -42,7 +42,7 @@
dec x_2;
inc x_8;
ret x_8
def Exp.casesOn._override (x_1 : ◾) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) (x_9 : @& tobj) : tobj :=
def Exp.casesOn._override (x_1 : ◾) (x_2 : tobj) (x_3 : obj) (x_4 : obj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) (x_9 : @& tobj) : tobj :=
case x_2 : tobj of
Exp.var._impl →
dec x_4;
@ -85,7 +85,7 @@
dec x_3;
inc x_9;
ret x_9
def Exp.casesOn._override._redArg._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) : tobj :=
def Exp.casesOn._override._redArg._boxed (x_1 : tobj) (x_2 : obj) (x_3 : obj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) : tobj :=
let x_9 : tobj := Exp.casesOn._override._redArg x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8;
dec x_8;
dec x_7;
@ -93,7 +93,7 @@
dec x_5;
dec x_4;
ret x_9
def Exp.casesOn._override._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) (x_9 : tobj) : tobj :=
def Exp.casesOn._override._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : obj) (x_4 : obj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) (x_9 : tobj) : tobj :=
let x_10 : tobj := Exp.casesOn._override x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9;
dec x_9;
dec x_8;