Compare commits
No commits in common. "b134c143ca3140af0f35e2a75f869fe54942a201" and "2f91ca113eb8082beaa00c2cde50b9932555567f" have entirely different histories.
b134c143ca
...
2f91ca113e
|
|
@ -3,7 +3,6 @@ module Language where
|
|||
open import Language.Base public
|
||||
open import Language.Semantics public
|
||||
open import Language.Graphs public
|
||||
open import Language.Properties public
|
||||
|
||||
open import Data.Fin using (Fin; suc; zero)
|
||||
open import Data.Fin.Properties as FinProp using (suc-injective)
|
||||
|
|
|
|||
|
|
@ -1,6 +1,7 @@
|
|||
module Language.Graphs where
|
||||
|
||||
open import Language.Base
|
||||
open import Language.Semantics
|
||||
|
||||
open import Data.Fin as Fin using (Fin; suc; zero; _↑ˡ_; _↑ʳ_)
|
||||
open import Data.Fin.Properties as FinProp using (suc-injective)
|
||||
|
|
@ -11,8 +12,8 @@ open import Data.Nat as Nat using (ℕ; suc)
|
|||
open import Data.Nat.Properties using (+-assoc; +-comm)
|
||||
open import Data.Product using (_×_; Σ; _,_)
|
||||
open import Data.Vec using (Vec; []; _∷_; lookup; cast; _++_)
|
||||
open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-sym; ++-identityʳ; lookup-++ʳ)
|
||||
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans)
|
||||
open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-sym; ++-identityʳ)
|
||||
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst)
|
||||
|
||||
open import Lattice
|
||||
open import Utils using (x∈xs⇒fx∈fxs; _⊗_; _,_)
|
||||
|
|
@ -56,39 +57,38 @@ record _⊆_ (g₁ g₂ : Graph) : Set where
|
|||
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₂)
|
||||
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
|
||||
↑ˡ-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
|
||||
↑ˡ-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
|
||||
↑ˡ-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
|
||||
↑ˡ-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
|
||||
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₃}
|
||||
|
|
@ -128,6 +128,12 @@ instance
|
|||
|
||||
open Relaxable {{...}}
|
||||
|
||||
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₁) _ _)
|
||||
|
||||
pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index
|
||||
pushBasicBlock bss g =
|
||||
( record
|
||||
|
|
@ -146,9 +152,6 @@ pushBasicBlock bss 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
|
||||
|
|
@ -169,6 +172,9 @@ addEdges (MkGraph s ns es) 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₂) =
|
||||
|
|
|
|||
|
|
@ -1,52 +0,0 @@
|
|||
module Language.Properties where
|
||||
|
||||
open import Language.Base
|
||||
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 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)
|
||||
|
||||
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₁) _ _)
|
||||
|
||||
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 {!!}
|
||||
|
|
@ -5,7 +5,7 @@ open import Language.Base
|
|||
open import Data.Integer using (ℤ; +_) renaming (_+_ to _+ᶻ_; _-_ to _-ᶻ_)
|
||||
open import Data.Product using (_×_; _,_)
|
||||
open import Data.String using (String)
|
||||
open import Data.List as List using (List)
|
||||
open import Data.List using (List; _∷_)
|
||||
open import Data.Nat using (ℕ)
|
||||
open import Relation.Nullary using (¬_)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_)
|
||||
|
|
@ -17,8 +17,8 @@ Env : Set
|
|||
Env = List (String × Value)
|
||||
|
||||
data _∈_ : (String × Value) → Env → Set where
|
||||
here : ∀ (s : String) (v : Value) (ρ : Env) → (s , v) ∈ ((s , v) List.∷ ρ)
|
||||
there : ∀ (s s' : String) (v v' : Value) (ρ : Env) → ¬ (s ≡ s') → (s , v) ∈ ρ → (s , v) ∈ ((s' , v') List.∷ ρ)
|
||||
here : ∀ (s : String) (v : Value) (ρ : Env) → (s , v) ∈ ((s , v) ∷ ρ)
|
||||
there : ∀ (s s' : String) (v v' : Value) (ρ : Env) → ¬ (s ≡ s') → (s , v) ∈ ρ → (s , v) ∈ ((s' , v') ∷ ρ)
|
||||
|
||||
data _,_⇒ᵉ_ : Env → Expr → Value → Set where
|
||||
⇒ᵉ-ℕ : ∀ (ρ : Env) (n : ℕ) → ρ , (# n) ⇒ᵉ (↑ᶻ (+ n))
|
||||
|
|
@ -33,12 +33,7 @@ data _,_⇒ᵉ_ : Env → Expr → Value → Set where
|
|||
data _,_⇒ᵇ_ : Env → BasicStmt → Env → Set where
|
||||
⇒ᵇ-noop : ∀ (ρ : Env) → ρ , noop ⇒ᵇ ρ
|
||||
⇒ᵇ-← : ∀ (ρ : Env) (x : String) (e : Expr) (v : Value) →
|
||||
ρ , e ⇒ᵉ v → ρ , (x ← e) ⇒ᵇ ((x , v) List.∷ ρ)
|
||||
|
||||
data _,_⇒ᵇˢ_ : Env → List BasicStmt → Env → Set where
|
||||
[] : ∀ {ρ : Env} → ρ , List.[] ⇒ᵇˢ ρ
|
||||
_∷_ : ∀ {ρ₁ ρ₂ ρ₃ : Env} {bs : BasicStmt} {bss : List BasicStmt} →
|
||||
ρ₁ , bs ⇒ᵇ ρ₂ → ρ₂ , bss ⇒ᵇˢ ρ₃ → ρ₁ , (bs List.∷ bss) ⇒ᵇˢ ρ₃
|
||||
ρ , e ⇒ᵉ v → ρ , (x ← e) ⇒ᵇ ((x , v) ∷ ρ)
|
||||
|
||||
data _,_⇒ˢ_ : Env → Stmt → Env → Set where
|
||||
⇒ˢ-⟨⟩ : ∀ (ρ₁ ρ₂ : Env) (bs : BasicStmt) →
|
||||
|
|
|
|||
|
|
@ -1,24 +0,0 @@
|
|||
module Language.Traces where
|
||||
|
||||
open import Language.Base public
|
||||
open import Language.Semantics public
|
||||
open import Language.Graphs public
|
||||
|
||||
open import Data.Product using (_,_)
|
||||
open import Data.List.Membership.Propositional as MemProp using ()
|
||||
|
||||
module _ {g : Graph} where
|
||||
open Graph g using (Index; edges)
|
||||
|
||||
data Trace : Index → Index → Env → Env → Set where
|
||||
Trace-single : ∀ {ρ₁ ρ₂ : Env} {idx : Index} →
|
||||
ρ₁ , (g [ idx ]) ⇒ᵇˢ ρ₂ → Trace idx idx ρ₁ ρ₂
|
||||
Trace-edge : ∀ {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : Index} →
|
||||
ρ₁ , (g [ idx₁ ]) ⇒ᵇˢ ρ₂ → (idx₁ , idx₂) MemProp.∈ edges →
|
||||
Trace idx₂ idx₃ ρ₂ ρ₃ → Trace idx₁ idx₃ ρ₁ ρ₃
|
||||
|
||||
_++⟨_⟩_ : ∀ {idx₁ idx₂ idx₃ idx₄ : Index} {ρ₁ ρ₂ ρ₃ : Env} →
|
||||
Trace idx₁ idx₂ ρ₁ ρ₂ → (idx₂ , idx₃) MemProp.∈ edges →
|
||||
Trace idx₃ idx₄ ρ₂ ρ₃ → Trace idx₁ idx₄ ρ₁ ρ₃
|
||||
_++⟨_⟩_ (Trace-single ρ₁⇒ρ₂) idx₂→idx₃ tr = Trace-edge ρ₁⇒ρ₂ idx₂→idx₃ tr
|
||||
_++⟨_⟩_ (Trace-edge ρ₁⇒ρ₂ idx₁→idx' tr') idx₂→idx₃ tr = Trace-edge ρ₁⇒ρ₂ idx₁→idx' (tr' ++⟨ idx₂→idx₃ ⟩ tr)
|
||||
|
|
@ -83,15 +83,9 @@ _map_ f fn s = let (s' , (t₁ , s≼s')) = f s in (s' , (fn s' t₁ , s≼s'))
|
|||
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
|
||||
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
|
||||
|
|
@ -103,82 +97,20 @@ record MonotonicPredicate {T : S → Set s} {{ r : Relaxable T }} (P : Dependent
|
|||
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
|
||||
always : ∀ {T : S → Set s} → DependentPredicate T → MonotonicState T → Set s
|
||||
always P m = ∀ s₁ → let (s₂ , t , _) = m s₁ in P s₂ t
|
||||
|
||||
infixr 4 _⟨⊗⟩-reason_
|
||||
_⟨⊗⟩-reason_ : ∀ {T₁ T₂ : S → Set s} {{ _ : Relaxable 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 = 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
|
||||
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)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user