From 040c13caba9490165bbba397a7fd22568c58ffd7 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 11 Mar 2024 12:50:05 -0700 Subject: [PATCH] Use instances to simplify printing code Signed-off-by: Danila Fedorin --- Analysis/Sign.agda | 26 ++++++++++++-------------- Lattice/AboveBelow.agda | 11 +++++++++++ Lattice/FiniteMap.agda | 6 ++++++ Lattice/Map.agda | 12 +++++++++++- Showable.agda | 38 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 78 insertions(+), 15 deletions(-) create mode 100644 Showable.agda diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda index 1fc555f..ca45e0f 100644 --- a/Analysis/Sign.agda +++ b/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 @@ -301,20 +312,7 @@ module WithProg (prog : Program) where 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 + output = show signs -- Debugging code: construct and run a program. diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda index 1ee94ae..970968a 100644 --- a/Lattice/AboveBelow.agda +++ b/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 ≈-⊥-⊥ : ⊥ ≈ ⊥ ≈-⊤-⊤ : ⊤ ≈ ⊤ diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda index 883914f..59d2f36 100644 --- a/Lattice/FiniteMap.agda +++ b/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₂ diff --git a/Lattice/Map.agda b/Lattice/Map.agda index afc86cd..cc7f0ea 100644 --- a/Lattice/Map.agda +++ b/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) diff --git a/Showable.agda b/Showable.agda new file mode 100644 index 0000000..62d4548 --- /dev/null +++ b/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 → "()" }