content: -- |
  -- Module           : Lang.Crucible.LLVM.Arch
  -- Description      : Representations of LLVM architectures
  -- Copyright        : (c) Galois, Inc 2015-2018
  -- License          : BSD3
  -- Maintainer       : rdockins@galois.com
  -- Stability        : provisional
  ------------------------------------------------------------------------
  
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DeriveDataTypeable #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE TemplateHaskell #-}
  {-# LANGUAGE TypeFamilies #-}
  
  module Lang.Crucible.LLVM.Extension.Arch
    ( type LLVMArch
    , type X86
    , ArchWidth
    , ArchRepr(..)
    ) where
  
  import           GHC.Generics (Generic)
  import           Data.Parameterized (NatRepr)
  import           Data.Parameterized.Classes (OrdF(..))
  import qualified Data.Parameterized.TH.GADT as U
  import           Data.Type.Equality (TestEquality(..))
  import           Data.Typeable (Typeable)
  import           GHC.TypeLits (Nat)
  
  -- | Data kind for representing LLVM architectures.
  --   Currently only X86 variants are supported.
  data LLVMArch = X86 Nat
    deriving (Generic, Typeable)
  
  -- | LLVM Architecture tag for X86 variants
  --
  --   @X86 :: Nat -> LLVMArch@
  type X86 = 'X86
  
  -- | Type family defining the native machine word size
  --   for a given architecture.
  type family ArchWidth (arch :: LLVMArch) :: Nat where
    ArchWidth (X86 wptr) = wptr
  
  -- | Runtime representation of architectures.
  data ArchRepr (arch :: LLVMArch) where
    X86Repr :: NatRepr w -> ArchRepr (X86 w)
  
  $(return [])
  
  instance TestEquality ArchRepr where
    testEquality =
      $(U.structuralTypeEquality [t|ArchRepr|]
          [ (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
          ])
  
  instance OrdF ArchRepr where
    compareF =
      $(U.structuralTypeOrd [t|ArchRepr|]
          [ (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|compareF|])
          ])
  