{-# 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 = IO (Maybe (SomeSymFn sym)) -> Text -> IO (Maybe (SomeSymFn sym))
forall a b. a -> b -> a
const (Maybe (SomeSymFn sym) -> IO (Maybe (SomeSymFn sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (SomeSymFn sym)
forall a. Maybe a
Nothing)
                            , cExprLookup :: Text -> IO (Maybe (Some (SymExpr sym)))
cExprLookup = IO (Maybe (Some (SymExpr sym)))
-> Text -> IO (Maybe (Some (SymExpr sym)))
forall a b. a -> b -> a
const (Maybe (Some (SymExpr sym)) -> IO (Maybe (Some (SymExpr sym)))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (Some (SymExpr sym))
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 = ReaderT (ProcessorEnv sym) IO (Either String a)
-> ProcessorEnv sym -> IO (Either String a)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
R.runReaderT (Processor sym a -> ReaderT (ProcessorEnv sym) IO (Either String a)
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
  userLookupFn <- (ProcessorEnv sym -> Text -> IO (Maybe (Some (SymExpr sym))))
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Text -> IO (Maybe (Some (SymExpr sym))))
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.asks ProcessorEnv sym -> Text -> IO (Maybe (Some (SymExpr sym)))
forall sym.
ProcessorEnv sym -> Text -> IO (Maybe (Some (SymExpr sym)))
procExprLookup
  letEnv <- R.asks procLetEnv
  case HM.lookup nm letEnv of
    Maybe (Some (SymExpr sym))
Nothing -> IO (Maybe (Some (SymExpr sym)))
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Maybe (Some (SymExpr sym)))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe (Some (SymExpr sym)))
 -> ExceptT
      String
      (ReaderT (ProcessorEnv sym) IO)
      (Maybe (Some (SymExpr sym))))
-> IO (Maybe (Some (SymExpr sym)))
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Maybe (Some (SymExpr sym)))
forall a b. (a -> b) -> a -> b
$ Text -> IO (Maybe (Some (SymExpr sym)))
userLookupFn Text
nm
    Maybe (Some (SymExpr sym))
res -> Maybe (Some (SymExpr sym))
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Maybe (Some (SymExpr sym)))
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
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
  userLookupFn <- (ProcessorEnv sym -> Text -> IO (Maybe (SomeSymFn sym)))
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Text -> IO (Maybe (SomeSymFn sym)))
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.asks ProcessorEnv sym -> Text -> IO (Maybe (SomeSymFn sym))
forall sym. ProcessorEnv sym -> Text -> IO (Maybe (SomeSymFn sym))
procSymFnLookup
  letEnv <- R.asks procLetFnEnv
  case HM.lookup nm letEnv of
    Maybe (SomeSymFn sym)
Nothing -> IO (Maybe (SomeSymFn sym))
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Maybe (SomeSymFn sym))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe (SomeSymFn sym))
 -> ExceptT
      String (ReaderT (ProcessorEnv sym) IO) (Maybe (SomeSymFn sym)))
-> IO (Maybe (SomeSymFn sym))
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Maybe (SomeSymFn sym))
forall a b. (a -> b) -> a -> b
$ Text -> IO (Maybe (SomeSymFn sym))
userLookupFn Text
nm
    Maybe (SomeSymFn sym)
res -> Maybe (SomeSymFn sym)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Maybe (SomeSymFn sym))
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
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 = sym
-> Config sym -> SExpr -> IO (Either String (Some (SymExpr 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 = sym -> Config sym
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 = ProcessorEnv sym
-> Processor sym (Some (Expr t))
-> IO (Either String (Some (Expr t)))
forall sym a.
ProcessorEnv sym -> Processor sym a -> IO (Either String a)
runProcessor ProcessorEnv sym
env (SExpr -> Processor sym (Some (SymExpr sym))
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 = Config sym -> Text -> IO (Maybe (SomeSymFn sym))
forall sym. Config sym -> Text -> IO (Maybe (SomeSymFn sym))
cSymFnLookup Config sym
cfg
                           , procExprLookup :: Text -> IO (Maybe (Some (SymExpr sym)))
procExprLookup = Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
forall sym. Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
cExprLookup Config sym
cfg
                           , procLetEnv :: HashMap Text (Some (SymExpr sym))
procLetEnv = HashMap Text (Some (SymExpr sym))
HashMap Text (Some (Expr t))
forall k v. HashMap k v
HM.empty
                           , procLetFnEnv :: HashMap Text (SomeSymFn sym)
procLetFnEnv = HashMap Text (SomeSymFn sym)
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 = sym -> Config sym -> SExpr -> IO (Either String (SomeSymFn 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 = sym -> Config sym
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 = ProcessorEnv sym
-> Processor sym (SomeSymFn sym)
-> IO (Either String (SomeSymFn sym))
forall sym a.
ProcessorEnv sym -> Processor sym a -> IO (Either String a)
runProcessor ProcessorEnv sym
env (SExpr -> Processor sym (SomeSymFn sym)
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 = Config sym -> Text -> IO (Maybe (SomeSymFn sym))
forall sym. Config sym -> Text -> IO (Maybe (SomeSymFn sym))
cSymFnLookup Config sym
cfg
                           , procExprLookup :: Text -> IO (Maybe (Some (SymExpr sym)))
procExprLookup = Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
forall sym. Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
cExprLookup Config sym
cfg
                           , procLetEnv :: HashMap Text (Some (SymExpr sym))
procLetEnv = HashMap Text (Some (SymExpr sym))
HashMap Text (Some (Expr t))
forall k v. HashMap k v
HM.empty
                           , procLetFnEnv :: HashMap Text (SomeSymFn sym)
procLetFnEnv = HashMap Text (SomeSymFn sym)
forall k v. HashMap k v
HM.empty
                           }


deserializeBaseType ::
  SExpr
  -> Either String (Some BaseTypeRepr)
deserializeBaseType :: SExpr -> Either String (Some BaseTypeRepr)
deserializeBaseType SExpr
sexpr = SExpr -> Either String (Some BaseTypeRepr)
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 = m a -> (e -> m a) -> m a
forall a. m a -> (e -> m a) -> m a
forall e (m :: Type -> Type) a.
MonadError e m =>
m a -> (e -> m a) -> m a
E.catchError m a
act (e -> m a
forall a. e -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (e -> m a) -> (e -> e) -> e -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> e -> e
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 = m a -> (a -> m a) -> Maybe a -> m a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (e -> m a
forall a. e -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError e
err) a -> m a
forall a. a -> m a
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" -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some BaseTypeRepr -> m (Some BaseTypeRepr))
-> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr 'BaseBoolType -> Some BaseTypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr 'BaseBoolType
BaseBoolRepr
        String
"Int" -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some BaseTypeRepr -> m (Some BaseTypeRepr))
-> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr 'BaseIntegerType -> Some BaseTypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr 'BaseIntegerType
BaseIntegerRepr
        String
"Real" -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some BaseTypeRepr -> m (Some BaseTypeRepr))
-> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr 'BaseRealType -> Some BaseTypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr 'BaseRealType
BaseRealRepr
        String
"String" -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some BaseTypeRepr -> m (Some BaseTypeRepr))
-> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr ('BaseStringType 'Unicode) -> Some BaseTypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (StringInfoRepr 'Unicode -> BaseTypeRepr ('BaseStringType 'Unicode)
forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
BaseStringRepr StringInfoRepr 'Unicode
UnicodeRepr)
        String
"Complex" -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some BaseTypeRepr -> m (Some BaseTypeRepr))
-> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr 'BaseComplexType -> Some BaseTypeRepr
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) <- Integer -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
w
      , Just LeqProof 1 x
LeqProof <- NatRepr 1 -> NatRepr x -> Maybe (LeqProof 1 x)
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
        -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some BaseTypeRepr -> m (Some BaseTypeRepr))
-> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr ('BaseBVType x) -> Some BaseTypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (NatRepr x -> BaseTypeRepr ('BaseBVType x)
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) <- Integer -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
e
      , Just (Some NatRepr x
sRepr) <- Integer -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
s
      , Just LeqProof 2 x
LeqProof <- NatRepr 2 -> NatRepr x -> Maybe (LeqProof 2 x)
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 <- NatRepr 2 -> NatRepr x -> Maybe (LeqProof 2 x)
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
        -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BaseTypeRepr ('BaseFloatType ('FloatingPointPrecision x x))
-> Some BaseTypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (FloatPrecisionRepr ('FloatingPointPrecision x x)
-> BaseTypeRepr ('BaseFloatType ('FloatingPointPrecision x x))
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
BaseFloatRepr (NatRepr x
-> NatRepr x -> FloatPrecisionRepr ('FloatingPointPrecision x x)
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 tps <- SExpr -> m (Some (Assignment BaseTypeRepr))
forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some (Assignment BaseTypeRepr))
readBaseTypes SExpr
args
      return $ Some (BaseStructRepr tps)
    S.WFSList [S.WFSAtom (AId Text
"Array"), SExpr
ixArgs, SExpr
tpArg] -> do
      Some ixs <- SExpr -> m (Some (Assignment BaseTypeRepr))
forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some (Assignment BaseTypeRepr))
readBaseTypes SExpr
ixArgs
      Some tp <- readBaseType tpArg
      case Ctx.viewAssign ixs of
        AssignView BaseTypeRepr x
Ctx.AssignEmpty -> String -> m (Some BaseTypeRepr)
forall a. String -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String -> m (Some BaseTypeRepr))
-> String -> m (Some BaseTypeRepr)
forall a b. (a -> b) -> a -> b
$ String
"array type has no indices: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
sexpr
        Ctx.AssignExtend Assignment BaseTypeRepr ctx1
_ BaseTypeRepr tp
_ -> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some BaseTypeRepr -> m (Some BaseTypeRepr))
-> Some BaseTypeRepr -> m (Some BaseTypeRepr)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr ('BaseArrayType (ctx1 '::> tp) x) -> Some BaseTypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Assignment BaseTypeRepr (ctx1 '::> tp)
-> BaseTypeRepr x -> BaseTypeRepr ('BaseArrayType (ctx1 '::> tp) x)
forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr ('BaseArrayType (idx ::> tp) xs)
BaseArrayRepr Assignment BaseTypeRepr x
Assignment BaseTypeRepr (ctx1 '::> tp)
ixs BaseTypeRepr x
tp)
    SExpr
_ -> m (Some BaseTypeRepr)
panic
  where
    panic :: m (Some BaseTypeRepr)
panic = String -> m (Some BaseTypeRepr)
forall a. String -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String -> m (Some BaseTypeRepr))
-> String -> m (Some BaseTypeRepr)
forall a b. (a -> b) -> a -> b
$ String
"unknown base type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
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
_) = String -> m (Some (Assignment BaseTypeRepr))
forall a. String -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String -> m (Some (Assignment BaseTypeRepr)))
-> String -> m (Some (Assignment BaseTypeRepr))
forall a b. (a -> b) -> a -> b
$ String
"expected list of base types: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
sexpr
readBaseTypes (S.WFSList [SExpr]
sexprs) = [Some BaseTypeRepr] -> Some (Assignment BaseTypeRepr)
forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList ([Some BaseTypeRepr] -> Some (Assignment BaseTypeRepr))
-> m [Some BaseTypeRepr] -> m (Some (Assignment BaseTypeRepr))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (SExpr -> m (Some BaseTypeRepr))
-> [SExpr] -> m [Some BaseTypeRepr]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM SExpr -> m (Some BaseTypeRepr)
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 ex tp -> BaseTypeRepr tp
forall (tp :: BaseType). ex tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType ex tp
expr of
    BaseBVRepr NatRepr w
n -> BVProof tp -> m (BVProof tp)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BVProof tp -> m (BVProof tp)) -> BVProof tp -> m (BVProof tp)
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BVProof ('BaseBVType w)
forall (res :: Nat).
(1 <= res) =>
NatRepr res -> BVProof (BaseBVType res)
BVProof NatRepr w
n
    BaseTypeRepr tp
t -> String -> m (BVProof tp)
forall a. String -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String -> m (BVProof tp)) -> String -> m (BVProof tp)
forall a b. (a -> b) -> a -> b
$ String -> String -> String
forall r. PrintfType r => String -> r
printf String
"expected BV, found %s" (BaseTypeRepr tp -> String
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 = Text -> HashMap Text (Op sym) -> Maybe (Op sym)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HM.lookup Text
name HashMap Text (Op sym)
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 =
  [(Text, Op sym)] -> HashMap Text (Op sym)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HM.fromList [
  -- -- -- Boolean ops -- -- --
    (Text
"andp", Assignment
  BaseTypeRepr (('EmptyCtx ::> 'BaseBoolType) ::> 'BaseBoolType)
-> (sym
    -> SymExpr sym 'BaseBoolType
    -> SymExpr sym 'BaseBoolType
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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 Assignment
  BaseTypeRepr (('EmptyCtx ::> 'BaseBoolType) ::> 'BaseBoolType)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym 'BaseBoolType
  -> SymExpr sym 'BaseBoolType
  -> IO (SymExpr sym 'BaseBoolType))
 -> Op sym)
-> (sym
    -> SymExpr sym 'BaseBoolType
    -> SymExpr sym 'BaseBoolType
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym 'BaseBoolType
-> SymExpr sym 'BaseBoolType
-> IO (SymExpr sym 'BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred)
  , (Text
"orp", Assignment
  BaseTypeRepr (('EmptyCtx ::> 'BaseBoolType) ::> 'BaseBoolType)
-> (sym
    -> SymExpr sym 'BaseBoolType
    -> SymExpr sym 'BaseBoolType
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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 Assignment
  BaseTypeRepr (('EmptyCtx ::> 'BaseBoolType) ::> 'BaseBoolType)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym 'BaseBoolType
  -> SymExpr sym 'BaseBoolType
  -> IO (SymExpr sym 'BaseBoolType))
 -> Op sym)
-> (sym
    -> SymExpr sym 'BaseBoolType
    -> SymExpr sym 'BaseBoolType
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym 'BaseBoolType
-> SymExpr sym 'BaseBoolType
-> IO (SymExpr sym 'BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.orPred)
  , (Text
"xorp", Assignment
  BaseTypeRepr (('EmptyCtx ::> 'BaseBoolType) ::> 'BaseBoolType)
-> (sym
    -> SymExpr sym 'BaseBoolType
    -> SymExpr sym 'BaseBoolType
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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 Assignment
  BaseTypeRepr (('EmptyCtx ::> 'BaseBoolType) ::> 'BaseBoolType)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym 'BaseBoolType
  -> SymExpr sym 'BaseBoolType
  -> IO (SymExpr sym 'BaseBoolType))
 -> Op sym)
-> (sym
    -> SymExpr sym 'BaseBoolType
    -> SymExpr sym 'BaseBoolType
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym 'BaseBoolType
-> SymExpr sym 'BaseBoolType
-> IO (SymExpr sym 'BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.xorPred)
  , (Text
"notp", Assignment BaseTypeRepr ('EmptyCtx ::> 'BaseBoolType)
-> (sym
    -> SymExpr sym 'BaseBoolType -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 Assignment BaseTypeRepr ('EmptyCtx ::> 'BaseBoolType)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym 'BaseBoolType -> IO (SymExpr sym 'BaseBoolType))
 -> Op sym)
-> (sym
    -> SymExpr sym 'BaseBoolType -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall a b. (a -> b) -> a -> b
$ sym -> SymExpr sym 'BaseBoolType -> IO (SymExpr sym 'BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred)
  -- -- -- Float ops -- -- --
  , (Text
"floatneg", (forall (fpp :: FloatPrecision).
 sym -> SymFloat sym fpp -> IO (SymFloat sym fpp))
-> Op sym
forall sym.
(forall (fpp :: FloatPrecision).
 sym -> SymFloat sym fpp -> IO (SymFloat sym fpp))
-> Op sym
FloatOp1 sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
forall (fpp :: FloatPrecision).
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatNeg)
  , (Text
"floatabs", (forall (fpp :: FloatPrecision).
 sym -> SymFloat sym fpp -> IO (SymFloat sym fpp))
-> Op sym
forall sym.
(forall (fpp :: FloatPrecision).
 sym -> SymFloat sym fpp -> IO (SymFloat sym fpp))
-> Op sym
FloatOp1 sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
forall (fpp :: FloatPrecision).
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatAbs)
  -- -- -- Integer ops -- -- --
  , (Text
"intmul", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
-> (sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym 'BaseIntegerType
  -> SymExpr sym 'BaseIntegerType
  -> IO (SymExpr sym 'BaseIntegerType))
 -> Op sym)
-> (sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType))
-> Op sym
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym 'BaseIntegerType
-> SymExpr sym 'BaseIntegerType
-> IO (SymExpr sym 'BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMul)
  , (Text
"intadd", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
-> (sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym 'BaseIntegerType
  -> SymExpr sym 'BaseIntegerType
  -> IO (SymExpr sym 'BaseIntegerType))
 -> Op sym)
-> (sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType))
-> Op sym
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym 'BaseIntegerType
-> SymExpr sym 'BaseIntegerType
-> IO (SymExpr sym 'BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intAdd)
  , (Text
"intmod", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
-> (sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym 'BaseIntegerType
  -> SymExpr sym 'BaseIntegerType
  -> IO (SymExpr sym 'BaseIntegerType))
 -> Op sym)
-> (sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType))
-> Op sym
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym 'BaseIntegerType
-> SymExpr sym 'BaseIntegerType
-> IO (SymExpr sym 'BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMod)
  , (Text
"intdiv", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
-> (sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym 'BaseIntegerType
  -> SymExpr sym 'BaseIntegerType
  -> IO (SymExpr sym 'BaseIntegerType))
 -> Op sym)
-> (sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType))
-> Op sym
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym 'BaseIntegerType
-> SymExpr sym 'BaseIntegerType
-> IO (SymExpr sym 'BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intDiv)
  , (Text
"intle", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
-> (sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> 'BaseIntegerType) ::> 'BaseIntegerType)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym 'BaseIntegerType
  -> SymExpr sym 'BaseIntegerType
  -> IO (SymExpr sym 'BaseBoolType))
 -> Op sym)
-> (sym
    -> SymExpr sym 'BaseIntegerType
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym 'BaseIntegerType
-> SymExpr sym 'BaseIntegerType
-> IO (SymExpr sym 'BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intLe)
  , (Text
"intabs", Assignment BaseTypeRepr ('EmptyCtx ::> 'BaseIntegerType)
-> (sym
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType))
-> Op sym
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 Assignment BaseTypeRepr ('EmptyCtx ::> 'BaseIntegerType)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym 'BaseIntegerType
  -> IO (SymExpr sym 'BaseIntegerType))
 -> Op sym)
-> (sym
    -> SymExpr sym 'BaseIntegerType
    -> IO (SymExpr sym 'BaseIntegerType))
-> Op sym
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym 'BaseIntegerType
-> IO (SymExpr sym 'BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intAbs)
  -- -- -- Bitvector ops -- -- --
  , (Text
"bvand", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvAndBits)
  , (Text
"bvor", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvOrBits)
  , (Text
"bvadd", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvAdd)
  , (Text
"bvmul", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvMul)
  , (Text
"bvudiv", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvUdiv)
  , (Text
"bvurem", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvUrem)
  , (Text
"bvshl", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvShl)
  , (Text
"bvlshr", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvLshr)
  , (Text
"bvnand", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 ((forall (w :: Nat).
  (1 <= w) =>
  sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
 -> Op sym)
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymBV sym w
arg1 SymBV sym w
arg2 -> sym -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNotBits sym
sym (SymBV sym w -> IO (SymBV sym w))
-> IO (SymBV sym w) -> IO (SymBV sym w)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
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 (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 ((forall (w :: Nat).
  (1 <= w) =>
  sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
 -> Op sym)
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymBV sym w
arg1 SymBV sym w
arg2 -> sym -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNotBits sym
sym (SymBV sym w -> IO (SymBV sym w))
-> IO (SymBV sym w) -> IO (SymBV sym w)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
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 (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvXorBits)
  , (Text
"bvxnor", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 ((forall (w :: Nat).
  (1 <= w) =>
  sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
 -> Op sym)
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymBV sym w
arg1 SymBV sym w
arg2 -> sym -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNotBits sym
sym (SymBV sym w -> IO (SymBV sym w))
-> IO (SymBV sym w) -> IO (SymBV sym w)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
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 (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvSub)
  , (Text
"bvsdiv", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvSdiv)
  , (Text
"bvsrem", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvSrem)
  , (Text
"bvsmod", String -> Op sym
forall a. HasCallStack => String -> a
error String
"bvsmod is not implemented")
  , (Text
"bvashr", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvAshr)
  , (Text
"bvult", (forall (w :: Nat).
 (1 <= w) =>
 sym
 -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUlt)
  , (Text
"bvule", (forall (w :: Nat).
 (1 <= w) =>
 sym
 -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUle)
  , (Text
"bvugt", (forall (w :: Nat).
 (1 <= w) =>
 sym
 -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUgt)
  , (Text
"bvuge", (forall (w :: Nat).
 (1 <= w) =>
 sym
 -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUge)
  , (Text
"bvslt", (forall (w :: Nat).
 (1 <= w) =>
 sym
 -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvSlt)
  , (Text
"bvsle", (forall (w :: Nat).
 (1 <= w) =>
 sym
 -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvSle)
  , (Text
"bvsgt", (forall (w :: Nat).
 (1 <= w) =>
 sym
 -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvSgt)
  , (Text
"bvsge", (forall (w :: Nat).
 (1 <= w) =>
 sym
 -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvSge)
  , (Text
"bveq", (forall (w :: Nat).
 (1 <= w) =>
 sym
 -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvEq)
  , (Text
"bvne", (forall (w :: Nat).
 (1 <= w) =>
 sym
 -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym 'BaseBoolType)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvNe)
  , (Text
"bvneg", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp1 sym -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNeg)
  , (Text
"bvnot", (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
forall sym.
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp1 sym -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNotBits)
  -- -- -- Floating point ops -- -- --
  , (Text
"fnegd", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
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", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
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", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
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", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
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", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> IO (SymExpr sym (BaseFloatType Prec64)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> IO (SymExpr sym (BaseFloatType Prec32)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym 'BaseBoolType))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym 'BaseBoolType))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> IO (SymExpr sym (BaseFloatType Prec32)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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 FloatPrecisionRepr Prec32
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", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
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 FloatPrecisionRepr Prec64
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
W4.RNE)
  , (Text
"fp_binary_to_double",
     Assignment BaseTypeRepr ('EmptyCtx ::> BaseBVType 64)
-> (sym
    -> SymExpr sym (BaseBVType 64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseBVType 64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 64)
  -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
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 FloatPrecisionRepr Prec64
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr)
  , (Text
"fp_binary_to_single",
     Assignment BaseTypeRepr ('EmptyCtx ::> BaseBVType 32)
-> (sym
    -> SymExpr sym (BaseBVType 32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseBVType 32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 32)
  -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
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 FloatPrecisionRepr Prec32
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr)
  , (Text
"fp_double_to_binary", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseBVType 64)))
-> Op sym
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseBVType 64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseBVType 64)))
-> Op sym
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", Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseBVType 32)))
-> Op sym
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 Assignment BaseTypeRepr ('EmptyCtx ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym (BaseBVType 32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseBVType 32)))
-> Op sym
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", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseBVType 64)))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseBVType 64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseBVType 64)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseBVType 64)))
-> IO (SymExpr sym (BaseBVType 64))
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 ((RoundingMode -> IO (SymExpr sym (BaseBVType 64)))
 -> IO (SymExpr sym (BaseBVType 64)))
-> (RoundingMode -> IO (SymExpr sym (BaseBVType 64)))
-> IO (SymExpr sym (BaseBVType 64))
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 NatRepr 64
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
  , (Text
"fctidu", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseBVType 64)))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseBVType 64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseBVType 64)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseBVType 64)))
-> IO (SymExpr sym (BaseBVType 64))
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 ((RoundingMode -> IO (SymExpr sym (BaseBVType 64)))
 -> IO (SymExpr sym (BaseBVType 64)))
-> (RoundingMode -> IO (SymExpr sym (BaseBVType 64)))
-> IO (SymExpr sym (BaseBVType 64))
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 NatRepr 64
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
  , (Text
"fctiw", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseBVType 32)))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseBVType 32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseBVType 32)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseBVType 32)))
-> IO (SymExpr sym (BaseBVType 32))
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 ((RoundingMode -> IO (SymExpr sym (BaseBVType 32)))
 -> IO (SymExpr sym (BaseBVType 32)))
-> (RoundingMode -> IO (SymExpr sym (BaseBVType 32)))
-> IO (SymExpr sym (BaseBVType 32))
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 NatRepr 32
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
  , (Text
"fctiwu", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseBVType 32)))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseBVType 32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseBVType 32)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseBVType 32)))
-> IO (SymExpr sym (BaseBVType 32))
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 ((RoundingMode -> IO (SymExpr sym (BaseBVType 32)))
 -> IO (SymExpr sym (BaseBVType 32)))
-> (RoundingMode -> IO (SymExpr sym (BaseBVType 32)))
-> IO (SymExpr sym (BaseBVType 32))
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 NatRepr 32
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
  , (Text
"fcfid", Assignment
  BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseBVType 64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
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 Assignment
  BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseBVType 64)
  -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseBVType 64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseBVType 64)
x -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> IO (SymExpr sym (BaseFloatType Prec64)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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 FloatPrecisionRepr Prec64
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseBVType 64)
x)
  , (Text
"fcfids", Assignment
  BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseBVType 64)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
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 Assignment
  BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseBVType 64)
  -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseBVType 64)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseBVType 64)
x -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> IO (SymExpr sym (BaseFloatType Prec32)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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 FloatPrecisionRepr Prec32
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseBVType 64)
x)
  , (Text
"fcfidu", Assignment
  BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseBVType 64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
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 Assignment
  BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseBVType 64)
  -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseBVType 64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseBVType 64)
x -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> IO (SymExpr sym (BaseFloatType Prec64)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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 FloatPrecisionRepr Prec64
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseBVType 64)
x)
  , (Text
"fcfidus", Assignment
  BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseBVType 64)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
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 Assignment
  BaseTypeRepr (('EmptyCtx ::> BaseBVType 2) ::> BaseBVType 64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseBVType 64)
  -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseBVType 64)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseBVType 64)
x -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> IO (SymExpr sym (BaseFloatType Prec32)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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 FloatPrecisionRepr Prec32
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseBVType 64)
x)
  , (Text
"frti", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> IO (SymExpr sym (BaseFloatType Prec64)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> IO (SymExpr sym (BaseFloatType Prec32)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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", Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
   ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
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 Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
   ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec64)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> IO (SymExpr sym (BaseFloatType Prec64)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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", Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
   ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
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 Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
   ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec32)
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> IO (SymExpr sym (BaseFloatType Prec32)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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", Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
   ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
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 Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
   ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec64)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> IO (SymExpr sym (BaseFloatType Prec64)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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", Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
   ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
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 Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
   ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec32)
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> IO (SymExpr sym (BaseFloatType Prec32)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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", Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
   ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
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 Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
   ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec64)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> IO (SymExpr sym (BaseFloatType Prec64)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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", Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
   ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
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 Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
   ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec32)
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> IO (SymExpr sym (BaseFloatType Prec32)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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", Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
   ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
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 Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
   ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec64)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> IO (SymExpr sym (BaseFloatType Prec64)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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", Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
   ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
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 Assignment
  BaseTypeRepr
  ((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
   ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec32)
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> IO (SymExpr sym (BaseFloatType Prec32)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseFloatType Prec64) ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseFloatType Prec64) ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec64)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym 'BaseBoolType))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseFloatType Prec32) ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseFloatType Prec32) ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec32)
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym 'BaseBoolType))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseFloatType Prec64) ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseFloatType Prec64) ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec64)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym 'BaseBoolType))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseFloatType Prec32) ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseFloatType Prec32) ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec32)
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym 'BaseBoolType))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseFloatType Prec64) ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseFloatType Prec64) ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec64)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym 'BaseBoolType))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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", Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseFloatType Prec32) ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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 Assignment
  BaseTypeRepr
  (('EmptyCtx ::> BaseFloatType Prec32) ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseFloatType Prec32)
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym 'BaseBoolType))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym 'BaseBoolType))
-> Op sym
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", Assignment
  BaseTypeRepr
  (((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    ::> BaseFloatType Prec64)
   ::> BaseFloatType Prec64)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
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 Assignment
  BaseTypeRepr
  (((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec64)
    ::> BaseFloatType Prec64)
   ::> BaseFloatType Prec64)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec64)
  -> SymExpr sym (BaseFloatType Prec64)
  -> SymExpr sym (BaseFloatType Prec64)
  -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> SymExpr sym (BaseFloatType Prec64)
    -> IO (SymExpr sym (BaseFloatType Prec64)))
-> Op sym
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 -> sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
 -> IO (SymExpr sym (BaseFloatType Prec64)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec64)))
-> IO (SymExpr sym (BaseFloatType Prec64))
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", Assignment
  BaseTypeRepr
  (((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
    ::> BaseFloatType Prec32)
   ::> BaseFloatType Prec32)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
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 Assignment
  BaseTypeRepr
  (((('EmptyCtx ::> BaseBVType 2) ::> BaseFloatType Prec32)
    ::> BaseFloatType Prec32)
   ::> BaseFloatType Prec32)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr ((sym
  -> SymExpr sym (BaseBVType 2)
  -> SymExpr sym (BaseFloatType Prec32)
  -> SymExpr sym (BaseFloatType Prec32)
  -> SymExpr sym (BaseFloatType Prec32)
  -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> Op sym)
-> (sym
    -> SymExpr sym (BaseBVType 2)
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> SymExpr sym (BaseFloatType Prec32)
    -> IO (SymExpr sym (BaseFloatType Prec32)))
-> Op sym
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 ->
    sym
-> SymExpr sym (BaseBVType 2)
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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 ((RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
 -> IO (SymExpr sym (BaseFloatType Prec32)))
-> (RoundingMode -> IO (SymExpr sym (BaseFloatType Prec32)))
-> IO (SymExpr sym (BaseFloatType Prec32))
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
  args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
  case args of
    [Some (Expr t)
arg] -> Some (Expr t)
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Some (Expr t)
arg
    [Some (Expr t)]
_ -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"expecting 1 argument, got %d" ([Some (Expr t)] -> Int
forall a. [a] -> Int
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
  args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
  case args of
    [Some (Expr t)
arg1, Some (Expr t)
arg2] -> (Some (Expr t), Some (Expr t))
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Some (Expr t), Some (Expr t))
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some (Expr t)
arg1, Some (Expr t)
arg2)
    [Some (Expr t)]
_ -> String
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Some (Expr t), Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT
      String
      (ReaderT (ProcessorEnv sym) IO)
      (Some (Expr t), Some (Expr t)))
-> String
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Some (Expr t), Some (Expr t))
forall a b. (a -> b) -> a -> b
$ String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"expecting 2 arguments, got %d" ([Some (Expr t)] -> Int
forall a. [a] -> Int
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
  args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
  case args of
    [Some (Expr t)
arg1, Some (Expr t)
arg2, Some (Expr t)
arg3] -> (Some (Expr t), Some (Expr t), Some (Expr t))
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Some (Expr t), Some (Expr t), Some (Expr t))
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
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)]
_ -> String
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Some (Expr t), Some (Expr t), Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT
      String
      (ReaderT (ProcessorEnv sym) IO)
      (Some (Expr t), Some (Expr t), Some (Expr t)))
-> String
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Some (Expr t), Some (Expr t), Some (Expr t))
forall a b. (a -> b) -> a -> b
$ String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"expecting 3 arguments, got %d" ([Some (Expr t)] -> Int
forall a. [a] -> Int
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
  sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.asks ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
forall sym. ProcessorEnv sym -> sym
procSym
  maybeFn <- lookupFn fnName
  case maybeFn of
    Just (SomeSymFn SymFn sym dom ret
fn) -> do
      args <- (SExpr
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> [SExpr]
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Some (Expr t)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM SExpr
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
SExpr
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr [SExpr]
operands
      assn <- exprAssignment (W4.fnArgTypes fn) args
      liftIO (Some <$> W4.applySymFn sym fn assn)
    Maybe (SomeSymFn sym)
Nothing -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ String
"The function name `"
               String -> String -> String
forall a. [a] -> [a] -> [a]
++(Text -> String
T.unpack Text
fnName)
               String -> String -> String
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 = String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError
  (String
 -> ExceptT
      String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
-> String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall a b. (a -> b) -> a -> b
$ String
"Unrecognized use of `call`: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (Seq String -> SExpr -> Text
printSExpr Seq String
forall a. Monoid a => a
mempty ([SExpr] -> SExpr
forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L (SExpr
opRawSExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
:[SExpr]
operands))))
readApp opRaw :: SExpr
opRaw@(S.WFSAtom (AId Text
operator)) [SExpr]
operands = do
  sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
forall a.
(ProcessorEnv (ExprBuilder t st fs) -> a)
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
forall sym. ProcessorEnv sym -> sym
procSym
  prefixError ("in reading expression:\n"
               ++(T.unpack $ printSExpr mempty $ S.WFSList (opRaw:operands))++"\n") $
  -- Parse an expression of the form @(fnname operands ...)@
    case lookupOp @sym operator of
      Just (FloatOp1 forall (fpp :: FloatPrecision).
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
fn) -> do
        args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
        case args of
          [Some Expr t x
a1]
            | BaseFloatRepr FloatPrecisionRepr fpp
_ <- Expr t x -> BaseTypeRepr x
forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
a1 -> IO (Some (Expr t))
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (Expr t ('BaseFloatType fpp) -> Some (Expr t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Expr t ('BaseFloatType fpp) -> Some (Expr t))
-> IO (Expr t ('BaseFloatType fpp)) -> IO (Some (Expr t))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
forall (fpp :: FloatPrecision).
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
fn sym
ExprBuilder t st fs
sym SymFloat sym fpp
Expr t x
a1)
          [Some (Expr t)]
_ -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
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
        args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
        exprAssignment arg_types args >>= \case
          Assignment (Expr t) ctx
Ctx.Empty Ctx.:> Expr t tp
arg1 ->
            IO (Some (Expr t))
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (Expr t ret -> Some (Expr t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Expr t ret -> Some (Expr t))
-> IO (Expr t ret) -> IO (Some (Expr t))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymExpr sym arg1 -> IO (SymExpr sym ret)
fn sym
ExprBuilder t st fs
sym SymExpr sym arg1
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
        args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
        exprAssignment arg_types args >>= \case
          Assignment (Expr t) ctx
Ctx.Empty Ctx.:> Expr t tp
arg1 Ctx.:> Expr t tp
arg2 ->
              IO (Some (Expr t))
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (Expr t ret -> Some (Expr t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Expr t ret -> Some (Expr t))
-> IO (Expr t ret) -> IO (Some (Expr t))
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 sym
ExprBuilder t st fs
sym SymExpr sym arg1
Expr t tp
arg1 SymExpr sym arg2
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
        args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
        exprAssignment arg_types args >>= \case
          Assignment (Expr t) ctx
Ctx.Empty Ctx.:> Expr t tp
arg1 Ctx.:> Expr t tp
arg2 Ctx.:> Expr t tp
arg3 ->
              IO (Some (Expr t))
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (Expr t ret -> Some (Expr t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Expr t ret -> Some (Expr t))
-> IO (Expr t ret) -> IO (Some (Expr t))
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 sym
ExprBuilder t st fs
sym SymExpr sym arg1
Expr t tp
arg1 SymExpr sym arg2
Expr t tp
arg2 SymExpr sym arg3
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
        args <- [SExpr] -> Processor sym [Some (SymExpr sym)]
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
        exprAssignment arg_types args >>= \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 ->
              IO (Some (Expr t))
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (Expr t ret -> Some (Expr t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Expr t ret -> Some (Expr t))
-> IO (Expr t ret) -> IO (Some (Expr t))
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 sym
ExprBuilder t st fs
sym SymExpr sym arg1
Expr t tp
arg1 SymExpr sym arg2
Expr t tp
arg2 SymExpr sym arg3
Expr t tp
arg3 SymExpr sym arg4
Expr t tp
arg4)
      Just (BVOp1 forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
op) -> do
        Some expr <- [SExpr]
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
operands
        BVProof _ <- getBVProof expr
        liftIO $ Some <$> op sym expr
      Just (BVOp2 forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
op) -> do
        (Some arg1, Some arg2)  <- [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
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 m <- prefixError "in arg 1: " $ getBVProof arg1
        BVProof n <- prefixError "in arg 2: " $ getBVProof arg2
        case testEquality m n of
          Just n :~: n
Refl -> IO (Some (Expr t))
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (Expr t ('BaseBVType n) -> Some (Expr t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Expr t ('BaseBVType n) -> Some (Expr t))
-> IO (Expr t ('BaseBVType n)) -> IO (Some (Expr t))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymBV sym n -> SymBV sym n -> IO (SymBV sym n)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
op sym
ExprBuilder t st fs
sym SymBV sym n
Expr t x
arg1 SymBV sym n
Expr t x
arg2)
          Maybe (n :~: n)
Nothing -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ String -> Text -> String -> String -> String
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
                                         (NatRepr n -> String
forall a. Show a => a -> String
show NatRepr n
m)
                                         (NatRepr n -> String
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 arg1, Some arg2)  <- [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
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 m <- prefixError "in arg 1: " $ getBVProof arg1
        BVProof n <- prefixError "in arg 2: " $ getBVProof arg2
        case testEquality m n of
          Just n :~: n
Refl -> IO (Some (Expr t))
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (Expr t 'BaseBoolType -> Some (Expr t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Expr t 'BaseBoolType -> Some (Expr t))
-> IO (Expr t 'BaseBoolType) -> IO (Some (Expr t))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymBV sym n -> SymBV sym n -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
op sym
ExprBuilder t st fs
sym SymBV sym n
Expr t x
arg1 SymBV sym n
Expr t x
arg2)
          Maybe (n :~: n)
Nothing -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ String -> Text -> String -> String -> String
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
                                         (NatRepr n -> String
forall a. Show a => a -> String
show NatRepr n
m)
                                         (NatRepr n -> String
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 arg1, Some arg2)  <- [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
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 _ <- prefixError "in arg 1: " $ getBVProof arg1
            BVProof _ <- prefixError "in arg 2: " $ getBVProof arg2
            liftIO (Some <$> W4.bvConcat sym arg1 arg2)
          Text
"=" -> do
            (Some arg1, Some arg2)  <- [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
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 testEquality (W4.exprType arg1) (W4.exprType arg2) of
              Just x :~: x
Refl -> IO (Some (Expr t))
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (Expr t 'BaseBoolType -> Some (Expr t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Expr t 'BaseBoolType -> Some (Expr t))
-> IO (Expr t 'BaseBoolType) -> IO (Some (Expr t))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SymExpr (ExprBuilder t st fs) x
-> SymExpr (ExprBuilder t st fs) x
-> IO (Pred (ExprBuilder t st fs))
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
forall (tp :: BaseType).
ExprBuilder t st fs
-> SymExpr (ExprBuilder t st fs) tp
-> SymExpr (ExprBuilder t st fs) tp
-> IO (Pred (ExprBuilder t st fs))
W4.isEq ExprBuilder t st fs
sym SymExpr (ExprBuilder t st fs) x
Expr t x
arg1 SymExpr (ExprBuilder t st fs) x
Expr t x
arg2)
              Maybe (x :~: x)
Nothing -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$
                String -> String -> String -> String
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"
                (BaseTypeRepr x -> String
forall a. Show a => a -> String
show (Expr t x -> BaseTypeRepr x
forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arg1))
                (BaseTypeRepr x -> String
forall a. Show a => a -> String
show (Expr t x -> BaseTypeRepr x
forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arg2))
          Text
"ite" -> do
            (Some test, Some then_, Some else_)  <- [SExpr]
-> Processor
     sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
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 W4.exprType test of
              BaseTypeRepr x
BaseBoolRepr ->
                case BaseTypeRepr x -> BaseTypeRepr x -> Maybe (x :~: x)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: BaseType) (b :: BaseType).
BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b)
testEquality (Expr t x -> BaseTypeRepr x
forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
then_) (Expr t x -> BaseTypeRepr x
forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
else_) of
                  Just x :~: x
Refl -> IO (Some (Expr t))
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (Expr t x -> Some (Expr t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Expr t x -> Some (Expr t)) -> IO (Expr t x) -> IO (Some (Expr t))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymExpr (ExprBuilder t st fs) x
-> SymExpr (ExprBuilder t st fs) x
-> IO (SymExpr (ExprBuilder t st fs) x)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
forall (tp :: BaseType).
ExprBuilder t st fs
-> Pred (ExprBuilder t st fs)
-> SymExpr (ExprBuilder t st fs) tp
-> SymExpr (ExprBuilder t st fs) tp
-> IO (SymExpr (ExprBuilder t st fs) tp)
W4.baseTypeIte ExprBuilder t st fs
sym Pred (ExprBuilder t st fs)
Expr t x
test SymExpr (ExprBuilder t st fs) x
Expr t x
then_ SymExpr (ExprBuilder t st fs) x
Expr t x
else_)
                  Maybe (x :~: x)
Nothing -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$
                    String -> String -> String -> String
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"
                    (BaseTypeRepr x -> String
forall a. Show a => a -> String
show (Expr t x -> BaseTypeRepr x
forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
then_))
                    (BaseTypeRepr x -> String
forall a. Show a => a -> String
show (Expr t x -> BaseTypeRepr x
forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
else_))
              BaseTypeRepr x
tp -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ String -> String -> String
forall r. PrintfType r => String -> r
printf String
"test expression must be a boolean; got %s" (BaseTypeRepr x -> String
forall a. Show a => a -> String
show BaseTypeRepr x
tp)
          Text
"select" -> do
            (Some arr, Some idx)  <- [SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
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 _ <- expectArrayWithIndex (W4.exprType idx) (W4.exprType arr)
            let idx' = Assignment (Expr t) 'EmptyCtx
forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty Assignment (Expr t) 'EmptyCtx
-> Expr t x -> Assignment (Expr t) (SingleCtx x)
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
            liftIO (Some <$> W4.arrayLookup sym arr idx')
          Text
"store" -> do
            (Some arr, Some idx, Some expr)  <- [SExpr]
-> Processor
     sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
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 resRepr <- expectArrayWithIndex (W4.exprType idx) (W4.exprType arr)
            case testEquality resRepr (W4.exprType expr) of
              Just res :~: x
Refl ->
                let idx' :: Assignment (Expr t) (SingleCtx x)
idx' = Assignment (Expr t) 'EmptyCtx
forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty Assignment (Expr t) 'EmptyCtx
-> Expr t x -> Assignment (Expr t) (SingleCtx x)
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 IO (Some (Expr t))
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (Expr t (BaseArrayType (SingleCtx x) x) -> Some (Expr t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Expr t (BaseArrayType (SingleCtx x) x) -> Some (Expr t))
-> IO (Expr t (BaseArrayType (SingleCtx x) x))
-> IO (Some (Expr t))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SymArray (ExprBuilder t st fs) (SingleCtx x) x
-> Assignment (SymExpr (ExprBuilder t st fs)) (SingleCtx x)
-> SymExpr (ExprBuilder t st fs) x
-> IO (SymArray (ExprBuilder t st fs) (SingleCtx x) x)
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)
forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
ExprBuilder t st fs
-> SymArray (ExprBuilder t st fs) (idx ::> tp) b
-> Assignment (SymExpr (ExprBuilder t st fs)) (idx ::> tp)
-> SymExpr (ExprBuilder t st fs) b
-> IO (SymArray (ExprBuilder t st fs) (idx ::> tp) b)
W4.arrayUpdate ExprBuilder t st fs
sym SymArray (ExprBuilder t st fs) (SingleCtx x) x
Expr t x
arr Assignment (SymExpr (ExprBuilder t st fs)) (SingleCtx x)
Assignment (Expr t) (SingleCtx x)
idx' SymExpr (ExprBuilder t st fs) x
Expr t x
expr)
              Maybe (res :~: x)
Nothing -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Array result type %s does not match %s"
                         (BaseTypeRepr res -> String
forall a. Show a => a -> String
show BaseTypeRepr res
resRepr)
                         (BaseTypeRepr x -> String
forall a. Show a => a -> String
show (Expr t x -> BaseTypeRepr x
forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
expr))
          Text
"updateArray" -> do
            (Some arr, Some idx, Some expr)  <- [SExpr]
-> Processor
     sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
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 resRepr <- expectArrayWithIndex (W4.exprType idx) (W4.exprType arr)
            case testEquality resRepr (W4.exprType expr) of
              Just res :~: x
Refl ->
                let idx' :: Assignment (Expr t) (SingleCtx x)
idx' = Assignment (Expr t) 'EmptyCtx
forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty Assignment (Expr t) 'EmptyCtx
-> Expr t x -> Assignment (Expr t) (SingleCtx x)
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 IO (Some (Expr t))
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (Expr t (BaseArrayType (SingleCtx x) x) -> Some (Expr t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Expr t (BaseArrayType (SingleCtx x) x) -> Some (Expr t))
-> IO (Expr t (BaseArrayType (SingleCtx x) x))
-> IO (Some (Expr t))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SymArray (ExprBuilder t st fs) (SingleCtx x) x
-> Assignment (SymExpr (ExprBuilder t st fs)) (SingleCtx x)
-> SymExpr (ExprBuilder t st fs) x
-> IO (SymArray (ExprBuilder t st fs) (SingleCtx x) x)
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)
forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
ExprBuilder t st fs
-> SymArray (ExprBuilder t st fs) (idx ::> tp) b
-> Assignment (SymExpr (ExprBuilder t st fs)) (idx ::> tp)
-> SymExpr (ExprBuilder t st fs) b
-> IO (SymArray (ExprBuilder t st fs) (idx ::> tp) b)
W4.arrayUpdate ExprBuilder t st fs
sym SymArray (ExprBuilder t st fs) (SingleCtx x) x
Expr t x
arr Assignment (SymExpr (ExprBuilder t st fs)) (SingleCtx x)
Assignment (Expr t) (SingleCtx x)
idx' SymExpr (ExprBuilder t st fs) x
Expr t x
expr)
              Maybe (res :~: x)
Nothing -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Array result type %s does not match %s"
                         (BaseTypeRepr res -> String
forall a. Show a => a -> String
show BaseTypeRepr res
resRepr)
                         (BaseTypeRepr x -> String
forall a. Show a => a -> String
show (Expr t x -> BaseTypeRepr x
forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
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 arrExpr <- SExpr
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
arrSExpr
                case W4.exprType arrExpr of
                  BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idxReprs BaseTypeRepr xs
arrTyRepr -> do
                    updateMap <- Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs
-> SExpr
-> Processor sym (ArrayUpdateMap (SymExpr sym) (idx ::> tp) xs)
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
                    liftIO (Some <$> W4.sbMakeExpr sym (W4.ArrayMap idxReprs arrTyRepr updateMap arrExpr))
                  BaseTypeRepr x
repr -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected an array type for the value in 'arrayMap', but got", BaseTypeRepr x -> String
forall a. Show a => a -> String
show BaseTypeRepr x
repr]
              [SExpr]
_ -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected a list of indices and an array expression, but got", [SExpr] -> String
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 struct  <- SExpr
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
rawStruct
                case W4.exprType struct of
                  (BaseStructRepr Assignment BaseTypeRepr ctx
fldTpReprs) ->
                    case Int -> Size ctx -> Maybe (Some (Index ctx))
forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
Ctx.intIndex (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
rawIdx) (Assignment BaseTypeRepr ctx -> Size ctx
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) -> IO (Some (Expr t))
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (Expr t x -> Some (Expr t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Expr t x -> Some (Expr t)) -> IO (Expr t x) -> IO (Some (Expr t))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SymStruct (ExprBuilder t st fs) ctx
-> Index ctx x
-> IO (SymExpr (ExprBuilder t st fs) x)
forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
forall (flds :: Ctx BaseType) (tp :: BaseType).
ExprBuilder t st fs
-> SymStruct (ExprBuilder t st fs) flds
-> Index flds tp
-> IO (SymExpr (ExprBuilder t st fs) tp)
W4.structField ExprBuilder t st fs
sym SymStruct (ExprBuilder t st fs) ctx
Expr t x
struct Index ctx x
i)
                      Maybe (Some (Index ctx))
Nothing -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$
                        [String] -> String
unwords [String
"invalid struct index, got", Assignment BaseTypeRepr ctx -> String
forall a. Show a => a -> String
show Assignment BaseTypeRepr ctx
fldTpReprs, String
"and", Integer -> String
forall a. Show a => a -> String
show Integer
rawIdx]
                  BaseTypeRepr x
srepr -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected a struct, got", BaseTypeRepr x -> String
forall a. Show a => a -> String
show BaseTypeRepr x
srepr]
              [SExpr]
_ -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected an arg and an Int, got", [SExpr] -> String
forall a. Show a => a -> String
show [SExpr]
operands]
          Text
"struct" -> do
            case [SExpr]
operands of
              [S.WFSList [SExpr]
rawFldExprs] -> do
                Some flds <- [SExpr] -> Processor sym (Some (Assignment (SymExpr sym)))
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (Assignment (SymExpr sym)))
readExprsAsAssignment [SExpr]
rawFldExprs
                liftIO (Some <$> W4.mkStruct sym flds)
              [SExpr]
_ -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"struct expects a single operand, got", [SExpr] -> String
forall a. Show a => a -> String
show [SExpr]
operands]
          Text
"sbvToInteger" -> do
            (Some arg) <- [SExpr]
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
operands
            BVProof _ <- getBVProof arg
            liftIO $ Some <$> W4.sbvToInteger sym arg
          Text
"bvToInteger" -> do
            (Some arg) <- [SExpr]
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
operands
            BVProof _ <- getBVProof arg
            liftIO $ Some <$> W4.bvToInteger sym arg
          Text
"integerToBV" -> do
            case [SExpr]
operands of
              [S.WFSAtom (ANat Nat
width), SExpr
rawValExpr] -> do
                Some x <- SExpr
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
rawValExpr
                case (mkNatRepr width, W4.exprType x) of
                  (Some NatRepr x
w, BaseTypeRepr x
BaseIntegerRepr)
                    | Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w -> do
                    IO (Some (Expr t))
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (Expr t (BaseBVType x) -> Some (Expr t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Expr t (BaseBVType x) -> Some (Expr t))
-> IO (Expr t (BaseBVType x)) -> IO (Some (Expr t))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SymInteger (ExprBuilder t st fs)
-> NatRepr x
-> IO (SymBV (ExprBuilder t st fs) x)
forall (w :: Nat).
(1 <= w) =>
ExprBuilder t st fs
-> SymInteger (ExprBuilder t st fs)
-> NatRepr w
-> IO (SymBV (ExprBuilder t st fs) w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
W4.integerToBV ExprBuilder t st fs
sym SymInteger (ExprBuilder t st fs)
Expr t x
x NatRepr x
w)
                  (Some NatRepr, BaseTypeRepr x)
srepr -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected a non-zero natural and an integer, got", (Some NatRepr, BaseTypeRepr x) -> String
forall a. Show a => a -> String
show (Some NatRepr, BaseTypeRepr x)
srepr]
              [SExpr]
_ -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"integerToBV expects two operands, the first of which is a nat, got", [SExpr] -> String
forall a. Show a => a -> String
show [SExpr]
operands]
          Text
_ -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ String -> Text -> String
forall r. PrintfType r => String -> r
printf String
"couldn't parse application of %s" (Seq String -> SExpr -> Text
printSExpr Seq String
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 = String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in reading extract expression: " (ExceptT
   String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
 -> ExceptT
      String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall a b. (a -> b) -> a -> b
$ do
  sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
forall a.
(ProcessorEnv (ExprBuilder t st fs) -> a)
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
forall sym. ProcessorEnv sym -> sym
procSym
  (Some arg) <- readOneArg 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
iInt Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
jInt Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
      idxInt = Integer
jInt
  Some nNat <- prefixError "in calculating extract length: " $ intToNatM nInt
  Some idxNat <- prefixError "in extract lower bound: " $ intToNatM idxInt
  LeqProof <- fromMaybeError "extract length must be positive" $ isPosNat nNat
  BVProof lenNat <- getBVProof arg
  LeqProof <- fromMaybeError "invalid extract for given bitvector" $
    testLeq (addNat idxNat nNat) lenNat
  liftIO (Some <$> W4.bvSelect sym idxNat nNat 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 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"zero_extend" Bool -> Bool -> Bool
||
    Text
extend Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"sign_extend" = String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError (String -> Text -> String
forall r. PrintfType r => String -> r
printf String
"in reading %s expression: " Text
extend) (ExceptT
   String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
 -> ExceptT
      String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall a b. (a -> b) -> a -> b
$ do
      sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
forall a.
(ProcessorEnv (ExprBuilder t st fs) -> a)
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
forall sym. ProcessorEnv sym -> sym
procSym
      Some arg <- readOneArg args
      Some iNat <- intToNatM iInt
      iPositive <- fromMaybeError "must extend by a positive length" $ isPosNat iNat
      BVProof lenNat <- getBVProof arg
      let newLen = NatRepr n -> NatRepr x -> NatRepr (n + x)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr n
lenNat NatRepr x
iNat
      liftIO $ withLeqProof (leqAdd2 (leqRefl lenNat) iPositive) $
        let op = if Text
extend Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"zero_extend" then ExprBuilder t st fs
-> NatRepr (n + x)
-> SymBV (ExprBuilder t st fs) n
-> IO (SymBV (ExprBuilder t st fs) (n + x))
forall (u :: Nat) (r :: Nat).
(1 <= u, (u + 1) <= r) =>
ExprBuilder t st fs
-> NatRepr r
-> SymBV (ExprBuilder t st fs) u
-> IO (SymBV (ExprBuilder t st fs) r)
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 ExprBuilder t st fs
-> NatRepr (n + x)
-> SymBV (ExprBuilder t st fs) n
-> IO (SymBV (ExprBuilder t st fs) (n + x))
forall (u :: Nat) (r :: Nat).
(1 <= u, (u + 1) <= r) =>
ExprBuilder t st fs
-> NatRepr r
-> SymBV (ExprBuilder t st fs) u
-> IO (SymBV (ExprBuilder t st fs) r)
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 Some <$> op sym newLen arg
readApp (S.WFSList [S.WFSAtom (AId Text
"_"), S.WFSAtom (AId Text
"bvfill"), S.WFSAtom (AInt Integer
width)]) [SExpr]
args =
  String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in reading bvfill expression" (ExceptT
   String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
 -> ExceptT
      String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall a b. (a -> b) -> a -> b
$ do
    sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
forall a.
(ProcessorEnv (ExprBuilder t st fs) -> a)
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
forall sym. ProcessorEnv sym -> sym
procSym
    Some arg <- readOneArg args
    case W4.exprType arg of
      BaseTypeRepr x
BaseBoolRepr -> do
        Some widthRep <- Integer
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some NatRepr)
forall (m :: Type -> Type).
MonadError String m =>
Integer -> m (Some NatRepr)
intToNatM Integer
width
        LeqProof <- fromMaybeError "must extend by a positive length" $ isPosNat widthRep
        liftIO (Some <$> W4.bvFill sym widthRep arg)
      BaseTypeRepr x
tyrep -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"Invalid argument type to bvFill: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BaseTypeRepr x -> String
forall a. Show a => a -> String
show BaseTypeRepr x
tyrep)
readApp SExpr
rator [SExpr]
rands = String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT
      String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
-> String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall a b. (a -> b) -> a -> b
$ (String
"readApp could not parse the following: "
                                      String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (Seq String -> SExpr -> Text
printSExpr Seq String
forall a. Monoid a => a
mempty (SExpr -> Text) -> SExpr -> Text
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.WFSList (SExpr
ratorSExpr -> [SExpr] -> [SExpr]
forall 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 = String -> Maybe (Some NatRepr) -> m (Some NatRepr)
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" (Maybe (Some NatRepr) -> m (Some NatRepr))
-> (Integer -> Maybe (Some NatRepr)) -> Integer -> m (Some NatRepr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Maybe (Some NatRepr)
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 -> (SExpr
 -> ArrayUpdateMap (Expr t) (i ::> itp) tp
 -> ExceptT
      String
      (ReaderT (ProcessorEnv sym) IO)
      (ArrayUpdateMap (Expr t) (i ::> itp) tp))
-> ArrayUpdateMap (Expr t) (i ::> itp) tp
-> [SExpr]
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (ArrayUpdateMap (Expr t) (i ::> itp) tp)
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 ArrayUpdateMap (Expr t) (i ::> itp) tp
forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
       (tp :: BaseType).
ArrayUpdateMap e ctx tp
WAU.empty [SExpr]
items
    SExpr
_ -> String
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (ArrayUpdateMap (Expr t) (i ::> itp) tp)
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
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
          idxs <- (forall (tp :: BaseType).
 Index (i ::> itp) tp
 -> BaseTypeRepr tp
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (IndexLit tp))
-> Assignment BaseTypeRepr (i ::> itp)
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Assignment IndexLit (i ::> itp))
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 ([SExpr]
-> Index (i ::> itp) tp
-> BaseTypeRepr tp
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (IndexLit tp)
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 x <- readExpr elt
          case testEquality arrTyRepr (W4.exprType x) of
            Just tp :~: x
Refl -> ArrayUpdateMap (Expr t) (i ::> itp) tp
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (ArrayUpdateMap (Expr t) (i ::> itp) tp)
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BaseTypeRepr tp
-> Assignment IndexLit (i ::> itp)
-> Expr t tp
-> ArrayUpdateMap (Expr t) (i ::> itp) tp
-> ArrayUpdateMap (Expr t) (i ::> itp) tp
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 tp
Expr t x
x ArrayUpdateMap (Expr t) (i ::> itp) tp
updateMap)
            Maybe (tp :~: x)
Nothing -> String
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (ArrayUpdateMap (Expr t) (i ::> itp) tp)
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError ([String] -> String
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [ String
"Invalid element type in ArrayMap update: expected "
                                            , BaseTypeRepr tp -> String
forall a. Show a => a -> String
show BaseTypeRepr tp
arrTyRepr
                                            , String
" but got "
                                            , BaseTypeRepr x -> String
forall a. Show a => a -> String
show (Expr t x -> BaseTypeRepr x
forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
x)])
        SExpr
_ -> String
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (ArrayUpdateMap (Expr t) (i ::> itp) tp)
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = Maybe a
forall a. Maybe a
Nothing
  | Bool
otherwise = Int -> [a] -> Maybe a
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) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
    go t
i (a
_:[a]
xs) = t -> [a] -> Maybe a
go (t
i t -> t -> t
forall a. Num a => a -> a -> a
- t
1) [a]
xs
    go t
_ [] = Maybe a
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 [SExpr] -> Int -> Maybe SExpr
forall a. [a] -> Int -> Maybe a
!? Index ctx tp -> Int
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)
          | NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
PN.intValue NatRepr w
w Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
w' ->
            IndexLit tp -> Processor sym (IndexLit tp)
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr w -> BV w -> IndexLit ('BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BV w -> IndexLit ('BaseBVType w)
WIL.BVIndexLit NatRepr w
w (NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
val))
          | Bool
otherwise -> String -> Processor sym (IndexLit tp)
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"Array update index bitvector size mismatch: expected " String -> String -> String
forall a. [a] -> [a] -> [a]
++ NatRepr w -> String
forall a. Show a => a -> String
show NatRepr w
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" but got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
w')
        (BaseTypeRepr tp
BaseIntegerRepr, AInt Integer
i) -> IndexLit tp -> Processor sym (IndexLit tp)
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Integer -> IndexLit 'BaseIntegerType
WIL.IntIndexLit Integer
i)
        (BaseTypeRepr tp, Atom)
_ -> String -> Processor sym (IndexLit tp)
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"Unexpected array update index type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BaseTypeRepr tp -> String
forall a. Show a => a -> String
show BaseTypeRepr tp
repr)
  | Bool
otherwise = String -> Processor sym (IndexLit tp)
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"Invalid or missing array update index at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Index ctx tp -> String
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 Assignment BaseTypeRepr (idx ::> tp)
-> AssignView BaseTypeRepr (idx ::> tp)
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 Assignment BaseTypeRepr ctx1 -> AssignView BaseTypeRepr ctx1
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 BaseTypeRepr tp -> BaseTypeRepr tp1 -> Maybe (tp :~: tp1)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: BaseType) (b :: BaseType).
BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b)
testEquality BaseTypeRepr tp
idxTpRepr BaseTypeRepr tp1
dimRepr of
            Just tp :~: tp1
Refl -> ArrayJudgment tp1 tp2 -> m (ArrayJudgment tp1 tp2)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ArrayJudgment tp1 tp2 -> m (ArrayJudgment tp1 tp2))
-> ArrayJudgment tp1 tp2 -> m (ArrayJudgment tp1 tp2)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr xs
-> ArrayJudgment tp1 (BaseArrayType (SingleCtx tp1) xs)
forall (idx :: BaseType) (res :: BaseType).
BaseTypeRepr res
-> ArrayJudgment idx (BaseArrayType (SingleCtx idx) res)
ArraySingleDim BaseTypeRepr xs
resRepr
            Maybe (tp :~: tp1)
Nothing -> String -> m (ArrayJudgment tp1 tp2)
forall a. String -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String -> m (ArrayJudgment tp1 tp2))
-> String -> m (ArrayJudgment tp1 tp2)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"Array index type", BaseTypeRepr tp -> String
forall a. Show a => a -> String
show BaseTypeRepr tp
idxTpRepr,
                                               String
"does not match", BaseTypeRepr tp1 -> String
forall a. Show a => a -> String
show BaseTypeRepr tp1
dimRepr]
        AssignView BaseTypeRepr ctx1
_ -> String -> m (ArrayJudgment tp1 tp2)
forall a. String -> m a
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 = String -> m (ArrayJudgment tp1 tp2)
forall a. String -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String -> m (ArrayJudgment tp1 tp2))
-> String -> m (ArrayJudgment tp1 tp2)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected an array, got", BaseTypeRepr tp2 -> String
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 exsAsn <- Some (Assignment ex)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (Assignment ex))
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some (Assignment ex)
 -> ExceptT
      String (ReaderT (ProcessorEnv sym) IO) (Some (Assignment ex)))
-> Some (Assignment ex)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (Assignment ex))
forall a b. (a -> b) -> a -> b
$ [Some ex] -> Some (Assignment ex)
forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList [Some ex]
exs
  exsRepr <- return $ FC.fmapFC W4.exprType exsAsn
  case testEquality exsRepr tpAssns of
    Just x :~: ctx
Refl -> Assignment ex ctx
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Assignment ex ctx)
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Assignment ex ctx
Assignment ex x
exsAsn
    Maybe (x :~: ctx)
Nothing -> String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Assignment ex ctx)
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT
      String (ReaderT (ProcessorEnv sym) IO) (Assignment ex ctx))
-> String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Assignment ex ctx)
forall a b. (a -> b) -> a -> b
$
      String
"Unexpected expression types for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Assignment ex x -> String
forall a. Show a => a -> String
show Assignment ex x
exsAsn
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nExpected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Assignment BaseTypeRepr ctx -> String
forall a. Show a => a -> String
show Assignment BaseTypeRepr ctx
tpAssns
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nGot: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Assignment BaseTypeRepr x -> String
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 = SExpr
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
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
  v <- SExpr
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
e
  R.local (\ProcessorEnv (ExprBuilder t st fs)
c -> ProcessorEnv (ExprBuilder t st fs)
c {procLetEnv = (HM.insert x v) $ procLetEnv c}) $
    readLetExpr rst body
readLetExpr [SExpr]
bindings SExpr
_body = String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT
      String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
-> String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall a b. (a -> b) -> a -> b
$
  String
"invalid s-expression for let-bindings: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([SExpr] -> String
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 = SExpr
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
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
  v <- SExpr -> Processor sym (SomeSymFn sym)
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (SomeSymFn sym)
readSymFn SExpr
e
  R.local (\ProcessorEnv sym
c -> ProcessorEnv sym
c {procLetFnEnv = (HM.insert f v) $ procLetFnEnv c}) $
    readLetExpr rst body
readLetFnExpr [SExpr]
bindings SExpr
_body = String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT
      String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
-> String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall a b. (a -> b) -> a -> b
$
  String
"invalid s-expression for let-bindings: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([SExpr] -> String
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
  sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
forall a.
(ProcessorEnv (ExprBuilder t st fs) -> a)
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
forall sym. ProcessorEnv sym -> sym
procSym
  liftIO $ (Some <$> W4.intLit sym n)
readExpr (S.WFSAtom (ANat Nat
_)) =
  String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
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
  sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
forall a.
(ProcessorEnv (ExprBuilder t st fs) -> a)
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
forall sym. ProcessorEnv sym -> sym
procSym
  liftIO $ return $ Some $ W4.backendPred sym b
readExpr (S.WFSAtom (AFloat (Some FloatPrecisionRepr x
repr) BigFloat
bf)) = do
  sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
forall a.
(ProcessorEnv (ExprBuilder t st fs) -> a)
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
forall sym. ProcessorEnv sym -> sym
procSym
  liftIO $ (Some <$> W4.floatLit sym repr bf)
readExpr (S.WFSAtom (AStr Some StringInfoRepr
prefix Text
content)) = do
  sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
forall a.
(ProcessorEnv (ExprBuilder t st fs) -> a)
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
forall sym. ProcessorEnv sym -> sym
procSym
  case prefix of
    (Some StringInfoRepr x
W4.UnicodeRepr) -> do
      s <- IO (Expr t ('BaseStringType 'Unicode))
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Expr t ('BaseStringType 'Unicode))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (Expr t ('BaseStringType 'Unicode))
 -> ExceptT
      String
      (ReaderT (ProcessorEnv sym) IO)
      (Expr t ('BaseStringType 'Unicode)))
-> IO (Expr t ('BaseStringType 'Unicode))
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Expr t ('BaseStringType 'Unicode))
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs
-> StringLiteral 'Unicode
-> IO (SymString (ExprBuilder t st fs) 'Unicode)
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
forall (si :: StringInfo).
ExprBuilder t st fs
-> StringLiteral si -> IO (SymString (ExprBuilder t st fs) si)
W4.stringLit ExprBuilder t st fs
sym (StringLiteral 'Unicode
 -> IO (SymString (ExprBuilder t st fs) 'Unicode))
-> StringLiteral 'Unicode
-> IO (SymString (ExprBuilder t st fs) 'Unicode)
forall a b. (a -> b) -> a -> b
$ Text -> StringLiteral 'Unicode
W4.UnicodeLiteral Text
content
      return $ Some $ s
    (Some StringInfoRepr x
W4.Char8Repr) -> do
      s <- IO (Expr t (BaseStringType 'Char8))
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Expr t (BaseStringType 'Char8))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (Expr t (BaseStringType 'Char8))
 -> ExceptT
      String
      (ReaderT (ProcessorEnv sym) IO)
      (Expr t (BaseStringType 'Char8)))
-> IO (Expr t (BaseStringType 'Char8))
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Expr t (BaseStringType 'Char8))
forall a b. (a -> b) -> a -> b
$ ExprBuilder t st fs
-> StringLiteral 'Char8
-> IO (SymString (ExprBuilder t st fs) 'Char8)
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
forall (si :: StringInfo).
ExprBuilder t st fs
-> StringLiteral si -> IO (SymString (ExprBuilder t st fs) si)
W4.stringLit ExprBuilder t st fs
sym (StringLiteral 'Char8
 -> IO (SymString (ExprBuilder t st fs) 'Char8))
-> StringLiteral 'Char8
-> IO (SymString (ExprBuilder t st fs) 'Char8)
forall a b. (a -> b) -> a -> b
$ ByteString -> StringLiteral 'Char8
W4.Char8Literal (ByteString -> StringLiteral 'Char8)
-> ByteString -> StringLiteral 'Char8
forall a b. (a -> b) -> a -> b
$ Text -> ByteString
T.encodeUtf8 Text
content
      return $ Some $ s
    (Some StringInfoRepr x
W4.Char16Repr) -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ String
"Char16 strings are not yet supported"
readExpr (S.WFSAtom (AReal Rational
_)) = String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT
      String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym)))
-> String
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
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.
  sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
forall a.
(ProcessorEnv (ExprBuilder t st fs) -> a)
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
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 someNat (toInteger len) of
    Just (Some NatRepr x
lenRepr) -> do
        pf <- case NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
lenRepr of
                Just LeqProof 1 x
pf -> LeqProof 1 x
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (LeqProof 1 x)
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return LeqProof 1 x
pf
                Maybe (LeqProof 1 x)
Nothing -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (LeqProof 1 x)
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"What4.Serialize.Parser.readExpr isPosNat failure"
        liftIO $ withLeqProof pf (Some <$> W4.bvLit sym lenRepr (BV.mkBV lenRepr val))
    Maybe (Some NatRepr)
Nothing -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
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
  maybeBinding <- Text -> Processor sym (Maybe (Some (SymExpr sym)))
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 maybeBinding of
    -- simply return it's bound value
    Just Some (Expr t)
binding -> Some (Expr t)
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Some (Expr t)
binding
    Maybe (Some (Expr t))
Nothing -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a b. (a -> b) -> a -> b
$ (String
"Unbound variable encountered during deserialization: "
                               String -> String -> String
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] -> [SExpr]
-> SExpr
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
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]
_ -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
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] -> [SExpr]
-> SExpr
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
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]
_ -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"ill-formed letfn s-expression"
readExpr (S.WFSList []) = String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
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)) = SExpr
-> [SExpr]
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (SymExpr sym))
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 = (SExpr
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t)))
-> [SExpr]
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Some (Expr t)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM SExpr -> Processor sym (Some (SymExpr sym))
SExpr
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (Some (Expr t))
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 = [Some (Expr t)] -> Some (Assignment (Expr t))
forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList ([Some (Expr t)] -> Some (Assignment (Expr t)))
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Some (Expr t)]
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some (Assignment (Expr t)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [SExpr] -> Processor sym [Some (SymExpr sym)]
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 [SExpr] -> Maybe ([SExpr], SExpr)
forall a. [a] -> Maybe ([a], a)
unsnoc [SExpr]
typeSExprs of
    Maybe ([SExpr], SExpr)
Nothing ->
      String -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr))
-> String -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
forall a b. (a -> b) -> a -> b
$ (String
"invalid type signature for function: "
                      String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr Seq String
forall a. Monoid a => a
mempty ([SExpr] -> SExpr
forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [SExpr]
typeSExprs)))
    Just ([SExpr]
domSExps, SExpr
retSExp) -> do
      dom <- (SExpr
 -> ExceptT
      String (ReaderT (ProcessorEnv sym) IO) (Some BaseTypeRepr))
-> [SExpr]
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) [Some BaseTypeRepr]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM SExpr
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (Some BaseTypeRepr)
forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some BaseTypeRepr)
readBaseType [SExpr]
domSExps
      ret <- readBaseType retSExp
      return (dom, ret)
readFnType SExpr
sexpr =
  String -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr))
-> String -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
forall a b. (a -> b) -> a -> b
$ (String
"invalid type signature for function: "
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr Seq String
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 []     = Maybe ([a], a)
forall a. Maybe a
Nothing
unsnoc (a
x:[a]
xs) = case [a] -> Maybe ([a], a)
forall a. [a] -> Maybe ([a], a)
unsnoc [a]
xs of
                  Maybe ([a], a)
Nothing    -> ([a], a) -> Maybe ([a], a)
forall a. a -> Maybe a
Just ([], a
x)
                  Just ([a]
a,a
b) -> ([a], a) -> Maybe ([a], a)
forall a. a -> Maybe a
Just (a
xa -> [a] -> [a]
forall 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 [] = [Text] -> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Text]
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return []
readFnArgs ((S.WFSAtom (AId Text
name)):[SExpr]
rest) = do
  names <- ([SExpr] -> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Text]
forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
[SExpr] -> Processor sym [Text]
readFnArgs [SExpr]
rest)
  return $ name:names
readFnArgs (SExpr
badArg:[SExpr]
_) =
  String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Text]
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Text])
-> String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) [Text]
forall a b. (a -> b) -> a -> b
$ (String
"invalid function argument encountered: "
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr Seq String
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) = SymExpr sym x -> Some (SymExpr sym)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (sym -> BoundVar sym x -> SymExpr sym x
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> SymExpr sym tp
forall (tp :: BaseType). 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
  sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
forall a.
(ProcessorEnv (ExprBuilder t st fs) -> a)
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
forall sym. ProcessorEnv sym -> sym
procSym
  symFnName <- case W4.userSymbol (T.unpack rawSymFnName) of
                 Left SolverSymbolError
_ -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol)
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol
forall a b. (a -> b) -> a -> b
$ (String
"Bad symbolic function name : "
                                           String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack Text
rawSymFnName))
                 Right SolverSymbol
solverSym -> SolverSymbol
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return SolverSymbol
solverSym
  argNames <- readFnArgs argVarsRaw
  (argTys, _retTy) <- readFnType rawFnType
  when (not (length argTys == length argNames)) $
    E.throwError $ "Function type expected "
    ++ (show $ length argTys)
    ++ " args but found "
    ++ (show $ length argNames)
  argVars <- mapM (\(Text
name, (Some BaseTypeRepr x
ty)) ->
                     case String -> Either SolverSymbolError SolverSymbol
W4.userSymbol (Text -> String
T.unpack Text
name) of
                       Left SolverSymbolError
_ -> String
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Some (BoundVar (ExprBuilder t st fs)))
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT
      String
      (ReaderT (ProcessorEnv sym) IO)
      (Some (BoundVar (ExprBuilder t st fs))))
-> String
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Some (BoundVar (ExprBuilder t st fs)))
forall a b. (a -> b) -> a -> b
$ String
"Bad arg name : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack Text
name)
                       Right SolverSymbol
solverSym -> IO (Some (BoundVar (ExprBuilder t st fs)))
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Some (BoundVar (ExprBuilder t st fs)))
forall a. IO a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (Some (BoundVar (ExprBuilder t st fs)))
 -> ExceptT
      String
      (ReaderT (ProcessorEnv sym) IO)
      (Some (BoundVar (ExprBuilder t st fs))))
-> IO (Some (BoundVar (ExprBuilder t st fs)))
-> ExceptT
     String
     (ReaderT (ProcessorEnv sym) IO)
     (Some (BoundVar (ExprBuilder t st fs)))
forall a b. (a -> b) -> a -> b
$ ExprBoundVar t x -> Some (BoundVar (ExprBuilder t st fs))
ExprBoundVar t x -> Some (ExprBoundVar t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (ExprBoundVar t x -> Some (BoundVar (ExprBuilder t st fs)))
-> IO (ExprBoundVar t x)
-> IO (Some (BoundVar (ExprBuilder t st fs)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr x
-> IO (BoundVar (ExprBuilder t st fs) x)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
forall (tp :: BaseType).
ExprBuilder t st fs
-> SolverSymbol
-> BaseTypeRepr tp
-> IO (BoundVar (ExprBuilder t st fs) tp)
W4.freshBoundVar ExprBuilder t st fs
sym SolverSymbol
solverSym BaseTypeRepr x
ty)
             $ zip argNames argTys
  (Some body) <- let newBindings = [(Text, Some (SymExpr (ExprBuilder t st fs)))]
-> HashMap Text (Some (SymExpr (ExprBuilder t st fs)))
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HM.fromList
                                   ([(Text, Some (SymExpr (ExprBuilder t st fs)))]
 -> HashMap Text (Some (SymExpr (ExprBuilder t st fs))))
-> [(Text, Some (SymExpr (ExprBuilder t st fs)))]
-> HashMap Text (Some (SymExpr (ExprBuilder t st fs)))
forall a b. (a -> b) -> a -> b
$ [Text]
-> [Some (SymExpr (ExprBuilder t st fs))]
-> [(Text, Some (SymExpr (ExprBuilder t st fs)))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
argNames
                                   ([Some (SymExpr (ExprBuilder t st fs))]
 -> [(Text, Some (SymExpr (ExprBuilder t st fs)))])
-> [Some (SymExpr (ExprBuilder t st fs))]
-> [(Text, Some (SymExpr (ExprBuilder t st fs)))]
forall a b. (a -> b) -> a -> b
$ (Some (BoundVar (ExprBuilder t st fs))
 -> Some (SymExpr (ExprBuilder t st fs)))
-> [Some (BoundVar (ExprBuilder t st fs))]
-> [Some (SymExpr (ExprBuilder t st fs))]
forall a b. (a -> b) -> [a] -> [b]
map (ExprBuilder t st fs
-> Some (BoundVar (ExprBuilder t st fs))
-> Some (SymExpr (ExprBuilder t st fs))
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 R.local
                    (\ProcessorEnv (ExprBuilder t st fs)
env -> ProcessorEnv (ExprBuilder t st fs)
env {procLetEnv = HM.union (procLetEnv env) newBindings})
                    $ readExpr bodyRaw
  Some argVarAssignment <- return $ Ctx.fromList argVars
  symFn <- liftIO $ W4.definedFn sym symFnName argVarAssignment body W4.UnfoldConcrete
  return $ SomeSymFn symFn
readSymFn badSExp :: SExpr
badSExp@(S.WFSList ((S.WFSAtom (AId Text
"definedfn")):[SExpr]
_)) =
  String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (SomeSymFn sym)
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (SomeSymFn sym))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (SomeSymFn sym)
forall a b. (a -> b) -> a -> b
$ (String
"invalid `definedfn`: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr Seq String
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
  sym <- (ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs)
-> ExceptT
     String (ReaderT (ProcessorEnv sym) IO) (ExprBuilder t st fs)
forall a.
(ProcessorEnv (ExprBuilder t st fs) -> a)
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader ProcessorEnv (ExprBuilder t st fs) -> ExprBuilder t st fs
forall sym. ProcessorEnv sym -> sym
procSym
  symFnName <- case W4.userSymbol (T.unpack rawSymFnName) of
                 Left SolverSymbolError
_ -> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol)
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol
forall a b. (a -> b) -> a -> b
$ (String
"Bad symbolic function name : "
                                           String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack Text
rawSymFnName))
                 Right SolverSymbol
solverSym -> SolverSymbol
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) SolverSymbol
forall a. a -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall (m :: Type -> Type) a. Monad m => a -> m a
return SolverSymbol
solverSym
  (argTys, (Some retTy)) <- readFnType rawFnType
  Some domain <- return $ Ctx.fromList argTys
  symFn <- liftIO $ W4.freshTotalUninterpFn sym symFnName domain retTy
  return $ SomeSymFn symFn
readSymFn badSExp :: SExpr
badSExp@(S.WFSList ((S.WFSAtom (AId Text
"uninterpfn")):[SExpr]
_)) =
  String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (SomeSymFn sym)
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
 -> ExceptT String (ReaderT (ProcessorEnv sym) IO) (SomeSymFn sym))
-> String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (SomeSymFn sym)
forall a b. (a -> b) -> a -> b
$ (String
"invalid `uninterpfn`: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr Seq String
forall a. Monoid a => a
mempty SExpr
badSExp))
readSymFn SExpr
sexpr = String
-> ExceptT String (ReaderT (ProcessorEnv sym) IO) (SomeSymFn sym)
forall a.
String -> ExceptT String (ReaderT (ProcessorEnv sym) IO) a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"invalid function definition: "
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr Seq String
forall a. Monoid a => a
mempty SExpr
sexpr))