{-|
Copyright  :  (C) 2019, Myrtle Software Ltd
License    :  BSD2 (see the file LICENSE)
Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>

Verification
-}

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}

module Clash.Verification.PrettyPrinters
  ( pprPslProperty
  , pprSvaProperty

  -- * Debugging functions
  , pprProperty
  ) where

import           Clash.Annotations.Primitive      (HDL(..))
import           Clash.Signal.Internal            (ActiveEdge, ActiveEdge(..))
import           Clash.Verification.Internal      hiding (assertion)
import           Data.Maybe                       (fromMaybe)
import           Data.Text                        (Text)
import           TextShow                         (showt)

data Symbol
  = TImpliesOverlapping
  | TImplies
  | Implies
  | BiImplies
  | Not
  | And
  | Or
  | To
  | Equals
  -- + [] ?
  | Assign
  | Is

------------------------------------------
--                 UTIL                 --
------------------------------------------
-- | Collapse constructs such as `next (next a)` down to `next[2] a`
squashBefore :: Assertion' a -> [Assertion' a]
squashBefore :: Assertion' a -> [Assertion' a]
squashBefore (CvBefore Assertion' a
e1 Assertion' a
e2) = [Assertion' a]
e1s [Assertion' a] -> [Assertion' a] -> [Assertion' a]
forall a. [a] -> [a] -> [a]
++ [Assertion' a]
e2s
 where
  e1s :: [Assertion' a]
e1s = case Assertion' a -> [Assertion' a]
forall a. Assertion' a -> [Assertion' a]
squashBefore Assertion' a
e1 of {[] -> [Assertion' a
e1]; [Assertion' a]
es -> [Assertion' a]
es}
  e2s :: [Assertion' a]
e2s = case Assertion' a -> [Assertion' a]
forall a. Assertion' a -> [Assertion' a]
squashBefore Assertion' a
e2 of {[] -> [Assertion' a
e2]; [Assertion' a]
es -> [Assertion' a]
es}
squashBefore Assertion' a
_ = []

parensIf :: Bool -> Text -> Text
parensIf :: Bool -> Text -> Text
parensIf Bool
True Text
s = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
parensIf Bool
False Text
s = Text
s

---------------------------------------
--                PSL                --
---------------------------------------
pslBinOp
  :: HDL
  -> Bool
  -> Symbol
  -> Assertion' Text
  -> Assertion' Text
  -> Text
pslBinOp :: HDL -> Bool -> Symbol -> Assertion' Text -> Assertion' Text -> Text
pslBinOp HDL
hdl Bool
parens Symbol
op Assertion' Text
e1 Assertion' Text
e2 =
  Bool -> Text -> Text
parensIf Bool
parens (Text
e1' Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> HDL -> Symbol -> Text
symbol HDL
hdl Symbol
op Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
e2')
 where
  e1' :: Text
e1' = HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion HDL
hdl Bool
True Assertion' Text
e1
  e2' :: Text
e2' = HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion HDL
hdl Bool
True Assertion' Text
e2

pslEdge :: HDL -> ActiveEdge -> Text -> Text
pslEdge :: HDL -> ActiveEdge -> Text -> Text
pslEdge HDL
SystemVerilog ActiveEdge
activeEdge Text
clkId = HDL -> ActiveEdge -> Text -> Text
pslEdge HDL
Verilog ActiveEdge
activeEdge Text
clkId
pslEdge HDL
Verilog ActiveEdge
Rising Text
clkId = Text
"posedge " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
clkId
pslEdge HDL
Verilog ActiveEdge
Falling Text
clkId = Text
"negedge " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
clkId
pslEdge HDL
VHDL ActiveEdge
Rising Text
clkId = Text
"rising_edge(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
clkId Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
pslEdge HDL
VHDL ActiveEdge
Falling Text
clkId = Text
"falling_edge(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
clkId Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

-- | Taken from IEEE Std 1850-2010a, Annex B.1, p149
symbol :: HDL -> Symbol -> Text
symbol :: HDL -> Symbol -> Text
symbol HDL
SystemVerilog = HDL -> Symbol -> Text
symbol HDL
Verilog
symbol HDL
Verilog = \case
  Symbol
TImpliesOverlapping -> Text
"|->"
  Symbol
TImplies  -> Text
"|=>"
  Symbol
Implies   -> Text
"->"
  Symbol
BiImplies -> Text
"<->"
  Symbol
Not       -> Text
"!"
  Symbol
And       -> Text
"&&"
  Symbol
Or        -> Text
"||"
  Symbol
To        -> Text
":"
  Symbol
Assign    -> Text
"<="
  Symbol
Is        -> Text
"="
  Symbol
Equals    -> Text
"=="

symbol HDL
VHDL = \case
  Symbol
TImpliesOverlapping -> Text
"|->"
  Symbol
TImplies  -> Text
"|=>"
  Symbol
Implies   -> Text
" -> "
  Symbol
BiImplies -> Text
" <-> "
  Symbol
Not       -> Text
"not"
  Symbol
And       -> Text
" and "
  Symbol
Or        -> Text
" or "
  Symbol
To        -> Text
" to "
  Symbol
Assign    -> Text
"<="
  Symbol
Is        -> Text
"is"
  Symbol
Equals    -> Text
"="

-- | Pretty print Property. Doesn't print valid HDL, but can be used for
-- debugging purposes.
pprProperty :: Property dom -> Text
pprProperty :: Property dom -> Text
pprProperty (Property Property' (Maybe Text, Signal dom Bool)
prop0) =
  let prop1 :: Property' Text
prop1 = Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
"__autogen__" (Maybe Text -> Text)
-> ((Maybe Text, Signal dom Bool) -> Maybe Text)
-> (Maybe Text, Signal dom Bool)
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Text, Signal dom Bool) -> Maybe Text
forall a b. (a, b) -> a
fst ((Maybe Text, Signal dom Bool) -> Text)
-> Property' (Maybe Text, Signal dom Bool) -> Property' Text
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Property' (Maybe Text, Signal dom Bool)
prop0 in
  HDL -> Text -> Text -> ActiveEdge -> Property' Text -> Text
pprPslProperty HDL
VHDL Text
"prop" Text
"clk" ActiveEdge
Rising Property' Text
prop1

pprPslProperty
  :: HDL
  -- ^ HDL to generate PSL expression for
  -> Text
  -- ^ Property name
  -> Text
  -- ^ Clock name
  -> ActiveEdge
  -- ^ Edge property should be sensitive to
  -> Property' Text
  -- ^ Assertion / Cover statement
  -> Text
pprPslProperty :: HDL -> Text -> Text -> ActiveEdge -> Property' Text -> Text
pprPslProperty HDL
hdl Text
propName Text
clkId ActiveEdge
edge Property' Text
assertion =
  Text
"psl property " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
propName Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> HDL -> Symbol -> Text
symbol HDL
hdl Symbol
Is Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>
  Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
prop Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") @(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> HDL -> ActiveEdge -> Text -> Text
pslEdge HDL
hdl ActiveEdge
edge Text
clkId Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>
  Text
";\n" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"psl " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
coverOrAssert Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>
  Text
propName Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
";"
 where
  (Text
coverOrAssert, Text
prop) =
    case Property' Text
assertion of
      CvCover Assertion' Text
e -> (Text
"cover", HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion HDL
hdl Bool
False Assertion' Text
e)
      CvAssert Assertion' Text
e -> (Text
"assert", HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion HDL
hdl Bool
False Assertion' Text
e)

pprPslAssertion :: HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion :: HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion HDL
hdl Bool
parens Assertion' Text
e =
  case Assertion' Text
e of
    (CvPure Text
p) -> Text
p

    -- ModelSim/QuastaSim doesn't support booleans in PSL. Anytime we want to
    -- use a boolean literal we use (0 == 0) or (0 == 1) instead.
    (CvLit Bool
False) -> Bool -> Text -> Text
parensIf Bool
parens (Text
"0" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> HDL -> Symbol -> Text
symbol HDL
hdl Symbol
Equals Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"1")
    (CvLit Bool
True) -> Bool -> Text -> Text
parensIf Bool
parens (Text
"0" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> HDL -> Symbol -> Text
symbol HDL
hdl Symbol
Equals Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"0")

    (CvNot Assertion' Text
e1) ->
      Bool -> Text -> Text
parensIf Bool
parens (HDL -> Symbol -> Text
symbol HDL
hdl Symbol
Not Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion HDL
hdl Bool
True Assertion' Text
e1)
    (CvAnd Assertion' Text
e1 Assertion' Text
e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
pslBinOp1 Symbol
And Assertion' Text
e1 Assertion' Text
e2
    (CvOr Assertion' Text
e1 Assertion' Text
e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
pslBinOp1 Symbol
Or Assertion' Text
e1 Assertion' Text
e2
    (CvImplies Assertion' Text
e1 Assertion' Text
e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
pslBinOp1 Symbol
Implies Assertion' Text
e1 Assertion' Text
e2

    (CvToTemporal Assertion' Text
e1) -> Text
"{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion HDL
hdl Bool
False Assertion' Text
e1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"

    (CvNext Word
0 Assertion' Text
e1) -> HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion HDL
hdl Bool
parens Assertion' Text
e1
    (CvNext Word
1 Assertion' Text
e1) -> Text
" ## " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion HDL
hdl Bool
True Assertion' Text
e1
    (CvNext Word
n Assertion' Text
e1) -> Text
" ##" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Word -> Text
forall a. TextShow a => a -> Text
showt Word
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion HDL
hdl Bool
False Assertion' Text
e1

    (CvBefore Assertion' Text
_ Assertion' Text
_) -> Text
"{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
afters1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"
     where
      afters0 :: [Text]
afters0 = (Assertion' Text -> Text) -> [Assertion' Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion HDL
hdl Bool
False) (Assertion' Text -> [Assertion' Text]
forall a. Assertion' a -> [Assertion' a]
squashBefore Assertion' Text
e)
      afters1 :: Text
afters1 = (Text -> Text -> Text) -> [Text] -> Text
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 (\Text
e1 Text
e2 -> Text
e1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"; " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
e2) [Text]
afters0

    (CvTemporalImplies Word
0 Assertion' Text
e1 Assertion' Text
e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
pslBinOp1 Symbol
TImpliesOverlapping Assertion' Text
e1 Assertion' Text
e2
    (CvTemporalImplies Word
1 Assertion' Text
e1 Assertion' Text
e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
pslBinOp1 Symbol
TImplies Assertion' Text
e1 Assertion' Text
e2
    (CvTemporalImplies Word
n Assertion' Text
e1 Assertion' Text
e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
pslBinOp1 Symbol
TImplies Assertion' Text
e1 (Word -> Assertion' Text -> Assertion' Text
forall a. Word -> Assertion' a -> Assertion' a
CvNext Word
n Assertion' Text
e2)

    (CvAlways Assertion' Text
e1) -> Text
"always " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion HDL
hdl Bool
True Assertion' Text
e1
    (CvNever Assertion' Text
e1) -> Text
"never " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> HDL -> Bool -> Assertion' Text -> Text
pprPslAssertion HDL
hdl Bool
True Assertion' Text
e1
 where
  pslBinOp1 :: Symbol -> Assertion' Text -> Assertion' Text -> Text
pslBinOp1 = HDL -> Bool -> Symbol -> Assertion' Text -> Assertion' Text -> Text
pslBinOp HDL
hdl Bool
True


---------------------------------------
--                SVA                --
---------------------------------------
svaEdge :: ActiveEdge -> Text -> Text
svaEdge :: ActiveEdge -> Text -> Text
svaEdge ActiveEdge
Rising Text
clkId = Text
"posedge " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
clkId
svaEdge ActiveEdge
Falling Text
clkId = Text
"negedge " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
clkId

svaBinOp
  :: Bool
  -> Symbol
  -> Assertion' Text
  -> Assertion' Text
  -> Text
svaBinOp :: Bool -> Symbol -> Assertion' Text -> Assertion' Text -> Text
svaBinOp Bool
parens Symbol
op Assertion' Text
e1 Assertion' Text
e2 =
  Bool -> Text -> Text
parensIf Bool
parens (Text
e1' Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> HDL -> Symbol -> Text
symbol HDL
SystemVerilog Symbol
op Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
e2')
 where
  e1' :: Text
e1' = Bool -> Assertion' Text -> Text
pprSvaAssertion Bool
True Assertion' Text
e1
  e2' :: Text
e2' = Bool -> Assertion' Text -> Text
pprSvaAssertion Bool
True Assertion' Text
e2

pprSvaAssertion :: Bool -> Assertion' Text -> Text
pprSvaAssertion :: Bool -> Assertion' Text -> Text
pprSvaAssertion Bool
parens Assertion' Text
e =
  case Assertion' Text
e of
    (CvPure Text
p) -> Text
p
    (CvLit Bool
False) -> Text
"false"
    (CvLit Bool
True) -> Text
"true"

    (CvNot Assertion' Text
e1) ->
      Bool -> Text -> Text
parensIf Bool
parens (Symbol -> Text
symbol' Symbol
Not Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Bool -> Assertion' Text -> Text
pprSvaAssertion Bool
True Assertion' Text
e1)
    (CvAnd Assertion' Text
e1 Assertion' Text
e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
svaBinOp1 Symbol
And Assertion' Text
e1 Assertion' Text
e2
    (CvOr Assertion' Text
e1 Assertion' Text
e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
svaBinOp1 Symbol
Or Assertion' Text
e1 Assertion' Text
e2
    (CvImplies Assertion' Text
e1 Assertion' Text
e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
svaBinOp1 Symbol
Implies Assertion' Text
e1 Assertion' Text
e2

    (CvToTemporal Assertion' Text
e1) -> Text
"{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Bool -> Assertion' Text -> Text
pprSvaAssertion Bool
False Assertion' Text
e1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"

    (CvNext Word
0 Assertion' Text
e1) -> Bool -> Assertion' Text -> Text
pprSvaAssertion Bool
parens Assertion' Text
e1
    (CvNext Word
n Assertion' Text
e1) -> Text
"nexttime[" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Word -> Text
forall a. TextShow a => a -> Text
showt Word
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"] " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Bool -> Assertion' Text -> Text
pprSvaAssertion Bool
False Assertion' Text
e1

    (CvBefore Assertion' Text
_ Assertion' Text
_) -> Text
"{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
afters1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"
     where
      afters0 :: [Text]
afters0 = (Assertion' Text -> Text) -> [Assertion' Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Assertion' Text -> Text
pprSvaAssertion Bool
False) (Assertion' Text -> [Assertion' Text]
forall a. Assertion' a -> [Assertion' a]
squashBefore Assertion' Text
e)
      afters1 :: Text
afters1 = (Text -> Text -> Text) -> [Text] -> Text
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 (\Text
e1 Text
e2 -> Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
e1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") ##1 (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
e2 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")") [Text]
afters0

    (CvTemporalImplies Word
0 Assertion' Text
e1 Assertion' Text
e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
svaBinOp1 Symbol
TImpliesOverlapping Assertion' Text
e1 Assertion' Text
e2
    (CvTemporalImplies Word
1 Assertion' Text
e1 Assertion' Text
e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
svaBinOp1 Symbol
TImplies Assertion' Text
e1 Assertion' Text
e2
    (CvTemporalImplies Word
n Assertion' Text
e1 Assertion' Text
e2) -> Symbol -> Assertion' Text -> Assertion' Text -> Text
svaBinOp1 Symbol
TImplies Assertion' Text
e1 (Word -> Assertion' Text -> Assertion' Text
forall a. Word -> Assertion' a -> Assertion' a
CvNext Word
n Assertion' Text
e2)

    (CvAlways Assertion' Text
e1) -> Text
"always (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Bool -> Assertion' Text -> Text
pprSvaAssertion Bool
False Assertion' Text
e1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
    (CvNever Assertion' Text
_e) -> [Char] -> Text
forall a. HasCallStack => [Char] -> a
error [Char]
"'never' not supported in SVA"
 where
  svaBinOp1 :: Symbol -> Assertion' Text -> Assertion' Text -> Text
svaBinOp1 = Bool -> Symbol -> Assertion' Text -> Assertion' Text -> Text
svaBinOp Bool
parens
  symbol' :: Symbol -> Text
symbol' = HDL -> Symbol -> Text
symbol HDL
SystemVerilog

pprSvaProperty
  :: Text
  -- ^ Property name
  -> Text
  -- ^ Clock name
  -> ActiveEdge
  -- ^ Edge property should be sensitive to
  -> Property' Text
  -- ^ Assertion / Cover statement
  -> Text
pprSvaProperty :: Text -> Text -> ActiveEdge -> Property' Text -> Text
pprSvaProperty Text
propName Text
clkId ActiveEdge
edge Property' Text
assertion =
  Text
propName Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
coverOrAssert Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" property (@(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>
  ActiveEdge -> Text -> Text
svaEdge ActiveEdge
edge Text
clkId Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
prop Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
");"
 where
  (Text
coverOrAssert, Text
prop) =
    case Property' Text
assertion of
      CvCover Assertion' Text
e -> (Text
"cover", Bool -> Assertion' Text -> Text
pprSvaAssertion Bool
False Assertion' Text
e)
      CvAssert Assertion' Text
e -> (Text
"assert", Bool -> Assertion' Text -> Text
pprSvaAssertion Bool
False Assertion' Text
e)