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 → "()" }