agda-spa/Analysis/Forward/Evaluation.agda

open import Language hiding (_[_])
open import Lattice

module Analysis.Forward.Evaluation
    (L : Set) {h}
    {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
    {{isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
    {{≈ˡ-dec : IsDecidable _≈ˡ_}}
    (prog : Program) where

open import Analysis.Forward.Lattices L prog
open import Data.Product using (_,_)

open IsFiniteHeightLattice isFiniteHeightLatticeˡ
    using ()
    renaming
        ( isLattice to isLatticeˡ
        ; _≼_ to _≼ˡ_
        )
open Program prog

-- The "full" version of the analysis ought to define a function
-- that analyzes each basic statement. For some analyses, the state ID
-- is used as part of the lattice, so include it here.
record StmtEvaluator : Set where
    field
        eval : State → BasicStmt → VariableValues → VariableValues
        eval-Monoʳ : ∀ (s : State) (bs : BasicStmt) → Monotonic _≼ᵛ_ _≼ᵛ_ (eval s bs)

-- For some "simpler" analyes, all we need to do is analyze the expressions.
-- For that purpose, provide a simpler evaluator type.
record ExprEvaluator : Set where
    field
        eval : Expr → VariableValues → L
        eval-Monoʳ : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)

-- Evaluators have a notion of being "valid", in which the (symbolic)
-- manipulations on lattice elements they perform match up with
-- the semantics. Define what it means to be valid for statement and
-- expression-based evaluators. Define "IsValidExprEvaluator"
-- and "IsValidStmtEvaluator" standalone so that users can use them
-- in their type expressions.

module _ {{evaluator : ExprEvaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where
    open ExprEvaluator evaluator
    open LatticeInterpretation interpretation

    IsValidExprEvaluator : Set
    IsValidExprEvaluator = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v

record ValidExprEvaluator (evaluator : ExprEvaluator)
                          (interpretation : LatticeInterpretation isLatticeˡ) : Set₁ where
    field
        valid : IsValidExprEvaluator {{evaluator}} {{interpretation}}

module _ {{evaluator : StmtEvaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where
    open StmtEvaluator evaluator
    open LatticeInterpretation interpretation

    IsValidStmtEvaluator : Set
    IsValidStmtEvaluator = ∀ {s vs ρ₁ ρ₂ bs} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ eval s bs vs ⟧ᵛ ρ₂

record ValidStmtEvaluator (evaluator : StmtEvaluator)
                           (interpretation : LatticeInterpretation isLatticeˡ) : Set₁ where
    field
        valid : IsValidStmtEvaluator {{evaluator}} {{interpretation}}