Compare commits
2 Commits
8dc5c40eae
...
7ed7f20227
Author | SHA1 | Date | |
---|---|---|---|
7ed7f20227 | |||
163108b9b3 |
|
@ -38,6 +38,8 @@ data BasicStmt : Set where
|
|||
noop : BasicStmt
|
||||
|
||||
infixr 2 _then_
|
||||
infix 3 while_repeat_
|
||||
infix 3 if_then_else_
|
||||
data Stmt : Set where
|
||||
⟨_⟩ : BasicStmt → Stmt
|
||||
_then_ : Stmt → Stmt → Stmt
|
||||
|
@ -350,7 +352,7 @@ module Graphs where
|
|||
buildCfg (while _ repeat s) =
|
||||
(buildCfg s ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock)
|
||||
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') })
|
||||
|
||||
open import Lattice.MapSet _≟ˢ_
|
||||
|
|
Loading…
Reference in New Issue
Block a user