{-
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 = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
doNotSupportMsg 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 <- forall sym n. ModuleState sym n -> IdxCache n IExp
vsExpCache forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = 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 forall a b. (a -> b) -> a -> b
$
    \case
      SemiRingLiteral (SR.SemiRingBVRepr BVFlavorRepr fv
_ NatRepr w
w) Coefficient sr
i ProgramLoc
_ ->
        forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
w Coefficient sr
i
      SemiRingLiteral SemiRingRepr sr
_ Coefficient sr
_ ProgramLoc
_ ->
        forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"non-bit-vector literals"
      BoolExpr Bool
b ProgramLoc
_   -> forall sym n. Bool -> VerilogM sym n (IExp 'BaseBoolType)
litBool Bool
b
      StringExpr StringLiteral si
_ ProgramLoc
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"strings"
      FloatExpr{} -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floating-point values"
      AppExpr AppExpr n tp
app -> 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 -> 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 <- forall n (tp :: BaseType) sym.
ExprBoundVar n tp -> Identifier -> VerilogM sym n Identifier
addBoundInput ExprBoundVar n tp
x (forall t (tp :: BaseType). ExprBoundVar t tp -> Identifier
bvarIdentifier ExprBoundVar n tp
x)
           forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
Ident (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 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
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"universal quantification"
    Exists ExprBoundVar n tp1
_ Expr n 'BaseBoolType
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"existential quantification"
    ArrayFromFn ExprSymFn n (idx ::> itp) ret
_ -> 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)
_ -> 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)
_ -> 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 <- forall {k} n sym.
Some (Nonce n)
-> Some BaseTypeRepr -> Identifier -> VerilogM sym n Identifier
addFreshInput (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Nonce n (args ::> tp)
idx) (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr tp
tp) Identifier
base
      forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
Ident BaseTypeRepr tp
tp Identifier
name
        where
          tp :: BaseTypeRepr tp
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 = 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 (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
_ -> 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 -> 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) = 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) = forall (tp :: BaseType) sym n.
Unop tp -> IExp tp -> VerilogM sym n (IExp tp)
unop Unop 'BaseBoolType
Not forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
BMap.viewBoolMap BoolMap (Expr n)
es of
    BoolMapView (Expr n)
BMap.BoolMapUnit -> forall sym n. Bool -> VerilogM sym n (IExp 'BaseBoolType)
litBool Bool
u
    BoolMapView (Expr n)
BMap.BoolMapDualUnit -> forall sym n. Bool -> VerilogM sym n (IExp 'BaseBoolType)
litBool Bool
du
    BMap.BoolMapTerms ((Expr n 'BaseBoolType, Polarity)
t:|[]) -> 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' <- 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' <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {sym} {n}.
(SymExpr sym ~ Expr n, IsExprBuilder sym) =>
(Expr n 'BaseBoolType, Polarity)
-> VerilogM sym n (IExp 'BaseBoolType)
pol [(Expr n 'BaseBoolType, Polarity)]
ts
      forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (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 (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, 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) ->
      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 (forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
       (g :: Natural -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (NatRepr n
nr forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
`addNat` NatRepr 1
one) NatRepr m
mr) (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 = 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 (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, 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) ->
      forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans (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) (forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
       (g :: Natural -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (NatRepr n
nr forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
`addNat` NatRepr 1
one) p m
mr)
  where one :: NatRepr 1
one = 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 = forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
App (Expr n) tp -> VerilogM sym n (IExp tp)
appVerilogExpr forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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' <- 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' <- 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' <- forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
Expr n tp -> VerilogM sym n (IExp tp)
exprToVerilogExpr Expr n tp
efalse
      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' <- 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' <- forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
Expr n tp -> VerilogM sym n (IExp tp)
exprToVerilogExpr Expr n tp1
e2
      forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop forall (tp :: BaseType). Binop tp 'BaseBoolType
Eq IExp tp1
e1' IExp tp1
e2'

    -- Boolean operations
    NotPred Expr n 'BaseBoolType
e -> do
      IExp 'BaseBoolType
e' <- forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
Expr n tp -> VerilogM sym n (IExp tp)
exprToVerilogExpr Expr n 'BaseBoolType
e
      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 -> 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 <- 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 = 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 forall (w :: Natural). Binop (BaseBVType w) (BaseBVType w)
BVMul BV w
c forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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
        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 (forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop forall (w :: Natural). Binop (BaseBVType w) (BaseBVType w)
BVAdd) BV w
-> Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
scalMult' (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 <- 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 = 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 forall (w :: Natural). Binop (BaseBVType w) (BaseBVType w)
BVAnd BV w
c forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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
        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 (forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop forall (w :: Natural). Binop (BaseBVType w) (BaseBVType w)
BVXor) BV w
-> Expr n (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
scalMult' (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
_ -> 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 <- forall (f :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct f sr -> SemiRingRepr sr
WS.prodRepr SemiRingProduct (Expr n) sr
p ->
        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 (forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop forall (w :: Natural). Binop (BaseBVType w) (BaseBVType w)
BVMul) 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 forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Maybe (IExp (BaseBVType w))
Nothing -> forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
w (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
1)
          Just IExp (BaseBVType w)
e  -> forall (m :: Type -> Type) a. Monad m => a -> m a
return IExp (BaseBVType w)
e
      | SR.SemiRingBVRepr BVFlavorRepr fv
SR.BVBitsRepr NatRepr w
w <- forall (f :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct f sr -> SemiRingRepr sr
WS.prodRepr SemiRingProduct (Expr n) sr
p ->
        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 (forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop forall (w :: Natural). Binop (BaseBVType w) (BaseBVType w)
BVAnd) 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 forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Maybe (IExp (BaseBVType w))
Nothing -> forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
w (forall (w :: Natural). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
w)
          Just IExp (BaseBVType w)
e  -> forall (m :: Type -> Type) a. Monad m => a -> m a
return IExp (BaseBVType w)
e
    SemiRingProd SemiRingProduct (Expr n) sr
_ -> 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)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"semiring operations on non-bitvectors"

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

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

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

    -- Irrational numbers
    RealSpecialFunction{} -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"real numbers"
    RoundEvenReal Expr n BaseRealType
_ -> 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 <- 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
                        forall (w :: Natural) sym n.
IExp (BaseBVType w)
-> Integer -> VerilogM sym n (IExp 'BaseBoolType)
bit IExp (BaseBVType w)
v (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' <- forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
signed forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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' <- forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
signed forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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
         forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop 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' <- 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' <- 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
         forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop 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 <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
Expr n tp -> VerilogM sym n (IExp tp)
exprToVerilogExpr (forall (e :: BaseType -> Type) (w :: Natural).
BVOrSet e w -> [e (BaseBVType w)]
bvOrToList BVOrSet (Expr n) w
bs)
         case [IExp ('BaseBVType w)]
exprs of
           [] -> forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
w (forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
w)
           IExp ('BaseBVType w)
e:[IExp ('BaseBVType w)]
es -> forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop forall (w :: Natural). Binop (BaseBVType w) (BaseBVType w)
BVOr) IExp ('BaseBVType w)
e [IExp ('BaseBVType w)]
es
    BVUnaryTerm UnaryBV (Expr n 'BaseBoolType) n
ubv -> 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 -> forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr n
w (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr n
w Integer
i)) 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 = 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' <- forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
Expr n tp -> VerilogM sym n (IExp tp)
exprToVerilogExpr Expr n 'BaseBoolType
e
                          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' <- 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' <- 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
                                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 <- 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
                                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 <- 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 <- forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
len (forall (w :: Natural). NatRepr w -> BV w
BV.maxUnsigned NatRepr w
len)
                       IExp ('BaseBVType w)
e2 <- forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
len (forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
len)
                       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' <- 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' <- 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
         forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop 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' <- 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' <- 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
         forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop 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' <- forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
signed forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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' <- forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
signed forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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
         forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop 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' <- forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
signed forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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' <- forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
signed forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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
         forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop 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 <- 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 <- 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
                             forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop 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 <- 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 <- 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
                             forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop 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 <- forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
signed forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 <- 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
                             forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop 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 <- 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
_ | Coefficient sr
n forall a. Ord a => a -> a -> Bool
<= forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w (forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr w
w) ->
             forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (w :: Natural) (tp :: BaseType).
NatRepr w -> IExp tp -> BV w -> Exp tp
BVRotateL NatRepr w
w IExp ('BaseBVType w)
e1 Coefficient sr
n)
           Expr n ('BaseBVType w)
_ -> 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 <- 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
_ | Coefficient sr
n forall a. Ord a => a -> a -> Bool
<= forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w (forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr w
w) ->
             forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (w :: Natural) (tp :: BaseType).
NatRepr w -> IExp tp -> BV w -> Exp tp
BVRotateR NatRepr w
w IExp ('BaseBVType w)
e1 Coefficient sr
n)
           Expr n ('BaseBVType w)
_ -> 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 ->
      forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (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) forall a b. (a -> b) -> a -> b
$
      forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (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) forall a b. (a -> b) -> a -> b
$
      case 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' <- 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 forall (n :: Natural) (m :: Natural).
(n <= m) =>
NatRepr m -> NatRepr n -> NatRepr (m - n)
`subNat` NatRepr w
ew
             IExp (BaseBVType (r - w))
zeros <- forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr (r - w)
n (forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr (r - w)
n)
             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 = 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 ->
      forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (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) forall a b. (a -> b) -> a -> b
$
      forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (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) forall a b. (a -> b) -> a -> b
$
      case 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' <- 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 forall (n :: Natural) (m :: Natural).
(n <= m) =>
NatRepr m -> NatRepr n -> NatRepr (m - n)
`subNat` NatRepr w
ew
             IExp (BaseBVType (r - w))
zeros <- forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr (r - w)
n (forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr (r - w)
n)
             IExp (BaseBVType (r - w))
ones <- forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr (r - w)
n (forall (w :: Natural). NatRepr w -> BV w
BV.maxUnsigned NatRepr (r - w)
n)
             IExp 'BaseBoolType
sgn <- forall (w :: Natural) sym n.
IExp (BaseBVType w)
-> Integer -> VerilogM sym n (IExp 'BaseBoolType)
bit IExp (BaseBVType w)
e' (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr r
w) forall a. Num a => a -> a -> a
- Integer
1)
             IExp (BaseBVType (r - w))
ext <- 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
             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 = 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)
_ ->
      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)
_ ->
      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)
_ ->
      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)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floats"
    FloatAbs FloatPrecisionRepr fpp
_ Expr n ('BaseFloatType fpp)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floats"
    FloatSqrt FloatPrecisionRepr fpp
_ RoundingMode
_ Expr n ('BaseFloatType fpp)
_ -> 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)
_ -> 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)
_ -> 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)
_ -> 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)
_ -> 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)
_ -> 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)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floats"
    FloatFpEq Expr n (BaseFloatType fpp)
_ Expr n (BaseFloatType fpp)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floats"
    FloatLe Expr n (BaseFloatType fpp)
_ Expr n (BaseFloatType fpp)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floats"
    FloatLt Expr n (BaseFloatType fpp)
_ Expr n (BaseFloatType fpp)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floats"

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

    FloatCast FloatPrecisionRepr fpp
_ RoundingMode
_ Expr n (BaseFloatType fpp')
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floats"
    FloatRound FloatPrecisionRepr fpp
_ RoundingMode
_ Expr n ('BaseFloatType fpp)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floats"
    FloatFromBinary FloatPrecisionRepr (FloatingPointPrecision eb sb)
_ Expr n (BaseBVType (eb + sb))
_ -> 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))
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floats"
    BVToFloat FloatPrecisionRepr fpp
_ RoundingMode
_ Expr n (BaseBVType w)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floats"
    SBVToFloat FloatPrecisionRepr fpp
_ RoundingMode
_ Expr n (BaseBVType w)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floats"
    RealToFloat FloatPrecisionRepr fpp
_ RoundingMode
_ Expr n BaseRealType
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floats"
    FloatToBV NatRepr w
_ RoundingMode
_ Expr n (BaseFloatType fpp)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floats"
    FloatToSBV NatRepr w
_ RoundingMode
_ Expr n (BaseFloatType fpp)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"floats"
    FloatToReal Expr n (BaseFloatType fpp)
_ -> 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
_ -> 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)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"arrays"
    ConstantArray Assignment BaseTypeRepr (i ::> tp1)
_ BaseTypeRepr b
_ Expr n b
_ -> 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
_ -> 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)
_ -> 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)
_ -> 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)
_ -> 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)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"arrays"

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

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

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

    -- Strings
    StringAppend StringInfoRepr si
_ StringSeq (Expr n) si
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"strings"
    StringContains Expr n (BaseStringType si)
_ Expr n (BaseStringType si)
_ -> 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
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"strings"
    StringIsPrefixOf Expr n (BaseStringType si)
_ Expr n (BaseStringType si)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"strings"
    StringIsSuffixOf Expr n (BaseStringType si)
_ Expr n (BaseStringType si)
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"strings"
    StringLength Expr n (BaseStringType si)
_ -> 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
_ -> forall (m :: Type -> Type) a. MonadError String m => String -> m a
doNotSupportError String
"strings"