Implement graph construction using <*>, map, and update.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-04-07 20:26:38 -07:00
parent d4b0796715
commit 195537fe15

View File

@ -182,6 +182,20 @@ module Graphs where
with (g'' , (t₂ , g'⊆g'')) f₂ g' =
(g'' , ((Relaxable.relax r g'⊆g'' t₁ , t₂) , ⊆-trans g⊆g' g'⊆g''))
infixl 2 _update_
_update_ : {T : Graph Set} {{ TRelaxable : Relaxable T }}
MonotonicGraphFunction T ( (g : Graph) T g Σ Graph (λ g' g g'))
MonotonicGraphFunction T
_update_ {{r}} f mod g
with (g' , (t , g⊆g')) f g
with (g'' , g'⊆g'') mod g' t =
(g'' , ((Relaxable.relax r g'⊆g'' t , ⊆-trans g⊆g' g'⊆g'')))
infixl 2 _map_
_map_ : {T₁ T₂ : Graph Set}
MonotonicGraphFunction T₁ ( (g : Graph) T₁ g T₂ g)
MonotonicGraphFunction T₂
_map_ f fn g = let (g' , (t₁ , g⊆g')) = f g in (g' , (fn g' t₁ , g⊆g'))
module Construction where
pushBasicBlock : List BasicStmt MonotonicGraphFunction Graph.Index
@ -196,9 +210,29 @@ module Graphs where
in
(g₁ g' , (Graph.size g₁ ↑ʳ zero , (g' , refl)))
addEdges : (g : Graph) List (Graph.Edge g) Σ Graph (λ g' g g')
addEdges g es = {!!}
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) []) })
map (λ { g ((idx₁ , idx₂) , idx , idx') (idx , idx') })
-- open Relaxable {{...}} public
open import Lattice.MapSet _≟ˢ_