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

Remove unused 'singleton' calls for if/else CFGs

Browse Source
This commit is contained in:
Danila Fedorin 2024-11-16 14:42:16 -08:00
parent 828b652d3b
commit 4fba1fe79a
2 changed files with 3 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Language/Graphs.agda
View File

@ -122,7 +122,7 @@ wrap g = singleton [] ↦ g ↦ singleton []
buildCfg : Stmt → Graph
buildCfg ⟨ bs₁ ⟩ = singleton (bs₁ ∷ [])
buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
buildCfg (if _ then s₁ else s₂) = singleton [] ↦ (buildCfg s₁ ∙ buildCfg s₂) ↦ singleton []
buildCfg (if _ then s₁ else s₂) = buildCfg s₁ ∙ buildCfg s₂
buildCfg (while _ repeat s) = loop (buildCfg s)
private

8
Language/Properties.agda
View File

@ -285,13 +285,9 @@ buildCfg-sufficient (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ₂) =
buildCfg-sufficient (⇒ˢ-then ρ₁ ρ₂ ρ₃ s₁ s₂ ρ₁,s₁⇒ρ₂ ρ₂,s₂⇒ρ₃) =
buildCfg-sufficient ρ₁,s₁⇒ρ₂ ++ buildCfg-sufficient ρ₂,s₂⇒ρ₃
buildCfg-sufficient (⇒ˢ-if-true ρ₁ ρ₂ _ _ s₁ s₂ _ _ ρ₁,s₁⇒ρ₂) =
EndToEndTrace-singleton[] ρ₁ ++
(EndToEndTrace-∙ˡ (buildCfg-sufficient ρ₁,s₁⇒ρ₂)) ++
EndToEndTrace-singleton[] ρ₂
EndToEndTrace-∙ˡ (buildCfg-sufficient ρ₁,s₁⇒ρ₂)
buildCfg-sufficient (⇒ˢ-if-false ρ₁ ρ₂ _ s₁ s₂ _ ρ₁,s₂⇒ρ₂) =
EndToEndTrace-singleton[] ρ₁ ++
(EndToEndTrace-∙ʳ {buildCfg s₁} (buildCfg-sufficient ρ₁,s₂⇒ρ₂)) ++
EndToEndTrace-singleton[] ρ₂
EndToEndTrace-∙ʳ {buildCfg s₁} (buildCfg-sufficient ρ₁,s₂⇒ρ₂)
buildCfg-sufficient (⇒ˢ-while-true ρ₁ ρ₂ ρ₃ _ _ s _ _ ρ₁,s⇒ρ₂ ρ₂,ws⇒ρ₃) =
EndToEndTrace-loop² {buildCfg s}
(EndToEndTrace-loop {buildCfg s} (buildCfg-sufficient ρ₁,s⇒ρ₂))