    -- 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