{-
Module           : Lang.Crucible.FunctionHandle
Copyright        : (c) Galois, Inc 2014-2016
Maintainer       : Joe Hendrix <jhendrix@galois.com>
License          : BSD3

This provides handles to functions, which provides a unique
identifier of a function at runtime.  Function handles can be thought of
as function pointers, but there are no operations to manipulate them.
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.FunctionHandle
  ( -- * Function handle
    FnHandle
  , handleID
  , handleName
  , handleArgTypes
  , handleReturnType
  , handleType
  , SomeHandle(..)
    -- * Allocate handle.
  , HandleAllocator
  , haCounter
  , newHandleAllocator
  , withHandleAllocator
  , mkHandle
  , mkHandle'
    -- * FnHandleMap
  , FnHandleMap
  , emptyHandleMap
  , insertHandleMap
  , lookupHandleMap
  , updateHandleMap
  , searchHandleMap
  , handleMapToHandles
    -- * Reference cells
  , RefCell
  , freshRefCell
  , refType
  ) where

import           Data.Hashable
import           Data.Kind
import           Data.Functor.Identity
import qualified Data.List as List
import           Data.Ord (comparing)

import           Data.Parameterized.Classes
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.Nonce
import           Data.Parameterized.Some ( Some(Some) )

import           What4.FunctionName

import           Lang.Crucible.Types

------------------------------------------------------------------------
-- FunctionHandle

-- | A handle uniquely identifies a function.  The signature indicates the
--   expected argument types and the return type of the function.
data FnHandle (args :: Ctx CrucibleType) (ret :: CrucibleType)
   = H { forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID         :: !(Nonce GlobalNonceGenerator (args ::> ret))
         -- ^ A unique identifier for the function.
       , forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
handleName       :: !FunctionName
         -- ^ The name of the function (not necessarily unique)
       , forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> CtxRepr args
handleArgTypes   :: !(CtxRepr args)
         -- ^ The arguments types for the function
       , forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr ret
handleReturnType :: !(TypeRepr ret)
         -- ^ The return type of the function.
       }

instance Eq (FnHandle args ret) where
  FnHandle args ret
h1 == :: FnHandle args ret -> FnHandle args ret -> Bool
== FnHandle args ret
h2 = FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle args ret
h1 Nonce GlobalNonceGenerator (args ::> ret)
-> Nonce GlobalNonceGenerator (args ::> ret) -> Bool
forall a. Eq a => a -> a -> Bool
== FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle args ret
h2

instance Ord (FnHandle args ret) where
  compare :: FnHandle args ret -> FnHandle args ret -> Ordering
compare FnHandle args ret
h1 FnHandle args ret
h2 = (FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret))
-> FnHandle args ret -> FnHandle args ret -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle args ret
h1 FnHandle args ret
h2

instance Show (FnHandle args ret) where
  show :: FnHandle args ret -> String
show FnHandle args ret
h = FunctionName -> String
forall a. Show a => a -> String
show (FnHandle args ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
handleName FnHandle args ret
h)

instance Hashable (FnHandle args ret) where
  hashWithSalt :: Int -> FnHandle args ret -> Int
hashWithSalt Int
s FnHandle args ret
h = Int -> Nonce GlobalNonceGenerator (args ::> ret) -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle args ret
h)

-- | Return type of handle.
handleType :: FnHandle args ret -> TypeRepr (FunctionHandleType args ret)
handleType :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr (FunctionHandleType args ret)
handleType FnHandle args ret
h = CtxRepr args
-> TypeRepr ret -> TypeRepr ('FunctionHandleType args ret)
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr ctx
-> TypeRepr ret -> TypeRepr ('FunctionHandleType ctx ret)
FunctionHandleRepr (FnHandle args ret -> CtxRepr args
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> CtxRepr args
handleArgTypes FnHandle args ret
h) (FnHandle args ret -> TypeRepr ret
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr ret
handleReturnType FnHandle args ret
h)

------------------------------------------------------------------------
-- SomeHandle

-- | A function handle is a reference to a function in a given
-- run of the simulator.  It has a set of expected arguments and return type.
data SomeHandle where
   SomeHandle :: !(FnHandle args ret) -> SomeHandle

instance Eq SomeHandle where
  SomeHandle FnHandle args ret
x == :: SomeHandle -> SomeHandle -> Bool
== SomeHandle FnHandle args ret
y = Maybe ((args ::> ret) :~: (args ::> ret)) -> Bool
forall a. Maybe a -> Bool
isJust (Nonce GlobalNonceGenerator (args ::> ret)
-> Nonce GlobalNonceGenerator (args ::> ret)
-> Maybe ((args ::> ret) :~: (args ::> ret))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType).
Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator b -> Maybe (a :~: b)
testEquality (FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle args ret
x) (FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle args ret
y))

instance Ord SomeHandle where
  compare :: SomeHandle -> SomeHandle -> Ordering
compare (SomeHandle FnHandle args ret
x) (SomeHandle FnHandle args ret
y) = OrderingF (args ::> ret) (args ::> ret) -> Ordering
forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (Nonce GlobalNonceGenerator (args ::> ret)
-> Nonce GlobalNonceGenerator (args ::> ret)
-> OrderingF (args ::> ret) (args ::> ret)
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType).
Nonce GlobalNonceGenerator x
-> Nonce GlobalNonceGenerator y -> OrderingF x y
compareF (FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle args ret
x) (FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle args ret
y))

instance Hashable SomeHandle where
  hashWithSalt :: Int -> SomeHandle -> Int
hashWithSalt Int
s (SomeHandle FnHandle args ret
x) = Int -> Nonce GlobalNonceGenerator (args ::> ret) -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle args ret
x)

instance Show SomeHandle where
  show :: SomeHandle -> String
show (SomeHandle FnHandle args ret
h) = FunctionName -> String
forall a. Show a => a -> String
show (FnHandle args ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
handleName FnHandle args ret
h)


------------------------------------------------------------------------
-- HandleAllocator

-- | Used to allocate function handles.
newtype HandleAllocator
   = HA ()

haCounter :: HandleAllocator -> NonceGenerator IO GlobalNonceGenerator
haCounter :: HandleAllocator -> NonceGenerator IO GlobalNonceGenerator
haCounter HandleAllocator
_ha = NonceGenerator IO GlobalNonceGenerator
globalNonceGenerator

-- | Create a new handle allocator.
newHandleAllocator :: IO (HandleAllocator)
newHandleAllocator :: IO HandleAllocator
newHandleAllocator = HandleAllocator -> IO HandleAllocator
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (() -> HandleAllocator
HA ())

-- | Create a new handle allocator and run the given computation.
withHandleAllocator :: (HandleAllocator -> IO a) -> IO a
withHandleAllocator :: forall a. (HandleAllocator -> IO a) -> IO a
withHandleAllocator HandleAllocator -> IO a
k = IO HandleAllocator
newHandleAllocator IO HandleAllocator -> (HandleAllocator -> IO a) -> IO a
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= HandleAllocator -> IO a
k

-- | Allocate a new function handle with requested 'args' and 'ret' types
mkHandle :: (KnownCtx TypeRepr args, KnownRepr TypeRepr ret)
         => HandleAllocator
         -> FunctionName
         -> IO (FnHandle args ret)
mkHandle :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
(KnownCtx TypeRepr args, KnownRepr TypeRepr ret) =>
HandleAllocator -> FunctionName -> IO (FnHandle args ret)
mkHandle HandleAllocator
a FunctionName
nm = HandleAllocator
-> FunctionName
-> Assignment TypeRepr args
-> TypeRepr ret
-> IO (FnHandle args ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
HandleAllocator
-> FunctionName
-> Assignment TypeRepr args
-> TypeRepr ret
-> IO (FnHandle args ret)
mkHandle' HandleAllocator
a FunctionName
nm Assignment TypeRepr args
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr TypeRepr ret
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

-- | Allocate a new function handle.
mkHandle' :: HandleAllocator
          -> FunctionName
          -> Ctx.Assignment TypeRepr args
          -> TypeRepr ret
          -> IO (FnHandle args ret)
mkHandle' :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
HandleAllocator
-> FunctionName
-> Assignment TypeRepr args
-> TypeRepr ret
-> IO (FnHandle args ret)
mkHandle' HandleAllocator
_ha FunctionName
nm Assignment TypeRepr args
args TypeRepr ret
ret = do
  Nonce GlobalNonceGenerator (args ::> ret)
i <- NonceGenerator IO GlobalNonceGenerator
-> IO (Nonce GlobalNonceGenerator (args ::> ret))
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO GlobalNonceGenerator
globalNonceGenerator
  FnHandle args ret -> IO (FnHandle args ret)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (FnHandle args ret -> IO (FnHandle args ret))
-> FnHandle args ret -> IO (FnHandle args ret)
forall a b. (a -> b) -> a -> b
$! H { handleID :: Nonce GlobalNonceGenerator (args ::> ret)
handleID   = Nonce GlobalNonceGenerator (args ::> ret)
i
              , handleName :: FunctionName
handleName = FunctionName
nm
              , handleArgTypes :: Assignment TypeRepr args
handleArgTypes   = Assignment TypeRepr args
args
              , handleReturnType :: TypeRepr ret
handleReturnType = TypeRepr ret
ret
              }

------------------------------------------------------------------------
-- Reference cells

data RefCell (tp :: CrucibleType)
   = RefCell (TypeRepr tp) (Nonce GlobalNonceGenerator tp)

refType :: RefCell tp -> TypeRepr tp
refType :: forall (tp :: CrucibleType). RefCell tp -> TypeRepr tp
refType (RefCell TypeRepr tp
tpr Nonce GlobalNonceGenerator tp
_) = TypeRepr tp
tpr

freshRefCell :: HandleAllocator
             -> TypeRepr tp
             -> IO (RefCell tp)
freshRefCell :: forall (tp :: CrucibleType).
HandleAllocator -> TypeRepr tp -> IO (RefCell tp)
freshRefCell HandleAllocator
_ha TypeRepr tp
tpr =
  TypeRepr tp -> Nonce GlobalNonceGenerator tp -> RefCell tp
forall (tp :: CrucibleType).
TypeRepr tp -> Nonce GlobalNonceGenerator tp -> RefCell tp
RefCell TypeRepr tp
tpr (Nonce GlobalNonceGenerator tp -> RefCell tp)
-> IO (Nonce GlobalNonceGenerator tp) -> IO (RefCell tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> NonceGenerator IO GlobalNonceGenerator
-> IO (Nonce GlobalNonceGenerator tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO GlobalNonceGenerator
globalNonceGenerator

instance Show (RefCell tp) where
  show :: RefCell tp -> String
show (RefCell TypeRepr tp
_ Nonce GlobalNonceGenerator tp
n) = Nonce GlobalNonceGenerator tp -> String
forall a. Show a => a -> String
show Nonce GlobalNonceGenerator tp
n

instance ShowF RefCell where

instance TestEquality RefCell where
  testEquality :: forall (a :: CrucibleType) (b :: CrucibleType).
RefCell a -> RefCell b -> Maybe (a :~: b)
testEquality (RefCell TypeRepr a
_ Nonce GlobalNonceGenerator a
x) (RefCell TypeRepr b
_ Nonce GlobalNonceGenerator b
y) =
    case Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator b -> Maybe (a :~: b)
testEquality Nonce GlobalNonceGenerator a
x Nonce GlobalNonceGenerator b
y of
      Just a :~: b
Refl -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
      Maybe (a :~: b)
Nothing   -> Maybe (a :~: b)
forall a. Maybe a
Nothing

instance OrdF RefCell where
  compareF :: forall (x :: CrucibleType) (y :: CrucibleType).
RefCell x -> RefCell y -> OrderingF x y
compareF (RefCell TypeRepr x
_tx Nonce GlobalNonceGenerator x
x) (RefCell TypeRepr y
_ty Nonce GlobalNonceGenerator y
y) =
    case Nonce GlobalNonceGenerator x
-> Nonce GlobalNonceGenerator y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
Nonce GlobalNonceGenerator x
-> Nonce GlobalNonceGenerator y -> OrderingF x y
compareF Nonce GlobalNonceGenerator x
x Nonce GlobalNonceGenerator y
y of
      OrderingF x y
LTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
      OrderingF x y
EQF -> OrderingF x x
OrderingF x y
forall {k} (x :: k). OrderingF x x
EQF
      OrderingF x y
GTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF

instance Eq (RefCell tp) where
  RefCell tp
x == :: RefCell tp -> RefCell tp -> Bool
== RefCell tp
y = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (RefCell tp -> RefCell tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
RefCell a -> RefCell b -> Maybe (a :~: b)
testEquality RefCell tp
x RefCell tp
y)

instance Ord (RefCell tp) where
  compare :: RefCell tp -> RefCell tp -> Ordering
compare RefCell tp
x RefCell tp
y = OrderingF tp tp -> Ordering
forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (RefCell tp -> RefCell tp -> OrderingF tp tp
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
RefCell x -> RefCell y -> OrderingF x y
compareF RefCell tp
x RefCell tp
y)

------------------------------------------------------------------------
-- FnHandleMap

data HandleElt (f :: Ctx CrucibleType -> CrucibleType -> Type) ctx where
  HandleElt :: FnHandle args ret -> f args ret -> HandleElt f (args::>ret)

newtype FnHandleMap f = FnHandleMap (MapF (Nonce GlobalNonceGenerator) (HandleElt f))

emptyHandleMap :: FnHandleMap f
emptyHandleMap :: forall (f :: Ctx CrucibleType -> CrucibleType -> Type).
FnHandleMap f
emptyHandleMap = MapF (Nonce GlobalNonceGenerator) (HandleElt f) -> FnHandleMap f
forall (f :: Ctx CrucibleType -> CrucibleType -> Type).
MapF (Nonce GlobalNonceGenerator) (HandleElt f) -> FnHandleMap f
FnHandleMap MapF (Nonce GlobalNonceGenerator) (HandleElt f)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty

insertHandleMap :: FnHandle args ret
                -> f args ret
                -> FnHandleMap f
                -> FnHandleMap f
insertHandleMap :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (f :: Ctx CrucibleType -> CrucibleType -> Type).
FnHandle args ret -> f args ret -> FnHandleMap f -> FnHandleMap f
insertHandleMap FnHandle args ret
hdl f args ret
x (FnHandleMap MapF (Nonce GlobalNonceGenerator) (HandleElt f)
m) =
    MapF (Nonce GlobalNonceGenerator) (HandleElt f) -> FnHandleMap f
forall (f :: Ctx CrucibleType -> CrucibleType -> Type).
MapF (Nonce GlobalNonceGenerator) (HandleElt f) -> FnHandleMap f
FnHandleMap (Nonce GlobalNonceGenerator (args ::> ret)
-> HandleElt f (args ::> ret)
-> MapF (Nonce GlobalNonceGenerator) (HandleElt f)
-> MapF (Nonce GlobalNonceGenerator) (HandleElt f)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert (FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle args ret
hdl) (FnHandle args ret -> f args ret -> HandleElt f (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (f :: Ctx CrucibleType -> CrucibleType -> Type).
FnHandle args ret -> f args ret -> HandleElt f (args ::> ret)
HandleElt FnHandle args ret
hdl f args ret
x) MapF (Nonce GlobalNonceGenerator) (HandleElt f)
m)

-- | Lookup the function specification in the map via the Nonce index
-- in the FnHandle argument.
lookupHandleMap :: FnHandle args ret
                -> FnHandleMap f
                -> Maybe (f args ret)
lookupHandleMap :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (f :: Ctx CrucibleType -> CrucibleType -> Type).
FnHandle args ret -> FnHandleMap f -> Maybe (f args ret)
lookupHandleMap FnHandle args ret
hdl (FnHandleMap MapF (Nonce GlobalNonceGenerator) (HandleElt f)
m) =
  case Nonce GlobalNonceGenerator (args ::> ret)
-> MapF (Nonce GlobalNonceGenerator) (HandleElt f)
-> Maybe (HandleElt f (args ::> ret))
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup (FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle args ret
hdl) MapF (Nonce GlobalNonceGenerator) (HandleElt f)
m of
     Just (HandleElt FnHandle args ret
_ f args ret
x) -> f args ret -> Maybe (f args ret)
forall a. a -> Maybe a
Just f args ret
f args ret
x
     Maybe (HandleElt f (args ::> ret))
Nothing -> Maybe (f args ret)
forall a. Maybe a
Nothing

-- | Update the entry of the function handle in the map.
updateHandleMap :: (f args ret -> f args ret)
                -> FnHandle args ret
                -> FnHandleMap f
                -> FnHandleMap f
updateHandleMap :: forall (f :: Ctx CrucibleType -> CrucibleType -> Type)
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(f args ret -> f args ret)
-> FnHandle args ret -> FnHandleMap f -> FnHandleMap f
updateHandleMap f args ret -> f args ret
f FnHandle args ret
hdl (FnHandleMap MapF (Nonce GlobalNonceGenerator) (HandleElt f)
m) =
  MapF (Nonce GlobalNonceGenerator) (HandleElt f) -> FnHandleMap f
forall (f :: Ctx CrucibleType -> CrucibleType -> Type).
MapF (Nonce GlobalNonceGenerator) (HandleElt f) -> FnHandleMap f
FnHandleMap (MapF (Nonce GlobalNonceGenerator) (HandleElt f) -> FnHandleMap f)
-> MapF (Nonce GlobalNonceGenerator) (HandleElt f) -> FnHandleMap f
forall a b. (a -> b) -> a -> b
$ Updated (MapF (Nonce GlobalNonceGenerator) (HandleElt f))
-> MapF (Nonce GlobalNonceGenerator) (HandleElt f)
forall a. Updated a -> a
MapF.updatedValue (Updated (MapF (Nonce GlobalNonceGenerator) (HandleElt f))
 -> MapF (Nonce GlobalNonceGenerator) (HandleElt f))
-> Updated (MapF (Nonce GlobalNonceGenerator) (HandleElt f))
-> MapF (Nonce GlobalNonceGenerator) (HandleElt f)
forall a b. (a -> b) -> a -> b
$ Identity
  (Updated (MapF (Nonce GlobalNonceGenerator) (HandleElt f)))
-> Updated (MapF (Nonce GlobalNonceGenerator) (HandleElt f))
forall a. Identity a -> a
runIdentity (Identity
   (Updated (MapF (Nonce GlobalNonceGenerator) (HandleElt f)))
 -> Updated (MapF (Nonce GlobalNonceGenerator) (HandleElt f)))
-> Identity
     (Updated (MapF (Nonce GlobalNonceGenerator) (HandleElt f)))
-> Updated (MapF (Nonce GlobalNonceGenerator) (HandleElt f))
forall a b. (a -> b) -> a -> b
$
    Nonce GlobalNonceGenerator (args ::> ret)
-> Identity (Maybe (HandleElt f (args ::> ret)))
-> (HandleElt f (args ::> ret)
    -> Identity (UpdateRequest (HandleElt f (args ::> ret))))
-> MapF (Nonce GlobalNonceGenerator) (HandleElt f)
-> Identity
     (Updated (MapF (Nonce GlobalNonceGenerator) (HandleElt f)))
forall {v} (k :: v -> Type) (f :: Type -> Type) (tp :: v)
       (a :: v -> Type).
(OrdF k, Functor f) =>
k tp
-> f (Maybe (a tp))
-> (a tp -> f (UpdateRequest (a tp)))
-> MapF k a
-> f (Updated (MapF k a))
MapF.updateAtKey
      (FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle args ret
hdl)
      (Maybe (HandleElt f (args ::> ret))
-> Identity (Maybe (HandleElt f (args ::> ret)))
forall a. a -> Identity a
Identity Maybe (HandleElt f (args ::> ret))
forall a. Maybe a
Nothing)
      (\(HandleElt FnHandle args ret
hdl' f args ret
x) -> UpdateRequest (HandleElt f (args ::> ret))
-> Identity (UpdateRequest (HandleElt f (args ::> ret)))
forall a. a -> Identity a
Identity (UpdateRequest (HandleElt f (args ::> ret))
 -> Identity (UpdateRequest (HandleElt f (args ::> ret))))
-> UpdateRequest (HandleElt f (args ::> ret))
-> Identity (UpdateRequest (HandleElt f (args ::> ret)))
forall a b. (a -> b) -> a -> b
$ HandleElt f (args ::> ret)
-> UpdateRequest (HandleElt f (args ::> ret))
forall v. v -> UpdateRequest v
MapF.Set (HandleElt f (args ::> ret)
 -> UpdateRequest (HandleElt f (args ::> ret)))
-> HandleElt f (args ::> ret)
-> UpdateRequest (HandleElt f (args ::> ret))
forall a b. (a -> b) -> a -> b
$ FnHandle args ret -> f args ret -> HandleElt f (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (f :: Ctx CrucibleType -> CrucibleType -> Type).
FnHandle args ret -> f args ret -> HandleElt f (args ::> ret)
HandleElt FnHandle args ret
FnHandle args ret
hdl' (f args ret -> HandleElt f (args ::> ret))
-> f args ret -> HandleElt f (args ::> ret)
forall a b. (a -> b) -> a -> b
$ f args ret -> f args ret
f f args ret
f args ret
x)
      MapF (Nonce GlobalNonceGenerator) (HandleElt f)
m

-- | Lookup the function name in the map by a linear scan of all
-- entries.  This will be much slower than using 'lookupHandleMap' to
-- find the function by ID, so the latter should be used if possible.
searchHandleMap :: FunctionName
                -> (TypeRepr (FunctionHandleType args ret))
                -> FnHandleMap f
                -> Maybe (FnHandle args ret, f args ret)
searchHandleMap :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (f :: Ctx CrucibleType -> CrucibleType -> Type).
FunctionName
-> TypeRepr (FunctionHandleType args ret)
-> FnHandleMap f
-> Maybe (FnHandle args ret, f args ret)
searchHandleMap FunctionName
nm TypeRepr (FunctionHandleType args ret)
fnTyRepr (FnHandleMap MapF (Nonce GlobalNonceGenerator) (HandleElt f)
m) =
  let nameMatch :: Some (HandleElt f) -> Bool
nameMatch (Some (HandleElt FnHandle args ret
h f args ret
_)) = FnHandle args ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
handleName FnHandle args ret
h FunctionName -> FunctionName -> Bool
forall a. Eq a => a -> a -> Bool
== FunctionName
nm
  in case (Some (HandleElt f) -> Bool)
-> [Some (HandleElt f)] -> Maybe (Some (HandleElt f))
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
List.find Some (HandleElt f) -> Bool
nameMatch (MapF (Nonce GlobalNonceGenerator) (HandleElt f)
-> [Some (HandleElt f)]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Some a]
MapF.elems MapF (Nonce GlobalNonceGenerator) (HandleElt f)
m) of
    Maybe (Some (HandleElt f))
Nothing -> Maybe (FnHandle args ret, f args ret)
forall a. Maybe a
Nothing
    (Just (Some (HandleElt FnHandle args ret
h f args ret
x))) ->
      case TypeRepr (FunctionHandleType args ret)
-> TypeRepr (FunctionHandleType args ret)
-> Maybe
     (FunctionHandleType args ret :~: FunctionHandleType args ret)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality (FnHandle args ret -> TypeRepr (FunctionHandleType args ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr (FunctionHandleType args ret)
handleType FnHandle args ret
h) TypeRepr (FunctionHandleType args ret)
fnTyRepr of
        Just FunctionHandleType args ret :~: FunctionHandleType args ret
Refl -> (FnHandle args ret, f args ret)
-> Maybe (FnHandle args ret, f args ret)
forall a. a -> Maybe a
Just (FnHandle args ret
FnHandle args ret
h,f args ret
f args ret
x)
        Maybe (FunctionHandleType args ret :~: FunctionHandleType args ret)
Nothing -> Maybe (FnHandle args ret, f args ret)
forall a. Maybe a
Nothing

handleMapToHandles :: FnHandleMap f -> [SomeHandle]
handleMapToHandles :: forall (f :: Ctx CrucibleType -> CrucibleType -> Type).
FnHandleMap f -> [SomeHandle]
handleMapToHandles (FnHandleMap MapF (Nonce GlobalNonceGenerator) (HandleElt f)
m) =
  (Some (HandleElt f) -> SomeHandle)
-> [Some (HandleElt f)] -> [SomeHandle]
forall a b. (a -> b) -> [a] -> [b]
map (\(Some (HandleElt FnHandle args ret
handle f args ret
_)) -> FnHandle args ret -> SomeHandle
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> SomeHandle
SomeHandle FnHandle args ret
handle) (MapF (Nonce GlobalNonceGenerator) (HandleElt f)
-> [Some (HandleElt f)]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Some a]
MapF.elems MapF (Nonce GlobalNonceGenerator) (HandleElt f)
m)