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

Fix up Graph construction

Browse Source
This commit is contained in:
Danila Fedorin 2024-04-27 13:50:06 -07:00
parent f2b8084a9c
commit 037358308f
1 changed files with 13 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
Language/Graphs.agda
View File

@ -79,13 +79,19 @@ _↦_ g₁ g₂ = record
} }
loop : Graph → Graph loop : Graph → Graph
loop g = record loop g = record g
{ size = Graph.size g { edges = Graph.edges g List.++
; nodes = Graph.nodes g
; edges = Graph.edges g List.++
List.cartesianProduct (Graph.outputs g) (Graph.inputs g) List.cartesianProduct (Graph.outputs g) (Graph.inputs g)
; inputs = Graph.inputs g }
; outputs = Graph.outputs g
infixl 5 _skipto_
_skipto_ : Graph → Graph → Graph
_skipto_ g₁ g₂ = record (g₁ ∙ g₂)
{ edges = Graph.edges (g₁ ∙ g₂) List.++
(List.cartesianProduct (Graph.inputs g₁ ↑ˡⁱ Graph.size g₂)
(Graph.size g₁ ↑ʳⁱ Graph.inputs g₂))
; inputs = Graph.inputs g₁ ↑ˡⁱ Graph.size g₂
; outputs = Graph.size g₁ ↑ʳⁱ Graph.inputs g₂
} }
_[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt _[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt
@ -104,4 +110,4 @@ buildCfg : Stmt → Graph
buildCfg ⟨ bs₁ ⟩ = singleton (bs₁ ∷ []) buildCfg ⟨ bs₁ ⟩ = singleton (bs₁ ∷ [])
buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂ buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
buildCfg (if _ then s₁ else s₂) = singleton [] ↦ (buildCfg s₁ ∙ buildCfg s₂) ↦ singleton [] buildCfg (if _ then s₁ else s₂) = singleton [] ↦ (buildCfg s₁ ∙ buildCfg s₂) ↦ singleton []
buildCfg (while _ repeat s) = loop (buildCfg s ↦ singleton []) buildCfg (while _ repeat s) = (loop (singleton [] ↦ buildCfg s)) skipto (singleton [])