Compare commits

..

No commits in common. "4ac9dffa9b046ba51e6b0de943942e0dbf4b1e1e" and "3859826293033ea1d4e7fd973a279141523d9fec" have entirely different histories.

4 changed files with 17 additions and 128 deletions

View File

@ -7,19 +7,17 @@ module Analysis.Forward
(isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_) (isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
(≈ˡ-dec : IsDecidable _≈ˡ_) where (≈ˡ-dec : IsDecidable _≈ˡ_) where
open import Data.Empty using (⊥-elim)
open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
open import Data.Nat using (suc) open import Data.Nat using (suc)
open import Data.Product using (_×_; proj₁; _,_) open import Data.Product using (_×_; proj₁; _,_)
open import Data.List using (List; _∷_; []; foldr; foldl; cartesianProduct; cartesianProductWith) open import Data.List using (List; _∷_; []; foldr; cartesianProduct; cartesianProductWith)
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
open import Data.List.Relation.Unary.Any as Any using ()
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst)
open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Unit using () open import Data.Unit using ()
open import Function using (_∘_; flip) open import Function using (_∘_)
open import Utils using (Pairwise; _⇒_) open import Utils using (Pairwise)
import Lattice.FiniteValueMap import Lattice.FiniteValueMap
open IsFiniteHeightLattice isFiniteHeightLatticeˡ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
@ -28,7 +26,6 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
( isLattice to isLatticeˡ ( isLattice to isLatticeˡ
; fixedHeight to fixedHeightˡ ; fixedHeight to fixedHeightˡ
; _≼_ to _≼ˡ_ ; _≼_ to _≼ˡ_
; ≈-sym to ≈ˡ-sym
) )
module WithProg (prog : Program) where module WithProg (prog : Program) where
@ -96,17 +93,6 @@ module WithProg (prog : Program) where
≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
-- We now have our (state -> (variables -> value)) map.
-- Define a couple of helpers to retrieve values from it. Specifically,
-- since the State type is as specific as possible, it's always possible to
-- retrieve the variable values at each state.
states-in-Map : (s : State) (sv : StateVariables) s ∈kᵐ sv
states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
variablesAt : State StateVariables VariableValues
variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
-- build up the 'join' function, which follows from Exercise 4.26's -- build up the 'join' function, which follows from Exercise 4.26's
-- --
-- L₁ → (A → L₂) -- L₁ → (A → L₂)
@ -130,15 +116,8 @@ module WithProg (prog : Program) where
renaming renaming
( f' to joinAll ( f' to joinAll
; f'-Monotonic to joinAll-Mono ; f'-Monotonic to joinAll-Mono
; f'-k∈ks-≡ to joinAll-k∈ks-≡
) )
variablesAt-joinAll : (s : State) (sv : StateVariables)
variablesAt s (joinAll sv) joinForKey s sv
variablesAt-joinAll s sv
with (vs , s,vs∈usv) locateᵐ {s} {joinAll sv} (states-in-Map s (joinAll sv)) =
joinAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
-- With 'join' in hand, we need to perform abstract evaluation. -- With 'join' in hand, we need to perform abstract evaluation.
module WithEvaluator (eval : Expr VariableValues L) module WithEvaluator (eval : Expr VariableValues L)
(eval-Mono : (e : Expr) Monotonic _≼ᵛ_ _≼ˡ_ (eval e)) where (eval-Mono : (e : Expr) Monotonic _≼ᵛ_ _≼ˡ_ (eval e)) where
@ -152,11 +131,12 @@ module WithProg (prog : Program) where
renaming renaming
( f' to updateVariablesFromExpression ( f' to updateVariablesFromExpression
; f'-Monotonic to updateVariablesFromExpression-Mono ; f'-Monotonic to updateVariablesFromExpression-Mono
; f'-k∈ks-≡ to updateVariablesFromExpression-k∈ks-≡
; f'-k∉ks-backward to updateVariablesFromExpression-k∉ks-backward
) )
public public
states-in-Map : (s : State) (sv : StateVariables) s ∈kᵐ sv
states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
-- The per-state update function makes use of the single-key setter, -- The per-state update function makes use of the single-key setter,
-- updateVariablesFromExpression, for the case where the statement -- updateVariablesFromExpression, for the case where the statement
-- is an assignment. -- is an assignment.
@ -175,7 +155,11 @@ module WithProg (prog : Program) where
updateVariablesForState : State StateVariables VariableValues updateVariablesForState : State StateVariables VariableValues
updateVariablesForState s sv = updateVariablesForState s sv =
foldl (flip updateVariablesFromStmt) (variablesAt s sv) (code s) let
bss = code s
(vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv)
in
foldr 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₂ =
@ -185,15 +169,14 @@ module WithProg (prog : Program) where
(vs₂ , s,vs₂∈sv₂) = locateᵐ {s} {sv₂} (states-in-Map s sv₂) (vs₂ , s,vs₂∈sv₂) = locateᵐ {s} {sv₂} (states-in-Map s sv₂)
vs₁≼vs₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ sv₁ sv₂ sv₁≼sv₂ s,vs₁∈sv₁ s,vs₂∈sv₂ vs₁≼vs₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ sv₁ sv₂ sv₁≼sv₂ s,vs₁∈sv₁ s,vs₂∈sv₂
in in
foldl-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss foldr-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss
(flip updateVariablesFromStmt) updateVariablesFromStmt-Monoʳ updateVariablesFromStmt updateVariablesFromStmt-Monoʳ
vs₁≼vs₂ vs₁≼vs₂
open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x x) (λ a₁≼a₂ a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x x) (λ a₁≼a₂ a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
renaming renaming
( f' to updateAll ( f' to updateAll
; f'-Monotonic to updateAll-Mono ; f'-Monotonic to updateAll-Mono
; f'-k∈ks-≡ to updateAll-k∈ks-≡
) )
-- Finally, the whole analysis consists of getting the 'join' -- Finally, the whole analysis consists of getting the 'join'
@ -211,62 +194,5 @@ module WithProg (prog : Program) where
-- The fixed point of the 'analyze' function is our final goal. -- The fixed point of the 'analyze' function is our final goal.
open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ analyze-Mono {m₁} {m₂} m₁≼m₂) open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ analyze-Mono {m₁} {m₂} m₁≼m₂)
using () using ()
renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result) renaming (aᶠ to result)
public public
variablesAt-updateAll : (s : State) (sv : StateVariables)
variablesAt s (updateAll sv) updateVariablesForState s sv
variablesAt-updateAll s sv
with (vs , s,vs∈usv) locateᵐ {s} {updateAll sv} (states-in-Map s (updateAll sv)) =
updateAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
open LatticeInterpretation latticeInterpretationˡ
using ()
renaming (⟦_⟧ to ⟦_⟧ˡ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ)
⟦_⟧ᵛ : VariableValues Env Set
⟦_⟧ᵛ vs ρ = {k l} (k , l) ∈ᵛ vs {v} (k , v) Language.∈ ρ l ⟧ˡ v
⟦⟧ᵛ-respects-≈ᵛ : {vs₁ vs₂ : VariableValues} vs₁ ≈ᵛ vs₂ vs₁ ⟧ᵛ vs₂ ⟧ᵛ
⟦⟧ᵛ-respects-≈ᵛ {m₁ , _} {m₂ , _}
(m₁⊆m₂ , m₂⊆m₁) ρ ⟦vs₁⟧ρ {k} {l} k,l∈m₂ {v} k,v∈ρ =
let
(l' , (l≈l' , k,l'∈m₁)) = m₂⊆m₁ _ _ k,l∈m₂
⟦l'⟧v = ⟦vs₁⟧ρ k,l'∈m₁ k,v∈ρ
in
⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v
InterpretationValid : Set
InterpretationValid = {vs ρ e v} ρ , e ⇒ᵉ v vs ⟧ᵛ ρ eval e vs ⟧ˡ v
module WithValidity (interpretationValidˡ : InterpretationValid) where
updateVariablesFromStmt-matches : {bs vs ρ₁ ρ₂} ρ₁ , bs ⇒ᵇ ρ₂ vs ⟧ᵛ ρ₁ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂
updateVariablesFromStmt-matches {_} {vs} {ρ₁} {ρ₁} (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ = ⟦vs⟧ρ
updateVariablesFromStmt-matches {_} {vs} {ρ₁} {_} (⇒ᵇ-← ρ₁ k e v ρ,e⇒v) ⟦vs⟧ρ {k'} {l} k',l∈vs' {v'} k',v'∈ρ₂
with k ≟ˢ k' | k',v'∈ρ₂
... | yes refl | here _ v _
rewrite updateVariablesFromExpression-k∈ks-≡ k e {l = vs} (Any.here refl) k',l∈vs' =
interpretationValidˡ ρ,e⇒v ⟦vs⟧ρ
... | yes k≡k' | there _ _ _ _ _ k'≢k _ = ⊥-elim (k'≢k (sym k≡k'))
... | no k≢k' | here _ _ _ = ⊥-elim (k≢k' refl)
... | no k≢k' | there _ _ _ _ _ _ k',v'∈ρ₁ =
let
k'∉[k] = (λ { (Any.here refl) k≢k' refl })
k',l∈vs = updateVariablesFromExpression-k∉ks-backward k e {l = vs} k'∉[k] k',l∈vs'
in
⟦vs⟧ρ k',l∈vs k',v'∈ρ₁
updateVariablesFromStmt-fold-matches : {bss vs ρ₁ ρ₂} ρ₁ , bss ⇒ᵇˢ ρ₂ vs ⟧ᵛ ρ₁ foldl (flip updateVariablesFromStmt) vs bss ⟧ᵛ ρ₂
updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ
updateVariablesFromStmt-fold-matches {bs bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ρ,bss'⇒ρ₂) ⟦vs⟧ρ =
updateVariablesFromStmt-fold-matches {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂ (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ)
updateVariablesForState-matches : {s sv ρ₁ ρ₂} ρ₁ , (code s) ⇒ᵇˢ ρ₂ variablesAt s sv ⟧ᵛ ρ₁ updateVariablesForState s sv ⟧ᵛ ρ₂
updateVariablesForState-matches = updateVariablesFromStmt-fold-matches
updateAll-matches : {s sv ρ₁ ρ₂} ρ₁ , (code s) ⇒ᵇˢ ρ₂ variablesAt s sv ⟧ᵛ ρ₁ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
updateAll-matches {s} {sv} ρ₁,bss⇒ρ ⟦vs⟧ρ rewrite variablesAt-updateAll s sv =
updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ ⟦vs⟧ρ

View File

@ -137,7 +137,7 @@ module _ {a b} {A : Set a} {B : Set b}
const-Mono : (x : B) Monotonic _≼₁_ _≼₂_ (λ _ x) const-Mono : (x : B) Monotonic _≼₁_ _≼₂_ (λ _ x)
const-Mono x _ = ⊔₂-idemp x const-Mono x _ = ⊔₂-idemp x
open import Data.List as List using (List; foldr; foldl; _∷_) open import Data.List as List using (List; foldr; _∷_)
open import Utils using (Pairwise; _∷_) open import Utils using (Pairwise; _∷_)
foldr-Mono : (l₁ l₂ : List A) (f : A B B) (b₁ b₂ : B) foldr-Mono : (l₁ l₂ : List A) (f : A B B) (b₁ b₂ : B)
@ -150,22 +150,13 @@ module _ {a b} {A : Set a} {B : Set b}
≼₂-trans (f-Mono₁ (foldr f b₁ xs) x≼y) ≼₂-trans (f-Mono₁ (foldr f b₁ xs) x≼y)
(f-Mono₂ y (foldr-Mono xs ys f b₁ b₂ xs≼ys b₁≼b₂ f-Mono₁ f-Mono₂)) (f-Mono₂ y (foldr-Mono xs ys f b₁ b₂ xs≼ys b₁≼b₂ f-Mono₁ f-Mono₂))
foldl-Mono : (l₁ l₂ : List A) (f : B A B) (b₁ b₂ : B)
Pairwise _≼₁_ l₁ l₂ b₁ ≼₂ b₂
( a Monotonic _≼₂_ _≼₂_ (λ b f b a))
( b Monotonic _≼₁_ _≼₂_ (f b))
foldl f b₁ l₁ ≼₂ foldl f b₂ l₂
foldl-Mono List.[] List.[] f b₁ b₂ _ b₁≼b₂ _ _ = b₁≼b₂
foldl-Mono (x xs) (y ys) f b₁ b₂ (x≼y xs≼ys) b₁≼b₂ f-Mono₁ f-Mono₂ =
foldl-Mono xs ys f (f b₁ x) (f b₂ y) xs≼ys (≼₂-trans (f-Mono₁ x b₁≼b₂) (f-Mono₂ b₂ x≼y)) f-Mono₁ f-Mono₂
module _ {a b} {A : Set a} {B : Set b} module _ {a b} {A : Set a} {B : Set b}
{_≈₂_ : B B Set b} {_⊔₂_ : B B B} {_≈₂_ : B B Set b} {_⊔₂_ : B B B}
(lB : IsSemilattice B _≈₂_ _⊔₂_) where (lB : IsSemilattice B _≈₂_ _⊔₂_) where
open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans) open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans)
open import Data.List as List using (List; foldr; foldl; _∷_) open import Data.List as List using (List; foldr; _∷_)
open import Utils using (Pairwise; _∷_) open import Utils using (Pairwise; _∷_)
foldr-Mono' : (l : List A) (f : A B B) foldr-Mono' : (l : List A) (f : A B B)
@ -174,12 +165,6 @@ module _ {a b} {A : Set a} {B : Set b}
foldr-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂ foldr-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
foldr-Mono' (x xs) f f-Mono₂ b₁≼b₂ = f-Mono₂ x (foldr-Mono' xs f f-Mono₂ b₁≼b₂) foldr-Mono' (x xs) f f-Mono₂ b₁≼b₂ = f-Mono₂ x (foldr-Mono' xs f f-Mono₂ b₁≼b₂)
foldl-Mono' : (l : List A) (f : B A B)
( b Monotonic _≼₂_ _≼₂_ (λ a f a b))
Monotonic _≼₂_ _≼₂_ (λ b foldl f b l)
foldl-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
foldl-Mono' (x xs) f f-Mono₁ b₁≼b₂ = foldl-Mono' xs f f-Mono₁ (f-Mono₁ x b₁≼b₂)
record IsLattice {a} (A : Set a) record IsLattice {a} (A : Set a)
(_≈_ : A A Set a) (_≈_ : A A Set a)
(_⊔_ : A A A) (_⊔_ : A A A)

View File

@ -35,11 +35,6 @@ open import Lattice.Map ≡-dec-A lB as Map
; keys to keysᵐ ; keys to keysᵐ
; _updating_via_ to _updatingᵐ_via_ ; _updating_via_ to _updatingᵐ_via_
; updating-via-keys-≡ to updatingᵐ-via-keys-≡ ; updating-via-keys-≡ to updatingᵐ-via-keys-≡
; updating-via-k∈ks to updatingᵐ-via-k∈ks
; updating-via-k∈ks-≡ to updatingᵐ-via-k∈ks-≡
; updating-via-∈k-forward to updatingᵐ-via-∈k-forward
; updating-via-k∉ks-forward to updatingᵐ-via-k∉ks-forward
; updating-via-k∉ks-backward to updatingᵐ-via-k∉ks-backward
; f'-Monotonic to f'-Monotonicᵐ ; f'-Monotonic to f'-Monotonicᵐ
; _≼_ to _≼ᵐ_ ; _≼_ to _≼ᵐ_
; ∈k-dec to ∈k-decᵐ ; ∈k-dec to ∈k-decᵐ
@ -88,8 +83,6 @@ module WithKeys (ks : List A) where
_∈k_ : A FiniteMap Set a _∈k_ : A FiniteMap Set a
_∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁) _∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁)
open Map using (forget) public
∈k-dec = ∈k-decᵐ ∈k-dec = ∈k-decᵐ
locate : {k : A} {fm : FiniteMap} k ∈k fm Σ B (λ v (k , v) fm) locate : {k : A} {fm : FiniteMap} k ∈k fm Σ B (λ v (k , v) fm)
@ -178,21 +171,6 @@ module WithKeys (ks : List A) where
f'-Monotonic : Monotonic _≼ˡ_ _≼_ f' f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂ f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂
f'-∈k-forward : {k l} k ∈k (f l) k ∈k (f' l)
f'-∈k-forward {k} {l} = updatingᵐ-via-∈k-forward (proj₁ (f l)) ks (updater l)
f'-k∈ks : {k l} k ∈ˡ ks k ∈k (f' l) (k , updater l k) (f' l)
f'-k∈ks {k} {l} = updatingᵐ-via-k∈ks (proj₁ (f l)) (updater l)
f'-k∈ks-≡ : {k v l} k ∈ˡ ks (k , v) (f' l) v updater l k
f'-k∈ks-≡ {k} {v} {l} = updatingᵐ-via-k∈ks-≡ (proj₁ (f l)) (updater l)
f'-k∉ks-forward : {k v l} ¬ k ∈ˡ ks (k , v) (f l) (k , v) (f' l)
f'-k∉ks-forward {k} {v} {l} = updatingᵐ-via-k∉ks-forward (proj₁ (f l)) (updater l)
f'-k∉ks-backward : {k v l} ¬ k ∈ˡ ks (k , v) (f' l) (k , v) (f l)
f'-k∉ks-backward {k} {v} {l} = updatingᵐ-via-k∉ks-backward (proj₁ (f l)) (updater l)
all-equal-keys : (fm₁ fm₂ : FiniteMap) (Map.keys (proj₁ fm₁) Map.keys (proj₁ fm₂)) all-equal-keys : (fm₁ fm₂ : FiniteMap) (Map.keys (proj₁ fm₁) Map.keys (proj₁ fm₂))
all-equal-keys (fm₁ , km₁≡ks) (fm₂ , km₂≡ks) = trans km₁≡ks (sym km₂≡ks) all-equal-keys (fm₁ , km₁≡ks) (fm₂ , km₂≡ks) = trans km₁≡ks (sym km₂≡ks)

View File

@ -32,7 +32,7 @@ open import Isomorphism using (IsInverseˡ; IsInverseʳ)
open import Lattice.Map ≡-dec-A lB open import Lattice.Map ≡-dec-A lB
using using
( subset-impl ( subset-impl
; locate ; locate; forget
; Map-functional ; Map-functional
; Expr-Provenance ; Expr-Provenance
; Expr-Provenance-≡ ; Expr-Provenance-≡