{-# 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.
      [(SomeExprSymFn t, Text)]
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 [(SomeExprSymFn t, Text)] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [(SomeExprSymFn t, Text)]
newFns
        then if [(Text, WellFormedSExpr Atom)] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [(Text, WellFormedSExpr Atom)]
fnBindings
             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 WellFormedSExpr Atom
sexpr
             else let bs :: [WellFormedSExpr Atom]
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 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
"letfn" , [WellFormedSExpr Atom] -> WellFormedSExpr Atom
forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [WellFormedSExpr Atom]
bs, WellFormedSExpr Atom
sexpr]
        else [(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 [(SomeExprSymFn t, Text)]
newFns [(Text, WellFormedSExpr Atom)]
fnBindings Set Text
seen
    go (((SomeExprSymFn ExprSymFn t dom ret
nextFn), Text
nextFnName):[(SomeExprSymFn t, Text)]
todo) [(Text, WellFormedSExpr Atom)]
fnBindings Set Text
seen = do
      WellFormedSExpr Atom
nextSExpr <- 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
nextFn
      let fnBindings' :: [(Text, WellFormedSExpr Atom)]
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' :: Set Text
seen' = Text -> Set Text -> Set Text
forall a. Ord a => a -> Set a -> Set a
Set.insert Text
nextFnName Set Text
seen
      [(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 [(SomeExprSymFn t, Text)]
todo [(Text, WellFormedSExpr Atom)]
fnBindings' Set Text
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
  WellFormedSExpr Atom
b <- Expr t tp -> Memo t (WellFormedSExpr Atom)
forall t (tp :: BaseType).
Expr t tp -> Memo t (WellFormedSExpr Atom)
convertExpr Expr t tp
expr
  [WellFormedSExpr Atom]
bs <- ((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])
-> ([(SKey, (Text, WellFormedSExpr Atom))]
    -> [(Text, WellFormedSExpr Atom)])
-> [(SKey, (Text, WellFormedSExpr Atom))]
-> [WellFormedSExpr Atom]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f 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))] -> [WellFormedSExpr Atom])
-> (OMap SKey (Text, WellFormedSExpr Atom)
    -> [(SKey, (Text, WellFormedSExpr Atom))])
-> OMap SKey (Text, WellFormedSExpr Atom)
-> [WellFormedSExpr Atom]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f 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) -> [WellFormedSExpr Atom])
-> StateT
     (MemoEnv t) Identity (OMap SKey (Text, WellFormedSExpr Atom))
-> StateT (MemoEnv t) Identity [WellFormedSExpr Atom]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (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
  (MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
MS.modify' (\MemoEnv t
r -> MemoEnv t
r {envLetBindings = OMap.empty})
  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 -> WellFormedSExpr Atom
mkLet [WellFormedSExpr Atom]
bs WellFormedSExpr Atom
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)
     [(Some (ExprBoundVar t), Text)]
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 ([Some (ExprBoundVar t)]
origBoundVars, [Text]
freshArgNames) = [(Some (ExprBoundVar t), Text)]
-> ([Some (ExprBoundVar t)], [Text])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Some (ExprBoundVar t), Text)]
argsWithFreshNames
     -- Convert the body with the bound variable set and
     -- free-variable mapping extended to reflect being
     -- under the function's binders.
     WellFormedSExpr Atom
sExpr <- (MemoEnv t -> MemoEnv t)
-> Memo t (WellFormedSExpr Atom) -> Memo t (WellFormedSExpr Atom)
forall s a. (s -> s) -> State s a -> State s a
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)})
              (Memo t (WellFormedSExpr Atom) -> Memo t (WellFormedSExpr Atom))
-> Memo t (WellFormedSExpr Atom) -> Memo t (WellFormedSExpr Atom)
forall a b. (a -> b) -> a -> b
$ Expr t ret -> Memo t (WellFormedSExpr Atom)
forall t (tp :: BaseType).
Expr t tp -> Memo t (WellFormedSExpr Atom)
convertExprWithLet Expr t ret
body
     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
"definedfn"
                  , 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])
                  , [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) -> [Text] -> [WellFormedSExpr Atom]
forall a b. (a -> b) -> [a] -> [b]
map Text -> WellFormedSExpr Atom
ident [Text]
freshArgNames
                  , WellFormedSExpr Atom
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
      Text
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)
      (Some (ExprBoundVar t), Text)
-> StateT (MemoEnv t) Identity (Some (ExprBoundVar t), Text)
forall a. a -> StateT (MemoEnv t) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some (ExprBoundVar t)
someVar, Text
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
  Natural
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
  (MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
MS.modify' ((MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ())
-> (MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ()
forall a b. (a -> b) -> a -> b
$ (\MemoEnv t
e -> MemoEnv t
e {envIdCounter = idCount + 1})
  let prefix :: String
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"
  Text -> Memo t Text
forall a. a -> StateT (MemoEnv t) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text -> Memo t Text) -> Text -> Memo t Text
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
prefixString -> ShowS
forall a. [a] -> [a] -> [a]
++(Natural -> String
forall a. Show a => a -> String
show (Natural -> String) -> Natural -> String
forall a b. (a -> b) -> a -> b
$ Natural
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
  Natural
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
  (MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
MS.modify' ((MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ())
-> (MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ()
forall a b. (a -> b) -> a -> b
$ (\MemoEnv t
e -> MemoEnv t
e {envIdCounter = idCount + 1})
  let prefix :: String
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"
  Text -> Memo t Text
forall a. a -> StateT (MemoEnv t) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text -> Memo t Text) -> Text -> Memo t Text
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
prefixString -> ShowS
forall a. [a] -> [a] -> [a]
++(Natural -> String
forall a. Show a => a -> String
show (Natural -> String) -> Natural -> String
forall a b. (a -> b) -> a -> b
$ Natural
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
  Text
letVarName <- BaseTypeRepr tp -> Memo t Text
forall (tp :: BaseType) t. BaseTypeRepr tp -> Memo t Text
freshName BaseTypeRepr tp
tp
  OMap SKey (Text, WellFormedSExpr Atom)
curLetBindings <- (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
  (MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
MS.modify' ((MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ())
-> (MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ()
forall a b. (a -> b) -> a -> b
$ (\MemoEnv t
e -> MemoEnv t
e {envLetBindings =  curLetBindings OMap.|> (key, (letVarName, sexp))})
  Text -> Memo t Text
forall a. a -> StateT (MemoEnv t) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Text
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
      OMap SKey (Text, WellFormedSExpr Atom)
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 SKey
-> OMap SKey (Text, WellFormedSExpr Atom)
-> Maybe (Text, WellFormedSExpr Atom)
forall k v. Ord k => k -> OMap k v -> Maybe v
OMap.lookup SKey
key OMap SKey (Text, WellFormedSExpr Atom)
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
          WellFormedSExpr Atom
sexp <- Expr t tp -> Memo t (WellFormedSExpr Atom)
go Expr t tp
initialExpr
          case WellFormedSExpr Atom
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
              Text
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)
              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
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
  Bool
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)
  Set (Some (ExprBoundVar t))
bvs <- (MemoEnv t -> Set (Some (ExprBoundVar t)))
-> StateT (MemoEnv t) Identity (Set (Some (ExprBoundVar t)))
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
MS.gets MemoEnv t -> Set (Some (ExprBoundVar t))
forall t. MemoEnv t -> Set (Some (ExprBoundVar t))
envBoundVars
  -- If this variable is not bound (in the standard syntactic sense)
  -- and free variables are not explicitly permitted, raise an error.
  Bool
-> StateT (MemoEnv t) Identity () -> StateT (MemoEnv t) Identity ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
M.when ((Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Some (ExprBoundVar t) -> Set (Some (ExprBoundVar t)) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (ExprBoundVar t tp -> Some (ExprBoundVar t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some ExprBoundVar t tp
x) Set (Some (ExprBoundVar t))
bvs) Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
fvsAllowed)) (StateT (MemoEnv t) Identity () -> StateT (MemoEnv t) Identity ())
-> StateT (MemoEnv t) Identity () -> StateT (MemoEnv t) Identity ()
forall a b. (a -> b) -> a -> b
$
    String -> StateT (MemoEnv t) Identity ()
forall a. HasCallStack => String -> a
error (String -> StateT (MemoEnv t) Identity ())
-> String -> StateT (MemoEnv t) Identity ()
forall a b. (a -> b) -> a -> b
$
    String
"encountered the free What4 ExprBoundVar `"
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (SolverSymbol -> Text
W4.solverSymbolAsText (ExprBoundVar t tp -> SolverSymbol
forall t (tp :: BaseType). ExprBoundVar t tp -> SolverSymbol
W4.bvarName ExprBoundVar t tp
x)))
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`, 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.
  VarNameEnv t
varEnv <- (MemoEnv t -> VarNameEnv t)
-> StateT (MemoEnv t) Identity (VarNameEnv t)
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
MS.gets MemoEnv t -> VarNameEnv t
forall t. MemoEnv t -> VarNameEnv t
envFreeVarEnv
  case Some (ExprBoundVar t) -> VarNameEnv t -> Maybe Text
forall k v. Ord k => k -> OMap k v -> Maybe v
OMap.lookup (ExprBoundVar t tp -> Some (ExprBoundVar t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some ExprBoundVar t tp
x) VarNameEnv t
varEnv of
    Just Text
var -> 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
var
    Maybe Text
Nothing -> do
      Text
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
      (MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
MS.modify' ((MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ())
-> (MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ()
forall a b. (a -> b) -> a -> b
$ (\MemoEnv t
e -> MemoEnv t
e {envFreeVarEnv = varEnv OMap.|> ((Some x), varName)})
      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
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
          WellFormedSExpr Atom
s1 <- Expr t 'BaseBoolType -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseBoolType
e1
          WellFormedSExpr Atom
s2 <- Expr t tp' -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t tp'
e2
          WellFormedSExpr Atom
s3 <- Expr t tp' -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t tp'
e3
          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
"ite", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2, WellFormedSExpr Atom
s3]
        go (W4.BaseEq BaseTypeRepr tp1
_bt Expr t tp1
e1 Expr t tp1
e2) = do
          WellFormedSExpr Atom
s1 <- Expr t tp1 -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t tp1
e1
          WellFormedSExpr Atom
s2 <- Expr t tp1 -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t tp1
e2
          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
"=", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.NotPred Expr t 'BaseBoolType
e) = do
          WellFormedSExpr Atom
s <- Expr t 'BaseBoolType -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseBoolType
e
          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
"notp", WellFormedSExpr Atom
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
          WellFormedSExpr Atom
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
          WellFormedSExpr Atom
s2 <- Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t (BaseBVType w)
e2
          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
"bvslt", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.BVUlt Expr t (BaseBVType w)
e1 Expr t (BaseBVType w)
e2) = do
          WellFormedSExpr Atom
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
          WellFormedSExpr Atom
s2 <- Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t (BaseBVType w)
e2
          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
"bvult", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.BVConcat NatRepr (u + v)
_ Expr t (BaseBVType u)
e1 Expr t (BaseBVType v)
e2) = do
          WellFormedSExpr Atom
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
          WellFormedSExpr Atom
s2 <- Expr t (BaseBVType v) -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t (BaseBVType v)
e2
          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
"concat", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
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
                    WellFormedSExpr Atom
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
                    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
"bvmul", 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
mul), WellFormedSExpr Atom
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
                    WellFormedSExpr Atom
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
                    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
"bvand", 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
mul), WellFormedSExpr Atom
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
                    WellFormedSExpr Atom
s <- Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseIntegerType
e
                    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
"intmul", Integer -> WellFormedSExpr Atom
int Integer
mul, WellFormedSExpr Atom
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 ]
              Maybe (WellFormedSExpr Atom)
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 Maybe (WellFormedSExpr Atom)
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 ]
              Maybe (WellFormedSExpr Atom)
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 Maybe (WellFormedSExpr Atom)
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 ]
              Maybe (WellFormedSExpr Atom)
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 Maybe (WellFormedSExpr Atom)
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
          WellFormedSExpr Atom
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
          WellFormedSExpr Atom
s2 <- Expr t (SemiRingBase sr) -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t (SemiRingBase sr)
e2
          case OrderedSemiRingRepr sr
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
              WellFormedSExpr Atom
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
-> Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
f = (\WellFormedSExpr Atom
acc Expr t ('BaseBVType w)
b -> do
                          WellFormedSExpr Atom
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
                          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 [WellFormedSExpr Atom
op, WellFormedSExpr Atom
b', WellFormedSExpr Atom
acc])
              (WellFormedSExpr Atom
 -> Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom))
-> WellFormedSExpr Atom
-> [Expr t ('BaseBVType w)]
-> Memo t (WellFormedSExpr Atom)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
M.foldM WellFormedSExpr Atom
-> Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
f WellFormedSExpr Atom
e [Expr t ('BaseBVType w)]
xs
        go (W4.BVUdiv NatRepr w
_ Expr t ('BaseBVType w)
e1 Expr t ('BaseBVType w)
e2) = do
          WellFormedSExpr Atom
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
          WellFormedSExpr Atom
s2 <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t ('BaseBVType w)
e2
          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
"bvudiv", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.BVUrem NatRepr w
_ Expr t ('BaseBVType w)
e1 Expr t ('BaseBVType w)
e2) = do
          WellFormedSExpr Atom
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
          WellFormedSExpr Atom
s2 <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t ('BaseBVType w)
e2
          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
"bvurem", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.BVSdiv NatRepr w
_ Expr t ('BaseBVType w)
e1 Expr t ('BaseBVType w)
e2) = do
          WellFormedSExpr Atom
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
          WellFormedSExpr Atom
s2 <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t ('BaseBVType w)
e2
          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
"bvsdiv", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.BVSrem NatRepr w
_ Expr t ('BaseBVType w)
e1 Expr t ('BaseBVType w)
e2) = do
          WellFormedSExpr Atom
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
          WellFormedSExpr Atom
s2 <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t ('BaseBVType w)
e2
          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
"bvsrem", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.BVShl NatRepr w
_ Expr t ('BaseBVType w)
e1 Expr t ('BaseBVType w)
e2) = do
          WellFormedSExpr Atom
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
          WellFormedSExpr Atom
s2 <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t ('BaseBVType w)
e2
          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
"bvshl", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.BVLshr NatRepr w
_ Expr t ('BaseBVType w)
e1 Expr t ('BaseBVType w)
e2) = do
          WellFormedSExpr Atom
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
          WellFormedSExpr Atom
s2 <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t ('BaseBVType w)
e2
          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
"bvlshr", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.BVAshr NatRepr w
_ Expr t ('BaseBVType w)
e1 Expr t ('BaseBVType w)
e2) = do
          WellFormedSExpr Atom
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
          WellFormedSExpr Atom
s2 <- Expr t ('BaseBVType w) -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t ('BaseBVType w)
e2
          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
"bvashr", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
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
          WellFormedSExpr Atom
s <- Expr t 'BaseBoolType -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseBoolType
e
          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 [ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [Text -> WellFormedSExpr Atom
ident Text
"_", Text -> WellFormedSExpr Atom
ident Text
"bvfill", Integer -> WellFormedSExpr Atom
int (NatRepr w -> Integer
forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr w
r)]
                       , WellFormedSExpr Atom
s
                       ]

        go (W4.BVToInteger Expr t (BaseBVType w)
e) = do
          WellFormedSExpr Atom
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
          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
"bvToInteger", WellFormedSExpr Atom
s]

        go (W4.SBVToInteger Expr t (BaseBVType w)
e) = do
          WellFormedSExpr Atom
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
          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
"sbvToInteger", WellFormedSExpr Atom
s]

        go (W4.FloatNeg FloatPrecisionRepr fpp
_repr Expr t ('BaseFloatType fpp)
e) = do
          WellFormedSExpr Atom
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
          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
"floatneg", WellFormedSExpr Atom
s]
        go (W4.FloatAbs FloatPrecisionRepr fpp
_repr Expr t ('BaseFloatType fpp)
e) = do
          WellFormedSExpr Atom
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
          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
"floatabs", WellFormedSExpr Atom
s]

        go (W4.IntDiv Expr t 'BaseIntegerType
e1 Expr t 'BaseIntegerType
e2) = do
          WellFormedSExpr Atom
s1 <- Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseIntegerType
e1
          WellFormedSExpr Atom
s2 <- Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseIntegerType
e2
          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
"intdiv", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.IntMod Expr t 'BaseIntegerType
e1 Expr t 'BaseIntegerType
e2) = do
          WellFormedSExpr Atom
s1 <- Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseIntegerType
e1
          WellFormedSExpr Atom
s2 <- Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseIntegerType
e2
          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
"intmod", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.IntAbs Expr t 'BaseIntegerType
e1) = do
          WellFormedSExpr Atom
s1 <- Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseIntegerType
e1
          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
"intabs", WellFormedSExpr Atom
s1]
        go (W4.IntegerToBV Expr t 'BaseIntegerType
e NatRepr w
wRepr)  = do
          WellFormedSExpr Atom
s <- Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseIntegerType
e
          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
"integerToBV"
                        , Natural -> WellFormedSExpr Atom
nat (Natural -> WellFormedSExpr Atom)
-> Natural -> WellFormedSExpr Atom
forall a b. (a -> b) -> a -> b
$ NatRepr w -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
wRepr
                        , WellFormedSExpr Atom
s]

        go (W4.StructCtor Assignment BaseTypeRepr flds
_tps Assignment (Expr t) flds
es) = do
          [WellFormedSExpr Atom]
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
          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
"struct", [WellFormedSExpr Atom] -> WellFormedSExpr Atom
forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [WellFormedSExpr Atom]
ss]
        go (W4.StructField Expr t (BaseStructType flds)
e Index flds tp'
ix BaseTypeRepr tp'
_fieldTp) = do
          WellFormedSExpr Atom
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
          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
"field"
                        , WellFormedSExpr Atom
s
                        , Integer -> WellFormedSExpr Atom
int (Integer -> WellFormedSExpr Atom)
-> Integer -> WellFormedSExpr Atom
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Index flds tp' -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal Index flds tp'
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
          WellFormedSExpr Atom
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
          [WellFormedSExpr Atom]
ss <- Assignment (Expr t) (i ::> tp1) -> Memo t [WellFormedSExpr Atom]
forall t (sh :: Ctx BaseType).
Assignment (Expr t) sh -> Memo t [WellFormedSExpr Atom]
convertExprAssignment Assignment (Expr t) (i ::> tp1)
es
          WellFormedSExpr Atom
s2 <- Expr t b -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t b
e2
          case [WellFormedSExpr Atom]
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
          WellFormedSExpr Atom
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
          [WellFormedSExpr Atom]
ss <- Assignment (Expr t) (i ::> tp1) -> Memo t [WellFormedSExpr Atom]
forall t (sh :: Ctx BaseType).
Assignment (Expr t) sh -> Memo t [WellFormedSExpr Atom]
convertExprAssignment Assignment (Expr t) (i ::> tp1)
es
          case [WellFormedSExpr Atom]
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
          [WellFormedSExpr Atom]
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)
          WellFormedSExpr Atom
arr' <- Expr t ('BaseArrayType (i ::> itp) tp1)
-> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t ('BaseArrayType (i ::> itp) tp1)
arr
          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
"arrayMap"
                       , [WellFormedSExpr Atom] -> WellFormedSExpr Atom
forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [WellFormedSExpr Atom]
updates
                       , WellFormedSExpr Atom
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
          WellFormedSExpr Atom
e' <- Expr t tp1 -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t tp1
e
          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 [ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L ((forall (x :: BaseType). IndexLit x -> WellFormedSExpr Atom)
-> forall (x :: Ctx BaseType).
   Assignment IndexLit x -> [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 IndexLit x -> WellFormedSExpr Atom
forall (x :: BaseType). IndexLit x -> WellFormedSExpr Atom
convertIndexLit Assignment IndexLit ctx
idxLits)
                       , WellFormedSExpr Atom
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
          WellFormedSExpr Atom
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
          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 [ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [ Text -> WellFormedSExpr Atom
ident Text
"_", Text -> WellFormedSExpr Atom
ident (Text -> WellFormedSExpr Atom) -> Text -> WellFormedSExpr Atom
forall a b. (a -> b) -> a -> b
$ Text
op Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_extend", Integer -> WellFormedSExpr Atom
int Integer
extension ]
                        , WellFormedSExpr Atom
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
          WellFormedSExpr Atom
s <- Expr t tp' -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t tp'
bv
          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 [ [WellFormedSExpr Atom] -> WellFormedSExpr Atom
forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [ Text -> WellFormedSExpr Atom
ident Text
"_", Text -> WellFormedSExpr Atom
ident Text
"extract", Integer -> WellFormedSExpr Atom
int Integer
i, Integer -> WellFormedSExpr Atom
int Integer
j ]
                        , WellFormedSExpr Atom
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
                       WellFormedSExpr Atom
s <- (Expr t 'BaseBoolType, Polarity) -> Memo t (WellFormedSExpr Atom)
arg (Expr t 'BaseBoolType, Polarity)
e
                       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
op, WellFormedSExpr Atom
s, WellFormedSExpr Atom
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
                       WellFormedSExpr Atom
s <- Expr t 'BaseBoolType -> Memo t (WellFormedSExpr Atom)
forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseBoolType
t
                       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
"notp", WellFormedSExpr Atom
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
  [WellFormedSExpr Atom]
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
  FnNameEnv t
fnEnv <- (MemoEnv t -> FnNameEnv t)
-> StateT (MemoEnv t) Identity (FnNameEnv t)
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
MS.gets MemoEnv t -> FnNameEnv t
forall t. MemoEnv t -> FnNameEnv t
envFreeSymFnEnv
  case SomeExprSymFn t -> FnNameEnv t -> Maybe Text
forall k v. Ord k => k -> OMap k v -> Maybe v
OMap.lookup (ExprSymFn t args ret -> SomeExprSymFn t
forall t (dom :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t dom ret -> SomeExprSymFn t
SomeExprSymFn ExprSymFn t args ret
fn) FnNameEnv t
fnEnv of
    Just Text
fnName ->
      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 ([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
      Text
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
      (MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
MS.modify' ((MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ())
-> (MemoEnv t -> MemoEnv t) -> StateT (MemoEnv t) Identity ()
forall a b. (a -> b) -> a -> b
$ (\MemoEnv t
e -> MemoEnv t
e {envFreeSymFnEnv =  fnEnv OMap.|> ((SomeExprSymFn fn), varName)})
      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 ([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
varName)WellFormedSExpr Atom
-> [WellFormedSExpr Atom] -> [WellFormedSExpr Atom]
forall a. a -> [a] -> [a]
:[WellFormedSExpr Atom]
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