    {-# LANGUAGE OverloadedStrings #-}

    module Clash.Primitives.Verification (checkBBF) where

    import Data.Either

    import qualified Control.Lens                    as Lens
    import           Control.Monad.State             (State)
    import           Data.List.Infinite              (Infinite(..), (...))
    import           Data.Maybe                      (listToMaybe)
    import           Data.Monoid                     (Ap(getAp))
    import           Data.Text.Prettyprint.Doc.Extra (Doc)
    import qualified Data.Text                       as Text
    import           GHC.Stack                       (HasCallStack)

    import           Clash.Annotations.Primitive     (HDL(..))
    import           Clash.Backend
      (Backend, blockDecl, hdlKind)
    import           Clash.Core.HasType
    import           Clash.Core.Term                 (Term(Var), varToId)
    import           Clash.Core.TermLiteral          (termToDataError)
    import           Clash.Util                      (indexNote)
    import           Clash.Netlist                   (mkExpr)
    import           Clash.Netlist.Util              (stripVoid)
    import qualified Clash.Netlist.Id                as Id
    import           Clash.Netlist.Types
      (BlackBox(BBFunction), TemplateFunction(..), BlackBoxContext, Identifier,
       NetlistMonad, Declaration(Assignment, NetDecl), Usage(Cont),
       HWType(Bool, KnownDomain), NetlistId(..),
       DeclarationType(Concurrent), tcCache, bbInputs, Expr(Identifier))
    import           Clash.Netlist.BlackBox.Types
      (BlackBoxFunction, BlackBoxMeta(..), TemplateKind(TDecl), RenderVoid(..),
       emptyBlackBoxMeta)

    import           Clash.Verification.Internal
    import           Clash.Verification.Pretty

    checkBBF :: BlackBoxFunction
    checkBBF :: BlackBoxFunction
    checkBBF Bool
    _isD Text
    _primName [Either Term Type]
    args [Type]
    _ty =
      case Either String (Text, RenderAs, Property' (Maybe String, Term))
    litArgs of
        Left String
    err -> Either String (BlackBoxMeta, BlackBox)
    -> NetlistMonad (Either String (BlackBoxMeta, BlackBox))
    forall a. a -> NetlistMonad a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (String -> Either String (BlackBoxMeta, BlackBox)
    forall a b. a -> Either a b
    Left String
    err)
        Right (Text
    propName, RenderAs
    renderAs, Property' (Maybe String, Term)
    cvProperty0) -> do
          Property' (Identifier, [Declaration])
    cvProperty1 <- ((Maybe String, Term) -> NetlistMonad (Identifier, [Declaration]))
    -> Property' (Maybe String, Term)
    -> NetlistMonad (Property' (Identifier, [Declaration]))
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Property' a -> m (Property' b)
    mapM ((Maybe String -> Term -> NetlistMonad (Identifier, [Declaration]))
    -> (Maybe String, Term) -> NetlistMonad (Identifier, [Declaration])
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Maybe String -> Term -> NetlistMonad (Identifier, [Declaration])
    bindMaybe) Property' (Maybe String, Term)
    cvProperty0
          let decls :: [Declaration]
    decls = ((Identifier, [Declaration]) -> [Declaration])
    -> Property' (Identifier, [Declaration]) -> [Declaration]
    forall (t :: Type -> Type) a b.
    Foldable t =>
    (a -> [b]) -> t a -> [b]
    concatMap (Identifier, [Declaration]) -> [Declaration]
    forall a b. (a, b) -> b
    snd Property' (Identifier, [Declaration])
    cvProperty1
              cvProperty2 :: Property' Identifier
    cvProperty2 = ((Identifier, [Declaration]) -> Identifier)
    -> Property' (Identifier, [Declaration]) -> Property' Identifier
    forall a b. (a -> b) -> Property' a -> Property' b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Identifier, [Declaration]) -> Identifier
    forall a b. (a, b) -> a
    fst Property' (Identifier, [Declaration])
    cvProperty1
          Either String (BlackBoxMeta, BlackBox)
    -> NetlistMonad (Either String (BlackBoxMeta, BlackBox))
    forall a. a -> NetlistMonad a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure ((BlackBoxMeta, BlackBox) -> Either String (BlackBoxMeta, BlackBox)
    forall a b. b -> Either a b
    Right (BlackBoxMeta
    meta, TemplateFunction -> BlackBox
    bb ([Declaration]
    -> (Expr, Identifier)
    -> Text
    -> RenderAs
    -> Property' Identifier
    -> TemplateFunction
    checkTF [Declaration]
    decls (Expr
    clkExpr, Identifier
    clkId) Text
    propName RenderAs
    renderAs Property' Identifier
    cvProperty2)))
     where
      -- TODO: Improve error handling; currently errors don't indicate what
      -- TODO: blackbox generated them.
      Int
    _knownDomainArg
        :< Int
    clkArg
        :< Int
    _rstArg
        :< Int
    propNameArg
        :< Int
    renderAsArg
        :< Int
    propArg
        :< Infinite Int
    _ = ((Int
    0 :: Int)...)
      (HasCallStack => Id -> Identifier
    Id -> Identifier
    Id.unsafeFromCoreId -> Identifier
    clkId) = Term -> Id
    varToId (String -> [Term] -> Int -> Term
    forall a. HasCallStack => String -> [a] -> Int -> a
    indexNote String
    "clk" ([Either Term Type] -> [Term]
    forall a b. [Either a b] -> [a]
    lefts [Either Term Type]
    args) Int
    clkArg)
      clkExpr :: Expr
    clkExpr = Identifier -> Maybe Modifier -> Expr
    Identifier Identifier
    clkId Maybe Modifier
    forall a. Maybe a
    Nothing

      litArgs :: Either String (Text, RenderAs, Property' (Maybe String, Term))
    litArgs = do
        Text
    propName <- Term -> Either String Text
    forall a. TermLiteral a => Term -> Either String a
    termToDataError (String -> [Term] -> Int -> Term
    forall a. HasCallStack => String -> [a] -> Int -> a
    indexNote String
    "propName" ([Either Term Type] -> [Term]
    forall a b. [Either a b] -> [a]
    lefts [Either Term Type]
    args) Int
    propNameArg)
        RenderAs
    renderAs <- Term -> Either String RenderAs
    forall a. TermLiteral a => Term -> Either String a
    termToDataError (String -> [Term] -> Int -> Term
    forall a. HasCallStack => String -> [a] -> Int -> a
    indexNote String
    "renderAs" ([Either Term Type] -> [Term]
    forall a b. [Either a b] -> [a]
    lefts [Either Term Type]
    args) Int
    renderAsArg)
        Property' (Maybe String, Term)
    cvProperty <- Term -> Either String (Property' (Maybe String, Term))
    forall a. TermLiteral a => Term -> Either String a
    termToDataError (String -> [Term] -> Int -> Term
    forall a. HasCallStack => String -> [a] -> Int -> a
    indexNote String
    "propArg" ([Either Term Type] -> [Term]
    forall a b. [Either a b] -> [a]
    lefts [Either Term Type]
    args) Int
    propArg)
        (Text, RenderAs, Property' (Maybe String, Term))
    -> Either String (Text, RenderAs, Property' (Maybe String, Term))
    forall a b. b -> Either a b
    Right (Text
    propName, RenderAs
    renderAs, Property' (Maybe String, Term)
    cvProperty)

      bb :: TemplateFunction -> BlackBox
    bb = String -> Int -> TemplateFunction -> BlackBox
    BBFunction String
    "Clash.Primitives.Verification.checkTF" Int
    0
      meta :: BlackBoxMeta
    meta = BlackBoxMeta
    emptyBlackBoxMeta {bbKind :: TemplateKind
    bbKind=TemplateKind
    TDecl, bbRenderVoid :: RenderVoid
    bbRenderVoid=RenderVoid
    RenderVoid}

      bindMaybe
        :: Maybe String
        -- ^ Hint for new identifier
        -> Term
        -- ^ Term to bind. Does not bind if it's already a reference to a signal
        -> NetlistMonad (Identifier, [Declaration])
        -- ^ ([new] reference to signal, [declarations need to get it in scope])
      bindMaybe :: Maybe String -> Term -> NetlistMonad (Identifier, [Declaration])
    bindMaybe Maybe String
    _ (Var Id
    vId) = (Identifier, [Declaration])
    -> NetlistMonad (Identifier, [Declaration])
    forall a. a -> NetlistMonad a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (HasCallStack => Id -> Identifier
    Id -> Identifier
    Id.unsafeFromCoreId Id
    vId, [])
      bindMaybe Maybe String
    Nothing Term
    t = Maybe String -> Term -> NetlistMonad (Identifier, [Declaration])
    bindMaybe (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "s") Term
    t
      bindMaybe (Just String
    nm) Term
    t = do
        TyConMap
    tcm <- Getting TyConMap NetlistEnv TyConMap -> NetlistMonad TyConMap
    forall s (m :: Type -> Type) a.
    MonadReader s m =>
    Getting a s a -> m a
    Lens.view Getting TyConMap NetlistEnv TyConMap
    Getter NetlistEnv TyConMap
    tcCache
        Identifier
    newId <- Text -> NetlistMonad Identifier
    forall (m :: Type -> Type).
    (HasCallStack, IdentifierSetMonad m) =>
    Text -> m Identifier
    Id.make (String -> Text
    Text.pack String
    nm)
        (Expr
    expr0, [Declaration]
    decls) <- HasCallStack =>
    Bool
    -> DeclarationType
    -> NetlistId
    -> Term
    -> NetlistMonad (Expr, [Declaration])
    Bool
    -> DeclarationType
    -> NetlistId
    -> Term
    -> NetlistMonad (Expr, [Declaration])
    mkExpr Bool
    False DeclarationType
    Concurrent (Identifier -> Type -> NetlistId
    NetlistId Identifier
    newId (TyConMap -> Term -> Type
    forall a. InferType a => TyConMap -> a -> Type
    inferCoreTypeOf TyConMap
    tcm Term
    t)) Term
    t
        (Identifier, [Declaration])
    -> NetlistMonad (Identifier, [Declaration])
    forall a. a -> NetlistMonad a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure
          ( Identifier
    newId
          , [Declaration]
    decls [Declaration] -> [Declaration] -> [Declaration]
    forall a. [a] -> [a] -> [a]
    ++ [HWType -> Identifier -> Declaration
    sigDecl HWType
    Bool Identifier
    newId, Identifier -> Usage -> Expr -> Declaration
    Assignment Identifier
    newId Usage
    Cont Expr
    expr0] )

      -- Simple wire without comment
      sigDecl :: HWType -> Identifier -> Declaration
      sigDecl :: HWType -> Identifier -> Declaration
    sigDecl HWType
    typ Identifier
    nm = Maybe Text -> Identifier -> HWType -> Declaration
    NetDecl Maybe Text
    forall a. Maybe a
    Nothing Identifier
    nm HWType
    typ

    checkTF
      :: [Declaration]
      -> (Expr, Identifier)
      -> Text.Text
      -> RenderAs
      -> Property' Identifier
      -> TemplateFunction
    checkTF :: [Declaration]
    -> (Expr, Identifier)
    -> Text
    -> RenderAs
    -> Property' Identifier
    -> TemplateFunction
    checkTF [Declaration]
    decls (Expr, Identifier)
    clk Text
    propName RenderAs
    renderAs Property' Identifier
    prop =
      [Int]
    -> (BlackBoxContext -> Bool)
    -> (forall s. Backend s => BlackBoxContext -> State s Doc)
    -> TemplateFunction
    TemplateFunction [] (Bool -> BlackBoxContext -> Bool
    forall a b. a -> b -> a
    const Bool
    True) ([Declaration]
    -> (Expr, Identifier)
    -> Text
    -> RenderAs
    -> Property' Identifier
    -> BlackBoxContext
    -> State s Doc
    forall s.
    (HasCallStack, Backend s) =>
    [Declaration]
    -> (Expr, Identifier)
    -> Text
    -> RenderAs
    -> Property' Identifier
    -> BlackBoxContext
    -> State s Doc
    checkTF' [Declaration]
    decls (Expr, Identifier)
    clk Text
    propName RenderAs
    renderAs Property' Identifier
    prop)

    checkTF'
      :: forall s
       . (HasCallStack, Backend s)
      => [Declaration]
      -- ^ Extra decls needed
      -> (Expr, Identifier)
      -- ^ Clock
      -> Text.Text
      -- ^ Prop name
      -> RenderAs
      -> Property' Identifier
      -> BlackBoxContext
      -> State s Doc
    checkTF' :: forall s.
    (HasCallStack, Backend s) =>
    [Declaration]
    -> (Expr, Identifier)
    -> Text
    -> RenderAs
    -> Property' Identifier
    -> BlackBoxContext
    -> State s Doc
    checkTF' [Declaration]
    decls (Expr
    clk, Identifier
    clkId) Text
    propName RenderAs
    renderAs Property' Identifier
    prop BlackBoxContext
    bbCtx = do
      Identifier
    blockName <- Text -> StateT s Identity Identifier
    forall (m :: Type -> Type).
    (HasCallStack, IdentifierSetMonad m) =>
    Text -> m Identifier
    Id.makeBasic (Text
    propName Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "_block")
      Ap (StateT s Identity) Doc -> State s Doc
    forall {k} (f :: k -> Type) (a :: k). Ap f a -> f a
    getAp (Identifier -> [Declaration] -> Ap (StateT s Identity) Doc
    forall state.
    Backend state =>
    Identifier -> [Declaration] -> Ap (State state) Doc
    blockDecl Identifier
    blockName (Declaration
    renderedPslProperty Declaration -> [Declaration] -> [Declaration]
    forall a. a -> [a] -> [a]
    : [Declaration]
    decls))

     where
      hdl :: HDL
    hdl = s -> HDL
    forall state. Backend state => state -> HDL
    hdlKind (s
    forall a. HasCallStack => a
    undefined :: s)

      edge :: ActiveEdge
    edge =
        case BlackBoxContext -> [(Expr, HWType, Bool)]
    bbInputs BlackBoxContext
    bbCtx of
          (Expr
    _, HWType -> HWType
    stripVoid -> KnownDomain Text
    _nm Integer
    _period ActiveEdge
    e ResetKind
    _rst InitBehavior
    _init ResetPolarity
    _polarity, Bool
    _):[(Expr, HWType, Bool)]
    _ -> ActiveEdge
    e
          [(Expr, HWType, Bool)]
    _ -> String -> ActiveEdge
    forall a. HasCallStack => String -> a
    error (String -> ActiveEdge) -> String -> ActiveEdge
    forall a b. (a -> b) -> a -> b
    $ String
    "Unexpected first argument: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Maybe (Expr, HWType, Bool) -> String
    forall a. Show a => a -> String
    show ([(Expr, HWType, Bool)] -> Maybe (Expr, HWType, Bool)
    forall a. [a] -> Maybe a
    listToMaybe (BlackBoxContext -> [(Expr, HWType, Bool)]
    bbInputs BlackBoxContext
    bbCtx))

      renderedPslProperty :: Declaration
    renderedPslProperty = case RenderAs
    renderAs of
        RenderAs
    PSL          -> Declaration
    psl
        RenderAs
    SVA          -> Declaration
    sva
        RenderAs
    AutoRenderAs -> case HDL
    hdl of
          HDL
    SystemVerilog -> Declaration
    sva
          HDL
    _             -> Declaration
    psl
        RenderAs
    YosysFormal -> case HDL
    hdl of
          HDL
    VHDL -> Declaration
    psl
          HDL
    _    -> Declaration
    ysva

       where
        sva :: Declaration
    sva = Text -> Text -> ActiveEdge -> Property' Text -> Declaration
    pprSvaProperty Text
    propName (Identifier -> Text
    Id.toText Identifier
    clkId) ActiveEdge
    edge ((Identifier -> Text) -> Property' Identifier -> Property' Text
    forall a b. (a -> b) -> Property' a -> Property' b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap Identifier -> Text
    Id.toText Property' Identifier
    prop)
        ysva :: Declaration
    ysva = Text -> Expr -> ActiveEdge -> Property' Text -> Declaration
    pprYosysSvaProperty Text
    propName Expr
    clk ActiveEdge
    edge ((Identifier -> Text) -> Property' Identifier -> Property' Text
    forall a b. (a -> b) -> Property' a -> Property' b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap Identifier -> Text
    Id.toText Property' Identifier
    prop)
        psl :: Declaration
    psl = HDL -> Text -> Text -> ActiveEdge -> Property' Text -> Declaration
    pprPslProperty HDL
    hdl Text
    propName (Identifier -> Text
    Id.toText Identifier
    clkId) ActiveEdge
    edge ((Identifier -> Text) -> Property' Identifier -> Property' Text
    forall a b. (a -> b) -> Property' a -> Property' b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap Identifier -> Text
    Id.toText Property' Identifier
    prop)