{-# 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 "
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)
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
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'
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'
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
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 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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"
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"