{-
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,
  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 (forM_)
import           Control.Monad.Except (ExceptT, MonadError(..))
import           Control.Monad.IO.Class (MonadIO(..))
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

-- | 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 :: forall (inTp :: BaseType) (outTp :: BaseType).
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 :: forall (tp :: BaseType). 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 :: forall (tp :: BaseType). 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 :: Natural).
(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 :: Natural).
(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 :: Natural).
(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 :: forall (tp :: BaseType) sym n. Exp tp -> VerilogM sym n (IExp tp)
mkLet (IExp IExp tp
x) = IExp tp -> VerilogM sym n (IExp tp)
forall a. a -> VerilogM sym n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return IExp tp
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
"wr" Exp tp
e
    IExp tp -> VerilogM sym n (IExp tp)
forall a. a -> VerilogM sym n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (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 :: forall (tp :: BaseType) sym n. 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
"wr" (IExp tp -> Exp tp
forall (tp :: BaseType). IExp tp -> Exp tp
IExp IExp tp
e)
    IExp tp -> VerilogM sym n (IExp tp)
forall a. a -> VerilogM sym n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (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 :: 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 = 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 (w :: BaseType) (outTp :: BaseType).
Binop w outTp -> IExp w -> IExp w -> 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 :: 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' <- NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
forall (w :: Natural) sym n.
(1 <= w) =>
NatRepr w -> BV w -> VerilogM sym n (IExp (BaseBVType w))
litBV NatRepr w
w BV w
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
$c== :: BVConst -> BVConst -> Bool
== :: BVConst -> BVConst -> Bool
$c/= :: BVConst -> BVConst -> Bool
/= :: 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 :: Natural). 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 :: Natural). 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 (x :: Natural) (y :: Natural).
NatRepr x -> NatRepr y -> OrderingF x y
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 :: Natural). 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 :: Natural). 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 :: 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 <- 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 a. a -> VerilogM sym n a
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 :: 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) <- 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 :: Natural).
(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.insert (BVConst (Pair w i)) name (vsBVCache s) }
      IExp (BaseBVType w) -> VerilogM sym n (IExp (BaseBVType w))
forall a. a -> VerilogM sym n a
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 :: forall sym n. 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 a. a -> VerilogM sym n a
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.insert b name (vsBoolCache s) }
      IExp 'BaseBoolType -> VerilogM sym n (IExp 'BaseBoolType)
forall a. a -> VerilogM sym n a
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 :: forall (tp :: BaseType) sym n.
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 :: 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 = 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 :: forall (w :: Natural) sym n.
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 :: Natural).
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 :: 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 = 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 (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)

-- | 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 :: 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 = 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 :: Natural).
(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 { forall sym n.
ModuleState sym n -> [(Word64, Some BaseTypeRepr, Identifier)]
vsInputs :: [(Word64, Some WT.BaseTypeRepr, Identifier)]
                -- ^ All module inputs, in reverse order. We use Word64 for Nonces to avoid GHC bugs.
                -- For more detail:
                --   https://gitlab.haskell.org/ghc/ghc/-/issues/2595
                --   https://gitlab.haskell.org/ghc/ghc/-/issues/10856
                --   https://gitlab.haskell.org/ghc/ghc/-/issues/16501
                , forall sym n.
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.
                , forall sym n.
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.
                , forall sym n. ModuleState sym n -> Map Word64 Identifier
vsSeenNonces :: Map.Map Word64 Identifier
                -- ^ A map from the identifier nonces seen so far to
                -- their identifier names. These nonces exist for
                -- identifiers from the original term, but not
                -- intermediate Verilog variables.
                , forall sym n. ModuleState sym n -> Set Identifier
vsUsedIdentifiers :: Set.Set Identifier
                -- ^ A set of all the identifiers used so far, including
                -- intermediate Verilog variables.
                , forall sym n. ModuleState sym n -> IdxCache n IExp
vsExpCache :: IdxCache n IExp
                -- ^ An expression cache to preserve sharing present in
                -- the What4 representation.
                , forall sym n. ModuleState sym n -> Map BVConst Identifier
vsBVCache :: Map.Map BVConst Identifier
                -- ^ A cache of bit vector constants, to avoid duplicating constant declarations.
                , forall sym n. ModuleState sym n -> Map Bool Identifier
vsBoolCache :: Map.Map Bool Identifier
                -- ^ A cache of Boolean constants, to avoid duplicating constant declarations.
                , forall sym n. 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 ( (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
$cfmap :: forall sym n a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b
fmap :: forall a b. (a -> b) -> VerilogM sym n a -> VerilogM sym n b
$c<$ :: forall sym n a b. a -> VerilogM sym n b -> VerilogM sym n a
<$ :: forall a b. a -> VerilogM sym n b -> VerilogM sym n a
Functor
          , Functor (VerilogM sym n)
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)
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
$cpure :: forall sym n a. a -> VerilogM sym n a
pure :: forall a. a -> VerilogM sym n a
$c<*> :: forall sym n a b.
VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
<*> :: forall a b.
VerilogM sym n (a -> b) -> VerilogM sym n a -> VerilogM sym n b
$cliftA2 :: forall sym n a b c.
(a -> b -> c)
-> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
liftA2 :: forall a b c.
(a -> b -> c)
-> VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n c
$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 -> 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 a
<* :: forall a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n a
Applicative
          , Applicative (VerilogM sym n)
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)
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
$c>>= :: forall sym n a b.
VerilogM sym n a -> (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 -> VerilogM sym n b -> VerilogM sym n b
>> :: forall a b.
VerilogM sym n a -> VerilogM sym n b -> VerilogM sym n b
$creturn :: forall sym n a. a -> VerilogM sym n a
return :: forall a. a -> VerilogM sym n a
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)
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
$cliftIO :: forall sym n a. IO a -> VerilogM sym n a
liftIO :: forall a. IO a -> VerilogM sym n a
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 ->
  [(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 = (ModuleState sym n -> Module sym n)
-> ExceptT String IO (ModuleState sym n)
-> ExceptT String IO (Module sym n)
forall a b. (a -> b) -> ExceptT String IO a -> ExceptT String IO b
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 String IO (ModuleState sym n)
 -> ExceptT String IO (Module sym n))
-> ExceptT String IO (ModuleState sym n)
-> ExceptT String IO (Module sym n)
forall a b. (a -> b) -> a -> b
$ sym -> VerilogM sym n () -> ExceptT String IO (ModuleState sym n)
forall sym n a.
sym -> VerilogM sym n a -> ExceptT String IO (ModuleState sym n)
execVerilogM sym
sym (VerilogM sym n () -> ExceptT String IO (ModuleState sym n))
-> VerilogM sym n () -> ExceptT String IO (ModuleState sym n)
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) -> ExprBoundVar n x -> Identifier -> VerilogM sym n Identifier
forall n (tp :: BaseType) sym.
ExprBoundVar n tp -> Identifier -> VerilogM sym n Identifier
addBoundInput ExprBoundVar n x
x Identifier
ident
            Some (Expr n)
_ -> String -> VerilogM sym n Identifier
forall a. String -> VerilogM sym n a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Input provided to mkModule isn't an input"
    ((Some (Expr n), Identifier) -> VerilogM sym n Identifier)
-> [(Some (Expr n), Identifier)] -> VerilogM sym n ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Some (Expr n) -> Identifier -> VerilogM sym n Identifier)
-> (Some (Expr n), Identifier) -> VerilogM sym n Identifier
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Some (Expr n) -> Identifier -> VerilogM sym n Identifier
forall {n} {sym}.
Some (Expr n) -> Identifier -> VerilogM sym n Identifier
addExprInput) [(Some (Expr n), Identifier)]
ins
    [Some IExp]
es <- [VerilogM sym n (Some IExp)] -> VerilogM sym n [Some IExp]
forall (t :: Type -> Type) (m :: Type -> Type) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: Type -> Type) a. Monad m => [m a] -> m [a]
sequence [VerilogM sym n (Some IExp)]
ops
    [Some IExp]
-> (Some IExp -> VerilogM sym n ()) -> VerilogM sym n ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Some IExp]
es ((Some IExp -> VerilogM sym n ()) -> VerilogM sym n ())
-> (Some IExp -> VerilogM sym n ()) -> VerilogM sym n ()
forall a b. (a -> b) -> a -> b
$ \Some IExp
se ->
      do Identifier
out <- Identifier -> VerilogM sym n Identifier
forall sym n. Identifier -> VerilogM sym n Identifier
freshIdentifier Identifier
"out"
         (forall (tp :: BaseType). IExp tp -> VerilogM sym n ())
-> Some IExp -> VerilogM sym n ()
forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome (\IExp tp
e -> 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)) 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 <- 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 a. a -> IO a
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
$ 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 = Map Word64 Identifier
forall k a. Map k a
Map.empty
           , vsUsedIdentifiers :: Set Identifier
vsUsedIdentifiers = Set Identifier
forall a. Set a
Set.empty
           , vsExpCache :: IdxCache n IExp
vsExpCache = IdxCache n IExp
cache
           , vsBVCache :: Map BVConst Identifier
vsBVCache = Map BVConst Identifier
forall k a. Map k a
Map.empty
           , vsBoolCache :: Map Bool Identifier
vsBoolCache = Map Bool Identifier
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) = StateT (ModuleState sym n) (ExceptT String IO) a
-> ModuleState sym n -> ExceptT String 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 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 <- IO (ModuleState sym n) -> ExceptT String IO (ModuleState sym n)
forall a. IO a -> ExceptT String IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (ModuleState sym n) -> ExceptT String IO (ModuleState sym n))
-> IO (ModuleState sym n) -> ExceptT String 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 String IO (a, ModuleState sym n)
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
     ModuleState sym n -> ExceptT String IO (ModuleState sym n)
forall a. a -> ExceptT String IO a
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 =
  Some (Nonce n)
-> Some BaseTypeRepr -> Identifier -> VerilogM sym n Identifier
forall {k} n sym.
Some (Nonce n)
-> Some BaseTypeRepr -> Identifier -> VerilogM sym n Identifier
addFreshInput (Nonce n tp -> Some (Nonce n)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Nonce n tp
idx) (BaseTypeRepr tp -> Some BaseTypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr tp
tp) Identifier
ident
    where
      tp :: BaseTypeRepr tp
tp = ExprBoundVar n tp -> BaseTypeRepr tp
forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
bvarType ExprBoundVar n tp
x
      idx :: Nonce n tp
idx = ExprBoundVar n tp -> Nonce n tp
forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar n tp
x

-- | Returns and records a fresh input with the given type and with a
-- name constructed from the given base.
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 <- (ModuleState sym n -> Map Word64 Identifier)
-> VerilogM sym n (Map Word64 Identifier)
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets ModuleState sym n -> Map Word64 Identifier
forall sym n. ModuleState sym n -> Map Word64 Identifier
vsSeenNonces
  let idx :: Word64
idx = (forall (tp :: k). Nonce n tp -> Word64)
-> Some (Nonce n) -> Word64
forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome Nonce n tp -> Word64
forall (tp :: k). Nonce n tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue Some (Nonce n)
n
  case Word64 -> Map Word64 Identifier -> Maybe Identifier
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Word64
idx Map Word64 Identifier
seenNonces of
    Just Identifier
ident -> Identifier -> VerilogM sym n Identifier
forall a. a -> VerilogM sym n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Identifier
ident
    Maybe Identifier
Nothing ->
      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 = (idx, tp, name) : vsInputs st
                            , vsSeenNonces = Map.insert idx name seenNonces
                            }
         Identifier -> VerilogM sym n Identifier
forall a. a -> VerilogM sym n a
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 :: forall (tp :: BaseType) sym n.
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 tp, False, name, Some e) : vsOutputs 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 :: 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 =
  (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 tp, isSigned, name, Some e) : vsWires st }

-- | Create a fresh identifier by concatenating the given base with the
-- current fresh identifier counter.
freshIdentifier :: T.Text -> VerilogM sym n Identifier
freshIdentifier :: forall sym n. 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 used :: Set Identifier
used = ModuleState sym n -> Set Identifier
forall sym n. ModuleState sym n -> Set Identifier
vsUsedIdentifiers ModuleState sym n
st
  let nm :: Identifier
nm | Identifier
basename Identifier -> Set Identifier -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Identifier
used =
             [Identifier] -> Identifier
T.concat [Identifier
basename, Identifier
"_", String -> Identifier
forall a. IsString a => String -> a
fromString (String -> Identifier) -> String -> Identifier
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ Set Identifier -> Int
forall a. Set a -> Int
Set.size Set Identifier
used ]
         | Bool
otherwise = Identifier
basename
  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 { vsUsedIdentifiers = Set.insert nm used }
  Identifier -> VerilogM sym n Identifier
forall a. a -> VerilogM sym n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Identifier
nm

-- | 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 ->
  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 <- 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 a. a -> VerilogM sym n a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Identifier
x