    {-
    Module           : What4.Protocol.VerilogWriter.Backend
    Copyright        : (c) Galois, Inc 2020
    Maintainer       : Jennifer Paykin <jpaykin@galois.com>
    License          : BSD3

    Convert What4 expressions into the data types defined in the @What4.Protocol.VerilogWriter.AST@ module.
    -}
    {-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, ScopedTypeVariables, RankNTypes,
      TypeApplications, PolyKinds, DataKinds, ExplicitNamespaces, TypeOperators,
      LambdaCase, FlexibleContexts, LambdaCase, OverloadedStrings #-}

    module What4.Protocol.VerilogWriter.Backend
      ( exprToVerilogExpr
      )
      where

    import           Control.Monad (foldM)
    import           Control.Monad.State (get)
    import           Control.Monad.Except (MonadError(..))
    import qualified Data.BitVector.Sized as BV
    import           Data.List.NonEmpty ( NonEmpty(..) )

    import           Data.Parameterized.Context
    import           Data.Parameterized.Some (Some(..))
    import           GHC.TypeNats

    import qualified What4.Expr.BoolMap as BMap
    import           What4.BaseTypes as WT
    import           What4.Expr.Builder
    import           What4.Interface
    import qualified What4.SemiRing as SR
    import           What4.Symbol
    import qualified What4.Expr.WeightedSum as WS
    import qualified What4.Expr.UnaryBV as UBV

    import What4.Protocol.VerilogWriter.AST

    doNotSupportError :: MonadError String m => String -> m a
    doNotSupportError :: forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    cstr = String -> m a
    forall a. String -> m a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    throwError (String -> m a) -> String -> m a
    forall a b. (a -> b) -> a -> b
    $ String
    doNotSupportMsg String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cstr

    doNotSupportMsg :: String
    doNotSupportMsg :: String
    doNotSupportMsg = String
    "the Verilog backend to What4 does not support "

    -- | Convert a What4 expresssion into a Verilog expression and return a
    -- name for that expression's result.
    exprToVerilogExpr ::
      (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
      Expr n tp ->
      VerilogM sym n (IExp tp)
    exprToVerilogExpr :: forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n tp
    e = do
      cache <- ModuleState sym n -> IdxCache n IExp
    forall sym n. ModuleState sym n -> IdxCache n IExp
    vsExpCache (ModuleState sym n -> IdxCache n IExp)
    -> VerilogM sym n (ModuleState sym n)
    -> VerilogM sym n (IdxCache n IExp)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> VerilogM sym n (ModuleState sym n)
    forall s (m :: Type -> Type). MonadState s m => m s
    get
      let cacheEval Expr n tp -> VerilogM sym n (IExp tp)
    go = IdxCache n IExp
    -> Expr n tp
    -> VerilogM sym n (IExp tp)
    -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) t (f :: BaseType -> Type)
           (tp :: BaseType).
    MonadIO m =>
    IdxCache t f -> Expr t tp -> m (f tp) -> m (f tp)
    idxCacheEval IdxCache n IExp
    cache Expr n tp
    e (Expr n tp -> VerilogM sym n (IExp tp)
    go Expr n tp
    e)
      cacheEval $
        \case
          SemiRingLiteral (SR.SemiRingBVRepr BVFlavorRepr fv
    _ NatRepr w
    w) Coefficient sr
    i ProgramLoc
    _ ->
            NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
    forall (w :: Natural) sym n.
    (1 <= w) =>
    NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
    litBV NatRepr w
    w BV w
    Coefficient sr
    i
          SemiRingLiteral SemiRingRepr sr
    _ Coefficient sr
    _ ProgramLoc
    _ ->
            String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "non-bit-vector literals"
          BoolExpr Bool
    b ProgramLoc
    _   -> Bool -> VerilogM sym n (IExp 'BaseBoolType)
    forall sym n. Bool -> VerilogM sym n (IExp 'BaseBoolType)
    litBool Bool
    b
          StringExpr StringLiteral si
    _ ProgramLoc
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "strings"
          FloatExpr{} -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floating-point values"
          AppExpr AppExpr n tp
    app -> AppExpr n tp -> VerilogM sym n (IExp tp)
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    AppExpr n tp -> VerilogM sym n (IExp tp)
    appExprVerilogExpr AppExpr n tp
    app
          NonceAppExpr NonceAppExpr n tp
    n -> NonceAppExpr n tp -> VerilogM sym n (IExp tp)
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    NonceAppExpr n tp -> VerilogM sym n (IExp tp)
    nonceAppExprVerilogExpr NonceAppExpr n tp
    n
          BoundVarExpr ExprBoundVar n tp
    x ->
            do name <- ExprBoundVar n tp -> Identifier -> VerilogM sym n Identifier
    forall n (tp :: BaseType) sym.
    ExprBoundVar n tp -> Identifier -> VerilogM sym n Identifier
    addBoundInput ExprBoundVar n tp
    x (ExprBoundVar n tp -> Identifier
    forall t (tp :: BaseType). ExprBoundVar t tp -> Identifier
    bvarIdentifier ExprBoundVar n tp
    x)
               return $ Ident (bvarType x) name

    bvarIdentifier :: ExprBoundVar t tp -> Identifier
    bvarIdentifier :: forall t (tp :: BaseType). ExprBoundVar t tp -> Identifier
    bvarIdentifier = SolverSymbol -> Identifier
    solverSymbolAsText (SolverSymbol -> Identifier)
    -> (ExprBoundVar t tp -> SolverSymbol)
    -> ExprBoundVar t tp
    -> Identifier
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExprBoundVar t tp -> SolverSymbol
    forall t (tp :: BaseType). ExprBoundVar t tp -> SolverSymbol
    bvarName

    nonceAppExprVerilogExpr ::
      (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
      NonceAppExpr n tp ->
      VerilogM sym n (IExp tp)
    nonceAppExprVerilogExpr :: forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    NonceAppExpr n tp -> VerilogM sym n (IExp tp)
    nonceAppExprVerilogExpr NonceAppExpr n tp
    nae =
      case NonceAppExpr n tp -> NonceApp n (Expr n) tp
    forall t (tp :: BaseType).
    NonceAppExpr t tp -> NonceApp t (Expr t) tp
    nonceExprApp NonceAppExpr n tp
    nae of
        Forall ExprBoundVar n tp1
    _ Expr n 'BaseBoolType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "universal quantification"
        Exists ExprBoundVar n tp1
    _ Expr n 'BaseBoolType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "existential quantification"
        ArrayFromFn ExprSymFn n (idx ::> itp) ret
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "arrays"
        MapOverArrays ExprSymFn n (ctx ::> d) r
    _ Assignment BaseTypeRepr (idx ::> itp)
    _ Assignment (ArrayResultWrapper (Expr n) (idx ::> itp)) (ctx ::> d)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "arrays"
        ArrayTrueOnEntries ExprSymFn n (idx ::> itp) 'BaseBoolType
    _ Expr n (BaseArrayType (idx ::> itp) 'BaseBoolType)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "arrays"
        FnApp ExprSymFn n args tp
    f Assignment (Expr n) args
    Empty -> do
          name <- Some (Nonce n)
    -> Some BaseTypeRepr -> Identifier -> VerilogM sym n Identifier
    forall {k} n sym.
    Some (Nonce n)
    -> Some BaseTypeRepr -> Identifier -> VerilogM sym n Identifier
    addFreshInput (Nonce n (args ::> tp) -> Some (Nonce n)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some Nonce n (args ::> tp)
    idx) (BaseTypeRepr tp -> Some BaseTypeRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some BaseTypeRepr tp
    tp) Identifier
    base
          return $ Ident tp name
            where
              tp :: BaseTypeRepr tp
    tp = ExprSymFn n args tp -> BaseTypeRepr tp
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> BaseTypeRepr ret
    symFnReturnType ExprSymFn n args tp
    f
              idx :: Nonce n (args ::> tp)
    idx = ExprSymFn n args tp -> Nonce n (args ::> tp)
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> Nonce t (args ::> ret)
    symFnId ExprSymFn n args tp
    f
              base :: Identifier
    base = SolverSymbol -> Identifier
    solverSymbolAsText (ExprSymFn n args tp -> SolverSymbol
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> SolverSymbol
    symFnName ExprSymFn n args tp
    f)
        -- TODO: inline defined functions?
        -- TODO: implement uninterpreted functions as uninterpreted functions
        FnApp ExprSymFn n args tp
    _ Assignment (Expr n) args
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "named function applications"
        Annotation BaseTypeRepr tp
    _ Nonce n tp
    _ Expr n tp
    e -> Expr n tp -> VerilogM sym n (IExp tp)
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n tp
    e

    boolMapToExpr ::
      (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
      Bool ->
      Bool ->
      Binop WT.BaseBoolType WT.BaseBoolType ->
      BMap.BoolMap (Expr n) ->
      VerilogM sym n (IExp WT.BaseBoolType)
    boolMapToExpr :: forall sym n.
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Bool
    -> Bool
    -> Binop 'BaseBoolType 'BaseBoolType
    -> BoolMap (Expr n)
    -> VerilogM sym n (IExp 'BaseBoolType)
    boolMapToExpr Bool
    u Bool
    du Binop 'BaseBoolType 'BaseBoolType
    op BoolMap (Expr n)
    es =
      let pol :: (Expr n 'BaseBoolType, Polarity)
    -> VerilogM sym n (IExp 'BaseBoolType)
    pol (Expr n 'BaseBoolType
    x,Polarity
    Positive) = Expr n 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType)
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n 'BaseBoolType
    x
          pol (Expr n 'BaseBoolType
    x,Polarity
    Negative) = Unop 'BaseBoolType
    -> IExp 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType)
    forall (tp :: BaseType) sym n.
    Unop tp -> IExp tp -> VerilogM sym n (IExp tp)
    unop Unop 'BaseBoolType
    Not (IExp 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType))
    -> VerilogM sym n (IExp 'BaseBoolType)
    -> VerilogM sym n (IExp 'BaseBoolType)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr n 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType)
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n 'BaseBoolType
    x
      in
      case BoolMap (Expr n) -> BoolMapView (Expr n)
    forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
    BMap.viewBoolMap BoolMap (Expr n)
    es of
        BoolMapView (Expr n)
    BMap.BoolMapUnit -> Bool -> VerilogM sym n (IExp 'BaseBoolType)
    forall sym n. Bool -> VerilogM sym n (IExp 'BaseBoolType)
    litBool Bool
    u
        BoolMapView (Expr n)
    BMap.BoolMapDualUnit -> Bool -> VerilogM sym n (IExp 'BaseBoolType)
    forall sym n. Bool -> VerilogM sym n (IExp 'BaseBoolType)
    litBool Bool
    du
        BMap.BoolMapTerms ((Expr n 'BaseBoolType, Polarity)
    t:|[]) -> (Expr n 'BaseBoolType, Polarity)
    -> VerilogM sym n (IExp 'BaseBoolType)
    forall {sym} {n}.
    (SymExpr sym ~ Expr n, IsExprBuilder sym) =>
    (Expr n 'BaseBoolType, Polarity)
    -> VerilogM sym n (IExp 'BaseBoolType)
    pol (Expr n 'BaseBoolType, Polarity)
    t
        BMap.BoolMapTerms ((Expr n 'BaseBoolType, Polarity)
    t:|[(Expr n 'BaseBoolType, Polarity)]
    ts) -> do
          t' <- (Expr n 'BaseBoolType, Polarity)
    -> VerilogM sym n (IExp 'BaseBoolType)
    forall {sym} {n}.
    (SymExpr sym ~ Expr n, IsExprBuilder sym) =>
    (Expr n 'BaseBoolType, Polarity)
    -> VerilogM sym n (IExp 'BaseBoolType)
    pol (Expr n 'BaseBoolType, Polarity)
    t
          ts' <- mapM pol ts
          foldM (binop op) t' ts'

    leqSubPos :: (1 <= m, 1 <= n, n+1 <= m) => NatRepr m -> NatRepr n -> LeqProof 1 (m - n)
    leqSubPos :: forall (m :: Natural) (n :: Natural).
    (1 <= m, 1 <= n, (n + 1) <= m) =>
    NatRepr m -> NatRepr n -> LeqProof 1 (m - n)
    leqSubPos NatRepr m
    mr NatRepr n
    nr =
      case (NatRepr n -> NatRepr 1 -> (n + 1) :~: (1 + n)
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> (m + n) :~: (n + m)
    plusComm NatRepr n
    nr NatRepr 1
    one, NatRepr 1 -> NatRepr n -> ((1 + n) - n) :~: 1
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> ((m + n) - n) :~: m
    plusMinusCancel NatRepr 1
    one NatRepr n
    nr) of
        ((n + 1) :~: (1 + n)
    Refl, ((n + 1) - n) :~: 1
    ((1 + n) - n) :~: 1
    Refl) ->
          LeqProof (n + 1) m
    -> LeqProof n n -> LeqProof ((n + 1) - n) (m - n)
    forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
           (y_h :: Natural).
    LeqProof x_l x_h
    -> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
    leqSub2 (NatRepr (n + 1) -> NatRepr m -> LeqProof (n + 1) m
    forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
           (g :: Natural -> Type).
    (m <= n) =>
    f m -> g n -> LeqProof m n
    leqProof (NatRepr n
    nr NatRepr n -> NatRepr 1 -> NatRepr (n + 1)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    `addNat` NatRepr 1
    one) NatRepr m
    mr) (NatRepr n -> NatRepr n -> LeqProof n n
    forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
           (g :: Natural -> Type).
    (m <= n) =>
    f m -> g n -> LeqProof m n
    leqProof NatRepr n
    nr NatRepr n
    nr)
      where one :: NatRepr 1
    one = NatRepr 1
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat :: NatRepr 1

    leqSuccLeft :: (n + 1 <= m) => p m -> NatRepr n -> LeqProof n m
    leqSuccLeft :: forall (n :: Natural) (m :: Natural) (p :: Natural -> Type).
    ((n + 1) <= m) =>
    p m -> NatRepr n -> LeqProof n m
    leqSuccLeft p m
    mr NatRepr n
    nr =
      case (NatRepr n -> NatRepr 1 -> (n + 1) :~: (1 + n)
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> (m + n) :~: (n + m)
    plusComm NatRepr n
    nr NatRepr 1
    one, NatRepr n -> NatRepr 1 -> LeqProof 1 (n + 1)
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    f m -> g n -> LeqProof n (m + n)
    addPrefixIsLeq NatRepr n
    nr NatRepr 1
    one) of
        ((n + 1) :~: (1 + n)
    Refl, LeqProof 1 (n + 1)
    LeqProof) ->
          LeqProof n (n + 1) -> LeqProof (n + 1) m -> LeqProof n m
    forall (m :: Natural) (n :: Natural) (p :: Natural).
    LeqProof m n -> LeqProof n p -> LeqProof m p
    leqTrans (NatRepr n -> NatRepr 1 -> LeqProof n (n + 1)
    forall (f :: Natural -> Type) (n :: Natural) (g :: Natural -> Type)
           (m :: Natural).
    f n -> g m -> LeqProof n (n + m)
    addIsLeq NatRepr n
    nr NatRepr 1
    one) (NatRepr (n + 1) -> p m -> LeqProof (n + 1) m
    forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
           (g :: Natural -> Type).
    (m <= n) =>
    f m -> g n -> LeqProof m n
    leqProof (NatRepr n
    nr NatRepr n -> NatRepr 1 -> NatRepr (n + 1)
    forall (m :: Natural) (n :: Natural).
    NatRepr m -> NatRepr n -> NatRepr (m + n)
    `addNat` NatRepr 1
    one) p m
    mr)
      where one :: NatRepr 1
    one = NatRepr 1
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat :: NatRepr 1

    appExprVerilogExpr ::
      (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
      AppExpr n tp ->
      VerilogM sym n (IExp tp)
    appExprVerilogExpr :: forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    AppExpr n tp -> VerilogM sym n (IExp tp)
    appExprVerilogExpr = App (Expr n) tp -> VerilogM sym n (IExp tp)
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    App (Expr n) tp -> VerilogM sym n (IExp tp)
    appVerilogExpr (App (Expr n) tp -> VerilogM sym n (IExp tp))
    -> (AppExpr n tp -> App (Expr n) tp)
    -> AppExpr n tp
    -> VerilogM sym n (IExp tp)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AppExpr n tp -> App (Expr n) tp
    forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
    appExprApp

    appVerilogExpr ::
      (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
      App (Expr n) tp ->
      VerilogM sym n (IExp tp)
    appVerilogExpr :: forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    App (Expr n) tp -> VerilogM sym n (IExp tp)
    appVerilogExpr App (Expr n) tp
    app =
      case App (Expr n) tp
    app of
        -- Generic operations
        BaseIte BaseTypeRepr tp
    _ Integer
    _ Expr n 'BaseBoolType
    b Expr n tp
    etrue Expr n tp
    efalse -> do
          b' <- Expr n 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType)
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n 'BaseBoolType
    b
          etrue' <- exprToVerilogExpr etrue
          efalse' <- exprToVerilogExpr efalse
          mux b' etrue' efalse'
        BaseEq BaseTypeRepr tp1
    _ Expr n tp1
    e1 Expr n tp1
    e2 -> do
          e1' <- Expr n tp1 -> VerilogM sym n (IExp tp1)
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n tp1
    e1
          e2' <- exprToVerilogExpr e2
          binop Eq e1' e2'

        -- Boolean operations
        NotPred Expr n 'BaseBoolType
    e -> do
          e' <- Expr n 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType)
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n 'BaseBoolType
    e
          unop Not e'
        --DisjPred es -> boolMapToExpr False True Or es
        ConjPred BoolMap (Expr n)
    es -> Bool
    -> Bool
    -> Binop 'BaseBoolType 'BaseBoolType
    -> BoolMap (Expr n)
    -> VerilogM sym n (IExp 'BaseBoolType)
    forall sym n.
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Bool
    -> Bool
    -> Binop 'BaseBoolType 'BaseBoolType
    -> BoolMap (Expr n)
    -> VerilogM sym n (IExp 'BaseBoolType)
    boolMapToExpr Bool
    True Bool
    False Binop 'BaseBoolType 'BaseBoolType
    And BoolMap (Expr n)
    es

        -- Semiring operations
        -- We only support bitvector semiring operations
        SemiRingSum WeightedSum (Expr n) sr
    s
          | SR.SemiRingBVRepr BVFlavorRepr fv
    SR.BVArithRepr NatRepr w
    w <- WeightedSum (Expr n) sr -> SemiRingRepr sr
    forall (f :: BaseType -> Type) (sr :: SemiRing).
    WeightedSum f sr -> SemiRingRepr sr
    WS.sumRepr WeightedSum (Expr n) sr
    s -> do
            let scalMult' :: BV w
    -> Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    scalMult' BV w
    c Expr n (BaseBVType w)
    e = NatRepr w
    -> Binop (BaseBVType w) (BaseBVType w)
    -> BV w
    -> IExp (BaseBVType w)
    -> VerilogM sym n (IExp (BaseBVType w))
    forall (w :: Natural) sym n.
    (1 <= w) =>
    NatRepr w
    -> Binop (BaseBVType w) (BaseBVType w)
    -> BV w
    -> IExp (BaseBVType w)
    -> VerilogM sym n (IExp (BaseBVType w))
    scalMult NatRepr w
    w Binop (BaseBVType w) (BaseBVType w)
    forall (w :: Natural). Binop ('BaseBVType w) ('BaseBVType w)
    BVMul BV w
    c (IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w)))
    -> VerilogM sym n (IExp (BaseBVType w))
    -> VerilogM sym n (IExp (BaseBVType w))
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n (BaseBVType w)
    e
            (IExp tp -> IExp tp -> VerilogM sym n (IExp tp))
    -> (Coefficient sr
        -> Expr n (SemiRingBase sr) -> VerilogM sym n (IExp tp))
    -> (Coefficient sr -> VerilogM sym n (IExp tp))
    -> WeightedSum (Expr n) sr
    -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) r (sr :: SemiRing)
           (f :: BaseType -> Type).
    Monad m =>
    (r -> r -> m r)
    -> (Coefficient sr -> f (SemiRingBase sr) -> m r)
    -> (Coefficient sr -> m r)
    -> WeightedSum f sr
    -> m r
    WS.evalM (Binop tp tp -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
    forall (inTp :: BaseType) (outTp :: BaseType) sym n.
    Binop inTp outTp
    -> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
    binop Binop tp tp
    Binop (BaseBVType w) (BaseBVType w)
    forall (w :: Natural). Binop ('BaseBVType w) ('BaseBVType w)
    BVAdd) BV w
    -> Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    Coefficient sr
    -> Expr n (SemiRingBase sr) -> VerilogM sym n (IExp tp)
    scalMult' (NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
    forall (w :: Natural) sym n.
    (1 <= w) =>
    NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
    litBV NatRepr w
    w) WeightedSum (Expr n) sr
    s
          | SR.SemiRingBVRepr BVFlavorRepr fv
    SR.BVBitsRepr NatRepr w
    w <- WeightedSum (Expr n) sr -> SemiRingRepr sr
    forall (f :: BaseType -> Type) (sr :: SemiRing).
    WeightedSum f sr -> SemiRingRepr sr
    WS.sumRepr WeightedSum (Expr n) sr
    s ->
            let scalMult' :: BV w
    -> Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    scalMult' BV w
    c Expr n (BaseBVType w)
    e = NatRepr w
    -> Binop (BaseBVType w) (BaseBVType w)
    -> BV w
    -> IExp (BaseBVType w)
    -> VerilogM sym n (IExp (BaseBVType w))
    forall (w :: Natural) sym n.
    (1 <= w) =>
    NatRepr w
    -> Binop (BaseBVType w) (BaseBVType w)
    -> BV w
    -> IExp (BaseBVType w)
    -> VerilogM sym n (IExp (BaseBVType w))
    scalMult NatRepr w
    w Binop (BaseBVType w) (BaseBVType w)
    forall (w :: Natural). Binop ('BaseBVType w) ('BaseBVType w)
    BVAnd BV w
    c (IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w)))
    -> VerilogM sym n (IExp (BaseBVType w))
    -> VerilogM sym n (IExp (BaseBVType w))
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n (BaseBVType w)
    e in
            (IExp tp -> IExp tp -> VerilogM sym n (IExp tp))
    -> (Coefficient sr
        -> Expr n (SemiRingBase sr) -> VerilogM sym n (IExp tp))
    -> (Coefficient sr -> VerilogM sym n (IExp tp))
    -> WeightedSum (Expr n) sr
    -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) r (sr :: SemiRing)
           (f :: BaseType -> Type).
    Monad m =>
    (r -> r -> m r)
    -> (Coefficient sr -> f (SemiRingBase sr) -> m r)
    -> (Coefficient sr -> m r)
    -> WeightedSum f sr
    -> m r
    WS.evalM (Binop tp tp -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
    forall (inTp :: BaseType) (outTp :: BaseType) sym n.
    Binop inTp outTp
    -> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
    binop Binop tp tp
    Binop (BaseBVType w) (BaseBVType w)
    forall (w :: Natural). Binop ('BaseBVType w) ('BaseBVType w)
    BVXor) BV w
    -> Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    Coefficient sr
    -> Expr n (SemiRingBase sr) -> VerilogM sym n (IExp tp)
    scalMult' (NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
    forall (w :: Natural) sym n.
    (1 <= w) =>
    NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
    litBV NatRepr w
    w) WeightedSum (Expr n) sr
    s
        SemiRingSum WeightedSum (Expr n) sr
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "semiring operations on non-bitvectors"
        SemiRingProd SemiRingProduct (Expr n) sr
    p
          | SR.SemiRingBVRepr BVFlavorRepr fv
    SR.BVArithRepr NatRepr w
    w <- SemiRingProduct (Expr n) sr -> SemiRingRepr sr
    forall (f :: BaseType -> Type) (sr :: SemiRing).
    SemiRingProduct f sr -> SemiRingRepr sr
    WS.prodRepr SemiRingProduct (Expr n) sr
    p ->
            (IExp (BaseBVType w)
     -> IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w)))
    -> (Expr n (SemiRingBase sr)
        -> VerilogM sym n (IExp (BaseBVType w)))
    -> SemiRingProduct (Expr n) sr
    -> VerilogM sym n (Maybe (IExp (BaseBVType w)))
    forall (m :: Type -> Type) r (f :: BaseType -> Type)
           (sr :: SemiRing).
    Monad m =>
    (r -> r -> m r)
    -> (f (SemiRingBase sr) -> m r)
    -> SemiRingProduct f sr
    -> m (Maybe r)
    WS.prodEvalM (Binop (BaseBVType w) (BaseBVType w)
    -> IExp (BaseBVType w)
    -> IExp (BaseBVType w)
    -> VerilogM sym n (IExp (BaseBVType w))
    forall (inTp :: BaseType) (outTp :: BaseType) sym n.
    Binop inTp outTp
    -> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
    binop Binop (BaseBVType w) (BaseBVType w)
    forall (w :: Natural). Binop ('BaseBVType w) ('BaseBVType w)
    BVMul) Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    Expr n (SemiRingBase sr) -> VerilogM sym n (IExp (BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr SemiRingProduct (Expr n) sr
    p VerilogM sym n (Maybe (IExp (BaseBVType w)))
    -> (Maybe (IExp (BaseBVType w)) -> VerilogM sym n (IExp tp))
    -> VerilogM sym n (IExp tp)
    forall a b.
    VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
              Maybe (IExp (BaseBVType w))
    Nothing -> NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
    forall (w :: Natural) sym n.
    (1 <= w) =>
    NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
    litBV NatRepr w
    w (NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    BV.mkBV NatRepr w
    w Integer
    1)
              Just IExp (BaseBVType w)
    e  -> IExp tp -> VerilogM sym n (IExp tp)
    forall a. a -> VerilogM sym n a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return IExp tp
    IExp (BaseBVType w)
    e
          | SR.SemiRingBVRepr BVFlavorRepr fv
    SR.BVBitsRepr NatRepr w
    w <- SemiRingProduct (Expr n) sr -> SemiRingRepr sr
    forall (f :: BaseType -> Type) (sr :: SemiRing).
    SemiRingProduct f sr -> SemiRingRepr sr
    WS.prodRepr SemiRingProduct (Expr n) sr
    p ->
            (IExp (BaseBVType w)
     -> IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w)))
    -> (Expr n (SemiRingBase sr)
        -> VerilogM sym n (IExp (BaseBVType w)))
    -> SemiRingProduct (Expr n) sr
    -> VerilogM sym n (Maybe (IExp (BaseBVType w)))
    forall (m :: Type -> Type) r (f :: BaseType -> Type)
           (sr :: SemiRing).
    Monad m =>
    (r -> r -> m r)
    -> (f (SemiRingBase sr) -> m r)
    -> SemiRingProduct f sr
    -> m (Maybe r)
    WS.prodEvalM (Binop (BaseBVType w) (BaseBVType w)
    -> IExp (BaseBVType w)
    -> IExp (BaseBVType w)
    -> VerilogM sym n (IExp (BaseBVType w))
    forall (inTp :: BaseType) (outTp :: BaseType) sym n.
    Binop inTp outTp
    -> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
    binop Binop (BaseBVType w) (BaseBVType w)
    forall (w :: Natural). Binop ('BaseBVType w) ('BaseBVType w)
    BVAnd) Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    Expr n (SemiRingBase sr) -> VerilogM sym n (IExp (BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr SemiRingProduct (Expr n) sr
    p VerilogM sym n (Maybe (IExp (BaseBVType w)))
    -> (Maybe (IExp (BaseBVType w)) -> VerilogM sym n (IExp tp))
    -> VerilogM sym n (IExp tp)
    forall a b.
    VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
              Maybe (IExp (BaseBVType w))
    Nothing -> NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
    forall (w :: Natural) sym n.
    (1 <= w) =>
    NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
    litBV NatRepr w
    w (NatRepr w -> BV w
    forall (w :: Natural). NatRepr w -> BV w
    BV.maxUnsigned NatRepr w
    w)
              Just IExp (BaseBVType w)
    e  -> IExp tp -> VerilogM sym n (IExp tp)
    forall a. a -> VerilogM sym n a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return IExp tp
    IExp (BaseBVType w)
    e
        SemiRingProd SemiRingProduct (Expr n) sr
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "semiring operations on non-bitvectors"
        -- SemiRingLe only accounts for Nats, Integers, and Reals, not bitvectors
        SemiRingLe OrderedSemiRingRepr sr
    _ Expr n (SemiRingBase sr)
    _ Expr n (SemiRingBase sr)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "semiring operations on non-bitvectors"

        -- Arithmetic operations
        RealIsInteger Expr n BaseRealType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "real numbers"

        IntDiv Expr n 'BaseIntegerType
    _ Expr n 'BaseIntegerType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "integers"
        IntMod Expr n 'BaseIntegerType
    _ Expr n 'BaseIntegerType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "integers"
        IntAbs Expr n 'BaseIntegerType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "integers"
        IntDivisible Expr n 'BaseIntegerType
    _ Natural
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "integers"

        RealDiv Expr n BaseRealType
    _ Expr n BaseRealType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "real numbers"
        RealSqrt Expr n BaseRealType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "real numbers"

        -- Irrational numbers
        RealSpecialFunction{} -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "real numbers"
        RoundEvenReal Expr n BaseRealType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "real numbers"

        -- Bitvector operations
        BVTestBit Natural
    i Expr n (BaseBVType w)
    e -> do v <- Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n (BaseBVType w)
    e
                            bit v (fromIntegral i)
        BVSlt Expr n (BaseBVType w)
    e1 Expr n (BaseBVType w)
    e2 ->
          do e1' <- IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
    signed (IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w)))
    -> VerilogM sym n (IExp (BaseBVType w))
    -> VerilogM sym n (IExp (BaseBVType w))
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n (BaseBVType w)
    e1
             e2' <- signed =<< exprToVerilogExpr e2
             binop Lt e1' e2'
        BVUlt Expr n (BaseBVType w)
    e1 Expr n (BaseBVType w)
    e2 ->
          do e1' <- Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n (BaseBVType w)
    e1
             e2' <- exprToVerilogExpr e2
             binop Lt e1' e2'

        BVOrBits NatRepr w
    w BVOrSet (Expr n) w
    bs ->
          do exprs <- (Expr n ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w)))
    -> [Expr n ('BaseBVType w)]
    -> VerilogM sym n [IExp ('BaseBVType w)]
    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 Expr n ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr (BVOrSet (Expr n) w -> [Expr n ('BaseBVType w)]
    forall (e :: BaseType -> Type) (w :: Natural).
    BVOrSet e w -> [e (BaseBVType w)]
    bvOrToList BVOrSet (Expr n) w
    bs)
             case exprs of
               [] -> NatRepr w -> BV w -> VerilogM sym n (IExp ('BaseBVType w))
    forall (w :: Natural) sym n.
    (1 <= w) =>
    NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
    litBV NatRepr w
    w (NatRepr w -> BV w
    forall (w :: Natural). NatRepr w -> BV w
    BV.zero NatRepr w
    w)
               IExp ('BaseBVType w)
    e:[IExp ('BaseBVType w)]
    es -> (IExp tp -> IExp tp -> VerilogM sym n (IExp tp))
    -> IExp tp -> [IExp tp] -> VerilogM sym n (IExp tp)
    forall (t :: Type -> Type) (m :: Type -> Type) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (Binop tp tp -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
    forall (inTp :: BaseType) (outTp :: BaseType) sym n.
    Binop inTp outTp
    -> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
    binop Binop tp tp
    Binop ('BaseBVType w) ('BaseBVType w)
    forall (w :: Natural). Binop ('BaseBVType w) ('BaseBVType w)
    BVOr) IExp tp
    IExp ('BaseBVType w)
    e [IExp tp]
    [IExp ('BaseBVType w)]
    es
        BVUnaryTerm UnaryBV (Expr n 'BaseBoolType) n
    ubv -> (Integer -> VerilogM sym n (IExp tp))
    -> (Expr n 'BaseBoolType
        -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp))
    -> UnaryBV (Expr n 'BaseBoolType) n
    -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) r p (n :: Natural).
    (Applicative m, Monad m) =>
    (Integer -> m r) -> (p -> r -> r -> m r) -> UnaryBV p n -> m r
    UBV.sym_evaluate (\Integer
    i -> NatRepr n -> BV n -> VerilogM sym n (IExp ('BaseBVType n))
    forall (w :: Natural) sym n.
    (1 <= w) =>
    NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
    litBV NatRepr n
    w (NatRepr n -> Integer -> BV n
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    BV.mkBV NatRepr n
    w Integer
    i)) Expr n 'BaseBoolType
    -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
    forall {sym} {n} {tp :: BaseType}.
    (SymExpr sym ~ Expr n, IsExprBuilder sym) =>
    Expr n 'BaseBoolType
    -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
    ite' UnaryBV (Expr n 'BaseBoolType) n
    ubv
          where
            w :: NatRepr n
    w = UnaryBV (Expr n 'BaseBoolType) n -> NatRepr n
    forall p (n :: Natural). UnaryBV p n -> NatRepr n
    UBV.width UnaryBV (Expr n 'BaseBoolType) n
    ubv
            ite' :: Expr n 'BaseBoolType
    -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
    ite' Expr n 'BaseBoolType
    e IExp tp
    e1 IExp tp
    e0 = do e' <- Expr n 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType)
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n 'BaseBoolType
    e
                              mux e' e0 e1

        BVConcat NatRepr (u + v)
    size12 Expr n (BaseBVType u)
    e1 Expr n (BaseBVType v)
    e2 -> do e1' <- Expr n (BaseBVType u) -> VerilogM sym n (IExp (BaseBVType u))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n (BaseBVType u)
    e1
                                    e2' <- exprToVerilogExpr e2
                                    concat2 size12 e1' e2'
        BVSelect NatRepr idx
    start NatRepr n
    len Expr n (BaseBVType w)
    bv -> do e <- Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n (BaseBVType w)
    bv
                                    bitSelect e start len
        BVFill NatRepr w
    len Expr n 'BaseBoolType
    b -> do e <- Expr n 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType)
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n 'BaseBoolType
    b
                           e1 <- litBV len (BV.maxUnsigned len)
                           e2 <- litBV len (BV.zero len)
                           mux e e1 e2
        BVUdiv NatRepr w
    _   Expr n ('BaseBVType w)
    bv1 Expr n ('BaseBVType w)
    bv2 ->
          do bv1' <- Expr n ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n ('BaseBVType w)
    bv1
             bv2' <- exprToVerilogExpr bv2
             binop BVDiv bv1' bv2'
        BVUrem NatRepr w
    _   Expr n ('BaseBVType w)
    bv1 Expr n ('BaseBVType w)
    bv2 ->
          do bv1' <- Expr n ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n ('BaseBVType w)
    bv1
             bv2' <- exprToVerilogExpr bv2
             binop BVRem bv1' bv2'
        BVSdiv NatRepr w
    _   Expr n ('BaseBVType w)
    bv1 Expr n ('BaseBVType w)
    bv2 ->
          do bv1' <- IExp ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w))
    forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
    signed (IExp ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w)))
    -> VerilogM sym n (IExp ('BaseBVType w))
    -> VerilogM sym n (IExp ('BaseBVType w))
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr n ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n ('BaseBVType w)
    bv1
             bv2' <- signed =<< exprToVerilogExpr bv2
             binop BVDiv bv1' bv2'
        BVSrem NatRepr w
    _   Expr n ('BaseBVType w)
    bv1 Expr n ('BaseBVType w)
    bv2 ->
          do bv1' <- IExp ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w))
    forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
    signed (IExp ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w)))
    -> VerilogM sym n (IExp ('BaseBVType w))
    -> VerilogM sym n (IExp ('BaseBVType w))
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr n ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n ('BaseBVType w)
    bv1
             bv2' <- signed =<< exprToVerilogExpr bv2
             binop BVRem bv1' bv2'
        BVShl  NatRepr w
    _   Expr n ('BaseBVType w)
    bv1 Expr n ('BaseBVType w)
    bv2 -> do e1 <- Expr n ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n ('BaseBVType w)
    bv1
                                 e2 <- exprToVerilogExpr bv2
                                 binop BVShiftL e1 e2
        BVLshr NatRepr w
    _   Expr n ('BaseBVType w)
    bv1 Expr n ('BaseBVType w)
    bv2 -> do e1 <- Expr n ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n ('BaseBVType w)
    bv1
                                 e2 <- exprToVerilogExpr bv2
                                 binop BVShiftR e1 e2
        BVAshr NatRepr w
    _   Expr n ('BaseBVType w)
    bv1 Expr n ('BaseBVType w)
    bv2 -> do e1 <- IExp ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w))
    forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
    signed (IExp ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w)))
    -> VerilogM sym n (IExp ('BaseBVType w))
    -> VerilogM sym n (IExp ('BaseBVType w))
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr n ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n ('BaseBVType w)
    bv1
                                 e2 <- exprToVerilogExpr bv2
                                 binop BVShiftRA e1 e2
        BVRol  NatRepr w
    w   Expr n ('BaseBVType w)
    bv1 Expr n ('BaseBVType w)
    bv2 ->
          do e1 <- Expr n ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n ('BaseBVType w)
    bv1
             case bv2 of
               SemiRingLiteral (SR.SemiRingBVRepr BVFlavorRepr fv
    _ NatRepr w
    _) Coefficient sr
    n ProgramLoc
    _ | BV w
    Coefficient sr
    n BV w -> BV w -> Bool
    forall a. Ord a => a -> a -> Bool
    <= NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    BV.mkBV NatRepr w
    w (NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue NatRepr w
    w) ->
                 Exp tp -> VerilogM sym n (IExp tp)
    forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
    mkLet (NatRepr w -> IExp tp -> BV w -> Exp tp
    forall (w :: Natural) (tp :: BaseType).
    NatRepr w -> IExp tp -> BV w -> Exp tp
    BVRotateL NatRepr w
    w IExp tp
    IExp ('BaseBVType w)
    e1 BV w
    Coefficient sr
    n)
               Expr n ('BaseBVType w)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "non-constant bit rotations"
        BVRor  NatRepr w
    w   Expr n ('BaseBVType w)
    bv1 Expr n ('BaseBVType w)
    bv2 ->
          do e1 <- Expr n ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n ('BaseBVType w)
    bv1
             case bv2 of
               SemiRingLiteral (SR.SemiRingBVRepr BVFlavorRepr fv
    _ NatRepr w
    _) Coefficient sr
    n ProgramLoc
    _ | BV w
    Coefficient sr
    n BV w -> BV w -> Bool
    forall a. Ord a => a -> a -> Bool
    <= NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    BV.mkBV NatRepr w
    w (NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue NatRepr w
    w) ->
                 Exp tp -> VerilogM sym n (IExp tp)
    forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
    mkLet (NatRepr w -> IExp tp -> BV w -> Exp tp
    forall (w :: Natural) (tp :: BaseType).
    NatRepr w -> IExp tp -> BV w -> Exp tp
    BVRotateR NatRepr w
    w IExp tp
    IExp ('BaseBVType w)
    e1 BV w
    Coefficient sr
    n)
               Expr n ('BaseBVType w)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "non-constant bit rotations"
        BVZext NatRepr r
    w Expr n (BaseBVType w)
    e ->
          LeqProof w r
    -> ((w <= r) => VerilogM sym n (IExp tp))
    -> VerilogM sym n (IExp tp)
    forall (m :: Natural) (n :: Natural) a.
    LeqProof m n -> ((m <= n) => a) -> a
    withLeqProof (NatRepr r -> NatRepr w -> LeqProof w r
    forall (n :: Natural) (m :: Natural) (p :: Natural -> Type).
    ((n + 1) <= m) =>
    p m -> NatRepr n -> LeqProof n m
    leqSuccLeft NatRepr r
    w NatRepr w
    ew) (((w <= r) => VerilogM sym n (IExp tp))
     -> VerilogM sym n (IExp tp))
    -> ((w <= r) => VerilogM sym n (IExp tp))
    -> VerilogM sym n (IExp tp)
    forall a b. (a -> b) -> a -> b
    $
          LeqProof 1 (r - w)
    -> ((1 <= (r - w)) => VerilogM sym n (IExp tp))
    -> VerilogM sym n (IExp tp)
    forall (m :: Natural) (n :: Natural) a.
    LeqProof m n -> ((m <= n) => a) -> a
    withLeqProof (NatRepr r -> NatRepr w -> LeqProof 1 (r - w)
    forall (m :: Natural) (n :: Natural).
    (1 <= m, 1 <= n, (n + 1) <= m) =>
    NatRepr m -> NatRepr n -> LeqProof 1 (m - n)
    leqSubPos NatRepr r
    w NatRepr w
    ew) (((1 <= (r - w)) => VerilogM sym n (IExp tp))
     -> VerilogM sym n (IExp tp))
    -> ((1 <= (r - w)) => VerilogM sym n (IExp tp))
    -> VerilogM sym n (IExp tp)
    forall a b. (a -> b) -> a -> b
    $
          case NatRepr r -> NatRepr w -> ((r - w) + w) :~: r
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    (n <= m) =>
    f m -> g n -> ((m - n) + n) :~: m
    minusPlusCancel NatRepr r
    w NatRepr w
    ew of
            ((r - w) + w) :~: r
    Refl ->
              do e' <- Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n (BaseBVType w)
    e
                 let n = NatRepr r
    w NatRepr r -> NatRepr w -> NatRepr (r - w)
    forall (n :: Natural) (m :: Natural).
    (n <= m) =>
    NatRepr m -> NatRepr n -> NatRepr (m - n)
    `subNat` NatRepr w
    ew
                 zeros <- litBV n (BV.zero n)
                 concat2 w zeros e'
          where ew :: NatRepr w
    ew = Expr n (BaseBVType w) -> NatRepr w
    forall (w :: Natural). Expr n (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    bvWidth Expr n (BaseBVType w)
    e
        BVSext NatRepr r
    w Expr n (BaseBVType w)
    e ->
          LeqProof w r
    -> ((w <= r) => VerilogM sym n (IExp tp))
    -> VerilogM sym n (IExp tp)
    forall (m :: Natural) (n :: Natural) a.
    LeqProof m n -> ((m <= n) => a) -> a
    withLeqProof (NatRepr r -> NatRepr w -> LeqProof w r
    forall (n :: Natural) (m :: Natural) (p :: Natural -> Type).
    ((n + 1) <= m) =>
    p m -> NatRepr n -> LeqProof n m
    leqSuccLeft NatRepr r
    w NatRepr w
    ew) (((w <= r) => VerilogM sym n (IExp tp))
     -> VerilogM sym n (IExp tp))
    -> ((w <= r) => VerilogM sym n (IExp tp))
    -> VerilogM sym n (IExp tp)
    forall a b. (a -> b) -> a -> b
    $
          LeqProof 1 (r - w)
    -> ((1 <= (r - w)) => VerilogM sym n (IExp tp))
    -> VerilogM sym n (IExp tp)
    forall (m :: Natural) (n :: Natural) a.
    LeqProof m n -> ((m <= n) => a) -> a
    withLeqProof (NatRepr r -> NatRepr w -> LeqProof 1 (r - w)
    forall (m :: Natural) (n :: Natural).
    (1 <= m, 1 <= n, (n + 1) <= m) =>
    NatRepr m -> NatRepr n -> LeqProof 1 (m - n)
    leqSubPos NatRepr r
    w NatRepr w
    ew) (((1 <= (r - w)) => VerilogM sym n (IExp tp))
     -> VerilogM sym n (IExp tp))
    -> ((1 <= (r - w)) => VerilogM sym n (IExp tp))
    -> VerilogM sym n (IExp tp)
    forall a b. (a -> b) -> a -> b
    $
          case NatRepr r -> NatRepr w -> ((r - w) + w) :~: r
    forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
           (n :: Natural).
    (n <= m) =>
    f m -> g n -> ((m - n) + n) :~: m
    minusPlusCancel NatRepr r
    w NatRepr w
    ew of
            ((r - w) + w) :~: r
    Refl ->
              do e' <- Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr Expr n (BaseBVType w)
    e
                 let n = NatRepr r
    w NatRepr r -> NatRepr w -> NatRepr (r - w)
    forall (n :: Natural) (m :: Natural).
    (n <= m) =>
    NatRepr m -> NatRepr n -> NatRepr (m - n)
    `subNat` NatRepr w
    ew
                 zeros <- litBV n (BV.zero n)
                 ones <- litBV n (BV.maxUnsigned n)
                 sgn <- bit e' (fromIntegral (natValue w) - 1)
                 ext <- mux sgn ones zeros
                 concat2 w ext e'
          where ew :: NatRepr w
    ew = Expr n (BaseBVType w) -> NatRepr w
    forall (w :: Natural). Expr n (BaseBVType w) -> NatRepr w
    forall (e :: BaseType -> Type) (w :: Natural).
    IsExpr e =>
    e (BaseBVType w) -> NatRepr w
    bvWidth Expr n (BaseBVType w)
    e
        BVPopcount NatRepr w
    _ Expr n ('BaseBVType w)
    _ ->
          String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "bit vector population count" -- TODO
        BVCountTrailingZeros NatRepr w
    _ Expr n ('BaseBVType w)
    _ ->
          String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "bit vector count trailing zeros" -- TODO
        BVCountLeadingZeros  NatRepr w
    _ Expr n ('BaseBVType w)
    _ ->
          String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "bit vector count leading zeros" -- TODO

        -- Float operations
        FloatNeg FloatPrecisionRepr fpp
    _ Expr n ('BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatAbs FloatPrecisionRepr fpp
    _ Expr n ('BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatSqrt FloatPrecisionRepr fpp
    _ RoundingMode
    _ Expr n ('BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatAdd  FloatPrecisionRepr fpp
    _ RoundingMode
    _ Expr n ('BaseFloatType fpp)
    _ Expr n ('BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatSub  FloatPrecisionRepr fpp
    _ RoundingMode
    _ Expr n ('BaseFloatType fpp)
    _ Expr n ('BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatMul  FloatPrecisionRepr fpp
    _ RoundingMode
    _ Expr n ('BaseFloatType fpp)
    _ Expr n ('BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatDiv FloatPrecisionRepr fpp
    _ RoundingMode
    _ Expr n ('BaseFloatType fpp)
    _ Expr n ('BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatRem FloatPrecisionRepr fpp
    _ Expr n ('BaseFloatType fpp)
    _ Expr n ('BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatFMA FloatPrecisionRepr fpp
    _ RoundingMode
    _ Expr n ('BaseFloatType fpp)
    _ Expr n ('BaseFloatType fpp)
    _ Expr n ('BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatFpEq Expr n (BaseFloatType fpp)
    _ Expr n (BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatLe Expr n (BaseFloatType fpp)
    _ Expr n (BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatLt Expr n (BaseFloatType fpp)
    _ Expr n (BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"

        FloatIsNaN Expr n (BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatIsInf Expr n (BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatIsZero Expr n (BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatIsPos Expr n (BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatIsNeg Expr n (BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatIsSubnorm Expr n (BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatIsNorm Expr n (BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"

        FloatCast FloatPrecisionRepr fpp
    _ RoundingMode
    _ Expr n (BaseFloatType fpp')
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatRound FloatPrecisionRepr fpp
    _ RoundingMode
    _ Expr n ('BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatFromBinary FloatPrecisionRepr (FloatingPointPrecision eb sb)
    _ Expr n (BaseBVType (eb + sb))
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatToBinary FloatPrecisionRepr (FloatingPointPrecision eb sb)
    _ Expr n (BaseFloatType (FloatingPointPrecision eb sb))
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        BVToFloat FloatPrecisionRepr fpp
    _ RoundingMode
    _ Expr n (BaseBVType w)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        SBVToFloat FloatPrecisionRepr fpp
    _ RoundingMode
    _ Expr n (BaseBVType w)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        RealToFloat FloatPrecisionRepr fpp
    _ RoundingMode
    _ Expr n BaseRealType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatToBV NatRepr w
    _ RoundingMode
    _ Expr n (BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatToSBV NatRepr w
    _ RoundingMode
    _ Expr n (BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatToReal Expr n (BaseFloatType fpp)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"
        FloatSpecialFunction FloatPrecisionRepr fpp
    _ SpecialFunction args
    _ SpecialFnArgs (Expr n) ('BaseFloatType fpp) args
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "floats"

        -- Array operations
        ArrayMap Assignment BaseTypeRepr (i ::> itp)
    _ BaseTypeRepr tp1
    _ ArrayUpdateMap (Expr n) (i ::> itp) tp1
    _ Expr n ('BaseArrayType (i ::> itp) tp1)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "arrays"
        ConstantArray Assignment BaseTypeRepr (i ::> tp1)
    _ BaseTypeRepr b
    _ Expr n b
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "arrays"
        UpdateArray BaseTypeRepr b
    _ Assignment BaseTypeRepr (i ::> tp1)
    _ Expr n ('BaseArrayType (i ::> tp1) b)
    _ Assignment (Expr n) (i ::> tp1)
    _ Expr n b
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "arrays"
        SelectArray BaseTypeRepr tp
    _ Expr n (BaseArrayType (i ::> tp1) tp)
    _ Assignment (Expr n) (i ::> tp1)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "arrays"
        CopyArray NatRepr w
    _ BaseTypeRepr a
    _ Expr n ('BaseArrayType (SingleCtx (BaseBVType w)) a)
    _ Expr n (BaseBVType w)
    _ Expr n ('BaseArrayType (SingleCtx (BaseBVType w)) a)
    _ Expr n (BaseBVType w)
    _ Expr n (BaseBVType w)
    _ Expr n (BaseBVType w)
    _ Expr n (BaseBVType w)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "arrays"
        SetArray NatRepr w
    _ BaseTypeRepr a
    _ Expr n ('BaseArrayType (SingleCtx (BaseBVType w)) a)
    _ Expr n (BaseBVType w)
    _ Expr n a
    _ Expr n (BaseBVType w)
    _ Expr n (BaseBVType w)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "arrays"
        EqualArrayRange NatRepr w
    _ BaseTypeRepr a
    _ Expr n (BaseArrayType (SingleCtx (BaseBVType w)) a)
    _ Expr n (BaseBVType w)
    _ Expr n (BaseArrayType (SingleCtx (BaseBVType w)) a)
    _ Expr n (BaseBVType w)
    _ Expr n (BaseBVType w)
    _ Expr n (BaseBVType w)
    _ Expr n (BaseBVType w)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "arrays"

        -- Conversions
        IntegerToReal Expr n 'BaseIntegerType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "integers"
        RealToInteger Expr n BaseRealType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "integers"
        BVToInteger Expr n (BaseBVType w)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "integers"
        SBVToInteger Expr n (BaseBVType w)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "integers"
        IntegerToBV Expr n 'BaseIntegerType
    _ NatRepr w
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "integers"
        RoundReal Expr n BaseRealType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "real numbers"
        FloorReal Expr n BaseRealType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "real numbers"
        CeilReal Expr n BaseRealType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "real numbers"

        -- Complex operations
        Cplx Complex (Expr n BaseRealType)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "complex numbers"
        RealPart Expr n 'BaseComplexType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "complex numbers"
        ImagPart Expr n 'BaseComplexType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "complex Numbers"

        -- Structs
        StructCtor Assignment BaseTypeRepr flds
    _ Assignment (Expr n) flds
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "structs"
        StructField Expr n (BaseStructType flds)
    _ Index flds tp
    _ BaseTypeRepr tp
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "structs"

        -- Strings
        StringAppend StringInfoRepr si
    _ StringSeq (Expr n) si
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "strings"
        StringContains Expr n (BaseStringType si)
    _ Expr n (BaseStringType si)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "strings"
        StringIndexOf Expr n (BaseStringType si)
    _ Expr n (BaseStringType si)
    _ Expr n 'BaseIntegerType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "strings"
        StringIsPrefixOf Expr n (BaseStringType si)
    _ Expr n (BaseStringType si)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "strings"
        StringIsSuffixOf Expr n (BaseStringType si)
    _ Expr n (BaseStringType si)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "strings"
        StringLength Expr n (BaseStringType si)
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "strings"
        StringSubstring StringInfoRepr si
    _ Expr n ('BaseStringType si)
    _ Expr n 'BaseIntegerType
    _ Expr n 'BaseIntegerType
    _ -> String -> VerilogM sym n (IExp tp)
    forall (m :: Type -> Type) a. MonadError String m => String -> m a
    doNotSupportError String
    "strings"