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

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

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

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

import qualified Data.SCargot.Repr.WellFormed as S

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


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

type SExpr = S.WellFormedSExpr Atom

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

instance Eq (SomeExprSymFn t) where
  (SomeExprSymFn fn1) == (SomeExprSymFn fn2) =
    case W4.testEquality (W4.symFnId fn1) (W4.symFnId fn2) of
      Just _ -> True
      _ -> False

instance Ord (SomeExprSymFn t) where
  compare (SomeExprSymFn fn1) (SomeExprSymFn fn2) =
    compare (Nonce.indexValue $ W4.symFnId fn1) (Nonce.indexValue $ W4.symFnId fn2)


instance Show (SomeExprSymFn t) where
  show (SomeExprSymFn f) = show f


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

ppFreeVarEnv :: VarNameEnv t -> String
ppFreeVarEnv env = show $ map toStr entries
  where entries = OMap.toAscList env
        toStr :: ((Some (W4.ExprBoundVar t)), Text) -> (String, String, String)
        toStr ((Some var), newName) = ( T.unpack $ W4.solverSymbolAsText $ W4.bvarName var
                                      , show $ W4.bvarType var
                                      , T.unpack newName
                                      )

ppFreeSymFnEnv :: FnNameEnv t -> String
ppFreeSymFnEnv env = show $ map toStr entries
  where entries = OMap.toAscList env
        toStr :: ((SomeExprSymFn t), Text) -> (String, String, String)
        toStr ((SomeExprSymFn fn), newName) = ( T.unpack $ W4.solverSymbolAsText $ W4.symFnName fn
                                              , show $ W4.symFnArgTypes fn
                                              , T.unpack newName
                                              )

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

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


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

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

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

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

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


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

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


serializeBaseType :: BaseTypeRepr tp -> SExpr
serializeBaseType bt = convertBaseType bt

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

initEnv :: forall t . Config -> MemoEnv t
initEnv cfg = MemoEnv { envConfig = cfg
                      , envIdCounter = 0
                      , envLetBindings = OMap.empty
                      , envFreeVarEnv = OMap.empty
                      , envFreeSymFnEnv = OMap.empty
                      , envBoundVars = Set.empty
                      }

type Memo t a = State (MemoEnv t) a

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


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


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

mkLet :: [SExpr] -> SExpr -> SExpr
mkLet [] body       = body
mkLet bindings body = S.L [ident "let", S.L bindings, body]


-- | Converts a What4 ExprSymFn into an s-expression within
-- the Memo monad (i.e., no @let@ or @letfn@s are emitted).
convertSymFn :: forall t args ret
              . W4.ExprSymFn t args ret
             -> Memo t SExpr
convertSymFn symFn@(W4.ExprSymFn _ symFnName symFnInfo _) = do
 case symFnInfo of
   W4.DefinedFnInfo argVars body _ -> do
     let sArgTs = convertBaseTypes (W4.fnArgTypes symFn)
         sRetT = convertBaseType (W4.fnReturnType symFn)
     argsWithFreshNames <- let rawArgs = FC.toListFC Some argVars
                           in mapM getBoundVarWithFreshName rawArgs
     let (origBoundVars, freshArgNames) = unzip argsWithFreshNames
     -- Convert the body with the bound variable set and
     -- free-variable mapping extended to reflect being
     -- under the function's binders.
     sExpr <- MS.withState (\ms -> let boundVars = envBoundVars ms
                                       fvEnv = envFreeVarEnv ms
                             in ms { envBoundVars = Set.union boundVars (Set.fromList origBoundVars)
                                   , envFreeVarEnv = fvEnv OMap.<>| (OMap.fromList argsWithFreshNames)})
              $ convertExprWithLet body
     return $ S.L [ ident "definedfn"
                  , string (Some W4.UnicodeRepr) $ W4.solverSymbolAsText symFnName
                  , S.L ((ident "->"):sArgTs ++ [sRetT])
                  , S.L $ map ident freshArgNames
                  , sExpr
                  ]
   W4.UninterpFnInfo argTs retT ->
     let sArgTs = convertBaseTypes argTs
         sRetT = convertBaseType retT
     in return $ S.L [ ident "uninterpfn"
                     , string (Some W4.UnicodeRepr) $ W4.solverSymbolAsText symFnName
                     , S.L ((ident "->"):sArgTs ++ [sRetT])
                     ]
   W4.MatlabSolverFnInfo _msfn _argTs _body ->
     error "MatlabSolverFnInfo SymFns are not yet supported"
  where
    getBoundVarWithFreshName ::
      (Some (W4.ExprBoundVar t)) ->
      Memo t (Some (W4.ExprBoundVar t), Text)
    getBoundVarWithFreshName someVar@(Some var) = do
      nm <- freshName (W4.bvarType var)
      return (someVar, nm)


-- | Key for sharing SExpr construction. Internally indexes are expression nonces,
-- but the let-binding identifiers are based on insertion order to the OMap
newtype SKey = SKey {sKeyValue :: Word64}
  deriving (Eq, Ord, Show)



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

freshFnName :: W4.ExprSymFn t args ret -> Memo t Text
freshFnName fn = do
  idCount <- MS.gets envIdCounter
  MS.modify' $ (\e -> e {envIdCounter = idCount + 1})
  let prefix = case W4.symFnInfo fn of
                 W4.UninterpFnInfo{} -> "ufn"
                 W4.DefinedFnInfo{} -> "dfn"
                 W4.MatlabSolverFnInfo{} -> "mfn"
  return $ T.pack $ prefix++(show $ idCount)



exprSKey :: W4.Expr t tp -> Maybe SKey
exprSKey x = SKey . Nonce.indexValue <$> W4.exprMaybeId x

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

-- | Converts a What 4 expression into an s-expression
-- within the Memo monad (i.e., no @let@ or @letfn@s are
-- emitted in the result).
convertExpr :: forall t tp . W4.Expr t tp -> Memo t SExpr
convertExpr initialExpr = do
  case exprSKey initialExpr of
    Nothing -> go initialExpr
    Just key -> do
      letCache <- MS.gets envLetBindings
      case OMap.lookup key letCache of
        Just (name, _) -> return $ ident name
        Nothing -> do
          sexp <- go initialExpr
          case sexp of
            S.A _ -> return sexp -- Don't memoize atomic s-expressions - that's just silly.
            _ -> do
              letVarName <- addLetBinding key sexp (W4.exprType initialExpr)
              return $ ident letVarName
  where go :: W4.Expr t tp -> Memo t SExpr
        go (W4.SemiRingLiteral W4.SemiRingIntegerRepr val _) = return $ int val -- do we need/want these?
        go (W4.SemiRingLiteral W4.SemiRingRealRepr val _) = return $ real val
        go (W4.SemiRingLiteral (W4.SemiRingBVRepr _ sz) val _) = return $ bitvec (natValue sz) (BV.asUnsigned val)
        go (W4.StringExpr str _) =
          case (W4.stringLiteralInfo str) of
            W4.UnicodeRepr -> return $ string (Some W4.UnicodeRepr) (W4S.fromUnicodeLit str)
            W4.Char8Repr -> return $ string (Some W4.Char8Repr) $ T.decodeUtf8 $ W4S.fromChar8Lit str
            W4.Char16Repr -> error "Char16 strings are not yet supported"
              -- TODO - there is no `W4S.toLEByteString` currently... hmm...
              -- return $ string (Some W4.Char16Repr) $ T.decodeUtf16LE $ W4S.toLEByteString $ W4S.fromChar16Lit str
        go (W4.FloatExpr prec bf _) = return $ float prec bf
        go (W4.BoolExpr b _) = return $ bool b
        go (W4.AppExpr appExpr) = convertAppExpr' appExpr
        go (W4.NonceAppExpr nae) =
          case W4.nonceExprApp nae of
            W4.FnApp fn args -> convertFnApp fn args
            W4.Forall {} -> error "Forall NonceAppExpr not yet supported"
            W4.Exists {} -> error "Exists NonceAppExpr not yet supported"
            W4.ArrayFromFn {} -> error "ArrayFromFn NonceAppExpr not yet supported"
            W4.MapOverArrays {} -> error "MapOverArrays NonceAppExpr not yet supported"
            W4.ArrayTrueOnEntries {} -> error "ArrayTrueOnEntries NonceAppExpr not yet supported"
            W4.Annotation {} -> error "Annotation NonceAppExpr not yet supported"
        go (W4.BoundVarExpr var) = convertBoundVarExpr var

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


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

        -- Note that because the SemiRing has an identity element that
        -- always gets applied, resulting in lots of additional,
        -- unnecessary elements like: "(bvand #xffffffff TERM)".
        -- These will get manifested in the stored form (but generally
        -- _not_ via DSL-generated versions since they don't output
        -- via Printer) and result in longer stored forms.  They could
        -- be eliminated by checking for the identity (e.g. "if mul ==
        -- SR.one (WSum.sumRepr sm)") but the re-loaded representation
        -- will still use the SemiRing, so it's probably not worth the
        -- effort to reduce these.
        go (W4.SemiRingSum sm) =
          case WSum.sumRepr sm of
            W4.SemiRingBVRepr W4.BVArithRepr w ->
              let smul mul e = do
                    s <- goE e
                    return $ S.L [ ident "bvmul", bitvec (natValue w) (BV.asUnsigned mul), s]
                  sval v = return $ bitvec (natValue w) (BV.asUnsigned v)
                  add x y = return $ S.L [ ident "bvadd", x, y ]
              in WSum.evalM add smul sval sm
            W4.SemiRingBVRepr W4.BVBitsRepr w ->
              let smul mul e = do
                    s <- goE e
                    return $ S.L [ ident "bvand", bitvec (natValue w) (BV.asUnsigned mul), s]
                  sval v = return $ bitvec (natValue w) (BV.asUnsigned v)
                  add x y = let op = ident "bvxor" in return $ S.L [ op, x, y ]
              in WSum.evalM add smul sval sm
            W4.SemiRingIntegerRepr ->
              let smul mul e = do
                    s <- goE e
                    return $ S.L [ ident "intmul", int mul, s]
                  sval v = return $ int v
                  add x y = return $ S.L [ ident "intadd", x, y ]
              in WSum.evalM add smul sval sm
            W4.SemiRingRealRepr    -> error "SemiRingSum RealRepr not supported"

        go (W4.SemiRingProd pd) =
          case WSum.prodRepr pd of
            W4.SemiRingBVRepr W4.BVArithRepr w -> do
              let pmul x y = return $ S.L [ ident "bvmul", x, y ]
              maybeS <- WSum.prodEvalM pmul goE pd
              case maybeS of
                Just s -> return s
                Nothing -> return $ bitvec (natValue w) 1
            W4.SemiRingBVRepr W4.BVBitsRepr w -> do
              let pmul x y = return $ S.L [ ident "bvand", x, y ]
              maybeS <- WSum.prodEvalM pmul goE pd
              case maybeS of
                Just s -> return s
                Nothing -> return $ bitvec (natValue w) 1
            W4.SemiRingIntegerRepr -> do
              let pmul x y = return $ S.L [ ident "intmul", x, y ]
              maybeS <- WSum.prodEvalM pmul goE pd
              case maybeS of
                Just s -> return s
                Nothing -> return $ int 1
            W4.SemiRingRealRepr    -> error "convertApp W4.SemiRingProd Real unsupported"

        go (W4.SemiRingLe sr e1 e2) = do
          s1 <- goE e1
          s2 <- goE e2
          case sr of
            W4.OrderedSemiRingIntegerRepr -> do
              return $ S.L [ ident "intle", s1, s2]
            W4.OrderedSemiRingRealRepr -> error $ "Printer: SemiRingLe is not supported for reals"

        go (W4.BVOrBits width bs) = do
          let op = ident "bvor"
          case W4.bvOrToList bs of
            [] -> return $ bitvec (NR.natValue width) 0
            (x:xs) -> do
              e <- goE x
              let f = (\acc b -> do
                          b' <- goE b
                          return $ S.L [op, b', acc])
              M.foldM f e xs
        go (W4.BVUdiv _ e1 e2) = do
          s1 <- goE e1
          s2 <- goE e2
          return $ S.L [ident "bvudiv", s1, s2]
        go (W4.BVUrem _ e1 e2) = do
          s1 <- goE e1
          s2 <- goE e2
          return $ S.L [ident "bvurem", s1, s2]
        go (W4.BVSdiv _ e1 e2) = do
          s1 <- goE e1
          s2 <- goE e2
          return $ S.L [ident "bvsdiv", s1, s2]
        go (W4.BVSrem _ e1 e2) = do
          s1 <- goE e1
          s2 <- goE e2
          return $ S.L [ident "bvsrem", s1, s2]
        go (W4.BVShl _ e1 e2) = do
          s1 <- goE e1
          s2 <- goE e2
          return $ S.L [ident "bvshl", s1, s2]
        go (W4.BVLshr _ e1 e2) = do
          s1 <- goE e1
          s2 <- goE e2
          return $ S.L [ident "bvlshr", s1, s2]
        go (W4.BVAshr _ e1 e2) = do
          s1 <- goE e1
          s2 <- goE e2
          return $ S.L [ident "bvashr", s1, s2]
        go (W4.BVZext r e) = extend "zero" (intValue r) e
        go (W4.BVSext r e) = extend "sign" (intValue r) e
        go (W4.BVFill r e) = do
          s <- goE e
          return $ S.L [ S.L [ident "_", ident "bvfill", int (intValue r)]
                       , s
                       ]

        go (W4.BVToInteger e) = do
          s <- goE e
          return $ S.L [ident "bvToInteger", s]

        go (W4.SBVToInteger e) = do
          s <- goE e
          return $ S.L [ident "sbvToInteger", s]

        go (W4.FloatNeg _repr e) = do
          s <- goE e
          return $ S.L [ident "floatneg", s]
        go (W4.FloatAbs _repr e) = do
          s <- goE e
          return $ S.L [ident "floatabs", s]

        go (W4.IntDiv e1 e2) = do
          s1 <- goE e1
          s2 <- goE e2
          return $ S.L [ident "intdiv", s1, s2]
        go (W4.IntMod e1 e2) = do
          s1 <- goE e1
          s2 <- goE e2
          return $ S.L [ident "intmod", s1, s2]
        go (W4.IntAbs e1) = do
          s1 <- goE e1
          return $ S.L [ident "intabs", s1]
        go (W4.IntegerToBV e wRepr)  = do
          s <- goE e
          return $ S.L [ident "integerToBV"
                        , nat $ natValue wRepr
                        , s]

        go (W4.StructCtor _tps es) = do
          ss <- convertExprAssignment es
          return $ S.L [ident "struct", S.L ss]
        go (W4.StructField e ix _fieldTp) = do
          s <- goE e
          return $ S.L [ident "field"
                        , s
                        , int $ toInteger $ Ctx.indexVal ix
                        ]

        go (W4.UpdateArray _ _ e1 es e2) = do
          s1 <- goE e1
          ss <- convertExprAssignment es
          s2 <- goE e2
          case ss of
            [idx] -> return $ S.L [ ident "updateArray", s1, idx, s2]
            _ -> error $ "multidimensional arrays not supported"
        go (W4.SelectArray _ e es) = do
          s <- goE e
          ss <- convertExprAssignment es
          case ss of
            [idx] -> return $ S.L [ ident "select", s, idx]
            _ -> error $ "multidimensional arrays not supported"

        go (W4.ArrayMap _idxReprs _resRepr updateMap arr) = do
          updates <- mapM convertArrayUpdate (WAU.toList updateMap)
          arr' <- goE arr
          return $ S.L [ ident "arrayMap"
                       , S.L updates
                       , arr'
                       ]

        go app = error $ "unhandled App: " ++ show app

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

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

        goE :: forall tp' . W4.Expr t tp' -> Memo t SExpr
        goE = convertExpr

        extend :: forall w. Text -> Integer -> W4.Expr t (BaseBVType w) -> Memo t SExpr
        extend op r e = do
          let w = case W4.exprType e of BaseBVRepr len -> intValue len
              extension = r - w
          s <- goE e
          return $ S.L [ S.L [ ident "_", ident $ op <> "_extend", int extension ]
                        , s
                        ]

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

        convertBoolMap :: Text -> Bool -> BooM.BoolMap (W4.Expr t) -> Memo t SExpr
        convertBoolMap op base bm =
          let strBase b = if b
                          then S.L [ident "=", bitvec 1 0, bitvec 1 0]  -- true
                          else S.L [ident "=", bitvec 1 0, bitvec 1 1]  -- false
              strNotBase = strBase . not
          in case BooM.viewBoolMap bm of
               BooM.BoolMapUnit -> return $ strBase base
               BooM.BoolMapDualUnit -> return $ strNotBase base
               BooM.BoolMapTerms ts ->
                 let onEach e r = do
                       s <- arg e
                       return $ S.L [ident op, s, r]
                     arg (t, BooM.Positive) = goE t
                     arg (t, BooM.Negative) = do
                       s <- goE t
                       return $ S.L [ident "notp", s]
                 in F.foldrM onEach (strBase base) ts

convertIndexLit :: WIL.IndexLit tp -> SExpr
convertIndexLit il =
  case il of
    WIL.IntIndexLit iidx -> int iidx
    WIL.BVIndexLit irep bvidx -> bitvec (natValue irep) (BV.asUnsigned bvidx)

convertExprAssignment ::
  Ctx.Assignment (W4.Expr t) sh
  -> Memo t [SExpr]
convertExprAssignment es =
  mapM (\(Some e) -> convertExpr e) (FC.toListFC Some es)

convertFnApp ::
  W4.ExprSymFn t args ret
  -> Ctx.Assignment (W4.Expr t) args
  -> Memo t SExpr
convertFnApp fn args = do
  argSExprs <- convertExprAssignment args
  fnEnv <- MS.gets envFreeSymFnEnv
  case OMap.lookup (SomeExprSymFn fn) fnEnv of
    Just fnName ->
      return $ S.L $ (ident "call"):(ident fnName):argSExprs
    Nothing -> do
      varName <- freshFnName fn
      MS.modify' $ (\e -> e {envFreeSymFnEnv =  fnEnv OMap.|> ((SomeExprSymFn fn), varName)})
      return $ S.L $ (ident "call"):(ident varName):argSExprs


convertBaseType :: BaseTypeRepr tp -> SExpr
convertBaseType tp = case tp of
  W4.BaseBoolRepr -> S.A $ AId "Bool"
  W4.BaseIntegerRepr -> S.A $ AId "Int"
  W4.BaseRealRepr -> S.A $ AId "Real"
  W4.BaseStringRepr si -> S.L [S.A $ AId "String", convertStringInfo si]
  W4.BaseComplexRepr -> S.A $ AId "Complex"
  W4.BaseBVRepr wRepr -> S.L [S.A (AId "BV"), S.A (AInt (NR.intValue wRepr)) ]
  W4.BaseStructRepr tps -> S.L [ S.A (AId "Struct"), S.L (convertBaseTypes tps) ]
  W4.BaseArrayRepr ixs repr -> S.L [S.A (AId "Array"), S.L $ convertBaseTypes ixs , convertBaseType repr]
  W4.BaseFloatRepr (W4.FloatingPointPrecisionRepr eRepr sRepr) ->
    S.L [ S.A (AId "Float"), S.A (AInt (NR.intValue eRepr)), S.A (AInt (NR.intValue sRepr)) ]



convertStringInfo :: StringInfoRepr si -> SExpr
convertStringInfo W4.Char8Repr = ident "Char8"
convertStringInfo W4.Char16Repr = ident "Char16"
convertStringInfo W4.UnicodeRepr = ident "Unicode"

-- | Convert an Assignment of base types into a list of base
-- types SExpr, where the left-to-right syntactic ordering
-- of the types is maintained.
convertBaseTypes ::
  Ctx.Assignment BaseTypeRepr tps
  -> [SExpr]
convertBaseTypes asn = FC.toListFC convertBaseType asn