Remove nested module from Graphs
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
de956cdc6a
commit
fc27b045d3
|
@ -52,7 +52,7 @@ record Program : Set where
|
|||
rootStmt : Stmt
|
||||
|
||||
private
|
||||
buildResult = Construction.buildCfg rootStmt empty
|
||||
buildResult = buildCfg rootStmt empty
|
||||
|
||||
graph : Graph
|
||||
graph = proj₁ buildResult
|
||||
|
|
|
@ -220,61 +220,60 @@ always P m = ∀ g₁ → let (g₂ , t , _) = m g₁ in P g₂ t
|
|||
with q ← aQ g'
|
||||
with (g'' , (t₂ , g'⊆g'')) ← m₂ g' = (P-Mono _ _ _ g'⊆g'' p , q)
|
||||
|
||||
module Construction where
|
||||
pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index
|
||||
pushBasicBlock bss g =
|
||||
( record
|
||||
{ size = Graph.size g Nat.+ 1
|
||||
; nodes = Graph.nodes g ++ (bss ∷ [])
|
||||
; edges = List.map (λ e → ↑ˡ-Edge e 1) (Graph.edges g)
|
||||
}
|
||||
, ( Graph.size g ↑ʳ zero
|
||||
, record
|
||||
{ n = 1
|
||||
; sg₂≡sg₁+n = refl
|
||||
; newNodes = (bss ∷ [])
|
||||
; nsg₂≡nsg₁++newNodes = cast-is-id refl _
|
||||
; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e → ↑ˡ-Edge e 1) e∈g₁
|
||||
}
|
||||
)
|
||||
)
|
||||
pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index
|
||||
pushBasicBlock bss g =
|
||||
( record
|
||||
{ size = Graph.size g Nat.+ 1
|
||||
; nodes = Graph.nodes g ++ (bss ∷ [])
|
||||
; edges = List.map (λ e → ↑ˡ-Edge e 1) (Graph.edges g)
|
||||
}
|
||||
, ( Graph.size g ↑ʳ zero
|
||||
, record
|
||||
{ n = 1
|
||||
; sg₂≡sg₁+n = refl
|
||||
; newNodes = (bss ∷ [])
|
||||
; nsg₂≡nsg₁++newNodes = cast-is-id refl _
|
||||
; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e → ↑ˡ-Edge e 1) e∈g₁
|
||||
}
|
||||
)
|
||||
)
|
||||
|
||||
addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g')
|
||||
addEdges (MkGraph s ns es) es' =
|
||||
( record
|
||||
{ size = s
|
||||
; nodes = ns
|
||||
; edges = es' List.++ es
|
||||
}
|
||||
, record
|
||||
{ n = 0
|
||||
; sg₂≡sg₁+n = +-comm 0 s
|
||||
; newNodes = []
|
||||
; nsg₂≡nsg₁++newNodes = cast-sym _ (++-identityʳ (+-comm s 0) ns)
|
||||
; e∈g₁⇒e∈g₂ = λ {e} e∈es →
|
||||
cast∈⇒∈subst (+-comm s 0) (+-comm 0 s) _ _
|
||||
(subst (λ e' → e' ListMem.∈ _)
|
||||
(↑ˡ-Edge-identityʳ e (+-comm s 0))
|
||||
(ListMemProp.∈-++⁺ʳ es' e∈es))
|
||||
}
|
||||
)
|
||||
addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g')
|
||||
addEdges (MkGraph s ns es) es' =
|
||||
( record
|
||||
{ size = s
|
||||
; nodes = ns
|
||||
; edges = es' List.++ es
|
||||
}
|
||||
, record
|
||||
{ n = 0
|
||||
; sg₂≡sg₁+n = +-comm 0 s
|
||||
; newNodes = []
|
||||
; nsg₂≡nsg₁++newNodes = cast-sym _ (++-identityʳ (+-comm s 0) ns)
|
||||
; e∈g₁⇒e∈g₂ = λ {e} e∈es →
|
||||
cast∈⇒∈subst (+-comm s 0) (+-comm 0 s) _ _
|
||||
(subst (λ e' → e' ListMem.∈ _)
|
||||
(↑ˡ-Edge-identityʳ e (+-comm s 0))
|
||||
(ListMemProp.∈-++⁺ʳ es' e∈es))
|
||||
}
|
||||
)
|
||||
|
||||
pushEmptyBlock : MonotonicGraphFunction Graph.Index
|
||||
pushEmptyBlock = pushBasicBlock []
|
||||
pushEmptyBlock : MonotonicGraphFunction Graph.Index
|
||||
pushEmptyBlock = pushBasicBlock []
|
||||
|
||||
buildCfg : Stmt → MonotonicGraphFunction (Graph.Index ⊗ Graph.Index)
|
||||
buildCfg ⟨ bs₁ ⟩ = pushBasicBlock (bs₁ ∷ []) map (λ g idx → (idx , idx))
|
||||
buildCfg (s₁ then s₂) =
|
||||
(buildCfg s₁ ⟨⊗⟩ buildCfg s₂)
|
||||
update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → addEdges g ((idx₂ , idx₃) ∷ []) })
|
||||
map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → (idx₁ , idx₄) })
|
||||
buildCfg (if _ then s₁ else s₂) =
|
||||
(buildCfg s₁ ⟨⊗⟩ buildCfg s₂ ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock)
|
||||
update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') →
|
||||
addEdges g ((idx , idx₁) ∷ (idx , idx₃) ∷ (idx₂ , idx') ∷ (idx₄ , idx') ∷ []) })
|
||||
map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') → (idx , idx') })
|
||||
buildCfg (while _ repeat s) =
|
||||
(buildCfg s ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock)
|
||||
update (λ { g ((idx₁ , idx₂) , idx , idx') →
|
||||
addEdges g ((idx , idx') ∷ (idx , idx₁) ∷ (idx₂ , idx) ∷ []) })
|
||||
map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') })
|
||||
buildCfg : Stmt → MonotonicGraphFunction (Graph.Index ⊗ Graph.Index)
|
||||
buildCfg ⟨ bs₁ ⟩ = pushBasicBlock (bs₁ ∷ []) map (λ g idx → (idx , idx))
|
||||
buildCfg (s₁ then s₂) =
|
||||
(buildCfg s₁ ⟨⊗⟩ buildCfg s₂)
|
||||
update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → addEdges g ((idx₂ , idx₃) ∷ []) })
|
||||
map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → (idx₁ , idx₄) })
|
||||
buildCfg (if _ then s₁ else s₂) =
|
||||
(buildCfg s₁ ⟨⊗⟩ buildCfg s₂ ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock)
|
||||
update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') →
|
||||
addEdges g ((idx , idx₁) ∷ (idx , idx₃) ∷ (idx₂ , idx') ∷ (idx₄ , idx') ∷ []) })
|
||||
map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') → (idx , idx') })
|
||||
buildCfg (while _ repeat s) =
|
||||
(buildCfg s ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock)
|
||||
update (λ { g ((idx₁ , idx₂) , idx , idx') →
|
||||
addEdges g ((idx , idx') ∷ (idx , idx₁) ∷ (idx₂ , idx) ∷ []) })
|
||||
map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') })
|
||||
|
|
Loading…
Reference in New Issue
Block a user