content: {- |
  Module           : Lang.Crucible.CFG.Common
  Description      : Common CFG datastructure definitions
  Copyright        : (c) Galois, Inc 2014-2016
  License          : BSD3
  Maintainer       : Joe Hendrix <jhendrix@galois.com>
  
  Data structures and operations that are common to both the
  registerized and the SSA form CFG representations.
  -}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE RankNTypes #-}
  module Lang.Crucible.CFG.Common
    ( -- * Global variables
      GlobalVar(..)
    , freshGlobalVar
    , BreakpointName(..)
    ) where
  
  import           Data.Text (Text)
  import qualified Data.Text as Text
  import           Prettyprinter
  
  import           Data.Parameterized.Classes
  import           Data.Parameterized.Nonce
  
  import           Lang.Crucible.FunctionHandle
  import           Lang.Crucible.Types
  
  ------------------------------------------------------------------------
  -- GlobalVar
  
  -- | A global variable.
  data GlobalVar (tp :: CrucibleType)
     = GlobalVar { globalNonce :: {-# UNPACK #-} !(Nonce GlobalNonceGenerator tp)
                 , globalName  :: !Text
                 , globalType  :: !(TypeRepr tp)
                 }
  
  instance TestEquality GlobalVar where
    x `testEquality` y = globalNonce x `testEquality` globalNonce y
  
  instance OrdF GlobalVar where
    x `compareF` y = globalNonce x `compareF` globalNonce y
  
  instance Show (GlobalVar tp) where
    show = Text.unpack . globalName
  
  instance ShowF GlobalVar
  
  instance Pretty (GlobalVar tp) where
    pretty = pretty . globalName
  
  
  freshGlobalVar :: HandleAllocator
                 -> Text
                 -> TypeRepr tp
                 -> IO (GlobalVar tp)
  freshGlobalVar halloc nm tp = do
    nonce <- freshNonce (haCounter halloc)
    return GlobalVar
           { globalNonce = nonce
           , globalName  = nm
           , globalType  = tp
           }
  
  newtype BreakpointName = BreakpointName { breakpointNameText :: Text }
    deriving (Eq, Ord, Show)
  
  instance Pretty BreakpointName where
    pretty = pretty . breakpointNameText
  