Delete code that won't be used for this approach
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
c00c8e3e85
commit
f2b8084a9c
|
|
@ -105,144 +105,3 @@ buildCfg ⟨ bs₁ ⟩ = singleton (bs₁ ∷ [])
|
||||||
buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
|
buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
|
||||||
buildCfg (if _ then s₁ else s₂) = singleton [] ↦ (buildCfg s₁ ∙ buildCfg s₂) ↦ singleton []
|
buildCfg (if _ then s₁ else s₂) = singleton [] ↦ (buildCfg s₁ ∙ buildCfg s₂) ↦ singleton []
|
||||||
buildCfg (while _ repeat s) = loop (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') })
|
|
||||||
|
|
|
||||||
|
|
@ -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
|
|
||||||
Loading…
Reference in New Issue
Block a user