{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE MultiWayIf #-}

-- | A parser for an s-expression representation of what4 expressions
module What4.Serialize.Parser
  ( deserializeExpr
  , deserializeExprWithConfig
  , deserializeSymFn
  , deserializeSymFnWithConfig
  , deserializeBaseType
  , readBaseTypes
  , Atom(..)
  , S.WellFormedSExpr(..)
  , Config(..)
  , defaultConfig
  , SomeSymFn(..)
  , type SExpr
  , parseSExpr
  , printSExpr
  ) where

import           Control.Monad ( when )
import qualified Control.Monad.Except as E
import           Control.Monad.IO.Class ( liftIO )
import qualified Control.Monad.Reader as R
import qualified Data.BitVector.Sized as BV
import qualified Data.Foldable as F
import qualified Data.HashMap.Lazy as HM
import           Data.Kind
import qualified Data.SCargot.Repr.WellFormed as S

import           Data.Text ( Text )
import qualified Data.Text as T
import qualified Data.Text.Encoding as T
import           Text.Printf ( printf )

import qualified Data.Parameterized.NatRepr as PN
import qualified Data.Parameterized.Ctx as Ctx
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Classes
import           Data.Parameterized.Some ( Some(..) )
import qualified Data.Parameterized.TraversableFC as FC
import           What4.BaseTypes

import qualified What4.Expr.ArrayUpdateMap as WAU
import qualified What4.Expr.Builder as W4
import qualified What4.IndexLit as WIL
import qualified What4.Interface as W4

import           What4.Serialize.SETokens ( Atom(..), printSExpr, parseSExpr )
import qualified What4.Utils.Serialize as U
import           What4.Serialize.Printer ( SExpr )

import           Prelude

data SomeSymFn t = forall dom ret. SomeSymFn (W4.SymFn t dom ret)

data Config sym =
  Config
  { forall sym. Config sym -> Text -> IO (Maybe (SomeSymFn sym))
cSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
  -- ^ The mapping of names to defined What4 SymFns.
  , forall sym. Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
cExprLookup :: Text -> IO (Maybe (Some (W4.SymExpr sym)))
  -- ^ The mapping of names to defined What4 expressions.
  }

defaultConfig :: (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym)) => sym -> Config sym
defaultConfig :: forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
sym -> Config sym
defaultConfig sym
_sym = Config { cSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
cSymFnLookup = forall a b. a -> b -> a
const (forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)
                            , cExprLookup :: Text -> IO (Maybe (Some (SymExpr sym)))
cExprLookup = forall a b. a -> b -> a
const (forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)
                            }


-- | The lexical environment for parsing s-expressions and
-- procesing them into What4 terms.
data ProcessorEnv sym =
  ProcessorEnv
  { forall sym. ProcessorEnv sym -> sym
procSym :: sym
  -- ^ The symbolic What4 backend being used.
  , forall sym. ProcessorEnv sym -> Text -> IO (Maybe (SomeSymFn sym))
procSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
    -- ^ The user-specified mapping of names to defined What4 SymFns.
  , forall sym.
ProcessorEnv sym -> Text -> IO (Maybe (Some (SymExpr sym)))
procExprLookup :: Text -> IO (Maybe (Some (W4.SymExpr sym)))
  -- ^ The user-specified mapping of names to defined What4 expressions.
  , forall sym. ProcessorEnv sym -> HashMap Text (Some (SymExpr sym))
procLetEnv :: HM.HashMap Text (Some (W4.SymExpr sym))
  -- ^ The current lexical environment w.r.t. let-bindings
  -- encountered while parsing. N.B., these bindings are
  -- checked _before_ the \"global\" bindings implied by the
  -- user-specified lookup functions.
  , forall sym. ProcessorEnv sym -> HashMap Text (SomeSymFn sym)
procLetFnEnv :: HM.HashMap Text (SomeSymFn sym)
  -- ^ The current lexical symfn environment
  -- w.r.t. letfn-bindings encountered while parsing. N.B.,
  -- these bindings are checked /before/ the \"global\"
  -- bindings implied by the user-specified lookup
  -- functions.
  }

type Processor sym a = E.ExceptT String (R.ReaderT (ProcessorEnv sym) IO) a

runProcessor :: ProcessorEnv sym -> Processor sym a -> IO (Either String a)
runProcessor :: forall sym a.
ProcessorEnv sym -> Processor sym a -> IO (Either String a)
runProcessor ProcessorEnv sym
env Processor sym a
action = forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
R.runReaderT (forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
E.runExceptT Processor sym a
action) ProcessorEnv sym
env

lookupExpr :: Text -> Processor sym (Maybe (Some (W4.SymExpr sym)))
lookupExpr :: forall sym. Text -> Processor sym (Maybe (Some (SymExpr sym)))
lookupExpr Text
nm = do
  Text -> IO (Maybe (Some (SymExpr sym)))
userLookupFn <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.asks forall sym.
ProcessorEnv sym -> Text -> IO (Maybe (Some (SymExpr sym)))
procExprLookup
  HashMap Text (Some (SymExpr sym))
letEnv <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.asks forall sym. ProcessorEnv sym -> HashMap Text (Some (SymExpr sym))
procLetEnv
  case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HM.lookup Text
nm HashMap Text (Some (SymExpr sym))
letEnv of
    Maybe (Some (SymExpr sym))
Nothing -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Text -> IO (Maybe (Some (SymExpr sym)))
userLookupFn Text
nm
    Maybe (Some (SymExpr sym))
res -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (Some (SymExpr sym))
res

lookupFn :: Text -> Processor sym (Maybe (SomeSymFn sym))
lookupFn :: forall sym. Text -> Processor sym (Maybe (SomeSymFn sym))
lookupFn Text
nm = do
  Text -> IO (Maybe (SomeSymFn sym))
userLookupFn <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.asks forall sym. ProcessorEnv sym -> Text -> IO (Maybe (SomeSymFn sym))
procSymFnLookup
  HashMap Text (SomeSymFn sym)
letEnv <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.asks forall sym. ProcessorEnv sym -> HashMap Text (SomeSymFn sym)
procLetFnEnv
  case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HM.lookup Text
nm HashMap Text (SomeSymFn sym)
letEnv of
    Maybe (SomeSymFn sym)
Nothing -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Text -> IO (Maybe (SomeSymFn sym))
userLookupFn Text
nm
    Maybe (SomeSymFn sym)
res -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (SomeSymFn sym)
res


-- | @(deserializeExpr sym)@ is equivalent
-- to @(deserializeExpr' (defaultConfig sym))@.
deserializeExpr ::
  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
  => sym
  -> SExpr
  -> IO (Either String (Some (W4.SymExpr sym)))
deserializeExpr :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym -> SExpr -> IO (Either String (Some (SymExpr sym)))
deserializeExpr sym
sym = forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> Config sym -> SExpr -> IO (Either String (Some (SymExpr sym)))
deserializeExprWithConfig sym
sym Config sym
cfg
  where cfg :: Config sym
cfg = forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
sym -> Config sym
defaultConfig sym
sym

deserializeExprWithConfig ::
  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
  => sym
  -> Config sym
  -> SExpr
  -> IO (Either String (Some (W4.SymExpr sym)))
deserializeExprWithConfig :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> Config sym -> SExpr -> IO (Either String (Some (SymExpr sym)))
deserializeExprWithConfig sym
sym Config sym
cfg SExpr
sexpr = forall sym a.
ProcessorEnv sym -> Processor sym a -> IO (Either String a)
runProcessor ProcessorEnv sym
env (forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
sexpr)
  where env :: ProcessorEnv sym
env = ProcessorEnv { procSym :: sym
procSym = sym
sym
                           , procSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
procSymFnLookup = forall sym. Config sym -> Text -> IO (Maybe (SomeSymFn sym))
cSymFnLookup Config sym
cfg
                           , procExprLookup :: Text -> IO (Maybe (Some (SymExpr sym)))
procExprLookup = forall sym. Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
cExprLookup Config sym
cfg
                           , procLetEnv :: HashMap Text (Some (SymExpr sym))
procLetEnv = forall k v. HashMap k v
HM.empty
                           , procLetFnEnv :: HashMap Text (SomeSymFn sym)
procLetFnEnv = forall k v. HashMap k v
HM.empty
                           }

-- | @(deserializeSymFn sym)@ is equivalent
-- to @(deserializeSymFn' (defaultConfig sym))@.
deserializeSymFn ::
  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
  => sym
  -> SExpr
  -> IO (Either String (SomeSymFn sym))
deserializeSymFn :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym -> SExpr -> IO (Either String (SomeSymFn sym))
deserializeSymFn sym
sym = forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym -> Config sym -> SExpr -> IO (Either String (SomeSymFn sym))
deserializeSymFnWithConfig sym
sym Config sym
cfg
  where cfg :: Config sym
cfg = forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
sym -> Config sym
defaultConfig sym
sym

deserializeSymFnWithConfig ::
  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
  => sym
  -> Config sym
  -> SExpr
  -> IO (Either String (SomeSymFn sym))
deserializeSymFnWithConfig :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym -> Config sym -> SExpr -> IO (Either String (SomeSymFn sym))
deserializeSymFnWithConfig sym
sym Config sym
cfg SExpr
sexpr = forall sym a.
ProcessorEnv sym -> Processor sym a -> IO (Either String a)
runProcessor ProcessorEnv sym
env (forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (SomeSymFn sym)
readSymFn SExpr
sexpr)
  where env :: ProcessorEnv sym
env = ProcessorEnv { procSym :: sym
procSym = sym
sym
                           , procSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
procSymFnLookup = forall sym. Config sym -> Text -> IO (Maybe (SomeSymFn sym))
cSymFnLookup Config sym
cfg
                           , procExprLookup :: Text -> IO (Maybe (Some (SymExpr sym)))
procExprLookup = forall sym. Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
cExprLookup Config sym
cfg
                           , procLetEnv :: HashMap Text (Some (SymExpr sym))
procLetEnv = forall k v. HashMap k v
HM.empty
                           , procLetFnEnv :: HashMap Text (SomeSymFn sym)
procLetFnEnv = forall k v. HashMap k v
HM.empty
                           }


deserializeBaseType ::
  SExpr
  -> Either String (Some BaseTypeRepr)
deserializeBaseType :: SExpr -> Either String (Some BaseTypeRepr)
deserializeBaseType SExpr
sexpr = forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some BaseTypeRepr)
readBaseType SExpr
sexpr





-- * First pass of parsing turns the raw text into s-expressions.
--   This pass is handled by the code in What4.Serialize.SETokens

-- * Second pass of parsing: turning the s-expressions into symbolic expressions
-- and the overall templated formula

-- ** Utility functions

-- | Utility function for contextualizing errors. Prepends the given prefix
-- whenever an error is thrown.
prefixError :: (Monoid e, E.MonadError e m) => e -> m a -> m a
prefixError :: forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError e
prefix m a
act = forall e (m :: Type -> Type) a.
MonadError e m =>
m a -> (e -> m a) -> m a
E.catchError m a
act (forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Monoid a => a -> a -> a
mappend e
prefix)

-- | Utility function for lifting a 'Maybe' into a 'MonadError'
fromMaybeError :: (E.MonadError e m) => e -> Maybe a -> m a
fromMaybeError :: forall e (m :: Type -> Type) a.
MonadError e m =>
e -> Maybe a -> m a
fromMaybeError e
err = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError e
err) forall (m :: Type -> Type) a. Monad m => a -> m a
return


readBaseType ::
  forall m . (E.MonadError String m)
  => SExpr
  -> m (Some BaseTypeRepr)
readBaseType :: forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some BaseTypeRepr)
readBaseType SExpr
sexpr =
  case SExpr
sexpr of
    S.WFSAtom (AId Text
atom) ->
      case (Text -> String
T.unpack Text
atom) of
        String
"Bool" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr 'BaseBoolType
BaseBoolRepr
        String
"Int" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr 'BaseIntegerType
BaseIntegerRepr
        String
"Real" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr 'BaseRealType
BaseRealRepr
        String
"String" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
BaseStringRepr StringInfoRepr 'Unicode
UnicodeRepr)
        String
"Complex" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr 'BaseComplexType
BaseComplexRepr
        String
_ -> m (Some BaseTypeRepr)
panic
    S.WFSList [(S.WFSAtom (AId Text
"BV")), (S.WFSAtom (AInt Integer
w))]
      | Just (Some NatRepr x
wRepr) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
w
      , Just LeqProof 1 x
LeqProof <- forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr x
wRepr
        -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr x
wRepr)
      | Bool
otherwise
        -> m (Some BaseTypeRepr)
panic
    S.WFSList [(S.WFSAtom (AId Text
"Float")), (S.WFSAtom (AInt Integer
e)), (S.WFSAtom (AInt Integer
s))]
      | Just (Some NatRepr x
eRepr) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
e
      , Just (Some NatRepr x
sRepr) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
s
      , Just LeqProof 2 x
LeqProof <- forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @2) NatRepr x
eRepr
      , Just LeqProof 2 x
LeqProof <- forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @2) NatRepr x
sRepr
        -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
BaseFloatRepr (forall (eb :: Nat) (sb :: Nat).
(2 <= eb, 2 <= sb) =>
NatRepr eb
-> NatRepr sb -> FloatPrecisionRepr ('FloatingPointPrecision eb sb)
FloatingPointPrecisionRepr NatRepr x
eRepr NatRepr x
sRepr)))
      | Bool
otherwise -> m (Some BaseTypeRepr)
panic
    S.WFSList [(S.WFSAtom (AId Text
"Struct")), SExpr
args] -> do
      Some Assignment BaseTypeRepr x
tps <- forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some (Assignment BaseTypeRepr))
readBaseTypes SExpr
args
      forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx -> BaseTypeRepr ('BaseStructType ctx)
BaseStructRepr Assignment BaseTypeRepr x
tps)
    S.WFSList [S.WFSAtom (AId Text
"Array"), SExpr
ixArgs, SExpr
tpArg] -> do
      Some Assignment BaseTypeRepr x
ixs <- forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some (Assignment BaseTypeRepr))
readBaseTypes SExpr
ixArgs
      Some BaseTypeRepr x
tp <- forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some BaseTypeRepr)
readBaseType SExpr
tpArg
      case forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
Ctx.viewAssign Assignment BaseTypeRepr x
ixs of
        AssignView BaseTypeRepr x
Ctx.AssignEmpty -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"array type has no indices: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExpr
sexpr
        Ctx.AssignExtend Assignment BaseTypeRepr ctx1
_ BaseTypeRepr tp
_ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr ('BaseArrayType (idx ::> tp) xs)
BaseArrayRepr Assignment BaseTypeRepr x
ixs BaseTypeRepr x
tp)
    SExpr
_ -> m (Some BaseTypeRepr)
panic
  where
    panic :: m (Some BaseTypeRepr)
panic = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"unknown base type: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExpr
sexpr

readBaseTypes ::
  forall m . (E.MonadError String m)
  => SExpr
  -> m (Some (Ctx.Assignment BaseTypeRepr))
readBaseTypes :: forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some (Assignment BaseTypeRepr))
readBaseTypes sexpr :: SExpr
sexpr@(S.WFSAtom Atom
_) = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"expected list of base types: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExpr
sexpr
readBaseTypes (S.WFSList [SExpr]
sexprs) = forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some BaseTypeRepr)
readBaseType [SExpr]
sexprs

-- ** Parsing definitions

-- | Stores a NatRepr along with proof that its type parameter is a bitvector of
-- that length. Used for easy pattern matching on the LHS of a binding in a
-- do-expression to extract the proof.
data BVProof tp where
  BVProof :: forall n. (1 <= n) => NatRepr n -> BVProof (BaseBVType n)

-- | Given an expression, monadically either returns proof that it is a
-- bitvector or throws an error.
getBVProof :: (W4.IsExpr ex, E.MonadError String m) => ex tp -> m (BVProof tp)
getBVProof :: forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof ex tp
expr =
  case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType ex tp
expr of
    BaseBVRepr NatRepr w
n -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (res :: Nat).
(1 <= res) =>
NatRepr res -> BVProof (BaseBVType res)
BVProof NatRepr w
n
    BaseTypeRepr tp
t -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"expected BV, found %s" (forall a. Show a => a -> String
show BaseTypeRepr tp
t)


-- | Operator type descriptions for parsing s-expression of
-- the form @(operator operands ...)@.
data Op sym where
    FloatOp1 :: (forall fpp . sym ->
                 W4.SymFloat sym fpp ->
                 IO (W4.SymFloat sym fpp))
             -> Op sym
    -- | Generic unary operator description.
    Op1 :: Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1)
        -> (sym ->
            W4.SymExpr sym arg1 ->
            IO (W4.SymExpr sym ret))
        -> Op sym
    -- | Generic dyadic operator description.
    Op2 :: Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1 Ctx.::> arg2)
        -> (sym ->
            W4.SymExpr sym arg1 ->
            W4.SymExpr sym arg2 ->
            IO (W4.SymExpr sym ret))
        -> Op sym
    -- | Generic triadic operator description.
    Op3 :: Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1 Ctx.::> arg2 Ctx.::> arg3)
        -> (sym ->
            W4.SymExpr sym arg1 ->
            W4.SymExpr sym arg2 ->
            W4.SymExpr sym arg3 ->
            IO (W4.SymExpr sym ret)
           )
        -> Op sym
    -- | Generic tetradic operator description.
    Op4 :: Ctx.Assignment
           BaseTypeRepr
           (Ctx.EmptyCtx Ctx.::> arg1 Ctx.::> arg2 Ctx.::> arg3 Ctx.::> arg4)
        -> ( sym ->
             W4.SymExpr sym arg1 ->
             W4.SymExpr sym arg2 ->
             W4.SymExpr sym arg3 ->
             W4.SymExpr sym arg4 ->
             IO (W4.SymExpr sym ret)
           )
        -> Op sym
    -- | Encapsulating type for a unary operation that takes one bitvector and
    -- returns another (in IO).
    BVOp1 :: (forall w . (1 <= w) =>
               sym ->
               W4.SymBV sym w ->
               IO (W4.SymBV sym w))
          -> Op sym
    -- | Binop with a bitvector return type, e.g., addition or bitwise operations.
    BVOp2 :: (forall w . (1 <= w) =>
               sym ->
               W4.SymBV sym w ->
               W4.SymBV sym w ->
               IO (W4.SymBV sym w))
          -> Op sym
    -- | Bitvector binop with a boolean return type, i.e., comparison operators.
    BVComp2 :: (forall w . (1 <= w) =>
                    sym ->
                    W4.SymBV sym w ->
                    W4.SymBV sym w ->
                    IO (W4.Pred sym))
                -> Op sym

-- | Lookup mapping operators to their Op definitions (if they exist)
lookupOp :: forall sym . W4.IsSymExprBuilder sym => Text -> Maybe (Op sym)
lookupOp :: forall sym. IsSymExprBuilder sym => Text -> Maybe (Op sym)
lookupOp Text
name = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HM.lookup Text
name forall sym. IsSymExprBuilder sym => HashMap Text (Op sym)
opTable


opTable :: (W4.IsSymExprBuilder sym) => HM.HashMap Text (Op sym)
opTable :: forall sym. IsSymExprBuilder sym => HashMap Text (Op sym)
opTable =
  forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HM.fromList [
  -- -- -- Boolean ops -- -- --
    (Text
"andp", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred)
  , (Text
"orp", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.orPred)
  , (Text
"xorp", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.xorPred)
  , (Text
"notp", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred)
  -- -- -- Float ops -- -- --
  , (Text
"floatneg", forall sym.
(forall (fpp :: FloatPrecision).
 sym -> SymFloat sym fpp -> IO (SymFloat sym fpp))
-> Op sym
FloatOp1 forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatNeg)
  , (Text
"floatabs", forall sym.
(forall (fpp :: FloatPrecision).
 sym -> SymFloat sym fpp -> IO (SymFloat sym fpp))
-> Op sym
FloatOp1 forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatAbs)
  -- -- -- Integer ops -- -- --
  , (Text
"intmul", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMul)
  , (Text
"intadd", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intAdd)
  , (Text
"intmod", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMod)
  , (Text
"intdiv", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intDiv)
  , (Text
"intle", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intLe)
  , (Text
"intabs", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intAbs)
  -- -- -- Bitvector ops -- -- --
  , (Text
"bvand", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvAndBits)
  , (Text
"bvor", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvOrBits)
  , (Text
"bvadd", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvAdd)
  , (Text
"bvmul", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvMul)
  , (Text
"bvudiv", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvUdiv)
  , (Text
"bvurem", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvUrem)
  , (Text
"bvshl", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvShl)
  , (Text
"bvlshr", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvLshr)
  , (Text
"bvnand", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall a b. (a -> b) -> a -> b
$ \sym
sym SymBV sym w
arg1 SymBV sym w
arg2 -> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNotBits sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvAndBits sym
sym SymBV sym w
arg1 SymBV sym w
arg2)
  , (Text
"bvnor", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall a b. (a -> b) -> a -> b
$ \sym
sym SymBV sym w
arg1 SymBV sym w
arg2 -> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNotBits sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvOrBits sym
sym SymBV sym w
arg1 SymBV sym w
arg2)
  , (Text
"bvxor", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvXorBits)
  , (Text
"bvxnor", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall a b. (a -> b) -> a -> b
$ \sym
sym SymBV sym w
arg1 SymBV sym w
arg2 -> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNotBits sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvXorBits sym
sym SymBV sym w
arg1 SymBV sym w
arg2)
  , (Text
"bvsub", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvSub)
  , (Text
"bvsdiv", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvSdiv)
  , (Text
"bvsrem", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvSrem)
  , (Text
"bvsmod", forall a. HasCallStack => String -> a
error String
"bvsmod is not implemented")
  , (Text
"bvashr", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvAshr)
  , (Text
"bvult", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUlt)
  , (Text
"bvule", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUle)
  , (Text
"bvugt", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUgt)
  , (Text
"bvuge", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUge)
  , (Text
"bvslt", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvSlt)
  , (Text
"bvsle", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvSle)
  , (Text
"bvsgt", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvSgt)
  , (Text
"bvsge", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvSge)
  , (Text
"bveq", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvEq)
  , (Text
"bvne", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvNe)
  , (Text
"bvneg", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp1 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNeg)
  , (Text
"bvnot", forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp1 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNotBits)
  -- -- -- Floating point ops -- -- --
  , (Text
"fnegd", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatNeg @_ @Prec64)
  , (Text
"fnegs", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatNeg @_ @Prec32)
  , (Text
"fabsd", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatAbs @_ @Prec64)
  , (Text
"fabss", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatAbs @_ @Prec32)
  , (Text
"fsqrt", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatSqrt @_ @Prec64 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
  , (Text
"fsqrts", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatSqrt @_ @Prec32 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec32)
x)
  , (Text
"fnand", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (Pred sym)
W4.floatIsNaN @_ @Prec64)
  , (Text
"fnans", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (Pred sym)
W4.floatIsNaN @_ @Prec32)
  , (Text
"frsp", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (fpp :: FloatPrecision) (fpp' :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymFloat sym fpp'
-> IO (SymFloat sym fpp)
W4.floatCast @_ @Prec32 @Prec64 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
  , (Text
"fp_single_to_double", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym ->
    forall sym (fpp :: FloatPrecision) (fpp' :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymFloat sym fpp'
-> IO (SymFloat sym fpp)
W4.floatCast @_ @Prec64 @Prec32 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
W4.RNE)
  , (Text
"fp_binary_to_double",
     forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym -> forall sym (eb :: Nat) (sb :: Nat).
(IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
sym
-> FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> SymBV sym (eb + sb)
-> IO (SymFloat sym (FloatingPointPrecision eb sb))
W4.floatFromBinary @_ @11 @53 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr)
  , (Text
"fp_binary_to_single",
     forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym -> forall sym (eb :: Nat) (sb :: Nat).
(IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
sym
-> FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> SymBV sym (eb + sb)
-> IO (SymFloat sym (FloatingPointPrecision eb sb))
W4.floatFromBinary @_ @8 @24 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr)
  , (Text
"fp_double_to_binary", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (eb :: Nat) (sb :: Nat).
(IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
sym
-> SymFloat sym (FloatingPointPrecision eb sb)
-> IO (SymBV sym (eb + sb))
W4.floatToBinary @_ @11 @53)
  , (Text
"fp_single_to_binary", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (eb :: Nat) (sb :: Nat).
(IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
sym
-> SymFloat sym (FloatingPointPrecision eb sb)
-> IO (SymBV sym (eb + sb))
W4.floatToBinary @_ @8 @24)
  , (Text
"fctid", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> NatRepr w
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymBV sym w)
W4.floatToSBV @_ @64 @Prec64 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
  , (Text
"fctidu", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> NatRepr w
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymBV sym w)
W4.floatToBV @_ @64 @Prec64 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
  , (Text
"fctiw", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> NatRepr w
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymBV sym w)
W4.floatToSBV @_ @32 @Prec64 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
  , (Text
"fctiwu", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> NatRepr w
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymBV sym w)
W4.floatToBV @_ @32 @Prec64 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
  , (Text
"fcfid", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseBVType 64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymBV sym w
-> IO (SymFloat sym fpp)
W4.sbvToFloat @_ @64 @Prec64 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseBVType 64)
x)
  , (Text
"fcfids", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseBVType 64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymBV sym w
-> IO (SymFloat sym fpp)
W4.sbvToFloat @_ @64 @Prec32 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseBVType 64)
x)
  , (Text
"fcfidu", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseBVType 64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymBV sym w
-> IO (SymFloat sym fpp)
W4.bvToFloat @_ @64 @Prec64 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseBVType 64)
x)
  , (Text
"fcfidus", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseBVType 64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymBV sym w
-> IO (SymFloat sym fpp)
W4.bvToFloat @_ @64 @Prec32 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseBVType 64)
x)
  , (Text
"frti", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatRound @_ @Prec64 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
  , (Text
"frtis", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatRound @_ @Prec32 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec32)
x)
  , (Text
"fadd", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
       (arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
    -> SymExpr sym res
    -> SymExpr sym arg2
    -> SymExpr sym arg3
    -> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatAdd @_ @Prec64 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y)
  , (Text
"fadds", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
       (arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
    -> SymExpr sym res
    -> SymExpr sym arg2
    -> SymExpr sym arg3
    -> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatAdd @_ @Prec32 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y)
  , (Text
"fsub", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
       (arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
    -> SymExpr sym res
    -> SymExpr sym arg2
    -> SymExpr sym arg3
    -> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatSub @_ @Prec64 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y)
  , (Text
"fsubs", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
       (arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
    -> SymExpr sym res
    -> SymExpr sym arg2
    -> SymExpr sym arg3
    -> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatSub @_ @Prec32 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y)
  , (Text
"fmul", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
       (arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
    -> SymExpr sym res
    -> SymExpr sym arg2
    -> SymExpr sym arg3
    -> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatMul @_ @Prec64 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y)
  , (Text
"fmuls", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
       (arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
    -> SymExpr sym res
    -> SymExpr sym arg2
    -> SymExpr sym arg3
    -> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatMul @_ @Prec32 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y)
  , (Text
"fdiv", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
       (arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
    -> SymExpr sym res
    -> SymExpr sym arg2
    -> SymExpr sym arg3
    -> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatDiv @_ @Prec64 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y)
  , (Text
"fdivs", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
       (arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
    -> SymExpr sym res
    -> SymExpr sym arg2
    -> SymExpr sym arg3
    -> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatDiv @_ @Prec32 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y)
  , (Text
"fltd", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
W4.floatLt @_ @Prec64)
  , (Text
"flts", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
W4.floatLt @_ @Prec32)
  , (Text
"feqd", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
W4.floatFpEq @_ @Prec64)
  , (Text
"feqs", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
W4.floatFpEq @_ @Prec32)
  , (Text
"fled", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
W4.floatLe @_ @Prec64)
  , (Text
"fles", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
    -> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
W4.floatLe @_ @Prec32)
  , (Text
"ffma", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType)
       (arg4 :: BaseType) sym (ret :: BaseType).
Assignment
  BaseTypeRepr (((('EmptyCtx ::> res) ::> arg2) ::> arg3) ::> arg4)
-> (sym
    -> SymExpr sym res
    -> SymExpr sym arg2
    -> SymExpr sym arg3
    -> SymExpr sym arg4
    -> IO (SymExpr sym ret))
-> Op sym
Op4 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y SymExpr sym (BaseFloatType Prec64)
z -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
    forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatFMA @_ @Prec64 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y SymExpr sym (BaseFloatType Prec64)
z)
  , (Text
"ffmas", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType)
       (arg4 :: BaseType) sym (ret :: BaseType).
Assignment
  BaseTypeRepr (((('EmptyCtx ::> res) ::> arg2) ::> arg3) ::> arg4)
-> (sym
    -> SymExpr sym res
    -> SymExpr sym arg2
    -> SymExpr sym arg3
    -> SymExpr sym arg4
    -> IO (SymExpr sym ret))
-> Op sym
Op4 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y SymExpr sym (BaseFloatType Prec32)
z ->
    forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm -> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatFMA @_ @Prec32 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y SymExpr sym (BaseFloatType Prec32)
z)
  ]

-- | Verify a list of arguments has a single argument and
-- return it, else raise an error.
readOneArg ::
  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
  => [SExpr]
  -> Processor sym (Some (W4.SymExpr sym))
readOneArg :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
operands = do
  [Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
  case [Some (Expr t)]
args of
    [Some (Expr t)
arg] -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Some (Expr t)
arg
    [Some (Expr t)]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"expecting 1 argument, got %d" (forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Some (Expr t)]
args)

-- | Verify a list of arguments has two arguments and return
-- it, else raise an error.
readTwoArgs ::
  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
  => [SExpr]
  -> Processor sym (Some (W4.SymExpr sym), Some (W4.SymExpr sym))
readTwoArgs :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs [SExpr]
operands = do
  [Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
  case [Some (Expr t)]
args of
    [Some (Expr t)
arg1, Some (Expr t)
arg2] -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some (Expr t)
arg1, Some (Expr t)
arg2)
    [Some (Expr t)]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"expecting 2 arguments, got %d" (forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Some (Expr t)]
args)

-- | Verify a list of arguments has three arguments and
-- return it, else raise an error.
readThreeArgs ::
  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
  => [SExpr]
  -> Processor sym (Some (W4.SymExpr sym), Some (W4.SymExpr sym), Some (W4.SymExpr sym))
readThreeArgs :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr]
-> Processor
     sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
readThreeArgs [SExpr]
operands = do
  [Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
  case [Some (Expr t)]
args of
    [Some (Expr t)
arg1, Some (Expr t)
arg2, Some (Expr t)
arg3] -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some (Expr t)
arg1, Some (Expr t)
arg2, Some (Expr t)
arg3)
    [Some (Expr t)]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"expecting 3 arguments, got %d" (forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Some (Expr t)]
args)



-- | Reads an "application" form, i.e. @(operator operands ...)@.
readApp ::
  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
  => SExpr
  -> [SExpr]
  -> Processor sym (Some (W4.SymExpr sym))
readApp :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> [SExpr] -> Processor sym (Some (SymExpr sym))
readApp (S.WFSAtom (AId Text
"call")) (S.WFSAtom (AId Text
fnName):[SExpr]
operands) = do
  ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.asks forall sym. ProcessorEnv sym -> sym
procSym
  Maybe (SomeSymFn sym)
maybeFn <- forall sym. Text -> Processor sym (Maybe (SomeSymFn sym))
lookupFn Text
fnName
  case Maybe (SomeSymFn sym)
maybeFn of
    Just (SomeSymFn SymFn sym dom ret
fn) -> do
      [Some (Expr t)]
args <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr [SExpr]
operands
      Assignment (Expr t) dom
assn <- forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, ShowF (SymExpr sym), ShowF ex, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment (forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> Assignment BaseTypeRepr args
W4.fnArgTypes SymFn sym dom ret
fn) [Some (Expr t)]
args
      forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn ExprBuilder t st fs
sym SymFn sym dom ret
fn Assignment (Expr t) dom
assn)
    Maybe (SomeSymFn sym)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"The function name `"
               forall a. [a] -> [a] -> [a]
++(Text -> String
T.unpack Text
fnName)
               forall a. [a] -> [a] -> [a]
++String
"` is not bound to a SymFn in the current Config."
readApp opRaw :: SExpr
opRaw@(S.WFSAtom (AId Text
"call")) [SExpr]
operands = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError
  forall a b. (a -> b) -> a -> b
$ String
"Unrecognized use of `call`: " forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty (forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L (SExpr
opRawforall a. a -> [a] -> [a]
:[SExpr]
operands))))
readApp opRaw :: SExpr
opRaw@(S.WFSAtom (AId Text
operator)) [SExpr]
operands = do
  ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
  forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError (String
"in reading expression:\n"
               forall a. [a] -> [a] -> [a]
++(Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.WFSList (SExpr
opRawforall a. a -> [a] -> [a]
:[SExpr]
operands))forall a. [a] -> [a] -> [a]
++String
"\n") forall a b. (a -> b) -> a -> b
$
  -- Parse an expression of the form @(fnname operands ...)@
    case forall sym. IsSymExprBuilder sym => Text -> Maybe (Op sym)
lookupOp @sym Text
operator of
      Just (FloatOp1 forall (fpp :: FloatPrecision).
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
fn) -> do
        [Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
        case [Some (Expr t)]
args of
          [Some Expr t x
a1]
            | BaseFloatRepr FloatPrecisionRepr fpp
_ <- forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
a1 -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fpp :: FloatPrecision).
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
fn ExprBuilder t st fs
sym Expr t x
a1)
          [Some (Expr t)]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"Unable to unpack FloatOp1 arg in Formula.Parser readApp"
      Just (Op1 Assignment BaseTypeRepr ('EmptyCtx ::> arg1)
arg_types sym -> SymExpr sym arg1 -> IO (SymExpr sym ret)
fn) -> do
        [Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
        forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, ShowF (SymExpr sym), ShowF ex, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment Assignment BaseTypeRepr ('EmptyCtx ::> arg1)
arg_types [Some (Expr t)]
args forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Assignment (Expr t) ctx
Ctx.Empty Ctx.:> Expr t tp
arg1 ->
            forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymExpr sym arg1 -> IO (SymExpr sym ret)
fn ExprBuilder t st fs
sym Expr t tp
arg1)
      Just (Op2 Assignment BaseTypeRepr (('EmptyCtx ::> arg1) ::> arg2)
arg_types sym -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret)
fn) -> do
        [Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
        forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, ShowF (SymExpr sym), ShowF ex, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment Assignment BaseTypeRepr (('EmptyCtx ::> arg1) ::> arg2)
arg_types [Some (Expr t)]
args forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Assignment (Expr t) ctx
Ctx.Empty Ctx.:> Expr t tp
arg1 Ctx.:> Expr t tp
arg2 ->
              forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret)
fn ExprBuilder t st fs
sym Expr t tp
arg1 Expr t tp
arg2)
      Just (Op3 Assignment BaseTypeRepr ((('EmptyCtx ::> arg1) ::> arg2) ::> arg3)
arg_types sym
-> SymExpr sym arg1
-> SymExpr sym arg2
-> SymExpr sym arg3
-> IO (SymExpr sym ret)
fn) -> do
        [Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
        forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, ShowF (SymExpr sym), ShowF ex, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment Assignment BaseTypeRepr ((('EmptyCtx ::> arg1) ::> arg2) ::> arg3)
arg_types [Some (Expr t)]
args forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Assignment (Expr t) ctx
Ctx.Empty Ctx.:> Expr t tp
arg1 Ctx.:> Expr t tp
arg2 Ctx.:> Expr t tp
arg3 ->
              forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymExpr sym arg1
-> SymExpr sym arg2
-> SymExpr sym arg3
-> IO (SymExpr sym ret)
fn ExprBuilder t st fs
sym Expr t tp
arg1 Expr t tp
arg2 Expr t tp
arg3)
      Just (Op4 Assignment
  BaseTypeRepr (((('EmptyCtx ::> arg1) ::> arg2) ::> arg3) ::> arg4)
arg_types sym
-> SymExpr sym arg1
-> SymExpr sym arg2
-> SymExpr sym arg3
-> SymExpr sym arg4
-> IO (SymExpr sym ret)
fn) -> do
        [Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
        forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, ShowF (SymExpr sym), ShowF ex, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment Assignment
  BaseTypeRepr (((('EmptyCtx ::> arg1) ::> arg2) ::> arg3) ::> arg4)
arg_types [Some (Expr t)]
args forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Assignment (Expr t) ctx
Ctx.Empty Ctx.:> Expr t tp
arg1 Ctx.:> Expr t tp
arg2 Ctx.:> Expr t tp
arg3 Ctx.:> Expr t tp
arg4 ->
              forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymExpr sym arg1
-> SymExpr sym arg2
-> SymExpr sym arg3
-> SymExpr sym arg4
-> IO (SymExpr sym ret)
fn ExprBuilder t st fs
sym Expr t tp
arg1 Expr t tp
arg2 Expr t tp
arg3 Expr t tp
arg4)
      Just (BVOp1 forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
op) -> do
        Some Expr t x
expr <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
operands
        BVProof NatRepr n
_ <- forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
expr
        forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
op ExprBuilder t st fs
sym Expr t x
expr
      Just (BVOp2 forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
op) -> do
        (Some Expr t x
arg1, Some Expr t x
arg2)  <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs [SExpr]
operands
        BVProof NatRepr n
m <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 1: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg1
        BVProof NatRepr n
n <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 2: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg2
        case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr n
m NatRepr n
n of
          Just n :~: n
Refl -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
op ExprBuilder t st fs
sym Expr t x
arg1 Expr t x
arg2)
          Maybe (n :~: n)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"arguments to %s must be the same length, \
                                         \but arg 1 has length %s \
                                         \and arg 2 has length %s"
                                         Text
operator
                                         (forall a. Show a => a -> String
show NatRepr n
m)
                                         (forall a. Show a => a -> String
show NatRepr n
n)
      Just (BVComp2 forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
op) -> do
        (Some Expr t x
arg1, Some Expr t x
arg2)  <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs [SExpr]
operands
        BVProof NatRepr n
m <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 1: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg1
        BVProof NatRepr n
n <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 2: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg2
        case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr n
m NatRepr n
n of
          Just n :~: n
Refl -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
op ExprBuilder t st fs
sym Expr t x
arg1 Expr t x
arg2)
          Maybe (n :~: n)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"arguments to %s must be the same length, \
                                         \but arg 1 has length %s \
                                         \and arg 2 has length %s"
                                         Text
operator
                                         (forall a. Show a => a -> String
show NatRepr n
m)
                                         (forall a. Show a => a -> String
show NatRepr n
n)
      Maybe (Op sym)
Nothing ->
        -- Operators/syntactic-forms with types too
        -- complicated to nicely fit in the Op type
        case Text
operator of
          Text
"concat" -> do
            (Some Expr t x
arg1, Some Expr t x
arg2)  <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs [SExpr]
operands
            BVProof NatRepr n
_ <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 1: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg1
            BVProof NatRepr n
_ <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 2: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg2
            forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Nat) (v :: Nat).
(IsExprBuilder sym, 1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
W4.bvConcat ExprBuilder t st fs
sym Expr t x
arg1 Expr t x
arg2)
          Text
"=" -> do
            (Some Expr t x
arg1, Some Expr t x
arg2)  <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs [SExpr]
operands
            case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arg1) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arg2) of
              Just x :~: x
Refl -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
W4.isEq ExprBuilder t st fs
sym Expr t x
arg1 Expr t x
arg2)
              Maybe (x :~: x)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$
                forall r. PrintfType r => String -> r
printf String
"arguments must have same types, \
                       \but arg 1 has type %s \
                       \and arg 2 has type %s"
                (forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arg1))
                (forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arg2))
          Text
"ite" -> do
            (Some Expr t x
test, Some Expr t x
then_, Some Expr t x
else_)  <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr]
-> Processor
     sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
readThreeArgs [SExpr]
operands
            case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
test of
              BaseTypeRepr x
BaseBoolRepr ->
                case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
then_) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
else_) of
                  Just x :~: x
Refl -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
W4.baseTypeIte ExprBuilder t st fs
sym Expr t x
test Expr t x
then_ Expr t x
else_)
                  Maybe (x :~: x)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$
                    forall r. PrintfType r => String -> r
printf String
"then and else branches must have same type, \
                           \but then has type %s \
                           \and else has type %s"
                    (forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
then_))
                    (forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
else_))
              BaseTypeRepr x
tp -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"test expression must be a boolean; got %s" (forall a. Show a => a -> String
show BaseTypeRepr x
tp)
          Text
"select" -> do
            (Some Expr t x
arr, Some Expr t x
idx)  <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs [SExpr]
operands
            ArraySingleDim BaseTypeRepr res
_ <- forall (m :: Type -> Type) (tp1 :: BaseType) (tp2 :: BaseType).
MonadError String m =>
BaseTypeRepr tp1 -> BaseTypeRepr tp2 -> m (ArrayJudgment tp1 tp2)
expectArrayWithIndex (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
idx) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arr)
            let idx' :: Assignment (Expr t) (SingleCtx x)
idx' = forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> Expr t x
idx
            forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> IO (SymExpr sym b)
W4.arrayLookup ExprBuilder t st fs
sym Expr t x
arr Assignment (Expr t) (SingleCtx x)
idx')
          Text
"store" -> do
            (Some Expr t x
arr, Some Expr t x
idx, Some Expr t x
expr)  <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr]
-> Processor
     sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
readThreeArgs [SExpr]
operands
            ArraySingleDim BaseTypeRepr res
resRepr <- forall (m :: Type -> Type) (tp1 :: BaseType) (tp2 :: BaseType).
MonadError String m =>
BaseTypeRepr tp1 -> BaseTypeRepr tp2 -> m (ArrayJudgment tp1 tp2)
expectArrayWithIndex (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
idx) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arr)
            case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality BaseTypeRepr res
resRepr (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
expr) of
              Just res :~: x
Refl ->
                let idx' :: Assignment (Expr t) (SingleCtx x)
idx' = forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> Expr t x
idx
                in forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
W4.arrayUpdate ExprBuilder t st fs
sym Expr t x
arr Assignment (Expr t) (SingleCtx x)
idx' Expr t x
expr)
              Maybe (res :~: x)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"Array result type %s does not match %s"
                         (forall a. Show a => a -> String
show BaseTypeRepr res
resRepr)
                         (forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
expr))
          Text
"updateArray" -> do
            (Some Expr t x
arr, Some Expr t x
idx, Some Expr t x
expr)  <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr]
-> Processor
     sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
readThreeArgs [SExpr]
operands
            ArraySingleDim BaseTypeRepr res
resRepr <- forall (m :: Type -> Type) (tp1 :: BaseType) (tp2 :: BaseType).
MonadError String m =>
BaseTypeRepr tp1 -> BaseTypeRepr tp2 -> m (ArrayJudgment tp1 tp2)
expectArrayWithIndex (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
idx) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arr)
            case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality BaseTypeRepr res
resRepr (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
expr) of
              Just res :~: x
Refl ->
                let idx' :: Assignment (Expr t) (SingleCtx x)
idx' = forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> Expr t x
idx
                in forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
W4.arrayUpdate ExprBuilder t st fs
sym Expr t x
arr Assignment (Expr t) (SingleCtx x)
idx' Expr t x
expr)
              Maybe (res :~: x)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"Array result type %s does not match %s"
                         (forall a. Show a => a -> String
show BaseTypeRepr res
resRepr)
                         (forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
expr))

          Text
"arrayMap" ->
            -- arrayMap(idxs, array)

            -- The list of indexes is a list of pairs where each pair is:
            --
            -- > (indexList, expr)


            -- Each list of indexes is a list of 'IndexLit' (since we have multi-dimensional indexing)
            case [SExpr]
operands of
              [SExpr
updateSExprList, SExpr
arrSExpr] -> do
                Some Expr t x
arrExpr <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
arrSExpr
                case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arrExpr of
                  BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idxReprs BaseTypeRepr xs
arrTyRepr -> do
                    ArrayUpdateMap (Expr t) (idx ::> tp) xs
updateMap <- forall sym t (st :: Type -> Type) fs (tp :: BaseType)
       (i :: Ctx BaseType) (itp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
Assignment BaseTypeRepr (i ::> itp)
-> BaseTypeRepr tp
-> SExpr
-> Processor sym (ArrayUpdateMap (SymExpr sym) (i ::> itp) tp)
expectArrayUpdateMap Assignment BaseTypeRepr (idx ::> tp)
idxReprs BaseTypeRepr xs
arrTyRepr SExpr
updateSExprList
                    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
W4.sbMakeExpr ExprBuilder t st fs
sym (forall (i :: Ctx BaseType) (itp :: BaseType) (tp1 :: BaseType)
       (e :: BaseType -> Type).
Assignment BaseTypeRepr (i ::> itp)
-> BaseTypeRepr tp1
-> ArrayUpdateMap e (i ::> itp) tp1
-> e (BaseArrayType (i ::> itp) tp1)
-> App e (BaseArrayType (i ::> itp) tp1)
W4.ArrayMap Assignment BaseTypeRepr (idx ::> tp)
idxReprs BaseTypeRepr xs
arrTyRepr ArrayUpdateMap (Expr t) (idx ::> tp) xs
updateMap Expr t x
arrExpr))
                  BaseTypeRepr x
repr -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected an array type for the value in 'arrayMap', but got", forall a. Show a => a -> String
show BaseTypeRepr x
repr]
              [SExpr]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected a list of indices and an array expression, but got", forall a. Show a => a -> String
show [SExpr]
operands]

          Text
"field" -> do
            case [SExpr]
operands of
              [SExpr
rawStruct, S.WFSAtom (AInt Integer
rawIdx)] -> do
                Some Expr t x
struct  <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
rawStruct
                case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
struct of
                  (BaseStructRepr Assignment BaseTypeRepr ctx
fldTpReprs) ->
                    case forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
Ctx.intIndex (forall a. Num a => Integer -> a
fromInteger Integer
rawIdx) (forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment BaseTypeRepr ctx
fldTpReprs) of
                      Just (Some Index ctx x
i) -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField ExprBuilder t st fs
sym Expr t x
struct Index ctx x
i)
                      Maybe (Some (Index ctx))
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$
                        [String] -> String
unwords [String
"invalid struct index, got", forall a. Show a => a -> String
show Assignment BaseTypeRepr ctx
fldTpReprs, String
"and", forall a. Show a => a -> String
show Integer
rawIdx]
                  BaseTypeRepr x
srepr -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected a struct, got", forall a. Show a => a -> String
show BaseTypeRepr x
srepr]
              [SExpr]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected an arg and an Int, got", forall a. Show a => a -> String
show [SExpr]
operands]
          Text
"struct" -> do
            case [SExpr]
operands of
              [S.WFSList [SExpr]
rawFldExprs] -> do
                Some Assignment (Expr t) x
flds <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (Assignment (SymExpr sym)))
readExprsAsAssignment [SExpr]
rawFldExprs
                forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym -> Assignment (SymExpr sym) flds -> IO (SymStruct sym flds)
W4.mkStruct ExprBuilder t st fs
sym Assignment (Expr t) x
flds)
              [SExpr]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"struct expects a single operand, got", forall a. Show a => a -> String
show [SExpr]
operands]
          Text
"sbvToInteger" -> do
            (Some Expr t x
arg) <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
operands
            BVProof NatRepr n
_ <- forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg
            forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
W4.sbvToInteger ExprBuilder t st fs
sym Expr t x
arg
          Text
"bvToInteger" -> do
            (Some Expr t x
arg) <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
operands
            BVProof NatRepr n
_ <- forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg
            forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
W4.bvToInteger ExprBuilder t st fs
sym Expr t x
arg
          Text
"integerToBV" -> do
            case [SExpr]
operands of
              [S.WFSAtom (ANat Nat
width), SExpr
rawValExpr] -> do
                Some Expr t x
x <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
rawValExpr
                case (Nat -> Some NatRepr
mkNatRepr Nat
width, forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
x) of
                  (Some NatRepr x
w, BaseTypeRepr x
BaseIntegerRepr)
                    | Just LeqProof 1 x
LeqProof <- forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w -> do
                    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
W4.integerToBV ExprBuilder t st fs
sym Expr t x
x NatRepr x
w)
                  (Some NatRepr, BaseTypeRepr x)
srepr -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected a non-zero natural and an integer, got", forall a. Show a => a -> String
show (Some NatRepr, BaseTypeRepr x)
srepr]
              [SExpr]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"integerToBV expects two operands, the first of which is a nat, got", forall a. Show a => a -> String
show [SExpr]
operands]
          Text
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"couldn't parse application of %s" (Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty SExpr
opRaw)
-- Parse an expression of the form @((_ extract i j) x)@.
readApp (S.WFSList [S.WFSAtom (AId Text
"_"), S.WFSAtom (AId Text
"extract"), S.WFSAtom (AInt Integer
iInt), S.WFSAtom (AInt Integer
jInt)])
  [SExpr]
args = forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in reading extract expression: " forall a b. (a -> b) -> a -> b
$ do
  ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
  (Some Expr t x
arg) <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
args
  -- The SMT-LIB spec represents extracts differently than Crucible does. Per
  -- SMT: "extraction of bits i down to j from a bitvector of size m to yield a
  -- new bitvector of size n, where n = i - j + 1". Per Crucible:
  --
  -- > -- | Select a subsequence from a bitvector.
  -- > bvSelect :: (1 <= n, idx + n <= w)
  -- >          => sym
  -- >          -> NatRepr idx  -- ^ Starting index, from 0 as least significant bit
  -- >          -> NatRepr n    -- ^ Number of bits to take
  -- >          -> SymBV sym w  -- ^ Bitvector to select from
  -- >          -> IO (SymBV sym n)
  --
  -- The "starting index" seems to be from the bottom, so that (in slightly
  -- pseudocode)
  --
  -- > > bvSelect sym 0 8 (0x01020304:[32])
  -- > 0x4:[8]
  -- > > bvSelect sym 24 8 (0x01020304:[32])
  -- > 0x1:[8]
  --
  -- Thus, n = i - j + 1, and idx = j.
  let nInt :: Integer
nInt = Integer
iInt forall a. Num a => a -> a -> a
- Integer
jInt forall a. Num a => a -> a -> a
+ Integer
1
      idxInt :: Integer
idxInt = Integer
jInt
  Some NatRepr x
nNat <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in calculating extract length: " forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type).
MonadError String m =>
Integer -> m (Some NatRepr)
intToNatM Integer
nInt
  Some NatRepr x
idxNat <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in extract lower bound: " forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type).
MonadError String m =>
Integer -> m (Some NatRepr)
intToNatM Integer
idxInt
  LeqProof 1 x
LeqProof <- forall e (m :: Type -> Type) a.
MonadError e m =>
e -> Maybe a -> m a
fromMaybeError String
"extract length must be positive" forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
nNat
  BVProof NatRepr n
lenNat <- forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg
  LeqProof (x + x) n
LeqProof <- forall e (m :: Type -> Type) a.
MonadError e m =>
e -> Maybe a -> m a
fromMaybeError String
"invalid extract for given bitvector" forall a b. (a -> b) -> a -> b
$
    forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr x
idxNat NatRepr x
nNat) NatRepr n
lenNat
  forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (idx :: Nat) (n :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
W4.bvSelect ExprBuilder t st fs
sym NatRepr x
idxNat NatRepr x
nNat Expr t x
arg)
-- Parse an expression of the form @((_ zero_extend i) x)@ or @((_ sign_extend i) x)@.
readApp (S.WFSList [S.WFSAtom (AId Text
"_"), S.WFSAtom (AId Text
extend), S.WFSAtom (AInt Integer
iInt)])
  [SExpr]
args
  | Text
extend forall a. Eq a => a -> a -> Bool
== Text
"zero_extend" Bool -> Bool -> Bool
||
    Text
extend forall a. Eq a => a -> a -> Bool
== Text
"sign_extend" = forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError (forall r. PrintfType r => String -> r
printf String
"in reading %s expression: " Text
extend) forall a b. (a -> b) -> a -> b
$ do
      ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
      Some Expr t x
arg <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
args
      Some NatRepr x
iNat <- forall (m :: Type -> Type).
MonadError String m =>
Integer -> m (Some NatRepr)
intToNatM Integer
iInt
      LeqProof 1 x
iPositive <- forall e (m :: Type -> Type) a.
MonadError e m =>
e -> Maybe a -> m a
fromMaybeError String
"must extend by a positive length" forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
iNat
      BVProof NatRepr n
lenNat <- forall (ex :: BaseType -> Type) (m :: Type -> Type)
       (tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg
      let newLen :: NatRepr (n + x)
newLen = forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr n
lenNat NatRepr x
iNat
      forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (m :: Nat) (n :: Nat) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 (forall (f :: Nat -> Type) (n :: Nat). f n -> LeqProof n n
leqRefl NatRepr n
lenNat) LeqProof 1 x
iPositive) forall a b. (a -> b) -> a -> b
$
        let op :: ExprBuilder t st fs
-> NatRepr (n + x)
-> SymBV (ExprBuilder t st fs) n
-> IO (SymBV (ExprBuilder t st fs) (n + x))
op = if Text
extend forall a. Eq a => a -> a -> Bool
== Text
"zero_extend" then forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
W4.bvZext else forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
W4.bvSext
        in forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr (n + x)
-> SymBV (ExprBuilder t st fs) n
-> IO (SymBV (ExprBuilder t st fs) (n + x))
op ExprBuilder t st fs
sym NatRepr (n + x)
newLen Expr t x
arg
readApp (S.WFSList [S.WFSAtom (AId Text
"_"), S.WFSAtom (AId Text
"bvfill"), S.WFSAtom (AInt Integer
width)]) [SExpr]
args =
  forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in reading bvfill expression" forall a b. (a -> b) -> a -> b
$ do
    ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
    Some Expr t x
arg <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
args
    case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arg of
      BaseTypeRepr x
BaseBoolRepr -> do
        Some NatRepr x
widthRep <- forall (m :: Type -> Type).
MonadError String m =>
Integer -> m (Some NatRepr)
intToNatM Integer
width
        LeqProof 1 x
LeqProof <- forall e (m :: Type -> Type) a.
MonadError e m =>
e -> Maybe a -> m a
fromMaybeError String
"must extend by a positive length" forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
widthRep
        forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> Pred sym -> IO (SymBV sym w)
W4.bvFill ExprBuilder t st fs
sym NatRepr x
widthRep Expr t x
arg)
      BaseTypeRepr x
tyrep -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"Invalid argument type to bvFill: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BaseTypeRepr x
tyrep)
readApp SExpr
rator [SExpr]
rands = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"readApp could not parse the following: "
                                      forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.WFSList (SExpr
ratorforall a. a -> [a] -> [a]
:[SExpr]
rands))))


-- | Try converting an 'Integer' to a 'NatRepr' or throw an error if not
-- possible.
intToNatM :: (E.MonadError String m) => Integer -> m (Some NatRepr)
intToNatM :: forall (m :: Type -> Type).
MonadError String m =>
Integer -> m (Some NatRepr)
intToNatM = forall e (m :: Type -> Type) a.
MonadError e m =>
e -> Maybe a -> m a
fromMaybeError String
"integer must be non-negative to be a nat" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Maybe (Some NatRepr)
someNat

-- | Parse a list of array updates where each entry in the list is:
--
-- > (idxs, elt)
--
-- where each @idxs@ is a list (assignment) of indexes (with type @idxReprs@)
-- and each element is an expr.
--
-- NOTE: We assume that there are no duplicates in the list and apply the
-- updates in an arbitrary order.  This is true for any map serialized by this
-- library.
expectArrayUpdateMap
  :: forall sym t st fs tp i itp
   . (sym ~ W4.ExprBuilder t st fs)
  => Ctx.Assignment BaseTypeRepr (i Ctx.::> itp)
  -> BaseTypeRepr tp
  -> SExpr
  -> Processor sym (WAU.ArrayUpdateMap (W4.SymExpr sym) (i Ctx.::> itp) tp)
expectArrayUpdateMap :: forall sym t (st :: Type -> Type) fs (tp :: BaseType)
       (i :: Ctx BaseType) (itp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
Assignment BaseTypeRepr (i ::> itp)
-> BaseTypeRepr tp
-> SExpr
-> Processor sym (ArrayUpdateMap (SymExpr sym) (i ::> itp) tp)
expectArrayUpdateMap Assignment BaseTypeRepr (i ::> itp)
idxReprs BaseTypeRepr tp
arrTyRepr SExpr
updateSExprList =
  case SExpr
updateSExprList of
    S.L [SExpr]
items -> forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
F.foldrM SExpr
-> ArrayUpdateMap (Expr t) (i ::> itp) tp
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (ArrayUpdateMap (Expr t) (i ::> itp) tp)
expectArrayUpdateEntry forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
       (tp :: BaseType).
ArrayUpdateMap e ctx tp
WAU.empty [SExpr]
items
    SExpr
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"Expected a list of array element updates in ArrayMap"
  where
    expectArrayUpdateEntry :: SExpr
-> ArrayUpdateMap (Expr t) (i ::> itp) tp
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (ArrayUpdateMap (Expr t) (i ::> itp) tp)
expectArrayUpdateEntry SExpr
pair ArrayUpdateMap (Expr t) (i ::> itp) tp
updateMap =
      case SExpr
pair of
        S.L [S.L [SExpr]
idxListExprs, SExpr
elt] -> do
          Assignment IndexLit (i ::> itp)
idxs <- forall {k} (m :: Type -> Type) (ctx :: Ctx k) (f :: k -> Type)
       (g :: k -> Type).
Applicative m =>
(forall (tp :: k). Index ctx tp -> f tp -> m (g tp))
-> Assignment f ctx -> m (Assignment g ctx)
Ctx.traverseWithIndex (forall (ctx :: Ctx BaseType) (tp :: BaseType) sym.
[SExpr]
-> Index ctx tp -> BaseTypeRepr tp -> Processor sym (IndexLit tp)
parseIndexLit [SExpr]
idxListExprs) Assignment BaseTypeRepr (i ::> itp)
idxReprs
          Some Expr t x
x <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
elt
          case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality BaseTypeRepr tp
arrTyRepr (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
x) of
            Just tp :~: x
Refl -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (e :: BaseType -> Type) (tp :: BaseType)
       (ctx :: Ctx BaseType).
(HashableF e, HasAbsValue e) =>
BaseTypeRepr tp
-> Assignment IndexLit ctx
-> e tp
-> ArrayUpdateMap e ctx tp
-> ArrayUpdateMap e ctx tp
WAU.insert BaseTypeRepr tp
arrTyRepr Assignment IndexLit (i ::> itp)
idxs Expr t x
x ArrayUpdateMap (Expr t) (i ::> itp) tp
updateMap)
            Maybe (tp :~: x)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [ String
"Invalid element type in ArrayMap update: expected "
                                            , forall a. Show a => a -> String
show BaseTypeRepr tp
arrTyRepr
                                            , String
" but got "
                                            , forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
x)])
        SExpr
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"Unexpected ArrayMap update item structure"

-- | Safe list indexing
--
-- This version only traverses the list once (compared to computing the length
-- and then using unsafe indexing)
(!?) :: [a] -> Int -> Maybe a
[a]
lst !? :: forall a. [a] -> Int -> Maybe a
!? Int
idx
  | Int
idx forall a. Ord a => a -> a -> Bool
< Int
0 = forall a. Maybe a
Nothing
  | Bool
otherwise = forall {t} {a}. (Eq t, Num t) => t -> [a] -> Maybe a
go Int
idx [a]
lst
  where
    go :: t -> [a] -> Maybe a
go t
0 (a
x:[a]
_xs) = forall a. a -> Maybe a
Just a
x
    go t
i (a
_:[a]
xs) = t -> [a] -> Maybe a
go (t
i forall a. Num a => a -> a -> a
- t
1) [a]
xs
    go t
_ [] = forall a. Maybe a
Nothing

-- | Parse a single 'WIL.IndexLit' out of a list of 'SExpr' (at the named index)
--
-- This is used to build the assignment of indexes
parseIndexLit :: [SExpr]
               -> Ctx.Index ctx tp
               -> BaseTypeRepr tp
               -> Processor sym (WIL.IndexLit tp)
parseIndexLit :: forall (ctx :: Ctx BaseType) (tp :: BaseType) sym.
[SExpr]
-> Index ctx tp -> BaseTypeRepr tp -> Processor sym (IndexLit tp)
parseIndexLit [SExpr]
exprs Index ctx tp
idx BaseTypeRepr tp
repr
  | Just (S.A Atom
atom) <- [SExpr]
exprs forall a. [a] -> Int -> Maybe a
!? forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal Index ctx tp
idx =
      case (BaseTypeRepr tp
repr, Atom
atom) of
        (BaseBVRepr NatRepr w
w, ABV Int
w' Integer
val)
          | forall (n :: Nat). NatRepr n -> Integer
PN.intValue NatRepr w
w forall a. Eq a => a -> a -> Bool
== forall a. Integral a => a -> Integer
toInteger Int
w' ->
            forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BV w -> IndexLit ('BaseBVType w)
WIL.BVIndexLit NatRepr w
w (forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
val))
          | Bool
otherwise -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"Array update index bitvector size mismatch: expected " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show NatRepr w
w forall a. [a] -> [a] -> [a]
++ String
" but got " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
w')
        (BaseTypeRepr tp
BaseIntegerRepr, AInt Integer
i) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (Integer -> IndexLit 'BaseIntegerType
WIL.IntIndexLit Integer
i)
        (BaseTypeRepr tp, Atom)
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"Unexpected array update index type: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BaseTypeRepr tp
repr)
  | Bool
otherwise = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"Invalid or missing array update index at " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Index ctx tp
idx)

data ArrayJudgment :: BaseType -> BaseType -> Type where
  ArraySingleDim :: forall idx res.
                    BaseTypeRepr res
                 -> ArrayJudgment idx (BaseArrayType (Ctx.SingleCtx idx) res)

expectArrayWithIndex :: (E.MonadError String m) => BaseTypeRepr tp1 -> BaseTypeRepr tp2 -> m (ArrayJudgment tp1 tp2)
expectArrayWithIndex :: forall (m :: Type -> Type) (tp1 :: BaseType) (tp2 :: BaseType).
MonadError String m =>
BaseTypeRepr tp1 -> BaseTypeRepr tp2 -> m (ArrayJudgment tp1 tp2)
expectArrayWithIndex BaseTypeRepr tp1
dimRepr (BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idxTpReprs BaseTypeRepr xs
resRepr) =
  case forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
Ctx.viewAssign Assignment BaseTypeRepr (idx ::> tp)
idxTpReprs of
    Ctx.AssignExtend Assignment BaseTypeRepr ctx1
rest BaseTypeRepr tp
idxTpRepr ->
      case forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
Ctx.viewAssign Assignment BaseTypeRepr ctx1
rest of
        AssignView BaseTypeRepr ctx1
Ctx.AssignEmpty ->
          case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality BaseTypeRepr tp
idxTpRepr BaseTypeRepr tp1
dimRepr of
            Just tp :~: tp1
Refl -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (idx :: BaseType) (res :: BaseType).
BaseTypeRepr res
-> ArrayJudgment idx (BaseArrayType (SingleCtx idx) res)
ArraySingleDim BaseTypeRepr xs
resRepr
            Maybe (tp :~: tp1)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"Array index type", forall a. Show a => a -> String
show BaseTypeRepr tp
idxTpRepr,
                                               String
"does not match", forall a. Show a => a -> String
show BaseTypeRepr tp1
dimRepr]
        AssignView BaseTypeRepr ctx1
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"multidimensional arrays are not supported"
expectArrayWithIndex BaseTypeRepr tp1
_ BaseTypeRepr tp2
repr = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected an array, got", forall a. Show a => a -> String
show BaseTypeRepr tp2
repr]

exprAssignment ::
  forall sym ctx ex . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym), ShowF ex, W4.IsExpr ex)
  => Ctx.Assignment BaseTypeRepr ctx
  -> [Some ex]
  -> Processor sym (Ctx.Assignment ex ctx)
exprAssignment :: forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, ShowF (SymExpr sym), ShowF ex, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment Assignment BaseTypeRepr ctx
tpAssns [Some ex]
exs = do
  Some Assignment ex x
exsAsn <- forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList [Some ex]
exs
  Assignment BaseTypeRepr x
exsRepr <- forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
FC.fmapFC forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Assignment ex x
exsAsn
  case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Assignment BaseTypeRepr x
exsRepr Assignment BaseTypeRepr ctx
tpAssns of
    Just x :~: ctx
Refl -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Assignment ex x
exsAsn
    Maybe (x :~: ctx)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$
      String
"Unexpected expression types for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Assignment ex x
exsAsn
      forall a. [a] -> [a] -> [a]
++ String
"\nExpected: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Assignment BaseTypeRepr ctx
tpAssns
      forall a. [a] -> [a] -> [a]
++ String
"\nGot: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Assignment BaseTypeRepr x
exsRepr


-- | Given the s-expressions for the bindings and body of a
-- let, parse the bindings into the Reader monad's state and
-- then parse the body with those newly bound variables.
readLetExpr ::
  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
  => [SExpr]
  -- ^ Bindings in a let-expression.
  -> SExpr
  -- ^ Body of the let-expression.
  -> Processor sym (Some (W4.SymExpr sym))
readLetExpr :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
readLetExpr [] SExpr
body = forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
body
readLetExpr ((S.WFSList [S.WFSAtom (AId Text
x), SExpr
e]):[SExpr]
rst) SExpr
body = do
  Some (Expr t)
v <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
e
  forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
R.local (\ProcessorEnv (ExprBuilder t st fs)
c -> ProcessorEnv (ExprBuilder t st fs)
c {procLetEnv :: HashMap Text (Some (SymExpr (ExprBuilder t st fs)))
procLetEnv = (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HM.insert Text
x Some (Expr t)
v) forall a b. (a -> b) -> a -> b
$ forall sym. ProcessorEnv sym -> HashMap Text (Some (SymExpr sym))
procLetEnv ProcessorEnv (ExprBuilder t st fs)
c}) forall a b. (a -> b) -> a -> b
$
    forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
readLetExpr [SExpr]
rst SExpr
body
readLetExpr [SExpr]
bindings SExpr
_body = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$
  String
"invalid s-expression for let-bindings: " forall a. [a] -> [a] -> [a]
++ (forall a. Show a => a -> String
show [SExpr]
bindings)


readLetFnExpr ::
  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
  => [SExpr]
  -- ^ Bindings in a let-expression.
  -> SExpr
  -- ^ Body of the let-expression.
  -> Processor sym (Some (W4.SymExpr sym))
readLetFnExpr :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
readLetFnExpr [] SExpr
body = forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
body
readLetFnExpr ((S.WFSList [S.WFSAtom (AId Text
f), SExpr
e]):[SExpr]
rst) SExpr
body = do
  SomeSymFn sym
v <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (SomeSymFn sym)
readSymFn SExpr
e
  forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
R.local (\ProcessorEnv sym
c -> ProcessorEnv sym
c {procLetFnEnv :: HashMap Text (SomeSymFn sym)
procLetFnEnv = (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HM.insert Text
f SomeSymFn sym
v) forall a b. (a -> b) -> a -> b
$ forall sym. ProcessorEnv sym -> HashMap Text (SomeSymFn sym)
procLetFnEnv ProcessorEnv sym
c}) forall a b. (a -> b) -> a -> b
$
    forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
readLetExpr [SExpr]
rst SExpr
body
readLetFnExpr [SExpr]
bindings SExpr
_body = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$
  String
"invalid s-expression for let-bindings: " forall a. [a] -> [a] -> [a]
++ (forall a. Show a => a -> String
show [SExpr]
bindings)


-- | Parse an arbitrary expression.
readExpr ::
  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
  => SExpr
  -> Processor sym (Some (W4.SymExpr sym))
readExpr :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr (S.WFSAtom (AInt Integer
n)) = do
  ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
  forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit ExprBuilder t st fs
sym Integer
n)
readExpr (S.WFSAtom (ANat Nat
_)) =
  forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"Bare Natural literals are no longer used"
readExpr (S.WFSAtom (ABool Bool
b)) = do
  ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
  forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
W4.backendPred ExprBuilder t st fs
sym Bool
b
readExpr (S.WFSAtom (AFloat (Some FloatPrecisionRepr x
repr) BigFloat
bf)) = do
  ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
  forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
W4.floatLit ExprBuilder t st fs
sym FloatPrecisionRepr x
repr BigFloat
bf)
readExpr (S.WFSAtom (AStr Some StringInfoRepr
prefix Text
content)) = do
  ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
  case Some StringInfoRepr
prefix of
    (Some StringInfoRepr x
W4.UnicodeRepr) -> do
      Expr t (BaseStringType 'Unicode)
s <- forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
W4.stringLit ExprBuilder t st fs
sym forall a b. (a -> b) -> a -> b
$ Text -> StringLiteral 'Unicode
W4.UnicodeLiteral Text
content
      forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall a b. (a -> b) -> a -> b
$ Expr t (BaseStringType 'Unicode)
s
    (Some StringInfoRepr x
W4.Char8Repr) -> do
      Expr t (BaseStringType 'Char8)
s <- forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
W4.stringLit ExprBuilder t st fs
sym forall a b. (a -> b) -> a -> b
$ ByteString -> StringLiteral 'Char8
W4.Char8Literal forall a b. (a -> b) -> a -> b
$ Text -> ByteString
T.encodeUtf8 Text
content
      forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall a b. (a -> b) -> a -> b
$ Expr t (BaseStringType 'Char8)
s
    (Some StringInfoRepr x
W4.Char16Repr) -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"Char16 strings are not yet supported"
readExpr (S.WFSAtom (AReal Rational
_)) = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"TODO: support readExpr for real literals"
readExpr (S.WFSAtom (ABV Int
len Integer
val)) = do
  -- This is a bitvector literal.
  ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
  -- The following two patterns should never fail, given that during parsing we
  -- can only construct BVs with positive length.
  case forall a. Integral a => a -> Maybe (Some NatRepr)
someNat (forall a. Integral a => a -> Integer
toInteger Int
len) of
    Just (Some NatRepr x
lenRepr) -> do
        LeqProof 1 x
pf <- case forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
lenRepr of
                Just LeqProof 1 x
pf -> forall (m :: Type -> Type) a. Monad m => a -> m a
return LeqProof 1 x
pf
                Maybe (LeqProof 1 x)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"What4.Serialize.Parser.readExpr isPosNat failure"
        forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (m :: Nat) (n :: Nat) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof LeqProof 1 x
pf (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit ExprBuilder t st fs
sym NatRepr x
lenRepr (forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr x
lenRepr Integer
val))
    Maybe (Some NatRepr)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"SemMC.Formula.Parser.readExpr someNat failure"
  -- Just (Some lenRepr) <- return $ someNat (toInteger len)
  -- let Just pf = isPosNat lenRepr
  -- liftIO $ withLeqProof pf (Some <$> W4.bvLit sym lenRepr val)
-- Let-bound variable
readExpr (S.WFSAtom (AId Text
name)) = do
  Maybe (Some (Expr t))
maybeBinding <- forall sym. Text -> Processor sym (Maybe (Some (SymExpr sym)))
lookupExpr Text
name
  -- We first check the local lexical environment (i.e., the
  -- in-scope let-bindings) before consulting the "global"
  -- scope.
  case Maybe (Some (Expr t))
maybeBinding of
    -- simply return it's bound value
    Just Some (Expr t)
binding -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Some (Expr t)
binding
    Maybe (Some (Expr t))
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"Unbound variable encountered during deserialization: "
                               forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack Text
name))
readExpr (S.WFSList ((S.WFSAtom (AId Text
"let")):[SExpr]
rhs)) =
  case [SExpr]
rhs of
    [S.WFSList [SExpr]
bindings, SExpr
body] -> forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
readLetExpr [SExpr]
bindings SExpr
body
    [SExpr]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"ill-formed let s-expression"
readExpr (S.WFSList ((S.WFSAtom (AId Text
"letfn")):[SExpr]
rhs)) =
  case [SExpr]
rhs of
    [S.WFSList [SExpr]
bindings, SExpr
body] -> forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
readLetFnExpr [SExpr]
bindings SExpr
body
    [SExpr]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"ill-formed letfn s-expression"
readExpr (S.WFSList []) = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"ill-formed empty s-expression"
readExpr (S.WFSList (SExpr
operator:[SExpr]
operands)) = forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> [SExpr] -> Processor sym (Some (SymExpr sym))
readApp SExpr
operator [SExpr]
operands



-- | Parse multiple expressions in a list.
readExprs ::
  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
  => [SExpr]
  -> Processor sym [Some (W4.SymExpr sym)]
readExprs :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
exprs = forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr [SExpr]
exprs

readExprsAsAssignment ::
  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
  => [SExpr]
  -> Processor sym (Some (Ctx.Assignment (W4.SymExpr sym)))
readExprsAsAssignment :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (Assignment (SymExpr sym)))
readExprsAsAssignment [SExpr]
exprs = forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
exprs


readFnType ::
  forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))
  => SExpr
  -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
readFnType :: forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
SExpr -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
readFnType (S.WFSList ((S.WFSAtom (AId Text
"->")):[SExpr]
typeSExprs)) =
  case forall a. [a] -> Maybe ([a], a)
unsnoc [SExpr]
typeSExprs of
    Maybe ([SExpr], SExpr)
Nothing ->
      forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"invalid type signature for function: "
                      forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty (forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [SExpr]
typeSExprs)))
    Just ([SExpr]
domSExps, SExpr
retSExp) -> do
      [Some BaseTypeRepr]
dom <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some BaseTypeRepr)
readBaseType [SExpr]
domSExps
      Some BaseTypeRepr
ret <- forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some BaseTypeRepr)
readBaseType SExpr
retSExp
      forall (m :: Type -> Type) a. Monad m => a -> m a
return ([Some BaseTypeRepr]
dom, Some BaseTypeRepr
ret)
readFnType SExpr
sexpr =
  forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"invalid type signature for function: "
                  forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty SExpr
sexpr))

-- | If the list is empty, return 'Nothing'. If the list is non-empty, return
-- @'Just' (xs, x)@, where @xs@ is equivalent to calling 'init' on the list and
-- @x@ is equivalent to calling 'last' on the list.
unsnoc :: [a] -> Maybe ([a], a)
unsnoc :: forall a. [a] -> Maybe ([a], a)
unsnoc []     = forall a. Maybe a
Nothing
unsnoc (a
x:[a]
xs) = case forall a. [a] -> Maybe ([a], a)
unsnoc [a]
xs of
                  Maybe ([a], a)
Nothing    -> forall a. a -> Maybe a
Just ([], a
x)
                  Just ([a]
a,a
b) -> forall a. a -> Maybe a
Just (a
xforall a. a -> [a] -> [a]
:[a]
a, a
b)

readFnArgs ::
  forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))
  => [SExpr]
  -> Processor sym [Text]
readFnArgs :: forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
[SExpr] -> Processor sym [Text]
readFnArgs [] = forall (m :: Type -> Type) a. Monad m => a -> m a
return []
readFnArgs ((S.WFSAtom (AId Text
name)):[SExpr]
rest) = do
  [Text]
names <- (forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
[SExpr] -> Processor sym [Text]
readFnArgs [SExpr]
rest)
  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Text
nameforall a. a -> [a] -> [a]
:[Text]
names
readFnArgs (SExpr
badArg:[SExpr]
_) =
  forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"invalid function argument encountered: "
                  forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty SExpr
badArg))

someVarExpr ::
    forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))
  => sym
  -> Some (W4.BoundVar sym)
  -> Some (W4.SymExpr sym)
someVarExpr :: forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
sym -> Some (BoundVar sym) -> Some (SymExpr sym)
someVarExpr sym
sym (Some BoundVar sym x
bv) = forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> SymExpr sym tp
W4.varExpr sym
sym BoundVar sym x
bv)


readSymFn ::
  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
  => SExpr
  -> Processor sym (SomeSymFn sym)
readSymFn :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (SomeSymFn sym)
readSymFn (S.WFSList [ S.WFSAtom (AId Text
"definedfn")
                     , S.WFSAtom (AStr Some StringInfoRepr
_ Text
rawSymFnName)
                     , SExpr
rawFnType
                     , S.WFSList [SExpr]
argVarsRaw
                     , SExpr
bodyRaw
                     ]) = do
  ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
  SolverSymbol
symFnName <- case String -> Either SolverSymbolError SolverSymbol
W4.userSymbol (Text -> String
T.unpack Text
rawSymFnName) of
                 Left SolverSymbolError
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"Bad symbolic function name : "
                                           forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack Text
rawSymFnName))
                 Right SolverSymbol
solverSym -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SolverSymbol
solverSym
  [Text]
argNames <- forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
[SExpr] -> Processor sym [Text]
readFnArgs [SExpr]
argVarsRaw
  ([Some BaseTypeRepr]
argTys, Some BaseTypeRepr
_retTy) <- forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
SExpr -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
readFnType SExpr
rawFnType
  forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Some BaseTypeRepr]
argTys forall a. Eq a => a -> a -> Bool
== forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Text]
argNames)) forall a b. (a -> b) -> a -> b
$
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"Function type expected "
    forall a. [a] -> [a] -> [a]
++ (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Some BaseTypeRepr]
argTys)
    forall a. [a] -> [a] -> [a]
++ String
" args but found "
    forall a. [a] -> [a] -> [a]
++ (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Text]
argNames)
  [Some (BoundVar (ExprBuilder t st fs))]
argVars <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Text
name, (Some BaseTypeRepr x
ty)) ->
                     case String -> Either SolverSymbolError SolverSymbol
W4.userSymbol (Text -> String
T.unpack Text
name) of
                       Left SolverSymbolError
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"Bad arg name : " forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack Text
name)
                       Right SolverSymbol
solverSym -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
W4.freshBoundVar ExprBuilder t st fs
sym SolverSymbol
solverSym BaseTypeRepr x
ty)
             forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
argNames [Some BaseTypeRepr]
argTys
  (Some Expr t x
body) <- let newBindings :: HashMap Text (Some (SymExpr (ExprBuilder t st fs)))
newBindings = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HM.fromList
                                   forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
argNames
                                   forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
sym -> Some (BoundVar sym) -> Some (SymExpr sym)
someVarExpr ExprBuilder t st fs
sym) [Some (BoundVar (ExprBuilder t st fs))]
argVars
                 in forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
R.local
                    (\ProcessorEnv (ExprBuilder t st fs)
env -> ProcessorEnv (ExprBuilder t st fs)
env {procLetEnv :: HashMap Text (Some (SymExpr (ExprBuilder t st fs)))
procLetEnv = forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
HM.union (forall sym. ProcessorEnv sym -> HashMap Text (Some (SymExpr sym))
procLetEnv ProcessorEnv (ExprBuilder t st fs)
env) HashMap Text (Some (SymExpr (ExprBuilder t st fs)))
newBindings})
                    forall a b. (a -> b) -> a -> b
$ forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
bodyRaw
  Some Assignment (ExprBoundVar t) x
argVarAssignment <- forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList [Some (BoundVar (ExprBuilder t st fs))]
argVars
  ExprSymFn t x x
symFn <- forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Assignment (BoundVar sym) args
-> SymExpr sym ret
-> UnfoldPolicy
-> IO (SymFn sym args ret)
W4.definedFn ExprBuilder t st fs
sym SolverSymbol
symFnName Assignment (ExprBoundVar t) x
argVarAssignment Expr t x
body UnfoldPolicy
W4.UnfoldConcrete
  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t (dom :: Ctx BaseType) (ret :: BaseType).
SymFn t dom ret -> SomeSymFn t
SomeSymFn ExprSymFn t x x
symFn
readSymFn badSExp :: SExpr
badSExp@(S.WFSList ((S.WFSAtom (AId Text
"definedfn")):[SExpr]
_)) =
  forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"invalid `definedfn`: " forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty SExpr
badSExp))
readSymFn (S.WFSList [ S.WFSAtom (AId Text
"uninterpfn")
                     , S.WFSAtom (AStr Some StringInfoRepr
_ Text
rawSymFnName)
                     , SExpr
rawFnType
                     ]) = do
  ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
  SolverSymbol
symFnName <- case String -> Either SolverSymbolError SolverSymbol
W4.userSymbol (Text -> String
T.unpack Text
rawSymFnName) of
                 Left SolverSymbolError
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"Bad symbolic function name : "
                                           forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack Text
rawSymFnName))
                 Right SolverSymbol
solverSym -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SolverSymbol
solverSym
  ([Some BaseTypeRepr]
argTys, (Some BaseTypeRepr x
retTy)) <- forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
SExpr -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
readFnType SExpr
rawFnType
  Some Assignment BaseTypeRepr x
domain <- forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList [Some BaseTypeRepr]
argTys
  ExprSymFn t x x
symFn <- forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
W4.freshTotalUninterpFn ExprBuilder t st fs
sym SolverSymbol
symFnName Assignment BaseTypeRepr x
domain BaseTypeRepr x
retTy
  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t (dom :: Ctx BaseType) (ret :: BaseType).
SymFn t dom ret -> SomeSymFn t
SomeSymFn ExprSymFn t x x
symFn
readSymFn badSExp :: SExpr
badSExp@(S.WFSList ((S.WFSAtom (AId Text
"uninterpfn")):[SExpr]
_)) =
  forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"invalid `uninterpfn`: " forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty SExpr
badSExp))
readSymFn SExpr
sexpr = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"invalid function definition: "
                                forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty SExpr
sexpr))