{-# 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 forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Nonce t (args ::> ret)
W4.symFnId ExprSymFn t dom ret
fn1) (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) =
    forall a. Ord a => a -> a -> Ordering
compare (forall k s (tp :: k). Nonce s tp -> Word64
Nonce.indexValue forall a b. (a -> b) -> a -> b
$ forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Nonce t (args ::> ret)
W4.symFnId ExprSymFn t dom ret
fn1) (forall k s (tp :: k). Nonce s tp -> Word64
Nonce.indexValue forall a b. (a -> b) -> a -> b
$ 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) = 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 = forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t. (Some (ExprBoundVar t), Text) -> (String, String, String)
toStr [(Some (ExprBoundVar t), Text)]
entries
  where entries :: [(Some (ExprBoundVar t), Text)]
entries = 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 forall a b. (a -> b) -> a -> b
$ SolverSymbol -> Text
W4.solverSymbolAsText forall a b. (a -> b) -> a -> b
$ forall t (tp :: BaseType). ExprBoundVar t tp -> SolverSymbol
W4.bvarName ExprBoundVar t x
var
                                      , forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t. (SomeExprSymFn t, Text) -> (String, String, String)
toStr [(SomeExprSymFn t, Text)]
entries
  where entries :: [(SomeExprSymFn t, Text)]
entries = 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 forall a b. (a -> b) -> a -> b
$ SolverSymbol -> Text
W4.solverSymbolAsText forall a b. (a -> b) -> a -> b
$ forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SolverSymbol
W4.symFnName ExprSymFn t dom ret
fn
                                              , forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ 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 = forall t. Result t -> WellFormedSExpr Atom
resSExpr forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 = forall t. Config -> Memo t (WellFormedSExpr Atom) -> Result t
serializeSomething Config
cfg (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 = forall t. Result t -> WellFormedSExpr Atom
resSExpr forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 = forall t. Config -> Memo t (WellFormedSExpr Atom) -> Result t
serializeSomething Config
cfg (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 (forall (m :: Type -> Type) a. Monad m => a -> m a
return, forall t. MemoEnv t -> FnNameEnv t
envFreeSymFnEnv)
                                      else (forall t. WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
letFn, \MemoEnv t
_ -> forall k v. OMap k v
OMap.empty)
      (WellFormedSExpr Atom
sexpr, MemoEnv t
menv) = forall t a. Config -> Memo t a -> (a, MemoEnv t)
runMemo Config
cfg forall a b. (a -> b) -> a -> b
$ Memo t (WellFormedSExpr Atom)
something 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 = forall a b. (a -> b) -> [a] -> [b]
map (\(Text
varName, WellFormedSExpr Atom
boundExpr) -> forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [ Text -> WellFormedSExpr Atom
ident Text
varName, WellFormedSExpr Atom
boundExpr ])
                    forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd
                    forall a b. (a -> b) -> a -> b
$ forall k v. OMap k v -> [(k, v)]
OMap.assocs
                    forall a b. (a -> b) -> a -> b
$ 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 = 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 = 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 = forall k v. OMap k v
OMap.empty
                      , envFreeVarEnv :: VarNameEnv t
envFreeVarEnv = forall k v. OMap k v
OMap.empty
                      , envFreeSymFnEnv :: FnNameEnv t
envFreeSymFnEnv = forall k v. OMap k v
OMap.empty
                      , envBoundVars :: Set (Some (ExprBoundVar t))
envBoundVars = 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 = forall s a. State s a -> s -> (a, s)
MS.runState Memo t a
m forall a b. (a -> b) -> a -> b
$ 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 = forall t.
[(SomeExprSymFn t, Text)]
-> [(Text, WellFormedSExpr Atom)]
-> Set Text
-> Memo t (WellFormedSExpr Atom)
go [] [] forall a. Set a
Set.empty
  where
    go :: [((SomeExprSymFn t), Text)] -> [(Text, SExpr)] -> Set Text ->  Memo t SExpr
    go :: forall t.
[(SomeExprSymFn t, Text)]
-> [(Text, WellFormedSExpr Atom)]
-> Set Text
-> Memo t (WellFormedSExpr Atom)
go [] [(Text, WellFormedSExpr Atom)]
fnBindings Set Text
seen = do
      -- Although the `todo` list is empty, we may have
      -- encountered some SymFns along the way, so check for
      -- those and serialize any previously unseen SymFns.
      [(SomeExprSymFn t, Text)]
newFns <- forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
MS.gets (forall a. (a -> Bool) -> [a] -> [a]
filter (\(SomeExprSymFn t
_symFn, Text
varName) -> Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Bool
Set.member Text
varName Set Text
seen)
                         forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. OMap k v -> [(k, v)]
OMap.assocs
                         forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. MemoEnv t -> FnNameEnv t
envFreeSymFnEnv)
      if forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [(SomeExprSymFn t, Text)]
newFns
        then if forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [(Text, WellFormedSExpr Atom)]
fnBindings
             then forall (m :: Type -> Type) a. Monad m => a -> m a
return WellFormedSExpr Atom
sexpr
             else let bs :: [WellFormedSExpr Atom]
bs = forall a b. (a -> b) -> [a] -> [b]
map (\(Text
name, WellFormedSExpr Atom
def) -> forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [Text -> WellFormedSExpr Atom
ident Text
name, WellFormedSExpr Atom
def]) [(Text, WellFormedSExpr Atom)]
fnBindings
                  in forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [Text -> WellFormedSExpr Atom
ident Text
"letfn" , forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [WellFormedSExpr Atom]
bs, WellFormedSExpr Atom
sexpr]
        else forall t.
[(SomeExprSymFn t, Text)]
-> [(Text, WellFormedSExpr Atom)]
-> Set Text
-> Memo t (WellFormedSExpr Atom)
go [(SomeExprSymFn t, Text)]
newFns [(Text, WellFormedSExpr Atom)]
fnBindings Set Text
seen
    go (((SomeExprSymFn ExprSymFn t dom ret
nextFn), Text
nextFnName):[(SomeExprSymFn t, Text)]
todo) [(Text, WellFormedSExpr Atom)]
fnBindings Set Text
seen = do
      WellFormedSExpr Atom
nextSExpr <- forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Memo t (WellFormedSExpr Atom)
convertSymFn ExprSymFn t dom ret
nextFn
      let fnBindings' :: [(Text, WellFormedSExpr Atom)]
fnBindings' = (Text
nextFnName, WellFormedSExpr Atom
nextSExpr)forall a. a -> [a] -> [a]
:[(Text, WellFormedSExpr Atom)]
fnBindings
          seen' :: Set Text
seen' = forall a. Ord a => a -> Set a -> Set a
Set.insert Text
nextFnName Set Text
seen
      forall t.
[(SomeExprSymFn t, Text)]
-> [(Text, WellFormedSExpr Atom)]
-> Set Text
-> Memo t (WellFormedSExpr Atom)
go [(SomeExprSymFn t, Text)]
todo [(Text, WellFormedSExpr Atom)]
fnBindings' Set Text
seen'


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

mkLet :: [SExpr] -> SExpr -> SExpr
mkLet :: [WellFormedSExpr Atom]
-> WellFormedSExpr Atom -> WellFormedSExpr Atom
mkLet [] WellFormedSExpr Atom
body       = WellFormedSExpr Atom
body
mkLet [WellFormedSExpr Atom]
bindings WellFormedSExpr Atom
body = forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [Text -> WellFormedSExpr Atom
ident Text
"let", 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 = forall (tps :: Ctx BaseType).
Assignment BaseTypeRepr tps -> [WellFormedSExpr Atom]
convertBaseTypes (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 = forall (tp :: BaseType). BaseTypeRepr tp -> WellFormedSExpr Atom
convertBaseType (forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> BaseTypeRepr ret
W4.fnReturnType ExprSymFn t args ret
symFn)
     [(Some (ExprBoundVar t), Text)]
argsWithFreshNames <- let rawArgs :: [Some (ExprBoundVar t)]
rawArgs = forall 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]
FC.toListFC forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Assignment (ExprBoundVar t) args
argVars
                           in forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Some (ExprBoundVar t) -> Memo t (Some (ExprBoundVar t), Text)
getBoundVarWithFreshName [Some (ExprBoundVar t)]
rawArgs
     let ([Some (ExprBoundVar t)]
origBoundVars, [Text]
freshArgNames) = forall a b. [(a, b)] -> ([a], [b])
unzip [(Some (ExprBoundVar t), Text)]
argsWithFreshNames
     -- Convert the body with the bound variable set and
     -- free-variable mapping extended to reflect being
     -- under the function's binders.
     WellFormedSExpr Atom
sExpr <- forall s a. (s -> s) -> State s a -> State s a
MS.withState (\MemoEnv t
ms -> let boundVars :: Set (Some (ExprBoundVar t))
boundVars = forall t. MemoEnv t -> Set (Some (ExprBoundVar t))
envBoundVars MemoEnv t
ms
                                       fvEnv :: VarNameEnv t
fvEnv = forall t. MemoEnv t -> VarNameEnv t
envFreeVarEnv MemoEnv t
ms
                             in MemoEnv t
ms { envBoundVars :: Set (Some (ExprBoundVar t))
envBoundVars = forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (Some (ExprBoundVar t))
boundVars (forall a. Ord a => [a] -> Set a
Set.fromList [Some (ExprBoundVar t)]
origBoundVars)
                                   , envFreeVarEnv :: VarNameEnv t
envFreeVarEnv = VarNameEnv t
fvEnv forall k v. Ord k => OMap k v -> OMap k v -> OMap k v
OMap.<>| (forall k v. Ord k => [(k, v)] -> OMap k v
OMap.fromList [(Some (ExprBoundVar t), Text)]
argsWithFreshNames)})
              forall a b. (a -> b) -> a -> b
$ forall t (tp :: BaseType).
Expr t tp -> Memo t (WellFormedSExpr Atom)
convertExprWithLet Expr t ret
body
     forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [ Text -> WellFormedSExpr Atom
ident Text
"definedfn"
                  , Some StringInfoRepr -> Text -> WellFormedSExpr Atom
string (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some StringInfoRepr 'Unicode
W4.UnicodeRepr) forall a b. (a -> b) -> a -> b
$ SolverSymbol -> Text
W4.solverSymbolAsText SolverSymbol
symFnName
                  , forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L ((Text -> WellFormedSExpr Atom
ident Text
"->")forall a. a -> [a] -> [a]
:[WellFormedSExpr Atom]
sArgTs forall a. [a] -> [a] -> [a]
++ [WellFormedSExpr Atom
sRetT])
                  , forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Text -> WellFormedSExpr Atom
ident [Text]
freshArgNames
                  , WellFormedSExpr Atom
sExpr
                  ]
   W4.UninterpFnInfo Assignment BaseTypeRepr args
argTs BaseTypeRepr ret
retT ->
     let sArgTs :: [WellFormedSExpr Atom]
sArgTs = forall (tps :: Ctx BaseType).
Assignment BaseTypeRepr tps -> [WellFormedSExpr Atom]
convertBaseTypes Assignment BaseTypeRepr args
argTs
         sRetT :: WellFormedSExpr Atom
sRetT = forall (tp :: BaseType). BaseTypeRepr tp -> WellFormedSExpr Atom
convertBaseType BaseTypeRepr ret
retT
     in forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [ Text -> WellFormedSExpr Atom
ident Text
"uninterpfn"
                     , Some StringInfoRepr -> Text -> WellFormedSExpr Atom
string (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some StringInfoRepr 'Unicode
W4.UnicodeRepr) forall a b. (a -> b) -> a -> b
$ SolverSymbol -> Text
W4.solverSymbolAsText SolverSymbol
symFnName
                     , forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L ((Text -> WellFormedSExpr Atom
ident Text
"->")forall a. a -> [a] -> [a]
:[WellFormedSExpr Atom]
sArgTs 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 ->
     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) -> Memo t (Some (ExprBoundVar t), Text)
getBoundVarWithFreshName someVar :: Some (ExprBoundVar t)
someVar@(Some ExprBoundVar t x
var) = do
      Text
nm <- forall (tp :: BaseType) t. BaseTypeRepr tp -> Memo t Text
freshName (forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
W4.bvarType ExprBoundVar t x
var)
      forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some (ExprBoundVar t)
someVar, Text
nm)


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



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

freshFnName :: W4.ExprSymFn t args ret -> Memo t Text
freshFnName :: forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Memo t Text
freshFnName ExprSymFn t args ret
fn = do
  Natural
idCount <- forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
MS.gets forall t. MemoEnv t -> Natural
envIdCounter
  forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
MS.modify' forall a b. (a -> b) -> a -> b
$ (\MemoEnv t
e -> MemoEnv t
e {envIdCounter :: Natural
envIdCounter = Natural
idCount forall a. Num a => a -> a -> a
+ Natural
1})
  let prefix :: String
prefix = case 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"
  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ String
prefixforall a. [a] -> [a] -> [a]
++(forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Natural
idCount)



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

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

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

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


convertAppExpr' :: forall t tp . W4.AppExpr t tp -> Memo t SExpr
convertAppExpr' :: forall t (tp :: BaseType).
AppExpr t tp -> Memo t (WellFormedSExpr Atom)
convertAppExpr' = forall (tp' :: BaseType).
App (Expr t) tp' -> Memo t (WellFormedSExpr Atom)
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
W4.appExprApp
  where go :: forall tp' . W4.App (W4.Expr t) tp' -> Memo t SExpr
        go :: forall (tp' :: BaseType).
App (Expr t) tp' -> Memo t (WellFormedSExpr Atom)
go (W4.BaseIte BaseTypeRepr tp'
_bt Integer
_ Expr t 'BaseBoolType
e1 Expr t tp'
e2 Expr t tp'
e3) = do
          WellFormedSExpr Atom
s1 <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseBoolType
e1
          WellFormedSExpr Atom
s2 <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t tp'
e2
          WellFormedSExpr Atom
s3 <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t tp'
e3
          forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [Text -> WellFormedSExpr Atom
ident Text
"ite", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2, WellFormedSExpr Atom
s3]
        go (W4.BaseEq BaseTypeRepr tp1
_bt Expr t tp1
e1 Expr t tp1
e2) = do
          WellFormedSExpr Atom
s1 <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t tp1
e1
          WellFormedSExpr Atom
s2 <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t tp1
e2
          forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [Text -> WellFormedSExpr Atom
ident Text
"=", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.NotPred Expr t 'BaseBoolType
e) = do
          WellFormedSExpr Atom
s <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseBoolType
e
          forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [Text -> WellFormedSExpr Atom
ident Text
"notp", WellFormedSExpr Atom
s]
        go (W4.ConjPred BoolMap (Expr t)
bm) = Text -> Bool -> BoolMap (Expr t) -> Memo t (WellFormedSExpr Atom)
convertBoolMap Text
"andp" Bool
True BoolMap (Expr t)
bm
        go (W4.BVSlt Expr t (BaseBVType w)
e1 Expr t (BaseBVType w)
e2) = do
          WellFormedSExpr Atom
s1 <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t (BaseBVType w)
e1
          WellFormedSExpr Atom
s2 <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t (BaseBVType w)
e2
          forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [Text -> WellFormedSExpr Atom
ident Text
"bvslt", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.BVUlt Expr t (BaseBVType w)
e1 Expr t (BaseBVType w)
e2) = do
          WellFormedSExpr Atom
s1 <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t (BaseBVType w)
e1
          WellFormedSExpr Atom
s2 <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t (BaseBVType w)
e2
          forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [Text -> WellFormedSExpr Atom
ident Text
"bvult", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.BVConcat NatRepr (u + v)
_ Expr t (BaseBVType u)
e1 Expr t (BaseBVType v)
e2) = do
          WellFormedSExpr Atom
s1 <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t (BaseBVType u)
e1
          WellFormedSExpr Atom
s2 <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t (BaseBVType v)
e2
          forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [Text -> WellFormedSExpr Atom
ident Text
"concat", WellFormedSExpr Atom
s1, WellFormedSExpr Atom
s2]
        go (W4.BVSelect NatRepr idx
idx NatRepr n
n Expr t (BaseBVType w)
bv) = 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 = forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr n
n forall a. Num a => a -> a -> a
+ Integer
j forall a. Num a => a -> a -> a
- Integer
1
                j :: Integer
j = 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 forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr -> SemiRingRepr sr
WSum.sumRepr WeightedSum (Expr t) sr
sm of
            W4.SemiRingBVRepr BVFlavorRepr fv
W4.BVArithRepr NatRepr w
w ->
              let smul :: BV w -> Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
smul BV w
mul Expr t (BaseBVType w)
e = do
                    WellFormedSExpr Atom
s <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t (BaseBVType w)
e
                    forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [ Text -> WellFormedSExpr Atom
ident Text
"bvmul", Natural -> Integer -> WellFormedSExpr Atom
bitvec (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w) (forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
mul), WellFormedSExpr Atom
s]
                  sval :: BV w -> Memo t (WellFormedSExpr Atom)
sval BV w
v = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Natural -> Integer -> WellFormedSExpr Atom
bitvec (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w) (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 = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [ Text -> WellFormedSExpr Atom
ident Text
"bvadd", WellFormedSExpr Atom
x, WellFormedSExpr Atom
y ]
              in 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 forall {m :: Type -> Type}.
Monad m =>
WellFormedSExpr Atom
-> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
add BV w -> Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
smul BV w -> Memo t (WellFormedSExpr Atom)
sval WeightedSum (Expr t) sr
sm
            W4.SemiRingBVRepr BVFlavorRepr fv
W4.BVBitsRepr NatRepr w
w ->
              let smul :: BV w -> Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
smul BV w
mul Expr t (BaseBVType w)
e = do
                    WellFormedSExpr Atom
s <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t (BaseBVType w)
e
                    forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [ Text -> WellFormedSExpr Atom
ident Text
"bvand", Natural -> Integer -> WellFormedSExpr Atom
bitvec (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w) (forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
mul), WellFormedSExpr Atom
s]
                  sval :: BV w -> Memo t (WellFormedSExpr Atom)
sval BV w
v = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Natural -> Integer -> WellFormedSExpr Atom
bitvec (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w) (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 forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [ WellFormedSExpr Atom
op, WellFormedSExpr Atom
x, WellFormedSExpr Atom
y ]
              in 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 forall {m :: Type -> Type}.
Monad m =>
WellFormedSExpr Atom
-> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
add BV w -> Expr t (BaseBVType w) -> Memo t (WellFormedSExpr Atom)
smul BV w -> Memo t (WellFormedSExpr Atom)
sval WeightedSum (Expr t) sr
sm
            SemiRingRepr sr
W4.SemiRingIntegerRepr ->
              let smul :: Integer -> Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
smul Integer
mul Expr t 'BaseIntegerType
e = do
                    WellFormedSExpr Atom
s <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseIntegerType
e
                    forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [ Text -> WellFormedSExpr Atom
ident Text
"intmul", Integer -> WellFormedSExpr Atom
int Integer
mul, WellFormedSExpr Atom
s]
                  sval :: Integer -> m (WellFormedSExpr Atom)
sval Integer
v = forall (m :: Type -> Type) a. Monad m => a -> m a
return 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 = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [ Text -> WellFormedSExpr Atom
ident Text
"intadd", WellFormedSExpr Atom
x, WellFormedSExpr Atom
y ]
              in 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 forall {m :: Type -> Type}.
Monad m =>
WellFormedSExpr Atom
-> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
add Integer -> Expr t 'BaseIntegerType -> Memo t (WellFormedSExpr Atom)
smul forall {m :: Type -> Type}.
Monad m =>
Integer -> m (WellFormedSExpr Atom)
sval WeightedSum (Expr t) sr
sm
            SemiRingRepr sr
W4.SemiRingRealRepr    -> forall a. HasCallStack => String -> a
error String
"SemiRingSum RealRepr not supported"

        go (W4.SemiRingProd SemiRingProduct (Expr t) sr
pd) =
          case 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 = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [ Text -> WellFormedSExpr Atom
ident Text
"bvmul", WellFormedSExpr Atom
x, WellFormedSExpr Atom
y ]
              Maybe (WellFormedSExpr Atom)
maybeS <- 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 forall {m :: Type -> Type}.
Monad m =>
WellFormedSExpr Atom
-> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
pmul forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE SemiRingProduct (Expr t) sr
pd
              case Maybe (WellFormedSExpr Atom)
maybeS of
                Just WellFormedSExpr Atom
s -> forall (m :: Type -> Type) a. Monad m => a -> m a
return WellFormedSExpr Atom
s
                Maybe (WellFormedSExpr Atom)
Nothing -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Natural -> Integer -> WellFormedSExpr Atom
bitvec (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 = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [ Text -> WellFormedSExpr Atom
ident Text
"bvand", WellFormedSExpr Atom
x, WellFormedSExpr Atom
y ]
              Maybe (WellFormedSExpr Atom)
maybeS <- 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 forall {m :: Type -> Type}.
Monad m =>
WellFormedSExpr Atom
-> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
pmul forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE SemiRingProduct (Expr t) sr
pd
              case Maybe (WellFormedSExpr Atom)
maybeS of
                Just WellFormedSExpr Atom
s -> forall (m :: Type -> Type) a. Monad m => a -> m a
return WellFormedSExpr Atom
s
                Maybe (WellFormedSExpr Atom)
Nothing -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Natural -> Integer -> WellFormedSExpr Atom
bitvec (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 = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [ Text -> WellFormedSExpr Atom
ident Text
"intmul", WellFormedSExpr Atom
x, WellFormedSExpr Atom
y ]
              Maybe (WellFormedSExpr Atom)
maybeS <- 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 forall {m :: Type -> Type}.
Monad m =>
WellFormedSExpr Atom
-> WellFormedSExpr Atom -> m (WellFormedSExpr Atom)
pmul forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE SemiRingProduct (Expr t) sr
pd
              case Maybe (WellFormedSExpr Atom)
maybeS of
                Just WellFormedSExpr Atom
s -> forall (m :: Type -> Type) a. Monad m => a -> m a
return WellFormedSExpr Atom
s
                Maybe (WellFormedSExpr Atom)
Nothing -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Integer -> WellFormedSExpr Atom
int Integer
1
            SemiRingRepr sr
W4.SemiRingRealRepr    -> forall a. HasCallStack => String -> a
error String
"convertApp W4.SemiRingProd Real unsupported"

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

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

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

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

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

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

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

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

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

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

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

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

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

        convertBoolMap :: Text -> Bool -> BooM.BoolMap (W4.Expr t) -> Memo t SExpr
        convertBoolMap :: Text -> Bool -> BoolMap (Expr t) -> Memo t (WellFormedSExpr Atom)
convertBoolMap Text
op Bool
base BoolMap (Expr t)
bm =
          let strBase :: Bool -> WellFormedSExpr Atom
strBase Bool
b = if Bool
b
                          then 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 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not
          in case forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
BooM.viewBoolMap BoolMap (Expr t)
bm of
               BoolMapView (Expr t)
BooM.BoolMapUnit -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> WellFormedSExpr Atom
strBase Bool
base
               BoolMapView (Expr t)
BooM.BoolMapDualUnit -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> WellFormedSExpr Atom
strNotBase Bool
base
               BooM.BoolMapTerms NonEmpty (Expr t 'BaseBoolType, Polarity)
ts ->
                 let onEach :: (Expr t 'BaseBoolType, Polarity)
-> WellFormedSExpr Atom -> Memo t (WellFormedSExpr Atom)
onEach (Expr t 'BaseBoolType, Polarity)
e WellFormedSExpr Atom
r = do
                       WellFormedSExpr Atom
s <- (Expr t 'BaseBoolType, Polarity) -> Memo t (WellFormedSExpr Atom)
arg (Expr t 'BaseBoolType, Polarity)
e
                       forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [Text -> WellFormedSExpr Atom
ident Text
op, WellFormedSExpr Atom
s, WellFormedSExpr Atom
r]
                     arg :: (Expr t 'BaseBoolType, Polarity) -> Memo t (WellFormedSExpr Atom)
arg (Expr t 'BaseBoolType
t, Polarity
BooM.Positive) = forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseBoolType
t
                     arg (Expr t 'BaseBoolType
t, Polarity
BooM.Negative) = do
                       WellFormedSExpr Atom
s <- forall (tp' :: BaseType).
Expr t tp' -> Memo t (WellFormedSExpr Atom)
goE Expr t 'BaseBoolType
t
                       forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [Text -> WellFormedSExpr Atom
ident Text
"notp", WellFormedSExpr Atom
s]
                 in 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 (tp :: BaseType). IndexLit tp -> 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 (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
irep) (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 =
  forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Some Expr t x
e) -> forall t (tp :: BaseType).
Expr t tp -> Memo t (WellFormedSExpr Atom)
convertExpr Expr t x
e) (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]
FC.toListFC forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Assignment (Expr t) sh
es)

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


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