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

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

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

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

import qualified Data.SCargot.Repr.WellFormed as S

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


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

type SExpr = S.WellFormedSExpr Atom

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

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

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


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


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

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

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

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

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


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

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

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

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

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


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

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


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

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

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

type Memo t a = State (MemoEnv t) a

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


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


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

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


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


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



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

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



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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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



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

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