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

Rename StateInterp to match the style of the rest of the codebase

Browse Source
This commit is contained in:
Danila Fedorin
2026-06-29 10:00:01 -05:00
parent 490c472d22
commit 59afbdaf71
3 changed files with 7 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
lean/Spa/Analysis/Forward.lean
View File

@@ -64,7 +64,7 @@ lemma joinForKey_initialState :
rfl rfl
class ValidStateEvaluator (L : Type) [FiniteHeightLattice L] (prog : Program) class ValidStateEvaluator (L : Type) [FiniteHeightLattice L] (prog : Program)
[E : StmtEvaluator L prog] [S : StateInterp L prog] where [E : StmtEvaluator L prog] [S : StateInterpretation L prog] where
step : (s : prog.State) → {ρ₁ ρ₂ : Env} → {bs : BasicStmt} → step : (s : prog.State) → {ρ₁ ρ₂ : Env} → {bs : BasicStmt} →
prog.code s = some bs → EvalBasicStmt ρ₁ bs ρ₂ → S.St ρ₁ → S.St ρ₂ prog.code s = some bs → EvalBasicStmt ρ₁ bs ρ₂ → S.St ρ₁ → S.St ρ₂
valid : ∀ (s : prog.State) {ρ₁ ρ₂ : Env} {bs : BasicStmt} valid : ∀ (s : prog.State) {ρ₁ ρ₂ : Env} {bs : BasicStmt}
@@ -80,7 +80,7 @@ instance [LatticeInterpretation L] [ValidStmtEvaluator L prog] :
botV_init := by intro k l _ v hmem; cases hmem botV_init := by intro k l _ v hmem; cases hmem
section section
variable [S : StateInterp L prog] [V : ValidStateEvaluator L prog] variable [S : StateInterpretation L prog] [V : ValidStateEvaluator L prog]
noncomputable def stepStmtOrNone (s : prog.State) {ρ₁ ρ₂ : Env} : noncomputable def stepStmtOrNone (s : prog.State) {ρ₁ ρ₂ : Env} :
(o : Option BasicStmt) → prog.code s = o → EvalBasicStmtOpt ρ₁ o ρ₂ → (o : Option BasicStmt) → prog.code s = o → EvalBasicStmtOpt ρ₁ o ρ₂ →

8
lean/Spa/Analysis/Forward/Lattices.lean
View File

@@ -64,7 +64,7 @@ lemma variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
variablesAt s (joinAll sv) = joinForKey s sv := variablesAt s (joinAll sv) = joinForKey s sv :=
joinAll_mem_eq (variablesAt_mem s (joinAll sv)) joinAll_mem_eq (variablesAt_mem s (joinAll sv))
class StateInterp (L : Type) [Lattice L] (prog : Program) where class StateInterpretation (L : Type) [Lattice L] (prog : Program) where
St : Env → Type St : Env → Type
init : St [] init : St []
interp : VariableValues L prog → (ρ : Env) → St ρ → Prop interp : VariableValues L prog → (ρ : Env) → St ρ → Prop
@@ -73,11 +73,11 @@ class StateInterp (L : Type) [Lattice L] (prog : Program) where
interp_inf : ∀ {vs₁ vs₂ : VariableValues L prog} {ρ : Env} {st : St ρ}, interp_inf : ∀ {vs₁ vs₂ : VariableValues L prog} {ρ : Env} {st : St ρ},
interp vs₁ ρ st ∧ interp vs₂ ρ st → interp (vs₁ ⊓ vs₂) ρ st interp vs₁ ρ st ∧ interp vs₂ ρ st → interp (vs₁ ⊓ vs₂) ρ st
instance [S : StateInterp L prog] : instance [S : StateInterpretation L prog] :
Interp (VariableValues L prog) ((ρ : Env) → S.St ρ → Prop) := Interp (VariableValues L prog) ((ρ : Env) → S.St ρ → Prop) :=
⟨S.interp⟩ ⟨S.interp⟩
lemma interp_foldr [S : StateInterp L prog] lemma interp_foldr [S : StateInterpretation L prog]
{vs : VariableValues L prog} {vss : List (VariableValues L prog)} {vs : VariableValues L prog} {vss : List (VariableValues L prog)}
{ρ : Env} {st : S.St ρ} (hvs : ⟦ vs ⟧ ρ st) (hmem : vs ∈ vss) : {ρ : Env} {st : S.St ρ} (hvs : ⟦ vs ⟧ ρ st) (hmem : vs ∈ vss) :
⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ st := by ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ st := by
@@ -90,7 +90,7 @@ lemma interp_foldr [S : StateInterp L prog]
variable [I : LatticeInterpretation L] variable [I : LatticeInterpretation L]
instance : StateInterp L prog where instance : StateInterpretation L prog where
St := fun _ => PUnit St := fun _ => PUnit
init := PUnit.unit init := PUnit.unit
interp vs ρ _ := ∀ (k : String) (l : L), (k, l) ∈ vs → interp vs ρ _ := ∀ (k : String) (l : L), (k, l) ∈ vs →

2
lean/Spa/Analysis/Reaching.lean
View File

@@ -58,7 +58,7 @@ inductive LastAssign (prog : Program) (x : String) : Run prog → prog.NodeId
(∀ e, bs ≠ .assign x e) → LastAssign prog x rest n → (∀ e, bs ≠ .assign x e) → LastAssign prog x rest n →
LastAssign prog x (Run.cons s bs hc rest) n LastAssign prog x (Run.cons s bs hc rest) n
instance stateInterp : StateInterp (DefSet prog) prog where instance stateInterp : StateInterpretation (DefSet prog) prog where
St := fun _ => Run prog St := fun _ => Run prog
init := Run.nil init := Run.nil
interp vs _ run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs → interp vs _ run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs →