Skip to content

refactor: port EmitC to LCNF #12781

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hargoniX merged 15 commits into from
Mar 11, 2026
Merged

refactor: port EmitC to LCNF #12781

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
0fc0c56
step1
hargoniX Mar 3, 2026
88869a0
step2
hargoniX Mar 3, 2026
4557819
step3
hargoniX Mar 9, 2026
2168e82
maybe better?
hargoniX Mar 9, 2026
d4dc12b
needs more caches
hargoniX Mar 9, 2026
c6b18f7
needs more sharing
hargoniX Mar 9, 2026
33a1a32
ahhhh
hargoniX Mar 9, 2026
795dee9
properly sorted at last
hargoniX Mar 10, 2026
a5d3588
chore: delete unused files
hargoniX Mar 10, 2026
f3d530b
bounds checks
hargoniX Mar 10, 2026
1f24b7c
microoptimization
hargoniX Mar 10, 2026
68b7955
chore: remove second decl check
hargoniX Mar 10, 2026
40ebc7d
later
hargoniX Mar 11, 2026
b069354
remove script
hargoniX Mar 11, 2026
f47aad8
indent proper
hargoniX Mar 11, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions src/Lean/Compiler/IR.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ public import Lean.Compiler.IR.CompilerM
public import Lean.Compiler.IR.NormIds
public import Lean.Compiler.IR.Checker
public import Lean.Compiler.IR.UnboxResult
public import Lean.Compiler.IR.EmitC
public import Lean.Compiler.IR.Sorry
public import Lean.Compiler.IR.ToIR
public import Lean.Compiler.IR.ToIRType
Expand All @@ -34,7 +33,6 @@ def compile (decls : Array Decl) : CompilerM (Array Decl) := do
let mut decls := decls
decls ← updateSorryDep decls
logDecls `result decls
checkDecls decls
addDecls decls
inferMeta decls
return decls
Expand Down
3 changes: 3 additions & 0 deletions src/Lean/Compiler/IR/AddExtern.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,9 @@ where
decl.saveImpure
let decls ← Compiler.LCNF.addBoxedVersions #[decl]
let decls ← Compiler.LCNF.runExplicitRc decls
for decl in decls do
decl.saveImpure
modifyEnv fun env => Compiler.LCNF.recordFinalImpureDecl env decl.name
return decls

addIr (decls : Array (Compiler.LCNF.Decl .impure)) : CoreM Unit := do
Expand Down
Loading
Loading