224 lines
9.7 KiB
Agda
224 lines
9.7 KiB
Agda
|
|
|||
|
|
module Analysis.Constant where
|
|||
|
|
|
|||
|
|
open import Data.Integer as Int using (ℤ; +_; -[1+_]; _≟_)
|
|||
|
|
open import Data.Integer.Show as IntShow using ()
|
|||
|
|
open import Data.Nat as Nat using (ℕ; suc; zero)
|
|||
|
|
open import Data.Product using (Σ; proj₁; proj₂; _,_)
|
|||
|
|
open import Data.Sum using (inj₁; inj₂)
|
|||
|
|
open import Data.Empty using (⊥; ⊥-elim)
|
|||
|
|
open import Data.Unit using (⊤; tt)
|
|||
|
|
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
|
|||
|
|
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst)
|
|||
|
|
open import Relation.Nullary using (¬_; yes; no)
|
|||
|
|
|
|||
|
|
open import Equivalence
|
|||
|
|
open import Language
|
|||
|
|
open import Lattice
|
|||
|
|
open import Showable using (Showable; show)
|
|||
|
|
open import Utils using (_⇒_; _∧_; _∨_)
|
|||
|
|
open import Analysis.Utils using (eval-combine₂)
|
|||
|
|
import Analysis.Forward
|
|||
|
|
|
|||
|
|
instance
|
|||
|
|
showable : Showable ℤ
|
|||
|
|
showable = record
|
|||
|
|
{ show = IntShow.show
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
instance
|
|||
|
|
≡-equiv : IsEquivalence ℤ _≡_
|
|||
|
|
≡-equiv = record
|
|||
|
|
{ ≈-refl = refl
|
|||
|
|
; ≈-sym = sym
|
|||
|
|
; ≈-trans = trans
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
≡-Decidable-ℤ : IsDecidable {_} {ℤ} _≡_
|
|||
|
|
≡-Decidable-ℤ = record { R-dec = _≟_ }
|
|||
|
|
|
|||
|
|
-- embelish 'ℕ' with a top and bottom element.
|
|||
|
|
open import Lattice.AboveBelow ℤ _ as AB
|
|||
|
|
using ()
|
|||
|
|
renaming
|
|||
|
|
( AboveBelow to ConstLattice
|
|||
|
|
; ≈-dec to ≈ᶜ-dec
|
|||
|
|
; ⊥ to ⊥ᶜ
|
|||
|
|
; ⊤ to ⊤ᶜ
|
|||
|
|
; [_] to [_]ᶜ
|
|||
|
|
; _≈_ to _≈ᶜ_
|
|||
|
|
; ≈-⊥-⊥ to ≈ᶜ-⊥ᶜ-⊥ᶜ
|
|||
|
|
; ≈-⊤-⊤ to ≈ᶜ-⊤ᶜ-⊤ᶜ
|
|||
|
|
; ≈-lift to ≈ᶜ-lift
|
|||
|
|
; ≈-refl to ≈ᶜ-refl
|
|||
|
|
)
|
|||
|
|
-- 'ℕ''s structure is not finite, so just use a 'plain' above-below Lattice.
|
|||
|
|
open AB.Plain (+ 0) using ()
|
|||
|
|
renaming
|
|||
|
|
( isLattice to isLatticeᶜ
|
|||
|
|
; isFiniteHeightLattice to isFiniteHeightLatticeᵍ
|
|||
|
|
; _≼_ to _≼ᶜ_
|
|||
|
|
; _⊔_ to _⊔ᶜ_
|
|||
|
|
; _⊓_ to _⊓ᶜ_
|
|||
|
|
; ≼-trans to ≼ᶜ-trans
|
|||
|
|
; ≼-refl to ≼ᶜ-refl
|
|||
|
|
)
|
|||
|
|
|
|||
|
|
plus : ConstLattice → ConstLattice → ConstLattice
|
|||
|
|
plus ⊥ᶜ _ = ⊥ᶜ
|
|||
|
|
plus _ ⊥ᶜ = ⊥ᶜ
|
|||
|
|
plus ⊤ᶜ _ = ⊤ᶜ
|
|||
|
|
plus _ ⊤ᶜ = ⊤ᶜ
|
|||
|
|
plus [ z₁ ]ᶜ [ z₂ ]ᶜ = [ z₁ Int.+ z₂ ]ᶜ
|
|||
|
|
|
|||
|
|
-- this is incredibly tedious: 125 cases per monotonicity proof, and tactics
|
|||
|
|
-- are hard. postulate for now.
|
|||
|
|
postulate plus-Monoˡ : ∀ (s₂ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (λ s₁ → plus s₁ s₂)
|
|||
|
|
postulate plus-Monoʳ : ∀ (s₁ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (plus s₁)
|
|||
|
|
|
|||
|
|
plus-Mono₂ : Monotonic₂ _≼ᶜ_ _≼ᶜ_ _≼ᶜ_ plus
|
|||
|
|
plus-Mono₂ = (plus-Monoˡ , plus-Monoʳ)
|
|||
|
|
|
|||
|
|
minus : ConstLattice → ConstLattice → ConstLattice
|
|||
|
|
minus ⊥ᶜ _ = ⊥ᶜ
|
|||
|
|
minus _ ⊥ᶜ = ⊥ᶜ
|
|||
|
|
minus ⊤ᶜ _ = ⊤ᶜ
|
|||
|
|
minus _ ⊤ᶜ = ⊤ᶜ
|
|||
|
|
minus [ z₁ ]ᶜ [ z₂ ]ᶜ = [ z₁ Int.- z₂ ]ᶜ
|
|||
|
|
|
|||
|
|
postulate minus-Monoˡ : ∀ (s₂ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (λ s₁ → minus s₁ s₂)
|
|||
|
|
postulate minus-Monoʳ : ∀ (s₁ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (minus s₁)
|
|||
|
|
|
|||
|
|
minus-Mono₂ : Monotonic₂ _≼ᶜ_ _≼ᶜ_ _≼ᶜ_ minus
|
|||
|
|
minus-Mono₂ = (minus-Monoˡ , minus-Monoʳ)
|
|||
|
|
|
|||
|
|
⟦_⟧ᶜ : ConstLattice → Value → Set
|
|||
|
|
⟦_⟧ᶜ ⊥ᶜ _ = ⊥
|
|||
|
|
⟦_⟧ᶜ ⊤ᶜ _ = ⊤
|
|||
|
|
⟦_⟧ᶜ [ z ]ᶜ v = v ≡ ↑ᶻ z
|
|||
|
|
|
|||
|
|
⟦⟧ᶜ-respects-≈ᶜ : ∀ {s₁ s₂ : ConstLattice} → s₁ ≈ᶜ s₂ → ⟦ s₁ ⟧ᶜ ⇒ ⟦ s₂ ⟧ᶜ
|
|||
|
|
⟦⟧ᶜ-respects-≈ᶜ ≈ᶜ-⊥ᶜ-⊥ᶜ v bot = bot
|
|||
|
|
⟦⟧ᶜ-respects-≈ᶜ ≈ᶜ-⊤ᶜ-⊤ᶜ v top = top
|
|||
|
|
⟦⟧ᶜ-respects-≈ᶜ (≈ᶜ-lift { z } { z } refl) v proof = proof
|
|||
|
|
|
|||
|
|
⟦⟧ᶜ-⊔ᶜ-∨ : ∀ {s₁ s₂ : ConstLattice} → (⟦ s₁ ⟧ᶜ ∨ ⟦ s₂ ⟧ᶜ) ⇒ ⟦ s₁ ⊔ᶜ s₂ ⟧ᶜ
|
|||
|
|
⟦⟧ᶜ-⊔ᶜ-∨ {⊥ᶜ} x (inj₂ px₂) = px₂
|
|||
|
|
⟦⟧ᶜ-⊔ᶜ-∨ {⊤ᶜ} x _ = tt
|
|||
|
|
⟦⟧ᶜ-⊔ᶜ-∨ {[ s₁ ]ᶜ} {[ s₂ ]ᶜ} x px
|
|||
|
|
with s₁ ≟ s₂
|
|||
|
|
... | no _ = tt
|
|||
|
|
... | yes refl
|
|||
|
|
with px
|
|||
|
|
... | inj₁ px₁ = px₁
|
|||
|
|
... | inj₂ px₂ = px₂
|
|||
|
|
⟦⟧ᶜ-⊔ᶜ-∨ {[ s₁ ]ᶜ} {⊥ᶜ} x (inj₁ px₁) = px₁
|
|||
|
|
⟦⟧ᶜ-⊔ᶜ-∨ {[ s₁ ]ᶜ} {⊤ᶜ} x _ = tt
|
|||
|
|
|
|||
|
|
s₁≢s₂⇒¬s₁∧s₂ : ∀ {z₁ z₂ : ℤ} → ¬ z₁ ≡ z₂ → ∀ {v} → ¬ ((⟦ [ z₁ ]ᶜ ⟧ᶜ ∧ ⟦ [ z₂ ]ᶜ ⟧ᶜ) v)
|
|||
|
|
s₁≢s₂⇒¬s₁∧s₂ { z₁ } { z₂ } z₁≢z₂ {v} (v≡z₁ , v≡z₂)
|
|||
|
|
with refl ← trans (sym v≡z₁) v≡z₂ = z₁≢z₂ refl
|
|||
|
|
|
|||
|
|
⟦⟧ᶜ-⊓ᶜ-∧ : ∀ {s₁ s₂ : ConstLattice} → (⟦ s₁ ⟧ᶜ ∧ ⟦ s₂ ⟧ᶜ) ⇒ ⟦ s₁ ⊓ᶜ s₂ ⟧ᶜ
|
|||
|
|
⟦⟧ᶜ-⊓ᶜ-∧ {⊥ᶜ} x (bot , _) = bot
|
|||
|
|
⟦⟧ᶜ-⊓ᶜ-∧ {⊤ᶜ} x (_ , px₂) = px₂
|
|||
|
|
⟦⟧ᶜ-⊓ᶜ-∧ {[ s₁ ]ᶜ} {[ s₂ ]ᶜ} x (px₁ , px₂)
|
|||
|
|
with s₁ ≟ s₂
|
|||
|
|
... | no s₁≢s₂ = s₁≢s₂⇒¬s₁∧s₂ s₁≢s₂ (px₁ , px₂)
|
|||
|
|
... | yes refl = px₁
|
|||
|
|
⟦⟧ᶜ-⊓ᶜ-∧ {[ g₁ ]ᶜ} {⊥ᶜ} x (_ , bot) = bot
|
|||
|
|
⟦⟧ᶜ-⊓ᶜ-∧ {[ g₁ ]ᶜ} {⊤ᶜ} x (px₁ , _) = px₁
|
|||
|
|
|
|||
|
|
instance
|
|||
|
|
latticeInterpretationᶜ : LatticeInterpretation isLatticeᶜ
|
|||
|
|
latticeInterpretationᶜ = record
|
|||
|
|
{ ⟦_⟧ = ⟦_⟧ᶜ
|
|||
|
|
; ⟦⟧-respects-≈ = ⟦⟧ᶜ-respects-≈ᶜ
|
|||
|
|
; ⟦⟧-⊔-∨ = ⟦⟧ᶜ-⊔ᶜ-∨
|
|||
|
|
; ⟦⟧-⊓-∧ = ⟦⟧ᶜ-⊓ᶜ-∧
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
module WithProg (prog : Program) where
|
|||
|
|
open Program prog
|
|||
|
|
|
|||
|
|
open import Analysis.Forward.Lattices ConstLattice prog
|
|||
|
|
open import Analysis.Forward.Evaluation ConstLattice prog
|
|||
|
|
open import Analysis.Forward.Adapters ConstLattice prog
|
|||
|
|
|
|||
|
|
eval : ∀ (e : Expr) → VariableValues → ConstLattice
|
|||
|
|
eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
|
|||
|
|
eval (e₁ - e₂) vs = minus (eval e₁ vs) (eval e₂ vs)
|
|||
|
|
eval (` k) vs
|
|||
|
|
with ∈k-decᵛ k (proj₁ (proj₁ vs))
|
|||
|
|
... | yes k∈vs = proj₁ (locateᵛ {k} {vs} k∈vs)
|
|||
|
|
... | no _ = ⊤ᶜ
|
|||
|
|
eval (# n) _ = [ + n ]ᶜ
|
|||
|
|
|
|||
|
|
eval-Monoʳ : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᶜ_ (eval e)
|
|||
|
|
eval-Monoʳ (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ =
|
|||
|
|
eval-combine₂ (λ {x} {y} {z} → ≼ᶜ-trans {x} {y} {z})
|
|||
|
|
plus plus-Mono₂ {o₁ = eval e₁ vs₁}
|
|||
|
|
(eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂)
|
|||
|
|
eval-Monoʳ (e₁ - e₂) {vs₁} {vs₂} vs₁≼vs₂ =
|
|||
|
|
eval-combine₂ (λ {x} {y} {z} → ≼ᶜ-trans {x} {y} {z})
|
|||
|
|
minus minus-Mono₂ {o₁ = eval e₁ vs₁}
|
|||
|
|
(eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂)
|
|||
|
|
eval-Monoʳ (` k) {vs₁@((kvs₁ , _) , _)} {vs₂@((kvs₂ , _), _)} vs₁≼vs₂
|
|||
|
|
with ∈k-decᵛ k kvs₁ | ∈k-decᵛ k kvs₂
|
|||
|
|
... | yes k∈kvs₁ | yes k∈kvs₂ =
|
|||
|
|
let
|
|||
|
|
(v₁ , k,v₁∈vs₁) = locateᵛ {k} {vs₁} k∈kvs₁
|
|||
|
|
(v₂ , k,v₂∈vs₂) = locateᵛ {k} {vs₂} k∈kvs₂
|
|||
|
|
in
|
|||
|
|
m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂
|
|||
|
|
... | yes k∈kvs₁ | no k∉kvs₂ = ⊥-elim (k∉kvs₂ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₁ vs₂) k∈kvs₁))
|
|||
|
|
... | no k∉kvs₁ | yes k∈kvs₂ = ⊥-elim (k∉kvs₁ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₂ vs₁) k∈kvs₂))
|
|||
|
|
... | no k∉kvs₁ | no k∉kvs₂ = IsLattice.≈-refl isLatticeᶜ
|
|||
|
|
eval-Monoʳ (# n) _ = ≼ᶜ-refl ([ + n ]ᶜ)
|
|||
|
|
|
|||
|
|
instance
|
|||
|
|
ConstEval : ExprEvaluator
|
|||
|
|
ConstEval = record { eval = eval; eval-Monoʳ = eval-Monoʳ }
|
|||
|
|
|
|||
|
|
-- For debugging purposes, print out the result.
|
|||
|
|
output = show (Analysis.Forward.WithProg.result ConstLattice prog)
|
|||
|
|
|
|||
|
|
-- This should have fewer cases -- the same number as the actual 'plus' above.
|
|||
|
|
-- But agda only simplifies on first argument, apparently, so we are stuck
|
|||
|
|
-- listing them all.
|
|||
|
|
plus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᶜ (↑ᶻ z₁) → ⟦ g₂ ⟧ᶜ (↑ᶻ z₂) → ⟦ plus g₁ g₂ ⟧ᶜ (↑ᶻ (z₁ Int.+ z₂))
|
|||
|
|
plus-valid {⊥ᶜ} {_} ⊥ _ = ⊥
|
|||
|
|
plus-valid {[ z ]ᶜ} {⊥ᶜ} _ ⊥ = ⊥
|
|||
|
|
plus-valid {⊤ᶜ} {⊥ᶜ} _ ⊥ = ⊥
|
|||
|
|
plus-valid {⊤ᶜ} {[ z ]ᶜ} _ _ = tt
|
|||
|
|
plus-valid {⊤ᶜ} {⊤ᶜ} _ _ = tt
|
|||
|
|
plus-valid {[ z₁ ]ᶜ} {[ z₂ ]ᶜ} refl refl = refl
|
|||
|
|
plus-valid {[ z ]ᶜ} {⊤ᶜ} _ _ = tt
|
|||
|
|
--
|
|||
|
|
-- Same for this one. It should be easier, but Agda won't simplify.
|
|||
|
|
minus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᶜ (↑ᶻ z₁) → ⟦ g₂ ⟧ᶜ (↑ᶻ z₂) → ⟦ minus g₁ g₂ ⟧ᶜ (↑ᶻ (z₁ Int.- z₂))
|
|||
|
|
minus-valid {⊥ᶜ} {_} ⊥ _ = ⊥
|
|||
|
|
minus-valid {[ z ]ᶜ} {⊥ᶜ} _ ⊥ = ⊥
|
|||
|
|
minus-valid {⊤ᶜ} {⊥ᶜ} _ ⊥ = ⊥
|
|||
|
|
minus-valid {⊤ᶜ} {[ z ]ᶜ} _ _ = tt
|
|||
|
|
minus-valid {⊤ᶜ} {⊤ᶜ} _ _ = tt
|
|||
|
|
minus-valid {[ z₁ ]ᶜ} {[ z₂ ]ᶜ} refl refl = refl
|
|||
|
|
minus-valid {[ z ]ᶜ} {⊤ᶜ} _ _ = tt
|
|||
|
|
|
|||
|
|
eval-valid : IsValidExprEvaluator
|
|||
|
|
eval-valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
|
|||
|
|
plus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
|
|||
|
|
eval-valid (⇒ᵉ-- ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
|
|||
|
|
minus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
|
|||
|
|
eval-valid {vs} (⇒ᵉ-Var ρ x v x,v∈ρ) ⟦vs⟧ρ
|
|||
|
|
with ∈k-decᵛ x (proj₁ (proj₁ vs))
|
|||
|
|
... | yes x∈kvs = ⟦vs⟧ρ (proj₂ (locateᵛ {x} {vs} x∈kvs)) x,v∈ρ
|
|||
|
|
... | no x∉kvs = tt
|
|||
|
|
eval-valid (⇒ᵉ-ℕ ρ n) _ = refl
|
|||
|
|
|
|||
|
|
instance
|
|||
|
|
ConstEvalValid : ValidExprEvaluator ConstEval latticeInterpretationᶜ
|
|||
|
|
ConstEvalValid = record { valid = eval-valid }
|
|||
|
|
|
|||
|
|
analyze-correct = Analysis.Forward.WithProg.analyze-correct ConstLattice prog tt
|