agda-spa/Language/Graphs.agda

123 lines
4.6 KiB
Agda
Raw Normal View History

module Language.Graphs where
open import Language.Base using (Expr; Stmt; BasicStmt; ⟨_⟩; _then_; if_then_else_; while_repeat_)
open import Data.Fin as Fin using (Fin; suc; zero)
open import Data.Fin.Properties as FinProp using (suc-injective)
open import Data.List as List using (List; []; _∷_)
open import Data.List.Membership.Propositional as ListMem using ()
open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
open import Data.Nat as Nat using (; suc)
open import Data.Nat.Properties using (+-assoc; +-comm)
open import Data.Product using (_×_; Σ; _,_)
open import Data.Vec using (Vec; []; _∷_; lookup; cast; _++_)
open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-sym; ++-identityʳ; lookup-++ʳ)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans)
open import Lattice
open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct)
record Graph : Set where
constructor MkGraph
field
size :
Index : Set
Index = Fin size
Edge : Set
Edge = Index × Index
field
nodes : Vec (List BasicStmt) size
edges : List Edge
inputs : List Index
outputs : List Index
_↑ˡ_ : {n} (Fin n × Fin n) m (Fin (n Nat.+ m) × Fin (n Nat.+ m))
_↑ˡ_ (idx₁ , idx₂) m = (idx₁ Fin.↑ˡ m , idx₂ Fin.↑ˡ m)
_↑ʳ_ : {m} n (Fin m × Fin m) Fin (n Nat.+ m) × Fin (n Nat.+ m)
_↑ʳ_ n (idx₁ , idx₂) = (n Fin.↑ʳ idx₁ , n Fin.↑ʳ idx₂)
_↑ˡⁱ_ : {n} List (Fin n) m List (Fin (n Nat.+ m))
_↑ˡⁱ_ l m = List.map (Fin._↑ˡ m) l
_↑ʳⁱ_ : {m} n List (Fin m) List (Fin (n Nat.+ m))
_↑ʳⁱ_ n l = List.map (n Fin.↑ʳ_) l
_↑ˡᵉ_ : {n} List (Fin n × Fin n) m List (Fin (n Nat.+ m) × Fin (n Nat.+ m))
_↑ˡᵉ_ l m = List.map (_↑ˡ m) l
_↑ʳᵉ_ : {m} n List (Fin m × Fin m) List (Fin (n Nat.+ m) × Fin (n Nat.+ m))
_↑ʳᵉ_ n l = List.map (n ↑ʳ_) l
infixr 5 _∙_
_∙_ : Graph Graph Graph
_∙_ g₁ g₂ = record
{ size = Graph.size g₁ Nat.+ Graph.size g₂
; nodes = Graph.nodes g₁ ++ Graph.nodes g₂
; edges = (Graph.edges g₁ ↑ˡᵉ Graph.size g₂) List.++
(Graph.size g₁ ↑ʳᵉ Graph.edges g₂)
; inputs = (Graph.inputs g₁ ↑ˡⁱ Graph.size g₂) List.++
(Graph.size g₁ ↑ʳⁱ Graph.inputs g₂)
; outputs = (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂) List.++
(Graph.size g₁ ↑ʳⁱ Graph.outputs g₂)
}
infixr 5 _↦_
_↦_ : Graph Graph Graph
_↦_ g₁ g₂ = record
{ size = Graph.size g₁ Nat.+ Graph.size g₂
; nodes = Graph.nodes g₁ ++ Graph.nodes g₂
; edges = (Graph.edges g₁ ↑ˡᵉ Graph.size g₂) List.++
(Graph.size g₁ ↑ʳᵉ Graph.edges g₂) List.++
(List.cartesianProduct (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂)
(Graph.size g₁ ↑ʳⁱ Graph.inputs g₂))
; inputs = Graph.inputs g₁ ↑ˡⁱ Graph.size g₂
; outputs = Graph.size g₁ ↑ʳⁱ Graph.outputs g₂
}
loop : Graph Graph
loop g = record
{ size = 2 Nat.+ Graph.size g
; nodes = [] [] Graph.nodes g
; edges = (2 ↑ʳᵉ Graph.edges g) List.++
List.map (zero ,_) (2 ↑ʳⁱ Graph.inputs g) List.++
List.map (_, suc zero) (2 ↑ʳⁱ Graph.outputs g) List.++
((suc zero , zero) (zero , suc zero) [])
; inputs = zero []
; outputs = (suc zero) []
}
infixr 5 _skipto_
2024-04-27 13:50:06 -07:00
_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 idx = lookup (Graph.nodes g) idx
singleton : List BasicStmt Graph
singleton bss = record
{ size = 1
; nodes = bss []
; edges = []
; inputs = zero []
; outputs = zero []
}
wrap : Graph Graph
wrap g = singleton [] g singleton []
buildCfg : Stmt Graph
buildCfg bs₁ = singleton (bs₁ [])
buildCfg (s₁ then s₂) = buildCfg s₁ buildCfg s₂
buildCfg (if _ then s₁ else s₂) = singleton [] (buildCfg s₁ buildCfg s₂) singleton []
buildCfg (while _ repeat s) = loop (buildCfg s)