    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE PatternSynonyms #-}

    module What4.Serialize.Printer
      (
        serializeExpr
      , serializeExprWithConfig
      , serializeSymFn
      , serializeSymFnWithConfig
      , serializeBaseType
      , convertBaseTypes
      , Config(..)
      , Result(..)
      , printSExpr
      , defaultConfig
      , SExpr
      , Atom(..)
      , SomeExprSymFn(..)
      , S.WellFormedSExpr(..)
      , ident, int, string
      , bitvec, bool, nat, real
      , ppFreeVarEnv
      , ppFreeSymFnEnv
      , pattern S.L
      , pattern S.A
      ) where

    import           Numeric.Natural
    import qualified Data.Foldable as F
    import           Data.Set ( Set )
    import qualified Data.Set as Set
    import           Data.Map.Ordered (OMap)
    import qualified Data.Map.Ordered as OMap
    import qualified Data.BitVector.Sized as BV
    import           Data.Parameterized.Some
    import qualified Data.Parameterized.Context as Ctx
    import qualified Data.Parameterized.NatRepr as NR
    import qualified Data.Parameterized.Nonce as Nonce
    import qualified Data.Parameterized.TraversableFC as FC

    import           Data.Text (Text)
    import qualified Data.Text as T
    import qualified Data.Text.Encoding as T
    import           Data.Word ( Word64 )
    import qualified Control.Monad as M
    import           Control.Monad.State.Strict (State)
    import qualified Control.Monad.State.Strict as MS

    import qualified Data.SCargot.Repr.WellFormed as S

    import           What4.BaseTypes
    import qualified What4.Expr as W4
    import qualified What4.Expr.ArrayUpdateMap as WAU
    import qualified What4.Expr.BoolMap as BooM
    import qualified What4.Expr.Builder as W4
    import qualified What4.Expr.WeightedSum as WSum
    import qualified What4.IndexLit as WIL
    import qualified What4.Interface as W4
    import qualified What4.Symbol as W4
    import qualified What4.Utils.StringLiteral as W4S

    import           What4.Serialize.SETokens ( Atom(..), printSExpr
                                              , ident, int, nat, string
                                              , bitvec, bool, real, float
                                              )

    type SExpr = S.WellFormedSExpr Atom

    data SomeExprSymFn t = forall dom ret. SomeExprSymFn (W4.ExprSymFn t dom ret)

    instance Eq (SomeExprSymFn t) where
      (SomeExprSymFn ExprSymFn t dom ret
    fn1) == :: SomeExprSymFn t -> SomeExprSymFn t -> Bool
    == (SomeExprSymFn ExprSymFn t dom ret
    fn2) =
        case Nonce t (dom ::> ret)
    -> Nonce t (dom ::> ret) -> Maybe ((dom ::> ret) :~: (dom ::> ret))
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: Ctx BaseType) (b :: Ctx BaseType).
    Nonce t a -> Nonce t b -> Maybe (a :~: b)
    W4.testEquality (ExprSymFn t dom ret -> Nonce t (dom ::> ret)
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> Nonce t (args ::> ret)
    W4.symFnId ExprSymFn t dom ret
    fn1) (ExprSymFn t dom ret -> Nonce t (dom ::> ret)
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> Nonce t (args ::> ret)
    W4.symFnId ExprSymFn t dom ret
    fn2) of
          Just (dom ::> ret) :~: (dom ::> ret)
    _ -> Bool
    True
          Maybe ((dom ::> ret) :~: (dom ::> ret))
    _ -> Bool
    False

    instance Ord (SomeExprSymFn t) where
      compare :: SomeExprSymFn t -> SomeExprSymFn t -> Ordering
    compare (SomeExprSymFn ExprSymFn t dom ret
    fn1) (SomeExprSymFn ExprSymFn t dom ret
    fn2) =
        Word64 -> Word64 -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Nonce t (dom ::> ret) -> Word64
    forall k s (tp :: k). Nonce s tp -> Word64
    Nonce.indexValue (Nonce t (dom ::> ret) -> Word64)
    -> Nonce t (dom ::> ret) -> Word64
    forall a b. (a -> b) -> a -> b
    $ ExprSymFn t dom ret -> Nonce t (dom ::> ret)
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> Nonce t (args ::> ret)
    W4.symFnId ExprSymFn t dom ret
    fn1) (Nonce t (dom ::> ret) -> Word64
    forall k s (tp :: k). Nonce s tp -> Word64
    Nonce.indexValue (Nonce t (dom ::> ret) -> Word64)
    -> Nonce t (dom ::> ret) -> Word64
    forall a b. (a -> b) -> a -> b
    $ ExprSymFn t dom ret -> Nonce t (dom ::> ret)
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> Nonce t (args ::> ret)
    W4.symFnId ExprSymFn t dom ret
    fn2)

    instance Show (SomeExprSymFn t) where
      show :: SomeExprSymFn t -> String
    show (SomeExprSymFn ExprSymFn t dom ret
    f) = ExprSymFn t dom ret -> String
    forall a. Show a => a -> String
    show ExprSymFn t dom ret
    f

    type VarNameEnv t = OMap (Some (W4.ExprBoundVar t)) Text
    type FnNameEnv t  = OMap (SomeExprSymFn t) Text

    ppFreeVarEnv :: VarNameEnv t -> String
    ppFreeVarEnv :: forall t. VarNameEnv t -> String
    ppFreeVarEnv VarNameEnv t
    env = [(String, String, String)] -> String
    forall a. Show a => a -> String
    show ([(String, String, String)] -> String)
    -> [(String, String, String)] -> String
    forall a b. (a -> b) -> a -> b
    $ ((Some (ExprBoundVar t), Text) -> (String, String, String))
    -> [(Some (ExprBoundVar t), Text)] -> [(String, String, String)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Some (ExprBoundVar t), Text) -> (String, String, String)
    forall t. (Some (ExprBoundVar t), Text) -> (String, String, String)
    toStr [(Some (ExprBoundVar t), Text)]
    entries
      where entries :: [(Some (ExprBoundVar t), Text)]
    entries = VarNameEnv t -> [(Some (ExprBoundVar t), Text)]
    forall k v. OMap k v -> [(k, v)]
    OMap.toAscList VarNameEnv t
    env
            toStr :: ((Some (W4.ExprBoundVar t)), Text) -> (String, String, String)
            toStr :: forall t. (Some (ExprBoundVar t), Text) -> (String, String, String)
    toStr ((Some ExprBoundVar t x
    var), Text
    newName) = ( Text -> String
    T.unpack (Text -> String) -> Text -> String
    forall a b. (a -> b) -> a -> b
    $ SolverSymbol -> Text
    W4.solverSymbolAsText (SolverSymbol -> Text) -> SolverSymbol -> Text
    forall a b. (a -> b) -> a -> b
    $ ExprBoundVar t x -> SolverSymbol
    forall t (tp :: BaseType). ExprBoundVar t tp -> SolverSymbol
    W4.bvarName ExprBoundVar t x
    var
                                          , BaseTypeRepr x -> String
    forall a. Show a => a -> String
    show (BaseTypeRepr x -> String) -> BaseTypeRepr x -> String
    forall a b. (a -> b) -> a -> b
    $ ExprBoundVar t x -> BaseTypeRepr x
    forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
    W4.bvarType ExprBoundVar t x
    var
                                          , Text -> String
    T.unpack Text
    newName
                                          )

    ppFreeSymFnEnv :: FnNameEnv t -> String
    ppFreeSymFnEnv :: forall t. FnNameEnv t -> String
    ppFreeSymFnEnv FnNameEnv t
    env = [(String, String, String)] -> String
    forall a. Show a => a -> String
    show ([(String, String, String)] -> String)
    -> [(String, String, String)] -> String
    forall a b. (a -> b) -> a -> b
    $ ((SomeExprSymFn t, Text) -> (String, String, String))
    -> [(SomeExprSymFn t, Text)] -> [(String, String, String)]
    forall a b. (a -> b) -> [a] -> [b]
    map (SomeExprSymFn t, Text) -> (String, String, String)
    forall t. (SomeExprSymFn t, Text) -> (String, String, String)
    toStr [(SomeExprSymFn t, Text)]
    entries
      where entries :: [(SomeExprSymFn t, Text)]
    entries = FnNameEnv t -> [(SomeExprSymFn t, Text)]
    forall k v. OMap k v -> [(k, v)]
    OMap.toAscList FnNameEnv t
    env
            toStr :: ((SomeExprSymFn t), Text) -> (String, String, String)
            toStr :: forall t. (SomeExprSymFn t, Text) -> (String, String, String)
    toStr ((SomeExprSymFn ExprSymFn t dom ret
    fn), Text
    newName) = ( Text -> String
    T.unpack (Text -> String) -> Text -> String
    forall a b. (a -> b) -> a -> b
    $ SolverSymbol -> Text
    W4.solverSymbolAsText (SolverSymbol -> Text) -> SolverSymbol -> Text
    forall a b. (a -> b) -> a -> b
    $ ExprSymFn t dom ret -> SolverSymbol
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> SolverSymbol
    W4.symFnName ExprSymFn t dom ret
    fn
                                                  , Assignment BaseTypeRepr dom -> String
    forall a. Show a => a -> String
    show (Assignment BaseTypeRepr dom -> String)
    -> Assignment BaseTypeRepr dom -> String
    forall a b. (a -> b) -> a -> b
    $ ExprSymFn t dom ret -> Assignment BaseTypeRepr dom
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> Assignment BaseTypeRepr args
    W4.symFnArgTypes ExprSymFn t dom ret
    fn
                                                  , Text -> String
    T.unpack Text
    newName
                                                  )

    -- | Controls how expressions and functions are serialized.
    data Config =
      Config
      { Config -> Bool
    cfgAllowFreeVars :: Bool
      -- ^ When @True@, any free What4 @ExprBoundVar@
      -- encountered is simply serialized with a unique name,
      -- and the mapping from What4 ExprBoundVar to unique names
      -- is returned after serialization. When False, an error
      -- is raised when a "free" @ExprBoundVar@ is encountered.
      , Config -> Bool
    cfgAllowFreeSymFns :: Bool
      -- ^ When @True@, any encountered What4 @ExprSymFn@ during
      -- serialization is simply assigned a unique name and the
      -- mapping from What4 ExprSymFn to unique name is returned
      -- after serialization. When @False, encountered
      -- ExprSymFns are serialized at the top level of the
      -- expression in a `(letfn ([f ...]) ...)`.
      }

    data Result t =
      Result
      { forall t. Result t -> WellFormedSExpr Atom
    resSExpr :: S.WellFormedSExpr Atom
      -- ^ The serialized term.
      , forall t. Result t -> VarNameEnv t
    resFreeVarEnv :: VarNameEnv t
      -- ^ The free BoundVars that were encountered during
      -- serialization and their associated fresh name
      -- that was used to generate the s-expression.
      , forall t. Result t -> FnNameEnv t
    resSymFnEnv :: FnNameEnv t
      -- ^ The SymFns that were encountered during serialization
      -- and their associated fresh name that was used to
      -- generate the s-expression.
      }

    defaultConfig :: Config
    defaultConfig :: Config
    defaultConfig = Config { cfgAllowFreeVars :: Bool
    cfgAllowFreeVars = Bool
    False, cfgAllowFreeSymFns :: Bool
    cfgAllowFreeSymFns = Bool
    False}

    -- This file is organized top-down, i.e., from high-level to low-level.

    -- | Serialize a What4 Expr as a well-formed s-expression
    -- (i.e., one which contains no improper lists). Equivalent
    -- to @(resSExpr (serializeExpr' defaultConfig))@. Sharing
    -- in the AST is achieved via a top-level let-binding around
    -- the emitted expression (unless there are no terms with
    -- non-atomic terms which can be shared).
    serializeExpr :: W4.Expr t tp -> SExpr
    serializeExpr :: forall t (tp :: BaseType). Expr t tp -> WellFormedSExpr Atom
    serializeExpr = Result t -> WellFormedSExpr Atom
    forall t. Result t -> WellFormedSExpr Atom
    resSExpr (Result t -> WellFormedSExpr Atom)
    -> (Expr t tp -> Result t) -> Expr t tp -> WellFormedSExpr Atom
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Config -> Expr t tp -> Result t
    forall t (tp :: BaseType). Config -> Expr t tp -> Result t
    serializeExprWithConfig Config
    defaultConfig)

    -- | Serialize a What4 Expr as a well-formed s-expression
    -- (i.e., one which contains no improper lists) according to
    -- the configuration. Sharing in the AST is achieved via a
    -- top-level let-binding around the emitted expression
    -- (unless there are no terms with non-atomic terms which
    -- can be shared).
    serializeExprWithConfig :: Config -> W4.Expr t tp -> Result t
    serializeExprWithConfig :: forall t (tp :: BaseType). Config -> Expr t tp -> Result t
    serializeExprWithConfig Config
    cfg Expr t tp
    expr = Config -> Memo t (WellFormedSExpr Atom) -> Result t
    forall t. Config -> Memo t (WellFormedSExpr Atom) -> Result t
    serializeSomething Config
    cfg (Expr t tp -> Memo t (WellFormedSExpr Atom)
    forall t (tp :: BaseType).
    Expr t tp -> Memo t (WellFormedSExpr Atom)
    convertExprWithLet Expr t tp
    expr)

    -- | Serialize a What4 ExprSymFn as a well-formed
    -- s-expression (i.e., one which contains no improper
    -- lists). Equivalent to @(resSExpr (serializeSymFn'
    -- defaultConfig))@. Sharing in the AST is achieved via a
    -- top-level let-binding around the emitted expression
    -- (unless there are no terms with non-atomic terms which
    -- can be shared).
    serializeSymFn :: W4.ExprSymFn t dom ret -> SExpr
    serializeSymFn :: forall t (dom :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t dom ret -> WellFormedSExpr Atom
    serializeSymFn = Result t -> WellFormedSExpr Atom
    forall t. Result t -> WellFormedSExpr Atom
    resSExpr (Result t -> WellFormedSExpr Atom)
    -> (ExprSymFn t dom ret -> Result t)
    -> ExprSymFn t dom ret
    -> WellFormedSExpr Atom
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Config -> ExprSymFn t dom ret -> Result t
    forall t (dom :: Ctx BaseType) (ret :: BaseType).
    Config -> ExprSymFn t dom ret -> Result t
    serializeSymFnWithConfig Config
    defaultConfig)

    -- | Serialize a What4 ExprSymFn as a well-formed
    -- s-expression (i.e., one which contains no improper lists)
    -- according to the configuration. Sharing in the AST is
    -- achieved via a top-level let-binding around the emitted
    -- expression (unless there are no terms with non-atomic
    -- terms which can be shared).
    serializeSymFnWithConfig :: Config -> W4.ExprSymFn t dom ret -> Result t
    serializeSymFnWithConfig :: forall t (dom :: Ctx BaseType) (ret :: BaseType).
    Config -> ExprSymFn t dom ret -> Result t
    serializeSymFnWithConfig Config
    cfg ExprSymFn t dom ret
    fn = Config -> Memo t (WellFormedSExpr Atom) -> Result t
    forall t. Config -> Memo t (WellFormedSExpr Atom) -> Result t
    serializeSomething Config
    cfg (ExprSymFn t dom ret -> Memo t (WellFormedSExpr Atom)
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> Memo t (WellFormedSExpr Atom)
    convertSymFn ExprSymFn t dom ret
    fn)

    -- | Run the given Memo computation to produce a well-formed
    -- s-expression (i.e., one which contains no improper lists)
    -- according to the configuration. Sharing in the AST is
    -- achieved via a top-level let-binding around the emitted
    -- expression (unless there are no terms with non-atomic
    -- terms which can be shared).
    serializeSomething :: Config -> Memo t SExpr -> Result t
    serializeSomething :: forall t. Config -> Memo t (WellFormedSExpr Atom) -> Result t
    serializeSomething Config
    cfg Memo t (WellFormedSExpr Atom)
    something =
      let (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    maybeLetFn, MemoEnv t -> FnNameEnv t
    getFreeSymFnEnv) = if Config -> Bool
    cfgAllowFreeSymFns Config
    cfg
                                          then (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return, MemoEnv t -> FnNameEnv t
    forall t. MemoEnv t -> FnNameEnv t
    envFreeSymFnEnv)
                                          else (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall t. WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    letFn, \MemoEnv t
    _ -> FnNameEnv t
    forall k v. OMap k v
    OMap.empty)
          (WellFormedSExpr Atom
    sexpr, MemoEnv t
    menv) = Config
    -> Memo t (WellFormedSExpr Atom)
    -> (WellFormedSExpr Atom, MemoEnv t)
    forall t a. Config -> Memo t a -> (a, MemoEnv t)
    runMemo Config
    cfg (Memo t (WellFormedSExpr Atom)
     -> (WellFormedSExpr Atom, MemoEnv t))
    -> Memo t (WellFormedSExpr Atom)
    -> (WellFormedSExpr Atom, MemoEnv t)
    forall a b. (a -> b) -> a -> b
    $ Memo t (WellFormedSExpr Atom)
    something Memo t (WellFormedSExpr Atom)
    -> (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> Memo t (WellFormedSExpr Atom)
    forall a b.
    StateT (MemoEnv t) Identity a
    -> (a -> StateT (MemoEnv t) Identity b)
    -> StateT (MemoEnv t) Identity b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    maybeLetFn
          letBindings :: [WellFormedSExpr Atom]
    letBindings = ((Text, WellFormedSExpr Atom) -> WellFormedSExpr Atom)
    -> [(Text, WellFormedSExpr Atom)] -> [WellFormedSExpr Atom]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Text
    varName, WellFormedSExpr Atom
    boundExpr) -> [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [ Text -> WellFormedSExpr Atom
    ident Text
    varName, WellFormedSExpr Atom
    boundExpr ])
                        ([(Text, WellFormedSExpr Atom)] -> [WellFormedSExpr Atom])
    -> [(Text, WellFormedSExpr Atom)] -> [WellFormedSExpr Atom]
    forall a b. (a -> b) -> a -> b
    $ ((SKey, (Text, WellFormedSExpr Atom))
     -> (Text, WellFormedSExpr Atom))
    -> [(SKey, (Text, WellFormedSExpr Atom))]
    -> [(Text, WellFormedSExpr Atom)]
    forall a b. (a -> b) -> [a] -> [b]
    map (SKey, (Text, WellFormedSExpr Atom))
    -> (Text, WellFormedSExpr Atom)
    forall a b. (a, b) -> b
    snd
                        ([(SKey, (Text, WellFormedSExpr Atom))]
     -> [(Text, WellFormedSExpr Atom)])
    -> [(SKey, (Text, WellFormedSExpr Atom))]
    -> [(Text, WellFormedSExpr Atom)]
    forall a b. (a -> b) -> a -> b
    $ OMap SKey (Text, WellFormedSExpr Atom)
    -> [(SKey, (Text, WellFormedSExpr Atom))]
    forall k v. OMap k v -> [(k, v)]
    OMap.assocs
                        (OMap SKey (Text, WellFormedSExpr Atom)
     -> [(SKey, (Text, WellFormedSExpr Atom))])
    -> OMap SKey (Text, WellFormedSExpr Atom)
    -> [(SKey, (Text, WellFormedSExpr Atom))]
    forall a b. (a -> b) -> a -> b
    $ MemoEnv t -> OMap SKey (Text, WellFormedSExpr Atom)
    forall t. MemoEnv t -> OMap SKey (Text, WellFormedSExpr Atom)
    envLetBindings MemoEnv t
    menv
          res :: WellFormedSExpr Atom
    res = [WellFormedSExpr Atom]
    -> WellFormedSExpr Atom -> WellFormedSExpr Atom
    mkLet [WellFormedSExpr Atom]
    letBindings WellFormedSExpr Atom
    sexpr
        in Result { resSExpr :: WellFormedSExpr Atom
    resSExpr = WellFormedSExpr Atom
    res
                  , resFreeVarEnv :: VarNameEnv t
    resFreeVarEnv = MemoEnv t -> VarNameEnv t
    forall t. MemoEnv t -> VarNameEnv t
    envFreeVarEnv MemoEnv t
    menv
                  , resSymFnEnv :: FnNameEnv t
    resSymFnEnv = MemoEnv t -> FnNameEnv t
    getFreeSymFnEnv MemoEnv t
    menv
                  }

    serializeBaseType :: BaseTypeRepr tp -> SExpr
    serializeBaseType :: forall (tp :: BaseType). BaseTypeRepr tp -> WellFormedSExpr Atom
    serializeBaseType BaseTypeRepr tp
    bt = BaseTypeRepr tp -> WellFormedSExpr Atom
    forall (tp :: BaseType). BaseTypeRepr tp -> WellFormedSExpr Atom
    convertBaseType BaseTypeRepr tp
    bt

    data MemoEnv t =
      MemoEnv
      { forall t. MemoEnv t -> Config
    envConfig :: !Config
      -- ^ User provided configuration for serialization.
      , forall t. MemoEnv t -> Natural
    envIdCounter :: !Natural
      -- ^ Internal counter for generating fresh names
      , forall t. MemoEnv t -> OMap SKey (Text, WellFormedSExpr Atom)
    envLetBindings :: !(OMap SKey (Text, SExpr))
      -- ^ Mapping from What4 expression nonces to the
      -- corresponding let-variable name (the @fst@) and the
      -- corresponding bound term (the @snd@).
      , forall t. MemoEnv t -> VarNameEnv t
    envFreeVarEnv :: !(VarNameEnv t)
      -- ^ Mapping from What4 ExprBoundVar to the fresh names
      -- assigned to them for serialization purposes.
      , forall t. MemoEnv t -> FnNameEnv t
    envFreeSymFnEnv :: !(FnNameEnv t)
      -- ^ Mapping from What4 ExprSymFn to the fresh names
      -- assigned to them for serialization purposes.
      , forall t. MemoEnv t -> Set (Some (ExprBoundVar t))
    envBoundVars :: Set (Some (W4.ExprBoundVar t))
      -- ^ Set of currently in-scope What4 ExprBoundVars (i.e.,
      -- ExprBoundVars for whom we are serializing the body of
      -- their binding form).
      }

    initEnv :: forall t . Config -> MemoEnv t
    initEnv :: forall t. Config -> MemoEnv t
    initEnv Config
    cfg = MemoEnv { envConfig :: Config
    envConfig = Config
    cfg
                          , envIdCounter :: Natural
    envIdCounter = Natural
    0
                          , envLetBindings :: OMap SKey (Text, WellFormedSExpr Atom)
    envLetBindings = OMap SKey (Text, WellFormedSExpr Atom)
    forall k v. OMap k v
    OMap.empty
                          , envFreeVarEnv :: VarNameEnv t
    envFreeVarEnv = VarNameEnv t
    forall k v. OMap k v
    OMap.empty
                          , envFreeSymFnEnv :: FnNameEnv t
    envFreeSymFnEnv = FnNameEnv t
    forall k v. OMap k v
    OMap.empty
                          , envBoundVars :: Set (Some (ExprBoundVar t))
    envBoundVars = Set (Some (ExprBoundVar t))
    forall a. Set a
    Set.empty
                          }

    type Memo t a = State (MemoEnv t) a

    runMemo :: Config -> (Memo t a) -> (a, MemoEnv t)
    runMemo :: forall t a. Config -> Memo t a -> (a, MemoEnv t)
    runMemo Config
    cfg Memo t a
    m = Memo t a -> MemoEnv t -> (a, MemoEnv t)
    forall s a. State s a -> s -> (a, s)
    MS.runState Memo t a
    m (MemoEnv t -> (a, MemoEnv t)) -> MemoEnv t -> (a, MemoEnv t)
    forall a b. (a -> b) -> a -> b
    $ Config -> MemoEnv t
    forall t. Config -> MemoEnv t
    initEnv Config
    cfg

    -- | Serialize the given sexpression within a @letfn@ which
    -- serializes and binds all of the encountered SymFns. Note:
    -- this recursively also discovers and then serializes
    -- SymFns referenced within the body of the SymFns
    -- encountered thus far.
    letFn :: SExpr -> Memo t SExpr
    letFn :: forall t. WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    letFn WellFormedSExpr Atom
    sexpr = [(SomeExprSymFn t, Text)]
    -> [(Text, WellFormedSExpr Atom)]
    -> Set Text
    -> Memo t (WellFormedSExpr Atom)
    forall t.
    [(SomeExprSymFn t, Text)]
    -> [(Text, WellFormedSExpr Atom)]
    -> Set Text
    -> Memo t (WellFormedSExpr Atom)
    go [] [] Set Text
    forall a. Set a
    Set.empty
      where
        go :: [((SomeExprSymFn t), Text)] -> [(Text, SExpr)] -> Set Text ->  Memo t SExpr
        go :: forall t.
    [(SomeExprSymFn t, Text)]
    -> [(Text, WellFormedSExpr Atom)]
    -> Set Text
    -> Memo t (WellFormedSExpr Atom)
    go [] [(Text, WellFormedSExpr Atom)]
    fnBindings Set Text
    seen = do
          -- Although the `todo` list is empty, we may have
          -- encountered some SymFns along the way, so check for
          -- those and serialize any previously unseen SymFns.
          newFns <- (MemoEnv t -> [(SomeExprSymFn t, Text)])
    -> StateT (MemoEnv t) Identity [(SomeExprSymFn t, Text)]
    forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
    MS.gets (((SomeExprSymFn t, Text) -> Bool)
    -> [(SomeExprSymFn t, Text)] -> [(SomeExprSymFn t, Text)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (\(SomeExprSymFn t
    _symFn, Text
    varName) -> Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Text -> Set Text -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Text
    varName Set Text
    seen)
                             ([(SomeExprSymFn t, Text)] -> [(SomeExprSymFn t, Text)])
    -> (MemoEnv t -> [(SomeExprSymFn t, Text)])
    -> MemoEnv t
    -> [(SomeExprSymFn t, Text)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OMap (SomeExprSymFn t) Text -> [(SomeExprSymFn t, Text)]
    forall k v. OMap k v -> [(k, v)]
    OMap.assocs
                             (OMap (SomeExprSymFn t) Text -> [(SomeExprSymFn t, Text)])
    -> (MemoEnv t -> OMap (SomeExprSymFn t) Text)
    -> MemoEnv t
    -> [(SomeExprSymFn t, Text)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MemoEnv t -> OMap (SomeExprSymFn t) Text
    forall t. MemoEnv t -> FnNameEnv t
    envFreeSymFnEnv)
          if null newFns
            then if null fnBindings
                 then return sexpr
                 else let bs = ((Text, WellFormedSExpr Atom) -> WellFormedSExpr Atom)
    -> [(Text, WellFormedSExpr Atom)] -> [WellFormedSExpr Atom]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Text
    name, WellFormedSExpr Atom
    def) -> [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [Text -> WellFormedSExpr Atom
    ident Text
    name, WellFormedSExpr Atom
    def]) [(Text, WellFormedSExpr Atom)]
    fnBindings
                      in return $ S.L [ident "letfn" , S.L bs, sexpr]
            else go newFns fnBindings seen
        go (((SomeExprSymFn ExprSymFn t dom ret
    nextFn), Text
    nextFnName):[(SomeExprSymFn t, Text)]
    todo) [(Text, WellFormedSExpr Atom)]
    fnBindings Set Text
    seen = do
          nextSExpr <- ExprSymFn t dom ret
    -> StateT (MemoEnv t) Identity (WellFormedSExpr Atom)
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> Memo t (WellFormedSExpr Atom)
    convertSymFn ExprSymFn t dom ret
    nextFn
          let fnBindings' = (Text
    nextFnName, WellFormedSExpr Atom
    nextSExpr)(Text, WellFormedSExpr Atom)
    -> [(Text, WellFormedSExpr Atom)] -> [(Text, WellFormedSExpr Atom)]
    forall a. a -> [a] -> [a]
    :[(Text, WellFormedSExpr Atom)]
    fnBindings
              seen' = Text -> Set Text -> Set Text
    forall a. Ord a => a -> Set a -> Set a
    Set.insert Text
    nextFnName Set Text
    seen
          go todo fnBindings' seen'

    -- | Converts the given What4 expression into an
    -- s-expression and clears the let-binding cache (since it
    -- just emitted a let binding with any necessary let-bound
    -- vars).
    convertExprWithLet :: W4.Expr t tp -> Memo t SExpr
    convertExprWithLet :: forall t (tp :: BaseType).
    Expr t tp -> Memo t (WellFormedSExpr Atom)
    convertExprWithLet Expr t tp
    expr = do
      b <- Expr t tp -> Memo t (WellFormedSExpr Atom)
    forall t (tp :: BaseType).
    Expr t tp -> Memo t (WellFormedSExpr Atom)
    convertExpr Expr t tp
    expr
      bs <- map (\(Text
    varName, WellFormedSExpr Atom
    boundExpr) -> [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [ Text -> WellFormedSExpr Atom
    ident Text
    varName, WellFormedSExpr Atom
    boundExpr ])
            <$> map snd
            <$> OMap.assocs
            <$> MS.gets envLetBindings
      MS.modify' (\MemoEnv t
    r -> MemoEnv t
    r {envLetBindings = OMap.empty})
      return $ mkLet bs b

    mkLet :: [SExpr] -> SExpr -> SExpr
    mkLet :: [WellFormedSExpr Atom]
    -> WellFormedSExpr Atom -> WellFormedSExpr Atom
    mkLet [] WellFormedSExpr Atom
    body       = WellFormedSExpr Atom
    body
    mkLet [WellFormedSExpr Atom]
    bindings WellFormedSExpr Atom
    body = [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [Text -> WellFormedSExpr Atom
    ident Text
    "let", [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [WellFormedSExpr Atom]
    bindings, WellFormedSExpr Atom
    body]

    -- | Converts a What4 ExprSymFn into an s-expression within
    -- the Memo monad (i.e., no @let@ or @letfn@s are emitted).
    convertSymFn :: forall t args ret
                  . W4.ExprSymFn t args ret
                 -> Memo t SExpr
    convertSymFn :: forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> Memo t (WellFormedSExpr Atom)
    convertSymFn symFn :: ExprSymFn t args ret
    symFn@(W4.ExprSymFn Nonce t (args ::> ret)
    _ SolverSymbol
    symFnName SymFnInfo t args ret
    symFnInfo ProgramLoc
    _) = do
     case SymFnInfo t args ret
    symFnInfo of
       W4.DefinedFnInfo Assignment (ExprBoundVar t) args
    argVars Expr t ret
    body UnfoldPolicy
    _ -> do
         let sArgTs :: [WellFormedSExpr Atom]
    sArgTs = Assignment BaseTypeRepr args -> [WellFormedSExpr Atom]
    forall (tps :: Ctx BaseType).
    Assignment BaseTypeRepr tps -> [WellFormedSExpr Atom]
    convertBaseTypes (ExprSymFn t args ret -> Assignment BaseTypeRepr args
    forall (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> Assignment BaseTypeRepr args
    forall (fn :: Ctx BaseType -> BaseType -> Type)
           (args :: Ctx BaseType) (ret :: BaseType).
    IsSymFn fn =>
    fn args ret -> Assignment BaseTypeRepr args
    W4.fnArgTypes ExprSymFn t args ret
    symFn)
             sRetT :: WellFormedSExpr Atom
    sRetT = BaseTypeRepr ret -> WellFormedSExpr Atom
    forall (tp :: BaseType). BaseTypeRepr tp -> WellFormedSExpr Atom
    convertBaseType (ExprSymFn t args ret -> BaseTypeRepr ret
    forall (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> BaseTypeRepr ret
    forall (fn :: Ctx BaseType -> BaseType -> Type)
           (args :: Ctx BaseType) (ret :: BaseType).
    IsSymFn fn =>
    fn args ret -> BaseTypeRepr ret
    W4.fnReturnType ExprSymFn t args ret
    symFn)
         argsWithFreshNames <- let rawArgs :: [Some (ExprBoundVar t)]
    rawArgs = (forall (x :: BaseType). ExprBoundVar t x -> Some (ExprBoundVar t))
    -> forall (x :: Ctx BaseType).
       Assignment (ExprBoundVar t) x -> [Some (ExprBoundVar t)]
    forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
    FoldableFC t =>
    (forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
    forall (f :: BaseType -> Type) a.
    (forall (x :: BaseType). f x -> a)
    -> forall (x :: Ctx BaseType). Assignment f x -> [a]
    FC.toListFC ExprBoundVar t x -> Some (ExprBoundVar t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    forall (x :: BaseType). ExprBoundVar t x -> Some (ExprBoundVar t)
    Some Assignment (ExprBoundVar t) args
    argVars
                               in (Some (ExprBoundVar t)
     -> StateT (MemoEnv t) Identity (Some (ExprBoundVar t), Text))
    -> [Some (ExprBoundVar t)]
    -> StateT (MemoEnv t) Identity [(Some (ExprBoundVar t), Text)]
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> [a] -> m [b]
    mapM Some (ExprBoundVar t)
    -> StateT (MemoEnv t) Identity (Some (ExprBoundVar t), Text)
    getBoundVarWithFreshName [Some (ExprBoundVar t)]
    rawArgs
         let (origBoundVars, freshArgNames) = unzip argsWithFreshNames
         -- Convert the body with the bound variable set and
         -- free-variable mapping extended to reflect being
         -- under the function's binders.
         sExpr <- MS.withState (\MemoEnv t
    ms -> let boundVars :: Set (Some (ExprBoundVar t))
    boundVars = MemoEnv t -> Set (Some (ExprBoundVar t))
    forall t. MemoEnv t -> Set (Some (ExprBoundVar t))
    envBoundVars MemoEnv t
    ms
                                           fvEnv :: VarNameEnv t
    fvEnv = MemoEnv t -> VarNameEnv t
    forall t. MemoEnv t -> VarNameEnv t
    envFreeVarEnv MemoEnv t
    ms
                                 in MemoEnv t
    ms { envBoundVars = Set.union boundVars (Set.fromList origBoundVars)
                                       , envFreeVarEnv = fvEnv OMap.<>| (OMap.fromList argsWithFreshNames)})
                  $ convertExprWithLet body
         return $ S.L [ ident "definedfn"
                      , string (Some W4.UnicodeRepr) $ W4.solverSymbolAsText symFnName
                      , S.L ((ident "->"):sArgTs ++ [sRetT])
                      , S.L $ map ident freshArgNames
                      , sExpr
                      ]
       W4.UninterpFnInfo Assignment BaseTypeRepr args
    argTs BaseTypeRepr ret
    retT ->
         let sArgTs :: [WellFormedSExpr Atom]
    sArgTs = Assignment BaseTypeRepr args -> [WellFormedSExpr Atom]
    forall (tps :: Ctx BaseType).
    Assignment BaseTypeRepr tps -> [WellFormedSExpr Atom]
    convertBaseTypes Assignment BaseTypeRepr args
    argTs
             sRetT :: WellFormedSExpr Atom
    sRetT = BaseTypeRepr ret -> WellFormedSExpr Atom
    forall (tp :: BaseType). BaseTypeRepr tp -> WellFormedSExpr Atom
    convertBaseType BaseTypeRepr ret
    retT
         in WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [ Text -> WellFormedSExpr Atom
    ident Text
    "uninterpfn"
                         , Some StringInfoRepr -> Text -> WellFormedSExpr Atom
    string (StringInfoRepr 'Unicode -> Some StringInfoRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some StringInfoRepr 'Unicode
    W4.UnicodeRepr) (Text -> WellFormedSExpr Atom) -> Text -> WellFormedSExpr Atom
    forall a b. (a -> b) -> a -> b
    $ SolverSymbol -> Text
    W4.solverSymbolAsText SolverSymbol
    symFnName
                         , [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L ((Text -> WellFormedSExpr Atom
    ident Text
    "->")WellFormedSExpr Atom
    -> [WellFormedSExpr Atom] -> [WellFormedSExpr Atom]
    forall a. a -> [a] -> [a]
    :[WellFormedSExpr Atom]
    sArgTs [WellFormedSExpr Atom]
    -> [WellFormedSExpr Atom] -> [WellFormedSExpr Atom]
    forall a. [a] -> [a] -> [a]
    ++ [WellFormedSExpr Atom
    sRetT])
                         ]
       W4.MatlabSolverFnInfo MatlabSolverFn (Expr t) args ret
    _msfn Assignment (ExprBoundVar t) args
    _argTs Expr t ret
    _body ->
         String -> Memo t (WellFormedSExpr Atom)
    forall a. HasCallStack => String -> a
    error String
    "MatlabSolverFnInfo SymFns are not yet supported"
      where
        getBoundVarWithFreshName ::
          (Some (W4.ExprBoundVar t)) ->
          Memo t (Some (W4.ExprBoundVar t), Text)
        getBoundVarWithFreshName :: Some (ExprBoundVar t)
    -> StateT (MemoEnv t) Identity (Some (ExprBoundVar t), Text)
    getBoundVarWithFreshName someVar :: Some (ExprBoundVar t)
    someVar@(Some ExprBoundVar t x
    var) = do
          nm <- BaseTypeRepr x -> Memo t Text
    forall (tp :: BaseType) t. BaseTypeRepr tp -> Memo t Text
    freshName (ExprBoundVar t x -> BaseTypeRepr x
    forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
    W4.bvarType ExprBoundVar t x
    var)
          return (someVar, nm)

    -- | Key for sharing SExpr construction. Internally indexes are expression nonces,
    -- but the let-binding identifiers are based on insertion order to the OMap
    newtype SKey = SKey {SKey -> Word64
    sKeyValue :: Word64}
      deriving (SKey -> SKey -> Bool
    (SKey -> SKey -> Bool) -> (SKey -> SKey -> Bool) -> Eq SKey
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: SKey -> SKey -> Bool
    == :: SKey -> SKey -> Bool
    $c/= :: SKey -> SKey -> Bool
    /= :: SKey -> SKey -> Bool
    Eq, Eq SKey
    Eq SKey =>
    (SKey -> SKey -> Ordering)
    -> (SKey -> SKey -> Bool)
    -> (SKey -> SKey -> Bool)
    -> (SKey -> SKey -> Bool)
    -> (SKey -> SKey -> Bool)
    -> (SKey -> SKey -> SKey)
    -> (SKey -> SKey -> SKey)
    -> Ord SKey
    SKey -> SKey -> Bool
    SKey -> SKey -> Ordering
    SKey -> SKey -> SKey
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: SKey -> SKey -> Ordering
    compare :: SKey -> SKey -> Ordering
    $c< :: SKey -> SKey -> Bool
    < :: SKey -> SKey -> Bool
    $c<= :: SKey -> SKey -> Bool
    <= :: SKey -> SKey -> Bool
    $c> :: SKey -> SKey -> Bool
    > :: SKey -> SKey -> Bool
    $c>= :: SKey -> SKey -> Bool
    >= :: SKey -> SKey -> Bool
    $cmax :: SKey -> SKey -> SKey
    max :: SKey -> SKey -> SKey
    $cmin :: SKey -> SKey -> SKey
    min :: SKey -> SKey -> SKey
    Ord, Int -> SKey -> ShowS
    [SKey] -> ShowS
    SKey -> String
    (Int -> SKey -> ShowS)
    -> (SKey -> String) -> ([SKey] -> ShowS) -> Show SKey
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> SKey -> ShowS
    showsPrec :: Int -> SKey -> ShowS
    $cshow :: SKey -> String
    show :: SKey -> String
    $cshowList :: [SKey] -> ShowS
    showList :: [SKey] -> ShowS
    Show)

    freshName :: W4.BaseTypeRepr tp -> Memo t Text
    freshName :: forall (tp :: BaseType) t. BaseTypeRepr tp -> Memo t Text
    freshName BaseTypeRepr tp
    tp = do
      idCount <- (MemoEnv t -> Natural) -> StateT (MemoEnv t) Identity Natural
    forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
    MS.gets MemoEnv t -> Natural
    forall t. MemoEnv t -> Natural
    envIdCounter
      MS.modify' $ (\MemoEnv t
    e -> MemoEnv t
    e {envIdCounter = idCount + 1})
      let prefix = case BaseTypeRepr tp
    tp of
                     W4.BaseBoolRepr{} -> String
    "bool"
                     W4.BaseIntegerRepr{} -> String
    "int"
                     W4.BaseRealRepr{} -> String
    "real"
                     W4.BaseFloatRepr{} -> String
    "fl"
                     W4.BaseStringRepr{} -> String
    "str"
                     BaseTypeRepr tp
    W4.BaseComplexRepr -> String
    "cmplx"
                     W4.BaseBVRepr{} -> String
    "bv"
                     W4.BaseStructRepr{} -> String
    "struct"
                     W4.BaseArrayRepr{} -> String
    "arr"
      return $ T.pack $ prefix++(show $ idCount)

    freshFnName :: W4.ExprSymFn t args ret -> Memo t Text
    freshFnName :: forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> Memo t Text
    freshFnName ExprSymFn t args ret
    fn = do
      idCount <- (MemoEnv t -> Natural) -> StateT (MemoEnv t) Identity Natural
    forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
    MS.gets MemoEnv t -> Natural
    forall t. MemoEnv t -> Natural
    envIdCounter
      MS.modify' $ (\MemoEnv t
    e -> MemoEnv t
    e {envIdCounter = idCount + 1})
      let prefix = case ExprSymFn t args ret -> SymFnInfo t args ret
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> SymFnInfo t args ret
    W4.symFnInfo ExprSymFn t args ret
    fn of
                     W4.UninterpFnInfo{} -> String
    "ufn"
                     W4.DefinedFnInfo{} -> String
    "dfn"
                     W4.MatlabSolverFnInfo{} -> String
    "mfn"
      return $ T.pack $ prefix++(show $ idCount)

    exprSKey :: W4.Expr t tp -> Maybe SKey
    exprSKey :: forall t (tp :: BaseType). Expr t tp -> Maybe SKey
    exprSKey Expr t tp
    x = Word64 -> SKey
    SKey (Word64 -> SKey) -> (Nonce t tp -> Word64) -> Nonce t tp -> SKey
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nonce t tp -> Word64
    forall k s (tp :: k). Nonce s tp -> Word64
    Nonce.indexValue (Nonce t tp -> SKey) -> Maybe (Nonce t tp) -> Maybe SKey
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr t tp -> Maybe (Nonce t tp)
    forall t (tp :: BaseType). Expr t tp -> Maybe (Nonce t tp)
    W4.exprMaybeId Expr t tp
    x

    -- | Allocate a fresh variable for the given
    -- nonce-key/s-expression and save the variable/expression
    -- mapping in the Memo monad.
    addLetBinding :: SKey -> SExpr -> W4.BaseTypeRepr tp -> Memo t Text
    addLetBinding :: forall (tp :: BaseType) t.
    SKey -> WellFormedSExpr Atom -> BaseTypeRepr tp -> Memo t Text
    addLetBinding SKey
    key WellFormedSExpr Atom
    sexp BaseTypeRepr tp
    tp = do
      letVarName <- BaseTypeRepr tp -> Memo t Text
    forall (tp :: BaseType) t. BaseTypeRepr tp -> Memo t Text
    freshName BaseTypeRepr tp
    tp
      curLetBindings <- MS.gets envLetBindings
      MS.modify' $ (\MemoEnv t
    e -> MemoEnv t
    e {envLetBindings =  curLetBindings OMap.|> (key, (letVarName, sexp))})
      return letVarName

    -- | Converts a What 4 expression into an s-expression
    -- within the Memo monad (i.e., no @let@ or @letfn@s are
    -- emitted in the result).
    convertExpr :: forall t tp . W4.Expr t tp -> Memo t SExpr
    convertExpr :: forall t (tp :: BaseType).
    Expr t tp -> Memo t (WellFormedSExpr Atom)
    convertExpr Expr t tp
    initialExpr = do
      case Expr t tp -> Maybe SKey
    forall t (tp :: BaseType). Expr t tp -> Maybe SKey
    exprSKey Expr t tp
    initialExpr of
        Maybe SKey
    Nothing -> Expr t tp -> Memo t (WellFormedSExpr Atom)
    go Expr t tp
    initialExpr
        Just SKey
    key -> do
          letCache <- (MemoEnv t -> OMap SKey (Text, WellFormedSExpr Atom))
    -> StateT
         (MemoEnv t) Identity (OMap SKey (Text, WellFormedSExpr Atom))
    forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
    MS.gets MemoEnv t -> OMap SKey (Text, WellFormedSExpr Atom)
    forall t. MemoEnv t -> OMap SKey (Text, WellFormedSExpr Atom)
    envLetBindings
          case OMap.lookup key letCache of
            Just (Text
    name, WellFormedSExpr Atom
    _) -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Text -> WellFormedSExpr Atom
    ident Text
    name
            Maybe (Text, WellFormedSExpr Atom)
    Nothing -> do
              sexp <- Expr t tp -> Memo t (WellFormedSExpr Atom)
    go Expr t tp
    initialExpr
              case sexp of
                S.A Atom
    _ -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return WellFormedSExpr Atom
    sexp -- Don't memoize atomic s-expressions - that's just silly.
                WellFormedSExpr Atom
    _ -> do
                  letVarName <- SKey -> WellFormedSExpr Atom -> BaseTypeRepr tp -> Memo t Text
    forall (tp :: BaseType) t.
    SKey -> WellFormedSExpr Atom -> BaseTypeRepr tp -> Memo t Text
    addLetBinding SKey
    key WellFormedSExpr Atom
    sexp (Expr t tp -> BaseTypeRepr tp
    forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W4.exprType Expr t tp
    initialExpr)
                  return $ ident letVarName
      where go :: W4.Expr t tp -> Memo t SExpr
            go :: Expr t tp -> Memo t (WellFormedSExpr Atom)
    go (W4.SemiRingLiteral SemiRingRepr sr
    W4.SemiRingIntegerRepr Coefficient sr
    val ProgramLoc
    _) = WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Integer -> WellFormedSExpr Atom
    int Integer
    Coefficient sr
    val -- do we need/want these?
            go (W4.SemiRingLiteral SemiRingRepr sr
    W4.SemiRingRealRepr Coefficient sr
    val ProgramLoc
    _) = WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Rational -> WellFormedSExpr Atom
    real Rational
    Coefficient sr
    val
            go (W4.SemiRingLiteral (W4.SemiRingBVRepr BVFlavorRepr fv
    _ NatRepr w
    sz) Coefficient sr
    val ProgramLoc
    _) = WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Natural -> Integer -> WellFormedSExpr Atom
    bitvec (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    sz) (BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    Coefficient sr
    val)
            go (W4.StringExpr StringLiteral si
    str ProgramLoc
    _) =
              case (StringLiteral si -> StringInfoRepr si
    forall (si :: StringInfo). StringLiteral si -> StringInfoRepr si
    W4.stringLiteralInfo StringLiteral si
    str) of
                StringInfoRepr si
    W4.UnicodeRepr -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Some StringInfoRepr -> Text -> WellFormedSExpr Atom
    string (StringInfoRepr 'Unicode -> Some StringInfoRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some StringInfoRepr 'Unicode
    W4.UnicodeRepr) (StringLiteral 'Unicode -> Text
    W4S.fromUnicodeLit StringLiteral si
    StringLiteral 'Unicode
    str)
                StringInfoRepr si
    W4.Char8Repr -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Some StringInfoRepr -> Text -> WellFormedSExpr Atom
    string (StringInfoRepr 'Char8 -> Some StringInfoRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some StringInfoRepr 'Char8
    W4.Char8Repr) (Text -> WellFormedSExpr Atom) -> Text -> WellFormedSExpr Atom
    forall a b. (a -> b) -> a -> b
    $ ByteString -> Text
    T.decodeUtf8 (ByteString -> Text) -> ByteString -> Text
    forall a b. (a -> b) -> a -> b
    $ StringLiteral 'Char8 -> ByteString
    W4S.fromChar8Lit StringLiteral si
    StringLiteral 'Char8
    str
                StringInfoRepr si
    W4.Char16Repr -> String -> Memo t (WellFormedSExpr Atom)
    forall a. HasCallStack => String -> a
    error String
    "Char16 strings are not yet supported"
                  -- TODO - there is no `W4S.toLEByteString` currently... hmm...
                  -- return $ string (Some W4.Char16Repr) $ T.decodeUtf16LE $ W4S.toLEByteString $ W4S.fromChar16Lit str
            go (W4.FloatExpr FloatPrecisionRepr fpp
    prec BigFloat
    bf ProgramLoc
    _) = WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ FloatPrecisionRepr fpp -> BigFloat -> WellFormedSExpr Atom
    forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp -> BigFloat -> WellFormedSExpr Atom
    float FloatPrecisionRepr fpp
    prec BigFloat
    bf
            go (W4.BoolExpr Bool
    b ProgramLoc
    _) = WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Bool -> WellFormedSExpr Atom
    bool Bool
    b
            go (W4.AppExpr AppExpr t tp
    appExpr) = AppExpr t tp -> Memo t (WellFormedSExpr Atom)
    forall t (tp :: BaseType).
    AppExpr t tp -> Memo t (WellFormedSExpr Atom)
    convertAppExpr' AppExpr t tp
    appExpr
            go (W4.NonceAppExpr NonceAppExpr t tp
    nae) =
              case NonceAppExpr t tp -> NonceApp t (Expr t) tp
    forall t (tp :: BaseType).
    NonceAppExpr t tp -> NonceApp t (Expr t) tp
    W4.nonceExprApp NonceAppExpr t tp
    nae of
                W4.FnApp ExprSymFn t args tp
    fn Assignment (Expr t) args
    args -> ExprSymFn t args tp
    -> Assignment (Expr t) args -> Memo t (WellFormedSExpr Atom)
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret
    -> Assignment (Expr t) args -> Memo t (WellFormedSExpr Atom)
    convertFnApp ExprSymFn t args tp
    fn Assignment (Expr t) args
    args
                W4.Forall {} -> String -> Memo t (WellFormedSExpr Atom)
    forall a. HasCallStack => String -> a
    error String
    "Forall NonceAppExpr not yet supported"
                W4.Exists {} -> String -> Memo t (WellFormedSExpr Atom)
    forall a. HasCallStack => String -> a
    error String
    "Exists NonceAppExpr not yet supported"
                W4.ArrayFromFn {} -> String -> Memo t (WellFormedSExpr Atom)
    forall a. HasCallStack => String -> a
    error String
    "ArrayFromFn NonceAppExpr not yet supported"
                W4.MapOverArrays {} -> String -> Memo t (WellFormedSExpr Atom)
    forall a. HasCallStack => String -> a
    error String
    "MapOverArrays NonceAppExpr not yet supported"
                W4.ArrayTrueOnEntries {} -> String -> Memo t (WellFormedSExpr Atom)
    forall a. HasCallStack => String -> a
    error String
    "ArrayTrueOnEntries NonceAppExpr not yet supported"
                W4.Annotation {} -> String -> Memo t (WellFormedSExpr Atom)
    forall a. HasCallStack => String -> a
    error String
    "Annotation NonceAppExpr not yet supported"
            go (W4.BoundVarExpr ExprBoundVar t tp
    var) = ExprBoundVar t tp -> Memo t (WellFormedSExpr Atom)
    forall t (tp :: BaseType).
    ExprBoundVar t tp -> Memo t (WellFormedSExpr Atom)
    convertBoundVarExpr ExprBoundVar t tp
    var

    -- | Serialize bound variables as the s-expression identifier `name_nonce`. This allows us to
    -- preserve their human-readable name while ensuring they are globally unique w/ the nonce suffix.
    convertBoundVarExpr :: forall t tp. W4.ExprBoundVar t tp -> Memo t SExpr
    convertBoundVarExpr :: forall t (tp :: BaseType).
    ExprBoundVar t tp -> Memo t (WellFormedSExpr Atom)
    convertBoundVarExpr ExprBoundVar t tp
    x = do
      fvsAllowed <- (MemoEnv t -> Bool) -> StateT (MemoEnv t) Identity Bool
    forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
    MS.gets (Config -> Bool
    cfgAllowFreeVars (Config -> Bool) -> (MemoEnv t -> Config) -> MemoEnv t -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MemoEnv t -> Config
    forall t. MemoEnv t -> Config
    envConfig)
      bvs <- MS.gets envBoundVars
      -- If this variable is not bound (in the standard syntactic sense)
      -- and free variables are not explicitly permitted, raise an error.
      M.when ((not $ Set.member (Some x) bvs) && (not fvsAllowed)) $
        error $
        "encountered the free What4 ExprBoundVar `"
        ++ (T.unpack (W4.solverSymbolAsText (W4.bvarName x)))
        ++ "`, but the user-specified configuration dissallows free variables."
      -- Get the renaming cache and either use the name already generated
      -- or generate a fresh name and record it.
      varEnv <- MS.gets envFreeVarEnv
      case OMap.lookup (Some x) varEnv of
        Just Text
    var -> WellFormedSExpr Atom
    -> StateT (MemoEnv t) Identity (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom
     -> StateT (MemoEnv t) Identity (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom
    -> StateT (MemoEnv t) Identity (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Text -> WellFormedSExpr Atom
    ident Text
    var
        Maybe Text
    Nothing -> do
          varName <- BaseTypeRepr tp -> Memo t Text
    forall (tp :: BaseType) t. BaseTypeRepr tp -> Memo t Text
    freshName (BaseTypeRepr tp -> Memo t Text) -> BaseTypeRepr tp -> Memo t Text
    forall a b. (a -> b) -> a -> b
    $ ExprBoundVar t tp -> BaseTypeRepr tp
    forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
    W4.bvarType ExprBoundVar t tp
    x
          MS.modify' $ (\MemoEnv t
    e -> MemoEnv t
    e {envFreeVarEnv = varEnv OMap.|> ((Some x), varName)})
          return $ ident varName

    convertAppExpr' :: forall t tp . W4.AppExpr t tp -> Memo t SExpr
    convertAppExpr' :: forall t (tp :: BaseType).
    AppExpr t tp -> Memo t (WellFormedSExpr Atom)
    convertAppExpr' = App (Expr t) tp -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    App (Expr t) tp' -> Memo t (WellFormedSExpr Atom)
    go (App (Expr t) tp -> Memo t (WellFormedSExpr Atom))
    -> (AppExpr t tp -> App (Expr t) tp)
    -> AppExpr t tp
    -> Memo t (WellFormedSExpr Atom)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AppExpr t tp -> App (Expr t) tp
    forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
    W4.appExprApp
      where go :: forall tp' . W4.App (W4.Expr t) tp' -> Memo t SExpr
            go :: forall (tp' :: BaseType).
    App (Expr t) tp' -> Memo t (WellFormedSExpr Atom)
    go (W4.BaseIte BaseTypeRepr tp'
    _bt Integer
    _ Expr t 'BaseBoolType
    e1 Expr t tp'
    e2 Expr t tp'
    e3) = do
              s1 <- Expr t 'BaseBoolType -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t 'BaseBoolType
    e1
              s2 <- goE e2
              s3 <- goE e3
              return $ S.L [ident "ite", s1, s2, s3]
            go (W4.BaseEq BaseTypeRepr tp1
    _bt Expr t tp1
    e1 Expr t tp1
    e2) = do
              s1 <- Expr t tp1 -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t tp1
    e1
              s2 <- goE e2
              return $ S.L [ident "=", s1, s2]
            go (W4.NotPred Expr t 'BaseBoolType
    e) = do
              s <- Expr t 'BaseBoolType -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t 'BaseBoolType
    e
              return $ S.L [ident "notp", s]
            go (W4.ConjPred BoolMap (Expr t)
    bm) = Text -> Bool -> BoolMap (Expr t) -> Memo t (WellFormedSExpr Atom)
    convertBoolMap Text
    "andp" Bool
    True BoolMap (Expr t)
    bm
            go (W4.BVSlt Expr t (BaseBVType w)
    e1 Expr t (BaseBVType w)
    e2) = do
              s1 <- Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t (BaseBVType w)
    e1
              s2 <- goE e2
              return $ S.L [ident "bvslt", s1, s2]
            go (W4.BVUlt Expr t (BaseBVType w)
    e1 Expr t (BaseBVType w)
    e2) = do
              s1 <- Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t (BaseBVType w)
    e1
              s2 <- goE e2
              return $ S.L [ident "bvult", s1, s2]
            go (W4.BVConcat NatRepr (u + v)
    _ Expr t (BaseBVType u)
    e1 Expr t (BaseBVType v)
    e2) = do
              s1 <- Expr t (BaseBVType u) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t (BaseBVType u)
    e1
              s2 <- goE e2
              return $ S.L [ident "concat", s1, s2]
            go (W4.BVSelect NatRepr idx
    idx NatRepr n
    n Expr t (BaseBVType w)
    bv) = Integer
    -> Integer
    -> Expr t (BaseBVType w)
    -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Integer -> Integer -> Expr t tp' -> Memo t (WellFormedSExpr Atom)
    extract Integer
    i Integer
    j Expr t (BaseBVType w)
    bv
              -- See SemMC.Formula.Parser.readExtract for the explanation behind
              -- these values.
              where i :: Integer
    i = NatRepr n -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue NatRepr n
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    j Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1
                    j :: Integer
    j = NatRepr idx -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue NatRepr idx
    idx

            -- Note that because the SemiRing has an identity element that
            -- always gets applied, resulting in lots of additional,
            -- unnecessary elements like: "(bvand #xffffffff TERM)".
            -- These will get manifested in the stored form (but generally
            -- _not_ via DSL-generated versions since they don't output
            -- via Printer) and result in longer stored forms.  They could
            -- be eliminated by checking for the identity (e.g. "if mul ==
            -- SR.one (WSum.sumRepr sm)") but the re-loaded representation
            -- will still use the SemiRing, so it's probably not worth the
            -- effort to reduce these.
            go (W4.SemiRingSum WeightedSum (Expr t) sr
    sm) =
              case WeightedSum (Expr t) sr -> SemiRingRepr sr
    forall (f :: BaseType -> Type) (sr :: SemiRing).
    WeightedSum f sr -> SemiRingRepr sr
    WSum.sumRepr WeightedSum (Expr t) sr
    sm of
                W4.SemiRingBVRepr BVFlavorRepr fv
    W4.BVArithRepr NatRepr w
    w ->
                  let smul :: BV w -> Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    smul BV w
    mul Expr t (BaseBVType w)
    e = do
                        s <- Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t (BaseBVType w)
    e
                        return $ S.L [ ident "bvmul", bitvec (natValue w) (BV.asUnsigned mul), s]
                      sval :: BV w -> Memo t (WellFormedSExpr Atom)
    sval BV w
    v = WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Natural -> Integer -> WellFormedSExpr Atom
    bitvec (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w) (BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    v)
                      add :: WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    add WellFormedSExpr Atom
    x WellFormedSExpr Atom
    y = WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> m (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [ Text -> WellFormedSExpr Atom
    ident Text
    "bvadd", WellFormedSExpr Atom
    x, WellFormedSExpr Atom
    y ]
                  in (WellFormedSExpr Atom
     -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> (Coefficient sr
        -> Expr t (SemiRingBase sr) -> Memo t (WellFormedSExpr Atom))
    -> (Coefficient sr -> Memo t (WellFormedSExpr Atom))
    -> WeightedSum (Expr t) sr
    -> Memo t (WellFormedSExpr Atom)
    forall (m :: Type -> Type) r (sr :: SemiRing)
           (f :: BaseType -> Type).
    Monad m =>
    (r -> r -> m r)
    -> (Coefficient sr -> f (SemiRingBase sr) -> m r)
    -> (Coefficient sr -> m r)
    -> WeightedSum f sr
    -> m r
    WSum.evalM WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall {m :: Type -> Type}.
    Monad m =>
    WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    add BV w -> Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    Coefficient sr
    -> Expr t (SemiRingBase sr) -> Memo t (WellFormedSExpr Atom)
    smul BV w -> Memo t (WellFormedSExpr Atom)
    Coefficient sr -> Memo t (WellFormedSExpr Atom)
    sval WeightedSum (Expr t) sr
    sm
                W4.SemiRingBVRepr BVFlavorRepr fv
    W4.BVBitsRepr NatRepr w
    w ->
                  let smul :: BV w -> Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    smul BV w
    mul Expr t (BaseBVType w)
    e = do
                        s <- Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t (BaseBVType w)
    e
                        return $ S.L [ ident "bvand", bitvec (natValue w) (BV.asUnsigned mul), s]
                      sval :: BV w -> Memo t (WellFormedSExpr Atom)
    sval BV w
    v = WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Natural -> Integer -> WellFormedSExpr Atom
    bitvec (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w) (BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    v)
                      add :: WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    add WellFormedSExpr Atom
    x WellFormedSExpr Atom
    y = let op :: WellFormedSExpr Atom
    op = Text -> WellFormedSExpr Atom
    ident Text
    "bvxor" in WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> m (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [ WellFormedSExpr Atom
    op, WellFormedSExpr Atom
    x, WellFormedSExpr Atom
    y ]
                  in (WellFormedSExpr Atom
     -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> (Coefficient sr
        -> Expr t (SemiRingBase sr) -> Memo t (WellFormedSExpr Atom))
    -> (Coefficient sr -> Memo t (WellFormedSExpr Atom))
    -> WeightedSum (Expr t) sr
    -> Memo t (WellFormedSExpr Atom)
    forall (m :: Type -> Type) r (sr :: SemiRing)
           (f :: BaseType -> Type).
    Monad m =>
    (r -> r -> m r)
    -> (Coefficient sr -> f (SemiRingBase sr) -> m r)
    -> (Coefficient sr -> m r)
    -> WeightedSum f sr
    -> m r
    WSum.evalM WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall {m :: Type -> Type}.
    Monad m =>
    WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    add BV w -> Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    Coefficient sr
    -> Expr t (SemiRingBase sr) -> Memo t (WellFormedSExpr Atom)
    smul BV w -> Memo t (WellFormedSExpr Atom)
    Coefficient sr -> Memo t (WellFormedSExpr Atom)
    sval WeightedSum (Expr t) sr
    sm
                SemiRingRepr sr
    W4.SemiRingIntegerRepr ->
                  let smul :: Integer -> Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
    smul Integer
    mul Expr t 'BaseIntegerType
    e = do
                        s <- Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t 'BaseIntegerType
    e
                        return $ S.L [ ident "intmul", int mul, s]
                      sval :: Integer -> m (WellFormedSExpr Atom)
    sval Integer
    v = WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> m (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Integer -> WellFormedSExpr Atom
    int Integer
    v
                      add :: WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    add WellFormedSExpr Atom
    x WellFormedSExpr Atom
    y = WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> m (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [ Text -> WellFormedSExpr Atom
    ident Text
    "intadd", WellFormedSExpr Atom
    x, WellFormedSExpr Atom
    y ]
                  in (WellFormedSExpr Atom
     -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> (Coefficient sr
        -> Expr t (SemiRingBase sr) -> Memo t (WellFormedSExpr Atom))
    -> (Coefficient sr -> Memo t (WellFormedSExpr Atom))
    -> WeightedSum (Expr t) sr
    -> Memo t (WellFormedSExpr Atom)
    forall (m :: Type -> Type) r (sr :: SemiRing)
           (f :: BaseType -> Type).
    Monad m =>
    (r -> r -> m r)
    -> (Coefficient sr -> f (SemiRingBase sr) -> m r)
    -> (Coefficient sr -> m r)
    -> WeightedSum f sr
    -> m r
    WSum.evalM WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall {m :: Type -> Type}.
    Monad m =>
    WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    add Integer -> Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
    Coefficient sr
    -> Expr t (SemiRingBase sr) -> Memo t (WellFormedSExpr Atom)
    smul Integer -> Memo t (WellFormedSExpr Atom)
    Coefficient sr -> Memo t (WellFormedSExpr Atom)
    forall {m :: Type -> Type}.
    Monad m =>
    Integer -> m (WellFormedSExpr Atom)
    sval WeightedSum (Expr t) sr
    sm
                SemiRingRepr sr
    W4.SemiRingRealRepr    -> String -> Memo t (WellFormedSExpr Atom)
    forall a. HasCallStack => String -> a
    error String
    "SemiRingSum RealRepr not supported"

            go (W4.SemiRingProd SemiRingProduct (Expr t) sr
    pd) =
              case SemiRingProduct (Expr t) sr -> SemiRingRepr sr
    forall (f :: BaseType -> Type) (sr :: SemiRing).
    SemiRingProduct f sr -> SemiRingRepr sr
    WSum.prodRepr SemiRingProduct (Expr t) sr
    pd of
                W4.SemiRingBVRepr BVFlavorRepr fv
    W4.BVArithRepr NatRepr w
    w -> do
                  let pmul :: WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    pmul WellFormedSExpr Atom
    x WellFormedSExpr Atom
    y = WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> m (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [ Text -> WellFormedSExpr Atom
    ident Text
    "bvmul", WellFormedSExpr Atom
    x, WellFormedSExpr Atom
    y ]
                  maybeS <- (WellFormedSExpr Atom
     -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> (Expr t (SemiRingBase sr) -> Memo t (WellFormedSExpr Atom))
    -> SemiRingProduct (Expr t) sr
    -> StateT (MemoEnv t) Identity (Maybe (WellFormedSExpr Atom))
    forall (m :: Type -> Type) r (f :: BaseType -> Type)
           (sr :: SemiRing).
    Monad m =>
    (r -> r -> m r)
    -> (f (SemiRingBase sr) -> m r)
    -> SemiRingProduct f sr
    -> m (Maybe r)
    WSum.prodEvalM WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall {m :: Type -> Type}.
    Monad m =>
    WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    pmul Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    Expr t (SemiRingBase sr) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE SemiRingProduct (Expr t) sr
    pd
                  case maybeS of
                    Just WellFormedSExpr Atom
    s -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return WellFormedSExpr Atom
    s
                    Maybe (WellFormedSExpr Atom)
    Nothing -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Natural -> Integer -> WellFormedSExpr Atom
    bitvec (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w) Integer
    1
                W4.SemiRingBVRepr BVFlavorRepr fv
    W4.BVBitsRepr NatRepr w
    w -> do
                  let pmul :: WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    pmul WellFormedSExpr Atom
    x WellFormedSExpr Atom
    y = WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> m (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [ Text -> WellFormedSExpr Atom
    ident Text
    "bvand", WellFormedSExpr Atom
    x, WellFormedSExpr Atom
    y ]
                  maybeS <- (WellFormedSExpr Atom
     -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> (Expr t (SemiRingBase sr) -> Memo t (WellFormedSExpr Atom))
    -> SemiRingProduct (Expr t) sr
    -> StateT (MemoEnv t) Identity (Maybe (WellFormedSExpr Atom))
    forall (m :: Type -> Type) r (f :: BaseType -> Type)
           (sr :: SemiRing).
    Monad m =>
    (r -> r -> m r)
    -> (f (SemiRingBase sr) -> m r)
    -> SemiRingProduct f sr
    -> m (Maybe r)
    WSum.prodEvalM WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall {m :: Type -> Type}.
    Monad m =>
    WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    pmul Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    Expr t (SemiRingBase sr) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE SemiRingProduct (Expr t) sr
    pd
                  case maybeS of
                    Just WellFormedSExpr Atom
    s -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return WellFormedSExpr Atom
    s
                    Maybe (WellFormedSExpr Atom)
    Nothing -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Natural -> Integer -> WellFormedSExpr Atom
    bitvec (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w) Integer
    1
                SemiRingRepr sr
    W4.SemiRingIntegerRepr -> do
                  let pmul :: WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    pmul WellFormedSExpr Atom
    x WellFormedSExpr Atom
    y = WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    forall a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> m (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [ Text -> WellFormedSExpr Atom
    ident Text
    "intmul", WellFormedSExpr Atom
    x, WellFormedSExpr Atom
    y ]
                  maybeS <- (WellFormedSExpr Atom
     -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> (Expr t (SemiRingBase sr) -> Memo t (WellFormedSExpr Atom))
    -> SemiRingProduct (Expr t) sr
    -> StateT (MemoEnv t) Identity (Maybe (WellFormedSExpr Atom))
    forall (m :: Type -> Type) r (f :: BaseType -> Type)
           (sr :: SemiRing).
    Monad m =>
    (r -> r -> m r)
    -> (f (SemiRingBase sr) -> m r)
    -> SemiRingProduct f sr
    -> m (Maybe r)
    WSum.prodEvalM WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall {m :: Type -> Type}.
    Monad m =>
    WellFormedSExpr Atom
    -> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
    pmul Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
    Expr t (SemiRingBase sr) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE SemiRingProduct (Expr t) sr
    pd
                  case maybeS of
                    Just WellFormedSExpr Atom
    s -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return WellFormedSExpr Atom
    s
                    Maybe (WellFormedSExpr Atom)
    Nothing -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Integer -> WellFormedSExpr Atom
    int Integer
    1
                SemiRingRepr sr
    W4.SemiRingRealRepr    -> String -> Memo t (WellFormedSExpr Atom)
    forall a. HasCallStack => String -> a
    error String
    "convertApp W4.SemiRingProd Real unsupported"

            go (W4.SemiRingLe OrderedSemiRingRepr sr
    sr Expr t (SemiRingBase sr)
    e1 Expr t (SemiRingBase sr)
    e2) = do
              s1 <- Expr t (SemiRingBase sr) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t (SemiRingBase sr)
    e1
              s2 <- goE e2
              case sr of
                OrderedSemiRingRepr sr
    W4.OrderedSemiRingIntegerRepr -> do
                  WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [ Text -> WellFormedSExpr Atom
    ident Text
    "intle", WellFormedSExpr Atom
    s1, WellFormedSExpr Atom
    s2]
                OrderedSemiRingRepr sr
    W4.OrderedSemiRingRealRepr -> String -> Memo t (WellFormedSExpr Atom)
    forall a. HasCallStack => String -> a
    error (String -> Memo t (WellFormedSExpr Atom))
    -> String -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ String
    "Printer: SemiRingLe is not supported for reals"

            go (W4.BVOrBits NatRepr w
    width BVOrSet (Expr t) w
    bs) = do
              let op :: WellFormedSExpr Atom
    op = Text -> WellFormedSExpr Atom
    ident Text
    "bvor"
              case BVOrSet (Expr t) w -> [Expr t ('BaseBVType w)]
    forall (e :: BaseType -> Type) (w :: Natural).
    BVOrSet e w -> [e (BaseBVType w)]
    W4.bvOrToList BVOrSet (Expr t) w
    bs of
                [] -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Natural -> Integer -> WellFormedSExpr Atom
    bitvec (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    NR.natValue NatRepr w
    width) Integer
    0
                (Expr t ('BaseBVType w)
    x:[Expr t ('BaseBVType w)]
    xs) -> do
                  e <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t ('BaseBVType w)
    x
                  let f = (\WellFormedSExpr Atom
    acc Expr t ('BaseBVType w)
    b -> do
                              b' <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t ('BaseBVType w)
    b
                              return $ S.L [op, b', acc])
                  M.foldM f e xs
            go (W4.BVUdiv NatRepr w
    _ Expr t ('BaseBVType w)
    e1 Expr t ('BaseBVType w)
    e2) = do
              s1 <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t ('BaseBVType w)
    e1
              s2 <- goE e2
              return $ S.L [ident "bvudiv", s1, s2]
            go (W4.BVUrem NatRepr w
    _ Expr t ('BaseBVType w)
    e1 Expr t ('BaseBVType w)
    e2) = do
              s1 <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t ('BaseBVType w)
    e1
              s2 <- goE e2
              return $ S.L [ident "bvurem", s1, s2]
            go (W4.BVSdiv NatRepr w
    _ Expr t ('BaseBVType w)
    e1 Expr t ('BaseBVType w)
    e2) = do
              s1 <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t ('BaseBVType w)
    e1
              s2 <- goE e2
              return $ S.L [ident "bvsdiv", s1, s2]
            go (W4.BVSrem NatRepr w
    _ Expr t ('BaseBVType w)
    e1 Expr t ('BaseBVType w)
    e2) = do
              s1 <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t ('BaseBVType w)
    e1
              s2 <- goE e2
              return $ S.L [ident "bvsrem", s1, s2]
            go (W4.BVShl NatRepr w
    _ Expr t ('BaseBVType w)
    e1 Expr t ('BaseBVType w)
    e2) = do
              s1 <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t ('BaseBVType w)
    e1
              s2 <- goE e2
              return $ S.L [ident "bvshl", s1, s2]
            go (W4.BVLshr NatRepr w
    _ Expr t ('BaseBVType w)
    e1 Expr t ('BaseBVType w)
    e2) = do
              s1 <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t ('BaseBVType w)
    e1
              s2 <- goE e2
              return $ S.L [ident "bvlshr", s1, s2]
            go (W4.BVAshr NatRepr w
    _ Expr t ('BaseBVType w)
    e1 Expr t ('BaseBVType w)
    e2) = do
              s1 <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t ('BaseBVType w)
    e1
              s2 <- goE e2
              return $ S.L [ident "bvashr", s1, s2]
            go (W4.BVZext NatRepr r
    r Expr t (BaseBVType w)
    e) = Text
    -> Integer
    -> Expr t (BaseBVType w)
    -> Memo t (WellFormedSExpr Atom)
    forall (w :: Natural).
    Text
    -> Integer
    -> Expr t (BaseBVType w)
    -> Memo t (WellFormedSExpr Atom)
    extend Text
    "zero" (NatRepr r -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue NatRepr r
    r) Expr t (BaseBVType w)
    e
            go (W4.BVSext NatRepr r
    r Expr t (BaseBVType w)
    e) = Text
    -> Integer
    -> Expr t (BaseBVType w)
    -> Memo t (WellFormedSExpr Atom)
    forall (w :: Natural).
    Text
    -> Integer
    -> Expr t (BaseBVType w)
    -> Memo t (WellFormedSExpr Atom)
    extend Text
    "sign" (NatRepr r -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue NatRepr r
    r) Expr t (BaseBVType w)
    e
            go (W4.BVFill NatRepr w
    r Expr t 'BaseBoolType
    e) = do
              s <- Expr t 'BaseBoolType -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t 'BaseBoolType
    e
              return $ S.L [ S.L [ident "_", ident "bvfill", int (intValue r)]
                           , s
                           ]

            go (W4.BVToInteger Expr t (BaseBVType w)
    e) = do
              s <- Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t (BaseBVType w)
    e
              return $ S.L [ident "bvToInteger", s]

            go (W4.SBVToInteger Expr t (BaseBVType w)
    e) = do
              s <- Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t (BaseBVType w)
    e
              return $ S.L [ident "sbvToInteger", s]

            go (W4.FloatNeg FloatPrecisionRepr fpp
    _repr Expr t ('BaseFloatType fpp)
    e) = do
              s <- Expr t ('BaseFloatType fpp) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t ('BaseFloatType fpp)
    e
              return $ S.L [ident "floatneg", s]
            go (W4.FloatAbs FloatPrecisionRepr fpp
    _repr Expr t ('BaseFloatType fpp)
    e) = do
              s <- Expr t ('BaseFloatType fpp) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t ('BaseFloatType fpp)
    e
              return $ S.L [ident "floatabs", s]

            go (W4.IntDiv Expr t 'BaseIntegerType
    e1 Expr t 'BaseIntegerType
    e2) = do
              s1 <- Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t 'BaseIntegerType
    e1
              s2 <- goE e2
              return $ S.L [ident "intdiv", s1, s2]
            go (W4.IntMod Expr t 'BaseIntegerType
    e1 Expr t 'BaseIntegerType
    e2) = do
              s1 <- Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t 'BaseIntegerType
    e1
              s2 <- goE e2
              return $ S.L [ident "intmod", s1, s2]
            go (W4.IntAbs Expr t 'BaseIntegerType
    e1) = do
              s1 <- Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t 'BaseIntegerType
    e1
              return $ S.L [ident "intabs", s1]
            go (W4.IntegerToBV Expr t 'BaseIntegerType
    e NatRepr w
    wRepr)  = do
              s <- Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t 'BaseIntegerType
    e
              return $ S.L [ident "integerToBV"
                            , nat $ natValue wRepr
                            , s]

            go (W4.StructCtor Assignment BaseTypeRepr flds
    _tps Assignment (Expr t) flds
    es) = do
              ss <- Assignment (Expr t) flds -> Memo t [WellFormedSExpr Atom]
    forall t (sh :: Ctx BaseType).
    Assignment (Expr t) sh -> Memo t [WellFormedSExpr Atom]
    convertExprAssignment Assignment (Expr t) flds
    es
              return $ S.L [ident "struct", S.L ss]
            go (W4.StructField Expr t (BaseStructType flds)
    e Index flds tp'
    ix BaseTypeRepr tp'
    _fieldTp) = do
              s <- Expr t (BaseStructType flds) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t (BaseStructType flds)
    e
              return $ S.L [ident "field"
                            , s
                            , int $ toInteger $ Ctx.indexVal ix
                            ]

            go (W4.UpdateArray BaseTypeRepr b
    _ Assignment BaseTypeRepr (i ::> tp1)
    _ Expr t ('BaseArrayType (i ::> tp1) b)
    e1 Assignment (Expr t) (i ::> tp1)
    es Expr t b
    e2) = do
              s1 <- Expr t ('BaseArrayType (i ::> tp1) b)
    -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t ('BaseArrayType (i ::> tp1) b)
    e1
              ss <- convertExprAssignment es
              s2 <- goE e2
              case ss of
                [WellFormedSExpr Atom
    idx] -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [ Text -> WellFormedSExpr Atom
    ident Text
    "updateArray", WellFormedSExpr Atom
    s1, WellFormedSExpr Atom
    idx, WellFormedSExpr Atom
    s2]
                [WellFormedSExpr Atom]
    _ -> String -> Memo t (WellFormedSExpr Atom)
    forall a. HasCallStack => String -> a
    error (String -> Memo t (WellFormedSExpr Atom))
    -> String -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ String
    "multidimensional arrays not supported"
            go (W4.SelectArray BaseTypeRepr tp'
    _ Expr t (BaseArrayType (i ::> tp1) tp')
    e Assignment (Expr t) (i ::> tp1)
    es) = do
              s <- Expr t (BaseArrayType (i ::> tp1) tp')
    -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t (BaseArrayType (i ::> tp1) tp')
    e
              ss <- convertExprAssignment es
              case ss of
                [WellFormedSExpr Atom
    idx] -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [ Text -> WellFormedSExpr Atom
    ident Text
    "select", WellFormedSExpr Atom
    s, WellFormedSExpr Atom
    idx]
                [WellFormedSExpr Atom]
    _ -> String -> Memo t (WellFormedSExpr Atom)
    forall a. HasCallStack => String -> a
    error (String -> Memo t (WellFormedSExpr Atom))
    -> String -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ String
    "multidimensional arrays not supported"

            go (W4.ArrayMap Assignment BaseTypeRepr (i ::> itp)
    _idxReprs BaseTypeRepr tp1
    _resRepr ArrayUpdateMap (Expr t) (i ::> itp) tp1
    updateMap Expr t ('BaseArrayType (i ::> itp) tp1)
    arr) = do
              updates <- ((Assignment IndexLit (i ::> itp), Expr t tp1)
     -> Memo t (WellFormedSExpr Atom))
    -> [(Assignment IndexLit (i ::> itp), Expr t tp1)]
    -> Memo t [WellFormedSExpr Atom]
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> [a] -> m [b]
    mapM (Assignment IndexLit (i ::> itp), Expr t tp1)
    -> Memo t (WellFormedSExpr Atom)
    forall (tp1 :: BaseType) (ctx :: Ctx BaseType).
    (Assignment IndexLit ctx, Expr t tp1)
    -> Memo t (WellFormedSExpr Atom)
    convertArrayUpdate (ArrayUpdateMap (Expr t) (i ::> itp) tp1
    -> [(Assignment IndexLit (i ::> itp), Expr t tp1)]
    forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
           (tp :: BaseType).
    ArrayUpdateMap e ctx tp -> [(Assignment IndexLit ctx, e tp)]
    WAU.toList ArrayUpdateMap (Expr t) (i ::> itp) tp1
    updateMap)
              arr' <- goE arr
              return $ S.L [ ident "arrayMap"
                           , S.L updates
                           , arr'
                           ]

            go App (Expr t) tp'
    app = String -> Memo t (WellFormedSExpr Atom)
    forall a. HasCallStack => String -> a
    error (String -> Memo t (WellFormedSExpr Atom))
    -> String -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ String
    "unhandled App: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ App (Expr t) tp' -> String
    forall a. Show a => a -> String
    show App (Expr t) tp'
    app

            convertArrayUpdate :: forall tp1 ctx . (Ctx.Assignment WIL.IndexLit ctx, W4.Expr t tp1) -> Memo t SExpr
            convertArrayUpdate :: forall (tp1 :: BaseType) (ctx :: Ctx BaseType).
    (Assignment IndexLit ctx, Expr t tp1)
    -> Memo t (WellFormedSExpr Atom)
    convertArrayUpdate (Assignment IndexLit ctx
    idxLits, Expr t tp1
    e) = do
              e' <- Expr t tp1 -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t tp1
    e
              return $ S.L [ S.L (FC.toListFC convertIndexLit idxLits)
                           , e'
                           ]

            -- -- -- -- Helper functions! -- -- -- --

            goE :: forall tp' . W4.Expr t tp' -> Memo t SExpr
            goE :: forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE = Expr t tp' -> Memo t (WellFormedSExpr Atom)
    forall t (tp :: BaseType).
    Expr t tp -> Memo t (WellFormedSExpr Atom)
    convertExpr

            extend :: forall w. Text -> Integer -> W4.Expr t (BaseBVType w) -> Memo t SExpr
            extend :: forall (w :: Natural).
    Text
    -> Integer
    -> Expr t (BaseBVType w)
    -> Memo t (WellFormedSExpr Atom)
    extend Text
    op Integer
    r Expr t (BaseBVType w)
    e = do
              let w :: Integer
    w = case Expr t (BaseBVType w) -> BaseTypeRepr (BaseBVType w)
    forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
    forall (e :: BaseType -> Type) (tp :: BaseType).
    IsExpr e =>
    e tp -> BaseTypeRepr tp
    W4.exprType Expr t (BaseBVType w)
    e of BaseBVRepr NatRepr w
    len -> NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue NatRepr w
    len
                  extension :: Integer
    extension = Integer
    r Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    w
              s <- Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t (BaseBVType w)
    e
              return $ S.L [ S.L [ ident "_", ident $ op <> "_extend", int extension ]
                            , s
                            ]

            extract :: forall tp'. Integer -> Integer -> W4.Expr t tp' -> Memo t SExpr
            extract :: forall (tp' :: BaseType).
    Integer -> Integer -> Expr t tp' -> Memo t (WellFormedSExpr Atom)
    extract Integer
    i Integer
    j Expr t tp'
    bv = do
              s <- Expr t tp' -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t tp'
    bv
              return $ S.L [ S.L [ ident "_", ident "extract", int i, int j ]
                            , s
                            ]

            convertBoolMap :: Text -> Bool -> BooM.BoolMap (W4.Expr t) -> Memo t SExpr
            convertBoolMap :: Text -> Bool -> BoolMap (Expr t) -> Memo t (WellFormedSExpr Atom)
    convertBoolMap Text
    op Bool
    base BoolMap (Expr t)
    bm =
              let strBase :: Bool -> WellFormedSExpr Atom
    strBase Bool
    b = if Bool
    b
                              then [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [Text -> WellFormedSExpr Atom
    ident Text
    "=", Natural -> Integer -> WellFormedSExpr Atom
    bitvec Natural
    1 Integer
    0, Natural -> Integer -> WellFormedSExpr Atom
    bitvec Natural
    1 Integer
    0]  -- true
                              else [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [Text -> WellFormedSExpr Atom
    ident Text
    "=", Natural -> Integer -> WellFormedSExpr Atom
    bitvec Natural
    1 Integer
    0, Natural -> Integer -> WellFormedSExpr Atom
    bitvec Natural
    1 Integer
    1]  -- false
                  strNotBase :: Bool -> WellFormedSExpr Atom
    strNotBase = Bool -> WellFormedSExpr Atom
    strBase (Bool -> WellFormedSExpr Atom)
    -> (Bool -> Bool) -> Bool -> WellFormedSExpr Atom
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    not
              in case BoolMap (Expr t) -> BoolMapView (Expr t)
    forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
    BooM.viewBoolMap BoolMap (Expr t)
    bm of
                   BoolMapView (Expr t)
    BooM.BoolMapUnit -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Bool -> WellFormedSExpr Atom
    strBase Bool
    base
                   BoolMapView (Expr t)
    BooM.BoolMapDualUnit -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ Bool -> WellFormedSExpr Atom
    strNotBase Bool
    base
                   BooM.BoolMapTerms NonEmpty (Expr t 'BaseBoolType, Polarity)
    ts ->
                     let onEach :: (Expr t 'BaseBoolType, Polarity)
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    onEach (Expr t 'BaseBoolType, Polarity)
    e WellFormedSExpr Atom
    r = do
                           s <- (Expr t 'BaseBoolType, Polarity) -> Memo t (WellFormedSExpr Atom)
    arg (Expr t 'BaseBoolType, Polarity)
    e
                           return $ S.L [ident op, s, r]
                         arg :: (Expr t 'BaseBoolType, Polarity) -> Memo t (WellFormedSExpr Atom)
    arg (Expr t 'BaseBoolType
    t, Polarity
    BooM.Positive) = Expr t 'BaseBoolType -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t 'BaseBoolType
    t
                         arg (Expr t 'BaseBoolType
    t, Polarity
    BooM.Negative) = do
                           s <- Expr t 'BaseBoolType -> Memo t (WellFormedSExpr Atom)
    forall (tp' :: BaseType).
    Expr t tp' -> Memo t (WellFormedSExpr Atom)
    goE Expr t 'BaseBoolType
    t
                           return $ S.L [ident "notp", s]
                     in ((Expr t 'BaseBoolType, Polarity)
     -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom
    -> NonEmpty (Expr t 'BaseBoolType, Polarity)
    -> Memo t (WellFormedSExpr Atom)
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Foldable t, Monad m) =>
    (a -> b -> m b) -> b -> t a -> m b
    F.foldrM (Expr t 'BaseBoolType, Polarity)
    -> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
    onEach (Bool -> WellFormedSExpr Atom
    strBase Bool
    base) NonEmpty (Expr t 'BaseBoolType, Polarity)
    ts

    convertIndexLit :: WIL.IndexLit tp -> SExpr
    convertIndexLit :: forall (x :: BaseType). IndexLit x -> WellFormedSExpr Atom
    convertIndexLit IndexLit tp
    il =
      case IndexLit tp
    il of
        WIL.IntIndexLit Integer
    iidx -> Integer -> WellFormedSExpr Atom
    int Integer
    iidx
        WIL.BVIndexLit NatRepr w
    irep BV w
    bvidx -> Natural -> Integer -> WellFormedSExpr Atom
    bitvec (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    irep) (BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    bvidx)

    convertExprAssignment ::
      Ctx.Assignment (W4.Expr t) sh
      -> Memo t [SExpr]
    convertExprAssignment :: forall t (sh :: Ctx BaseType).
    Assignment (Expr t) sh -> Memo t [WellFormedSExpr Atom]
    convertExprAssignment Assignment (Expr t) sh
    es =
      (Some (Expr t)
     -> StateT (MemoEnv t) Identity (WellFormedSExpr Atom))
    -> [Some (Expr t)]
    -> StateT (MemoEnv t) Identity [WellFormedSExpr Atom]
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> [a] -> m [b]
    mapM (\(Some Expr t x
    e) -> Expr t x -> StateT (MemoEnv t) Identity (WellFormedSExpr Atom)
    forall t (tp :: BaseType).
    Expr t tp -> Memo t (WellFormedSExpr Atom)
    convertExpr Expr t x
    e) ((forall (x :: BaseType). Expr t x -> Some (Expr t))
    -> forall (x :: Ctx BaseType).
       Assignment (Expr t) x -> [Some (Expr t)]
    forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
    FoldableFC t =>
    (forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
    forall (f :: BaseType -> Type) a.
    (forall (x :: BaseType). f x -> a)
    -> forall (x :: Ctx BaseType). Assignment f x -> [a]
    FC.toListFC Expr t x -> Some (Expr t)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    forall (x :: BaseType). Expr t x -> Some (Expr t)
    Some Assignment (Expr t) sh
    es)

    convertFnApp ::
      W4.ExprSymFn t args ret
      -> Ctx.Assignment (W4.Expr t) args
      -> Memo t SExpr
    convertFnApp :: forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret
    -> Assignment (Expr t) args -> Memo t (WellFormedSExpr Atom)
    convertFnApp ExprSymFn t args ret
    fn Assignment (Expr t) args
    args = do
      argSExprs <- Assignment (Expr t) args -> Memo t [WellFormedSExpr Atom]
    forall t (sh :: Ctx BaseType).
    Assignment (Expr t) sh -> Memo t [WellFormedSExpr Atom]
    convertExprAssignment Assignment (Expr t) args
    args
      fnEnv <- MS.gets envFreeSymFnEnv
      case OMap.lookup (SomeExprSymFn fn) fnEnv of
        Just Text
    fnName ->
          WellFormedSExpr Atom
    -> StateT (MemoEnv t) Identity (WellFormedSExpr Atom)
    forall a. a -> StateT (MemoEnv t) Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (WellFormedSExpr Atom
     -> StateT (MemoEnv t) Identity (WellFormedSExpr Atom))
    -> WellFormedSExpr Atom
    -> StateT (MemoEnv t) Identity (WellFormedSExpr Atom)
    forall a b. (a -> b) -> a -> b
    $ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L ([WellFormedSExpr Atom] -> WellFormedSExpr Atom)
    -> [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall a b. (a -> b) -> a -> b
    $ (Text -> WellFormedSExpr Atom
    ident Text
    "call")WellFormedSExpr Atom
    -> [WellFormedSExpr Atom] -> [WellFormedSExpr Atom]
    forall a. a -> [a] -> [a]
    :(Text -> WellFormedSExpr Atom
    ident Text
    fnName)WellFormedSExpr Atom
    -> [WellFormedSExpr Atom] -> [WellFormedSExpr Atom]
    forall a. a -> [a] -> [a]
    :[WellFormedSExpr Atom]
    argSExprs
        Maybe Text
    Nothing -> do
          varName <- ExprSymFn t args ret -> Memo t Text
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> Memo t Text
    freshFnName ExprSymFn t args ret
    fn
          MS.modify' $ (\MemoEnv t
    e -> MemoEnv t
    e {envFreeSymFnEnv =  fnEnv OMap.|> ((SomeExprSymFn fn), varName)})
          return $ S.L $ (ident "call"):(ident varName):argSExprs

    convertBaseType :: BaseTypeRepr tp -> SExpr
    convertBaseType :: forall (tp :: BaseType). BaseTypeRepr tp -> WellFormedSExpr Atom
    convertBaseType BaseTypeRepr tp
    tp = case BaseTypeRepr tp
    tp of
      BaseTypeRepr tp
    W4.BaseBoolRepr -> Atom -> WellFormedSExpr Atom
    forall t. t -> WellFormedSExpr t
    S.A (Atom -> WellFormedSExpr Atom) -> Atom -> WellFormedSExpr Atom
    forall a b. (a -> b) -> a -> b
    $ Text -> Atom
    AId Text
    "Bool"
      BaseTypeRepr tp
    W4.BaseIntegerRepr -> Atom -> WellFormedSExpr Atom
    forall t. t -> WellFormedSExpr t
    S.A (Atom -> WellFormedSExpr Atom) -> Atom -> WellFormedSExpr Atom
    forall a b. (a -> b) -> a -> b
    $ Text -> Atom
    AId Text
    "Int"
      BaseTypeRepr tp
    W4.BaseRealRepr -> Atom -> WellFormedSExpr Atom
    forall t. t -> WellFormedSExpr t
    S.A (Atom -> WellFormedSExpr Atom) -> Atom -> WellFormedSExpr Atom
    forall a b. (a -> b) -> a -> b
    $ Text -> Atom
    AId Text
    "Real"
      W4.BaseStringRepr StringInfoRepr si
    si -> [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [Atom -> WellFormedSExpr Atom
    forall t. t -> WellFormedSExpr t
    S.A (Atom -> WellFormedSExpr Atom) -> Atom -> WellFormedSExpr Atom
    forall a b. (a -> b) -> a -> b
    $ Text -> Atom
    AId Text
    "String", StringInfoRepr si -> WellFormedSExpr Atom
    forall (si :: StringInfo).
    StringInfoRepr si -> WellFormedSExpr Atom
    convertStringInfo StringInfoRepr si
    si]
      BaseTypeRepr tp
    W4.BaseComplexRepr -> Atom -> WellFormedSExpr Atom
    forall t. t -> WellFormedSExpr t
    S.A (Atom -> WellFormedSExpr Atom) -> Atom -> WellFormedSExpr Atom
    forall a b. (a -> b) -> a -> b
    $ Text -> Atom
    AId Text
    "Complex"
      W4.BaseBVRepr NatRepr w
    wRepr -> [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [Atom -> WellFormedSExpr Atom
    forall t. t -> WellFormedSExpr t
    S.A (Text -> Atom
    AId Text
    "BV"), Atom -> WellFormedSExpr Atom
    forall t. t -> WellFormedSExpr t
    S.A (Integer -> Atom
    AInt (NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    NR.intValue NatRepr w
    wRepr)) ]
      W4.BaseStructRepr Assignment BaseTypeRepr ctx
    tps -> [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [ Atom -> WellFormedSExpr Atom
    forall t. t -> WellFormedSExpr t
    S.A (Text -> Atom
    AId Text
    "Struct"), [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L (Assignment BaseTypeRepr ctx -> [WellFormedSExpr Atom]
    forall (tps :: Ctx BaseType).
    Assignment BaseTypeRepr tps -> [WellFormedSExpr Atom]
    convertBaseTypes Assignment BaseTypeRepr ctx
    tps) ]
      W4.BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
    ixs BaseTypeRepr xs
    repr -> [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [Atom -> WellFormedSExpr Atom
    forall t. t -> WellFormedSExpr t
    S.A (Text -> Atom
    AId Text
    "Array"), [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L ([WellFormedSExpr Atom] -> WellFormedSExpr Atom)
    -> [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall a b. (a -> b) -> a -> b
    $ Assignment BaseTypeRepr (idx ::> tp) -> [WellFormedSExpr Atom]
    forall (tps :: Ctx BaseType).
    Assignment BaseTypeRepr tps -> [WellFormedSExpr Atom]
    convertBaseTypes Assignment BaseTypeRepr (idx ::> tp)
    ixs , BaseTypeRepr xs -> WellFormedSExpr Atom
    forall (tp :: BaseType). BaseTypeRepr tp -> WellFormedSExpr Atom
    convertBaseType BaseTypeRepr xs
    repr]
      W4.BaseFloatRepr (W4.FloatingPointPrecisionRepr NatRepr eb
    eRepr NatRepr sb
    sRepr) ->
        [WellFormedSExpr Atom] -> WellFormedSExpr Atom
    forall t. [WellFormedSExpr t] -> WellFormedSExpr t
    S.L [ Atom -> WellFormedSExpr Atom
    forall t. t -> WellFormedSExpr t
    S.A (Text -> Atom
    AId Text
    "Float"), Atom -> WellFormedSExpr Atom
    forall t. t -> WellFormedSExpr t
    S.A (Integer -> Atom
    AInt (NatRepr eb -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    NR.intValue NatRepr eb
    eRepr)), Atom -> WellFormedSExpr Atom
    forall t. t -> WellFormedSExpr t
    S.A (Integer -> Atom
    AInt (NatRepr sb -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    NR.intValue NatRepr sb
    sRepr)) ]

    convertStringInfo :: StringInfoRepr si -> SExpr
    convertStringInfo :: forall (si :: StringInfo).
    StringInfoRepr si -> WellFormedSExpr Atom
    convertStringInfo StringInfoRepr si
    W4.Char8Repr = Text -> WellFormedSExpr Atom
    ident Text
    "Char8"
    convertStringInfo StringInfoRepr si
    W4.Char16Repr = Text -> WellFormedSExpr Atom
    ident Text
    "Char16"
    convertStringInfo StringInfoRepr si
    W4.UnicodeRepr = Text -> WellFormedSExpr Atom
    ident Text
    "Unicode"

    -- | Convert an Assignment of base types into a list of base
    -- types SExpr, where the left-to-right syntactic ordering
    -- of the types is maintained.
    convertBaseTypes ::
      Ctx.Assignment BaseTypeRepr tps
      -> [SExpr]
    convertBaseTypes :: forall (tps :: Ctx BaseType).
    Assignment BaseTypeRepr tps -> [WellFormedSExpr Atom]
    convertBaseTypes Assignment BaseTypeRepr tps
    asn = (forall (tp :: BaseType). BaseTypeRepr tp -> WellFormedSExpr Atom)
    -> forall (tps :: Ctx BaseType).
       Assignment BaseTypeRepr tps -> [WellFormedSExpr Atom]
    forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
    FoldableFC t =>
    (forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
    forall (f :: BaseType -> Type) a.
    (forall (x :: BaseType). f x -> a)
    -> forall (x :: Ctx BaseType). Assignment f x -> [a]
    FC.toListFC BaseTypeRepr x -> WellFormedSExpr Atom
    forall (tp :: BaseType). BaseTypeRepr tp -> WellFormedSExpr Atom
    convertBaseType Assignment BaseTypeRepr tps
    asn