DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Allow promoting end-to-end traces too

Browse Source
This commit is contained in:
Danila Fedorin 2024-04-28 12:00:06 -07:00
parent 0fb884eb07
commit 9366ec4a97
1 changed files with 29 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
Language/Properties.agda
View File

@ -54,6 +54,35 @@ Trace-∙ʳ {g₁} {g₂} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr')
Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ʳ _ (x∈xs⇒fx∈fxs (Graph.size g₁ ↑ʳ_) idx₁→idx)) Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ʳ _ (x∈xs⇒fx∈fxs (Graph.size g₁ ↑ʳ_) idx₁→idx))
(Trace-∙ʳ tr') (Trace-∙ʳ tr')
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₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env} →
Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ → Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ →
Trace {g₁ ↦ g₂} (idx₁ Fin.↑ˡ Graph.size g₂) (idx₂ Fin.↑ˡ Graph.size g₂) ρ₁ ρ₂ Trace {g₁ ↦ g₂} (idx₁ Fin.↑ˡ Graph.size g₂) (idx₂ Fin.↑ˡ Graph.size g₂) ρ₁ ρ₂