module Clash.Verification.DSL where

import qualified Clash.Verification           as Cv
import           Clash.Verification.Internal

-- Precedences taken from:
--
--   Table 2—FL operator precedence and associativity
--
-- of
--
--   IEEE Std 1850-2010a, Annex B.1, p149

infixr 5 |&|
(|&|) :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
a
a |&| :: a -> b -> Assertion dom
|&| b
b = a -> b -> Assertion dom
forall (dom :: Domain) a b.
(AssertionValue dom a, AssertionValue dom b) =>
a -> b -> Assertion dom
Cv.and a
a b
b
{-# INLINE (|&|) #-}

infixr 4 |||
(|||) :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
a
a ||| :: a -> b -> Assertion dom
||| b
b = a -> b -> Assertion dom
forall (dom :: Domain) a b.
(AssertionValue dom a, AssertionValue dom b) =>
a -> b -> Assertion dom
Cv.or a
a b
b
{-# INLINE (|||) #-}

(~>) :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
a
a ~> :: a -> b -> Assertion dom
~> b
b = a -> b -> Assertion dom
forall (dom :: Domain) a b.
(AssertionValue dom a, AssertionValue dom b) =>
a -> b -> Assertion dom
Cv.implies a
a b
b
{-# INLINE (~>) #-}
infixr 0 ~>

(|=>) :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
a
a |=> :: a -> b -> Assertion dom
|=> b
b = a -> b -> Assertion dom
forall (dom :: Domain) a b.
(AssertionValue dom a, AssertionValue dom b) =>
a -> b -> Assertion dom
Cv.timplies a
a b
b
{-# INLINE (|=>) #-}
infixr 1 |=>

(|->) :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
a
a |-> :: a -> b -> Assertion dom
|-> b
b = a -> b -> Assertion dom
forall (dom :: Domain) a b.
(AssertionValue dom a, AssertionValue dom b) =>
a -> b -> Assertion dom
Cv.timpliesOverlapping a
a b
b
{-# INLINE (|->) #-}
infixr 1 |->

(#|#) :: (AssertionValue dom a, AssertionValue dom b) => a -> b -> Assertion dom
a
a #|# :: a -> b -> Assertion dom
#|# b
b = a -> b -> Assertion dom
forall (dom :: Domain) a b.
(AssertionValue dom a, AssertionValue dom b) =>
a -> b -> Assertion dom
Cv.before a
a b
b
{-# INLINE (#|#) #-}
infixr 3 #|#