Move more code out of Sign and into Main

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

Analysis/Sign.agda

@@ -13,6 +13,7 @@ open import Function using (_∘_)
 open import Language
 open import Lattice
 open import Utils using (Pairwise)
+open import Showable using (Showable; show)
 import Lattice.FiniteValueMap
 
 data Sign : Set where
@@ -20,6 +21,16 @@ data Sign : Set where
     - : Sign
     0ˢ : Sign
 
+instance
+    showable : Showable Sign
+    showable = record
+        { show = (λ
+            { + → "+"
+            ; - → "-"
+            ; 0ˢ → "0"
+            })
+        }
+
 -- g for siGn; s is used for strings and i is not very descriptive.
 _≟ᵍ_ : IsDecidable (_≡_ {_} {Sign})
 _≟ᵍ_ + + = yes refl
@@ -295,47 +306,4 @@ module WithProg (prog : Program) where
 
 
     -- 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)
+    output = show signs

Lattice/AboveBelow.agda

@@ -11,6 +11,7 @@ open import Data.Empty using (⊥-elim)
 open import Data.Product using (_,_)
 open import Data.Nat using (_≤_; ℕ; z≤n; s≤s; suc)
 open import Function using (_∘_)
+open import Showable using (Showable; show)
 open import Relation.Binary.PropositionalEquality as Eq
     using (_≡_; sym; subst; refl)
 
@@ -24,6 +25,16 @@ data AboveBelow : Set a where
     ⊤ : AboveBelow
     [_] : A → AboveBelow
 
+instance
+    showable : {{ showableA : Showable A }} → Showable AboveBelow
+    showable = record
+        { show = (λ
+            { ⊥ → "⊥"
+            ; ⊤ → "⊤"
+            ; [ a ] → show a
+            })
+        }
+
 data _≈_ : AboveBelow → AboveBelow → Set a where
     ≈-⊥-⊥ : ⊥ ≈ ⊥
     ≈-⊤-⊤ : ⊤ ≈ ⊤

Lattice/Bundles/FiniteValueMap.agda

@@ -1,30 +0,0 @@
-open import Relation.Binary.PropositionalEquality using (_≡_)
-open import Relation.Binary.Definitions using (Decidable)
-
-module Lattice.Bundles.FiniteValueMap (A B : Set) (≡-dec-A : Decidable (_≡_ {_} {A})) where
-
-open import Lattice
-open import Data.List using (List)
-open import Data.Nat using (ℕ)
-open import Utils using (Unique)
-
-module FromFiniteHeightLattice (fhB : FiniteHeightLattice B)
-                               {ks : List A} (uks : Unique ks)
-                               (≈₂-dec : Decidable (FiniteHeightLattice._≈_ fhB)) where
-
-    open Lattice.FiniteHeightLattice fhB using () renaming
-        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
-        ; height to height₂
-        ; isLattice to isLattice₂
-        ; fixedHeight to fixedHeight₂
-        )
-
-    import Lattice.FiniteMap
-    module FM = Lattice.FiniteMap ≡-dec-A isLattice₂
-    open FM.WithKeys ks public
-
-    import Lattice.FiniteValueMap
-    module FVM = Lattice.FiniteValueMap ≡-dec-A isLattice₂
-    open FVM.IterProdIsomorphism.WithUniqueKeysAndFixedHeight uks ≈₂-dec height₂ fixedHeight₂ public
-
-    ≈-dec = ≈₂-dec⇒≈-dec ≈₂-dec

Lattice/Bundles/IterProd.agda

@@ -1,38 +0,0 @@
-open import Lattice
-
-module Lattice.Bundles.IterProd {a} (A B : Set a) where
-open import Data.Nat using (ℕ)
-
-module _ (lA : Lattice A) (lB : Lattice B) where
-    open Lattice.Lattice lA using () renaming
-        ( _≈_ to _≈₁_; _⊔_ to _⊔₁_; _⊓_ to _⊓₁_
-        ; isLattice to isLattice₁
-        )
-
-    open Lattice.Lattice lB using () renaming
-        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
-        ; isLattice to isLattice₂
-        )
-
-    module _ (k : ℕ) where
-        open import Lattice.IterProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_ isLattice₁ isLattice₂ using (lattice) public
-
-module _ (fhA : FiniteHeightLattice A) (fhB : FiniteHeightLattice B) where
-    open Lattice.FiniteHeightLattice fhA using () renaming
-        ( _≈_ to _≈₁_; _⊔_ to _⊔₁_; _⊓_ to _⊓₁_
-        ; height to height₁
-        ; isLattice to isLattice₁
-        ; fixedHeight to fixedHeight₁
-        )
-
-    open Lattice.FiniteHeightLattice fhB using () renaming
-        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
-        ; height to height₂
-        ; isLattice to isLattice₂
-        ; fixedHeight to fixedHeight₂
-        )
-
-    module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) (k : ℕ) where
-        import Lattice.IterProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_ isLattice₁ isLattice₂ as IP
-
-        finiteHeightLattice = IP.finiteHeightLattice k ≈₁-dec ≈₂-dec height₁ height₂ fixedHeight₁ fixedHeight₂

Lattice/FiniteMap.agda

@@ -45,11 +45,17 @@ open import Function using (_∘_)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Utils using (Pairwise; _∷_; [])
 open import Data.Empty using (⊥-elim)
+open import Showable using (Showable; show)
 
 module WithKeys (ks : List A) where
     FiniteMap : Set (a ⊔ℓ b)
     FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)
 
+    instance
+        showable : {{ showableA : Showable A }} {{ showableB : Showable B }} →
+                   Showable FiniteMap
+        showable = record { show = λ (m₁ , _) → show m₁ }
+
     _≈_ : FiniteMap → FiniteMap → Set (a ⊔ℓ b)
     _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂
 

Lattice/Map.agda

@@ -13,13 +13,15 @@ open import Data.List.Membership.Propositional as MemProp using () renaming (_
 
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Data.Nat using (ℕ)
-open import Data.List using (List; map; []; _∷_; _++_)
+open import Data.List using (List; map; []; _∷_; _++_) renaming (foldr to foldrˡ)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
 open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Equivalence
 open import Utils using (Unique; push; Unique-append; All¬-¬Any; All-x∈xs)
+open import Data.String using () renaming (_++_ to _++ˢ_)
+open import Showable using (Showable; show)
 
 open IsLattice lB using () renaming
     ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
@@ -478,6 +480,14 @@ private module ImplInsert (f : B → B → B) where
 Map : Set (a ⊔ℓ b)
 Map = Σ (List (A × B)) (λ l → Unique (ImplKeys.keys l))
 
+instance
+    showable : {{ showableA : Showable A }} {{ showableB : Showable B }} →
+               Showable Map
+    showable = record
+        { show = λ (kvs , _) →
+            "{" ++ˢ foldrˡ (λ (x , y) rest → show x ++ˢ " ↦ " ++ˢ show y ++ˢ ", " ++ˢ rest) "" kvs ++ˢ "}"
+        }
+
 empty : Map
 empty = ([] , Utils.empty)
 

Main.agda

@@ -0,0 +1,25 @@
+module Main where
+
+open import Language
+open import Analysis.Sign
+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)

Showable.agda

@@ -0,0 +1,38 @@
+module Showable where
+
+open import Data.String using (String; _++_)
+open import Data.Nat using (ℕ)
+open import Data.Nat.Show using () renaming (show to showNat)
+open import Data.Fin using (Fin)
+open import Data.Fin.Show using () renaming (show to showFin)
+open import Data.Product using (_×_; _,_)
+open import Data.Unit using (⊤; tt)
+
+record Showable {a} (A : Set a) : Set a where
+    field
+        show : A → String
+
+open Showable {{ ... }} public
+
+instance
+    showableString : Showable String
+    showableString = record { show = λ s → "\"" ++ s ++ "\"" }
+
+    showableNat : Showable ℕ
+    showableNat = record { show = showNat }
+
+    showableFin : ∀ {n : ℕ} → Showable (Fin n)
+    showableFin = record { show = showFin }
+
+    showableProd : ∀ {a b} {A : Set a} {B : Set b}
+                     {{ showableA : Showable A }} {{ showableB : Showable B }} →
+                   Showable (A × B)
+    showableProd {{ showableA }} {{ showableB }} = record
+        { show = λ (a , b) →
+            "(" ++ show a ++
+            ", " ++ show b ++
+            ")"
+        }
+
+    showableUnit : Showable ⊤
+    showableUnit = record { show = λ tt → "()" }