Make 'MonotonicPredicate' into another typeclass

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

Language.agda

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

Language/Graphs.agda

@@ -110,8 +110,7 @@ cast∈⇒∈subst refl refl (idx₁ , idx₂) es e∈es
                                 (e∈g₂⇒e∈g₃ (e∈g₁⇒e∈g₂ e∈g₁)))
         }
 
-record Relaxable (T : Graph → Set) : Set where
-    field relax : ∀ {g₁ g₂ : Graph} → g₁ ⊆ g₂ → T g₁ → T g₂
+open import MonotonicState _⊆_ ⊆-trans renaming (MonotonicState to MonotonicGraphFunction)
 
 instance
     IndexRelaxable : Relaxable Graph.Index
@@ -127,17 +126,7 @@ instance
             )
         }
 
-    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
+open Relaxable {{...}}
 
 relax-preserves-[]≡ : ∀ (g₁ g₂ : Graph) (g₁⊆g₂ : g₁ ⊆ g₂) (idx : Graph.Index g₁) →
                       g₁ [ idx ] ≡ g₂ [ relax g₁⊆g₂ idx ]
@@ -145,84 +134,8 @@ 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₁) _ _)
 
--- 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.
-
-MonotonicGraphFunction : (Graph → Set) → Set
-MonotonicGraphFunction T = (g₁ : Graph) → Σ Graph (λ g₂ → T g₂ × g₁ ⊆ g₂)
-
--- Now, define some operations on monotonic functions; these are useful
--- to save the work of threading intermediate graphs in and out of operations.
-
-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 =
+pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index
+pushBasicBlock bss g =
     ( record
         { size = Graph.size g Nat.+ 1
         ; nodes = Graph.nodes g ++ (bss ∷ [])
@@ -239,8 +152,8 @@ module Construction where
       )
     )
 
-    addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g')
-    addEdges (MkGraph s ns es) es' =
+addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g')
+addEdges (MkGraph s ns es) es' =
     ( record
         { size = s
         ; nodes = ns
@@ -259,21 +172,21 @@ module Construction where
         }
     )
 
-    pushEmptyBlock : MonotonicGraphFunction Graph.Index
-    pushEmptyBlock = pushBasicBlock []
+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 : 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 (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 (while _ repeat s) =
     (buildCfg s ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock)
     update (λ { g ((idx₁ , idx₂) , idx , idx') →
               addEdges g ((idx , idx') ∷ (idx , idx₁) ∷ (idx₂ , idx) ∷ []) })

MonotonicState.agda

@@ -0,0 +1,116 @@
+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)