    {-# 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 :: forall t.
    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 a b. (a -> b) -> Maybe a -> Maybe b
    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 a b. IO a -> IO b -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> OptionSetResult -> IO OptionSetResult
    forall a. a -> IO a
    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 a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()

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

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

    cacheOptDesc ::
      NonceGenerator IO t ->
      IORef (ExprAllocator t) ->
      OptionSetting BaseIntegerType ->
      ConfigDesc
    cacheOptDesc :: forall t.
    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 { forall t.
    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)
                      , forall t.
    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 :: forall t. NonceGenerator IO t -> IO (ExprAllocator t)
    newStorage NonceGenerator IO t
    g = do
      ExprAllocator t -> IO (ExprAllocator t)
    forall a. a -> IO a
    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 { 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 :: forall t (tp :: BaseType).
    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
      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
      return $! mkExpr n pc a v

    uncachedNonceExpr :: NonceGenerator IO t
                     -> ProgramLoc
                     -> NonceApp t (Expr t) tp
                     -> AbstractValue tp
                     -> IO (Expr t tp)
    uncachedNonceExpr :: forall t (tp :: BaseType).
    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
      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
      return $! NonceAppExpr $ NonceAppExprCtor { nonceExprId = n
                                              , nonceExprLoc = pc
                                              , nonceExprApp = p
                                              , nonceExprAbsValue = 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 :: 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)
    h ProgramLoc
    pc NonceApp t (Expr t) tp
    p AbstractValue tp
    v = do
      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 me of
        Just Expr t tp
    e -> Expr t tp -> IO (Expr t tp)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Expr t tp
    e
        Maybe (Expr t tp)
    Nothing -> do
          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 = 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 { 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
                                                }
          seq e $ stToIO $ PH.insert h p e
          return 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 :: 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)
    h ProgramLoc
    pc App (Expr t) tp
    a AbstractValue tp
    v = do
      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 me of
        Just Expr t tp
    e -> Expr t tp -> IO (Expr t tp)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Expr t tp
    e
        Maybe (Expr t tp)
    Nothing -> do
          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 = 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
          seq e $ stToIO $ PH.insert h a e
          return e

    -- | Create a storage that does hash consing.
    newCachedStorage :: forall t
                      . NonceGenerator IO t
                     -> Int
                     -> IO (ExprAllocator t)
    newCachedStorage :: forall t. 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
      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
      predCache <- PH.newSized sz
      return $ ExprAllocator { appExpr = cachedAppExpr g appCache
                            , nonceExpr = cachedNonceExpr g predCache
                            }