From fdc40632bf92a71583190f92aa97e950c9a5216e Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 9 Mar 2024 23:09:50 -0800 Subject: [PATCH] Add a way to retrieve the code for a particular state Signed-off-by: Danila Fedorin --- Language.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Language.agda b/Language.agda index d9d25e2..4b37771 100644 --- a/Language.agda +++ b/Language.agda @@ -3,7 +3,7 @@ module Language where open import Data.Nat using (ℕ; suc; pred) open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.Product using (Σ; _,_; proj₁; proj₂) -open import Data.Vec using (Vec; foldr) +open import Data.Vec using (Vec; foldr; lookup) open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ) open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁) renaming (_≟_ to _≟ᶠ_) @@ -83,6 +83,9 @@ record Program : Set where State : Set State = Fin length + code : State → Stmt + code = lookup stmts + states : List State states = proj₁ (indices length)