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


-- | An intermediate representation for Copilot.
--   
--   Intermediate representation 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, examples, and other information are available at
--   <a>https://copilot-language.github.io</a>.
@package copilot-core
@version 3.2

module Copilot.Core.Error
impossible :: String -> String -> a
badUsage :: String -> a


-- | Implementation of an array that uses type literals to store length. No
--   explicit indexing is used for the input data. Supports arbitrary
--   nesting of arrays.
module Copilot.Core.Type.Array
data Array (n :: Nat) t
array :: forall n t. KnownNat n => [t] -> Array n t
flatten :: Flatten a b => Array n a -> [b]
size :: forall a n b. (Flatten a b, b ~ InnerType a) => Array n a -> Int
class Flatten a b
type family InnerType x
arrayelems :: Array n a -> [a]
instance Copilot.Core.Type.Array.Flatten a a
instance Copilot.Core.Type.Array.Flatten a b => Copilot.Core.Type.Array.Flatten (Copilot.Core.Type.Array.Array n a) b
instance GHC.Show.Show t => GHC.Show.Show (Copilot.Core.Type.Array.Array n t)
instance Data.Foldable.Foldable (Copilot.Core.Type.Array.Array n)

module Copilot.Core.Type.Equality
data Equal :: * -> * -> *
[Refl] :: Equal a a
class EqualType t
(=~=) :: EqualType t => t a -> t b -> Maybe (Equal a b)
coerce :: Equal a b -> a -> b
refl :: Equal a a
trans :: Equal a b -> Equal b c -> Equal a c
symm :: Equal a b -> Equal b a
cong :: Equal a b -> Equal (f a) (f b)


-- | An implementation of dynamic types using
--   <a>Copilot.Core.Type.Equality</a>. The theory behind this technique is
--   described the following paper:
--   
--   <ul>
--   <li>Baars, Arthur I. and Swierstra, S. Doaitse, "<i>Typing dynamic
--   typing</i>", ACM SIGPLAN Notices vol. 37, p. 157-166, 2002</li>
--   </ul>
module Copilot.Core.Type.Dynamic
data Dynamic :: (* -> *) -> *
[Dynamic] :: a -> t a -> Dynamic t
data DynamicF :: (* -> *) -> (* -> *) -> *
[DynamicF] :: f a -> t a -> DynamicF f t
toDyn :: t a -> a -> Dynamic t
fromDyn :: EqualType t => t a -> Dynamic t -> Maybe a
toDynF :: t a -> f a -> DynamicF f t
fromDynF :: EqualType t => t a -> DynamicF f t -> Maybe (f a)


-- | Typing for Core.
module Copilot.Core.Type
data Type :: * -> *
[Bool] :: Type Bool
[Int8] :: Type Int8
[Int16] :: Type Int16
[Int32] :: Type Int32
[Int64] :: Type Int64
[Word8] :: Type Word8
[Word16] :: Type Word16
[Word32] :: Type Word32
[Word64] :: Type Word64
[Float] :: Type Float
[Double] :: Type Double
[Array] :: forall n t. (KnownNat n, Typed t, Typed (InnerType t), Flatten t (InnerType t)) => Type t -> Type (Array n t)
[Struct] :: (Typed a, Struct a) => a -> Type a
class (Show a, Typeable a) => Typed a
typeOf :: Typed a => Type a
simpleType :: Typed a => Type a -> SimpleType

-- | A untyped type (no phantom type).
data UType
UType :: Type a -> UType
[uTypeType] :: UType -> Type a
data SimpleType
[SBool] :: SimpleType
[SInt8] :: SimpleType
[SInt16] :: SimpleType
[SInt32] :: SimpleType
[SInt64] :: SimpleType
[SWord8] :: SimpleType
[SWord16] :: SimpleType
[SWord32] :: SimpleType
[SWord64] :: SimpleType
[SFloat] :: SimpleType
[SDouble] :: SimpleType
[SArray] :: Type t -> SimpleType
[SStruct] :: SimpleType
tysize :: forall n t. KnownNat n => Type (Array n t) -> Int
tylength :: forall n t. KnownNat n => Type (Array n t) -> Int
data Value a
Value :: Type t -> Field s t -> Value a
toValues :: Struct a => a -> [Value a]
data Field (s :: Symbol) t
Field :: t -> Field (s :: Symbol) t
typename :: Struct a => a -> String
class Struct a
fieldname :: forall s t. KnownSymbol s => Field s t -> String
accessorname :: forall a s t. (Struct a, KnownSymbol s) => (a -> Field s t) -> String
instance GHC.Classes.Eq Copilot.Core.Type.UType
instance (Copilot.Core.Type.Typed t, Copilot.Core.Type.Struct t) => GHC.Show.Show t
instance Copilot.Core.Type.Equality.EqualType Copilot.Core.Type.Type
instance GHC.Classes.Eq Copilot.Core.Type.SimpleType
instance Copilot.Core.Type.Typed GHC.Types.Bool
instance Copilot.Core.Type.Typed GHC.Int.Int8
instance Copilot.Core.Type.Typed GHC.Int.Int16
instance Copilot.Core.Type.Typed GHC.Int.Int32
instance Copilot.Core.Type.Typed GHC.Int.Int64
instance Copilot.Core.Type.Typed GHC.Word.Word8
instance Copilot.Core.Type.Typed GHC.Word.Word16
instance Copilot.Core.Type.Typed GHC.Word.Word32
instance Copilot.Core.Type.Typed GHC.Word.Word64
instance Copilot.Core.Type.Typed GHC.Types.Float
instance Copilot.Core.Type.Typed GHC.Types.Double
instance (Data.Typeable.Internal.Typeable t, Copilot.Core.Type.Typed t, GHC.TypeNats.KnownNat n, Copilot.Core.Type.Array.Flatten t (Copilot.Core.Type.Array.InnerType t), Copilot.Core.Type.Typed (Copilot.Core.Type.Array.InnerType t)) => Copilot.Core.Type.Typed (Copilot.Core.Type.Array.Array n t)
instance (GHC.TypeLits.KnownSymbol s, GHC.Show.Show t) => GHC.Show.Show (Copilot.Core.Type.Field s t)

module Copilot.Core.Type.Eq
data EqWit a
EqWit :: EqWit a
eqWit :: Type a -> EqWit a
data UVal
UVal :: Type a -> a -> UVal
[uType] :: UVal -> Type a
[uVal] :: UVal -> a
instance GHC.Classes.Eq Copilot.Core.Type.Eq.UVal

module Copilot.Core.Operators
data Op1 a b
[Not] :: Op1 Bool Bool
[Abs] :: Num a => Type a -> Op1 a a
[Sign] :: Num a => Type a -> Op1 a a
[Recip] :: Fractional a => Type a -> Op1 a a
[Exp] :: Floating a => Type a -> Op1 a a
[Sqrt] :: Floating a => Type a -> Op1 a a
[Log] :: Floating a => Type a -> Op1 a a
[Sin] :: Floating a => Type a -> Op1 a a
[Tan] :: Floating a => Type a -> Op1 a a
[Cos] :: Floating a => Type a -> Op1 a a
[Asin] :: Floating a => Type a -> Op1 a a
[Atan] :: Floating a => Type a -> Op1 a a
[Acos] :: Floating a => Type a -> Op1 a a
[Sinh] :: Floating a => Type a -> Op1 a a
[Tanh] :: Floating a => Type a -> Op1 a a
[Cosh] :: Floating a => Type a -> Op1 a a
[Asinh] :: Floating a => Type a -> Op1 a a
[Atanh] :: Floating a => Type a -> Op1 a a
[Acosh] :: Floating a => Type a -> Op1 a a
[BwNot] :: Bits a => Type a -> Op1 a a
[Cast] :: (Integral a, Num b) => Type a -> Type b -> Op1 a b
[GetField] :: KnownSymbol s => Type a -> Type b -> (a -> Field s b) -> Op1 a b

-- | Binary operators.
data Op2 a b c
[And] :: Op2 Bool Bool Bool
[Or] :: Op2 Bool Bool Bool
[Add] :: Num a => Type a -> Op2 a a a
[Sub] :: Num a => Type a -> Op2 a a a
[Mul] :: Num a => Type a -> Op2 a a a
[Mod] :: Integral a => Type a -> Op2 a a a
[Div] :: Integral a => Type a -> Op2 a a a
[Fdiv] :: Fractional a => Type a -> Op2 a a a
[Pow] :: Floating a => Type a -> Op2 a a a
[Logb] :: Floating a => Type a -> Op2 a a a
[Eq] :: Eq a => Type a -> Op2 a a Bool
[Ne] :: Eq a => Type a -> Op2 a a Bool
[Le] :: Ord a => Type a -> Op2 a a Bool
[Ge] :: Ord a => Type a -> Op2 a a Bool
[Lt] :: Ord a => Type a -> Op2 a a Bool
[Gt] :: Ord a => Type a -> Op2 a a Bool
[BwAnd] :: Bits a => Type a -> Op2 a a a
[BwOr] :: Bits a => Type a -> Op2 a a a
[BwXor] :: Bits a => Type a -> Op2 a a a
[BwShiftL] :: (Bits a, Integral b) => Type a -> Type b -> Op2 a b a
[BwShiftR] :: (Bits a, Integral b) => Type a -> Type b -> Op2 a b a
[Index] :: Type (Array n t) -> Op2 (Array n t) Word32 t

-- | Ternary operators.
data Op3 a b c d
[Mux] :: Type a -> Op3 Bool a a a

module Copilot.Core.Expr

-- | A stream identifier.
type Id = Int

-- | A name of a trigger, an external variable, or an external function.
type Name = String
data Expr a
[Const] :: Typeable a => Type a -> a -> Expr a
[Drop] :: Typeable a => Type a -> DropIdx -> Id -> Expr a
[Local] :: Typeable a => Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b
[Var] :: Typeable a => Type a -> Name -> Expr a
[ExternVar] :: Typeable a => Type a -> Name -> Maybe [a] -> Expr a
[Op1] :: Typeable a => Op1 a b -> Expr a -> Expr b
[Op2] :: (Typeable a, Typeable b) => Op2 a b c -> Expr a -> Expr b -> Expr c
[Op3] :: (Typeable a, Typeable b, Typeable c) => Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d
[Label] :: Typeable a => Type a -> String -> Expr a -> Expr a

-- | A untyped expression (no phantom type).
data UExpr
UExpr :: Type a -> Expr a -> UExpr
[uExprType] :: UExpr -> Type a
[uExprExpr] :: UExpr -> Expr a

-- | An index for the drop operator.
type DropIdx = Word32

-- | A unique tag for external arrays/function calls.
type Tag = Int

module Copilot.Core.Spec

-- | A stream.
data Stream
Stream :: Id -> [a] -> Expr a -> Type a -> Stream
[streamId] :: Stream -> Id
[streamBuffer] :: Stream -> [a]
[streamExpr] :: Stream -> Expr a
[streamExprType] :: Stream -> Type a

-- | An observer.
data Observer
Observer :: Name -> Expr a -> Type a -> Observer
[observerName] :: Observer -> Name
[observerExpr] :: Observer -> Expr a
[observerExprType] :: Observer -> Type a

-- | A trigger.
data Trigger
Trigger :: Name -> Expr Bool -> [UExpr] -> Trigger
[triggerName] :: Trigger -> Name
[triggerGuard] :: Trigger -> Expr Bool
[triggerArgs] :: Trigger -> [UExpr]

-- | A Copilot specification consists of a list of variables bound to
--   anonymous streams, a list of anomymous streams, a list of observers, a
--   list of triggers, and a list of structs.
data Spec
Spec :: [Stream] -> [Observer] -> [Trigger] -> [Property] -> Spec
[specStreams] :: Spec -> [Stream]
[specObservers] :: Spec -> [Observer]
[specTriggers] :: Spec -> [Trigger]
[specProperties] :: Spec -> [Property]

-- | A property.
data Property
Property :: Name -> Expr Bool -> Property
[propertyName] :: Property -> Name
[propertyExpr] :: Property -> Expr Bool


-- | Sets a unique tags for each external array<i>function</i>struct call.
module Copilot.Core.MakeTags
makeTags :: Spec -> Spec

module Copilot.Core.External
data ExtVar
ExtVar :: Name -> UType -> ExtVar
[externVarName] :: ExtVar -> Name
[externVarType] :: ExtVar -> UType
externVars :: Spec -> [ExtVar]

module Copilot.Core.Type.Read
data ReadWit a
ReadWit :: ReadWit a
readWit :: Type a -> ReadWit a
readWithType :: Type a -> String -> a

module Copilot.Core.Type.Show
data ShowWit a
ShowWit :: ShowWit a
showWit :: Type a -> ShowWit a
showWithType :: ShowType -> Type a -> a -> String
data ShowType
C :: ShowType
Haskell :: ShowType
showType :: Type a -> String


-- | Initial values for give types.
module Copilot.Core.Type.Uninitialized
uninitialized :: Type a -> a


-- | Intermediate representation for Copilot specifications. The form of
--   the representation is based on this paper:
--   
--   <ul>
--   <li>Carette, Jacques and Kiselyov, Oleg and Shan, Chung-chieh,
--   "<i>Finally tagless, partially evaluated: Tagless staged</i>
--   <i>interpreters for simpler typed languages</i>", Journal of
--   Functional Programming vol. 19, p. 509-543, 2009.</li>
--   </ul>
--   
--   The following article might also be useful:
--   
--   <ul>
--   <li>Guillemette, Louis-Julien and Monnier, Stefan, "<i>Type-Safe Code
--   Transformations in Haskell</i>", Electronic Notes in Theoretical
--   Computer Science vol. 174, p. 23-39, 2007.</li>
--   </ul>
--   
--   For examples of how to traverse a Copilot specification see the source
--   code of the interpreter (<a>Copilot.Core.Interpret</a>) and the
--   pretty-printer (<a>Copilot.Core.PrettyPrint</a>).
module Copilot.Core


-- | A pretty printer for Copilot specifications.
module Copilot.Core.PrettyPrint

-- | Pretty-prints a Copilot specification.
prettyPrint :: Spec -> String
ppExpr :: Expr a -> Doc


-- | A pretty printer for Copilot specifications.
module Copilot.Core.PrettyDot

-- | Pretty-prints a Copilot specification.
prettyPrintDot :: Spec -> String

-- | Pretty-prints a Copilot expression.
prettyPrintExprDot :: Bool -> Expr a -> String


-- | Let expressions.
module Copilot.Core.Locals
data Loc
Loc :: Name -> Type a -> Loc
[localName] :: Loc -> Name
[localType] :: Loc -> Type a
locals :: Spec -> [Loc]
instance GHC.Show.Show Copilot.Core.Locals.Loc


-- | A tagless interpreter for Copilot specifications.
module Copilot.Core.Interpret.Eval
type Env nm = [(nm, Dynamic)]
type Output = String
data ExecTrace
ExecTrace :: [(String, [Maybe [Output]])] -> [(String, [Output])] -> ExecTrace
[interpTriggers] :: ExecTrace -> [(String, [Maybe [Output]])]
[interpObservers] :: ExecTrace -> [(String, [Output])]
eval :: ShowType -> Int -> Spec -> ExecTrace
instance GHC.Show.Show Copilot.Core.Interpret.Eval.ExecTrace
instance GHC.Show.Show Copilot.Core.Interpret.Eval.InterpException
instance GHC.Exception.Type.Exception Copilot.Core.Interpret.Eval.InterpException


-- | An tagless interpreter for Copilot specifications.
module Copilot.Core.Interpret.Render
renderAsTable :: ExecTrace -> String
renderAsCSV :: ExecTrace -> String


-- | An interpreter for Copilot specifications.
module Copilot.Core.Interpret
data Format
Table :: Format
CSV :: Format

-- | Interprets a Copilot specification.
interpret :: Format -> Int -> Spec -> String