From 316e56f2bc2d144862f7eaf9f101b736199fc86a Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 27 Apr 2024 15:27:46 -0700 Subject: [PATCH] Dip toes into creating end-to-end traces Signed-off-by: Danila Fedorin --- Language/Properties.agda | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/Language/Properties.agda b/Language/Properties.agda index 6c0d268..04b20db 100644 --- a/Language/Properties.agda +++ b/Language/Properties.agda @@ -7,6 +7,7 @@ open import Language.Traces open import Data.Fin as Fin using (zero) open import Data.List using (_∷_; []) +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-++ʳ) @@ -84,4 +85,11 @@ Trace-loop g₁ {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr') = buildCfg-sufficient : ∀ {s : Stmt} {ρ₁ ρ₂ : Env} → ρ₁ , s ⇒ˢ ρ₂ → EndToEndTrace {buildCfg s} ρ₁ ρ₂ -buildCfg-sufficient = {!!} +buildCfg-sufficient (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ₂) = + record + { idx₁ = zero + ; idx₁∈inputs = here refl + ; idx₂ = zero + ; idx₂∈outputs = here refl + ; trace = Trace-single (ρ₁,bs⇒ρ₂ ∷ []) + }