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

Slightly tweak LICM implementation

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2026-06-25 14:40:25 -05:00
parent c38c10fe9e
commit 6a6ed521ca
1 changed files with 6 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
lean/Spa/Transformation/Licm.lean
View File

@@ -47,17 +47,17 @@ structure Candidate where
`enclosing` carries the current loop's tag and body id-set, or `none` outside any `enclosing` carries the current loop's tag and body id-set, or `none` outside any
loop (in which case assignments are skipped — only in-loop assignments are loop (in which case assignments are skipped — only in-loop assignments are
candidates). -/ candidates). -/
def collectCandidates : def collectCandidates (enc : Option (NodeId × List NodeId)) :
Option (NodeId × List NodeId) → Stmt.Tagged NodeId → List Candidate Stmt.Tagged NodeId → List Candidate
| enc, .basic _ bs => | .basic _ bs =>
match bs, enc with match bs, enc with
| .assign t _ e, some (loopId, bodyIds) => | .assign t _ e, some (loopId, bodyIds) =>
[{ loopId := loopId, bodyIds := bodyIds, assignId := t, [{ loopId := loopId, bodyIds := bodyIds, assignId := t,
rhsVars := e.erase.vars.sort (· ≤ ·) }] rhsVars := e.erase.vars.sort (· ≤ ·) }]
| _, _ => [] | _, _ => []
| enc, .andThen _ a b => collectCandidates enc a ++ collectCandidates enc b | .andThen _ a b => collectCandidates enc a ++ collectCandidates enc b
| enc, .ifElse _ _ a b => collectCandidates enc a ++ collectCandidates enc b | .ifElse _ _ a b => collectCandidates enc a ++ collectCandidates enc b
| _, .whileLoop loopT _ body => | .whileLoop loopT _ body =>
collectCandidates (some (loopT, body.subtreeIds)) body collectCandidates (some (loopT, body.subtreeIds)) body
/-- Read the definition set assigned to variable `k`, or `⊥` if absent. -/ /-- Read the definition set assigned to variable `k`, or `⊥` if absent. -/