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

Dip toes into creating end-to-end traces

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-04-27 15:27:46 -07:00
parent ab40a27e78
commit 316e56f2bc
1 changed files with 9 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
Language/Properties.agda
View File

@ -7,6 +7,7 @@ open import Language.Traces
open import Data.Fin as Fin using (zero) open import Data.Fin as Fin using (zero)
open import Data.List using (_∷_; []) 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.List.Membership.Propositional.Properties as ListMemProp using ()
open import Data.Product using (Σ; _,_; _×_) open import Data.Product using (Σ; _,_; _×_)
open import Data.Vec.Properties using (lookup-++ˡ; ++-identityʳ; lookup-++ʳ) 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 ⇒ˢ ρ₂ → buildCfg-sufficient : ∀ {s : Stmt} {ρ₁ ρ₂ : Env} → ρ₁ , s ⇒ˢ ρ₂ →
EndToEndTrace {buildCfg 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⇒ρ₂ ∷ [])
}