
   0 | module Text.Show.PrettyVal
   1 | 
   2 | import Data.List
   3 | import Data.List1
   4 | import Data.Vect
   5 | import Text.Show.Value
   6 | 
   7 | ||| A class for types that may be reified into a value.
   8 | ||| Instances of this class may be derived automatically,
   9 | ||| for datatypes that support `Generics`.
  10 | public export
  11 | interface PrettyVal a where
  12 |   constructor MkPrettyVal
  13 |   prettyVal : a -> Value
  14 | 
  15 | --------------------------------------------------------------------------------
  16 | --          Implementations
  17 | --------------------------------------------------------------------------------
  18 | 
  19 | public export
  20 | PrettyVal Void where
  21 |   prettyVal v impossible
  22 | 
  23 | public export
  24 | PrettyVal Value where
  25 |   prettyVal v = v
  26 | 
  27 | public export
  28 | PrettyVal () where
  29 |   prettyVal _ = Con "()" []
  30 | 
  31 | public export
  32 | PrettyVal Bits8 where
  33 |   prettyVal = Natural . show
  34 | 
  35 | public export
  36 | PrettyVal Bits16 where
  37 |   prettyVal = Natural . show
  38 | 
  39 | public export
  40 | PrettyVal Bits32 where
  41 |   prettyVal = Natural . show
  42 | 
  43 | public export
  44 | PrettyVal Bits64 where
  45 |   prettyVal = Natural . show
  46 | 
  47 | public export
  48 | PrettyVal Nat where
  49 |   prettyVal = Natural . show
  50 | 
  51 | mkNum :  (Ord a, Neg a, Num a, Show a)
  52 |       => (String -> Value) -> a -> Value
  53 | mkNum c x = if x >= 0 then c (show x)
  54 |                       else Neg . c . show $ negate x
  55 | 
  56 | public export
  57 | PrettyVal Int where
  58 |   prettyVal = mkNum Natural
  59 | 
  60 | public export
  61 | PrettyVal Int8 where
  62 |   prettyVal = mkNum Natural
  63 | 
  64 | public export
  65 | PrettyVal Int16 where
  66 |   prettyVal = mkNum Natural
  67 | 
  68 | public export
  69 | PrettyVal Int32 where
  70 |   prettyVal = mkNum Natural
  71 | 
  72 | public export
  73 | PrettyVal Int64 where
  74 |   prettyVal = mkNum Natural
  75 | 
  76 | public export
  77 | PrettyVal Integer where
  78 |   prettyVal = mkNum Natural
  79 | 
  80 | public export
  81 | PrettyVal Double where
  82 |   prettyVal = mkNum Dbl
  83 | 
  84 | public export
  85 | PrettyVal Char where
  86 |   prettyVal = Chr . show
  87 | 
  88 | public export
  89 | PrettyVal String where
  90 |   prettyVal = Str . show
  91 | 
  92 | public export
  93 | PrettyVal a => PrettyVal (List a) where
  94 |   prettyVal = Lst . map prettyVal
  95 | 
  96 | public export
  97 | PrettyVal a => PrettyVal (Vect n a) where
  98 |   prettyVal = Lst . toList . map prettyVal
  99 | 
 100 | public export
 101 | (PrettyVal a, PrettyVal b) => PrettyVal (a,b) where
 102 |   prettyVal (a,b) = case prettyVal b of
 103 |     Tuple v1 v2 vs => Tuple (prettyVal a) v1 (v2 :: vs)
 104 |     val            => Tuple (prettyVal a) val []
 105 |