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

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

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

import Copilot.Core.Type

--------------------------------------------------------------------------------

-- | 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 :: Type a -> ShowWit a
showWit t :: Type a
t =
  case Type a
t of
    Bool   -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Int8   -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Int16  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Int32  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Int64  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Word8  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Word16 -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Word32 -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Word64 -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Float  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Double -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Array t :: Type t
t -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Struct t :: a
t -> ShowWit a
forall a. Show a => ShowWit a
ShowWit

--------------------------------------------------------------------------------

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

--------------------------------------------------------------------------------

-- 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 :: ShowType -> Type a -> a -> String
showWithType showT :: ShowType
showT t :: Type a
t x :: a
x =
  case ShowType
showT of
    C         -> case Type a
t of
                   Bool -> if a
Bool
x then "1" else "0"
                   _    -> String
sw
    Haskell   -> case Type a
t of
                   Bool -> if a
Bool
x then "true" else "false"
                   _    -> String
sw
  where
  sw :: String
sw = case Type a -> ShowWit a
forall a. Type a -> ShowWit a
showWit Type a
t of
         ShowWit -> a -> String
forall a. Show a => a -> String
show a
x

--------------------------------------------------------------------------------