175 lines
7.1 KiB
Plaintext
175 lines
7.1 KiB
Plaintext
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 (∈-filter⁺; ∈-filter⁻)
|
||
open import Data.List.Relation.Unary.All using (All; []; _∷_)
|
||
open import Data.List.Relation.Unary.Any as RelAny using ()
|
||
open import Data.Nat as Nat using (ℕ; suc)
|
||
open import Data.Nat.Properties using (+-assoc; +-comm)
|
||
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
|
||
open import Data.Product.Properties as ProdProp 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 Relation.Nullary using (¬_)
|
||
|
||
open import Lattice
|
||
open import Utils using (Unique; push; Unique-map; 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_
|
||
_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)
|
||
|
||
private
|
||
z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
|
||
z≢sf f ()
|
||
|
||
z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (List.map suc fs)
|
||
z≢mapsfs [] = []
|
||
z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
|
||
|
||
finValues : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
|
||
finValues 0 = ([] , Utils.empty)
|
||
finValues (suc n') =
|
||
let
|
||
(inds' , unids') = finValues n'
|
||
in
|
||
( zero ∷ List.map suc inds'
|
||
, push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
|
||
)
|
||
|
||
finValues-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (finValues n))
|
||
finValues-complete (suc n') zero = RelAny.here refl
|
||
finValues-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (finValues-complete n' f'))
|
||
|
||
module _ (g : Graph) where
|
||
open import Data.List.Membership.DecPropositional (ProdProp.≡-dec (FinProp._≟_ {Graph.size g}) (FinProp._≟_ {Graph.size g})) using (_∈?_)
|
||
|
||
indices : List (Graph.Index g)
|
||
indices = proj₁ (finValues (Graph.size g))
|
||
|
||
indices-complete : ∀ (idx : (Graph.Index g)) → idx ListMem.∈ indices
|
||
indices-complete = finValues-complete (Graph.size g)
|
||
|
||
indices-Unique : Unique indices
|
||
indices-Unique = proj₂ (finValues (Graph.size g))
|
||
|
||
predecessors : (Graph.Index g) → List (Graph.Index g)
|
||
predecessors idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges g)) indices
|
||
|
||
edge⇒predecessor : ∀ {idx₁ idx₂ : Graph.Index g} → (idx₁ , idx₂) ListMem.∈ (Graph.edges g) →
|
||
idx₁ ListMem.∈ (predecessors idx₂)
|
||
edge⇒predecessor {idx₁} {idx₂} idx₁,idx₂∈es =
|
||
∈-filter⁺ (λ idx' → (idx' , idx₂) ∈? (Graph.edges g))
|
||
(indices-complete idx₁) idx₁,idx₂∈es
|
||
|
||
predecessor⇒edge : ∀ {idx₁ idx₂ : Graph.Index g} → idx₁ ListMem.∈ (predecessors idx₂) →
|
||
(idx₁ , idx₂) ListMem.∈ (Graph.edges g)
|
||
predecessor⇒edge {idx₁} {idx₂} idx₁∈pred =
|
||
proj₂ (∈-filter⁻ (λ idx' → (idx' , idx₂) ∈? (Graph.edges g)) {v = idx₁} {xs = indices} idx₁∈pred )
|