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

    An intermediate AST to use for generating Verilog modules from What4 expressions.
    -}
    {-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, ScopedTypeVariables,
      TypeApplications, PolyKinds, DataKinds, ExplicitNamespaces, TypeOperators,
      OverloadedStrings #-}

    module What4.Protocol.VerilogWriter.AST
      where

    import qualified Data.BitVector.Sized as BV
    import qualified Data.Map as Map
    import qualified Data.Text as T
    import qualified Data.Set as Set
    import           Data.String
    import           Data.Word
    import           Control.Monad (forM_)
    import           Control.Monad.Except (ExceptT, MonadError(..))
    import           Control.Monad.IO.Class (MonadIO(..))
    import           Control.Monad.State (MonadState(), StateT(..), get, put, modify, gets)

    import qualified What4.BaseTypes as WT
    import           What4.Expr.Builder
    import           Data.Parameterized.Classes (OrderingF(..), compareF)
    import           Data.Parameterized.Nonce (Nonce, indexValue)
    import           Data.Parameterized.Some (Some(..), viewSome)
    import           Data.Parameterized.Pair
    import           GHC.TypeNats ( type (<=) )

    type Identifier = T.Text

    -- | A type for Verilog binary operators that enforces well-typedness,
    -- including bitvector size constraints.
    data Binop (inTp :: WT.BaseType) (outTp :: WT.BaseType) where
      And :: Binop WT.BaseBoolType WT.BaseBoolType
      Or  :: Binop WT.BaseBoolType WT.BaseBoolType
      Xor :: Binop WT.BaseBoolType WT.BaseBoolType

      Eq :: Binop tp WT.BaseBoolType
      Ne :: Binop tp WT.BaseBoolType
      Lt :: Binop (WT.BaseBVType w) WT.BaseBoolType
      Le :: Binop (WT.BaseBVType w) WT.BaseBoolType

      BVAnd :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
      BVOr  :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
      BVXor :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
      BVAdd :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
      BVSub :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
      BVMul :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
      BVDiv :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
      BVRem :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
      BVPow :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
      BVShiftL :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
      BVShiftR :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
      BVShiftRA :: Binop (WT.BaseBVType w) (WT.BaseBVType w)

    binopType ::
      Binop inTp outTp ->
      WT.BaseTypeRepr inTp ->
      WT.BaseTypeRepr outTp
    binopType :: forall (inTp :: BaseType) (outTp :: BaseType).
    Binop inTp outTp -> BaseTypeRepr inTp -> BaseTypeRepr outTp
    binopType Binop inTp outTp
    And BaseTypeRepr inTp
    _ = BaseTypeRepr outTp
    BaseTypeRepr 'BaseBoolType
    WT.BaseBoolRepr
    binopType Binop inTp outTp
    Or  BaseTypeRepr inTp
    _ = BaseTypeRepr outTp
    BaseTypeRepr 'BaseBoolType
    WT.BaseBoolRepr
    binopType Binop inTp outTp
    Xor BaseTypeRepr inTp
    _ = BaseTypeRepr outTp
    BaseTypeRepr 'BaseBoolType
    WT.BaseBoolRepr
    binopType Binop inTp outTp
    Eq  BaseTypeRepr inTp
    _ = BaseTypeRepr outTp
    BaseTypeRepr 'BaseBoolType
    WT.BaseBoolRepr
    binopType Binop inTp outTp
    Ne  BaseTypeRepr inTp
    _ = BaseTypeRepr outTp
    BaseTypeRepr 'BaseBoolType
    WT.BaseBoolRepr
    binopType Binop inTp outTp
    Lt  BaseTypeRepr inTp
    _ = BaseTypeRepr outTp
    BaseTypeRepr 'BaseBoolType
    WT.BaseBoolRepr
    binopType Binop inTp outTp
    Le  BaseTypeRepr inTp
    _ = BaseTypeRepr outTp
    BaseTypeRepr 'BaseBoolType
    WT.BaseBoolRepr
    binopType Binop inTp outTp
    BVAnd  BaseTypeRepr inTp
    tp = BaseTypeRepr inTp
    BaseTypeRepr outTp
    tp
    binopType Binop inTp outTp
    BVOr  BaseTypeRepr inTp
    tp = BaseTypeRepr inTp
    BaseTypeRepr outTp
    tp
    binopType Binop inTp outTp
    BVXor BaseTypeRepr inTp
    tp = BaseTypeRepr inTp
    BaseTypeRepr outTp
    tp
    binopType Binop inTp outTp
    BVAdd BaseTypeRepr inTp
    tp = BaseTypeRepr inTp
    BaseTypeRepr outTp
    tp
    binopType Binop inTp outTp
    BVSub BaseTypeRepr inTp
    tp = BaseTypeRepr inTp
    BaseTypeRepr outTp
    tp
    binopType Binop inTp outTp
    BVMul BaseTypeRepr inTp
    tp = BaseTypeRepr inTp
    BaseTypeRepr outTp
    tp
    binopType Binop inTp outTp
    BVDiv BaseTypeRepr inTp
    tp = BaseTypeRepr inTp
    BaseTypeRepr outTp
    tp
    binopType Binop inTp outTp
    BVRem BaseTypeRepr inTp
    tp = BaseTypeRepr inTp
    BaseTypeRepr outTp
    tp
    binopType Binop inTp outTp
    BVPow BaseTypeRepr inTp
    tp = BaseTypeRepr inTp
    BaseTypeRepr outTp
    tp
    binopType Binop inTp outTp
    BVShiftL BaseTypeRepr inTp
    tp = BaseTypeRepr inTp
    BaseTypeRepr outTp
    tp
    binopType Binop inTp outTp
    BVShiftR BaseTypeRepr inTp
    tp = BaseTypeRepr inTp
    BaseTypeRepr outTp
    tp
    binopType Binop inTp outTp
    BVShiftRA BaseTypeRepr inTp
    tp = BaseTypeRepr inTp
    BaseTypeRepr outTp
    tp

    -- | A type for Verilog unary operators that enforces well-typedness.
    data Unop (tp :: WT.BaseType) where
      Not :: Unop WT.BaseBoolType
      BVNot :: Unop (WT.BaseBVType w)

    -- | A type for Verilog expression names that enforces well-typedness.
    -- This type exists essentially to pair a name and type to avoid needing
    -- to repeat them and ensure that all uses of the name are well-typed.
    data IExp (tp :: WT.BaseType) where
      Ident   :: WT.BaseTypeRepr tp -> Identifier -> IExp tp

    iexpType :: IExp tp -> WT.BaseTypeRepr tp
    iexpType :: forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
    iexpType (Ident BaseTypeRepr tp
    tp Identifier
    _) = BaseTypeRepr tp
    tp

    data LHS = LHS Identifier | LHSBit Identifier Integer

    -- | A type for Verilog expressions that enforces well-typedness,
    -- including bitvector size constraints.
    data Exp (tp :: WT.BaseType) where
      IExp :: IExp tp -> Exp tp
      Binop :: Binop inTp outTp -> IExp inTp -> IExp inTp -> Exp outTp
      Unop :: Unop tp -> IExp tp -> Exp tp
      BVRotateL :: WT.NatRepr w -> IExp tp -> BV.BV w -> Exp tp
      BVRotateR :: WT.NatRepr w -> IExp tp -> BV.BV w -> Exp tp
      Mux :: IExp WT.BaseBoolType -> IExp tp -> IExp tp -> Exp tp
      Bit :: IExp (WT.BaseBVType w)
          -> Integer
          -> Exp WT.BaseBoolType
      BitSelect :: (1 WT.<= len, start WT.+ len WT.<= w)
          => IExp (WT.BaseBVType w)
          -> WT.NatRepr start
          -> WT.NatRepr len
          -> Exp (WT.BaseBVType len)
      Concat :: 1 <= w
              => WT.NatRepr w -> [Some IExp] -> Exp (WT.BaseBVType w)
      BVLit   :: (1 <= w)
              => WT.NatRepr w -- the width
              -> BV.BV w -- the value
              -> Exp (WT.BaseBVType w)
      BoolLit :: Bool -> Exp WT.BaseBoolType

    expType :: Exp tp -> WT.BaseTypeRepr tp
    expType :: forall (tp :: BaseType). Exp tp -> BaseTypeRepr tp
    expType (IExp IExp tp
    e) = IExp tp -> BaseTypeRepr tp
    forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
    iexpType IExp tp
    e
    expType (Binop Binop inTp tp
    op IExp inTp
    e1 IExp inTp
    _) = Binop inTp tp -> BaseTypeRepr inTp -> BaseTypeRepr tp
    forall (inTp :: BaseType) (outTp :: BaseType).
    Binop inTp outTp -> BaseTypeRepr inTp -> BaseTypeRepr outTp
    binopType Binop inTp tp
    op (IExp inTp -> BaseTypeRepr inTp
    forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
    iexpType IExp inTp
    e1)
    expType (BVRotateL NatRepr w
    _ IExp tp
    e BV w
    _) = IExp tp -> BaseTypeRepr tp
    forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
    iexpType IExp tp
    e
    expType (BVRotateR NatRepr w
    _ IExp tp
    e BV w
    _) = IExp tp -> BaseTypeRepr tp
    forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
    iexpType IExp tp
    e
    expType (Unop Unop tp
    _ IExp tp
    e) = IExp tp -> BaseTypeRepr tp
    forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
    iexpType IExp tp
    e
    expType (Mux IExp 'BaseBoolType
    _ IExp tp
    e1 IExp tp
    _) = IExp tp -> BaseTypeRepr tp
    forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
    iexpType IExp tp
    e1
    expType (Bit IExp (BaseBVType w)
    _ Integer
    _) = BaseTypeRepr tp
    BaseTypeRepr 'BaseBoolType
    WT.BaseBoolRepr
    expType (BitSelect IExp (BaseBVType w)
    _ NatRepr start
    _ NatRepr len
    n) = NatRepr len -> BaseTypeRepr ('BaseBVType len)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    WT.BaseBVRepr NatRepr len
    n
    expType (Concat NatRepr w
    w [Some IExp]
    _) = NatRepr w -> BaseTypeRepr ('BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    WT.BaseBVRepr NatRepr w
    w
    expType (BVLit NatRepr w
    w BV w
    _) = NatRepr w -> BaseTypeRepr ('BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    WT.BaseBVRepr NatRepr w
    w
    expType (BoolLit Bool
    _) = BaseTypeRepr tp
    BaseTypeRepr 'BaseBoolType
    WT.BaseBoolRepr

    -- | Create a let binding, associating a name with an expression. In
    -- Verilog, this is a new "wire".
    mkLet :: Exp tp -> VerilogM sym n (IExp tp)
    mkLet :: forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
    mkLet (IExp IExp tp
    x) = 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
    x
    mkLet Exp tp
    e = do
        let tp :: BaseTypeRepr tp
    tp = Exp tp -> BaseTypeRepr tp
    forall (tp :: BaseType). Exp tp -> BaseTypeRepr tp
    expType Exp tp
    e
        x <- BaseTypeRepr tp
    -> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
    forall (tp :: BaseType) sym n.
    BaseTypeRepr tp
    -> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
    addFreshWire BaseTypeRepr tp
    tp Bool
    False Identifier
    "wr" Exp tp
    e
        return (Ident tp x)

    -- | Indicate than an expression name is signed. This causes arithmetic
    -- operations involving this name to be interpreted as signed
    -- operations.
    signed :: IExp tp -> VerilogM sym n (IExp tp)
    signed :: forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
    signed IExp tp
    e = do
        let tp :: BaseTypeRepr tp
    tp = IExp tp -> BaseTypeRepr tp
    forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
    iexpType IExp tp
    e
        x <- BaseTypeRepr tp
    -> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
    forall (tp :: BaseType) sym n.
    BaseTypeRepr tp
    -> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
    addFreshWire BaseTypeRepr tp
    tp Bool
    True Identifier
    "wr" (IExp tp -> Exp tp
    forall (tp :: BaseType). IExp tp -> Exp tp
    IExp IExp tp
    e)
        return (Ident tp x)

    -- | Apply a binary operation to two expressions and bind the result to
    -- a new, returned name.
    binop ::
      Binop inTp outTp ->
      IExp inTp -> IExp inTp ->
      VerilogM sym n (IExp outTp)
    binop :: forall (inTp :: BaseType) (outTp :: BaseType) sym n.
    Binop inTp outTp
    -> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
    binop Binop inTp outTp
    op IExp inTp
    e1 IExp inTp
    e2 = Exp outTp -> VerilogM sym n (IExp outTp)
    forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
    mkLet (Binop inTp outTp -> IExp inTp -> IExp inTp -> Exp outTp
    forall (w :: BaseType) (outTp :: BaseType).
    Binop w outTp -> IExp w -> IExp w -> Exp outTp
    Binop Binop inTp outTp
    op IExp inTp
    e1 IExp inTp
    e2)

    -- | A special binary operation for scalar multiplication. This avoids
    -- the need to call `litBV` at every call site.
    scalMult ::
      1 <= w =>
      WT.NatRepr w ->
      Binop (WT.BaseBVType w) (WT.BaseBVType w) ->
      BV.BV w ->
      IExp (WT.BaseBVType w) ->
      VerilogM sym n (IExp (WT.BaseBVType w))
    scalMult :: 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)
    op BV w
    n IExp (BaseBVType w)
    e = do
      n' <- 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
    n
      binop op n' e

    -- | A wrapper around the BV type allowing it to be put into a map or
    -- set. We use this to make sure we generate only one instance of each
    -- distinct constant.
    data BVConst = BVConst (Pair WT.NatRepr BV.BV)
      deriving (BVConst -> BVConst -> Bool
    (BVConst -> BVConst -> Bool)
    -> (BVConst -> BVConst -> Bool) -> Eq BVConst
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: BVConst -> BVConst -> Bool
    == :: BVConst -> BVConst -> Bool
    $c/= :: BVConst -> BVConst -> Bool
    /= :: BVConst -> BVConst -> Bool
    Eq)

    instance Ord BVConst where
      compare :: BVConst -> BVConst -> Ordering
    compare (BVConst Pair NatRepr BV
    cx) (BVConst Pair NatRepr BV
    cy) =
        (forall (tp :: Natural). NatRepr tp -> BV tp -> Ordering)
    -> Pair NatRepr BV -> Ordering
    forall {k} (a :: k -> Type) (b :: k -> Type) c.
    (forall (tp :: k). a tp -> b tp -> c) -> Pair a b -> c
    viewPair (\NatRepr tp
    wx BV tp
    x -> (forall (tp :: Natural). NatRepr tp -> BV tp -> Ordering)
    -> Pair NatRepr BV -> Ordering
    forall {k} (a :: k -> Type) (b :: k -> Type) c.
    (forall (tp :: k). a tp -> b tp -> c) -> Pair a b -> c
    viewPair (\NatRepr tp
    wy BV tp
    y ->
          case NatRepr tp -> NatRepr tp -> OrderingF tp tp
    forall (x :: Natural) (y :: Natural).
    NatRepr x -> NatRepr y -> OrderingF x y
    forall k (ktp :: k -> Type) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> OrderingF x y
    compareF NatRepr tp
    wx NatRepr tp
    wy of
            OrderingF tp tp
    LTF -> Ordering
    LT
            OrderingF tp tp
    EQF | BV tp -> BV tp -> Bool
    forall (w :: Natural). BV w -> BV w -> Bool
    BV.ult BV tp
    x BV tp
    BV tp
    y -> Ordering
    LT
            OrderingF tp tp
    EQF | BV tp -> BV tp -> Bool
    forall (w :: Natural). BV w -> BV w -> Bool
    BV.ult BV tp
    BV tp
    y BV tp
    x -> Ordering
    GT
            OrderingF tp tp
    EQF -> Ordering
    EQ
            OrderingF tp tp
    GTF -> Ordering
    GT
        ) Pair NatRepr BV
    cy) Pair NatRepr BV
    cx

    -- | Return the (possibly-cached) name for a literal bitvector value.
    litBV ::
      (1 <= w) =>
      WT.NatRepr w ->
      BV.BV w ->
      VerilogM sym n (IExp (WT.BaseBVType w))
    litBV :: forall (w :: Natural) sym n.
    (1 <= w) =>
    NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
    litBV NatRepr w
    w BV w
    i = do
      cache <- ModuleState sym n -> Map BVConst Identifier
    forall sym n. ModuleState sym n -> Map BVConst Identifier
    vsBVCache (ModuleState sym n -> Map BVConst Identifier)
    -> VerilogM sym n (ModuleState sym n)
    -> VerilogM sym n (Map BVConst Identifier)
    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
      case Map.lookup (BVConst (Pair w i)) cache of
        Just Identifier
    x -> IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    forall a. a -> VerilogM sym n a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (BaseTypeRepr (BaseBVType w) -> Identifier -> IExp (BaseBVType w)
    forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
    Ident (NatRepr w -> BaseTypeRepr (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BaseTypeRepr ('BaseBVType w)
    WT.BaseBVRepr NatRepr w
    w) Identifier
    x)
        Maybe Identifier
    Nothing -> do
          x@(Ident _ name) <- Exp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
    mkLet (NatRepr w -> BV w -> Exp (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> BV w -> Exp (BaseBVType w)
    BVLit NatRepr w
    w BV w
    i)
          modify $ \ModuleState sym n
    s -> ModuleState sym n
    s { vsBVCache = Map.insert (BVConst (Pair w i)) name (vsBVCache s) }
          return x

    -- | Return the (possibly-cached) name for a literal Boolean value.
    litBool :: Bool -> VerilogM sym n (IExp WT.BaseBoolType)
    litBool :: forall sym n. Bool -> VerilogM sym n (IExp 'BaseBoolType)
    litBool Bool
    b = do
      cache <- ModuleState sym n -> Map Bool Identifier
    forall sym n. ModuleState sym n -> Map Bool Identifier
    vsBoolCache (ModuleState sym n -> Map Bool Identifier)
    -> VerilogM sym n (ModuleState sym n)
    -> VerilogM sym n (Map Bool Identifier)
    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
      case Map.lookup b cache of
        Just Identifier
    x -> IExp 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType)
    forall a. a -> VerilogM sym n a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (BaseTypeRepr 'BaseBoolType -> Identifier -> IExp 'BaseBoolType
    forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
    Ident BaseTypeRepr 'BaseBoolType
    WT.BaseBoolRepr Identifier
    x)
        Maybe Identifier
    Nothing -> do
          x@(Ident _ name) <- Exp 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType)
    forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
    mkLet (Bool -> Exp 'BaseBoolType
    BoolLit Bool
    b)
          modify $ \ModuleState sym n
    s -> ModuleState sym n
    s { vsBoolCache = Map.insert b name (vsBoolCache s) }
          return x

    -- | Apply a unary operation to an expression and bind the result to a
    -- new, returned name.
    unop :: Unop tp -> IExp tp -> VerilogM sym n (IExp tp)
    unop :: forall (tp :: BaseType) sym n.
    Unop tp -> IExp tp -> VerilogM sym n (IExp tp)
    unop Unop tp
    op IExp tp
    e = Exp tp -> VerilogM sym n (IExp tp)
    forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
    mkLet (Unop tp -> IExp tp -> Exp tp
    forall (tp :: BaseType). Unop tp -> IExp tp -> Exp tp
    Unop Unop tp
    op IExp tp
    e)

    -- | Create a conditional, with the given condition, true, and false
    -- branches, and bind the result to a new, returned name.
    mux ::
      IExp WT.BaseBoolType ->
      IExp tp ->
      IExp tp ->
      VerilogM sym n (IExp tp)
    mux :: forall (tp :: BaseType) sym n.
    IExp 'BaseBoolType
    -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
    mux IExp 'BaseBoolType
    e IExp tp
    e1 IExp tp
    e2 = Exp tp -> VerilogM sym n (IExp tp)
    forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
    mkLet (IExp 'BaseBoolType -> IExp tp -> IExp tp -> Exp tp
    forall (tp :: BaseType).
    IExp 'BaseBoolType -> IExp tp -> IExp tp -> Exp tp
    Mux IExp 'BaseBoolType
    e IExp tp
    e1 IExp tp
    e2)

    -- | Extract a single bit from a bit vector and bind the result to a
    -- new, returned name.
    bit ::
      IExp (WT.BaseBVType w) ->
      Integer ->
      VerilogM sym n (IExp WT.BaseBoolType)
    bit :: forall (w :: Natural) sym n.
    IExp (BaseBVType w)
    -> Integer -> VerilogM sym n (IExp 'BaseBoolType)
    bit IExp (BaseBVType w)
    e Integer
    i = Exp 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType)
    forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
    mkLet (IExp (BaseBVType w) -> Integer -> Exp 'BaseBoolType
    forall (w :: Natural).
    IExp (BaseBVType w) -> Integer -> Exp 'BaseBoolType
    Bit IExp (BaseBVType w)
    e Integer
    i)

    -- | Extract a range of bits from a bit vector and bind the result to a
    -- new, returned name. The two `NatRepr` values are the starting index
    -- and the number of bits to extract, respectively.
    bitSelect ::
      (1 WT.<= len, idx WT.+ len WT.<= w) =>
      IExp (WT.BaseBVType w) ->
      WT.NatRepr idx ->
      WT.NatRepr len ->
      VerilogM sym n (IExp (WT.BaseBVType len))
    bitSelect :: forall (len :: Natural) (idx :: Natural) (w :: Natural) sym n.
    (1 <= len, (idx + len) <= w) =>
    IExp (BaseBVType w)
    -> NatRepr idx
    -> NatRepr len
    -> VerilogM sym n (IExp (BaseBVType len))
    bitSelect IExp (BaseBVType w)
    e NatRepr idx
    start NatRepr len
    len = Exp (BaseBVType len) -> VerilogM sym n (IExp (BaseBVType len))
    forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
    mkLet (IExp (BaseBVType w)
    -> NatRepr idx -> NatRepr len -> Exp (BaseBVType len)
    forall (w :: Natural) (start :: Natural) (w :: Natural).
    (1 <= w, (start + w) <= w) =>
    IExp (BaseBVType w)
    -> NatRepr start -> NatRepr w -> Exp (BaseBVType w)
    BitSelect IExp (BaseBVType w)
    e NatRepr idx
    start NatRepr len
    len)

    -- | Concatenate two bit vectors and bind the result to a new, returned
    -- name.
    concat2 ::
      (w ~ (w1 WT.+ w2), 1 <= w) =>
      WT.NatRepr w ->
      IExp (WT.BaseBVType w1) ->
      IExp (WT.BaseBVType w2) ->
      VerilogM sym n (IExp (WT.BaseBVType w))
    concat2 :: forall (w :: Natural) (w1 :: Natural) (w2 :: Natural) sym n.
    (w ~ (w1 + w2), 1 <= w) =>
    NatRepr w
    -> IExp (BaseBVType w1)
    -> IExp (BaseBVType w2)
    -> VerilogM sym n (IExp (BaseBVType w))
    concat2 NatRepr w
    w IExp (BaseBVType w1)
    e1 IExp (BaseBVType w2)
    e2 = Exp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
    forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
    mkLet (NatRepr w -> [Some IExp] -> Exp (BaseBVType w)
    forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> [Some IExp] -> Exp (BaseBVType w)
    Concat NatRepr w
    w [IExp (BaseBVType w1) -> Some IExp
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some IExp (BaseBVType w1)
    e1, IExp (BaseBVType w2) -> Some IExp
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some IExp (BaseBVType w2)
    e2])

    -- | A data type for items that may show up in a Verilog module.
    data Item where
      Input  :: WT.BaseTypeRepr tp -> Identifier -> Item
      Output :: WT.BaseTypeRepr tp -> Identifier -> Item
      Wire   :: WT.BaseTypeRepr tp -> Identifier -> Item
      Assign :: LHS -> Exp tp -> Item

    -- | Necessary monadic operations

    data ModuleState sym n =
        ModuleState { forall sym n.
    ModuleState sym n -> [(Word64, Some BaseTypeRepr, Identifier)]
    vsInputs :: [(Word64, Some WT.BaseTypeRepr, Identifier)]
                    -- ^ All module inputs, in reverse order. We use Word64 for Nonces to avoid GHC bugs.
                    -- For more detail:
                    --   https://gitlab.haskell.org/ghc/ghc/-/issues/2595
                    --   https://gitlab.haskell.org/ghc/ghc/-/issues/10856
                    --   https://gitlab.haskell.org/ghc/ghc/-/issues/16501
                    , forall sym n.
    ModuleState sym n
    -> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
    vsOutputs :: [(Some WT.BaseTypeRepr, Bool, Identifier, Some Exp)]
                    -- ^ All module outputs, in reverse order. Includes the
                    -- type, signedness, name, and initializer of each.
                    , forall sym n.
    ModuleState sym n
    -> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
    vsWires :: [(Some WT.BaseTypeRepr, Bool, Identifier, Some Exp)]
                    -- ^ All internal wires, in reverse order. Includes the
                    -- type, signedness, name, and initializer of each.
                    , forall sym n. ModuleState sym n -> Map Word64 Identifier
    vsSeenNonces :: Map.Map Word64 Identifier
                    -- ^ A map from the identifier nonces seen so far to
                    -- their identifier names. These nonces exist for
                    -- identifiers from the original term, but not
                    -- intermediate Verilog variables.
                    , forall sym n. ModuleState sym n -> Set Identifier
    vsUsedIdentifiers :: Set.Set Identifier
                    -- ^ A set of all the identifiers used so far, including
                    -- intermediate Verilog variables.
                    , forall sym n. ModuleState sym n -> IdxCache n IExp
    vsExpCache :: IdxCache n IExp
                    -- ^ An expression cache to preserve sharing present in
                    -- the What4 representation.
                    , forall sym n. ModuleState sym n -> Map BVConst Identifier
    vsBVCache :: Map.Map BVConst Identifier
                    -- ^ A cache of bit vector constants, to avoid duplicating constant declarations.
                    , forall sym n. ModuleState sym n -> Map Bool Identifier
    vsBoolCache :: Map.Map Bool Identifier
                    -- ^ A cache of Boolean constants, to avoid duplicating constant declarations.
                    , forall sym n. ModuleState sym n -> sym
    vsSym :: sym
                    -- ^ The What4 symbolic backend to use with `vsBVCache`.
                    }

    newtype VerilogM sym n a =
     VerilogM (StateT (ModuleState sym n) (ExceptT String IO) a)
     deriving ( (forall a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b)
    -> (forall a b. a -> VerilogM sym n b -> VerilogM sym n a)
    -> Functor (VerilogM sym n)
    forall a b. a -> VerilogM sym n b -> VerilogM sym n a
    forall a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b
    forall sym n a b. a -> VerilogM sym n b -> VerilogM sym n a
    forall sym n a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b
    forall (f :: Type -> Type).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall sym n a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b
    fmap :: forall a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b
    $c<$ :: forall sym n a b. a -> VerilogM sym n b -> VerilogM sym n a
    <$ :: forall a b. a -> VerilogM sym n b -> VerilogM sym n a
    Functor
              , Functor (VerilogM sym n)
    Functor (VerilogM sym n) =>
    (forall a. a -> VerilogM sym n a)
    -> (forall a b.
        VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b)
    -> (forall a b c.
        (a -> b -> c)
        -> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c)
    -> (forall a b.
        VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b)
    -> (forall a b.
        VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a)
    -> Applicative (VerilogM sym n)
    forall a. a -> VerilogM sym n a
    forall sym n. Functor (VerilogM sym n)
    forall a b.
    VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a
    forall a b.
    VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
    forall a b.
    VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
    forall sym n a. a -> VerilogM sym n a
    forall a b c.
    (a -> b -> c)
    -> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
    forall sym n a b.
    VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a
    forall sym n a b.
    VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
    forall sym n a b.
    VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
    forall sym n a b c.
    (a -> b -> c)
    -> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
    forall (f :: Type -> Type).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    $cpure :: forall sym n a. a -> VerilogM sym n a
    pure :: forall a. a -> VerilogM sym n a
    $c<*> :: forall sym n a b.
    VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
    <*> :: forall a b.
    VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
    $cliftA2 :: forall sym n a b c.
    (a -> b -> c)
    -> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
    liftA2 :: forall a b c.
    (a -> b -> c)
    -> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
    $c*> :: forall sym n a b.
    VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
    *> :: forall a b.
    VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
    $c<* :: forall sym n a b.
    VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a
    <* :: forall a b.
    VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a
    Applicative
              , Applicative (VerilogM sym n)
    Applicative (VerilogM sym n) =>
    (forall a b.
     VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b)
    -> (forall a b.
        VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b)
    -> (forall a. a -> VerilogM sym n a)
    -> Monad (VerilogM sym n)
    forall a. a -> VerilogM sym n a
    forall sym n. Applicative (VerilogM sym n)
    forall a b.
    VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
    forall a b.
    VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
    forall sym n a. a -> VerilogM sym n a
    forall sym n a b.
    VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
    forall sym n a b.
    VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
    forall (m :: Type -> Type).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    $c>>= :: forall sym n a b.
    VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
    >>= :: forall a b.
    VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
    $c>> :: forall sym n a b.
    VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
    >> :: forall a b.
    VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
    $creturn :: forall sym n a. a -> VerilogM sym n a
    return :: forall a. a -> VerilogM sym n a
    Monad
              , MonadState (ModuleState sym n)
              , MonadError String
              , Monad (VerilogM sym n)
    Monad (VerilogM sym n) =>
    (forall a. IO a -> VerilogM sym n a) -> MonadIO (VerilogM sym n)
    forall a. IO a -> VerilogM sym n a
    forall sym n. Monad (VerilogM sym n)
    forall sym n a. IO a -> VerilogM sym n a
    forall (m :: Type -> Type).
    Monad m =>
    (forall a. IO a -> m a) -> MonadIO m
    $cliftIO :: forall sym n a. IO a -> VerilogM sym n a
    liftIO :: forall a. IO a -> VerilogM sym n a
    MonadIO
              )

    newtype Module sym n = Module (ModuleState sym n)

    -- | Create a Verilog module in the context of a given What4 symbolic
    -- backend and a monadic computation that returns an expression name
    -- that corresponds to the module's output.
    mkModule ::
      sym ->
      [(Some (Expr n), T.Text)] ->
      [VerilogM sym n (Some IExp)] ->
      ExceptT String IO (Module sym n)
    mkModule :: forall sym n.
    sym
    -> [(Some (Expr n), Identifier)]
    -> [VerilogM sym n (Some IExp)]
    -> ExceptT String IO (Module sym n)
    mkModule sym
    sym [(Some (Expr n), Identifier)]
    ins [VerilogM sym n (Some IExp)]
    ops = (ModuleState sym n -> Module sym n)
    -> ExceptT String IO (ModuleState sym n)
    -> ExceptT String IO (Module sym n)
    forall a b. (a -> b) -> ExceptT String IO a -> ExceptT String IO b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap ModuleState sym n -> Module sym n
    forall sym n. ModuleState sym n -> Module sym n
    Module (ExceptT String IO (ModuleState sym n)
     -> ExceptT String IO (Module sym n))
    -> ExceptT String IO (ModuleState sym n)
    -> ExceptT String IO (Module sym n)
    forall a b. (a -> b) -> a -> b
    $ sym -> VerilogM sym n () -> ExceptT String IO (ModuleState sym n)
    forall sym n a.
    sym -> VerilogM sym n a -> ExceptT String IO (ModuleState sym n)
    execVerilogM sym
    sym (VerilogM sym n () -> ExceptT String IO (ModuleState sym n))
    -> VerilogM sym n () -> ExceptT String IO (ModuleState sym n)
    forall a b. (a -> b) -> a -> b
    $ do
        let addExprInput :: Some (Expr n) -> Identifier -> VerilogM sym n Identifier
    addExprInput Some (Expr n)
    e Identifier
    ident =
              case Some (Expr n)
    e of
                Some (BoundVarExpr ExprBoundVar n x
    x) -> ExprBoundVar n x -> Identifier -> VerilogM sym n Identifier
    forall n (tp :: BaseType) sym.
    ExprBoundVar n tp -> Identifier -> VerilogM sym n Identifier
    addBoundInput ExprBoundVar n x
    x Identifier
    ident
                Some (Expr n)
    _ -> String -> VerilogM sym n Identifier
    forall a. String -> VerilogM sym n a
    forall e (m :: Type -> Type) a. MonadError e m => e -> m a
    throwError String
    "Input provided to mkModule isn't an input"
        ((Some (Expr n), Identifier) -> VerilogM sym n Identifier)
    -> [(Some (Expr n), Identifier)] -> VerilogM sym n ()
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ ((Some (Expr n) -> Identifier -> VerilogM sym n Identifier)
    -> (Some (Expr n), Identifier) -> VerilogM sym n Identifier
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Some (Expr n) -> Identifier -> VerilogM sym n Identifier
    forall {n} {sym}.
    Some (Expr n) -> Identifier -> VerilogM sym n Identifier
    addExprInput) [(Some (Expr n), Identifier)]
    ins
        es <- [VerilogM sym n (Some IExp)] -> VerilogM sym n [Some IExp]
    forall (t :: Type -> Type) (m :: Type -> Type) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: Type -> Type) a. Monad m => [m a] -> m [a]
    sequence [VerilogM sym n (Some IExp)]
    ops
        forM_ es $ \Some IExp
    se ->
          do out <- Identifier -> VerilogM sym n Identifier
    forall sym n. Identifier -> VerilogM sym n Identifier
    freshIdentifier Identifier
    "out"
             viewSome (\IExp tp
    e -> BaseTypeRepr tp -> Identifier -> Exp tp -> VerilogM sym n ()
    forall (tp :: BaseType) sym n.
    BaseTypeRepr tp -> Identifier -> Exp tp -> VerilogM sym n ()
    addOutput (IExp tp -> BaseTypeRepr tp
    forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
    iexpType IExp tp
    e) Identifier
    out (IExp tp -> Exp tp
    forall (tp :: BaseType). IExp tp -> Exp tp
    IExp IExp tp
    e)) se

    initModuleState :: sym -> IO (ModuleState sym n)
    initModuleState :: forall sym n. sym -> IO (ModuleState sym n)
    initModuleState sym
    sym = do
      cache <- IO (IdxCache n IExp)
    forall (m :: Type -> Type) t (f :: BaseType -> Type).
    MonadIO m =>
    m (IdxCache t f)
    newIdxCache
      return $ ModuleState
               { vsInputs = []
               , vsOutputs = []
               , vsWires = []
               , vsSeenNonces = Map.empty
               , vsUsedIdentifiers = Set.empty
               , vsExpCache = cache
               , vsBVCache = Map.empty
               , vsBoolCache = Map.empty
               , vsSym = sym
               }

    runVerilogM ::
      VerilogM sym n a ->
      ModuleState sym n ->
      ExceptT String IO (a, ModuleState sym n)
    runVerilogM :: forall sym n a.
    VerilogM sym n a
    -> ModuleState sym n -> ExceptT String IO (a, ModuleState sym n)
    runVerilogM (VerilogM StateT (ModuleState sym n) (ExceptT String IO) a
    op) = StateT (ModuleState sym n) (ExceptT String IO) a
    -> ModuleState sym n -> ExceptT String IO (a, ModuleState sym n)
    forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
    runStateT StateT (ModuleState sym n) (ExceptT String IO) a
    op

    execVerilogM ::
      sym ->
      VerilogM sym n a ->
      ExceptT String IO (ModuleState sym n)
    execVerilogM :: forall sym n a.
    sym -> VerilogM sym n a -> ExceptT String IO (ModuleState sym n)
    execVerilogM sym
    sym VerilogM sym n a
    op =
      do s <- IO (ModuleState sym n) -> ExceptT String IO (ModuleState sym n)
    forall a. IO a -> ExceptT String IO a
    forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
    liftIO (IO (ModuleState sym n) -> ExceptT String IO (ModuleState sym n))
    -> IO (ModuleState sym n) -> ExceptT String IO (ModuleState sym n)
    forall a b. (a -> b) -> a -> b
    $ sym -> IO (ModuleState sym n)
    forall sym n. sym -> IO (ModuleState sym n)
    initModuleState sym
    sym
         (_a,m) <- runVerilogM op s
         return m

    addBoundInput ::
      ExprBoundVar n tp ->
      Identifier ->
      VerilogM sym n Identifier
    addBoundInput :: forall n (tp :: BaseType) sym.
    ExprBoundVar n tp -> Identifier -> VerilogM sym n Identifier
    addBoundInput ExprBoundVar n tp
    x Identifier
    ident =
      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 tp -> Some (Nonce n)
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some Nonce n tp
    idx) (BaseTypeRepr tp -> Some BaseTypeRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some BaseTypeRepr tp
    tp) Identifier
    ident
        where
          tp :: BaseTypeRepr tp
    tp = ExprBoundVar n tp -> BaseTypeRepr tp
    forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
    bvarType ExprBoundVar n tp
    x
          idx :: Nonce n tp
    idx = ExprBoundVar n tp -> Nonce n tp
    forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
    bvarId ExprBoundVar n tp
    x

    -- | Returns and records a fresh input with the given type and with a
    -- name constructed from the given base.
    addFreshInput ::
      Some (Nonce n) ->
      Some WT.BaseTypeRepr ->
      Identifier ->
      VerilogM sym n Identifier
    addFreshInput :: forall {k} n sym.
    Some (Nonce n)
    -> Some BaseTypeRepr -> Identifier -> VerilogM sym n Identifier
    addFreshInput Some (Nonce n)
    n Some BaseTypeRepr
    tp Identifier
    base = do
      seenNonces <- (ModuleState sym n -> Map Word64 Identifier)
    -> VerilogM sym n (Map Word64 Identifier)
    forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
    gets ModuleState sym n -> Map Word64 Identifier
    forall sym n. ModuleState sym n -> Map Word64 Identifier
    vsSeenNonces
      let idx = (forall (tp :: k). Nonce n tp -> Word64)
    -> Some (Nonce n) -> Word64
    forall {k} (f :: k -> Type) r.
    (forall (tp :: k). f tp -> r) -> Some f -> r
    viewSome Nonce n tp -> Word64
    forall (tp :: k). Nonce n tp -> Word64
    forall k s (tp :: k). Nonce s tp -> Word64
    indexValue Some (Nonce n)
    n
      case Map.lookup idx seenNonces of
        Just Identifier
    ident -> Identifier -> VerilogM sym n Identifier
    forall a. a -> VerilogM sym n a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Identifier
    ident
        Maybe Identifier
    Nothing ->
          do name <- Identifier -> VerilogM sym n Identifier
    forall sym n. Identifier -> VerilogM sym n Identifier
    freshIdentifier Identifier
    base
             modify $ \ModuleState sym n
    st -> ModuleState sym n
    st { vsInputs = (idx, tp, name) : vsInputs st
                                , vsSeenNonces = Map.insert idx name seenNonces
                                }
             return name

    -- | Add an output to the current Verilog module state, given a type, a
    -- name, and an initializer expression.
    addOutput ::
      WT.BaseTypeRepr tp ->
      Identifier ->
      Exp tp ->
      VerilogM sym n ()
    addOutput :: forall (tp :: BaseType) sym n.
    BaseTypeRepr tp -> Identifier -> Exp tp -> VerilogM sym n ()
    addOutput BaseTypeRepr tp
    tp Identifier
    name Exp tp
    e =
      (ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ()
    forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
    modify ((ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ())
    -> (ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ()
    forall a b. (a -> b) -> a -> b
    $ \ModuleState sym n
    st -> ModuleState sym n
    st { vsOutputs = (Some tp, False, name, Some e) : vsOutputs st }

    -- | Add a new wire to the current Verilog module state, given a type, a
    -- signedness flag, a name, and an initializer expression.
    addWire ::
      WT.BaseTypeRepr tp ->
      Bool ->
      Identifier ->
      Exp tp ->
      VerilogM sym n ()
    addWire :: forall (tp :: BaseType) sym n.
    BaseTypeRepr tp
    -> Bool -> Identifier -> Exp tp -> VerilogM sym n ()
    addWire BaseTypeRepr tp
    tp Bool
    isSigned Identifier
    name Exp tp
    e =
      (ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ()
    forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
    modify ((ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ())
    -> (ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ()
    forall a b. (a -> b) -> a -> b
    $ \ModuleState sym n
    st -> ModuleState sym n
    st { vsWires = (Some tp, isSigned, name, Some e) : vsWires st }

    -- | Create a fresh identifier by concatenating the given base with the
    -- current fresh identifier counter.
    freshIdentifier :: T.Text -> VerilogM sym n Identifier
    freshIdentifier :: forall sym n. Identifier -> VerilogM sym n Identifier
    freshIdentifier Identifier
    basename = do
      st <- VerilogM sym n (ModuleState sym n)
    forall s (m :: Type -> Type). MonadState s m => m s
    get
      let used = ModuleState sym n -> Set Identifier
    forall sym n. ModuleState sym n -> Set Identifier
    vsUsedIdentifiers ModuleState sym n
    st
      let nm | Identifier
    basename Identifier -> Set Identifier -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Identifier
    used =
                 [Identifier] -> Identifier
    T.concat [Identifier
    basename, Identifier
    "_", String -> Identifier
    forall a. IsString a => String -> a
    fromString (String -> Identifier) -> String -> Identifier
    forall a b. (a -> b) -> a -> b
    $ Int -> String
    forall a. Show a => a -> String
    show (Int -> String) -> Int -> String
    forall a b. (a -> b) -> a -> b
    $ Set Identifier -> Int
    forall a. Set a -> Int
    Set.size Set Identifier
    used ]
             | Bool
    otherwise = Identifier
    basename
      put $ st { vsUsedIdentifiers = Set.insert nm used }
      return nm

    -- | Add a new wire to the current Verilog module state, given a type, a
    -- signedness flag, the prefix of a name, and an initializer expression.
    -- The name prefix will be freshened by appending current value of the
    -- fresh variable counter.
    addFreshWire ::
      WT.BaseTypeRepr tp ->
      Bool ->
      T.Text ->
      Exp tp ->
      VerilogM sym n Identifier
    addFreshWire :: forall (tp :: BaseType) sym n.
    BaseTypeRepr tp
    -> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
    addFreshWire BaseTypeRepr tp
    repr Bool
    isSigned Identifier
    basename Exp tp
    e = do
      x <- Identifier -> VerilogM sym n Identifier
    forall sym n. Identifier -> VerilogM sym n Identifier
    freshIdentifier Identifier
    basename
      addWire repr isSigned x e
      return x