DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Improve performance by caching CFG building

Browse Source 
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
Danila Fedorin
2026-06-28 14:39:14 -05:00
parent d66a7d0e3e
commit 8fa822b2e6
1 changed files with 8 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
lean/Spa/Language.lean
View File

@@ -10,11 +10,19 @@ namespace Spa
structure Program where structure Program where
rootStmt : Stmt rootStmt : Stmt
/-- A memoized copy of the control-flow graph. This field is an
implementation detail to avoid re-computing `Graph.wrap` and `Stmt.cfg`
every time the program's control flow graph is needed -/
cfgCache : Thunk Graph := Thunk.mk fun _ => Graph.wrap rootStmt.cfg
namespace Program namespace Program
variable (p : Program) variable (p : Program)
-- Runtime implementation of `cfg`: read the memoized graph.
private def cfgImpl : Graph := p.cfgCache.get
@[implemented_by cfgImpl]
def cfg : Graph := Graph.wrap p.rootStmt.cfg def cfg : Graph := Graph.wrap p.rootStmt.cfg
abbrev State : Type := p.cfg.Index abbrev State : Type := p.cfg.Index