Delete code that won't be used for this approach

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

Language.agda

@@ -52,20 +52,17 @@ record Program : Set where
     field
         rootStmt : Stmt
 
-    private
-        buildResult = buildCfg rootStmt empty
-
     graph : Graph
-    graph = proj₁ buildResult
+    graph = buildCfg rootStmt
 
     State : Set
     State = Graph.Index graph
 
     initialState : State
-    initialState = Utils.proj₁ (proj₁ (proj₂ buildResult))
+    initialState = proj₁ (buildCfg-input rootStmt)
 
     finalState : State
-    finalState = Utils.proj₂ (proj₁ (proj₂ buildResult))
+    finalState = proj₁ (buildCfg-output rootStmt)
 
     private
         vars-Set : StringSet

Language/Graphs.agda

@@ -1,8 +1,8 @@
 module Language.Graphs where
 
-open import Language.Base
+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 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 ()
@@ -15,7 +15,7 @@ open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-s
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans)
 
 open import Lattice
-open import Utils using (x∈xs⇒fx∈fxs; _⊗_; _,_)
+open import Utils using (x∈xs⇒fx∈fxs; _⊗_; _,_; ∈-cartesianProduct)
 
 record Graph : Set where
     constructor MkGraph
@@ -31,157 +31,77 @@ record Graph : Set where
     field
         nodes : Vec (List BasicStmt) size
         edges : List Edge
+        inputs : List Index
+        outputs : List Index
 
-empty : Graph
-empty = record
-    { size = 0
-    ; nodes = []
-    ; edges = []
+_↑ˡ_ : ∀ {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
+
+infixl 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₂)
     }
 
-↑ˡ-Edge : ∀ {n} → (Fin n × Fin n) → ∀ m → (Fin (n Nat.+ m) × Fin (n Nat.+ m))
-↑ˡ-Edge (idx₁ , idx₂) m = (idx₁ ↑ˡ m , idx₂ ↑ˡ m)
+infixl 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 = Graph.size g
+    ; nodes = Graph.nodes g
+    ; edges = Graph.edges g List.++
+              List.cartesianProduct (Graph.outputs g) (Graph.inputs g)
+    ; inputs = Graph.inputs g
+    ; outputs = Graph.outputs g
+    }
 
 _[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt
 _[_] g idx = lookup (Graph.nodes g) idx
 
-record _⊆_ (g₁ g₂ : Graph) : Set where
-    constructor Mk-⊆
-    field
-        n : ℕ
-        sg₂≡sg₁+n : Graph.size g₂ ≡ Graph.size g₁ Nat.+ n
-        newNodes : Vec (List BasicStmt) n
-        nsg₂≡nsg₁++newNodes : cast sg₂≡sg₁+n (Graph.nodes g₂) ≡ Graph.nodes g₁ ++ newNodes
-        e∈g₁⇒e∈g₂ : ∀ {e : Graph.Edge g₁} →
-                    e ListMem.∈ (Graph.edges g₁) →
-                    (↑ˡ-Edge e n) ListMem.∈ (subst (λ m → List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂))
+singleton : List BasicStmt → Graph
+singleton bss = record
+    { size = 1
+    ; nodes = bss ∷ []
+    ; edges = []
+    ; inputs = zero ∷ []
+    ; outputs = zero ∷ []
+    }
 
-private
-    castᵉ : ∀ {n m : ℕ} .(p : n ≡ m) → (Fin n × Fin n) → (Fin m × Fin m)
-    castᵉ p (idx₁ , idx₂) = (Fin.cast p idx₁ , Fin.cast p idx₂)
-
-    ↑ˡ-assoc : ∀ {s n₁ n₂} (f : Fin s) (p : s Nat.+ (n₁ Nat.+ n₂) ≡ s Nat.+ n₁ Nat.+ n₂) →
-               f ↑ˡ n₁ ↑ˡ n₂ ≡ Fin.cast p (f ↑ˡ (n₁ Nat.+ n₂))
-    ↑ˡ-assoc zero p = refl
-    ↑ˡ-assoc {suc s'} {n₁} {n₂} (suc f') p rewrite ↑ˡ-assoc f' (sym (+-assoc s' n₁ n₂)) = refl
-
-    ↑ˡ-Edge-assoc : ∀ {s n₁ n₂} (e : Fin s × Fin s) (p : s Nat.+ (n₁ Nat.+ n₂) ≡ s Nat.+ n₁ Nat.+ n₂) →
-                    ↑ˡ-Edge (↑ˡ-Edge e n₁) n₂ ≡ castᵉ p (↑ˡ-Edge e (n₁ Nat.+ n₂))
-    ↑ˡ-Edge-assoc (idx₁ , idx₂) p
-        rewrite ↑ˡ-assoc idx₁ p
-        rewrite ↑ˡ-assoc idx₂ p = refl
-
-    ↑ˡ-identityʳ : ∀ {s} (f : Fin s) (p : s Nat.+ 0 ≡ s) →
-               f ≡ Fin.cast p (f ↑ˡ 0)
-    ↑ˡ-identityʳ zero p = refl
-    ↑ˡ-identityʳ {suc s'} (suc f') p rewrite sym (↑ˡ-identityʳ f' (+-comm s' 0)) = refl
-
-    ↑ˡ-Edge-identityʳ : ∀ {s} (e : Fin s × Fin s) (p : s Nat.+ 0 ≡ s) →
-                        e ≡ castᵉ p (↑ˡ-Edge e 0)
-    ↑ˡ-Edge-identityʳ (idx₁ , idx₂) p
-        rewrite sym (↑ˡ-identityʳ idx₁ p)
-        rewrite sym (↑ˡ-identityʳ idx₂ p) = refl
-
-    cast∈⇒∈subst : ∀ {n m : ℕ} (p : n ≡ m) (q : m ≡ n)
-                   (e : Fin n × Fin n) (es : List (Fin m × Fin m)) →
-                   castᵉ p e ListMem.∈ es →
-                   e ListMem.∈ subst (λ m → List (Fin m × Fin m)) q es
-    cast∈⇒∈subst refl refl (idx₁ , idx₂) es e∈es
-        rewrite FinProp.cast-is-id refl idx₁
-        rewrite FinProp.cast-is-id refl idx₂ = e∈es
-
-⊆-trans : ∀ {g₁ g₂ g₃ : Graph} → g₁ ⊆ g₂ → g₂ ⊆ g₃ → g₁ ⊆ g₃
-⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃}
-        (Mk-⊆ n₁ p₁@refl newNodes₁ nsg₂≡nsg₁++newNodes₁ e∈g₁⇒e∈g₂)
-        (Mk-⊆ n₂ p₂@refl newNodes₂ nsg₃≡nsg₂++newNodes₂ e∈g₂⇒e∈g₃)
-    rewrite cast-is-id refl ns₂
-    rewrite cast-is-id refl ns₃
-    with refl ← nsg₂≡nsg₁++newNodes₁
-    with refl ← nsg₃≡nsg₂++newNodes₂ =
-    record
-        { n = n₁ Nat.+ n₂
-        ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂
-        ; newNodes = newNodes₁ ++ newNodes₂
-        ; nsg₂≡nsg₁++newNodes = ++-assoc (+-assoc s₁ n₁ n₂) ns₁ newNodes₁ newNodes₂
-        ; e∈g₁⇒e∈g₂ = λ {e} e∈g₁ →
-            cast∈⇒∈subst (sym (+-assoc s₁ n₁ n₂)) (+-assoc s₁ n₁ n₂) _ _
-                         (subst (λ e' → e' ListMem.∈ es₃)
-                                (↑ˡ-Edge-assoc e (sym (+-assoc s₁ n₁ n₂)))
-                                (e∈g₂⇒e∈g₃ (e∈g₁⇒e∈g₂ e∈g₁)))
-        }
-
-open import MonotonicState _⊆_ ⊆-trans renaming (MonotonicState to MonotonicGraphFunction)
-
-instance
-    IndexRelaxable : Relaxable Graph.Index
-    IndexRelaxable = record
-        { relax = λ { (Mk-⊆ n refl _ _ _) idx → idx ↑ˡ n }
-        }
-
-    EdgeRelaxable : Relaxable Graph.Edge
-    EdgeRelaxable = record
-        { relax = λ g₁⊆g₂ (idx₁ , idx₂) →
-            ( Relaxable.relax IndexRelaxable g₁⊆g₂ idx₁
-            , Relaxable.relax IndexRelaxable g₁⊆g₂ idx₂
-            )
-        }
-
-open Relaxable {{...}}
-
-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₁
-          }
-      )
-    )
-
-pushEmptyBlock : MonotonicGraphFunction Graph.Index
-pushEmptyBlock = pushBasicBlock []
-
-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))
-        }
-    )
-
-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') })
+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 ↦ singleton [])

Language/Properties.agda

@@ -5,48 +5,24 @@ open import Language.Semantics
 open import Language.Graphs
 open import Language.Traces
 
-open import MonotonicState _⊆_ ⊆-trans renaming (MonotonicState to MonotonicGraphFunction)
-open import Utils using (_⊗_; _,_)
-open Relaxable {{...}}
+open import Data.Fin as Fin using (zero)
+open import Data.List using (_∷_; [])
+open import Data.Product using (Σ; _,_)
 
-open import Data.Fin using (zero)
-open import Data.List using (List; _∷_; [])
-open import Data.Vec using (_∷_; [])
-open import Data.Vec.Properties using (cast-is-id; lookup-++ˡ; lookup-++ʳ)
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; subst)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 
-relax-preserves-[]≡ : ∀ (g₁ g₂ : Graph) (g₁⊆g₂ : g₁ ⊆ g₂) (idx : Graph.Index g₁) →
-                      g₁ [ idx ] ≡ g₂ [ relax g₁⊆g₂ idx ]
-relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl newNodes nsg₂≡nsg₁++newNodes _) idx
-    rewrite cast-is-id refl (Graph.nodes g₂)
-    with refl ← nsg₂≡nsg₁++newNodes = sym (lookup-++ˡ (Graph.nodes g₁) _ _)
+buildCfg-input : ∀ (s : Stmt) → let g = buildCfg s in Σ (Graph.Index g) (λ idx → Graph.inputs g ≡ idx ∷ [])
+buildCfg-input ⟨ bs₁ ⟩ = (zero , refl)
+buildCfg-input (s₁ then s₂)
+    with (idx , p) ← buildCfg-input s₁ rewrite p = (_ , refl)
+buildCfg-input (if _ then s₁ else s₂) = (zero , refl)
+buildCfg-input (while _ repeat s)
+    with (idx , p) ← buildCfg-input s rewrite p = (_ , refl)
 
-instance
-    NodeEqualsMonotonic : ∀ {bss : List BasicStmt} →
-                          MonotonicPredicate (λ g n → g [ n ] ≡ bss)
-    NodeEqualsMonotonic = record
-        { relaxPredicate = λ g₁ g₂ idx g₁⊆g₂ g₁[idx]≡bss →
-            trans (sym (relax-preserves-[]≡ g₁ g₂ g₁⊆g₂ idx)) g₁[idx]≡bss
-        }
-
-pushBasicBlock-works : ∀ (bss : List BasicStmt) → Always (λ g idx → g [ idx ] ≡ bss) (pushBasicBlock bss)
-pushBasicBlock-works bss = MkAlways (λ g → lookup-++ʳ (Graph.nodes g) (bss ∷ []) zero)
-
-TransformsEnv : ∀ (ρ₁ ρ₂ : Env) → DependentPredicate (Graph.Index ⊗ Graph.Index)
-TransformsEnv ρ₁ ρ₂ g (idx₁ , idx₂) = Trace {g} idx₁ idx₂ ρ₁ ρ₂
-
-instance
-    TransformsEnvMonotonic : ∀ {ρ₁ ρ₂ : Env} → MonotonicPredicate (TransformsEnv ρ₁ ρ₂)
-    TransformsEnvMonotonic = {!!}
-
-buildCfg-sufficient : ∀ {ρ₁ ρ₂ : Env} {s : Stmt} → ρ₁ , s ⇒ˢ ρ₂ → Always (TransformsEnv ρ₁ ρ₂) (buildCfg s)
-buildCfg-sufficient {ρ₁} {ρ₂} {⟨ bs ⟩} (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ₂) =
-    pushBasicBlock-works (bs ∷ [])
-    map-reason
-        (λ g idx g[idx]≡[bs] → Trace-single (subst (ρ₁ ,_⇒ᵇˢ ρ₂)
-                                                   (sym g[idx]≡[bs])
-                                                   (ρ₁,bs⇒ρ₂ ∷ [])))
-buildCfg-sufficient {ρ₁} {ρ₂} {s₁ then s₂} (⇒ˢ-then ρ₁ ρ ρ₂ s₁ s₂ ρ₁,s₁⇒ρ₂ ρ₂,s₂⇒ρ₃) =
-    (buildCfg-sufficient ρ₁,s₁⇒ρ₂ ⟨⊗⟩-reason buildCfg-sufficient ρ₂,s₂⇒ρ₃)
-    update-reason {!!}
-    map-reason {!!}
+buildCfg-output : ∀ (s : Stmt) → let g = buildCfg s in Σ (Graph.Index g) (λ idx → Graph.outputs g ≡ idx ∷ [])
+buildCfg-output ⟨ bs₁ ⟩ = (zero , refl)
+buildCfg-output (s₁ then s₂)
+    with (idx , p) ← buildCfg-output s₂ rewrite p = (_ , refl)
+buildCfg-output (if _ then s₁ else s₂) = (_ , refl)
+buildCfg-output (while _ repeat s)
+    with (idx , p) ← buildCfg-output s rewrite p = (_ , refl)

MonotonicState.agda

@@ -1,184 +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
-
-data Both {T₁ T₂ : S → Set s}
-          (P : DependentPredicate T₁)
-          (Q : DependentPredicate T₂) : DependentPredicate (T₁ ⊗ T₂) where
-    MkBoth : ∀ {s : S} {t₁ : T₁ s} {t₂ : T₂ s} → P s t₁ → Q s t₂ → Both P Q s (t₁ , t₂)
-
-data And {T : S → Set s}
-         (P : DependentPredicate T)
-         (Q : DependentPredicate T) : DependentPredicate T where
-    MkAnd : ∀ {s : S} {t : T s} → P s t → Q s t → And P 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₁)
-
-instance
-    BothMonotonic : ∀ {T₁ : S → Set s} {T₂ : S → Set s}
-                    {{ _ : Relaxable T₁ }} {{ _ : Relaxable T₂ }}
-                    {P : DependentPredicate T₁} {Q : DependentPredicate T₂}
-                    {{_ : MonotonicPredicate P}} {{_ : MonotonicPredicate Q}} →
-                    MonotonicPredicate (Both P Q)
-    BothMonotonic {{_}} {{_}} {{P-Mono}} {{Q-Mono}} = record
-        { relaxPredicate = (λ { s₁ s₂ (t₁ , t₂) s₁≼s₂ (MkBoth p q) →
-            MkBoth (MonotonicPredicate.relaxPredicate P-Mono s₁ s₂ t₁ s₁≼s₂ p)
-                   (MonotonicPredicate.relaxPredicate Q-Mono s₁ s₂ t₂ s₁≼s₂ q)})
-        }
-
-    AndMonotonic : ∀ {T : S → Set s} {{ _ : Relaxable T }}
-                   {P : DependentPredicate T} {Q : DependentPredicate T}
-                   {{_ : MonotonicPredicate P}} {{_ : MonotonicPredicate Q}} →
-                   MonotonicPredicate (And P Q)
-    AndMonotonic {{_}} {{P-Mono}} {{Q-Mono}} = record
-        { relaxPredicate = (λ { s₁ s₂ t s₁≼s₂ (MkAnd p q) →
-            MkAnd (MonotonicPredicate.relaxPredicate P-Mono s₁ s₂ t s₁≼s₂ p)
-                   (MonotonicPredicate.relaxPredicate Q-Mono s₁ s₂ t s₁≼s₂ q)})
-        }
-
--- A MonotonicState "monad" m has a certain property if its ouputs satisfy that
--- property for all inputs.
-
-data Always {T : S → Set s} (P : DependentPredicate T) (m : MonotonicState T) : Set s where
-    MkAlways : (∀ s₁ → let (s₂ , t , _) = m s₁ in P s₂ t) → Always P m
-
-infixr 4 _⟨⊗⟩-reason_
-_⟨⊗⟩-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 = P} {Q = Q} {{P-Mono = P-Mono}} {m₁ = m₁} {m₂ = m₂} (MkAlways aP) (MkAlways aQ) =
-    MkAlways impl
-    where
-        impl : ∀ s₁ → let (s₂ , t , _) = (m₁ ⟨⊗⟩ m₂) s₁ in (Both P Q) s₂ t
-        impl s
-            with p ← aP s
-            with (s' , (t₁ , s≼s')) ← m₁ s
-            with q ← aQ s'
-            with (s'' , (t₂ , s'≼s'')) ← m₂ s' =
-            MkBoth (MonotonicPredicate.relaxPredicate P-Mono _ _ _ s'≼s'' p) q
-
-infixl 4 _update-reason_
-_update-reason_ : ∀ {T : S → Set s} {{ r : Relaxable T }} →
-                  {P : DependentPredicate T} {Q : DependentPredicate T}
-                  {{P-Mono : MonotonicPredicate P}}
-                  {m : MonotonicState T} {mod : ∀ (s : S) → T s → Σ S (λ s' → s ≼ s')} →
-                  Always P m → (∀ (s : S) (t : T s) →
-                                let (s' , s≼s') = mod s t
-                                in P s t → Q s' (Relaxable.relax r s≼s' t)) →
-                  Always (And P Q) (m update mod)
-_update-reason_ {{r = r}} {P = P} {Q = Q} {{P-Mono = P-Mono}} {m = m} {mod = mod} (MkAlways aP) modQ =
-    MkAlways impl
-    where
-        impl : ∀ s₁ → let (s₂ , t , _) = (m update mod) s₁ in (And P Q) s₂ t
-        impl s
-            with p ← aP s
-            with (s' , (t , s≼s')) ← m s
-            with q ← modQ s' t p
-            with (s'' , s'≼s'') ← mod s' t =
-            MkAnd (MonotonicPredicate.relaxPredicate P-Mono _ _ _ s'≼s'' p) q
-
-infixl 4 _map-reason_
-_map-reason_ : ∀ {T₁ T₂ : S → Set s}
-               {P : DependentPredicate T₁} {Q : DependentPredicate T₂}
-               {m : MonotonicState T₁}
-               {f : ∀ (s : S) → T₁ s → T₂ s} →
-               Always P m → (∀ (s : S) (t₁ : T₁ s) → P s t₁ → Q s (f s t₁)) →
-               Always Q (m map f)
-_map-reason_ {P = P} {Q = Q} {m = m} {f = f} (MkAlways aP) P⇒Q =
-    MkAlways impl
-    where
-        impl : ∀ s₁ → let (s₂ , t , _) = (m map f) s₁ in Q s₂ t
-        impl s
-            with p ← aP s
-            with (s' , (t₁ , s≼s')) ← m s = P⇒Q s' t₁ p

Utils.agda

@@ -1,9 +1,11 @@
 module Utils where
 
 open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
+open import Data.Product as Prod using ()
 open import Data.Nat using (ℕ; suc)
-open import Data.List using (List; []; _∷_; _++_) renaming (map to mapˡ)
+open import Data.List using (List; cartesianProduct; []; _∷_; _++_) renaming (map to mapˡ)
 open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
 open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
 open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
 open import Function.Definitions using (Injective)
@@ -78,3 +80,9 @@ proj₁ (v , _) = v
 
 proj₂ : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {a : A} → (P ⊗ Q) a → Q a
 proj₂ (_ , v) = v
+
+∈-cartesianProduct : ∀ {a b} {A : Set a} {B : Set b}
+                     {x : A} {xs : List A} {y : B} {ys : List B} →
+                     x ∈ xs → y ∈ ys → (x Prod., y) ∈ cartesianProduct xs ys
+∈-cartesianProduct {x = x} (here refl) y∈ys = ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (x Prod.,_) y∈ys)
+∈-cartesianProduct {x = x} {xs = x' ∷ _} {ys = ys} (there x∈rest) y∈ys = ListMemProp.∈-++⁺ʳ (mapˡ (x' Prod.,_) ys) (∈-cartesianProduct x∈rest y∈ys)