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

Compare commits

base: DanilaFe:8dc5c40eae16befc3c9fd6af2ea752ff3415dfdb
Branches Tags
DanilaFe:main
..
compare: DanilaFe:7ed7f2022792a82969a5d5596951b85df9be1861
Branches Tags
DanilaFe:main

2 Commits
8dc5c40eae ... 7ed7f20227

Author SHA1 Message Date
Danila Fedorin
7ed7f20227 Add missing edge 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-13 15:30:07 -07:00
Danila Fedorin
163108b9b3 Add precedence to some language constructs 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-13 15:29:50 -07:00
1 changed files with 3 additions and 1 deletions
Show Stats Expand all files Collapse all files

4
Language.agda
View File

@ -38,6 +38,8 @@ data BasicStmt : Set where
noop : BasicStmt noop : BasicStmt
infixr 2 _then_ infixr 2 _then_
infix 3 while_repeat_
infix 3 if_then_else_
data Stmt : Set where data Stmt : Set where
⟨_⟩ : BasicStmt → Stmt ⟨_⟩ : BasicStmt → Stmt
_then_ : Stmt → Stmt → Stmt _then_ : Stmt → Stmt → Stmt
@ -350,7 +352,7 @@ module Graphs where
buildCfg (while _ repeat s) = buildCfg (while _ repeat s) =
(buildCfg s ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock) (buildCfg s ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock)
update (λ { g ((idx₁ , idx₂) , idx , idx') → update (λ { g ((idx₁ , idx₂) , idx , idx') →
addEdges g ((idx , idx') ∷ (idx₂ , idx) ∷ []) }) addEdges g ((idx , idx') ∷ (idx , idx₁) ∷ (idx₂ , idx) ∷ []) })
map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') }) map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') })
open import Lattice.MapSet _≟ˢ_ open import Lattice.MapSet _≟ˢ_