From 9366ec4a978afab2512c0b1d3b9695f76a61d6e3 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 28 Apr 2024 12:00:06 -0700 Subject: [PATCH] Allow promoting end-to-end traces too --- Language/Properties.agda | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/Language/Properties.agda b/Language/Properties.agda index 2fb870e..42fe80e 100644 --- a/Language/Properties.agda +++ b/Language/Properties.agda @@ -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-∙ʳ 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₁} idx₁ idx₂ ρ₁ ρ₂ → Trace {g₁ ↦ g₂} (idx₁ Fin.↑ˡ Graph.size g₂) (idx₂ Fin.↑ˡ Graph.size g₂) ρ₁ ρ₂