content: {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE ImplicitParams #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE PatternSynonyms #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE ViewPatterns #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  {-# OPTIONS_GHC -fno-warn-orphans #-}
  -----------------------------------------------------------------------
  -- |
  -- Module           : Lang.Crucible.LLVM.Types
  -- Description      : Crucible type definitions related to LLVM
  -- Copyright        : (c) Galois, Inc 2015-2016
  -- License          : BSD3
  -- Maintainer       : Rob Dockins <rdockins@galois.com>
  -- Stability        : provisional
  ------------------------------------------------------------------------
  module Lang.Crucible.LLVM.Types
    ( Mem
    , memRepr
    , LLVMPointerType
    , LLVMPtr
    , pattern LLVMPointerRepr
    , pattern PtrRepr
    , pattern SizeT
    , pattern SSizeT
    , withPtrWidth
    , HasPtrWidth
    , pattern PtrWidth
    , GlobalSymbol(..)
    , globalSymbolName
    ) where
  
  import           GHC.TypeNats
  import           Data.Typeable
  
  import           Data.Parameterized.Context
  
  import qualified Text.LLVM.AST as L
  
  import           Lang.Crucible.Simulator.RegValue
  import           Lang.Crucible.Types
  
  newtype GlobalSymbol = GlobalSymbol L.Symbol
    deriving (Typeable, Eq, Ord, Show)
  
  globalSymbolName :: GlobalSymbol -> String
  globalSymbolName (GlobalSymbol (L.Symbol nm)) = nm
  
  -- | The 'CrucibleType' of an LLVM memory. @'RegValue' sym 'Mem'@ is
  -- implemented as @'MemImpl' sym@.
  type Mem = IntrinsicType "LLVM_memory" EmptyCtx
  
  memRepr :: TypeRepr Mem
  memRepr = knownRepr
  
  -- | This constraint captures the idea that there is a distinguished
  --   pointer width in scope which is appropriate according to the C
  --   notion of pointer, and object size. In particular, it must be at
  --   least 16-bits wide (as required for the @size_t@ type).
  type HasPtrWidth w = (1 <= w, 16 <= w, ?ptrWidth :: NatRepr w)
  
  pattern PtrWidth :: HasPtrWidth w => w ~ w' => NatRepr w'
  pattern PtrWidth <- (testEquality ?ptrWidth -> Just Refl)
    where PtrWidth = ?ptrWidth
  
  withPtrWidth :: forall w a. (16 <= w) => NatRepr w -> (HasPtrWidth w => a) -> a
  withPtrWidth w a =
    case leqTrans (LeqProof :: LeqProof 1 16) (LeqProof :: LeqProof 16 w) of
      LeqProof -> let ?ptrWidth = w in a
  
  -- | Crucible type of pointers/bitvector values of width @w@.
  type LLVMPointerType w = IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w)
  
  -- | Symbolic LLVM pointer or bitvector values of width @w@.
  type LLVMPtr sym w = RegValue sym (LLVMPointerType w)
  
  -- | This pattern synonym makes it easy to build and destruct runtime
  --   representatives of @'LLVMPointerType' w@.
  pattern LLVMPointerRepr :: () => (1 <= w, ty ~ LLVMPointerType w) => NatRepr w -> TypeRepr ty
  pattern LLVMPointerRepr w <- IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "LLVM_pointer") -> Just Refl)
                                             (Empty :> BVRepr w)
    where
      LLVMPointerRepr w = IntrinsicRepr knownSymbol (Empty :> BVRepr w)
  
  -- | This pattern creates/matches against the TypeRepr for LLVM pointer values
  --   that are of the distinguished pointer width.
  pattern PtrRepr :: HasPtrWidth wptr => (ty ~ LLVMPointerType wptr) => TypeRepr ty
  pattern PtrRepr = LLVMPointerRepr PtrWidth
  
  -- | This pattern creates/matches against the TypeRepr for raw bitvector values
  --   that are of the distinguished pointer width.
  pattern SizeT :: HasPtrWidth wptr => (ty ~ BVType wptr) => TypeRepr ty
  pattern SizeT = BVRepr PtrWidth
  
  -- | This pattern creates/matches against the TypeRepr for raw signed bitvector values
  --   that are of the distinguished pointer width.
  pattern SSizeT :: HasPtrWidth wptr => (ty ~ BVType wptr) => TypeRepr ty
  pattern SSizeT = BVRepr PtrWidth
  