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