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