-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A Haskell-embedded DSL for monitoring hard real-time
--   distributed systems.
--   
--   The concrete syntax for Copilot.
--   
--   Copilot is a stream (i.e., infinite lists) domain-specific language
--   (DSL) in Haskell that compiles into embedded C. Copilot contains an
--   interpreter, multiple back-end compilers, and other verification
--   tools. A tutorial, bug reports, and todos are available at
--   <a>https://github.com/leepike/copilot-discussion</a>.
--   
--   Examples are available at
--   <a>https://github.com/leepike/Copilot/tree/master/Examples</a>.
@package copilot-language
@version 2.2.0


-- | Reexports <tt>Prelude</tt> from package "base" hiding identifiers
--   redefined by Copilot.
module Copilot.Language.Prelude


-- | Bitwise operators.
module Copilot.Language.Operators.BitWise

-- | The <a>Bits</a> class defines bitwise operations over integral types.
--   
--   <ul>
--   <li>Bits are numbered from 0 with bit 0 being the least significant
--   bit.</li>
--   </ul>
class Eq a => Bits a

-- | Bitwise "and"
(.&.) :: Bits a => a -> a -> a

-- | Bitwise "or"
(.|.) :: Bits a => a -> a -> a

-- | Reverse all the bits in the argument
complement :: Bits a => a -> a
(.^.) :: Bits a => a -> a -> a
(.<<.) :: (Bits a, Typed a, Typed b, Integral b) => Stream a -> Stream b -> Stream a
(.>>.) :: (Bits a, Typed a, Typed b, Integral b) => Stream a -> Stream b -> Stream a
instance (Copilot.Core.Type.Typed a, Data.Bits.Bits a) => Data.Bits.Bits (Copilot.Language.Stream.Stream a)


-- | Stream construction.
module Copilot.Language.Operators.Temporal
(++) :: Typed a => [a] -> Stream a -> Stream a
drop :: Typed a => Int -> Stream a -> Stream a
(#) :: (Typed a, Typed b) => Stream a -> String -> Stream b


-- | Comparison operators.
module Copilot.Language.Operators.Ord
(<=) :: (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
(>=) :: (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
(<) :: (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
(>) :: (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool


-- | if-then-else.
module Copilot.Language.Operators.Mux
mux :: Typed a => Stream Bool -> Stream a -> Stream a -> Stream a
ifThenElse :: Typed a => Stream Bool -> Stream a -> Stream a -> Stream a


-- | Integral class operators.
module Copilot.Language.Operators.Integral
div :: (Typed a, Integral a) => Stream a -> Stream a -> Stream a
mod :: (Typed a, Integral a) => Stream a -> Stream a -> Stream a
(^) :: (Typed a, Typed b, Num a, Bits a, Integral b) => Stream a -> Stream b -> Stream a


-- | Let expressions.
module Copilot.Language.Operators.Label
label :: (Typed a) => String -> Stream a -> Stream a


-- | Let expressions.
module Copilot.Language.Operators.Local
local :: (Typed a, Typed b) => Stream a -> (Stream a -> Stream b) -> Stream b


-- | External variables, arrays, and functions.
module Copilot.Language.Operators.Extern
extern :: Typed a => String -> Maybe [a] -> Stream a
externB :: String -> Maybe [Bool] -> Stream Bool
externW8 :: String -> Maybe [Word8] -> Stream Word8
externW16 :: String -> Maybe [Word16] -> Stream Word16
externW32 :: String -> Maybe [Word32] -> Stream Word32
externW64 :: String -> Maybe [Word64] -> Stream Word64
externI8 :: String -> Maybe [Int8] -> Stream Int8
externI16 :: String -> Maybe [Int16] -> Stream Int16
externI32 :: String -> Maybe [Int32] -> Stream Int32
externI64 :: String -> Maybe [Int64] -> Stream Int64
externF :: String -> Maybe [Float] -> Stream Float
externD :: String -> Maybe [Double] -> Stream Double
externFun :: Typed a => String -> [Arg] -> Maybe (Stream a) -> Stream a
externArray :: (Typed a, Typed b, Integral a) => String -> Stream a -> Size -> Maybe [[b]] -> Stream b
externArrayB :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Bool]] -> Stream Bool
externArrayW8 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Word8]] -> Stream Word8
externArrayW16 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Word16]] -> Stream Word16
externArrayW32 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Word32]] -> Stream Word32
externArrayW64 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Word64]] -> Stream Word64
externArrayI8 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Int8]] -> Stream Int8
externArrayI16 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Int16]] -> Stream Int16
externArrayI32 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Int32]] -> Stream Int32
externArrayI64 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Int64]] -> Stream Int64
externArrayF :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Float]] -> Stream Float
externArrayD :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Double]] -> Stream Double
externStruct :: Typed a => String -> [(String, Arg)] -> Stream a

-- | Deprecated.
funArg :: Typed a => Stream a -> Arg


-- | Equality operator.
module Copilot.Language.Operators.Eq
(==) :: (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
(/=) :: (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool


-- | Constants.
module Copilot.Language.Operators.Constant
constant :: Typed a => a -> Stream a
constB :: Bool -> Stream Bool
constW8 :: Word8 -> Stream Word8
constW16 :: Word16 -> Stream Word16
constW32 :: Word32 -> Stream Word32
constW64 :: Word64 -> Stream Word64
constI8 :: Int8 -> Stream Int8
constI16 :: Int16 -> Stream Int16
constI32 :: Int32 -> Stream Int32
constI64 :: Int64 -> Stream Int64
constF :: Float -> Stream Float
constD :: Double -> Stream Double


-- | Type-safe casting operators.
module Copilot.Language.Operators.Cast
cast :: (Cast a b, Typed a, Typed b) => Stream a -> Stream b
unsafeCast :: (UnsafeCast a b, Typed a, Typed b) => Stream a -> Stream b
instance Copilot.Language.Operators.Cast.Cast GHC.Types.Bool GHC.Types.Bool
instance Copilot.Language.Operators.Cast.Cast GHC.Types.Bool GHC.Word.Word8
instance Copilot.Language.Operators.Cast.Cast GHC.Types.Bool GHC.Word.Word16
instance Copilot.Language.Operators.Cast.Cast GHC.Types.Bool GHC.Word.Word32
instance Copilot.Language.Operators.Cast.Cast GHC.Types.Bool GHC.Word.Word64
instance Copilot.Language.Operators.Cast.Cast GHC.Types.Bool GHC.Int.Int8
instance Copilot.Language.Operators.Cast.Cast GHC.Types.Bool GHC.Int.Int16
instance Copilot.Language.Operators.Cast.Cast GHC.Types.Bool GHC.Int.Int32
instance Copilot.Language.Operators.Cast.Cast GHC.Types.Bool GHC.Int.Int64
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word8 GHC.Word.Word8
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word8 GHC.Word.Word16
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word8 GHC.Word.Word32
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word8 GHC.Word.Word64
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word8 GHC.Int.Int16
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word8 GHC.Int.Int32
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word8 GHC.Int.Int64
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word16 GHC.Word.Word16
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word16 GHC.Word.Word32
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word16 GHC.Word.Word64
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word16 GHC.Int.Int32
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word16 GHC.Int.Int64
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word32 GHC.Word.Word32
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word32 GHC.Word.Word64
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word32 GHC.Int.Int64
instance Copilot.Language.Operators.Cast.Cast GHC.Word.Word64 GHC.Word.Word64
instance Copilot.Language.Operators.Cast.Cast GHC.Int.Int8 GHC.Int.Int8
instance Copilot.Language.Operators.Cast.Cast GHC.Int.Int8 GHC.Int.Int16
instance Copilot.Language.Operators.Cast.Cast GHC.Int.Int8 GHC.Int.Int32
instance Copilot.Language.Operators.Cast.Cast GHC.Int.Int8 GHC.Int.Int64
instance Copilot.Language.Operators.Cast.Cast GHC.Int.Int16 GHC.Int.Int16
instance Copilot.Language.Operators.Cast.Cast GHC.Int.Int16 GHC.Int.Int32
instance Copilot.Language.Operators.Cast.Cast GHC.Int.Int16 GHC.Int.Int64
instance Copilot.Language.Operators.Cast.Cast GHC.Int.Int32 GHC.Int.Int32
instance Copilot.Language.Operators.Cast.Cast GHC.Int.Int32 GHC.Int.Int64
instance Copilot.Language.Operators.Cast.Cast GHC.Int.Int64 GHC.Int.Int64
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word64 GHC.Word.Word32
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word64 GHC.Word.Word16
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word64 GHC.Word.Word8
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word32 GHC.Word.Word16
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word32 GHC.Word.Word8
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word16 GHC.Word.Word8
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int64 GHC.Int.Int32
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int64 GHC.Int.Int16
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int64 GHC.Int.Int8
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int32 GHC.Int.Int16
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int32 GHC.Int.Int8
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int16 GHC.Int.Int8
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int64 GHC.Types.Float
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int32 GHC.Types.Float
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int16 GHC.Types.Float
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int8 GHC.Types.Float
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int64 GHC.Types.Double
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int32 GHC.Types.Double
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int16 GHC.Types.Double
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int8 GHC.Types.Double
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word64 GHC.Types.Float
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word32 GHC.Types.Float
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word16 GHC.Types.Float
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word8 GHC.Types.Float
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word64 GHC.Types.Double
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word32 GHC.Types.Double
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word16 GHC.Types.Double
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word8 GHC.Types.Double
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word64 GHC.Int.Int64
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word32 GHC.Int.Int32
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word16 GHC.Int.Int16
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Word.Word8 GHC.Int.Int8
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int64 GHC.Word.Word64
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int32 GHC.Word.Word32
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int16 GHC.Word.Word16
instance Copilot.Language.Operators.Cast.UnsafeCast GHC.Int.Int8 GHC.Word.Word8


-- | Boolean operators.
module Copilot.Language.Operators.Boolean
(&&) :: Stream Bool -> Stream Bool -> Stream Bool
(||) :: Stream Bool -> Stream Bool -> Stream Bool
not :: Stream Bool -> Stream Bool
true :: Stream Bool
false :: Stream Bool
xor :: Stream Bool -> Stream Bool -> Stream Bool
(==>) :: Stream Bool -> Stream Bool -> Stream Bool

module Copilot.Language.Operators.Propositional
not :: Negatable a b => a -> b
instance Copilot.Language.Operators.Propositional.Negatable (Copilot.Language.Spec.Prop Copilot.Theorem.Prove.Existential) (Copilot.Language.Spec.Prop Copilot.Theorem.Prove.Universal)
instance Copilot.Language.Operators.Propositional.Negatable (Copilot.Language.Spec.Prop Copilot.Theorem.Prove.Universal) (Copilot.Language.Spec.Prop Copilot.Theorem.Prove.Existential)


-- | Transforms a Copilot Language specification into a Copilot Core
--   specification.
module Copilot.Language.Reify
reify :: Spec' a -> IO Spec


-- | Main Copilot language export file.
module Copilot.Language
impossible :: String -> String -> a
badUsage :: String -> a
csv :: Integer -> Spec -> IO ()

-- | Much slower, but pretty-printed interpreter output.
interpret :: Integer -> Spec -> IO ()
type Spec = Writer [SpecItem] ()
data Stream :: * -> *
observer :: Typed a => String -> Stream a -> Spec
trigger :: String -> Stream Bool -> [Arg] -> Spec
arg :: Typed a => Stream a -> Arg
prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)
theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)
forall :: Stream Bool -> Prop Universal
exists :: Stream Bool -> Prop Existential
prettyPrint :: Spec -> IO ()


-- | Main import module for the front-end lanugage.
module Copilot