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

Slightly simplify evaluation code

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-08 22:05:50 -07:00
parent 66d229c493
commit 7fe46b014c
1 changed files with 4 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
Analysis/Forward.agda
View File

@ -158,13 +158,12 @@ module WithProg (prog : Program) where
updateVariablesFromStmt-Monoʳ (k ← e) {vs₁} {vs₂} vs₁≼vs₂ = updateVariablesFromExpression-Mono k e {vs₁} {vs₂} vs₁≼vs₂ updateVariablesFromStmt-Monoʳ (k ← e) {vs₁} {vs₂} vs₁≼vs₂ = updateVariablesFromExpression-Mono k e {vs₁} {vs₂} vs₁≼vs₂
updateVariablesFromStmt-Monoʳ noop vs₁≼vs₂ = vs₁≼vs₂ updateVariablesFromStmt-Monoʳ noop vs₁≼vs₂ = vs₁≼vs₂
variablesAt : State → StateVariables → VariableValues
variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
updateVariablesForState : State → StateVariables → VariableValues updateVariablesForState : State → StateVariables → VariableValues
updateVariablesForState s sv = updateVariablesForState s sv =
let foldl (flip updateVariablesFromStmt) (variablesAt s sv) (code s)
bss = code s
(vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv)
in
foldl (flip updateVariablesFromStmt) vs bss
updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s) updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ = updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ =