Analysis/Sign.agda

@@ -13,7 +13,6 @@ 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
@@ -21,16 +20,6 @@ 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
@@ -306,4 +295,47 @@ module WithProg (prog : Program) where
 
 
     -- Debugging code: print the resulting map.
-    output = show signs
+    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)

Lattice/AboveBelow.agda

@@ -11,7 +11,6 @@ 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)
 
@@ -25,16 +24,6 @@ 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

@@ -0,0 +1,30 @@
+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

@@ -0,0 +1,38 @@
+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,17 +45,11 @@ 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,15 +13,13 @@ 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; []; _∷_; _++_) renaming (foldr to foldrˡ)
+open import Data.List using (List; map; []; _∷_; _++_)
 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
@@ -480,14 +478,6 @@ 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

@@ -1,25 +0,0 @@
-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

@@ -1,38 +0,0 @@
-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 → "()" }