diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda index 14a0ceb..1fc555f 100644 --- a/Analysis/Sign.agda +++ b/Analysis/Sign.agda @@ -8,6 +8,7 @@ open import Data.List.Membership.Propositional as MemProp using () renaming (_ open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst) open import Relation.Nullary using (¬_; Dec; yes; no) open import Data.Unit using (⊤) +open import Function using (_∘_) open import Language open import Lattice @@ -99,7 +100,7 @@ minus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ postulate minus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → minus s₁ s₂) postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (minus s₁) -module _ (prog : Program) where +module WithProg (prog : Program) where open Program prog -- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators. @@ -157,6 +158,7 @@ module _ (prog : Program) where ) ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec + fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ -- build up the 'join' function, which follows from Exercise 4.26's -- @@ -243,7 +245,7 @@ module _ (prog : Program) where eval-Mono (# (suc n')) _ _ = ≈ᵍ-refl private module _ (k : String) (e : Expr) (k∈e⇒k∈vars : ∀ k → k ∈ᵉ e → k ∈ˡ vars) where - open VariableSignsFiniteMap.GeneralizedUpdate vars isLatticeᵛ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → eval e k∈e⇒k∈vars) (λ _ → eval-Mono e k∈e⇒k∈vars) (k ∷ []) + open VariableSignsFiniteMap.GeneralizedUpdate vars isLatticeᵛ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → eval e k∈e⇒k∈vars) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → eval-Mono e k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂) (k ∷ []) renaming ( f' to updateVariablesFromExpression ; f'-Monotonic to updateVariablesFromExpression-Mono @@ -275,12 +277,65 @@ module _ (prog : Program) where in updateVariablesFromExpression-Mono k e (λ k k∈e → k∈codes⇒k∈vars k (in←₂ k∈e)) {vs₁} {vs₂} vs₁≼vs₂ - open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ joinAll (λ {a₁} {a₂} a₁≼a₂ → joinAll-Mono {a₁} {a₂} a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states + open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states renaming ( f' to updateAll ; f'-Monotonic to updateAll-Mono ) - open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ updateAll (λ {m₁} {m₂} m₁≼m₂ → updateAll-Mono {m₁} {m₂} m₁≼m₂) + analyze : StateVariables → StateVariables + analyze = updateAll ∘ joinAll + + analyze-Mono : Monotonic _≼ᵐ_ _≼ᵐ_ analyze + analyze-Mono {sv₁} {sv₂} sv₁≼sv₂ = updateAll-Mono {joinAll sv₁} {joinAll sv₂} (joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂) + + open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂) using () renaming (aᶠ to signs) + + + -- Debugging code: print the resulting map. + open import Data.Fin using (suc; zero) + open import Data.Fin.Show using () renaming (show to showFin) + open import Data.Nat.Show using () renaming (show to showNat) + open import Data.String using (_++_) + open import Data.List using () renaming (length to lengthˡ) + + showAboveBelow : AB.AboveBelow → String + showAboveBelow AB.⊤ = "⊤" + showAboveBelow AB.⊥ = "⊥" + showAboveBelow (AB.[_] +) = "+" + showAboveBelow (AB.[_] -) = "-" + showAboveBelow (AB.[_] 0ˢ) = "0" + + showVarSigns : VariableSigns → String + showVarSigns ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → x ++ " ↦ " ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}" + + showStateVars : StateVariables → String + showStateVars ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → (showFin x) ++ " ↦ " ++ showVarSigns y ++ ", " ++ rest) "" kvs ++ "}" + + output = showStateVars signs + + +-- Debugging code: construct and run a program. +open import Data.Vec using (Vec; _∷_; []) +open import IO +open import Level using (0ℓ) + +testCode : Vec Stmt _ +testCode = + ("zero" ← (# 0)) ∷ + ("pos" ← ((` "zero") Expr.+ (# 1))) ∷ + ("neg" ← ((` "zero") Expr.- (# 1))) ∷ + ("unknown" ← ((` "pos") Expr.+ (` "neg"))) ∷ + [] + +testProgram : Program +testProgram = record + { length = _ + ; stmts = testCode + } + +open WithProg testProgram using (output) + +main = run {0ℓ} (putStrLn output) diff --git a/Language.agda b/Language.agda index 4bf0be7..a9bc644 100644 --- a/Language.agda +++ b/Language.agda @@ -198,7 +198,7 @@ record Program : Set where _≟_ : IsDecidable (_≡_ {_} {State}) _≟_ = _≟ᶠ_ - -- Computations for incoming and outgoing edged will have to change too + -- Computations for incoming and outgoing edges will have to change too -- when we support branching etc. incoming : State → List State diff --git a/Main.agda b/Main.agda deleted file mode 100644 index 8230d58..0000000 --- a/Main.agda +++ /dev/null @@ -1,55 +0,0 @@ -module Main where - -open import IO -open import Level using (0ℓ) -open import Data.Nat.Show using (show) -open import Data.List using (List; _∷_; []; foldr) -open import Data.String using (String; _++_) renaming (_≟_ to _≟ˢ_) -open import Data.Unit using (⊤; tt) renaming (_≟_ to _≟ᵘ_) -open import Data.Product using (_,_; _×_; proj₁; proj₂) -open import Data.List.Relation.Unary.All using (_∷_; []) -open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl; trans) -open import Relation.Nullary using (¬_) - -open import Utils using (Unique; push; empty) - -xyzw : List String -xyzw = "x" ∷ "y" ∷ "z" ∷ "w" ∷ [] - -xyzw-Unique : Unique xyzw -xyzw-Unique = push ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ []) (push [] empty))) - -open import Lattice using (IsFiniteHeightLattice; FiniteHeightLattice; Monotonic) - -open import Lattice.AboveBelow ⊤ _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵘ_ as AB using () renaming (≈-dec to ≈ᵘ-dec) -open AB.Plain (Data.Unit.tt) using () renaming (finiteHeightLattice to fhlᵘ) - -showAboveBelow : AB.AboveBelow → String -showAboveBelow AB.⊤ = "⊤" -showAboveBelow AB.⊥ = "⊥" -showAboveBelow (AB.[_] tt) = "()" - -import Lattice.Bundles.FiniteValueMap -open Lattice.Bundles.FiniteValueMap.FromFiniteHeightLattice String AB.AboveBelow _≟ˢ_ fhlᵘ xyzw-Unique ≈ᵘ-dec using (FiniteMap; ≈-dec) renaming (finiteHeightLattice to fhlⁱᵖ) - -showMap : FiniteMap → String -showMap ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → x ++ " ↦ " ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}" - -open FiniteHeightLattice fhlⁱᵖ using (_≈_; _⊔_; _⊓_; ⊔-idemp; _≼_; ≈-⊔-cong; ≈-refl; ≈-trans; ≈-sym; ⊔-assoc; ⊔-comm; ⊔-Monotonicˡ) -open import Relation.Binary.Reasoning.Base.Single _≈_ (λ {m} → ≈-refl {m}) (λ {m₁} {m₂} {m₃} → ≈-trans {m₁} {m₂} {m₃}) -- why am I having to eta-expand here? - -smallestMap = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ))) -largestMap = proj₂ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ))) - -dumb : FiniteMap -dumb = ((("x" , AB.[_] tt) ∷ ("y" , AB.⊥) ∷ ("z" , AB.⊥) ∷ ("w" , AB.⊥) ∷ [] , xyzw-Unique) , refl) - -dumbFunction : FiniteMap → FiniteMap -dumbFunction = _⊔_ dumb - -dumbFunction-Monotonic : Monotonic _≼_ _≼_ dumbFunction -dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂ = ⊔-Monotonicˡ dumb {m₁} {m₂} m₁≼m₂ - -open import Fixedpoint {0ℓ} {FiniteMap} {8} {_≈_} {_⊔_} {_⊓_} ≈-dec (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂) - -main = run {0ℓ} (putStrLn (showMap aᶠ))