Move predecessor computation into Graphs

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Language.agda

@@ -11,8 +11,6 @@ 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⁺)
-open import Data.List.Relation.Unary.All using (All; []; _∷_)
-open import Data.List.Relation.Unary.Any as RelAny using ()
 open import Data.Nat using (ℕ; suc)
 open import Data.Product using (_,_; Σ; proj₁; proj₂)
 open import Data.Product.Properties as ProdProp using ()
@@ -28,28 +26,6 @@ open import Lattice.MapSet _≟ˢ_ using ()
         ; to-List to to-Listˢ
         )
 
-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'
-
-    indices : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
-    indices 0 = ([] , Utils.empty)
-    indices (suc n') =
-        let
-            (inds' , unids') = indices n'
-        in
-            ( zero ∷ List.map suc inds'
-            , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
-            )
-
-    indices-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (indices n))
-    indices-complete (suc n') zero = RelAny.here refl
-    indices-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (indices-complete n' f'))
-
 record Program : Set where
     field
         rootStmt : Stmt
@@ -77,13 +53,13 @@ record Program : Set where
     vars-Unique = proj₂ vars-Set
 
     states : List State
-    states = proj₁ (indices (Graph.size graph))
+    states = indices graph
 
     states-complete : ∀ (s : State) → s ListMem.∈ states
-    states-complete = indices-complete (Graph.size graph)
+    states-complete = indices-complete graph
 
     states-Unique : Unique states
-    states-Unique = proj₂ (indices (Graph.size graph))
+    states-Unique = indices-Unique graph
 
     code : State → List BasicStmt
     code st = graph [ st ]
@@ -100,7 +76,7 @@ record Program : Set where
     open import Data.List.Membership.DecPropositional _≟ᵉ_ using (_∈?_)
 
     incoming : State → List State
-    incoming idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges graph)) states
+    incoming = predecessors graph
 
     edge⇒incoming : ∀ {s₁ s₂ : State} → (s₁ , s₂) ListMem.∈ (Graph.edges graph) →
                     s₁ ListMem.∈ (incoming s₂)

Language/Graphs.agda

@@ -7,15 +7,19 @@ 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.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 (_×_; Σ; _,_)
+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 (x∈xs⇒fx∈fxs; ∈-cartesianProduct)
+open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct)
 
 record Graph : Set where
     constructor MkGraph
@@ -120,3 +124,40 @@ 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