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

An intermediate AST to use for generating Verilog modules from What4 expressions.
-}
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, ScopedTypeVariables,
  TypeApplications, PolyKinds, DataKinds, ExplicitNamespaces, TypeOperators #-}

module What4.Protocol.VerilogWriter.AST
  where

import qualified Data.BitVector.Sized as BV
import qualified Data.Map as Map
import           Control.Monad.Except
import           Control.Monad.State (MonadState(), StateT(..), get, put, modify)

import qualified What4.BaseTypes as WT
import           What4.Expr.Builder
import           Data.Parameterized.Classes (OrderingF(..), compareF)
import           Data.Parameterized.Some (Some(..))
import           Data.Parameterized.Pair
import           GHC.TypeNats ( type (<=) )

type Identifier = String

-- | A type for Verilog binary operators that enforces well-typedness,
-- including bitvector size constraints.
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 :: Binop inTp outTp -> BaseTypeRepr inTp -> BaseTypeRepr outTp
binopType Binop inTp outTp
And BaseTypeRepr inTp
_ = BaseTypeRepr outTp
BaseTypeRepr BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Or  BaseTypeRepr inTp
_ = BaseTypeRepr outTp
BaseTypeRepr BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Xor BaseTypeRepr inTp
_ = BaseTypeRepr outTp
BaseTypeRepr BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Eq  BaseTypeRepr inTp
_ = BaseTypeRepr outTp
BaseTypeRepr BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Ne  BaseTypeRepr inTp
_ = BaseTypeRepr outTp
BaseTypeRepr BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Lt  BaseTypeRepr inTp
_ = BaseTypeRepr outTp
BaseTypeRepr BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
Le  BaseTypeRepr inTp
_ = BaseTypeRepr outTp
BaseTypeRepr BaseBoolType
WT.BaseBoolRepr
binopType Binop inTp outTp
BVAnd  BaseTypeRepr inTp
tp = BaseTypeRepr inTp
BaseTypeRepr outTp
tp
binopType Binop inTp outTp
BVOr  BaseTypeRepr inTp
tp = BaseTypeRepr inTp
BaseTypeRepr outTp
tp
binopType Binop inTp outTp
BVXor BaseTypeRepr inTp
tp = BaseTypeRepr inTp
BaseTypeRepr outTp
tp
binopType Binop inTp outTp
BVAdd BaseTypeRepr inTp
tp = BaseTypeRepr inTp
BaseTypeRepr outTp
tp
binopType Binop inTp outTp
BVSub BaseTypeRepr inTp
tp = BaseTypeRepr inTp
BaseTypeRepr outTp
tp
binopType Binop inTp outTp
BVMul BaseTypeRepr inTp
tp = BaseTypeRepr inTp
BaseTypeRepr outTp
tp
binopType Binop inTp outTp
BVDiv BaseTypeRepr inTp
tp = BaseTypeRepr inTp
BaseTypeRepr outTp
tp
binopType Binop inTp outTp
BVRem BaseTypeRepr inTp
tp = BaseTypeRepr inTp
BaseTypeRepr outTp
tp
binopType Binop inTp outTp
BVPow BaseTypeRepr inTp
tp = BaseTypeRepr inTp
BaseTypeRepr outTp
tp
binopType Binop inTp outTp
BVShiftL BaseTypeRepr inTp
tp = BaseTypeRepr inTp
BaseTypeRepr outTp
tp
binopType Binop inTp outTp
BVShiftR BaseTypeRepr inTp
tp = BaseTypeRepr inTp
BaseTypeRepr outTp
tp
binopType Binop inTp outTp
BVShiftRA BaseTypeRepr inTp
tp = BaseTypeRepr inTp
BaseTypeRepr outTp
tp

-- | A type for Verilog unary operators that enforces well-typedness.
data Unop (tp :: WT.BaseType) where
  Not :: Unop WT.BaseBoolType
  BVNot :: Unop (WT.BaseBVType w)

-- | A type for Verilog expression names that enforces well-typedness.
-- This type exists essentially to pair a name and type to avoid needing
-- to repeat them and ensure that all uses of the name are well-typed.
data IExp (tp :: WT.BaseType) where
  Ident   :: WT.BaseTypeRepr tp -> Identifier -> IExp tp

iexpType :: IExp tp -> WT.BaseTypeRepr tp
iexpType :: IExp tp -> BaseTypeRepr tp
iexpType (Ident BaseTypeRepr tp
tp Identifier
_) = BaseTypeRepr tp
tp

data LHS = LHS Identifier | LHSBit Identifier Integer

-- | A type for Verilog expressions that enforces well-typedness,
-- including bitvector size constraints.
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 -- the width
          -> BV.BV w -- the value
          -> Exp (WT.BaseBVType w)
  BoolLit :: Bool -> Exp WT.BaseBoolType

expType :: Exp tp -> WT.BaseTypeRepr tp
expType :: Exp tp -> BaseTypeRepr tp
expType (IExp IExp tp
e) = IExp tp -> BaseTypeRepr tp
forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
expType (Binop Binop inTp tp
op IExp inTp
e1 IExp inTp
_) = Binop inTp tp -> BaseTypeRepr inTp -> BaseTypeRepr tp
forall (inTp :: BaseType) (outTp :: BaseType).
Binop inTp outTp -> BaseTypeRepr inTp -> BaseTypeRepr outTp
binopType Binop inTp tp
op (IExp inTp -> BaseTypeRepr inTp
forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp inTp
e1)
expType (BVRotateL NatRepr w
_ IExp tp
e BV w
_) = IExp tp -> BaseTypeRepr tp
forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
expType (BVRotateR NatRepr w
_ IExp tp
e BV w
_) = IExp tp -> BaseTypeRepr tp
forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
expType (Unop Unop tp
_ IExp tp
e) = IExp tp -> BaseTypeRepr tp
forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
expType (Mux IExp BaseBoolType
_ IExp tp
e1 IExp tp
_) = IExp tp -> BaseTypeRepr tp
forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e1
expType (Bit IExp (BaseBVType w)
_ Integer
_) = BaseTypeRepr tp
BaseTypeRepr BaseBoolType
WT.BaseBoolRepr
expType (BitSelect IExp (BaseBVType w)
_ NatRepr start
_ NatRepr len
n) = NatRepr len -> BaseTypeRepr (BaseBVType len)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
WT.BaseBVRepr NatRepr len
n
expType (Concat NatRepr w
w [Some IExp]
_) = NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
WT.BaseBVRepr NatRepr w
w
expType (BVLit NatRepr w
w BV w
_) = NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
WT.BaseBVRepr NatRepr w
w
expType (BoolLit Bool
_) = BaseTypeRepr tp
BaseTypeRepr BaseBoolType
WT.BaseBoolRepr


-- | Create a let binding, associating a name with an expression. In
-- Verilog, this is a new "wire".
mkLet :: Exp tp -> VerilogM sym n (IExp tp)
mkLet :: Exp tp -> VerilogM sym n (IExp tp)
mkLet (IExp IExp tp
x) = IExp tp -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return IExp tp
x
mkLet Exp tp
e = do
    let tp :: BaseTypeRepr tp
tp = Exp tp -> BaseTypeRepr tp
forall (tp :: BaseType). Exp tp -> BaseTypeRepr tp
expType Exp tp
e
    Identifier
x <- BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
forall (tp :: BaseType) sym n.
BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
addFreshWire BaseTypeRepr tp
tp Bool
False Identifier
"x" Exp tp
e
    IExp tp -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BaseTypeRepr tp -> Identifier -> IExp tp
forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
Ident BaseTypeRepr tp
tp Identifier
x)

-- | Indicate than an expression name is signed. This causes arithmetic
-- operations involving this name to be interpreted as signed
-- operations.
signed :: IExp tp -> VerilogM sym n (IExp tp)
signed :: IExp tp -> VerilogM sym n (IExp tp)
signed IExp tp
e = do
    let tp :: BaseTypeRepr tp
tp = IExp tp -> BaseTypeRepr tp
forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e
    Identifier
x <- BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
forall (tp :: BaseType) sym n.
BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
addFreshWire BaseTypeRepr tp
tp Bool
True Identifier
"x" (IExp tp -> Exp tp
forall (tp :: BaseType). IExp tp -> Exp tp
IExp IExp tp
e)
    IExp tp -> VerilogM sym n (IExp tp)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BaseTypeRepr tp -> Identifier -> IExp tp
forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
Ident BaseTypeRepr tp
tp Identifier
x)

-- | Apply a binary operation to two expressions and bind the result to
-- a new, returned name.
binop ::
  Binop inTp outTp ->
  IExp inTp -> IExp inTp ->
  VerilogM sym n (IExp outTp)
binop :: Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop inTp outTp
op IExp inTp
e1 IExp inTp
e2 = Exp outTp -> VerilogM sym n (IExp outTp)
forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (Binop inTp outTp -> IExp inTp -> IExp inTp -> Exp outTp
forall (inTp :: BaseType) (outTp :: BaseType).
Binop inTp outTp -> IExp inTp -> IExp inTp -> Exp outTp
Binop Binop inTp outTp
op IExp inTp
e1 IExp inTp
e2)

-- | A special binary operation for scalar multiplication. This avoids
-- the need to call `litBV` at every call site.
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 :: 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' <- NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
forall (w :: Nat) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
w BV w
n
  Binop (BaseBVType w) (BaseBVType w)
-> IExp (BaseBVType w)
-> IExp (BaseBVType w)
-> VerilogM sym n (IExp (BaseBVType w))
forall (inTp :: BaseType) (outTp :: BaseType) sym n.
Binop inTp outTp
-> IExp inTp -> IExp inTp -> VerilogM sym n (IExp outTp)
binop Binop (BaseBVType w) (BaseBVType w)
op IExp (BaseBVType w)
n' IExp (BaseBVType w)
e

-- | A wrapper around the BV type allowing it to be put into a map or
-- set. We use this to make sure we generate only one instance of each
-- distinct constant.
data BVConst = BVConst (Pair WT.NatRepr BV.BV)
  deriving (BVConst -> BVConst -> Bool
(BVConst -> BVConst -> Bool)
-> (BVConst -> BVConst -> Bool) -> Eq BVConst
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 (tp :: Nat). NatRepr tp -> BV tp -> Ordering)
-> Pair NatRepr BV -> Ordering
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 (tp :: Nat). NatRepr tp -> BV tp -> Ordering)
-> Pair NatRepr BV -> Ordering
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 NatRepr tp -> NatRepr tp -> OrderingF tp tp
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 | BV tp -> BV tp -> Bool
forall (w :: Nat). BV w -> BV w -> Bool
BV.ult BV tp
x BV tp
BV tp
y -> Ordering
LT
        OrderingF tp tp
EQF | BV tp -> BV tp -> Bool
forall (w :: Nat). BV w -> BV w -> Bool
BV.ult BV tp
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

-- | Return the (possibly-cached) name for a literal bitvector value.
litBV ::
  (1 <= w) =>
  WT.NatRepr w ->
  BV.BV w ->
  VerilogM sym n (IExp (WT.BaseBVType w))
litBV :: NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
w BV w
i = do
  Map BVConst Identifier
cache <- ModuleState sym n -> Map BVConst Identifier
forall sym n. ModuleState sym n -> Map BVConst Identifier
vsBVCache (ModuleState sym n -> Map BVConst Identifier)
-> VerilogM sym n (ModuleState sym n)
-> VerilogM sym n (Map BVConst Identifier)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> VerilogM sym n (ModuleState sym n)
forall s (m :: Type -> Type). MonadState s m => m s
get
  case BVConst -> Map BVConst Identifier -> Maybe Identifier
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Pair NatRepr BV -> BVConst
BVConst (NatRepr w -> BV w -> Pair NatRepr BV
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 -> IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BaseTypeRepr (BaseBVType w) -> Identifier -> IExp (BaseBVType w)
forall (tp :: BaseType). BaseTypeRepr tp -> Identifier -> IExp tp
Ident (NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(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) <- Exp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (NatRepr w -> BV w -> Exp (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BV w -> Exp (BaseBVType w)
BVLit NatRepr w
w BV w
i)
      (ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify ((ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ())
-> (ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ()
forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
s -> ModuleState sym n
s { vsBVCache :: Map BVConst Identifier
vsBVCache = BVConst
-> Identifier -> Map BVConst Identifier -> Map BVConst Identifier
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Pair NatRepr BV -> BVConst
BVConst (NatRepr w -> BV w -> Pair NatRepr BV
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 (ModuleState sym n -> Map BVConst Identifier
forall sym n. ModuleState sym n -> Map BVConst Identifier
vsBVCache ModuleState sym n
s) }
      IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
forall (m :: Type -> Type) a. Monad m => a -> m a
return IExp (BaseBVType w)
x

-- | Return the (possibly-cached) name for a literal Boolean value.
litBool :: Bool -> VerilogM sym n (IExp WT.BaseBoolType)
litBool :: Bool -> VerilogM sym n (IExp BaseBoolType)
litBool Bool
b = do
  Map Bool Identifier
cache <- ModuleState sym n -> Map Bool Identifier
forall sym n. ModuleState sym n -> Map Bool Identifier
vsBoolCache (ModuleState sym n -> Map Bool Identifier)
-> VerilogM sym n (ModuleState sym n)
-> VerilogM sym n (Map Bool Identifier)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> VerilogM sym n (ModuleState sym n)
forall s (m :: Type -> Type). MonadState s m => m s
get
  case Bool -> Map Bool Identifier -> Maybe Identifier
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Bool
b Map Bool Identifier
cache of
    Just Identifier
x -> IExp BaseBoolType -> VerilogM sym n (IExp BaseBoolType)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BaseTypeRepr BaseBoolType -> Identifier -> IExp BaseBoolType
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) <- Exp BaseBoolType -> VerilogM sym n (IExp BaseBoolType)
forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (Bool -> Exp BaseBoolType
BoolLit Bool
b)
      (ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify ((ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ())
-> (ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ()
forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
s -> ModuleState sym n
s { vsBoolCache :: Map Bool Identifier
vsBoolCache = Bool -> Identifier -> Map Bool Identifier -> Map Bool Identifier
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Bool
b Identifier
name (ModuleState sym n -> Map Bool Identifier
forall sym n. ModuleState sym n -> Map Bool Identifier
vsBoolCache ModuleState sym n
s) }
      IExp BaseBoolType -> VerilogM sym n (IExp BaseBoolType)
forall (m :: Type -> Type) a. Monad m => a -> m a
return IExp BaseBoolType
x

-- | Apply a unary operation to an expression and bind the result to a
-- new, returned name.
unop :: Unop tp -> IExp tp -> VerilogM sym n (IExp tp)
unop :: Unop tp -> IExp tp -> VerilogM sym n (IExp tp)
unop Unop tp
op IExp tp
e = Exp tp -> VerilogM sym n (IExp tp)
forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (Unop tp -> IExp tp -> Exp tp
forall (tp :: BaseType). Unop tp -> IExp tp -> Exp tp
Unop Unop tp
op IExp tp
e)

-- | Create a conditional, with the given condition, true, and false
-- branches, and bind the result to a new, returned name.
mux ::
  IExp WT.BaseBoolType ->
  IExp tp ->
  IExp tp ->
  VerilogM sym n (IExp tp)
mux :: IExp BaseBoolType -> IExp tp -> IExp tp -> VerilogM sym n (IExp tp)
mux IExp BaseBoolType
e IExp tp
e1 IExp tp
e2 = Exp tp -> VerilogM sym n (IExp tp)
forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (IExp BaseBoolType -> IExp tp -> IExp tp -> Exp tp
forall (tp :: BaseType).
IExp BaseBoolType -> IExp tp -> IExp tp -> Exp tp
Mux IExp BaseBoolType
e IExp tp
e1 IExp tp
e2)

-- | Extract a single bit from a bit vector and bind the result to a
-- new, returned name.
bit ::
  IExp (WT.BaseBVType w) ->
  Integer ->
  VerilogM sym n (IExp WT.BaseBoolType)
bit :: IExp (BaseBVType w)
-> Integer -> VerilogM sym n (IExp BaseBoolType)
bit IExp (BaseBVType w)
e Integer
i = Exp BaseBoolType -> VerilogM sym n (IExp BaseBoolType)
forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (IExp (BaseBVType w) -> Integer -> Exp BaseBoolType
forall (w :: Nat).
IExp (BaseBVType w) -> Integer -> Exp BaseBoolType
Bit IExp (BaseBVType w)
e Integer
i)

-- | Extract a range of bits from a bit vector and bind the result to a
-- new, returned name. The two `NatRepr` values are the starting index
-- and the number of bits to extract, respectively.
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 :: IExp (BaseBVType w)
-> NatRepr idx
-> NatRepr len
-> VerilogM sym n (IExp (BaseBVType len))
bitSelect IExp (BaseBVType w)
e NatRepr idx
start NatRepr len
len = Exp (BaseBVType len) -> VerilogM sym n (IExp (BaseBVType len))
forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (IExp (BaseBVType w)
-> NatRepr idx -> NatRepr len -> Exp (BaseBVType len)
forall (len :: Nat) (start :: Nat) (w :: Nat).
(1 <= len, (start + len) <= w) =>
IExp (BaseBVType w)
-> NatRepr start -> NatRepr len -> Exp (BaseBVType len)
BitSelect IExp (BaseBVType w)
e NatRepr idx
start NatRepr len
len)

-- | Concatenate two bit vectors and bind the result to a new, returned
-- name.
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 :: 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 = Exp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (NatRepr w -> [Some IExp] -> Exp (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> [Some IExp] -> Exp (BaseBVType w)
Concat NatRepr w
w [IExp (BaseBVType w1) -> Some IExp
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some IExp (BaseBVType w1)
e1, IExp (BaseBVType w2) -> Some IExp
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some IExp (BaseBVType w2)
e2])

-- | A data type for items that may show up in a Verilog module.
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

-- | Necessary monadic operations

data ModuleState sym n =
    ModuleState { ModuleState sym n -> [(Some BaseTypeRepr, Identifier)]
vsInputs :: [(Some WT.BaseTypeRepr, Identifier)]
                -- ^ All module inputs, in reverse order.
                , ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsOutputs :: [(Some WT.BaseTypeRepr, Bool, Identifier, Some Exp)]
                -- ^ All module outputs, in reverse order. Includes the
                -- type, signedness, name, and initializer of each.
                , ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsWires :: [(Some WT.BaseTypeRepr, Bool, Identifier, Some Exp)]
                -- ^ All internal wires, in reverse order. Includes the
                -- type, signedness, name, and initializer of each.
                , ModuleState sym n -> Int
vsFreshIdent :: Int
                -- ^ A counter for generating fresh names.
                , ModuleState sym n -> IdxCache n IExp
vsExpCache :: IdxCache n IExp
                -- ^ An expression cache to preserve sharing present in
                -- the What4 representation.
                , ModuleState sym n -> Map BVConst Identifier
vsBVCache :: Map.Map BVConst Identifier
                -- ^ A cache of bit vector constants, to avoid duplicating constant declarations.
                , ModuleState sym n -> Map Bool Identifier
vsBoolCache :: Map.Map Bool Identifier
                -- ^ A cache of Boolean constants, to avoid duplicating constant declarations.
                , ModuleState sym n -> sym
vsSym :: sym
                -- ^ The What4 symbolic backend to use with `vsBVCache`.
                }

newtype VerilogM sym n a =
 VerilogM (StateT (ModuleState sym n) (ExceptT String IO) a)
 deriving ( a -> VerilogM sym n b -> VerilogM sym n a
(a -> b) -> VerilogM sym n a -> VerilogM sym n b
(forall a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b)
-> (forall a b. a -> VerilogM sym n b -> VerilogM sym n a)
-> Functor (VerilogM sym n)
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
<$ :: 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 :: (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
          , Functor (VerilogM sym n)
a -> VerilogM sym n a
Functor (VerilogM sym n)
-> (forall a. a -> VerilogM sym n a)
-> (forall a b.
    VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b)
-> (forall 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 -> VerilogM sym n b -> VerilogM sym n b)
-> (forall a b.
    VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a)
-> Applicative (VerilogM sym n)
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a
VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
(a -> b -> c)
-> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
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
<* :: 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
*> :: 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 :: (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
<*> :: 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 :: a -> VerilogM sym n a
$cpure :: forall sym n a. a -> VerilogM sym n a
$cp1Applicative :: forall sym n. Functor (VerilogM sym n)
Applicative
          , Applicative (VerilogM sym n)
a -> VerilogM sym n a
Applicative (VerilogM sym n)
-> (forall a b.
    VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b)
-> (forall a b.
    VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b)
-> (forall a. a -> VerilogM sym n a)
-> Monad (VerilogM sym n)
VerilogM sym n a -> (a -> VerilogM sym n b) -> VerilogM sym n b
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
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 :: a -> VerilogM sym n a
$creturn :: forall sym n a. a -> VerilogM sym n a
>> :: 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
>>= :: 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
$cp1Monad :: forall sym n. Applicative (VerilogM sym n)
Monad
          , MonadState (ModuleState sym n)
          , MonadError String
          , Monad (VerilogM sym n)
Monad (VerilogM sym n)
-> (forall a. IO a -> VerilogM sym n a) -> MonadIO (VerilogM sym n)
IO a -> VerilogM sym n a
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 :: IO a -> VerilogM sym n a
$cliftIO :: forall sym n a. IO a -> VerilogM sym n a
$cp1MonadIO :: forall sym n. Monad (VerilogM sym n)
MonadIO
          )


newtype Module sym n = Module (ModuleState sym n)

-- | Create a Verilog module in the context of a given What4 symbolic
-- backend and a monadic computation that returns an expression name
-- that corresponds to the module's output.
mkModule ::
  sym ->
  VerilogM sym n (IExp tp) ->
  ExceptT String IO (Module sym n)
mkModule :: sym
-> VerilogM sym n (IExp tp) -> ExceptT Identifier IO (Module sym n)
mkModule sym
sym VerilogM sym n (IExp tp)
op = (ModuleState sym n -> Module sym n)
-> ExceptT Identifier IO (ModuleState sym n)
-> ExceptT Identifier IO (Module sym n)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ModuleState sym n -> Module sym n
forall sym n. ModuleState sym n -> Module sym n
Module (ExceptT Identifier IO (ModuleState sym n)
 -> ExceptT Identifier IO (Module sym n))
-> ExceptT Identifier IO (ModuleState sym n)
-> ExceptT Identifier IO (Module sym n)
forall a b. (a -> b) -> a -> b
$ sym
-> VerilogM sym n () -> ExceptT Identifier IO (ModuleState sym n)
forall sym n a.
sym
-> VerilogM sym n a -> ExceptT Identifier IO (ModuleState sym n)
execVerilogM sym
sym (VerilogM sym n () -> ExceptT Identifier IO (ModuleState sym n))
-> VerilogM sym n () -> ExceptT Identifier IO (ModuleState sym n)
forall a b. (a -> b) -> a -> b
$ do
    IExp tp
e <- VerilogM sym n (IExp tp)
op
    Identifier
out <- Identifier -> VerilogM sym n Identifier
forall sym n. Identifier -> VerilogM sym n Identifier
freshIdentifier Identifier
"out"
    BaseTypeRepr tp -> Identifier -> Exp tp -> VerilogM sym n ()
forall (tp :: BaseType) sym n.
BaseTypeRepr tp -> Identifier -> Exp tp -> VerilogM sym n ()
addOutput (IExp tp -> BaseTypeRepr tp
forall (tp :: BaseType). IExp tp -> BaseTypeRepr tp
iexpType IExp tp
e) Identifier
out (IExp tp -> Exp tp
forall (tp :: BaseType). IExp tp -> Exp tp
IExp IExp tp
e)

initModuleState :: sym -> IO (ModuleState sym n)
initModuleState :: sym -> IO (ModuleState sym n)
initModuleState sym
sym = do
  IdxCache n IExp
cache <- IO (IdxCache n IExp)
forall (m :: Type -> Type) t (f :: BaseType -> Type).
MonadIO m =>
m (IdxCache t f)
newIdxCache
  ModuleState sym n -> IO (ModuleState sym n)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ModuleState sym n -> IO (ModuleState sym n))
-> ModuleState sym n -> IO (ModuleState sym n)
forall a b. (a -> b) -> a -> b
$ [(Some BaseTypeRepr, Identifier)]
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
-> Int
-> IdxCache n IExp
-> Map BVConst Identifier
-> Map Bool Identifier
-> sym
-> ModuleState sym n
forall sym n.
[(Some BaseTypeRepr, Identifier)]
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
-> Int
-> IdxCache n IExp
-> Map BVConst Identifier
-> Map Bool Identifier
-> sym
-> ModuleState sym n
ModuleState [] [] [] Int
0 IdxCache n IExp
cache Map BVConst Identifier
forall k a. Map k a
Map.empty Map Bool Identifier
forall k a. Map k a
Map.empty sym
sym

runVerilogM ::
  VerilogM sym n a ->
  ModuleState sym n ->
  ExceptT String IO (a, ModuleState sym n)
runVerilogM :: VerilogM sym n a
-> ModuleState sym n
-> ExceptT Identifier IO (a, ModuleState sym n)
runVerilogM (VerilogM StateT (ModuleState sym n) (ExceptT Identifier IO) a
op) = StateT (ModuleState sym n) (ExceptT Identifier IO) a
-> ModuleState sym n
-> ExceptT Identifier IO (a, ModuleState sym n)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT StateT (ModuleState sym n) (ExceptT Identifier IO) a
op

execVerilogM ::
  sym ->
  VerilogM sym n a ->
  ExceptT String IO (ModuleState sym n)
execVerilogM :: sym
-> VerilogM sym n a -> ExceptT Identifier IO (ModuleState sym n)
execVerilogM sym
sym VerilogM sym n a
op =
  do ModuleState sym n
s <- IO (ModuleState sym n) -> ExceptT Identifier IO (ModuleState sym n)
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (ModuleState sym n)
 -> ExceptT Identifier IO (ModuleState sym n))
-> IO (ModuleState sym n)
-> ExceptT Identifier IO (ModuleState sym n)
forall a b. (a -> b) -> a -> b
$ sym -> IO (ModuleState sym n)
forall sym n. sym -> IO (ModuleState sym n)
initModuleState sym
sym
     (a
_a,ModuleState sym n
m) <- VerilogM sym n a
-> ModuleState sym n
-> ExceptT Identifier IO (a, ModuleState sym n)
forall sym n a.
VerilogM sym n a
-> ModuleState sym n
-> ExceptT Identifier IO (a, ModuleState sym n)
runVerilogM VerilogM sym n a
op ModuleState sym n
s
     ModuleState sym n -> ExceptT Identifier IO (ModuleState sym n)
forall (m :: Type -> Type) a. Monad m => a -> m a
return ModuleState sym n
m

-- | Returns and records a fresh input with the given type and with a
-- name constructed from the given base.
addFreshInput ::
  WT.BaseTypeRepr tp ->
  Identifier ->
  VerilogM sym n Identifier
addFreshInput :: BaseTypeRepr tp -> Identifier -> VerilogM sym n Identifier
addFreshInput BaseTypeRepr tp
tp Identifier
base = do
  Identifier
name <- Identifier -> VerilogM sym n Identifier
forall sym n. Identifier -> VerilogM sym n Identifier
freshIdentifier Identifier
base
  (ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify ((ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ())
-> (ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ()
forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
st -> ModuleState sym n
st { vsInputs :: [(Some BaseTypeRepr, Identifier)]
vsInputs = (BaseTypeRepr tp -> Some BaseTypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr tp
tp, Identifier
name) (Some BaseTypeRepr, Identifier)
-> [(Some BaseTypeRepr, Identifier)]
-> [(Some BaseTypeRepr, Identifier)]
forall a. a -> [a] -> [a]
: ModuleState sym n -> [(Some BaseTypeRepr, Identifier)]
forall sym n.
ModuleState sym n -> [(Some BaseTypeRepr, Identifier)]
vsInputs ModuleState sym n
st }
  Identifier -> VerilogM sym n Identifier
forall (m :: Type -> Type) a. Monad m => a -> m a
return Identifier
name

-- | Add an output to the current Verilog module state, given a type, a
-- name, and an initializer expression.
addOutput ::
  WT.BaseTypeRepr tp ->
  Identifier ->
  Exp tp ->
  VerilogM sym n ()
addOutput :: BaseTypeRepr tp -> Identifier -> Exp tp -> VerilogM sym n ()
addOutput BaseTypeRepr tp
tp Identifier
name Exp tp
e =
  (ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify ((ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ())
-> (ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ()
forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
st -> ModuleState sym n
st { vsOutputs :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsOutputs = (BaseTypeRepr tp -> Some BaseTypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr tp
tp, Bool
False, Identifier
name, Exp tp -> Some Exp
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Exp tp
e) (Some BaseTypeRepr, Bool, Identifier, Some Exp)
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
forall a. a -> [a] -> [a]
: ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
forall sym n.
ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsOutputs ModuleState sym n
st }

-- | Add a new wire to the current Verilog module state, given a type, a
-- signedness flag, a name, and an initializer expression.
addWire ::
  WT.BaseTypeRepr tp ->
  Bool ->
  Identifier ->
  Exp tp ->
  VerilogM sym n ()
addWire :: BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n ()
addWire BaseTypeRepr tp
tp Bool
isSigned Identifier
name Exp tp
e =
  (ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify ((ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ())
-> (ModuleState sym n -> ModuleState sym n) -> VerilogM sym n ()
forall a b. (a -> b) -> a -> b
$ \ModuleState sym n
st -> ModuleState sym n
st { vsWires :: [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsWires = (BaseTypeRepr tp -> Some BaseTypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr tp
tp, Bool
isSigned, Identifier
name, Exp tp -> Some Exp
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Exp tp
e) (Some BaseTypeRepr, Bool, Identifier, Some Exp)
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
forall a. a -> [a] -> [a]
: ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
forall sym n.
ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsWires ModuleState sym n
st }

-- | Create a fresh identifier by concatenating the given base with the
-- current fresh identifier counter.
freshIdentifier :: String -> VerilogM sym n Identifier
freshIdentifier :: Identifier -> VerilogM sym n Identifier
freshIdentifier Identifier
basename = do
  ModuleState sym n
st <- VerilogM sym n (ModuleState sym n)
forall s (m :: Type -> Type). MonadState s m => m s
get
  let x :: Int
x = ModuleState sym n -> Int
forall sym n. ModuleState sym n -> Int
vsFreshIdent ModuleState sym n
st
  ModuleState sym n -> VerilogM sym n ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put (ModuleState sym n -> VerilogM sym n ())
-> ModuleState sym n -> VerilogM sym n ()
forall a b. (a -> b) -> a -> b
$ ModuleState sym n
st { vsFreshIdent :: Int
vsFreshIdent = Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 }
  Identifier -> VerilogM sym n Identifier
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Identifier -> VerilogM sym n Identifier)
-> Identifier -> VerilogM sym n Identifier
forall a b. (a -> b) -> a -> b
$ Identifier
basename Identifier -> Identifier -> Identifier
forall a. [a] -> [a] -> [a]
++ Identifier
"_" Identifier -> Identifier -> Identifier
forall a. [a] -> [a] -> [a]
++ Int -> Identifier
forall a. Show a => a -> Identifier
show Int
x


-- | Add a new wire to the current Verilog module state, given a type, a
-- signedness flag, the prefix of a name, and an initializer expression.
-- The name prefix will be freshened by appending current value of the
-- fresh variable counter.
addFreshWire ::
  WT.BaseTypeRepr tp ->
  Bool ->
  String ->
  Exp tp ->
  VerilogM sym n Identifier
addFreshWire :: BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n Identifier
addFreshWire BaseTypeRepr tp
repr Bool
isSigned Identifier
basename Exp tp
e = do
  Identifier
x <- Identifier -> VerilogM sym n Identifier
forall sym n. Identifier -> VerilogM sym n Identifier
freshIdentifier Identifier
basename
  BaseTypeRepr tp
-> Bool -> Identifier -> Exp tp -> VerilogM sym n ()
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
  Identifier -> VerilogM sym n Identifier
forall (m :: Type -> Type) a. Monad m => a -> m a
return Identifier
x