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

Add a way to retrieve the code for a particular state

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-09 23:09:50 -08:00
parent f84a1c923c
commit fdc40632bf
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Language.agda
View File

@ -3,7 +3,7 @@ module Language where
open import Data.Nat using (ℕ; suc; pred) open import Data.Nat using (ℕ; suc; pred)
open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
open import Data.Product using (Σ; _,_; proj₁; proj₂) 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 using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ)
open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁) renaming (_≟_ to _≟ᶠ_) open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁) renaming (_≟_ to _≟ᶠ_)
@ -83,6 +83,9 @@ record Program : Set where
State : Set State : Set
State = Fin length State = Fin length
code : State → Stmt
code = lookup stmts
states : List State states : List State
states = proj₁ (indices length) states = proj₁ (indices length)