{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}

{-|
Module      : What4.Expr.Allocator
Description : Expression allocators for controlling hash-consing
Copyright   : (c) Galois Inc, 2015-2022
License     : BSD3
Maintainer  : rdockins@galois.com
-}
module What4.Expr.Allocator
( ExprAllocator(..)
, newStorage
, newCachedStorage

, cacheStartSizeOption
, cacheStartSizeDesc
, cacheTerms
, cacheOptDesc
) where

import           Control.Lens ( (&) )
import           Control.Monad.ST (stToIO)
import           Data.IORef

import qualified Data.Parameterized.HashTable as PH
import           Data.Parameterized.Nonce

import           What4.BaseTypes
import           What4.Concrete
import           What4.Config as CFG
import           What4.Expr.App
import           What4.ProgramLoc
import           What4.Utils.AbstractDomains

------------------------------------------------------------------------
-- Cache start size

-- | Starting size for element cache when caching is enabled.
--   The default value is 100000 elements.
--
--   This option is named \"backend.cache_start_size\"
cacheStartSizeOption :: ConfigOption BaseIntegerType
cacheStartSizeOption :: ConfigOption BaseIntegerType
cacheStartSizeOption = BaseTypeRepr BaseIntegerType
-> String -> ConfigOption BaseIntegerType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseIntegerType
BaseIntegerRepr String
"backend.cache_start_size"

-- | The configuration option for setting the size of the initial hash set
--   used by simple builder (measured in number of elements).
cacheStartSizeDesc :: ConfigDesc
cacheStartSizeDesc :: ConfigDesc
cacheStartSizeDesc = ConfigOption BaseIntegerType
-> OptionStyle BaseIntegerType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseIntegerType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseIntegerType
cacheStartSizeOption OptionStyle BaseIntegerType
sty Maybe (Doc Void)
help (ConcreteVal BaseIntegerType -> Maybe (ConcreteVal BaseIntegerType)
forall a. a -> Maybe a
Just (Integer -> ConcreteVal BaseIntegerType
ConcreteInteger Integer
100000))
  where sty :: OptionStyle BaseIntegerType
sty = Bound Integer -> OptionStyle BaseIntegerType
integerWithMinOptSty (Integer -> Bound Integer
forall r. r -> Bound r
CFG.Inclusive Integer
0)
        help :: Maybe (Doc Void)
help = Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Starting size for element cache"

------------------------------------------------------------------------
-- Cache terms

-- | Indicates if we should cache terms.  When enabled, hash-consing
--   is used to find and deduplicate common subexpressions.
--   Toggling this option from disabled to enabled will allocate a new
--   hash table; toggling it from enabled to disabled will discard
--   the current hash table.  The default value for this option is `False`.
--
--   This option is named \"use_cache\"
cacheTerms :: ConfigOption BaseBoolType
cacheTerms :: ConfigOption BaseBoolType
cacheTerms = BaseTypeRepr BaseBoolType -> String -> ConfigOption BaseBoolType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseBoolType
BaseBoolRepr String
"use_cache"

cacheOptStyle ::
  NonceGenerator IO t ->
  IORef (ExprAllocator t) ->
  OptionSetting BaseIntegerType ->
  OptionStyle BaseBoolType
cacheOptStyle :: NonceGenerator IO t
-> IORef (ExprAllocator t)
-> OptionSetting BaseIntegerType
-> OptionStyle BaseBoolType
cacheOptStyle NonceGenerator IO t
gen IORef (ExprAllocator t)
storageRef OptionSetting BaseIntegerType
szSetting =
  OptionStyle BaseBoolType
boolOptSty OptionStyle BaseBoolType
-> (OptionStyle BaseBoolType -> OptionStyle BaseBoolType)
-> OptionStyle BaseBoolType
forall a b. a -> (a -> b) -> b
& (Maybe (ConcreteVal BaseBoolType)
 -> ConcreteVal BaseBoolType -> IO OptionSetResult)
-> OptionStyle BaseBoolType -> OptionStyle BaseBoolType
forall (tp :: BaseType).
(Maybe (ConcreteVal tp) -> ConcreteVal tp -> IO OptionSetResult)
-> OptionStyle tp -> OptionStyle tp
set_opt_onset
        (\Maybe (ConcreteVal BaseBoolType)
mb ConcreteVal BaseBoolType
b -> Maybe Bool -> Bool -> IO ()
f ((ConcreteVal BaseBoolType -> Bool)
-> Maybe (ConcreteVal BaseBoolType) -> Maybe Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ConcreteVal BaseBoolType -> Bool
fromConcreteBool Maybe (ConcreteVal BaseBoolType)
mb) (ConcreteVal BaseBoolType -> Bool
fromConcreteBool ConcreteVal BaseBoolType
b) IO () -> IO OptionSetResult -> IO OptionSetResult
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> OptionSetResult -> IO OptionSetResult
forall (m :: Type -> Type) a. Monad m => a -> m a
return OptionSetResult
optOK)
 where
 f :: Maybe Bool -> Bool -> IO ()
 f :: Maybe Bool -> Bool -> IO ()
f Maybe Bool
mb Bool
b | Maybe Bool
mb Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b = if Bool
b then IO ()
start else IO ()
stop
        | Bool
otherwise = () -> IO ()
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

 stop :: IO ()
stop  = do ExprAllocator t
s <- NonceGenerator IO t -> IO (ExprAllocator t)
forall t. NonceGenerator IO t -> IO (ExprAllocator t)
newStorage NonceGenerator IO t
gen
            IORef (ExprAllocator t) -> ExprAllocator t -> IO ()
forall a. IORef a -> a -> IO ()
atomicWriteIORef IORef (ExprAllocator t)
storageRef ExprAllocator t
s

 start :: IO ()
start = do Integer
sz <- OptionSetting BaseIntegerType -> IO Integer
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt OptionSetting BaseIntegerType
szSetting
            ExprAllocator t
s <- NonceGenerator IO t -> Int -> IO (ExprAllocator t)
forall t. NonceGenerator IO t -> Int -> IO (ExprAllocator t)
newCachedStorage NonceGenerator IO t
gen (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
sz)
            IORef (ExprAllocator t) -> ExprAllocator t -> IO ()
forall a. IORef a -> a -> IO ()
atomicWriteIORef IORef (ExprAllocator t)
storageRef ExprAllocator t
s

cacheOptDesc ::
  NonceGenerator IO t ->
  IORef (ExprAllocator t) ->
  OptionSetting BaseIntegerType ->
  ConfigDesc
cacheOptDesc :: NonceGenerator IO t
-> IORef (ExprAllocator t)
-> OptionSetting BaseIntegerType
-> ConfigDesc
cacheOptDesc NonceGenerator IO t
gen IORef (ExprAllocator t)
storageRef OptionSetting BaseIntegerType
szSetting =
  ConfigOption BaseBoolType
-> OptionStyle BaseBoolType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseBoolType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt
    ConfigOption BaseBoolType
cacheTerms
    (NonceGenerator IO t
-> IORef (ExprAllocator t)
-> OptionSetting BaseIntegerType
-> OptionStyle BaseBoolType
forall t.
NonceGenerator IO t
-> IORef (ExprAllocator t)
-> OptionSetting BaseIntegerType
-> OptionStyle BaseBoolType
cacheOptStyle NonceGenerator IO t
gen IORef (ExprAllocator t)
storageRef OptionSetting BaseIntegerType
szSetting)
    (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Use hash-consing during term construction")
    (ConcreteVal BaseBoolType -> Maybe (ConcreteVal BaseBoolType)
forall a. a -> Maybe a
Just (Bool -> ConcreteVal BaseBoolType
ConcreteBool Bool
False))


------------------------------------------------------------------------
-- | ExprAllocator provides an interface for creating expressions from
-- an applications.
-- Parameter @t@ is a phantom type brand used to track nonces.
data ExprAllocator t
   = ExprAllocator { ExprAllocator t
-> forall (tp :: BaseType).
   ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
appExpr  :: forall tp
                            .  ProgramLoc
                            -> App (Expr t) tp
                            -> AbstractValue tp
                            -> IO (Expr t tp)
                  , ExprAllocator t
-> forall (tp :: BaseType).
   ProgramLoc
   -> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
nonceExpr :: forall tp
                             .  ProgramLoc
                             -> NonceApp t (Expr t) tp
                             -> AbstractValue tp
                             -> IO (Expr t tp)
                  }


------------------------------------------------------------------------
-- Uncached storage

-- | Create a new storage that does not do hash consing.
newStorage :: NonceGenerator IO t -> IO (ExprAllocator t)
newStorage :: NonceGenerator IO t -> IO (ExprAllocator t)
newStorage NonceGenerator IO t
g = do
  ExprAllocator t -> IO (ExprAllocator t)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExprAllocator t -> IO (ExprAllocator t))
-> ExprAllocator t -> IO (ExprAllocator t)
forall a b. (a -> b) -> a -> b
$! ExprAllocator :: forall t.
(forall (tp :: BaseType).
 ProgramLoc
 -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp))
-> (forall (tp :: BaseType).
    ProgramLoc
    -> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp))
-> ExprAllocator t
ExprAllocator { appExpr :: forall (tp :: BaseType).
ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
appExpr = NonceGenerator IO t
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
forall t (tp :: BaseType).
NonceGenerator IO t
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
uncachedExprFn NonceGenerator IO t
g
                         , nonceExpr :: forall (tp :: BaseType).
ProgramLoc
-> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
nonceExpr = NonceGenerator IO t
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
forall t (tp :: BaseType).
NonceGenerator IO t
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
uncachedNonceExpr NonceGenerator IO t
g
                         }

uncachedExprFn :: NonceGenerator IO t
              -> ProgramLoc
              -> App (Expr t) tp
              -> AbstractValue tp
              -> IO (Expr t tp)
uncachedExprFn :: NonceGenerator IO t
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
uncachedExprFn NonceGenerator IO t
g ProgramLoc
pc App (Expr t) tp
a AbstractValue tp
v = do
  Nonce t tp
n <- NonceGenerator IO t -> IO (Nonce t tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO t
g
  Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Expr t tp -> IO (Expr t tp)) -> Expr t tp -> IO (Expr t tp)
forall a b. (a -> b) -> a -> b
$! Nonce t tp
-> ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> Expr t tp
forall t (tp :: BaseType).
Nonce t tp
-> ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> Expr t tp
mkExpr Nonce t tp
n ProgramLoc
pc App (Expr t) tp
a AbstractValue tp
v

uncachedNonceExpr :: NonceGenerator IO t
                 -> ProgramLoc
                 -> NonceApp t (Expr t) tp
                 -> AbstractValue tp
                 -> IO (Expr t tp)
uncachedNonceExpr :: NonceGenerator IO t
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
uncachedNonceExpr NonceGenerator IO t
g ProgramLoc
pc NonceApp t (Expr t) tp
p AbstractValue tp
v = do
  Nonce t tp
n <- NonceGenerator IO t -> IO (Nonce t tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO t
g
  Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Expr t tp -> IO (Expr t tp)) -> Expr t tp -> IO (Expr t tp)
forall a b. (a -> b) -> a -> b
$! NonceAppExpr t tp -> Expr t tp
forall t (tp :: BaseType). NonceAppExpr t tp -> Expr t tp
NonceAppExpr (NonceAppExpr t tp -> Expr t tp) -> NonceAppExpr t tp -> Expr t tp
forall a b. (a -> b) -> a -> b
$ NonceAppExprCtor :: forall t (tp :: BaseType).
Nonce t tp
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> NonceAppExpr t tp
NonceAppExprCtor { nonceExprId :: Nonce t tp
nonceExprId = Nonce t tp
n
                                          , nonceExprLoc :: ProgramLoc
nonceExprLoc = ProgramLoc
pc
                                          , nonceExprApp :: NonceApp t (Expr t) tp
nonceExprApp = NonceApp t (Expr t) tp
p
                                          , nonceExprAbsValue :: AbstractValue tp
nonceExprAbsValue = AbstractValue tp
v
                                          }

------------------------------------------------------------------------
-- Cached storage

cachedNonceExpr :: NonceGenerator IO t
               -> PH.HashTable PH.RealWorld (NonceApp t (Expr t)) (Expr t)
               -> ProgramLoc
               -> NonceApp t (Expr t) tp
               -> AbstractValue tp
               -> IO (Expr t tp)
cachedNonceExpr :: NonceGenerator IO t
-> HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
cachedNonceExpr NonceGenerator IO t
g HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
h ProgramLoc
pc NonceApp t (Expr t) tp
p AbstractValue tp
v = do
  Maybe (Expr t tp)
me <- ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp))
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp)))
-> ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp))
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
-> NonceApp t (Expr t) tp -> ST RealWorld (Maybe (Expr t tp))
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> ST s (Maybe (val tp))
PH.lookup HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
h NonceApp t (Expr t) tp
p
  case Maybe (Expr t tp)
me of
    Just Expr t tp
e -> Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
e
    Maybe (Expr t tp)
Nothing -> do
      Nonce t tp
n <- NonceGenerator IO t -> IO (Nonce t tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO t
g
      let e :: Expr t tp
e = NonceAppExpr t tp -> Expr t tp
forall t (tp :: BaseType). NonceAppExpr t tp -> Expr t tp
NonceAppExpr (NonceAppExpr t tp -> Expr t tp) -> NonceAppExpr t tp -> Expr t tp
forall a b. (a -> b) -> a -> b
$ NonceAppExprCtor :: forall t (tp :: BaseType).
Nonce t tp
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> NonceAppExpr t tp
NonceAppExprCtor { nonceExprId :: Nonce t tp
nonceExprId = Nonce t tp
n
                                            , nonceExprLoc :: ProgramLoc
nonceExprLoc = ProgramLoc
pc
                                            , nonceExprApp :: NonceApp t (Expr t) tp
nonceExprApp = NonceApp t (Expr t) tp
p
                                            , nonceExprAbsValue :: AbstractValue tp
nonceExprAbsValue = AbstractValue tp
v
                                            }
      Expr t tp -> IO () -> IO ()
seq Expr t tp
e (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ ST RealWorld () -> IO ()
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld () -> IO ()) -> ST RealWorld () -> IO ()
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
-> NonceApp t (Expr t) tp -> Expr t tp -> ST RealWorld ()
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> val tp -> ST s ()
PH.insert HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
h NonceApp t (Expr t) tp
p Expr t tp
e
      Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
e


cachedAppExpr :: forall t tp
               . NonceGenerator IO t
              -> PH.HashTable PH.RealWorld (App (Expr t)) (Expr t)
              -> ProgramLoc
              -> App (Expr t) tp
              -> AbstractValue tp
              -> IO (Expr t tp)
cachedAppExpr :: NonceGenerator IO t
-> HashTable RealWorld (App (Expr t)) (Expr t)
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
cachedAppExpr NonceGenerator IO t
g HashTable RealWorld (App (Expr t)) (Expr t)
h ProgramLoc
pc App (Expr t) tp
a AbstractValue tp
v = do
  Maybe (Expr t tp)
me <- ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp))
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp)))
-> ST RealWorld (Maybe (Expr t tp)) -> IO (Maybe (Expr t tp))
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld (App (Expr t)) (Expr t)
-> App (Expr t) tp -> ST RealWorld (Maybe (Expr t tp))
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> ST s (Maybe (val tp))
PH.lookup HashTable RealWorld (App (Expr t)) (Expr t)
h App (Expr t) tp
a
  case Maybe (Expr t tp)
me of
    Just Expr t tp
e -> Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
e
    Maybe (Expr t tp)
Nothing -> do
      Nonce t tp
n <- NonceGenerator IO t -> IO (Nonce t tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO t
g
      let e :: Expr t tp
e = Nonce t tp
-> ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> Expr t tp
forall t (tp :: BaseType).
Nonce t tp
-> ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> Expr t tp
mkExpr Nonce t tp
n ProgramLoc
pc App (Expr t) tp
a AbstractValue tp
v
      Expr t tp -> IO () -> IO ()
seq Expr t tp
e (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ ST RealWorld () -> IO ()
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld () -> IO ()) -> ST RealWorld () -> IO ()
forall a b. (a -> b) -> a -> b
$ HashTable RealWorld (App (Expr t)) (Expr t)
-> App (Expr t) tp -> Expr t tp -> ST RealWorld ()
forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> val tp -> ST s ()
PH.insert HashTable RealWorld (App (Expr t)) (Expr t)
h App (Expr t) tp
a Expr t tp
e
      Expr t tp -> IO (Expr t tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
e

-- | Create a storage that does hash consing.
newCachedStorage :: forall t
                  . NonceGenerator IO t
                 -> Int
                 -> IO (ExprAllocator t)
newCachedStorage :: NonceGenerator IO t -> Int -> IO (ExprAllocator t)
newCachedStorage NonceGenerator IO t
g Int
sz = ST RealWorld (ExprAllocator t) -> IO (ExprAllocator t)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (ExprAllocator t) -> IO (ExprAllocator t))
-> ST RealWorld (ExprAllocator t) -> IO (ExprAllocator t)
forall a b. (a -> b) -> a -> b
$ do
  HashTable RealWorld (App (Expr t)) (Expr t)
appCache  <- Int -> ST RealWorld (HashTable RealWorld (App (Expr t)) (Expr t))
forall k1 s (k2 :: k1 -> Type) (v :: k1 -> Type).
Int -> ST s (HashTable s k2 v)
PH.newSized Int
sz
  HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
predCache <- Int
-> ST
     RealWorld (HashTable RealWorld (NonceApp t (Expr t)) (Expr t))
forall k1 s (k2 :: k1 -> Type) (v :: k1 -> Type).
Int -> ST s (HashTable s k2 v)
PH.newSized Int
sz
  ExprAllocator t -> ST RealWorld (ExprAllocator t)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExprAllocator t -> ST RealWorld (ExprAllocator t))
-> ExprAllocator t -> ST RealWorld (ExprAllocator t)
forall a b. (a -> b) -> a -> b
$ ExprAllocator :: forall t.
(forall (tp :: BaseType).
 ProgramLoc
 -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp))
-> (forall (tp :: BaseType).
    ProgramLoc
    -> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp))
-> ExprAllocator t
ExprAllocator { appExpr :: forall (tp :: BaseType).
ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
appExpr = NonceGenerator IO t
-> HashTable RealWorld (App (Expr t)) (Expr t)
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
forall t (tp :: BaseType).
NonceGenerator IO t
-> HashTable RealWorld (App (Expr t)) (Expr t)
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
cachedAppExpr NonceGenerator IO t
g HashTable RealWorld (App (Expr t)) (Expr t)
appCache
                        , nonceExpr :: forall (tp :: BaseType).
ProgramLoc
-> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
nonceExpr = NonceGenerator IO t
-> HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
forall t (tp :: BaseType).
NonceGenerator IO t
-> HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
cachedNonceExpr NonceGenerator IO t
g HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
predCache
                        }