-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.

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

-- | Show Copilot Core types and typed values.
module Copilot.PrettyPrint.Type
  ( showWithType
  , ShowType(..)
  , showType
  ) where

import Copilot.Core.Type

-- Are we proving equivalence with a C backend, in which case we want to show
-- Booleans as '0' and '1'.

-- | 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
Bool
x then String
"1" else String
"0"
                   Type a
_    -> String
sw
    ShowType
Haskell   -> case Type a
t of
                   Type a
Bool -> if a
Bool
x then String
"true" else String
"false"
                   Type a
_    -> String
sw
  where
  sw :: String
sw = case Type a -> ShowWit a
forall a. Type a -> ShowWit a
showWit Type a
t of
         ShowWit a
ShowWit -> a -> String
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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type t -> String
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   -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Int8   -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Int16  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Int32  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Int64  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Word8  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Word16 -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Word32 -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Word64 -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Float  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Double -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Array Type t
t -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Struct a
t -> ShowWit a
forall a. Show a => ShowWit a
ShowWit