{-# 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 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)
type X86 = 'X86
type family ArchWidth (arch :: LLVMArch) :: Nat where
ArchWidth (X86 wptr) = wptr
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|])
])