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

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

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


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

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


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

import What4.Protocol.VerilogWriter.AST

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

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

-- | Convert a What4 expresssion into a Verilog expression and return a
-- name for that expression's result.
exprToVerilogExpr ::
  (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
  Expr n tp ->
  VerilogM sym n (IExp tp)
exprToVerilogExpr :: forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
Expr n tp -> VerilogM sym n (IExp tp)
exprToVerilogExpr Expr n tp
e = do
  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 :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
w BV w
Coefficient sr
i
      SemiRingLiteral SemiRingRepr sr
_ Coefficient sr
_ ProgramLoc
_ ->
        String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"non-bit-vector literals"
      BoolExpr Bool
b ProgramLoc
_   -> Bool -> VerilogM sym n (IExp 'BaseBoolType)
forall sym n. Bool -> VerilogM sym n (IExp 'BaseBoolType)
litBool Bool
b
      StringExpr StringLiteral si
_ ProgramLoc
_ -> String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"strings"
      FloatExpr{} -> String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floating-point values"
      AppExpr AppExpr n tp
app -> AppExpr n tp -> VerilogM sym n (IExp tp)
forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
AppExpr n tp -> VerilogM sym n (IExp tp)
appExprVerilogExpr AppExpr n tp
app
      NonceAppExpr NonceAppExpr n tp
n -> NonceAppExpr n tp -> VerilogM sym n (IExp tp)
forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
NonceAppExpr n tp -> VerilogM sym n (IExp tp)
nonceAppExprVerilogExpr NonceAppExpr n tp
n
      BoundVarExpr ExprBoundVar n tp
x ->
        do Identifier
name <- ExprBoundVar n tp -> Identifier -> VerilogM sym n Identifier
forall n (tp :: BaseType) sym.
ExprBoundVar n tp -> Identifier -> VerilogM sym n Identifier
addBoundInput ExprBoundVar n tp
x (ExprBoundVar n tp -> Identifier
forall t (tp :: BaseType). ExprBoundVar t tp -> Identifier
bvarIdentifier ExprBoundVar n tp
x)
           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 -> VerilogM sym n (IExp tp))
-> IExp tp -> VerilogM sym n (IExp tp)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr tp -> Identifier -> IExp tp
forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
Ident (ExprBoundVar n tp -> BaseTypeRepr tp
forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
bvarType ExprBoundVar n tp
x) Identifier
name

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

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

boolMapToExpr ::
  (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
  Bool ->
  Bool ->
  Binop WT.BaseBoolType WT.BaseBoolType ->
  BMap.BoolMap (Expr n) ->
  VerilogM sym n (IExp WT.BaseBoolType)
boolMapToExpr :: forall sym n.
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
Bool
-> Bool
-> Binop 'BaseBoolType 'BaseBoolType
-> BoolMap (Expr n)
-> VerilogM sym n (IExp 'BaseBoolType)
boolMapToExpr Bool
u Bool
du Binop 'BaseBoolType 'BaseBoolType
op BoolMap (Expr n)
es =
  let pol :: (Expr n 'BaseBoolType, Polarity)
-> VerilogM sym n (IExp 'BaseBoolType)
pol (Expr n 'BaseBoolType
x,Polarity
Positive) = Expr n 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType)
forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
Expr n tp -> VerilogM sym n (IExp tp)
exprToVerilogExpr Expr n 'BaseBoolType
x
      pol (Expr n 'BaseBoolType
x,Polarity
Negative) = Unop 'BaseBoolType
-> IExp 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType)
forall (tp :: BaseType) sym n.
Unop tp -> IExp tp -> VerilogM sym n (IExp tp)
unop Unop 'BaseBoolType
Not (IExp 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType))
-> VerilogM sym n (IExp 'BaseBoolType)
-> VerilogM sym n (IExp 'BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr n 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType)
forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
Expr n tp -> VerilogM sym n (IExp tp)
exprToVerilogExpr Expr n 'BaseBoolType
x
  in
  case BoolMap (Expr n) -> BoolMapView (Expr n)
forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
BMap.viewBoolMap BoolMap (Expr n)
es of
    BoolMapView (Expr n)
BMap.BoolMapUnit -> Bool -> VerilogM sym n (IExp 'BaseBoolType)
forall sym n. Bool -> VerilogM sym n (IExp 'BaseBoolType)
litBool Bool
u
    BoolMapView (Expr n)
BMap.BoolMapDualUnit -> Bool -> VerilogM sym n (IExp 'BaseBoolType)
forall sym n. Bool -> VerilogM sym n (IExp 'BaseBoolType)
litBool Bool
du
    BMap.BoolMapTerms ((Expr n 'BaseBoolType, Polarity)
t:|[]) -> (Expr n 'BaseBoolType, Polarity)
-> VerilogM sym n (IExp 'BaseBoolType)
forall {sym} {n}.
(SymExpr sym ~ Expr n, IsExprBuilder sym) =>
(Expr n 'BaseBoolType, Polarity)
-> VerilogM sym n (IExp 'BaseBoolType)
pol (Expr n 'BaseBoolType, Polarity)
t
    BMap.BoolMapTerms ((Expr n 'BaseBoolType, Polarity)
t:|[(Expr n 'BaseBoolType, Polarity)]
ts) -> do
      IExp 'BaseBoolType
t' <- (Expr n 'BaseBoolType, Polarity)
-> VerilogM sym n (IExp 'BaseBoolType)
forall {sym} {n}.
(SymExpr sym ~ Expr n, IsExprBuilder sym) =>
(Expr n 'BaseBoolType, Polarity)
-> VerilogM sym n (IExp 'BaseBoolType)
pol (Expr n 'BaseBoolType, Polarity)
t
      [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)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (Expr n 'BaseBoolType, Polarity)
-> VerilogM sym n (IExp 'BaseBoolType)
forall {sym} {n}.
(SymExpr sym ~ Expr n, IsExprBuilder sym) =>
(Expr n 'BaseBoolType, Polarity)
-> VerilogM sym n (IExp 'BaseBoolType)
pol [(Expr n 'BaseBoolType, Polarity)]
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 :: forall (m :: Natural) (n :: Natural).
(1 <= m, 1 <= n, (n + 1) <= m) =>
NatRepr m -> NatRepr n -> LeqProof 1 (m - n)
leqSubPos NatRepr m
mr NatRepr n
nr =
  case (NatRepr n -> NatRepr 1 -> (n + 1) :~: (1 + n)
forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> (m + n) :~: (n + m)
plusComm NatRepr n
nr NatRepr 1
one, NatRepr 1 -> NatRepr n -> ((1 + n) - n) :~: 1
forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
f m -> g n -> ((m + n) - n) :~: m
plusMinusCancel NatRepr 1
one NatRepr n
nr) of
    ((n + 1) :~: (1 + n)
Refl, ((n + 1) - n) :~: 1
((1 + n) - n) :~: 1
Refl) ->
      LeqProof (n + 1) m
-> LeqProof n n -> LeqProof ((n + 1) - n) (m - n)
forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
       (y_h :: Natural).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
leqSub2 (NatRepr (n + 1) -> NatRepr m -> LeqProof (n + 1) m
forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
       (g :: Natural -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (NatRepr n
nr NatRepr n -> NatRepr 1 -> NatRepr (n + 1)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
`addNat` NatRepr 1
one) NatRepr m
mr) (NatRepr n -> NatRepr n -> LeqProof n n
forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
       (g :: Natural -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof NatRepr n
nr NatRepr n
nr)
  where one :: NatRepr 1
one = NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat :: NatRepr 1

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

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

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

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

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

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

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

    -- Bitvector operations
    BVTestBit Natural
i Expr n (BaseBVType w)
e -> do 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 :: Natural) 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) tp
-> IExp (BaseBVType w)
-> IExp (BaseBVType w)
-> VerilogM sym n (IExp tp)
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop (BaseBVType w) tp
Binop (BaseBVType w) 'BaseBoolType
forall (w :: Natural). 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) tp
-> IExp (BaseBVType w)
-> IExp (BaseBVType w)
-> VerilogM sym n (IExp tp)
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop (BaseBVType w) tp
Binop (BaseBVType w) 'BaseBoolType
forall (w :: Natural). 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)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM Expr n ('BaseBVType w) -> VerilogM sym n (IExp ('BaseBVType w))
forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
Expr n tp -> VerilogM sym n (IExp tp)
exprToVerilogExpr (BVOrSet (Expr n) w -> [Expr n ('BaseBVType w)]
forall (e :: BaseType -> Type) (w :: Natural).
BVOrSet e w -> [e (BaseBVType w)]
bvOrToList BVOrSet (Expr n) w
bs)
         case [IExp ('BaseBVType w)]
exprs of
           [] -> NatRepr w -> BV w -> VerilogM sym n (IExp ('BaseBVType w))
forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
w (NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w)
           IExp ('BaseBVType w)
e:[IExp ('BaseBVType w)]
es -> (IExp tp -> IExp tp -> VerilogM sym n (IExp tp))
-> IExp tp -> [IExp tp] -> VerilogM sym n (IExp tp)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Binop tp tp -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop tp tp
Binop ('BaseBVType w) ('BaseBVType w)
forall (w :: Natural). Binop ('BaseBVType w) ('BaseBVType w)
BVOr) IExp tp
IExp ('BaseBVType w)
e [IExp tp]
[IExp ('BaseBVType w)]
es
    BVUnaryTerm UnaryBV (Expr n 'BaseBoolType) n
ubv -> (Integer -> VerilogM sym n (IExp tp))
-> (Expr n 'BaseBoolType
    -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp))
-> UnaryBV (Expr n 'BaseBoolType) n
-> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) r p (n :: Natural).
(Applicative m, Monad m) =>
(Integer -> m r) -> (p -> r -> r -> m r) -> UnaryBV p n -> m r
UBV.sym_evaluate (\Integer
i -> NatRepr n -> BV n -> VerilogM sym n (IExp ('BaseBVType n))
forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr n
w (NatRepr n -> Integer -> BV n
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr n
w Integer
i)) Expr n 'BaseBoolType
-> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
forall {sym} {n} {tp :: BaseType}.
(SymExpr sym ~ Expr n, IsExprBuilder sym) =>
Expr n 'BaseBoolType
-> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
ite' UnaryBV (Expr n 'BaseBoolType) n
ubv
      where
        w :: NatRepr n
w = UnaryBV (Expr n 'BaseBoolType) n -> NatRepr n
forall p (n :: Natural). UnaryBV p n -> NatRepr n
UBV.width UnaryBV (Expr n 'BaseBoolType) n
ubv
        ite' :: Expr n 'BaseBoolType
-> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
ite' Expr n 'BaseBoolType
e IExp tp
e1 IExp tp
e0 = do 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 :: 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 (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 :: 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 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 :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
len (NatRepr w -> BV w
forall (w :: Natural). 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 :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
len (NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
len)
                       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
IExp ('BaseBVType w)
e1 IExp tp
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) tp
-> IExp ('BaseBVType w)
-> IExp ('BaseBVType w)
-> VerilogM sym n (IExp tp)
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop ('BaseBVType w) tp
Binop ('BaseBVType w) ('BaseBVType w)
forall (w :: Natural). 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) tp
-> IExp ('BaseBVType w)
-> IExp ('BaseBVType w)
-> VerilogM sym n (IExp tp)
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop ('BaseBVType w) tp
Binop ('BaseBVType w) ('BaseBVType w)
forall (w :: Natural). 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) tp
-> IExp ('BaseBVType w)
-> IExp ('BaseBVType w)
-> VerilogM sym n (IExp tp)
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop ('BaseBVType w) tp
Binop ('BaseBVType w) ('BaseBVType w)
forall (w :: Natural). 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) tp
-> IExp ('BaseBVType w)
-> IExp ('BaseBVType w)
-> VerilogM sym n (IExp tp)
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop ('BaseBVType w) tp
Binop ('BaseBVType w) ('BaseBVType w)
forall (w :: Natural). 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) tp
-> IExp ('BaseBVType w)
-> IExp ('BaseBVType w)
-> VerilogM sym n (IExp tp)
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop ('BaseBVType w) tp
Binop ('BaseBVType w) ('BaseBVType w)
forall (w :: Natural). 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) tp
-> IExp ('BaseBVType w)
-> IExp ('BaseBVType w)
-> VerilogM sym n (IExp tp)
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop ('BaseBVType w) tp
Binop ('BaseBVType w) ('BaseBVType w)
forall (w :: Natural). 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) tp
-> IExp ('BaseBVType w)
-> IExp ('BaseBVType w)
-> VerilogM sym n (IExp tp)
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop ('BaseBVType w) tp
Binop ('BaseBVType w) ('BaseBVType w)
forall (w :: Natural). 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 :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w (NatRepr w -> Integer
forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr w
w) ->
             Exp tp -> VerilogM sym n (IExp tp)
forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (NatRepr w -> IExp tp -> BV w -> Exp tp
forall (w :: Natural) (tp :: BaseType).
NatRepr w -> IExp tp -> BV w -> Exp tp
BVRotateL NatRepr w
w IExp tp
IExp ('BaseBVType w)
e1 BV w
Coefficient sr
n)
           Expr n ('BaseBVType w)
_ -> String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"non-constant bit rotations"
    BVRor  NatRepr w
w   Expr n ('BaseBVType w)
bv1 Expr n ('BaseBVType w)
bv2 ->
      do 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 :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w (NatRepr w -> Integer
forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr w
w) ->
             Exp tp -> VerilogM sym n (IExp tp)
forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (NatRepr w -> IExp tp -> BV w -> Exp tp
forall (w :: Natural) (tp :: BaseType).
NatRepr w -> IExp tp -> BV w -> Exp tp
BVRotateR NatRepr w
w IExp tp
IExp ('BaseBVType w)
e1 BV w
Coefficient sr
n)
           Expr n ('BaseBVType w)
_ -> String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"non-constant bit rotations"
    BVZext NatRepr r
w Expr n (BaseBVType w)
e ->
      LeqProof w r
-> ((w <= r) => VerilogM sym n (IExp tp))
-> VerilogM sym n (IExp tp)
forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (NatRepr r -> NatRepr w -> LeqProof w r
forall (n :: Natural) (m :: Natural) (p :: Natural -> Type).
((n + 1) <= m) =>
p m -> NatRepr n -> LeqProof n m
leqSuccLeft NatRepr r
w NatRepr w
ew) (((w <= r) => VerilogM sym n (IExp tp))
 -> VerilogM sym n (IExp tp))
-> ((w <= r) => VerilogM sym n (IExp tp))
-> VerilogM sym n (IExp tp)
forall a b. (a -> b) -> a -> b
$
      LeqProof 1 (r - w)
-> ((1 <= (r - w)) => VerilogM sym n (IExp tp))
-> VerilogM sym n (IExp tp)
forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (NatRepr r -> NatRepr w -> LeqProof 1 (r - w)
forall (m :: Natural) (n :: Natural).
(1 <= m, 1 <= n, (n + 1) <= m) =>
NatRepr m -> NatRepr n -> LeqProof 1 (m - n)
leqSubPos NatRepr r
w NatRepr w
ew) (((1 <= (r - w)) => VerilogM sym n (IExp tp))
 -> VerilogM sym n (IExp tp))
-> ((1 <= (r - w)) => VerilogM sym n (IExp tp))
-> VerilogM sym n (IExp tp)
forall a b. (a -> b) -> a -> b
$
      case NatRepr r -> NatRepr w -> ((r - w) + w) :~: r
forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel NatRepr r
w NatRepr w
ew of
        ((r - w) + w) :~: r
Refl ->
          do 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 :: Natural) (m :: Natural).
(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 :: Natural) 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 :: Natural). 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 :: 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 r
w IExp (BaseBVType (r - w))
zeros IExp (BaseBVType w)
e'
      where ew :: NatRepr w
ew = Expr n (BaseBVType w) -> NatRepr w
forall (w :: Natural). Expr n (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr n (BaseBVType w)
e
    BVSext NatRepr r
w Expr n (BaseBVType w)
e ->
      LeqProof w r
-> ((w <= r) => VerilogM sym n (IExp tp))
-> VerilogM sym n (IExp tp)
forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (NatRepr r -> NatRepr w -> LeqProof w r
forall (n :: Natural) (m :: Natural) (p :: Natural -> Type).
((n + 1) <= m) =>
p m -> NatRepr n -> LeqProof n m
leqSuccLeft NatRepr r
w NatRepr w
ew) (((w <= r) => VerilogM sym n (IExp tp))
 -> VerilogM sym n (IExp tp))
-> ((w <= r) => VerilogM sym n (IExp tp))
-> VerilogM sym n (IExp tp)
forall a b. (a -> b) -> a -> b
$
      LeqProof 1 (r - w)
-> ((1 <= (r - w)) => VerilogM sym n (IExp tp))
-> VerilogM sym n (IExp tp)
forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (NatRepr r -> NatRepr w -> LeqProof 1 (r - w)
forall (m :: Natural) (n :: Natural).
(1 <= m, 1 <= n, (n + 1) <= m) =>
NatRepr m -> NatRepr n -> LeqProof 1 (m - n)
leqSubPos NatRepr r
w NatRepr w
ew) (((1 <= (r - w)) => VerilogM sym n (IExp tp))
 -> VerilogM sym n (IExp tp))
-> ((1 <= (r - w)) => VerilogM sym n (IExp tp))
-> VerilogM sym n (IExp tp)
forall a b. (a -> b) -> a -> b
$
      case NatRepr r -> NatRepr w -> ((r - w) + w) :~: r
forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
       (n :: Natural).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel NatRepr r
w NatRepr w
ew of
        ((r - w) + w) :~: r
Refl ->
          do 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 :: Natural) (m :: Natural).
(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 :: Natural) 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 :: Natural). 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 :: Natural) 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 :: Natural). NatRepr w -> BV w
BV.maxUnsigned NatRepr (r - w)
n)
             IExp 'BaseBoolType
sgn <- IExp (BaseBVType w)
-> Integer -> VerilogM sym n (IExp 'BaseBoolType)
forall (w :: Natural) 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 :: Natural). 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 :: 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 r
w IExp (BaseBVType (r - w))
ext IExp (BaseBVType w)
e'
      where ew :: NatRepr w
ew = Expr n (BaseBVType w) -> NatRepr w
forall (w :: Natural). Expr n (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr n (BaseBVType w)
e
    BVPopcount NatRepr w
_ Expr n ('BaseBVType w)
_ ->
      String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"bit vector population count" -- TODO
    BVCountTrailingZeros NatRepr w
_ Expr n ('BaseBVType w)
_ ->
      String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"bit vector count trailing zeros" -- TODO
    BVCountLeadingZeros  NatRepr w
_ Expr n ('BaseBVType w)
_ ->
      String -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"bit vector count leading zeros" -- TODO

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

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

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

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

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

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

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

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