agda-spa/Language/Properties.agda

164 lines
9.3 KiB
Agda
Raw Normal View History

module Language.Properties where
open import Language.Base
open import Language.Semantics
open import Language.Graphs
open import Language.Traces
open import Data.Fin as Fin using (zero)
open import Data.List using (List; _∷_; [])
open import Data.List.Relation.Unary.Any using (here)
open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
open import Data.Product using (Σ; _,_; _×_)
open import Data.Vec.Properties using (lookup-++ˡ; ++-identityʳ; lookup-++ʳ)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym)
open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct)
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)
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)
Trace-∙ˡ : {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env}
Trace {g₁} idx₁ idx₂ ρ₁ ρ₂
Trace {g₁ g₂} (idx₁ Fin.↑ˡ Graph.size g₂) (idx₂ Fin.↑ˡ Graph.size g₂) ρ₁ ρ₂
Trace-∙ˡ {g₁} {g₂} {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂)
rewrite sym (lookup-++ˡ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
Trace-single ρ₁⇒ρ₂
Trace-∙ˡ {g₁} {g₂} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr')
rewrite sym (lookup-++ˡ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (_↑ˡ Graph.size g₂) idx₁→idx))
(Trace-∙ˡ tr')
Trace-∙ʳ : {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₂} {ρ₁ ρ₂ : Env}
Trace {g₂} idx₁ idx₂ ρ₁ ρ₂
Trace {g₁ g₂} (Graph.size g₁ Fin.↑ʳ idx₁) (Graph.size g₁ Fin.↑ʳ idx₂) ρ₁ ρ₂
Trace-∙ʳ {g₁} {g₂} {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂)
rewrite sym (lookup-++ʳ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
Trace-single ρ₁⇒ρ₂
Trace-∙ʳ {g₁} {g₂} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr')
rewrite sym (lookup-++ʳ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ʳ _ (x∈xs⇒fx∈fxs (Graph.size g₁ ↑ʳ_) idx₁→idx))
(Trace-∙ʳ tr')
2024-04-28 12:00:06 -07:00
EndToEndTrace-∙ˡ : {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env}
EndToEndTrace {g₁} ρ₁ ρ₂
EndToEndTrace {g₁ g₂} ρ₁ ρ₂
EndToEndTrace-∙ˡ {g₁} {g₂} etr = record
{ idx₁ = EndToEndTrace.idx₁ etr Fin.↑ˡ Graph.size g₂
; idx₁∈inputs = ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (Fin._↑ˡ Graph.size g₂)
(EndToEndTrace.idx₁∈inputs etr))
; idx₂ = EndToEndTrace.idx₂ etr Fin.↑ˡ Graph.size g₂
; idx₂∈outputs = ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (Fin._↑ˡ Graph.size g₂)
(EndToEndTrace.idx₂∈outputs etr))
; trace = Trace-∙ˡ (EndToEndTrace.trace etr)
}
EndToEndTrace-∙ʳ : {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env}
EndToEndTrace {g₂} ρ₁ ρ₂
EndToEndTrace {g₁ g₂} ρ₁ ρ₂
EndToEndTrace-∙ʳ {g₁} {g₂} etr = record
{ idx₁ = Graph.size g₁ Fin.↑ʳ EndToEndTrace.idx₁ etr
; idx₁∈inputs = ListMemProp.∈-++⁺ʳ (Graph.inputs g₁ ↑ˡⁱ Graph.size g₂)
((x∈xs⇒fx∈fxs (Graph.size g₁ Fin.↑ʳ_)
(EndToEndTrace.idx₁∈inputs etr)))
; idx₂ = Graph.size g₁ Fin.↑ʳ EndToEndTrace.idx₂ etr
; idx₂∈outputs = ListMemProp.∈-++⁺ʳ (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂)
((x∈xs⇒fx∈fxs (Graph.size g₁ Fin.↑ʳ_)
(EndToEndTrace.idx₂∈outputs etr)))
; trace = Trace-∙ʳ (EndToEndTrace.trace etr)
}
Trace-↦ˡ : {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env}
Trace {g₁} idx₁ idx₂ ρ₁ ρ₂
Trace {g₁ g₂} (idx₁ Fin.↑ˡ Graph.size g₂) (idx₂ Fin.↑ˡ Graph.size g₂) ρ₁ ρ₂
Trace-↦ˡ {g₁} {g₂} {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂)
rewrite sym (lookup-++ˡ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
Trace-single ρ₁⇒ρ₂
Trace-↦ˡ {g₁} {g₂} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr')
rewrite sym (lookup-++ˡ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (_↑ˡ Graph.size g₂) idx₁→idx))
(Trace-↦ˡ tr')
Trace-↦ʳ : {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₂} {ρ₁ ρ₂ : Env}
Trace {g₂} idx₁ idx₂ ρ₁ ρ₂
Trace {g₁ g₂} (Graph.size g₁ Fin.↑ʳ idx₁) (Graph.size g₁ Fin.↑ʳ idx₂) ρ₁ ρ₂
Trace-↦ʳ {g₁} {g₂} {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂)
rewrite sym (lookup-++ʳ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
Trace-single ρ₁⇒ρ₂
Trace-↦ʳ {g₁} {g₂} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr')
rewrite sym (lookup-++ʳ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ʳ (Graph.edges g₁ ↑ˡᵉ Graph.size g₂)
(ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (Graph.size g₁ ↑ʳ_) idx₁→idx)))
(Trace-↦ʳ {g₁} {g₂} tr')
Trace-loop : {g₁ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env}
Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ Trace {loop g₁} idx₁ idx₂ ρ₁ ρ₂
Trace-loop {idx₁ = idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂) = Trace-single ρ₁⇒ρ₂
Trace-loop {g₁} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr') =
Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ˡ idx₁→idx) (Trace-loop tr')
infixr 5 _++_
_++_ : {g₁ g₂ : Graph} {ρ₁ ρ₂ ρ₃ : Env}
EndToEndTrace {g₁} ρ₁ ρ₂ EndToEndTrace {g₂} ρ₂ ρ₃
EndToEndTrace {g₁ g₂} ρ₁ ρ₃
_++_ {g₁} {g₂} etr₁ etr₂
= record
{ idx₁ = EndToEndTrace.idx₁ etr₁ Fin.↑ˡ Graph.size g₂
; idx₁∈inputs = x∈xs⇒fx∈fxs (Fin._↑ˡ Graph.size g₂) (EndToEndTrace.idx₁∈inputs etr₁)
; idx₂ = Graph.size g₁ Fin.↑ʳ EndToEndTrace.idx₂ etr₂
; idx₂∈outputs = x∈xs⇒fx∈fxs (Graph.size g₁ Fin.↑ʳ_) (EndToEndTrace.idx₂∈outputs etr₂)
; trace =
let
o∈tr₁ = x∈xs⇒fx∈fxs (Fin._↑ˡ Graph.size g₂) (EndToEndTrace.idx₂∈outputs etr₁)
i∈tr₂ = x∈xs⇒fx∈fxs (Graph.size g₁ Fin.↑ʳ_) (EndToEndTrace.idx₁∈inputs etr₂)
oi∈es = ListMemProp.∈-++⁺ʳ (Graph.edges g₁ ↑ˡᵉ Graph.size g₂)
(ListMemProp.∈-++⁺ʳ (Graph.size g₁ ↑ʳᵉ Graph.edges g₂)
(∈-cartesianProduct o∈tr₁ i∈tr₂))
in
(Trace-↦ˡ {g₁} {g₂} (EndToEndTrace.trace etr₁)) ++⟨ oi∈es
(Trace-↦ʳ {g₁} {g₂} (EndToEndTrace.trace etr₂))
}
Trace-singleton : {bss : List BasicStmt} {ρ₁ ρ₂ : Env}
ρ₁ , bss ⇒ᵇˢ ρ₂ EndToEndTrace {singleton bss} ρ₁ ρ₂
Trace-singleton ρ₁⇒ρ₂ = record
{ idx₁ = zero
; idx₁∈inputs = here refl
; idx₂ = zero
; idx₂∈outputs = here refl
; trace = Trace-single ρ₁⇒ρ₂
}
Trace-singleton[] : (ρ : Env) EndToEndTrace {singleton []} ρ ρ
Trace-singleton[] env = Trace-singleton []
buildCfg-sufficient : {s : Stmt} {ρ₁ ρ₂ : Env} ρ₁ , s ⇒ˢ ρ₂
EndToEndTrace {buildCfg s} ρ₁ ρ₂
buildCfg-sufficient (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ) =
Trace-singleton (ρ₁,bs⇒ρ [])
buildCfg-sufficient (⇒ˢ-then ρ₁ ρ₂ ρ₃ s₁ s₂ ρ₁,s₁⇒ρ ρ₂,s₂⇒ρ) =
buildCfg-sufficient ρ₁,s₁⇒ρ ++ buildCfg-sufficient ρ₂,s₂⇒ρ
buildCfg-sufficient (⇒ˢ-if-true ρ₁ ρ₂ _ _ s₁ s₂ _ _ ρ₁,s₁⇒ρ) =
Trace-singleton[] ρ₁ ++
(EndToEndTrace-∙ˡ (buildCfg-sufficient ρ₁,s₁⇒ρ)) ++
Trace-singleton[] ρ₂
buildCfg-sufficient (⇒ˢ-if-false ρ₁ ρ₂ _ s₁ s₂ _ ρ₁,s₂⇒ρ) =
Trace-singleton[] ρ₁ ++
(EndToEndTrace-∙ʳ {buildCfg s₁} (buildCfg-sufficient ρ₁,s₂⇒ρ)) ++
Trace-singleton[] ρ₂