From 8fa822b2e657400b1c7a614943b4a85b8ca43af1 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 28 Jun 2026 14:39:14 -0500 Subject: [PATCH] Improve performance by caching CFG building Co-Authored-By: Claude Opus 4.8 --- lean/Spa/Language.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/lean/Spa/Language.lean b/lean/Spa/Language.lean index f42f75c..ae9f4a6 100644 --- a/lean/Spa/Language.lean +++ b/lean/Spa/Language.lean @@ -10,11 +10,19 @@ namespace Spa structure Program where 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 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 abbrev State : Type := p.cfg.Index