content: -----------------------------------------------------------------------
  -- |
  -- Module           : Lang.Crucible.Simulator.Intrinsics
  -- Description      : Basic definitions for defining intrinsic types
  -- Copyright        : (c) Galois, Inc 2015-2016
  -- License          : BSD3
  -- Maintainer       : Rob Dockins <rdockins@galois.com>
  -- Stability        : provisional
  --
  -- 'Intrinsic' types can be used to extend the basic set of types available
  -- to the Crucible simulator.  A new intrinsic type is defined by
  -- implementing an `IntrinsicClass` instance, which binds a type-level name
  -- to a particular impelementation.  To use an intrinsic type, one must
  -- register the associated `IntrinsicMuxFn` value with the simulator
  -- prior to starting it.  This is done by building an `IntrinsicMuxFns`
  -- map to be passed to the `initSimContext` function.
  -----------------------------------------------------------------------
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  module Lang.Crucible.Simulator.Intrinsics
    ( -- * Intrinsic types
      IntrinsicClass(..)
    , GetIntrinsic
    , IntrinsicMuxFn(..)
    , IntrinsicTypes
    , emptyIntrinsicTypes
    , typeError
    ) where
  
  import           Data.Kind
  import qualified Data.Parameterized.Map as MapF
  import           Data.Parameterized.SymbolRepr
  import qualified GHC.TypeLits (Symbol)
  import qualified GHC.TypeLits as TL
  import           GHC.Stack
  
  import           What4.Interface
  import           Lang.Crucible.Panic
  import           Lang.Crucible.Types
  
  -- | Type family for intrinsic type representations.  Intrinsic types
  --   are identified by a type-level `Symbol`, and this typeclass allows
  --   backends to define implementations for these types.
  --
  --   An instance of this class defines both an instance for the
  --   `Intrinsic` type family (which defines the runtime representation
  --   for this intrinsic type) and also the `muxIntrinsic` method
  --   (which defines how to merge to intrinsic values when the simulator
  --   reaches a merge point).
  --
  -- Note: Instances of this will typically end up as orphan instances.
  -- This warning is normally quite important, as orphan instances allow
  -- one to define multiple instances for a particular class.  However, in
  -- this case, 'IntrinsicClass' contains a type family, and GHC will globally
  -- check consistency of all type family instances.  Consequently, there
  -- can be at most one implementation of 'IntrinsicClass' in a program.
  class IntrinsicClass (sym :: Type) (nm :: GHC.TypeLits.Symbol) where
    -- | The 'Intrinsic' type family defines, for a given backend and symbol name,
    --   the runtime implementation of that Crucible intrinsic type.
    type Intrinsic (sym :: Type) (nm :: GHC.TypeLits.Symbol) (ctx :: Ctx CrucibleType) :: Type
  
    -- | The push branch function is called when an intrinsic value is
    --   passed through a symbolic branch.  This allows it to do any
    --   necessary bookkeeping to prepare for an upcoming merge.
    --   A push branch should eventually be followed by a matching
    --   abort or mux call.
    pushBranchIntrinsic
                 :: sym
                 -> IntrinsicTypes sym
                 -> SymbolRepr nm
                 -> CtxRepr ctx
                 -> Intrinsic sym nm ctx
                 -> IO (Intrinsic sym nm ctx)
    pushBranchIntrinsic _ _ _ _ = return
  
    -- | The abort branch function is called when an intrinsic value
    --   reaches a merge point, but the sibling branch has aborted.
    abortBranchIntrinsic
                 :: sym
                 -> IntrinsicTypes sym
                 -> SymbolRepr nm
                 -> CtxRepr ctx
                 -> Intrinsic sym nm ctx
                 -> IO (Intrinsic sym nm ctx)
    abortBranchIntrinsic _ _ _ _ = return
  
    -- | The `muxIntrinsic` method defines the if-then-else operation that is used
    --   when paths are merged in the simulator and intrinsic types need to be used.
    muxIntrinsic :: sym
                 -> IntrinsicTypes sym
                 -> SymbolRepr nm
                 -> CtxRepr ctx
                 -> Pred sym
                 -> Intrinsic sym nm ctx
                 -> Intrinsic sym nm ctx
                 -> IO (Intrinsic sym nm ctx)
  
  -- | Sometimes it is convenient to provide a 'CrucibleType' as the type
  -- argument to 'Intrinsic', rather than the symbol and context. If you
  -- accidentally supply a non-'IntrinsicType' type, this family will be stuck.
  type family GetIntrinsic sym ity where
    GetIntrinsic sym (IntrinsicType nm ctx) = Intrinsic sym nm ctx
    GetIntrinsic sym x = TL.TypeError
      (        ('TL.Text "Type mismatch:")
      'TL.:$$: ('TL.Text "  Expected ‘IntrinsicType a b’")
      'TL.:$$: ('TL.Text "  Actual " 'TL.:<>: 'TL.ShowType x)
      'TL.:$$: ('TL.Text "In type family application ‘GetIntrinsic (" 'TL.:<>: 'TL.ShowType sym 'TL.:<>: 'TL.Text ") (" 'TL.:<>: 'TL.ShowType x 'TL.:<>: 'TL.Text ")’")
      )
  
  -- | The `IntrinsicMuxFn` datatype allows an `IntrinsicClass` instance
  --   to be packaged up into a value.  This allows us to get access to 'IntrinsicClass'
  --   instance methods (the `muxIntrinsic` method in particular) at runtime even
  --   for symbol names that are not known statically.
  --
  --   By packaging up a type class instance (rather than just providing some method with the
  --   same signature as `muxIntrinsic`) we get the compiler to ensure that a single
  --   distinguished implementation is always used for each backend/symbol name combination.
  --   This prevents any possible confusion between different parts of the system.
  data IntrinsicMuxFn (sym :: Type) (nm :: Symbol) where
    IntrinsicMuxFn :: IntrinsicClass sym nm => IntrinsicMuxFn sym nm
  
  
  -- | `IntrinsicTypes` is a map from symbol name representatives to `IntrinsicMuxFn`
  --    values.  Such a map is useful for providing access to intrinsic type implementations
  --   that are not known statically at compile time.
  type IntrinsicTypes sym = MapF.MapF SymbolRepr (IntrinsicMuxFn sym)
  
  -- | An empty collection of intrinsic types, for cases where no additional types are required
  emptyIntrinsicTypes :: IntrinsicTypes sym
  emptyIntrinsicTypes = MapF.empty
  
  -- | Utility function for reporting errors when improper Crucible type arguments
  --   are applied to an intrinsic type symbol.
  typeError :: HasCallStack => SymbolRepr nm -> CtxRepr ctx -> b
  typeError nm ctx =
    panic "Crucible type error"
          [ "Named type constructor '" ++ show nm ++ "' applied to incorrect arguments:"
          , show ctx
          ]
  