-- |
-- 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 ((forall x. LLVMArch -> Rep LLVMArch x)
-> (forall x. Rep LLVMArch x -> LLVMArch) -> Generic LLVMArch
forall x. Rep LLVMArch x -> LLVMArch
forall x. LLVMArch -> Rep LLVMArch x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LLVMArch -> Rep LLVMArch x
from :: forall x. LLVMArch -> Rep LLVMArch x
$cto :: forall x. Rep LLVMArch x -> LLVMArch
to :: forall x. Rep LLVMArch x -> LLVMArch
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 :: forall (a :: LLVMArch) (b :: LLVMArch).
ArchRepr a -> ArchRepr b -> Maybe (a :~: b)
testEquality =
    $(U.structuralTypeEquality [t|ArchRepr|]
        [ (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
        ])

instance OrdF ArchRepr where
  compareF :: forall (x :: LLVMArch) (y :: LLVMArch).
ArchRepr x -> ArchRepr y -> OrderingF x y
compareF =
    $(U.structuralTypeOrd [t|ArchRepr|]
        [ (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|compareF|])
        ])