    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE ViewPatterns #-}
    {-
    Module           : What4.Protocol.VerilogWriter.Export.ABCVerilog
    Copyright        : (c) Galois, Inc 2020
    Maintainer       : Aaron Tomb <atomb@galois.com>
    License          : BSD3

    Export Verilog in the particular syntax ABC supports.
    -}

    module What4.Protocol.VerilogWriter.ABCVerilog where

    import Data.BitVector.Sized
    import Data.Parameterized.NatRepr
    import Data.Parameterized.Some
    import Data.String
    import qualified Data.Text as T
    import Data.Word
    import Prettyprinter
    import What4.BaseTypes
    import What4.Protocol.VerilogWriter.AST
    import Numeric (showHex)
    import Prelude hiding ((<$>))

    moduleDoc :: Module sym n -> Doc () -> Doc ()
    moduleDoc :: forall sym n. Module sym n -> Doc () -> Doc ()
    moduleDoc (Module ModuleState sym n
    ms) Doc ()
    name =
      [Doc ()] -> Doc ()
    forall ann. [Doc ann] -> Doc ann
    vsep
        [ Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    nest Int
    2 (Doc () -> Doc ()) -> Doc () -> Doc ()
    forall a b. (a -> b) -> a -> b
    $ [Doc ()] -> Doc ()
    forall ann. [Doc ann] -> Doc ann
    vsep
          [ Doc ()
    "module" Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Doc ()
    name Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> [Doc ()] -> Doc ()
    forall ann. [Doc ann] -> Doc ann
    tupled [Doc ()]
    params Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    forall ann. Doc ann
    semi
          , [Doc ()] -> Doc ()
    forall ann. [Doc ann] -> Doc ann
    vsep (((Word64, Some BaseTypeRepr, Text) -> Doc ())
    -> [(Word64, Some BaseTypeRepr, Text)] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map (Word64, Some BaseTypeRepr, Text) -> Doc ()
    inputDoc ([(Word64, Some BaseTypeRepr, Text)]
    -> [(Word64, Some BaseTypeRepr, Text)]
    forall a. [a] -> [a]
    reverse (ModuleState sym n -> [(Word64, Some BaseTypeRepr, Text)]
    forall sym n.
    ModuleState sym n -> [(Word64, Some BaseTypeRepr, Text)]
    vsInputs ModuleState sym n
    ms)))
          , [Doc ()] -> Doc ()
    forall ann. [Doc ann] -> Doc ann
    vsep (((Some BaseTypeRepr, Bool, Text, Some Exp) -> Doc ())
    -> [(Some BaseTypeRepr, Bool, Text, Some Exp)] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc () -> (Some BaseTypeRepr, Bool, Text, Some Exp) -> Doc ()
    wireDoc Doc ()
    "wire") ([(Some BaseTypeRepr, Bool, Text, Some Exp)]
    -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
    forall a. [a] -> [a]
    reverse (ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
    forall sym n.
    ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
    vsWires ModuleState sym n
    ms)))
          , [Doc ()] -> Doc ()
    forall ann. [Doc ann] -> Doc ann
    vsep (((Some BaseTypeRepr, Bool, Text, Some Exp) -> Doc ())
    -> [(Some BaseTypeRepr, Bool, Text, Some Exp)] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc () -> (Some BaseTypeRepr, Bool, Text, Some Exp) -> Doc ()
    wireDoc Doc ()
    "output") ([(Some BaseTypeRepr, Bool, Text, Some Exp)]
    -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
    forall a. [a] -> [a]
    reverse (ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
    forall sym n.
    ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
    vsOutputs ModuleState sym n
    ms)))
          ]
        , Doc ()
    "endmodule"
        ]
      where
        inputNames :: [Doc ()]
    inputNames = ((Word64, Some BaseTypeRepr, Text) -> Doc ())
    -> [(Word64, Some BaseTypeRepr, Text)] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map (Text -> Doc ()
    identDoc (Text -> Doc ())
    -> ((Word64, Some BaseTypeRepr, Text) -> Text)
    -> (Word64, Some BaseTypeRepr, Text)
    -> Doc ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (\(Word64
    _, Some BaseTypeRepr
    _, Text
    n) -> Text
    n)) (ModuleState sym n -> [(Word64, Some BaseTypeRepr, Text)]
    forall sym n.
    ModuleState sym n -> [(Word64, Some BaseTypeRepr, Text)]
    vsInputs ModuleState sym n
    ms)
        outputNames :: [Doc ()]
    outputNames = ((Some BaseTypeRepr, Bool, Text, Some Exp) -> Doc ())
    -> [(Some BaseTypeRepr, Bool, Text, Some Exp)] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map (Text -> Doc ()
    identDoc (Text -> Doc ())
    -> ((Some BaseTypeRepr, Bool, Text, Some Exp) -> Text)
    -> (Some BaseTypeRepr, Bool, Text, Some Exp)
    -> Doc ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (\(Some BaseTypeRepr
    _, Bool
    _, Text
    n, Some Exp
    _) -> Text
    n)) (ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
    forall sym n.
    ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
    vsOutputs ModuleState sym n
    ms)
        params :: [Doc ()]
    params = [Doc ()] -> [Doc ()]
    forall a. [a] -> [a]
    reverse [Doc ()]
    inputNames [Doc ()] -> [Doc ()] -> [Doc ()]
    forall a. [a] -> [a] -> [a]
    ++ [Doc ()] -> [Doc ()]
    forall a. [a] -> [a]
    reverse [Doc ()]
    outputNames

    typeDoc :: Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
    typeDoc :: forall (tp :: BaseType).
    Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
    typeDoc Doc ()
    ty Bool
    _ BaseTypeRepr tp
    BaseBoolRepr = Doc ()
    ty
    typeDoc Doc ()
    ty Bool
    isSigned (BaseBVRepr NatRepr w
    w) =
      Doc ()
    ty Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+>
      (if Bool
    isSigned then Doc ()
    "signed " else Doc ()
    forall a. Monoid a => a
    mempty) Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <>
      Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    brackets (Integer -> Doc ()
    forall ann. Integer -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue NatRepr w
    w Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    ":0")
    typeDoc Doc ()
    _ Bool
    _ BaseTypeRepr tp
    _ = Doc ()
    "<type error>"

    identDoc :: Identifier -> Doc ()
    identDoc :: Text -> Doc ()
    identDoc = Text -> Doc ()
    forall ann. Text -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Text -> Doc ()) -> (Text -> Text) -> Text -> Doc ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HasCallStack => Text -> Text -> Text -> Text
    Text -> Text -> Text -> Text
    T.replace Text
    "!" Text
    "_"

    lhsDoc :: LHS -> Doc ()
    lhsDoc :: LHS -> Doc ()
    lhsDoc (LHS Text
    name) = Text -> Doc ()
    identDoc Text
    name
    lhsDoc (LHSBit Text
    name Integer
    idx) =
      Text -> Doc ()
    identDoc Text
    name Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    brackets (Integer -> Doc ()
    forall ann. Integer -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty Integer
    idx)

    inputDoc :: (Word64, Some BaseTypeRepr, Identifier) -> Doc ()
    inputDoc :: (Word64, Some BaseTypeRepr, Text) -> Doc ()
    inputDoc (Word64
    _, Some BaseTypeRepr
    tp, Text
    name) =
      (forall (tp :: BaseType). BaseTypeRepr tp -> Doc ())
    -> Some BaseTypeRepr -> Doc ()
    forall {k} (f :: k -> Type) r.
    (forall (tp :: k). f tp -> r) -> Some f -> r
    viewSome (Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
    forall (tp :: BaseType).
    Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
    typeDoc Doc ()
    "input" Bool
    False) Some BaseTypeRepr
    tp Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Text -> Doc ()
    identDoc Text
    name Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    forall ann. Doc ann
    semi

    wireDoc :: Doc () -> (Some BaseTypeRepr, Bool, Identifier, Some Exp) -> Doc ()
    wireDoc :: Doc () -> (Some BaseTypeRepr, Bool, Text, Some Exp) -> Doc ()
    wireDoc Doc ()
    ty (Some BaseTypeRepr
    tp, Bool
    isSigned, Text
    name, Some Exp
    e) =
      (forall (tp :: BaseType). BaseTypeRepr tp -> Doc ())
    -> Some BaseTypeRepr -> Doc ()
    forall {k} (f :: k -> Type) r.
    (forall (tp :: k). f tp -> r) -> Some f -> r
    viewSome (Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
    forall (tp :: BaseType).
    Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
    typeDoc Doc ()
    ty Bool
    isSigned) Some BaseTypeRepr
    tp Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+>
      Text -> Doc ()
    identDoc Text
    name Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+>
      Doc ()
    forall ann. Doc ann
    equals Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+>
      (forall (tp :: BaseType). Exp tp -> Doc ()) -> Some Exp -> Doc ()
    forall {k} (f :: k -> Type) r.
    (forall (tp :: k). f tp -> r) -> Some f -> r
    viewSome Exp tp -> Doc ()
    forall (tp :: BaseType). Exp tp -> Doc ()
    expDoc Some Exp
    e Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <>
      Doc ()
    forall ann. Doc ann
    semi

    unopDoc :: Unop tp -> Doc ()
    unopDoc :: forall (tp :: BaseType). Unop tp -> Doc ()
    unopDoc Unop tp
    Not   = Doc ()
    "!"
    unopDoc Unop tp
    BVNot = Doc ()
    "~"

    binopDoc :: Binop inTp outTp -> Doc ()
    binopDoc :: forall (inTp :: BaseType) (outTp :: BaseType).
    Binop inTp outTp -> Doc ()
    binopDoc Binop inTp outTp
    And      = Doc ()
    "&&"
    binopDoc Binop inTp outTp
    Or       = Doc ()
    "||"
    binopDoc Binop inTp outTp
    Xor      = Doc ()
    "^^"
    binopDoc Binop inTp outTp
    BVAnd    = Doc ()
    "&"
    binopDoc Binop inTp outTp
    BVOr     = Doc ()
    "|"
    binopDoc Binop inTp outTp
    BVXor    = Doc ()
    "^"
    binopDoc Binop inTp outTp
    BVAdd    = Doc ()
    "+"
    binopDoc Binop inTp outTp
    BVSub    = Doc ()
    "-"
    binopDoc Binop inTp outTp
    BVMul    = Doc ()
    "*"
    binopDoc Binop inTp outTp
    BVDiv    = Doc ()
    "/"
    binopDoc Binop inTp outTp
    BVRem    = Doc ()
    "%"
    binopDoc Binop inTp outTp
    BVPow    = Doc ()
    "**"
    binopDoc Binop inTp outTp
    BVShiftL = Doc ()
    "<<"
    binopDoc Binop inTp outTp
    BVShiftR = Doc ()
    ">>"
    binopDoc Binop inTp outTp
    BVShiftRA = Doc ()
    ">>>"
    binopDoc Binop inTp outTp
    Eq       = Doc ()
    "=="
    binopDoc Binop inTp outTp
    Ne       = Doc ()
    "!="
    binopDoc Binop inTp outTp
    Lt       = Doc ()
    "<"
    binopDoc Binop inTp outTp
    Le       = Doc ()
    "<="

    -- | Show non-negative Integral numbers in base 16.
    hexDoc :: BV w -> Doc ()
    hexDoc :: forall (w :: Natural). BV w -> Doc ()
    hexDoc BV w
    n = String -> Doc ()
    forall a. IsString a => String -> a
    fromString (String -> Doc ()) -> String -> Doc ()
    forall a b. (a -> b) -> a -> b
    $ Integer -> ShowS
    forall a. Integral a => a -> ShowS
    showHex (BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    asUnsigned BV w
    n) String
    ""

    decDoc :: NatRepr w -> BV w -> Doc ()
    decDoc :: forall (w :: Natural). NatRepr w -> BV w -> Doc ()
    decDoc NatRepr w
    w BV w
    n = String -> Doc ()
    forall a. IsString a => String -> a
    fromString (String -> Doc ()) -> String -> Doc ()
    forall a b. (a -> b) -> a -> b
    $ NatRepr w -> BV w -> String
    forall (w :: Natural). NatRepr w -> BV w -> String
    ppDec NatRepr w
    w BV w
    n

    iexpDoc :: IExp tp -> Doc ()
    iexpDoc :: forall (tp :: BaseType). IExp tp -> Doc ()
    iexpDoc (Ident BaseTypeRepr tp
    _ Text
    name) = Text -> Doc ()
    identDoc Text
    name

    -- NB: special pretty-printer because ABC has a hack to detect this specific syntax
    rotateDoc :: String -> String -> NatRepr w -> IExp tp -> BV w -> Doc ()
    rotateDoc :: forall (w :: Natural) (tp :: BaseType).
    String -> String -> NatRepr w -> IExp tp -> BV w -> Doc ()
    rotateDoc String
    op1 String
    op2 (NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue -> Integer
    w) IExp tp
    e (BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    asUnsigned -> Integer
    n) =
      Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    parens (Doc ()
    v Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> String -> Doc ()
    forall a. IsString a => String -> a
    fromString String
    op1 Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Integer -> Doc ()
    forall ann. Integer -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty Integer
    n) Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Doc ()
    "|" Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+>
      Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    parens (Doc ()
    v Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> String -> Doc ()
    forall a. IsString a => String -> a
    fromString String
    op2 Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Integer -> Doc ()
    forall ann. Integer -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Integer
    w Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    n))
        where v :: Doc ()
    v = IExp tp -> Doc ()
    forall (tp :: BaseType). IExp tp -> Doc ()
    iexpDoc IExp tp
    e

    expDoc :: Exp tp -> Doc ()
    expDoc :: forall (tp :: BaseType). Exp tp -> Doc ()
    expDoc (IExp IExp tp
    e) = IExp tp -> Doc ()
    forall (tp :: BaseType). IExp tp -> Doc ()
    iexpDoc IExp tp
    e
    expDoc (Binop Binop inTp tp
    op IExp inTp
    l IExp inTp
    r) = IExp inTp -> Doc ()
    forall (tp :: BaseType). IExp tp -> Doc ()
    iexpDoc IExp inTp
    l Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Binop inTp tp -> Doc ()
    forall (inTp :: BaseType) (outTp :: BaseType).
    Binop inTp outTp -> Doc ()
    binopDoc Binop inTp tp
    op Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> IExp inTp -> Doc ()
    forall (tp :: BaseType). IExp tp -> Doc ()
    iexpDoc IExp inTp
    r
    expDoc (Unop Unop tp
    op IExp tp
    e) = Unop tp -> Doc ()
    forall (tp :: BaseType). Unop tp -> Doc ()
    unopDoc Unop tp
    op Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> IExp tp -> Doc ()
    forall (tp :: BaseType). IExp tp -> Doc ()
    iexpDoc IExp tp
    e
    expDoc (BVRotateL NatRepr w
    wr IExp tp
    e BV w
    n) = String -> String -> NatRepr w -> IExp tp -> BV w -> Doc ()
    forall (w :: Natural) (tp :: BaseType).
    String -> String -> NatRepr w -> IExp tp -> BV w -> Doc ()
    rotateDoc String
    "<<" String
    ">>" NatRepr w
    wr IExp tp
    e BV w
    n
    expDoc (BVRotateR NatRepr w
    wr IExp tp
    e BV w
    n) = String -> String -> NatRepr w -> IExp tp -> BV w -> Doc ()
    forall (w :: Natural) (tp :: BaseType).
    String -> String -> NatRepr w -> IExp tp -> BV w -> Doc ()
    rotateDoc String
    ">>" String
    "<<" NatRepr w
    wr IExp tp
    e BV w
    n
    expDoc (Mux IExp 'BaseBoolType
    c IExp tp
    t IExp tp
    e) = IExp 'BaseBoolType -> Doc ()
    forall (tp :: BaseType). IExp tp -> Doc ()
    iexpDoc IExp 'BaseBoolType
    c Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Doc ()
    "?" Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> IExp tp -> Doc ()
    forall (tp :: BaseType). IExp tp -> Doc ()
    iexpDoc IExp tp
    t Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> Doc ()
    forall ann. Doc ann
    colon Doc () -> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann
    <+> IExp tp -> Doc ()
    forall (tp :: BaseType). IExp tp -> Doc ()
    iexpDoc IExp tp
    e
    expDoc (Bit IExp (BaseBVType w)
    e Integer
    i) =
      IExp (BaseBVType w) -> Doc ()
    forall (tp :: BaseType). IExp tp -> Doc ()
    iexpDoc IExp (BaseBVType w)
    e Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    brackets (Integer -> Doc ()
    forall ann. Integer -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty Integer
    i)
    expDoc (BitSelect IExp (BaseBVType w)
    e (NatRepr start -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue -> Integer
    start) (NatRepr len -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue -> Integer
    len)) =
      IExp (BaseBVType w) -> Doc ()
    forall (tp :: BaseType). IExp tp -> Doc ()
    iexpDoc IExp (BaseBVType w)
    e Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    brackets (Integer -> Doc ()
    forall ann. Integer -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Integer
    start Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + (Integer
    len Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1)) Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    forall ann. Doc ann
    colon Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Integer -> Doc ()
    forall ann. Integer -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty Integer
    start)
    expDoc (Concat NatRepr w
    _ [Some IExp]
    es) = Doc () -> Doc () -> Doc () -> [Doc ()] -> Doc ()
    forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
    encloseSep Doc ()
    forall ann. Doc ann
    lbrace Doc ()
    forall ann. Doc ann
    rbrace Doc ()
    forall ann. Doc ann
    comma ((Some IExp -> Doc ()) -> [Some IExp] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map ((forall (tp :: BaseType). IExp tp -> Doc ()) -> Some IExp -> Doc ()
    forall {k} (f :: k -> Type) r.
    (forall (tp :: k). f tp -> r) -> Some f -> r
    viewSome IExp tp -> Doc ()
    forall (tp :: BaseType). IExp tp -> Doc ()
    iexpDoc) [Some IExp]
    es)
    expDoc (BVLit NatRepr w
    w BV w
    n) = Integer -> Doc ()
    forall ann. Integer -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (NatRepr w -> Integer
    forall (n :: Natural). NatRepr n -> Integer
    intValue NatRepr w
    w) Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "'h" Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> BV w -> Doc ()
    forall (w :: Natural). BV w -> Doc ()
    hexDoc BV w
    n
    expDoc (BoolLit Bool
    True) = Doc ()
    "1'b1"
    expDoc (BoolLit Bool
    False) = Doc ()
    "1'b0"