{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, ScopedTypeVariables,
TypeApplications, PolyKinds, DataKinds, ExplicitNamespaces, TypeOperators,
OverloadedStrings #-}
module What4.Protocol.VerilogWriter.AST
where
import qualified Data.BitVector.Sized as BV
import qualified Data.Map as Map
import qualified Data.Text as T
import qualified Data.Set as Set
import Data.String
import Data.Word
import Control.Monad.Except
import Control.Monad.State (MonadState(), StateT(..), get, put, modify, gets)
import qualified What4.BaseTypes as WT
import What4.Expr.Builder
import Data.Parameterized.Classes (OrderingF(..), compareF)
import Data.Parameterized.Nonce (Nonce, indexValue)
import Data.Parameterized.Some (Some(..), viewSome)
import Data.Parameterized.Pair
import GHC.TypeNats ( type (<=) )
type Identifier = T.Text
data Binop (inTp :: WT.BaseType) (outTp :: WT.BaseType) where
And :: Binop WT.BaseBoolType WT.BaseBoolType
Or :: Binop WT.BaseBoolType WT.BaseBoolType
Xor :: Binop WT.BaseBoolType WT.BaseBoolType
Eq :: Binop tp WT.BaseBoolType
Ne :: Binop tp WT.BaseBoolType
Lt :: Binop (WT.BaseBVType w) WT.BaseBoolType
Le :: Binop (WT.BaseBVType w) WT.BaseBoolType
BVAnd :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
BVOr :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
BVXor :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
BVAdd :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
BVSub :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
BVMul :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
BVDiv :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
BVRem :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
BVPow :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
BVShiftL :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
BVShiftR :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
BVShiftRA :: Binop (WT.BaseBVType w) (WT.BaseBVType w)
binopType ::
Binop inTp outTp ->
WT.BaseTypeRepr inTp ->
WT.BaseTypeRepr outTp
binopType :: forall (inTp :: BaseType) (outTp :: BaseType).
Binop inTp outTp -> BaseTypeRepr inTp -> BaseTypeRepr outTp
binopType Binop inTp outTp
And BaseTypeRepr inTp
_ = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Or BaseTypeRepr inTp
_ = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Xor BaseTypeRepr inTp
_ = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Eq BaseTypeRepr inTp
_ = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Ne BaseTypeRepr inTp
_ = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Lt BaseTypeRepr inTp
_ = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Le BaseTypeRepr inTp
_ = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
BVAnd BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVOr BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVXor BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVAdd BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVSub BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVMul BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVDiv BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVRem BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVPow BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVShiftL BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVShiftR BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
binopType Binop inTp outTp
BVShiftRA BaseTypeRepr inTp
tp = BaseTypeRepr inTp
tp
data Unop (tp :: WT.BaseType) where
Not :: Unop WT.BaseBoolType
BVNot :: Unop (WT.BaseBVType w)
data IExp (tp :: WT.BaseType) where
Ident :: WT.BaseTypeRepr tp -> Identifier -> IExp tp
iexpType :: IExp tp -> WT.BaseTypeRepr tp
iexpType :: forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType (Ident BaseTypeRepr tp
tp Identifier
_) = BaseTypeRepr tp
tp
data LHS = LHS Identifier | LHSBit Identifier Integer
data Exp (tp :: WT.BaseType) where
IExp :: IExp tp -> Exp tp
Binop :: Binop inTp outTp -> IExp inTp -> IExp inTp -> Exp outTp
Unop :: Unop tp -> IExp tp -> Exp tp
BVRotateL :: WT.NatRepr w -> IExp tp -> BV.BV w -> Exp tp
BVRotateR :: WT.NatRepr w -> IExp tp -> BV.BV w -> Exp tp
Mux :: IExp WT.BaseBoolType -> IExp tp -> IExp tp -> Exp tp
Bit :: IExp (WT.BaseBVType w)
-> Integer
-> Exp WT.BaseBoolType
BitSelect :: (1 WT.<= len, start WT.+ len WT.<= w)
=> IExp (WT.BaseBVType w)
-> WT.NatRepr start
-> WT.NatRepr len
-> Exp (WT.BaseBVType len)
Concat :: 1 <= w
=> WT.NatRepr w -> [Some IExp] -> Exp (WT.BaseBVType w)
BVLit :: (1 <= w)
=> WT.NatRepr w
-> BV.BV w
-> Exp (WT.BaseBVType w)
BoolLit :: Bool -> Exp WT.BaseBoolType
expType :: Exp tp -> WT.BaseTypeRepr tp
expType :: forall (tp :: BaseType). Exp tp -> BaseTypeRepr tp
expType (IExp IExp tp
e) = forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
expType (Binop Binop inTp tp
op IExp inTp
e1 IExp inTp
_) = forall (inTp :: BaseType) (outTp :: BaseType).
Binop inTp outTp -> BaseTypeRepr inTp -> BaseTypeRepr outTp
binopType Binop inTp tp
op (forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp inTp
e1)
expType (BVRotateL NatRepr w
_ IExp tp
e BV w
_) = forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
expType (BVRotateR NatRepr w
_ IExp tp
e BV w
_) = forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
expType (Unop Unop tp
_ IExp tp
e) = forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
expType (Mux IExp 'BaseBoolType
_ IExp tp
e1 IExp tp
_) = forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e1
expType (Bit IExp (BaseBVType w)
_ Integer
_) = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
expType (BitSelect IExp (BaseBVType w)
_ NatRepr start
_ NatRepr len
n) = forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
WT.BaseBVRepr NatRepr len
n
expType (Concat NatRepr w
w [Some IExp]
_) = forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
WT.BaseBVRepr NatRepr w
w
expType (BVLit NatRepr w
w BV w
_) = forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
WT.BaseBVRepr NatRepr w
w
expType (BoolLit Bool
_) = BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr
mkLet :: Exp tp -> VerilogM sym n (IExp tp)
mkLet :: forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (IExp IExp tp
x) = forall (m :: Type -> Type) a. Monad m => a -> m a
return IExp tp
x
mkLet Exp tp
e = do
let tp :: BaseTypeRepr tp
tp = forall (tp :: BaseType). Exp tp -> BaseTypeRepr tp
expType Exp tp
e
Identifier
x <- forall (tp :: BaseType) sym n.
BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
addFreshWire BaseTypeRepr tp
tp Bool
False Identifier
"wr" Exp tp
e
forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
Ident BaseTypeRepr tp
tp Identifier
x)
signed :: IExp tp -> VerilogM sym n (IExp tp)
signed :: forall (tp :: BaseType) sym n. IExp tp -> VerilogM sym n (IExp tp)
signed IExp tp
e = do
let tp :: BaseTypeRepr tp
tp = forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
Identifier
x <- forall (tp :: BaseType) sym n.
BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
addFreshWire BaseTypeRepr tp
tp Bool
True Identifier
"wr" (forall (tp :: BaseType). IExp tp -> Exp tp
IExp IExp tp
e)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
Ident BaseTypeRepr tp
tp Identifier
x)
binop ::
Binop inTp outTp ->
IExp inTp -> IExp inTp ->
VerilogM sym n (IExp outTp)
binop :: forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop inTp outTp
op IExp inTp
e1 IExp inTp
e2 = forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (w :: BaseType) (outTp :: BaseType).
Binop w outTp -> IExp w -> IExp w -> Exp outTp
Binop Binop inTp outTp
op IExp inTp
e1 IExp inTp
e2)
scalMult ::
1 <= w =>
WT.NatRepr w ->
Binop (WT.BaseBVType w) (WT.BaseBVType w) ->
BV.BV w ->
IExp (WT.BaseBVType w) ->
VerilogM sym n (IExp (WT.BaseBVType w))
scalMult :: forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w
-> Binop (BaseBVType w) (BaseBVType w)
-> BV w
-> IExp (BaseBVType w)
-> VerilogM sym n (IExp (BaseBVType w))
scalMult NatRepr w
w Binop (BaseBVType w) (BaseBVType w)
op BV w
n IExp (BaseBVType w)
e = do
IExp (BaseBVType w)
n' <- forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
w BV w
n
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop (BaseBVType w) (BaseBVType w)
op IExp (BaseBVType w)
n' IExp (BaseBVType w)
e
data BVConst = BVConst (Pair WT.NatRepr BV.BV)
deriving (BVConst -> BVConst -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BVConst -> BVConst -> Bool
$c/= :: BVConst -> BVConst -> Bool
== :: BVConst -> BVConst -> Bool
$c== :: BVConst -> BVConst -> Bool
Eq)
instance Ord BVConst where
compare :: BVConst -> BVConst -> Ordering
compare (BVConst Pair NatRepr BV
cx) (BVConst Pair NatRepr BV
cy) =
forall {k} (a :: k -> Type) (b :: k -> Type) c.
(forall (tp :: k). a tp -> b tp -> c) -> Pair a b -> c
viewPair (\NatRepr tp
wx BV tp
x -> forall {k} (a :: k -> Type) (b :: k -> Type) c.
(forall (tp :: k). a tp -> b tp -> c) -> Pair a b -> c
viewPair (\NatRepr tp
wy BV tp
y ->
case forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF NatRepr tp
wx NatRepr tp
wy of
OrderingF tp tp
LTF -> Ordering
LT
OrderingF tp tp
EQF | forall (w :: Natural). BV w -> BV w -> Bool
BV.ult BV tp
x BV tp
y -> Ordering
LT
OrderingF tp tp
EQF | forall (w :: Natural). BV w -> BV w -> Bool
BV.ult BV tp
y BV tp
x -> Ordering
GT
OrderingF tp tp
EQF -> Ordering
EQ
OrderingF tp tp
GTF -> Ordering
GT
) Pair NatRepr BV
cy) Pair NatRepr BV
cx
litBV ::
(1 <= w) =>
WT.NatRepr w ->
BV.BV w ->
VerilogM sym n (IExp (WT.BaseBVType w))
litBV :: forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
w BV w
i = do
Map BVConst Identifier
cache <- forall sym n. ModuleState sym n -> Map BVConst Identifier
vsBVCache 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
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Pair NatRepr BV -> BVConst
BVConst (forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair NatRepr w
w BV w
i)) Map BVConst Identifier
cache of
Just Identifier
x -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
Ident (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
WT.BaseBVRepr NatRepr w
w) Identifier
x)
Maybe Identifier
Nothing -> do
x :: IExp (BaseBVType w)
x@(Ident BaseTypeRepr (BaseBVType w)
_ Identifier
name) <- forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BV w -> Exp (BaseBVType w)
BVLit NatRepr w
w BV w
i)
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
s -> ModuleState sym n
s { vsBVCache :: Map BVConst Identifier
vsBVCache = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Pair NatRepr BV -> BVConst
BVConst (forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair NatRepr w
w BV w
i)) Identifier
name (forall sym n. ModuleState sym n -> Map BVConst Identifier
vsBVCache ModuleState sym n
s) }
forall (m :: Type -> Type) a. Monad m => a -> m a
return IExp (BaseBVType w)
x
litBool :: Bool -> VerilogM sym n (IExp WT.BaseBoolType)
litBool :: forall sym n. Bool -> VerilogM sym n (IExp 'BaseBoolType)
litBool Bool
b = do
Map Bool Identifier
cache <- forall sym n. ModuleState sym n -> Map Bool Identifier
vsBoolCache 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
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Bool
b Map Bool Identifier
cache of
Just Identifier
x -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
Ident BaseTypeRepr 'BaseBoolType
WT.BaseBoolRepr Identifier
x)
Maybe Identifier
Nothing -> do
x :: IExp 'BaseBoolType
x@(Ident BaseTypeRepr 'BaseBoolType
_ Identifier
name) <- forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (Bool -> Exp 'BaseBoolType
BoolLit Bool
b)
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
s -> ModuleState sym n
s { vsBoolCache :: Map Bool Identifier
vsBoolCache = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Bool
b Identifier
name (forall sym n. ModuleState sym n -> Map Bool Identifier
vsBoolCache ModuleState sym n
s) }
forall (m :: Type -> Type) a. Monad m => a -> m a
return IExp 'BaseBoolType
x
unop :: Unop tp -> IExp tp -> VerilogM sym n (IExp tp)
unop :: forall (tp :: BaseType) sym n.
Unop tp -> IExp tp -> VerilogM sym n (IExp tp)
unop Unop tp
op IExp tp
e = forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (tp :: BaseType). Unop tp -> IExp tp -> Exp tp
Unop Unop tp
op IExp tp
e)
mux ::
IExp WT.BaseBoolType ->
IExp tp ->
IExp tp ->
VerilogM sym n (IExp tp)
mux :: forall (tp :: BaseType) sym n.
IExp 'BaseBoolType
-> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
mux IExp 'BaseBoolType
e IExp tp
e1 IExp tp
e2 = forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (tp :: BaseType).
IExp 'BaseBoolType -> IExp tp -> IExp tp -> Exp tp
Mux IExp 'BaseBoolType
e IExp tp
e1 IExp tp
e2)
bit ::
IExp (WT.BaseBVType w) ->
Integer ->
VerilogM sym n (IExp WT.BaseBoolType)
bit :: forall (w :: Natural) sym n.
IExp (BaseBVType w)
-> Integer -> VerilogM sym n (IExp 'BaseBoolType)
bit IExp (BaseBVType w)
e Integer
i = forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (w :: Natural).
IExp (BaseBVType w) -> Integer -> Exp 'BaseBoolType
Bit IExp (BaseBVType w)
e Integer
i)
bitSelect ::
(1 WT.<= len, idx WT.+ len WT.<= w) =>
IExp (WT.BaseBVType w) ->
WT.NatRepr idx ->
WT.NatRepr len ->
VerilogM sym n (IExp (WT.BaseBVType len))
bitSelect :: 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 len
len = forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (w :: Natural) (start :: Natural) (w :: Natural).
(1 <= w, (start + w) <= w) =>
IExp (BaseBVType w)
-> NatRepr start -> NatRepr w -> Exp (BaseBVType w)
BitSelect IExp (BaseBVType w)
e NatRepr idx
start NatRepr len
len)
concat2 ::
(w ~ (w1 WT.+ w2), 1 <= w) =>
WT.NatRepr w ->
IExp (WT.BaseBVType w1) ->
IExp (WT.BaseBVType w2) ->
VerilogM sym n (IExp (WT.BaseBVType w))
concat2 :: 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 w
w IExp (BaseBVType w1)
e1 IExp (BaseBVType w2)
e2 = forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> [Some IExp] -> Exp (BaseBVType w)
Concat NatRepr w
w [forall k (f :: k -> Type) (x :: k). f x -> Some f
Some IExp (BaseBVType w1)
e1, forall k (f :: k -> Type) (x :: k). f x -> Some f
Some IExp (BaseBVType w2)
e2])
data Item where
Input :: WT.BaseTypeRepr tp -> Identifier -> Item
Output :: WT.BaseTypeRepr tp -> Identifier -> Item
Wire :: WT.BaseTypeRepr tp -> Identifier -> Item
Assign :: LHS -> Exp tp -> Item
data ModuleState sym n =
ModuleState { forall sym n.
ModuleState sym n -> [(Word64, Some BaseTypeRepr, Identifier)]
vsInputs :: [(Word64, Some WT.BaseTypeRepr, Identifier)]
, forall sym n.
ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsOutputs :: [(Some WT.BaseTypeRepr, Bool, Identifier, Some Exp)]
, forall sym n.
ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsWires :: [(Some WT.BaseTypeRepr, Bool, Identifier, Some Exp)]
, forall sym n. ModuleState sym n -> Map Word64 Identifier
vsSeenNonces :: Map.Map Word64 Identifier
, forall sym n. ModuleState sym n -> Set Identifier
vsUsedIdentifiers :: Set.Set Identifier
, forall sym n. ModuleState sym n -> IdxCache n IExp
vsExpCache :: IdxCache n IExp
, forall sym n. ModuleState sym n -> Map BVConst Identifier
vsBVCache :: Map.Map BVConst Identifier
, forall sym n. ModuleState sym n -> Map Bool Identifier
vsBoolCache :: Map.Map Bool Identifier
, forall sym n. ModuleState sym n -> sym
vsSym :: sym
}
newtype VerilogM sym n a =
VerilogM (StateT (ModuleState sym n) (ExceptT String IO) a)
deriving ( forall a b. a -> VerilogM sym n b -> VerilogM sym n a
forall a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b
forall sym n a b. a -> VerilogM sym n b -> VerilogM sym n a
forall sym n a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> VerilogM sym n b -> VerilogM sym n a
$c<$ :: forall sym n a b. a -> VerilogM sym n b -> VerilogM sym n a
fmap :: forall a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b
$cfmap :: forall sym n a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b
Functor
, forall a. a -> VerilogM sym n a
forall sym n. Functor (VerilogM sym n)
forall a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a
forall a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
forall a b.
VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
forall sym n a. a -> VerilogM sym n a
forall a b c.
(a -> b -> c)
-> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
forall sym n a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a
forall sym n a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
forall sym n a b.
VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
forall sym n a b c.
(a -> b -> c)
-> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
forall (f :: Type -> Type).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a
$c<* :: forall sym n a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a
*> :: forall a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
$c*> :: forall sym n a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
liftA2 :: forall a b c.
(a -> b -> c)
-> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
$cliftA2 :: forall sym n a b c.
(a -> b -> c)
-> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
<*> :: forall a b.
VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
$c<*> :: forall sym n a b.
VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
pure :: forall a. a -> VerilogM sym n a
$cpure :: forall sym n a. a -> VerilogM sym n a
Applicative
, forall a. a -> VerilogM sym n a
forall sym n. Applicative (VerilogM sym n)
forall a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
forall a b.
VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
forall sym n a. a -> VerilogM sym n a
forall sym n a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
forall sym n a b.
VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
forall (m :: Type -> Type).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> VerilogM sym n a
$creturn :: forall sym n a. a -> VerilogM sym n a
>> :: forall a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
$c>> :: forall sym n a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
>>= :: forall a b.
VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
$c>>= :: forall sym n a b.
VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
Monad
, MonadState (ModuleState sym n)
, MonadError String
, forall a. IO a -> VerilogM sym n a
forall sym n. Monad (VerilogM sym n)
forall sym n a. IO a -> VerilogM sym n a
forall (m :: Type -> Type).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> VerilogM sym n a
$cliftIO :: forall sym n a. IO a -> VerilogM sym n a
MonadIO
)
newtype Module sym n = Module (ModuleState sym n)
mkModule ::
sym ->
[(Some (Expr n), T.Text)] ->
[VerilogM sym n (Some IExp)] ->
ExceptT String IO (Module sym n)
mkModule :: forall sym n.
sym
-> [(Some (Expr n), Identifier)]
-> [VerilogM sym n (Some IExp)]
-> ExceptT String IO (Module sym n)
mkModule sym
sym [(Some (Expr n), Identifier)]
ins [VerilogM sym n (Some IExp)]
ops = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall sym n. ModuleState sym n -> Module sym n
Module forall a b. (a -> b) -> a -> b
$ forall sym n a.
sym -> VerilogM sym n a -> ExceptT String IO (ModuleState sym n)
execVerilogM sym
sym forall a b. (a -> b) -> a -> b
$ do
let addExprInput :: Some (Expr n) -> Identifier -> VerilogM sym n Identifier
addExprInput Some (Expr n)
e Identifier
ident =
case Some (Expr n)
e of
Some (BoundVarExpr ExprBoundVar n x
x) -> forall n (tp :: BaseType) sym.
ExprBoundVar n tp -> Identifier -> VerilogM sym n Identifier
addBoundInput ExprBoundVar n x
x Identifier
ident
Some (Expr n)
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Input provided to mkModule isn't an input"
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall {n} {sym}.
Some (Expr n) -> Identifier -> VerilogM sym n Identifier
addExprInput) [(Some (Expr n), Identifier)]
ins
[Some IExp]
es <- forall (t :: Type -> Type) (m :: Type -> Type) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [VerilogM sym n (Some IExp)]
ops
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Some IExp]
es forall a b. (a -> b) -> a -> b
$ \Some IExp
se ->
do Identifier
out <- forall sym n. Identifier -> VerilogM sym n Identifier
freshIdentifier Identifier
"out"
forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome (\IExp tp
e -> forall (tp :: BaseType) sym n.
BaseTypeRepr tp -> Identifier -> Exp tp -> VerilogM sym n ()
addOutput (forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e) Identifier
out (forall (tp :: BaseType). IExp tp -> Exp tp
IExp IExp tp
e)) Some IExp
se
initModuleState :: sym -> IO (ModuleState sym n)
initModuleState :: forall sym n. sym -> IO (ModuleState sym n)
initModuleState sym
sym = do
IdxCache n IExp
cache <- forall (m :: Type -> Type) t (f :: BaseType -> Type).
MonadIO m =>
m (IdxCache t f)
newIdxCache
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ModuleState
{ vsInputs :: [(Word64, Some BaseTypeRepr, Identifier)]
vsInputs = []
, vsOutputs :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsOutputs = []
, vsWires :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsWires = []
, vsSeenNonces :: Map Word64 Identifier
vsSeenNonces = forall k a. Map k a
Map.empty
, vsUsedIdentifiers :: Set Identifier
vsUsedIdentifiers = forall a. Set a
Set.empty
, vsExpCache :: IdxCache n IExp
vsExpCache = IdxCache n IExp
cache
, vsBVCache :: Map BVConst Identifier
vsBVCache = forall k a. Map k a
Map.empty
, vsBoolCache :: Map Bool Identifier
vsBoolCache = forall k a. Map k a
Map.empty
, vsSym :: sym
vsSym = sym
sym
}
runVerilogM ::
VerilogM sym n a ->
ModuleState sym n ->
ExceptT String IO (a, ModuleState sym n)
runVerilogM :: forall sym n a.
VerilogM sym n a
-> ModuleState sym n -> ExceptT String IO (a, ModuleState sym n)
runVerilogM (VerilogM StateT (ModuleState sym n) (ExceptT String IO) a
op) = forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT StateT (ModuleState sym n) (ExceptT String IO) a
op
execVerilogM ::
sym ->
VerilogM sym n a ->
ExceptT String IO (ModuleState sym n)
execVerilogM :: forall sym n a.
sym -> VerilogM sym n a -> ExceptT String IO (ModuleState sym n)
execVerilogM sym
sym VerilogM sym n a
op =
do ModuleState sym n
s <- forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym n. sym -> IO (ModuleState sym n)
initModuleState sym
sym
(a
_a,ModuleState sym n
m) <- forall sym n a.
VerilogM sym n a
-> ModuleState sym n -> ExceptT String IO (a, ModuleState sym n)
runVerilogM VerilogM sym n a
op ModuleState sym n
s
forall (m :: Type -> Type) a. Monad m => a -> m a
return ModuleState sym n
m
addBoundInput ::
ExprBoundVar n tp ->
Identifier ->
VerilogM sym n Identifier
addBoundInput :: forall n (tp :: BaseType) sym.
ExprBoundVar n tp -> Identifier -> VerilogM sym n Identifier
addBoundInput ExprBoundVar n tp
x Identifier
ident =
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 tp
idx) (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr tp
tp) Identifier
ident
where
tp :: BaseTypeRepr tp
tp = forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
bvarType ExprBoundVar n tp
x
idx :: Nonce n tp
idx = forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar n tp
x
addFreshInput ::
Some (Nonce n) ->
Some WT.BaseTypeRepr ->
Identifier ->
VerilogM sym n Identifier
addFreshInput :: forall {k} n sym.
Some (Nonce n)
-> Some BaseTypeRepr -> Identifier -> VerilogM sym n Identifier
addFreshInput Some (Nonce n)
n Some BaseTypeRepr
tp Identifier
base = do
Map Word64 Identifier
seenNonces <- forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets forall sym n. ModuleState sym n -> Map Word64 Identifier
vsSeenNonces
let idx :: Word64
idx = forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome forall k s (tp :: k). Nonce s tp -> Word64
indexValue Some (Nonce n)
n
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Word64
idx Map Word64 Identifier
seenNonces of
Just Identifier
ident -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Identifier
ident
Maybe Identifier
Nothing ->
do Identifier
name <- forall sym n. Identifier -> VerilogM sym n Identifier
freshIdentifier Identifier
base
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
st -> ModuleState sym n
st { vsInputs :: [(Word64, Some BaseTypeRepr, Identifier)]
vsInputs = (Word64
idx, Some BaseTypeRepr
tp, Identifier
name) forall a. a -> [a] -> [a]
: forall sym n.
ModuleState sym n -> [(Word64, Some BaseTypeRepr, Identifier)]
vsInputs ModuleState sym n
st
, vsSeenNonces :: Map Word64 Identifier
vsSeenNonces = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Word64
idx Identifier
name Map Word64 Identifier
seenNonces
}
forall (m :: Type -> Type) a. Monad m => a -> m a
return Identifier
name
addOutput ::
WT.BaseTypeRepr tp ->
Identifier ->
Exp tp ->
VerilogM sym n ()
addOutput :: forall (tp :: BaseType) sym n.
BaseTypeRepr tp -> Identifier -> Exp tp -> VerilogM sym n ()
addOutput BaseTypeRepr tp
tp Identifier
name Exp tp
e =
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
st -> ModuleState sym n
st { vsOutputs :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsOutputs = (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr tp
tp, Bool
False, Identifier
name, forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Exp tp
e) forall a. a -> [a] -> [a]
: forall sym n.
ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsOutputs ModuleState sym n
st }
addWire ::
WT.BaseTypeRepr tp ->
Bool ->
Identifier ->
Exp tp ->
VerilogM sym n ()
addWire :: forall (tp :: BaseType) sym n.
BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n ()
addWire BaseTypeRepr tp
tp Bool
isSigned Identifier
name Exp tp
e =
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
st -> ModuleState sym n
st { vsWires :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsWires = (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr tp
tp, Bool
isSigned, Identifier
name, forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Exp tp
e) forall a. a -> [a] -> [a]
: forall sym n.
ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsWires ModuleState sym n
st }
freshIdentifier :: T.Text -> VerilogM sym n Identifier
freshIdentifier :: forall sym n. Identifier -> VerilogM sym n Identifier
freshIdentifier Identifier
basename = do
ModuleState sym n
st <- forall s (m :: Type -> Type). MonadState s m => m s
get
let used :: Set Identifier
used = forall sym n. ModuleState sym n -> Set Identifier
vsUsedIdentifiers ModuleState sym n
st
let nm :: Identifier
nm | Identifier
basename forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Identifier
used =
[Identifier] -> Identifier
T.concat [Identifier
basename, Identifier
"_", forall a. IsString a => String -> a
fromString forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. Set a -> Int
Set.size Set Identifier
used ]
| Bool
otherwise = Identifier
basename
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ ModuleState sym n
st { vsUsedIdentifiers :: Set Identifier
vsUsedIdentifiers = forall a. Ord a => a -> Set a -> Set a
Set.insert Identifier
nm Set Identifier
used }
forall (m :: Type -> Type) a. Monad m => a -> m a
return Identifier
nm
addFreshWire ::
WT.BaseTypeRepr tp ->
Bool ->
T.Text ->
Exp tp ->
VerilogM sym n Identifier
addFreshWire :: forall (tp :: BaseType) sym n.
BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
addFreshWire BaseTypeRepr tp
repr Bool
isSigned Identifier
basename Exp tp
e = do
Identifier
x <- forall sym n. Identifier -> VerilogM sym n Identifier
freshIdentifier Identifier
basename
forall (tp :: BaseType) sym n.
BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n ()
addWire BaseTypeRepr tp
repr Bool
isSigned Identifier
x Exp tp
e
forall (m :: Type -> Type) a. Monad m => a -> m a
return Identifier
x