{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE Safe                      #-}

-- |
-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.
--
-- Show Copilot Core types and typed values.
module Copilot.Core.Type.ShowInternal
    ( showWithType
    , ShowType (..)
    , showType
    )
  where

-- Internal imports
import Copilot.Core.Type (Type (..))

-- | Target language for showing a typed value. Used to adapt the
-- representation of booleans.
data ShowType = C | Haskell

-- | Show a value. The representation depends on the type and the target
-- language. Booleans are represented differently depending on the backend.
showWithType :: ShowType -> Type a -> a -> String
showWithType :: forall a. ShowType -> Type a -> a -> String
showWithType ShowType
showT Type a
t a
x =
    case ShowType
showT of
      ShowType
C       -> case Type a
t of
                   Type a
Bool -> if a
x then String
"1" else String
"0"
                   Type a
_    -> String
sw
      ShowType
Haskell -> case Type a
t of
                   Type a
Bool -> if a
x then String
"true" else String
"false"
                   Type a
_    -> String
sw
  where
    sw :: String
sw = case forall a. Type a -> ShowWit a
showWit Type a
t of
           ShowWit a
ShowWit -> forall a. Show a => a -> String
show a
x

-- | Show Copilot Core type.
showType :: Type a -> String
showType :: forall a. Type a -> String
showType Type a
t =
  case Type a
t of
    Type a
Bool     -> String
"Bool"
    Type a
Int8     -> String
"Int8"
    Type a
Int16    -> String
"Int16"
    Type a
Int32    -> String
"Int32"
    Type a
Int64    -> String
"Int64"
    Type a
Word8    -> String
"Word8"
    Type a
Word16   -> String
"Word16"
    Type a
Word32   -> String
"Word32"
    Type a
Word64   -> String
"Word64"
    Type a
Float    -> String
"Float"
    Type a
Double   -> String
"Double"
    Array Type t
t  -> String
"Array " forall a. [a] -> [a] -> [a]
++ forall a. Type a -> String
showType Type t
t
    Struct a
t -> String
"Struct"

-- * Auxiliary show instance

-- | Witness datatype for showing a value, used by 'showWithType'.
data ShowWit a = Show a => ShowWit

-- | Turn a type into a show witness.
showWit :: Type a -> ShowWit a
showWit :: forall a. Type a -> ShowWit a
showWit Type a
t =
  case Type a
t of
    Type a
Bool     -> forall a. Show a => ShowWit a
ShowWit
    Type a
Int8     -> forall a. Show a => ShowWit a
ShowWit
    Type a
Int16    -> forall a. Show a => ShowWit a
ShowWit
    Type a
Int32    -> forall a. Show a => ShowWit a
ShowWit
    Type a
Int64    -> forall a. Show a => ShowWit a
ShowWit
    Type a
Word8    -> forall a. Show a => ShowWit a
ShowWit
    Type a
Word16   -> forall a. Show a => ShowWit a
ShowWit
    Type a
Word32   -> forall a. Show a => ShowWit a
ShowWit
    Type a
Word64   -> forall a. Show a => ShowWit a
ShowWit
    Type a
Float    -> forall a. Show a => ShowWit a
ShowWit
    Type a
Double   -> forall a. Show a => ShowWit a
ShowWit
    Array Type t
t  -> forall a. Show a => ShowWit a
ShowWit
    Struct a
t -> forall a. Show a => ShowWit a
ShowWit