Show.ds

module Class.Show
export
{       show; show_bool; show_nat;
        show_text;
        show_tup2;
        show_list;
}
import Data.Text
import Data.List
where


-- | Class dictionary for Show.
data Show (a: Data) where
        Show    : (a -> Text) -> Show a

show ((Show sh): Show a) (x: a): Text
 = sh x


-------------------------------------------------------------------------------
-- Instances for basic types.
-- We define these in this module to avoid making it recursive
-- with the modules that define basic data types.
show_bool       = Show showBool
show_nat        = Show showNat


-- ISSUE: #381: Escape non-printable characters in base Show library.
show_text: Show Text
 = Show sh
 where  sh tx           = "\"" % tx % "\""


show_tup2 ((Show sh_a): Show a) ((Show sh_b): Show b)
        : Show (Tup2 a b)
 = Show sh
 where  
        sh (T2 x y)     = parens $ "T2" %% sh_a x %% sh_b y


show_list ((Show sh_a): Show a): Show (List a)
 = Show sh
 where  
        sh Nil          = "Nil"
        sh (Cons x xs)  = parens $ "Cons" %% sh_a x %% sh xs