{-
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.State (get)
import           Control.Monad.Except
import qualified Data.BitVector.Sized as BV
import           Data.List.NonEmpty ( NonEmpty(..) )

import           Data.Parameterized.Context
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 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 :: String -> m a
doNotSupportError String
cstr = 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 :: Expr n tp -> VerilogM sym n (IExp tp)
exprToVerilogExpr Expr n tp
e = do
  IdxCache n IExp
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)) -> VerilogM sym n (IExp tp)
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)
  (Expr n tp -> VerilogM sym n (IExp tp)) -> VerilogM sym n (IExp tp)
cacheEval ((Expr n tp -> VerilogM sym n (IExp tp))
 -> VerilogM sym n (IExp tp))
-> (Expr n tp -> VerilogM sym n (IExp tp))
-> VerilogM sym n (IExp tp)
forall a b. (a -> b) -> a -> b
$
    \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 :: Nat) 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 String
name <- BaseTypeRepr tp -> String -> VerilogM sym n String
forall (tp :: BaseType) sym n.
BaseTypeRepr tp -> String -> VerilogM sym n String
addFreshInput BaseTypeRepr tp
tp String
base
           IExp tp -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (IExp tp -> VerilogM sym n (IExp tp))
-> IExp tp -> VerilogM sym n (IExp tp)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr tp -> String -> IExp tp
forall (tp :: BaseType). BaseTypeRepr tp -> String -> IExp tp
Ident BaseTypeRepr tp
tp String
name
        where
          tp :: BaseTypeRepr tp
tp = ExprBoundVar n tp -> BaseTypeRepr tp
forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
bvarType ExprBoundVar n tp
x
          base :: String
base = ExprBoundVar n tp -> String
forall t (tp :: BaseType). ExprBoundVar t tp -> String
bvarIdentifier ExprBoundVar n tp
x

bvarIdentifier :: ExprBoundVar t tp -> Identifier
bvarIdentifier :: ExprBoundVar t tp -> String
bvarIdentifier ExprBoundVar t tp
x = SolverSymbol -> String
forall a. Show a => a -> String
show (ExprBoundVar t tp -> SolverSymbol
forall t (tp :: BaseType). ExprBoundVar t tp -> SolverSymbol
bvarName ExprBoundVar t tp
x)

nonceAppExprVerilogExpr ::
  (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
  NonceAppExpr n tp ->
  VerilogM sym n (IExp tp)
nonceAppExprVerilogExpr :: 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 tp
_ 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 tp
_ 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
      String
name <- BaseTypeRepr tp -> String -> VerilogM sym n String
forall (tp :: BaseType) sym n.
BaseTypeRepr tp -> String -> VerilogM sym n String
addFreshInput BaseTypeRepr tp
tp String
base
      IExp tp -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (IExp tp -> VerilogM sym n (IExp tp))
-> IExp tp -> VerilogM sym n (IExp tp)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr tp -> String -> IExp tp
forall (tp :: BaseType). BaseTypeRepr tp -> String -> IExp tp
Ident BaseTypeRepr tp
tp String
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
          base :: String
base = SolverSymbol -> String
forall a. Show a => a -> String
show (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 :: 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.
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
(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
      IExp BaseBoolType
t' <- (Expr n BaseBoolType, Polarity)
-> VerilogM sym n (IExp BaseBoolType)
forall sym n.
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
(Expr n BaseBoolType, Polarity)
-> VerilogM sym n (IExp BaseBoolType)
pol (Expr n BaseBoolType, Polarity)
t
      [IExp BaseBoolType]
ts' <- ((Expr n BaseBoolType, Polarity)
 -> VerilogM sym n (IExp BaseBoolType))
-> [(Expr n BaseBoolType, Polarity)]
-> VerilogM sym n [IExp BaseBoolType]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Expr n BaseBoolType, Polarity)
-> VerilogM sym n (IExp BaseBoolType)
forall sym n.
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
(Expr n BaseBoolType, Polarity)
-> VerilogM sym n (IExp BaseBoolType)
pol [(Expr n BaseBoolType, Polarity)]
ts
      (IExp BaseBoolType
 -> IExp BaseBoolType -> VerilogM sym n (IExp BaseBoolType))
-> IExp BaseBoolType
-> [IExp BaseBoolType]
-> VerilogM sym n (IExp BaseBoolType)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Binop BaseBoolType BaseBoolType
-> IExp BaseBoolType
-> IExp BaseBoolType
-> VerilogM sym n (IExp BaseBoolType)
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop BaseBoolType BaseBoolType
op) IExp BaseBoolType
t' [IExp BaseBoolType]
ts'

leqSubPos :: (1 <= m, 1 <= n, n+1 <= m) => NatRepr m -> NatRepr n -> LeqProof 1 (m - n)
leqSubPos :: 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 :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
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 :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
f m -> g n -> ((m + n) - n) :~: m
plusMinusCancel NatRepr 1
one NatRepr n
nr) of
    ((n + 1) :~: (1 + n)
Refl, ((1 + n) - n) :~: 1
Refl) ->
      LeqProof (n + 1) m
-> LeqProof n n -> LeqProof ((n + 1) - n) (m - n)
forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
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 :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (NatRepr n
nr NatRepr n -> NatRepr 1 -> NatRepr (n + 1)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
`addNat` NatRepr 1
one) NatRepr m
mr) (NatRepr n -> NatRepr n -> LeqProof n n
forall (m :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> 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 :: Nat). KnownNat n => NatRepr n
knownNat :: NatRepr 1

leqSuccLeft :: (n + 1 <= m) => p m -> NatRepr n -> LeqProof n m
leqSuccLeft :: 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 :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
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 :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
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 :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans (NatRepr n -> NatRepr 1 -> LeqProof n (n + 1)
forall (f :: Nat -> Type) (n :: Nat) (g :: Nat -> Type) (m :: Nat).
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 :: Nat) (n :: Nat) (f :: Nat -> Type) (g :: Nat -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (NatRepr n
nr NatRepr n -> NatRepr 1 -> NatRepr (n + 1)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
`addNat` NatRepr 1
one) p m
mr)
  where one :: NatRepr 1
one = NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat :: NatRepr 1

appExprVerilogExpr ::
  (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
  AppExpr n tp ->
  VerilogM sym n (IExp tp)
appExprVerilogExpr :: 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 :: 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
      IExp BaseBoolType
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
      IExp tp
etrue' <- 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
etrue
      IExp tp
efalse' <- 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
efalse
      IExp BaseBoolType -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
forall (tp :: BaseType) sym n.
IExp BaseBoolType -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
mux IExp BaseBoolType
b' IExp tp
etrue' IExp tp
efalse'
    BaseEq BaseTypeRepr tp
_ Expr n tp
e1 Expr n tp
e2 -> do
      IExp tp
e1' <- 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
e1
      IExp tp
e2' <- 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
e2
      Binop tp BaseBoolType
-> IExp tp -> IExp tp -> VerilogM sym n (IExp BaseBoolType)
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop tp BaseBoolType
forall (tp :: BaseType). Binop tp BaseBoolType
Eq IExp tp
e1' IExp tp
e2'

    -- Boolean operations
    NotPred Expr n BaseBoolType
e -> do
      IExp BaseBoolType
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 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
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 :: Nat) 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 :: Nat). 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 (BaseBVType w)
 -> IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w)))
-> (Coefficient sr
    -> Expr n (SemiRingBase sr)
    -> VerilogM sym n (IExp (BaseBVType w)))
-> (Coefficient sr -> VerilogM sym n (IExp (BaseBVType w)))
-> WeightedSum (Expr n) sr
-> VerilogM sym n (IExp (BaseBVType w))
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 (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 :: Nat). 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 (BaseBVType w))
scalMult' (NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
forall (w :: Nat) 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 :: Nat) 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 :: Nat). 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 (BaseBVType w)
 -> IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w)))
-> (Coefficient sr
    -> Expr n (SemiRingBase sr)
    -> VerilogM sym n (IExp (BaseBVType w)))
-> (Coefficient sr -> VerilogM sym n (IExp (BaseBVType w)))
-> WeightedSum (Expr n) sr
-> VerilogM sym n (IExp (BaseBVType w))
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 (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 :: Nat). 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 (BaseBVType w))
scalMult' (NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
forall (w :: Nat) 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 :: Nat). Binop (BaseBVType w) (BaseBVType w)
BVMul) 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 (BaseBVType w)))
-> VerilogM sym n (IExp (BaseBVType w))
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 :: Nat) 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 :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
1)
          Just IExp (BaseBVType w)
e  -> IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return 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 :: Nat). Binop (BaseBVType w) (BaseBVType w)
BVAnd) 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 (BaseBVType w)))
-> VerilogM sym n (IExp (BaseBVType w))
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 :: Nat) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
w (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w)
          Just IExp (BaseBVType w)
e  -> IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return 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
    App (Expr n) tp
Pi -> String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"real numbers"

    RealSin Expr n BaseRealType
_ -> String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"real numbers"
    RealCos Expr n BaseRealType
_ -> String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"real numbers"
    RealATan2 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"
    RealSinh Expr n BaseRealType
_ -> String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"real numbers"
    RealCosh Expr n BaseRealType
_ -> String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"real numbers"

    RealExp Expr n BaseRealType
_ -> String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"real numbers"
    RealLog Expr n BaseRealType
_ -> 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 IExp (BaseBVType w)
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
                        IExp (BaseBVType w)
-> Integer -> VerilogM sym n (IExp BaseBoolType)
forall (w :: Nat) sym n.
IExp (BaseBVType w)
-> Integer -> VerilogM sym n (IExp BaseBoolType)
bit IExp (BaseBVType w)
v (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i)
    BVSlt Expr n (BaseBVType w)
e1 Expr n (BaseBVType w)
e2 ->
      do IExp (BaseBVType w)
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
         IExp (BaseBVType w)
e2' <- 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)
e2
         Binop (BaseBVType w) BaseBoolType
-> IExp (BaseBVType w)
-> IExp (BaseBVType w)
-> VerilogM sym n (IExp BaseBoolType)
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop (BaseBVType w) BaseBoolType
forall (w :: Nat). Binop (BaseBVType w) BaseBoolType
Lt IExp (BaseBVType w)
e1' IExp (BaseBVType w)
e2'
    BVUlt Expr n (BaseBVType w)
e1 Expr n (BaseBVType w)
e2 ->
      do IExp (BaseBVType w)
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
         IExp (BaseBVType w)
e2' <- 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)
e2
         Binop (BaseBVType w) BaseBoolType
-> IExp (BaseBVType w)
-> IExp (BaseBVType w)
-> VerilogM sym n (IExp BaseBoolType)
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop (BaseBVType w) BaseBoolType
forall (w :: Nat). Binop (BaseBVType w) BaseBoolType
Lt IExp (BaseBVType w)
e1' IExp (BaseBVType w)
e2'

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

    BVConcat NatRepr (u + v)
size12 Expr n (BaseBVType u)
e1 Expr n (BaseBVType v)
e2 -> do IExp (BaseBVType u)
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
                                IExp (BaseBVType v)
e2' <- Expr n (BaseBVType v) -> VerilogM sym n (IExp (BaseBVType v))
forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
Expr n tp -> VerilogM sym n (IExp tp)
exprToVerilogExpr Expr n (BaseBVType v)
e2
                                NatRepr (u + v)
-> IExp (BaseBVType u)
-> IExp (BaseBVType v)
-> VerilogM sym n (IExp (BaseBVType (u + v)))
forall (w :: Nat) (w1 :: Nat) (w2 :: Nat) sym n.
(w ~ (w1 + w2), 1 <= w) =>
NatRepr w
-> IExp (BaseBVType w1)
-> IExp (BaseBVType w2)
-> VerilogM sym n (IExp (BaseBVType w))
concat2 NatRepr (u + v)
size12 IExp (BaseBVType u)
e1' IExp (BaseBVType v)
e2'
    BVSelect NatRepr idx
start NatRepr n
len Expr n (BaseBVType w)
bv -> do IExp (BaseBVType w)
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
                                IExp (BaseBVType w)
-> NatRepr idx -> NatRepr n -> VerilogM sym n (IExp (BaseBVType n))
forall (len :: Nat) (idx :: Nat) (w :: Nat) 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 n
len
    BVFill NatRepr w
len Expr n BaseBoolType
b -> do IExp BaseBoolType
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
                       IExp (BaseBVType w)
e1 <- NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
forall (w :: Nat) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
len (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
len)
                       IExp (BaseBVType w)
e2 <- NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
forall (w :: Nat) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
len (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
len)
                       IExp BaseBoolType
-> IExp (BaseBVType w)
-> IExp (BaseBVType w)
-> VerilogM sym n (IExp (BaseBVType w))
forall (tp :: BaseType) sym n.
IExp BaseBoolType -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
mux IExp BaseBoolType
e IExp (BaseBVType w)
e1 IExp (BaseBVType w)
e2
    BVUdiv NatRepr w
_   Expr n (BaseBVType w)
bv1 Expr n (BaseBVType w)
bv2 ->
      do IExp (BaseBVType w)
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
         IExp (BaseBVType w)
bv2' <- 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)
bv2
         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 :: Nat). Binop (BaseBVType w) (BaseBVType w)
BVDiv IExp (BaseBVType w)
bv1' IExp (BaseBVType w)
bv2'
    BVUrem NatRepr w
_   Expr n (BaseBVType w)
bv1 Expr n (BaseBVType w)
bv2 ->
      do IExp (BaseBVType w)
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
         IExp (BaseBVType w)
bv2' <- 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)
bv2
         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 :: Nat). Binop (BaseBVType w) (BaseBVType w)
BVRem IExp (BaseBVType w)
bv1' IExp (BaseBVType w)
bv2'
    BVSdiv NatRepr w
_   Expr n (BaseBVType w)
bv1 Expr n (BaseBVType w)
bv2 ->
      do IExp (BaseBVType w)
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
         IExp (BaseBVType w)
bv2' <- 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)
bv2
         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 :: Nat). Binop (BaseBVType w) (BaseBVType w)
BVDiv IExp (BaseBVType w)
bv1' IExp (BaseBVType w)
bv2'
    BVSrem NatRepr w
_   Expr n (BaseBVType w)
bv1 Expr n (BaseBVType w)
bv2 ->
      do IExp (BaseBVType w)
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
         IExp (BaseBVType w)
bv2' <- 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)
bv2
         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 :: Nat). Binop (BaseBVType w) (BaseBVType w)
BVRem IExp (BaseBVType w)
bv1' IExp (BaseBVType w)
bv2'
    BVShl  NatRepr w
_   Expr n (BaseBVType w)
bv1 Expr n (BaseBVType w)
bv2 -> do IExp (BaseBVType w)
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
                             IExp (BaseBVType w)
e2 <- 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)
bv2
                             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 :: Nat). Binop (BaseBVType w) (BaseBVType w)
BVShiftL IExp (BaseBVType w)
e1 IExp (BaseBVType w)
e2
    BVLshr NatRepr w
_   Expr n (BaseBVType w)
bv1 Expr n (BaseBVType w)
bv2 -> do IExp (BaseBVType w)
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
                             IExp (BaseBVType w)
e2 <- 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)
bv2
                             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 :: Nat). Binop (BaseBVType w) (BaseBVType w)
BVShiftR IExp (BaseBVType w)
e1 IExp (BaseBVType w)
e2
    BVAshr NatRepr w
_   Expr n (BaseBVType w)
bv1 Expr n (BaseBVType w)
bv2 -> do IExp (BaseBVType w)
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
                             IExp (BaseBVType w)
e2 <- 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)
bv2
                             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 :: Nat). Binop (BaseBVType w) (BaseBVType w)
BVShiftRA IExp (BaseBVType w)
e1 IExp (BaseBVType w)
e2
    BVRol  NatRepr w
w   Expr n (BaseBVType w)
bv1 Expr n (BaseBVType w)
bv2 ->
      do IExp (BaseBVType w)
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 Expr n (BaseBVType w)
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 :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w (NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w) ->
             Exp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (NatRepr w -> IExp (BaseBVType w) -> BV w -> Exp (BaseBVType w)
forall (w :: Nat) (tp :: BaseType).
NatRepr w -> IExp tp -> BV w -> Exp tp
BVRotateL NatRepr w
w 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 IExp (BaseBVType w)
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 Expr n (BaseBVType w)
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 :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w (NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w) ->
             Exp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (NatRepr w -> IExp (BaseBVType w) -> BV w -> Exp (BaseBVType w)
forall (w :: Nat) (tp :: BaseType).
NatRepr w -> IExp tp -> BV w -> Exp tp
BVRotateR NatRepr w
w 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 :: Nat) (n :: Nat) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (NatRepr r -> NatRepr w -> LeqProof w r
forall (n :: Nat) (m :: Nat) (p :: Nat -> 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 :: Nat) (n :: Nat) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (NatRepr r -> NatRepr w -> LeqProof 1 (r - w)
forall (m :: Nat) (n :: Nat).
(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 :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel NatRepr r
w NatRepr w
ew of
        ((r - w) + w) :~: r
Refl ->
          do IExp (BaseBVType w)
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)
n = NatRepr r
w NatRepr r -> NatRepr w -> NatRepr (r - w)
forall (n :: Nat) (m :: Nat).
(n <= m) =>
NatRepr m -> NatRepr n -> NatRepr (m - n)
`subNat` NatRepr w
ew
             IExp (BaseBVType (r - w))
zeros <- NatRepr (r - w)
-> BV (r - w) -> VerilogM sym n (IExp (BaseBVType (r - w)))
forall (w :: Nat) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr (r - w)
n (NatRepr (r - w) -> BV (r - w)
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr (r - w)
n)
             NatRepr r
-> IExp (BaseBVType (r - w))
-> IExp (BaseBVType w)
-> VerilogM sym n (IExp (BaseBVType r))
forall (w :: Nat) (w1 :: Nat) (w2 :: Nat) sym n.
(w ~ (w1 + w2), 1 <= w) =>
NatRepr w
-> IExp (BaseBVType w1)
-> IExp (BaseBVType w2)
-> VerilogM sym n (IExp (BaseBVType w))
concat2 NatRepr r
w IExp (BaseBVType (r - w))
zeros IExp (BaseBVType w)
e'
      where ew :: NatRepr w
ew = Expr n (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
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 :: Nat) (n :: Nat) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (NatRepr r -> NatRepr w -> LeqProof w r
forall (n :: Nat) (m :: Nat) (p :: Nat -> 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 :: Nat) (n :: Nat) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (NatRepr r -> NatRepr w -> LeqProof 1 (r - w)
forall (m :: Nat) (n :: Nat).
(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 :: Nat -> Type) (m :: Nat) (g :: Nat -> Type) (n :: Nat).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel NatRepr r
w NatRepr w
ew of
        ((r - w) + w) :~: r
Refl ->
          do IExp (BaseBVType w)
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)
n = NatRepr r
w NatRepr r -> NatRepr w -> NatRepr (r - w)
forall (n :: Nat) (m :: Nat).
(n <= m) =>
NatRepr m -> NatRepr n -> NatRepr (m - n)
`subNat` NatRepr w
ew
             IExp (BaseBVType (r - w))
zeros <- NatRepr (r - w)
-> BV (r - w) -> VerilogM sym n (IExp (BaseBVType (r - w)))
forall (w :: Nat) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr (r - w)
n (NatRepr (r - w) -> BV (r - w)
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr (r - w)
n)
             IExp (BaseBVType (r - w))
ones <- NatRepr (r - w)
-> BV (r - w) -> VerilogM sym n (IExp (BaseBVType (r - w)))
forall (w :: Nat) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr (r - w)
n (NatRepr (r - w) -> BV (r - w)
forall (w :: Nat). NatRepr w -> BV w
BV.maxUnsigned NatRepr (r - w)
n)
             IExp BaseBoolType
sgn <- IExp (BaseBVType w)
-> Integer -> VerilogM sym n (IExp BaseBoolType)
forall (w :: Nat) sym n.
IExp (BaseBVType w)
-> Integer -> VerilogM sym n (IExp BaseBoolType)
bit IExp (BaseBVType w)
e' (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (NatRepr r -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr r
w) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
             IExp (BaseBVType (r - w))
ext <- IExp BaseBoolType
-> IExp (BaseBVType (r - w))
-> IExp (BaseBVType (r - w))
-> VerilogM sym n (IExp (BaseBVType (r - w)))
forall (tp :: BaseType) sym n.
IExp BaseBoolType -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
mux IExp BaseBoolType
sgn IExp (BaseBVType (r - w))
ones IExp (BaseBVType (r - w))
zeros
             NatRepr r
-> IExp (BaseBVType (r - w))
-> IExp (BaseBVType w)
-> VerilogM sym n (IExp (BaseBVType r))
forall (w :: Nat) (w1 :: Nat) (w2 :: Nat) sym n.
(w ~ (w1 + w2), 1 <= w) =>
NatRepr w
-> IExp (BaseBVType w1)
-> IExp (BaseBVType w2)
-> VerilogM sym n (IExp (BaseBVType w))
concat2 NatRepr r
w IExp (BaseBVType (r - w))
ext IExp (BaseBVType w)
e'
      where ew :: NatRepr w
ew = Expr n (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
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"

    -- Array operations
    ArrayMap Assignment BaseTypeRepr (i ::> itp)
_ BaseTypeRepr tp
_ ArrayUpdateMap (Expr n) (i ::> itp) tp
_ Expr n (BaseArrayType (i ::> itp) tp)
_ -> String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"arrays"
    ConstantArray Assignment BaseTypeRepr (i ::> tp)
_ 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 ::> tp)
_ Expr n (BaseArrayType (i ::> tp) b)
_ Assignment (Expr n) (i ::> tp)
_ 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 ::> tp) tp)
_ Assignment (Expr n) (i ::> tp)
_ -> 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"