From f2b8084a9cddba4f49f9a7719e19c721a0c35cd2 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 25 Apr 2024 23:13:15 -0700 Subject: [PATCH] Delete code that won't be used for this approach Signed-off-by: Danila Fedorin --- Language/Graphs.agda | 141 --------------------------------- MonotonicState.agda | 184 ------------------------------------------- 2 files changed, 325 deletions(-) delete mode 100644 MonotonicState.agda diff --git a/Language/Graphs.agda b/Language/Graphs.agda index dfd1580..338f739 100644 --- a/Language/Graphs.agda +++ b/Language/Graphs.agda @@ -105,144 +105,3 @@ 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 []) - --- 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₂)) --- --- 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') }) diff --git a/MonotonicState.agda b/MonotonicState.agda deleted file mode 100644 index 4830b3a..0000000 --- a/MonotonicState.agda +++ /dev/null @@ -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