Language.agda

@@ -52,7 +52,7 @@ record Program : Set where
         rootStmt : Stmt
 
     private
-        buildResult = buildCfg rootStmt empty
+        buildResult = Construction.buildCfg rootStmt empty
 
     graph : Graph
     graph = proj₁ buildResult

Language/Graphs.agda

@@ -110,7 +110,8 @@ cast∈⇒∈subst refl refl (idx₁ , idx₂) es e∈es
                                 (e∈g₂⇒e∈g₃ (e∈g₁⇒e∈g₂ e∈g₁)))
         }
 
-open import MonotonicState _⊆_ ⊆-trans renaming (MonotonicState to MonotonicGraphFunction)
+record Relaxable (T : Graph → Set) : Set where
+    field relax : ∀ {g₁ g₂ : Graph} → g₁ ⊆ g₂ → T g₁ → T g₂
 
 instance
     IndexRelaxable : Relaxable Graph.Index
@@ -126,7 +127,17 @@ instance
             )
         }
 
-open Relaxable {{...}}
+    ProdRelaxable : ∀ {P : Graph → Set} {Q : Graph → Set} →
+                    {{ PRelaxable : Relaxable P }} → {{ QRelaxable : Relaxable Q }} →
+                    Relaxable (P ⊗ Q)
+    ProdRelaxable {{pr}} {{qr}} = record
+        { relax = (λ { g₁⊆g₂ (p , q) →
+            ( Relaxable.relax pr g₁⊆g₂ p
+            , Relaxable.relax qr g₁⊆g₂ q) }
+            )
+        }
+
+open Relaxable {{...}} public
 
 relax-preserves-[]≡ : ∀ (g₁ g₂ : Graph) (g₁⊆g₂ : g₁ ⊆ g₂) (idx : Graph.Index g₁) →
                       g₁ [ idx ] ≡ g₂ [ relax g₁⊆g₂ idx ]
@@ -134,60 +145,136 @@ relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl newNodes nsg₂≡nsg₁++newNode
     rewrite cast-is-id refl (Graph.nodes g₂)
     with refl ← nsg₂≡nsg₁++newNodes = sym (lookup-++ˡ (Graph.nodes 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₁
-          }
-      )
-    )
+-- Tools for graph construction. The most important is a 'monotonic function':
+-- one that takes a graph, and produces another graph, such that the
+-- new graph includes all the information from the old one.
 
-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))
-        }
-    )
+MonotonicGraphFunction : (Graph → Set) → Set
+MonotonicGraphFunction T = (g₁ : Graph) → Σ Graph (λ g₂ → T g₂ × g₁ ⊆ g₂)
 
-pushEmptyBlock : MonotonicGraphFunction Graph.Index
-pushEmptyBlock = pushBasicBlock []
+-- Now, define some operations on monotonic functions; these are useful
+-- to save the work of threading intermediate graphs in and out of operations.
 
-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') })
+infixr 2 _⟨⊗⟩_
+_⟨⊗⟩_ : ∀ {T₁ T₂ : Graph → Set} {{ T₁Relaxable : Relaxable T₁ }} →
+      MonotonicGraphFunction T₁ → MonotonicGraphFunction T₂ →
+      MonotonicGraphFunction (T₁ ⊗ T₂)
+_⟨⊗⟩_ {{r}} f₁ f₂ g
+    with (g' , (t₁ , g⊆g')) ← f₁ g
+    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'))
+
+
+-- To reason about monotonic functions and what we do, we need a way
+-- to describe values they produce. A 'graph-value predicate' is
+-- just a predicate for some (dependent) value.
+
+GraphValuePredicate : (Graph → Set) → Set₁
+GraphValuePredicate T = ∀ (g : Graph) → T g → Set
+
+Both : {T₁ T₂ : Graph → Set} → GraphValuePredicate T₁ → GraphValuePredicate T₂ →
+       GraphValuePredicate (T₁ ⊗ T₂)
+Both P Q = (λ { g (t₁ , t₂) → (P g t₁ × Q g t₂) })
+
+-- Since monotnic functions keep adding on to a function, proofs of
+-- graph-value predicates go stale fast (they describe old values of
+-- the graph). To keep propagating them through, we need them to still
+-- on 'bigger graphs'. We call such predicates monotonic as well, since
+-- they respect the ordering of graphs.
+
+MonotonicPredicate : ∀ {T : Graph → Set} {{ TRelaxable : Relaxable T }} →
+                     GraphValuePredicate T → Set
+MonotonicPredicate {T} P = ∀ (g₁ g₂ : Graph) (t₁ : T g₁) (g₁⊆g₂ : g₁ ⊆ g₂) →
+                           P g₁ t₁ → P g₂ (relax g₁⊆g₂ t₁)
+
+
+-- A 'map' has a certain property if its ouputs satisfy that property
+-- for all inputs.
+
+always : ∀ {T : Graph → Set} → GraphValuePredicate T → MonotonicGraphFunction T → Set
+always P m = ∀ g₁ → let (g₂ , t , _) = m g₁ in P g₂ t
+
+⟨⊗⟩-reason : ∀ {T₁ T₂ : Graph → Set} {{ T₁Relaxable : Relaxable T₁ }}
+             {P : GraphValuePredicate T₁} {Q : GraphValuePredicate T₂}
+             {P-Mono : MonotonicPredicate P}
+             {m₁ : MonotonicGraphFunction T₁} {m₂ : MonotonicGraphFunction T₂} →
+             always P m₁ → always Q m₂ → always (Both P Q) (m₁ ⟨⊗⟩ m₂)
+⟨⊗⟩-reason {P-Mono = P-Mono} {m₁ = m₁} {m₂ = m₂} aP aQ g
+    with p ← aP g
+    with (g' , (t₁ , g⊆g')) ← m₁ g
+    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₁
+              }
+          )
+        )
+
+    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 []
+
+    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') })

MonotonicState.agda

@@ -1,116 +0,0 @@
-open import Agda.Primitive using (lsuc)
-
-module MonotonicState {s} {S : Set s}
-                      (_≼_ : S → S → Set s)
-                      (≼-trans : ∀ {s₁ s₂ s₃ : S} → s₁ ≼ s₂ → s₂ ≼ s₃ → s₁ ≼ s₃) where
-
-open import Data.Product using (Σ; _×_; _,_)
-
-open import Utils using (_⊗_; _,_)
-
--- Sometimes, we need a state monad whose values depend on the state. However,
--- one trouble with such monads is that as the state evolves, old values
--- in scope are over the 'old' state, and don't get updated accordingly.
--- Apparently, a related version of this problem is called 'demonic bind'.
---
--- One solution to the problem is to also witness some kind of relationtion
--- between the input and output states. Using this relationship makes it possible
--- to 'bring old values up to speed'.
---
--- Motivated primarily by constructing a Control Flow Graph, the 'relationship'
--- I've chosen is a 'less-than' relation. Thus, 'MonotonicState' is just
--- a (dependent) state "monad" that also witnesses that the state keeps growing.
-
-MonotonicState : (S → Set s) → Set s
-MonotonicState T = (s₁ : S) → Σ S (λ s₂ → T s₂ × s₁ ≼ s₂)
-
--- It's not a given that the (arbitrary) _≼_ relationship can be used for
--- updating old values. The Relaxable typeclass represents type constructor
--- that support the operation.
-
-record Relaxable (T : S → Set s) : Set (lsuc s) where
-    field relax : ∀ {s₁ s₂ : S} → s₁ ≼ s₂ → T s₁ → T s₂
-
-instance
-    ProdRelaxable : ∀ {P : S → Set s} {Q : S → Set s} →
-                    {{ PRelaxable : Relaxable P }} → {{ QRelaxable : Relaxable Q }} →
-                    Relaxable (P ⊗ Q)
-    ProdRelaxable {{pr}} {{qr}} = record
-        { relax = (λ { g₁≼g₂ (p , q) →
-            ( Relaxable.relax pr g₁≼g₂ p
-            , Relaxable.relax qr g₁≼g₂ q) }
-            )
-        }
-
--- In general, the "MonotonicState monad" is not even a monad; it's not
--- even applicative. The trouble is that functions in general cannot be
--- 'relaxed', and to apply an 'old' function to a 'new' value, you'd thus
--- need to un-relax the value (which also isn't possible in general).
---
--- However, we _can_ combine pairs from two functions into a tuple, which
--- would equivalent to the applicative operation if functions were relaxable.
---
--- TODO: Now that I think about it, the swapped version of the applicative
--- operation is possible, since it doesn't require lifting functions.
-
-infixr 4 _⟨⊗⟩_
-_⟨⊗⟩_ : ∀ {T₁ T₂ : S → Set s} {{ _ : Relaxable T₁ }} →
-        MonotonicState T₁ → MonotonicState T₂ → MonotonicState (T₁ ⊗ T₂)
-_⟨⊗⟩_ {{r}} f₁ f₂ s
-    with (s' , (t₁ , s≼s')) ← f₁ s
-    with (s'' , (t₂ , s'≼s'')) ← f₂ s' =
-    (s'' , ((Relaxable.relax r s'≼s'' t₁ , t₂) , ≼-trans s≼s' s'≼s''))
-
-infixl 4 _update_
-_update_ : ∀ {T : S → Set s} {{ _ : Relaxable T }} →
-         MonotonicState T → (∀ (s : S) → T s → Σ S (λ s' → s ≼ s')) →
-         MonotonicState T
-_update_ {{r}} f mod s
-    with (s' , (t , s≼s')) ← f s
-    with (s'' , s'≼s'') ← mod s' t =
-    (s'' , ((Relaxable.relax r s'≼s'' t , ≼-trans s≼s' s'≼s'')))
-
-infixl 4 _map_
-_map_ : ∀ {T₁ T₂ : S → Set s} →
-        MonotonicState T₁ → (∀ (s : S) → T₁ s → T₂ s) → MonotonicState T₂
-_map_ f fn s = let (s' , (t₁ , s≼s')) = f s in (s' , (fn s' t₁ , s≼s'))
-
-
--- To reason about MonotonicState instances, we need predicates over their
--- values. But such values are dependent, so our predicates need to accept
--- the state as argument, too.
-
-DependentPredicate : (S → Set s) → Set (lsuc s)
-DependentPredicate T = ∀ (s₁ : S) → T s₁ → Set s
-
-Both : {T₁ T₂ : S → Set s} → DependentPredicate T₁ → DependentPredicate T₂ →
-       DependentPredicate (T₁ ⊗ T₂)
-Both P Q = (λ { s (t₁ , t₂) → (P s t₁ × Q s t₂) })
-
--- Since monotnic functions keep adding on to the state, proofs of
--- predicates over their outputs go stale fast (they describe old values of
--- the state). To keep them relevant, we need them to still hold on 'bigger
--- states'. We call such predicates monotonic as well, since they respect the
--- ordering relation.
-
-record MonotonicPredicate {T : S → Set s} {{ r : Relaxable T }} (P : DependentPredicate T) : Set s where
-    field relaxPredicate : ∀ (s₁ s₂ : S) (t₁ : T s₁) (s₁≼s₂ : s₁ ≼ s₂) →
-                           P s₁ t₁ → P s₂ (Relaxable.relax r s₁≼s₂ t₁)
-
--- A MonotonicState "monad" m has a certain property if its ouputs satisfy that
--- property for all inputs.
-
-always : ∀ {T : S → Set s} → DependentPredicate T → MonotonicState T → Set s
-always P m = ∀ s₁ → let (s₂ , t , _) = m s₁ in P s₂ t
-
-⟨⊗⟩-reason : ∀ {T₁ T₂ : S → Set s} {{ _ : Relaxable T₁ }}
-             {P : DependentPredicate T₁} {Q : DependentPredicate T₂}
-             {{P-Mono : MonotonicPredicate P}}
-             {m₁ : MonotonicState T₁} {m₂ : MonotonicState T₂} →
-             always P m₁ → always Q m₂ → always (Both P Q) (m₁ ⟨⊗⟩ m₂)
-⟨⊗⟩-reason {{P-Mono = P-Mono}} {m₁ = m₁} {m₂ = m₂} aP aQ s
-    with p ← aP s
-    with (s' , (t₁ , s≼s')) ← m₁ s
-    with q ← aQ s'
-    with (s'' , (t₂ , s'≼s'')) ← m₂ s' =
-    (MonotonicPredicate.relaxPredicate P-Mono _ _ _ s'≼s'' p , q)