Add some debugging code to sign analysis to print the results

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

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)

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

Main.agda

@@ -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ᶠ))