content: {-# 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
    { cSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
    -- ^ The mapping of names to defined What4 SymFns.
    , 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 _sym = Config { cSymFnLookup = const (return Nothing)
                              , cExprLookup = const (return Nothing)
                              }
  
  
  -- | The lexical environment for parsing s-expressions and
  -- procesing them into What4 terms.
  data ProcessorEnv sym =
    ProcessorEnv
    { procSym :: sym
    -- ^ The symbolic What4 backend being used.
    , procSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
      -- ^ The user-specified mapping of names to defined What4 SymFns.
    , procExprLookup :: Text -> IO (Maybe (Some (W4.SymExpr sym)))
    -- ^ The user-specified mapping of names to defined What4 expressions.
    , 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.
    , 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 env action = R.runReaderT (E.runExceptT action) env
  
  lookupExpr :: Text -> Processor sym (Maybe (Some (W4.SymExpr sym)))
  lookupExpr nm = do
    userLookupFn <- R.asks procExprLookup
    letEnv <- R.asks procLetEnv
    case HM.lookup nm letEnv of
      Nothing -> liftIO $ userLookupFn nm
      res -> return res
  
  lookupFn :: Text -> Processor sym (Maybe (SomeSymFn sym))
  lookupFn nm = do
    userLookupFn <- R.asks procSymFnLookup
    letEnv <- R.asks procLetFnEnv
    case HM.lookup nm letEnv of
      Nothing -> liftIO $ userLookupFn nm
      res -> return 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 sym = deserializeExprWithConfig sym cfg
    where cfg = defaultConfig 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 sym cfg sexpr = runProcessor env (readExpr sexpr)
    where env = ProcessorEnv { procSym = sym
                             , procSymFnLookup = cSymFnLookup cfg
                             , procExprLookup = cExprLookup cfg
                             , procLetEnv = HM.empty
                             , procLetFnEnv = 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 sym = deserializeSymFnWithConfig sym cfg
    where cfg = defaultConfig sym
  
  deserializeSymFnWithConfig ::
    forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
    => sym
    -> Config sym
    -> SExpr
    -> IO (Either String (SomeSymFn sym))
  deserializeSymFnWithConfig sym cfg sexpr = runProcessor env (readSymFn sexpr)
    where env = ProcessorEnv { procSym = sym
                             , procSymFnLookup = cSymFnLookup cfg
                             , procExprLookup = cExprLookup cfg
                             , procLetEnv = HM.empty
                             , procLetFnEnv = HM.empty
                             }
  
  
  deserializeBaseType ::
    SExpr
    -> Either String (Some BaseTypeRepr)
  deserializeBaseType sexpr = readBaseType 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 prefix act = E.catchError act (E.throwError . mappend prefix)
  
  -- | Utility function for lifting a 'Maybe' into a 'MonadError'
  fromMaybeError :: (E.MonadError e m) => e -> Maybe a -> m a
  fromMaybeError err = maybe (E.throwError err) return
  
  
  readBaseType ::
    forall m . (E.MonadError String m)
    => SExpr
    -> m (Some BaseTypeRepr)
  readBaseType sexpr =
    case sexpr of
      S.WFSAtom (AId atom) ->
        case (T.unpack atom) of
          "Bool" -> return $ Some BaseBoolRepr
          "Int" -> return $ Some BaseIntegerRepr
          "Real" -> return $ Some BaseRealRepr
          "String" -> return $ Some (BaseStringRepr UnicodeRepr)
          "Complex" -> return $ Some BaseComplexRepr
          _ -> panic
      S.WFSList [(S.WFSAtom (AId "BV")), (S.WFSAtom (AInt w))]
        | Just (Some wRepr) <- someNat w
        , Just LeqProof <- testLeq (knownNat @1) wRepr
          -> return $ Some (BaseBVRepr wRepr)
        | otherwise
          -> panic
      S.WFSList [(S.WFSAtom (AId "Float")), (S.WFSAtom (AInt e)), (S.WFSAtom (AInt s))]
        | Just (Some eRepr) <- someNat e
        , Just (Some sRepr) <- someNat s
        , Just LeqProof <- testLeq (knownNat @2) eRepr
        , Just LeqProof <- testLeq (knownNat @2) sRepr
          -> return (Some (BaseFloatRepr (FloatingPointPrecisionRepr eRepr sRepr)))
        | otherwise -> panic
      S.WFSList [(S.WFSAtom (AId "Struct")), args] -> do
        Some tps <- readBaseTypes args
        return $ Some (BaseStructRepr tps)
      S.WFSList [S.WFSAtom (AId "Array"), ixArgs, tpArg] -> do
        Some ixs <- readBaseTypes ixArgs
        Some tp <- readBaseType tpArg
        case Ctx.viewAssign ixs of
          Ctx.AssignEmpty -> E.throwError $ "array type has no indices: " ++ show sexpr
          Ctx.AssignExtend _ _ -> return $ Some (BaseArrayRepr ixs tp)
      _ -> panic
    where
      panic = E.throwError $ "unknown base type: " ++ show sexpr
  
  readBaseTypes ::
    forall m . (E.MonadError String m)
    => SExpr
    -> m (Some (Ctx.Assignment BaseTypeRepr))
  readBaseTypes sexpr@(S.WFSAtom _) = E.throwError $ "expected list of base types: " ++ show sexpr
  readBaseTypes (S.WFSList sexprs) = Ctx.fromList <$> mapM readBaseType 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 expr =
    case W4.exprType expr of
      BaseBVRepr n -> return $ BVProof n
      t -> E.throwError $ printf "expected BV, found %s" (show 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 name = HM.lookup name opTable
  
  
  opTable :: (W4.IsSymExprBuilder sym) => HM.HashMap Text (Op sym)
  opTable =
    HM.fromList [
    -- -- -- Boolean ops -- -- --
      ("andp", Op2 knownRepr $ W4.andPred)
    , ("orp", Op2 knownRepr $ W4.orPred)
    , ("xorp", Op2 knownRepr $ W4.xorPred)
    , ("notp", Op1 knownRepr $ W4.notPred)
    -- -- -- Float ops -- -- --
    , ("floatneg", FloatOp1 W4.floatNeg)
    , ("floatabs", FloatOp1 W4.floatAbs)
    -- -- -- Integer ops -- -- --
    , ("intmul", Op2 knownRepr $ W4.intMul)
    , ("intadd", Op2 knownRepr $ W4.intAdd)
    , ("intmod", Op2 knownRepr $ W4.intMod)
    , ("intdiv", Op2 knownRepr $ W4.intDiv)
    , ("intle", Op2 knownRepr $ W4.intLe)
    , ("intabs", Op1 knownRepr $ W4.intAbs)
    -- -- -- Bitvector ops -- -- --
    , ("bvand", BVOp2 W4.bvAndBits)
    , ("bvor", BVOp2 W4.bvOrBits)
    , ("bvadd", BVOp2 W4.bvAdd)
    , ("bvmul", BVOp2 W4.bvMul)
    , ("bvudiv", BVOp2 W4.bvUdiv)
    , ("bvurem", BVOp2 W4.bvUrem)
    , ("bvshl", BVOp2 W4.bvShl)
    , ("bvlshr", BVOp2 W4.bvLshr)
    , ("bvnand", BVOp2 $ \sym arg1 arg2 -> W4.bvNotBits sym =<< W4.bvAndBits sym arg1 arg2)
    , ("bvnor", BVOp2 $ \sym arg1 arg2 -> W4.bvNotBits sym =<< W4.bvOrBits sym arg1 arg2)
    , ("bvxor", BVOp2 W4.bvXorBits)
    , ("bvxnor", BVOp2 $ \sym arg1 arg2 -> W4.bvNotBits sym =<< W4.bvXorBits sym arg1 arg2)
    , ("bvsub", BVOp2 W4.bvSub)
    , ("bvsdiv", BVOp2 W4.bvSdiv)
    , ("bvsrem", BVOp2 W4.bvSrem)
    , ("bvsmod", error "bvsmod is not implemented")
    , ("bvashr", BVOp2 W4.bvAshr)
    , ("bvult", BVComp2 W4.bvUlt)
    , ("bvule", BVComp2 W4.bvUle)
    , ("bvugt", BVComp2 W4.bvUgt)
    , ("bvuge", BVComp2 W4.bvUge)
    , ("bvslt", BVComp2 W4.bvSlt)
    , ("bvsle", BVComp2 W4.bvSle)
    , ("bvsgt", BVComp2 W4.bvSgt)
    , ("bvsge", BVComp2 W4.bvSge)
    , ("bveq", BVComp2 W4.bvEq)
    , ("bvne", BVComp2 W4.bvNe)
    , ("bvneg", BVOp1 W4.bvNeg)
    , ("bvnot", BVOp1 W4.bvNotBits)
    -- -- -- Floating point ops -- -- --
    , ("fnegd", Op1 knownRepr $ W4.floatNeg @_ @Prec64)
    , ("fnegs", Op1 knownRepr $ W4.floatNeg @_ @Prec32)
    , ("fabsd", Op1 knownRepr $ W4.floatAbs @_ @Prec64)
    , ("fabss", Op1 knownRepr $ W4.floatAbs @_ @Prec32)
    , ("fsqrt", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->
      W4.floatSqrt @_ @Prec64 sym rm x)
    , ("fsqrts", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->
      W4.floatSqrt @_ @Prec32 sym rm x)
    , ("fnand", Op1 knownRepr $ W4.floatIsNaN @_ @Prec64)
    , ("fnans", Op1 knownRepr $ W4.floatIsNaN @_ @Prec32)
    , ("frsp", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->
      W4.floatCast @_ @Prec32 @Prec64 sym knownRepr rm x)
    , ("fp_single_to_double", Op1 knownRepr $ \sym ->
      W4.floatCast @_ @Prec64 @Prec32 sym knownRepr W4.RNE)
    , ("fp_binary_to_double",
       Op1 knownRepr $ \sym -> W4.floatFromBinary @_ @11 @53 sym knownRepr)
    , ("fp_binary_to_single",
       Op1 knownRepr $ \sym -> W4.floatFromBinary @_ @8 @24 sym knownRepr)
    , ("fp_double_to_binary", Op1 knownRepr $ W4.floatToBinary @_ @11 @53)
    , ("fp_single_to_binary", Op1 knownRepr $ W4.floatToBinary @_ @8 @24)
    , ("fctid", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->
      W4.floatToSBV @_ @64 @Prec64 sym knownRepr rm x)
    , ("fctidu", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->
      W4.floatToBV @_ @64 @Prec64 sym knownRepr rm x)
    , ("fctiw", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->
      W4.floatToSBV @_ @32 @Prec64 sym knownRepr rm x)
    , ("fctiwu", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->
      W4.floatToBV @_ @32 @Prec64 sym knownRepr rm x)
    , ("fcfid", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->
      W4.sbvToFloat @_ @64 @Prec64 sym knownRepr rm x)
    , ("fcfids", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->
      W4.sbvToFloat @_ @64 @Prec32 sym knownRepr rm x)
    , ("fcfidu", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->
      W4.bvToFloat @_ @64 @Prec64 sym knownRepr rm x)
    , ("fcfidus", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->
      W4.bvToFloat @_ @64 @Prec32 sym knownRepr rm x)
    , ("frti", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->
      W4.floatRound @_ @Prec64 sym rm x)
    , ("frtis", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->
      W4.floatRound @_ @Prec32 sym rm x)
    , ("fadd", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->
      W4.floatAdd @_ @Prec64 sym rm x y)
    , ("fadds", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->
      W4.floatAdd @_ @Prec32 sym rm x y)
    , ("fsub", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->
      W4.floatSub @_ @Prec64 sym rm x y)
    , ("fsubs", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->
      W4.floatSub @_ @Prec32 sym rm x y)
    , ("fmul", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->
      W4.floatMul @_ @Prec64 sym rm x y)
    , ("fmuls", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->
      W4.floatMul @_ @Prec32 sym rm x y)
    , ("fdiv", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->
      W4.floatDiv @_ @Prec64 sym rm x y)
    , ("fdivs", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->
      W4.floatDiv @_ @Prec32 sym rm x y)
    , ("fltd", Op2 knownRepr $ W4.floatLt @_ @Prec64)
    , ("flts", Op2 knownRepr $ W4.floatLt @_ @Prec32)
    , ("feqd", Op2 knownRepr $ W4.floatFpEq @_ @Prec64)
    , ("feqs", Op2 knownRepr $ W4.floatFpEq @_ @Prec32)
    , ("fled", Op2 knownRepr $ W4.floatLe @_ @Prec64)
    , ("fles", Op2 knownRepr $ W4.floatLe @_ @Prec32)
    , ("ffma", Op4 knownRepr $ \sym r x y z -> U.withRounding sym r $ \rm ->
      W4.floatFMA @_ @Prec64 sym rm x y z)
    , ("ffmas", Op4 knownRepr $ \sym r x y z ->
      U.withRounding sym r $ \rm -> W4.floatFMA @_ @Prec32 sym rm x y 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 operands = do
    args <- readExprs operands
    case args of
      [arg] -> return arg
      _ -> E.throwError $ printf "expecting 1 argument, got %d" (length 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 operands = do
    args <- readExprs operands
    case args of
      [arg1, arg2] -> return (arg1, arg2)
      _ -> E.throwError $ printf "expecting 2 arguments, got %d" (length 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 operands = do
    args <- readExprs operands
    case args of
      [arg1, arg2, arg3] -> return (arg1, arg2, arg3)
      _ -> E.throwError $ printf "expecting 3 arguments, got %d" (length 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 (S.WFSAtom (AId "call")) (S.WFSAtom (AId fnName):operands) = do
    sym <- R.asks procSym
    maybeFn <- lookupFn fnName
    case maybeFn of
      Just (SomeSymFn fn) -> do
        args <- mapM readExpr operands
        assn <- exprAssignment (W4.fnArgTypes fn) args
        liftIO (Some <$> W4.applySymFn sym fn assn)
      Nothing -> E.throwError $ "The function name `"
                 ++(T.unpack fnName)
                 ++"` is not bound to a SymFn in the current Config."
  readApp opRaw@(S.WFSAtom (AId "call")) operands = E.throwError
    $ "Unrecognized use of `call`: " ++ (T.unpack (printSExpr mempty (S.L (opRaw:operands))))
  readApp opRaw@(S.WFSAtom (AId operator)) operands = do
    sym <- R.reader 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 fn) -> do
          args <- readExprs operands
          case args of
            [Some a1]
              | BaseFloatRepr _ <- W4.exprType a1 -> liftIO (Some <$> fn sym a1)
            _ -> E.throwError "Unable to unpack FloatOp1 arg in Formula.Parser readApp"
        Just (Op1 arg_types fn) -> do
          args <- readExprs operands
          exprAssignment arg_types args >>= \case
            Ctx.Empty Ctx.:> arg1 ->
              liftIO (Some <$> fn sym arg1)
        Just (Op2 arg_types fn) -> do
          args <- readExprs operands
          exprAssignment arg_types args >>= \case
            Ctx.Empty Ctx.:> arg1 Ctx.:> arg2 ->
                liftIO (Some <$> fn sym arg1 arg2)
        Just (Op3 arg_types fn) -> do
          args <- readExprs operands
          exprAssignment arg_types args >>= \case
            Ctx.Empty Ctx.:> arg1 Ctx.:> arg2 Ctx.:> arg3 ->
                liftIO (Some <$> fn sym arg1 arg2 arg3)
        Just (Op4 arg_types fn) -> do
          args <- readExprs operands
          exprAssignment arg_types args >>= \case
            Ctx.Empty Ctx.:> arg1 Ctx.:> arg2 Ctx.:> arg3 Ctx.:> arg4 ->
                liftIO (Some <$> fn sym arg1 arg2 arg3 arg4)
        Just (BVOp1 op) -> do
          Some expr <- readOneArg operands
          BVProof _ <- getBVProof expr
          liftIO $ Some <$> op sym expr
        Just (BVOp2 op) -> do
          (Some arg1, Some arg2)  <- readTwoArgs operands
          BVProof m <- prefixError "in arg 1: " $ getBVProof arg1
          BVProof n <- prefixError "in arg 2: " $ getBVProof arg2
          case testEquality m n of
            Just Refl -> liftIO (Some <$> op sym arg1 arg2)
            Nothing -> E.throwError $ printf "arguments to %s must be the same length, \
                                           \but arg 1 has length %s \
                                           \and arg 2 has length %s"
                                           operator
                                           (show m)
                                           (show n)
        Just (BVComp2 op) -> do
          (Some arg1, Some arg2)  <- readTwoArgs operands
          BVProof m <- prefixError "in arg 1: " $ getBVProof arg1
          BVProof n <- prefixError "in arg 2: " $ getBVProof arg2
          case testEquality m n of
            Just Refl -> liftIO (Some <$> op sym arg1 arg2)
            Nothing -> E.throwError $ printf "arguments to %s must be the same length, \
                                           \but arg 1 has length %s \
                                           \and arg 2 has length %s"
                                           operator
                                           (show m)
                                           (show n)
        Nothing ->
          -- Operators/syntactic-forms with types too
          -- complicated to nicely fit in the Op type
          case operator of
            "concat" -> do
              (Some arg1, Some arg2)  <- readTwoArgs operands
              BVProof _ <- prefixError "in arg 1: " $ getBVProof arg1
              BVProof _ <- prefixError "in arg 2: " $ getBVProof arg2
              liftIO (Some <$> W4.bvConcat sym arg1 arg2)
            "=" -> do
              (Some arg1, Some arg2)  <- readTwoArgs operands
              case testEquality (W4.exprType arg1) (W4.exprType arg2) of
                Just Refl -> liftIO (Some <$> W4.isEq sym arg1 arg2)
                Nothing -> E.throwError $
                  printf "arguments must have same types, \
                         \but arg 1 has type %s \
                         \and arg 2 has type %s"
                  (show (W4.exprType arg1))
                  (show (W4.exprType arg2))
            "ite" -> do
              (Some test, Some then_, Some else_)  <- readThreeArgs operands
              case W4.exprType test of
                BaseBoolRepr ->
                  case testEquality (W4.exprType then_) (W4.exprType else_) of
                    Just Refl -> liftIO (Some <$> W4.baseTypeIte sym test then_ else_)
                    Nothing -> E.throwError $
                      printf "then and else branches must have same type, \
                             \but then has type %s \
                             \and else has type %s"
                      (show (W4.exprType then_))
                      (show (W4.exprType else_))
                tp -> E.throwError $ printf "test expression must be a boolean; got %s" (show tp)
            "select" -> do
              (Some arr, Some idx)  <- readTwoArgs operands
              ArraySingleDim _ <- expectArrayWithIndex (W4.exprType idx) (W4.exprType arr)
              let idx' = Ctx.empty Ctx.:> idx
              liftIO (Some <$> W4.arrayLookup sym arr idx')
            "store" -> do
              (Some arr, Some idx, Some expr)  <- readThreeArgs operands
              ArraySingleDim resRepr <- expectArrayWithIndex (W4.exprType idx) (W4.exprType arr)
              case testEquality resRepr (W4.exprType expr) of
                Just Refl ->
                  let idx' = Ctx.empty Ctx.:> idx
                  in liftIO (Some <$> W4.arrayUpdate sym arr idx' expr)
                Nothing -> E.throwError $ printf "Array result type %s does not match %s"
                           (show resRepr)
                           (show (W4.exprType expr))
            "updateArray" -> do
              (Some arr, Some idx, Some expr)  <- readThreeArgs operands
              ArraySingleDim resRepr <- expectArrayWithIndex (W4.exprType idx) (W4.exprType arr)
              case testEquality resRepr (W4.exprType expr) of
                Just Refl ->
                  let idx' = Ctx.empty Ctx.:> idx
                  in liftIO (Some <$> W4.arrayUpdate sym arr idx' expr)
                Nothing -> E.throwError $ printf "Array result type %s does not match %s"
                           (show resRepr)
                           (show (W4.exprType expr))
  
            "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 operands of
                [updateSExprList, arrSExpr] -> do
                  Some arrExpr <- readExpr arrSExpr
                  case W4.exprType arrExpr of
                    BaseArrayRepr idxReprs arrTyRepr -> do
                      updateMap <- expectArrayUpdateMap idxReprs arrTyRepr updateSExprList
                      liftIO (Some <$> W4.sbMakeExpr sym (W4.ArrayMap idxReprs arrTyRepr updateMap arrExpr))
                    repr -> E.throwError $ unwords ["expected an array type for the value in 'arrayMap', but got", show repr]
                _ -> E.throwError $ unwords ["expected a list of indices and an array expression, but got", show operands]
  
            "field" -> do
              case operands of
                [rawStruct, S.WFSAtom (AInt rawIdx)] -> do
                  Some struct  <- readExpr rawStruct
                  case W4.exprType struct of
                    (BaseStructRepr fldTpReprs) ->
                      case Ctx.intIndex (fromInteger rawIdx) (Ctx.size fldTpReprs) of
                        Just (Some i) -> liftIO (Some <$> W4.structField sym struct i)
                        Nothing -> E.throwError $
                          unwords ["invalid struct index, got", show fldTpReprs, "and", show rawIdx]
                    srepr -> E.throwError $ unwords ["expected a struct, got", show srepr]
                _ -> E.throwError $ unwords ["expected an arg and an Int, got", show operands]
            "struct" -> do
              case operands of
                [S.WFSList rawFldExprs] -> do
                  Some flds <- readExprsAsAssignment rawFldExprs
                  liftIO (Some <$> W4.mkStruct sym flds)
                _ -> E.throwError $ unwords ["struct expects a single operand, got", show operands]
            "sbvToInteger" -> do
              (Some arg) <- readOneArg operands
              BVProof _ <- getBVProof arg
              liftIO $ Some <$> W4.sbvToInteger sym arg
            "bvToInteger" -> do
              (Some arg) <- readOneArg operands
              BVProof _ <- getBVProof arg
              liftIO $ Some <$> W4.bvToInteger sym arg
            "integerToBV" -> do
              case operands of
                [S.WFSAtom (ANat width), rawValExpr] -> do
                  Some x <- readExpr rawValExpr
                  case (mkNatRepr width, W4.exprType x) of
                    (Some w, BaseIntegerRepr)
                      | Just LeqProof <- isPosNat w -> do
                      liftIO (Some <$> W4.integerToBV sym x w)
                    srepr -> E.throwError $ unwords ["expected a non-zero natural and an integer, got", show srepr]
                _ -> E.throwError $ unwords ["integerToBV expects two operands, the first of which is a nat, got", show operands]
            _ -> E.throwError $ printf "couldn't parse application of %s" (printSExpr mempty opRaw)
  -- Parse an expression of the form @((_ extract i j) x)@.
  readApp (S.WFSList [S.WFSAtom (AId "_"), S.WFSAtom (AId "extract"), S.WFSAtom (AInt iInt), S.WFSAtom (AInt jInt)])
    args = prefixError "in reading extract expression: " $ do
    sym <- R.reader 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 = iInt - jInt + 1
        idxInt = 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 "_"), S.WFSAtom (AId extend), S.WFSAtom (AInt iInt)])
    args
    | extend == "zero_extend" ||
      extend == "sign_extend" = prefixError (printf "in reading %s expression: " extend) $ do
        sym <- R.reader 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 = addNat lenNat iNat
        liftIO $ withLeqProof (leqAdd2 (leqRefl lenNat) iPositive) $
          let op = if extend == "zero_extend" then W4.bvZext else W4.bvSext
          in Some <$> op sym newLen arg
  readApp (S.WFSList [S.WFSAtom (AId "_"), S.WFSAtom (AId "bvfill"), S.WFSAtom (AInt width)]) args =
    prefixError "in reading bvfill expression" $ do
      sym <- R.reader procSym
      Some arg <- readOneArg args
      case W4.exprType arg of
        BaseBoolRepr -> do
          Some widthRep <- intToNatM width
          LeqProof <- fromMaybeError "must extend by a positive length" $ isPosNat widthRep
          liftIO (Some <$> W4.bvFill sym widthRep arg)
        tyrep -> E.throwError ("Invalid argument type to bvFill: " ++ show tyrep)
  readApp rator rands = E.throwError $ ("readApp could not parse the following: "
                                        ++ (T.unpack (printSExpr mempty $ S.WFSList (rator: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 = fromMaybeError "integer must be non-negative to be a nat" . 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 idxReprs arrTyRepr updateSExprList =
    case updateSExprList of
      S.L items -> F.foldrM expectArrayUpdateEntry WAU.empty items
      _ -> E.throwError "Expected a list of array element updates in ArrayMap"
    where
      expectArrayUpdateEntry pair updateMap =
        case pair of
          S.L [S.L idxListExprs, elt] -> do
            idxs <- Ctx.traverseWithIndex (parseIndexLit idxListExprs) idxReprs
            Some x <- readExpr elt
            case testEquality arrTyRepr (W4.exprType x) of
              Just Refl -> return (WAU.insert arrTyRepr idxs x updateMap)
              Nothing -> E.throwError (concat [ "Invalid element type in ArrayMap update: expected "
                                              , show arrTyRepr
                                              , " but got "
                                              , show (W4.exprType x)])
          _ -> E.throwError "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
  lst !? idx
    | idx < 0 = Nothing
    | otherwise = go idx lst
    where
      go 0 (x:_xs) = Just x
      go i (_:xs) = go (i - 1) xs
      go _ [] = 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 exprs idx repr
    | Just (S.A atom) <- exprs !? Ctx.indexVal idx =
        case (repr, atom) of
          (BaseBVRepr w, ABV w' val)
            | PN.intValue w == toInteger w' ->
              return (WIL.BVIndexLit w (BV.mkBV w val))
            | otherwise -> E.throwError ("Array update index bitvector size mismatch: expected " ++ show w ++ " but got " ++ show w')
          (BaseIntegerRepr, AInt i) -> return (WIL.IntIndexLit i)
          _ -> E.throwError ("Unexpected array update index type: " ++ show repr)
    | otherwise = E.throwError ("Invalid or missing array update index at " ++ show 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 dimRepr (BaseArrayRepr idxTpReprs resRepr) =
    case Ctx.viewAssign idxTpReprs of
      Ctx.AssignExtend rest idxTpRepr ->
        case Ctx.viewAssign rest of
          Ctx.AssignEmpty ->
            case testEquality idxTpRepr dimRepr of
              Just Refl -> return $ ArraySingleDim resRepr
              Nothing -> E.throwError $ unwords ["Array index type", show idxTpRepr,
                                                 "does not match", show dimRepr]
          _ -> E.throwError "multidimensional arrays are not supported"
  expectArrayWithIndex _ repr = E.throwError $ unwords ["expected an array, got", show 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 tpAssns exs = do
    Some exsAsn <- return $ Ctx.fromList exs
    exsRepr <- return $ FC.fmapFC W4.exprType exsAsn
    case testEquality exsRepr tpAssns of
      Just Refl -> return exsAsn
      Nothing -> E.throwError $
        "Unexpected expression types for " ++ show exsAsn
        ++ "\nExpected: " ++ show tpAssns
        ++ "\nGot: " ++ show 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 [] body = readExpr body
  readLetExpr ((S.WFSList [S.WFSAtom (AId x), e]):rst) body = do
    v <- readExpr e
    R.local (\c -> c {procLetEnv = (HM.insert x v) $ procLetEnv c}) $
      readLetExpr rst body
  readLetExpr bindings _body = E.throwError $
    "invalid s-expression for let-bindings: " ++ (show 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 [] body = readExpr body
  readLetFnExpr ((S.WFSList [S.WFSAtom (AId f), e]):rst) body = do
    v <- readSymFn e
    R.local (\c -> c {procLetFnEnv = (HM.insert f v) $ procLetFnEnv c}) $
      readLetExpr rst body
  readLetFnExpr bindings _body = E.throwError $
    "invalid s-expression for let-bindings: " ++ (show 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 (S.WFSAtom (AInt n)) = do
    sym <- R.reader procSym
    liftIO $ (Some <$> W4.intLit sym n)
  readExpr (S.WFSAtom (ANat _)) =
    E.throwError "Bare Natural literals are no longer used"
  readExpr (S.WFSAtom (ABool b)) = do
    sym <- R.reader procSym
    liftIO $ return $ Some $ W4.backendPred sym b
  readExpr (S.WFSAtom (AFloat (Some repr) bf)) = do
    sym <- R.reader procSym
    liftIO $ (Some <$> W4.floatLit sym repr bf)
  readExpr (S.WFSAtom (AStr prefix content)) = do
    sym <- R.reader procSym
    case prefix of
      (Some W4.UnicodeRepr) -> do
        s <- liftIO $ W4.stringLit sym $ W4.UnicodeLiteral content
        return $ Some $ s
      (Some W4.Char8Repr) -> do
        s <- liftIO $ W4.stringLit sym $ W4.Char8Literal $ T.encodeUtf8 content
        return $ Some $ s
      (Some W4.Char16Repr) -> E.throwError $ "Char16 strings are not yet supported"
  readExpr (S.WFSAtom (AReal _)) = E.throwError $ "TODO: support readExpr for real literals"
  readExpr (S.WFSAtom (ABV len val)) = do
    -- This is a bitvector literal.
    sym <- R.reader 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 lenRepr) -> do
          pf <- case isPosNat lenRepr of
                  Just pf -> return pf
                  Nothing -> E.throwError "What4.Serialize.Parser.readExpr isPosNat failure"
          liftIO $ withLeqProof pf (Some <$> W4.bvLit sym lenRepr (BV.mkBV lenRepr val))
      Nothing -> E.throwError "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 name)) = do
    maybeBinding <- lookupExpr 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 binding -> return binding
      Nothing -> E.throwError $ ("Unbound variable encountered during deserialization: "
                                 ++ (T.unpack name))
  readExpr (S.WFSList ((S.WFSAtom (AId "let")):rhs)) =
    case rhs of
      [S.WFSList bindings, body] -> readLetExpr bindings body
      _ -> E.throwError "ill-formed let s-expression"
  readExpr (S.WFSList ((S.WFSAtom (AId "letfn")):rhs)) =
    case rhs of
      [S.WFSList bindings, body] -> readLetFnExpr bindings body
      _ -> E.throwError "ill-formed letfn s-expression"
  readExpr (S.WFSList []) = E.throwError "ill-formed empty s-expression"
  readExpr (S.WFSList (operator:operands)) = readApp operator 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 exprs = mapM readExpr exprs
  
  readExprsAsAssignment ::
    forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
    => [SExpr]
    -> Processor sym (Some (Ctx.Assignment (W4.SymExpr sym)))
  readExprsAsAssignment exprs = Ctx.fromList <$> readExprs exprs
  
  
  readFnType ::
    forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))
    => SExpr
    -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
  readFnType (S.WFSList ((S.WFSAtom (AId "->")):typeSExprs)) =
    case unsnoc typeSExprs of
      Nothing ->
        E.throwError $ ("invalid type signature for function: "
                        ++ (T.unpack $ printSExpr mempty (S.L typeSExprs)))
      Just (domSExps, retSExp) -> do
        dom <- mapM readBaseType domSExps
        ret <- readBaseType retSExp
        return (dom, ret)
  readFnType sexpr =
    E.throwError $ ("invalid type signature for function: "
                    ++ (T.unpack $ printSExpr mempty 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 []     = Nothing
  unsnoc (x:xs) = case unsnoc xs of
                    Nothing    -> Just ([], x)
                    Just (a,b) -> Just (x:a, b)
  
  readFnArgs ::
    forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))
    => [SExpr]
    -> Processor sym [Text]
  readFnArgs [] = return []
  readFnArgs ((S.WFSAtom (AId name)):rest) = do
    names <- (readFnArgs rest)
    return $ name:names
  readFnArgs (badArg:_) =
    E.throwError $ ("invalid function argument encountered: "
                    ++ (T.unpack $ printSExpr mempty badArg))
  
  someVarExpr ::
      forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))
    => sym
    -> Some (W4.BoundVar sym)
    -> Some (W4.SymExpr sym)
  someVarExpr sym (Some bv) = Some (W4.varExpr sym bv)
  
  
  readSymFn ::
    forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
    => SExpr
    -> Processor sym (SomeSymFn sym)
  readSymFn (S.WFSList [ S.WFSAtom (AId "definedfn")
                       , S.WFSAtom (AStr _ rawSymFnName)
                       , rawFnType
                       , S.WFSList argVarsRaw
                       , bodyRaw
                       ]) = do
    sym <- R.reader procSym
    symFnName <- case W4.userSymbol (T.unpack rawSymFnName) of
                   Left _ -> E.throwError $ ("Bad symbolic function name : "
                                             ++ (T.unpack rawSymFnName))
                   Right solverSym -> return 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 (\(name, (Some ty)) ->
                       case W4.userSymbol (T.unpack name) of
                         Left _ -> E.throwError $ "Bad arg name : " ++ (T.unpack name)
                         Right solverSym -> liftIO $ Some <$> W4.freshBoundVar sym solverSym ty)
               $ zip argNames argTys
    (Some body) <- let newBindings = HM.fromList
                                     $ zip argNames
                                     $ map (someVarExpr sym) argVars
                   in R.local
                      (\env -> 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@(S.WFSList ((S.WFSAtom (AId "definedfn")):_)) =
    E.throwError $ ("invalid `definedfn`: " ++ (T.unpack $ printSExpr mempty badSExp))
  readSymFn (S.WFSList [ S.WFSAtom (AId "uninterpfn")
                       , S.WFSAtom (AStr _ rawSymFnName)
                       , rawFnType
                       ]) = do
    sym <- R.reader procSym
    symFnName <- case W4.userSymbol (T.unpack rawSymFnName) of
                   Left _ -> E.throwError $ ("Bad symbolic function name : "
                                             ++ (T.unpack rawSymFnName))
                   Right solverSym -> return 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@(S.WFSList ((S.WFSAtom (AId "uninterpfn")):_)) =
    E.throwError $ ("invalid `uninterpfn`: " ++ (T.unpack $ printSExpr mempty badSExp))
  readSymFn sexpr = E.throwError ("invalid function definition: "
                                  ++ (T.unpack $ printSExpr mempty sexpr))
  