From 7fe46b014c614839b6bf55be1c9965443b97a4aa Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 8 May 2024 22:05:50 -0700 Subject: [PATCH] Slightly simplify evaluation code Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index 784fc99..c2f4d2d 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -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ʳ 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 s sv = - let - bss = code s - (vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv) - in - foldl (flip updateVariablesFromStmt) vs bss + foldl (flip updateVariablesFromStmt) (variablesAt s sv) (code s) updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s) updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ =