-- 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.4


-- | Custom functions to report error messages to users.
module Copilot.Core.Error

-- | Report an error due to a bug in Copilot.
impossible :: String -> String -> a

-- | Report an error due to an error detected by Copilot (e.g., user
--   error).
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

-- | Implementation of an array that uses type literals to store length.
data Array (n :: Nat) t

-- | Smart array constructor that only type checks if the length of the
--   given list matches the length of the array at type level.
array :: forall n t. KnownNat n => [t] -> Array n t

-- | Flatten an array to a list.
flatten :: Flatten a b => Array n a -> [b]

-- | Total number of elements in a possibly nested array.
size :: forall a n b. (Flatten a b, b ~ InnerType a) => Array n a -> Int

-- | Flattening or conversion of arrays to lists.
class Flatten a b

-- | Association between an array and the type of the elements it contains.
type family InnerType x

-- | Return the elemts of an array.
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)


-- | Propositional equality and type equality.
module Copilot.Core.Type.Equality

-- | Propositional equality.
data Equal :: * -> * -> *
[Refl] :: Equal a a

-- | Type equality. If the value of <tt>x =~= y</tt> is <tt>Just Refl</tt>,
--   then the two types <tt>x</tt> and <tt>y</tt> are equal.
class EqualType t
(=~=) :: EqualType t => t a -> t b -> Maybe (Equal a b)

-- | Safe coercion, which requires proof of equality.
coerce :: Equal a b -> a -> b

-- | Proof of propositional equality.
refl :: Equal a a

-- | Transitivity.
trans :: Equal a b -> Equal b c -> Equal a c

-- | Symmetry.
symm :: Equal a b -> Equal b a

-- | Congruence.
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

-- | Representation of a value accompanied by its type.
data Dynamic :: (* -> *) -> *
[Dynamic] :: a -> t a -> Dynamic t

-- | Representation of a function accompanied by its type.
data DynamicF :: (* -> *) -> (* -> *) -> *
[DynamicF] :: f a -> t a -> DynamicF f t

-- | Enclose a value and its type in a container.
toDyn :: t a -> a -> Dynamic t

-- | Extract a value from a dynamic. Return <a>Nothing</a> if the value is
--   not of the given type.
fromDyn :: EqualType t => t a -> Dynamic t -> Maybe a

-- | Enclose a function and its type in a container.
toDynF :: t a -> f a -> DynamicF f t

-- | Extract a value from a dynamic function container. Return
--   <a>Nothing</a> if the value is not of the given type.
fromDynF :: EqualType t => t a -> DynamicF f t -> Maybe (f a)


-- | Typing for Core.
--   
--   All expressions and streams in Core are accompanied by a
--   representation of the types of the underlying expressions used or
--   carried by the streams. This information is needed by the compiler to
--   generate code, since it must initialize variables and equivalent
--   representations for those types in the target languages.
module Copilot.Core.Type

-- | A Type representing the types of expressions or values handled by
--   Copilot Core.
--   
--   Note that both arrays and structs use dependently typed features. In
--   the former, the length of the array is part of the type. In the
--   latter, the names of the fields are part of the 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

-- | A typed expression, from which we can obtain the two type
--   representations used by Copilot: <a>Type</a> and <a>SimpleType</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

-- | A simple, monomorphic representation of types that facilitates putting
--   variables in heterogeneous lists and environments in spite of their
--   types being different.
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

-- | Return the total (nested) size of an array from its type
tysize :: forall n t. KnownNat n => Type (Array n t) -> Int

-- | Return the length of an array from its type
tylength :: forall n t. KnownNat n => Type (Array n t) -> Int

-- | The field of a struct, together with a representation of its type.
data Value a
Value :: Type t -> Field s t -> Value a

-- | Transforms all the struct's fields into a list of values.
toValues :: Struct a => a -> [Value a]

-- | A field in a struct. The name of the field is a literal at the type
--   level.
data Field (s :: Symbol) t
Field :: t -> Field (s :: Symbol) t

-- | Returns the name of struct in the target language.
typename :: Struct a => a -> String

-- | The value of that is a product or struct, defined as a constructor
--   with several fields.
class Struct a

-- | Extract the name of a field.
fieldname :: forall s t. KnownSymbol s => Field s t -> String

-- | Extract the name of an accessor (a function that returns a field of a
--   struct).
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)


-- | <i>Deprecated: This module is deprecated.</i>
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


-- | Internal representation of Copilot operators.
module Copilot.Core.Operators

-- | Unary 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


-- | Internal representation of Copilot stream expressions.
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

-- | Internal representation of Copilot stream expressions.
--   
--   The Core representation mimics the high-level Copilot stream, but the
--   Core representation contains information about the types of elements
--   in the stream.
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 that carries the information about the type of
--   the expression as a value, as opposed to exposing it at type level
--   (using an existential).
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


-- | Copilot specifications constitute the main declaration of Copilot
--   modules.
--   
--   A specification normally contains the association between streams to
--   monitor and their handling functions, or streams to observe, or a
--   theorem that must be proved.
--   
--   In order to be executed, high-level Copilot Language Spec must be
--   turned into Copilot Core's <a>Spec</a>. This module defines the
--   low-level Copilot Core representations for Specs and the main types of
--   element in a spec..
module Copilot.Core.Spec

-- | A stream in an infinite succession of values of the same type.
--   
--   Stream can carry different types of data. Boolean streams play a
--   special role: they are used by other parts (e.g., <a>Trigger</a>) to
--   detect when the properties being monitored are violated.
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, representing a stream that we observe during
--   interpretation at every sample.
data Observer
Observer :: Name -> Expr a -> Type a -> Observer
[observerName] :: Observer -> Name
[observerExpr] :: Observer -> Expr a
[observerExprType] :: Observer -> Type a

-- | A trigger, representing a function we execute when a boolean stream
--   becomes true at a sample.
data Trigger
Trigger :: Name -> Expr Bool -> [UExpr] -> Trigger
[triggerName] :: Trigger -> Name
[triggerGuard] :: Trigger -> Expr Bool
[triggerArgs] :: Trigger -> [UExpr]

-- | A Copilot specification is a list of streams, together with monitors
--   on these streams implemented as observers, triggers or properties.
data Spec
Spec :: [Stream] -> [Observer] -> [Trigger] -> [Property] -> Spec
[specStreams] :: Spec -> [Stream]
[specObservers] :: Spec -> [Observer]
[specTriggers] :: Spec -> [Trigger]
[specProperties] :: Spec -> [Property]

-- | A property, representing a boolean stream that is existentially or
--   universally quantified over time.
data Property
Property :: Name -> Expr Bool -> Property
[propertyName] :: Property -> Name
[propertyExpr] :: Property -> Expr Bool


-- | Sets a unique tags for each external array/function/struct call.

-- | <i>Deprecated: This module is deprecated in Copilot 3.3.</i>
module Copilot.Core.MakeTags
makeTags :: Spec -> Spec


-- | Internal Copilot Core representation of Copilot externs.
module Copilot.Core.External

-- | An extern variable declaration, together with the type of the
--   underlying extern.
data ExtVar
ExtVar :: Name -> UType -> ExtVar
[externVarName] :: ExtVar -> Name
[externVarType] :: ExtVar -> UType

-- | List of all externs used in a specification.
externVars :: Spec -> [ExtVar]


-- | <i>Deprecated: This module is deprecated.</i>
module Copilot.Core.Type.Read
data ReadWit a
ReadWit :: ReadWit a
readWit :: Type a -> ReadWit a
readWithType :: Type a -> String -> a


-- | Show Copilot Core types and typed values.
module Copilot.Core.Type.Show

-- | Witness datatype for showing a value, used by <a>showWithType</a>.
data ShowWit a
ShowWit :: ShowWit a

-- | Turn a type into a show witness.

-- | <i>Deprecated: This function is deprecated in Copilot 3.4.</i>
showWit :: Type a -> ShowWit a

-- | Show a value. The representation depends on the type and the target
--   language. Booleans are represented differently depending on the
--   backend.
showWithType :: ShowType -> Type a -> a -> String

-- | Target language for showing a typed value. Used to adapt the
--   representation of booleans.
data ShowType
C :: ShowType
Haskell :: ShowType

-- | Show Copilot Core type.
showType :: Type a -> String


-- | Initial values for a given type.
module Copilot.Core.Type.Uninitialized

-- | Initial value for a given type.
--   
--   Does not support structs or arrays.
uninitialized :: Type a -> a


-- | Intermediate representation for Copilot specifications. The following
--   articles might also be useful:
--   
--   <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>
--   <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-print a Copilot specification.
prettyPrint :: Spec -> String

-- | Pretty-print a Copilot expression.
--   
--   The type is ignored, and only the expression is pretty-printed.
ppExpr :: Expr a -> Doc


-- | A pretty printer for Copilot specifications as GraphViz/dot graphs.
module Copilot.Core.PrettyDot

-- | Pretty-print a Copilot specification as a GraphViz/dot graph.
prettyPrintDot :: Spec -> String

-- | Pretty-print a Copilot expression as a GraphViz/dot graph.
prettyPrintExprDot :: Bool -> Expr a -> String


-- | Let expressions.
--   
--   Although Copilot is a DSL embedded in Haskell and Haskell does support
--   let expressions, we want Copilot to be able to implement explicit
--   sharing, to detect when the same stream is being used in multiple
--   places in a specification and avoid recomputing it unnecessarily.

-- | <i>Deprecated: This module is deprecated.</i>
module Copilot.Core.Locals

-- | A local definition, with a given stream name and stream type.
data Loc
Loc :: Name -> Type a -> Loc
[localName] :: Loc -> Name
[localType] :: Loc -> Type a

-- | Obtain all the local definitions in a specification.
locals :: Spec -> [Loc]
instance GHC.Show.Show Copilot.Core.Locals.Loc


-- | A tagless interpreter for Copilot specifications.
module Copilot.Core.Interpret.Eval

-- | An environment that contains an association between (stream or extern)
--   names and their values.
type Env nm = [(nm, Dynamic)]

-- | The simulation output is defined as a string. Different backends may
--   choose to format their results differently.
type Output = String

-- | An execution trace, containing the traces associated to each
--   individual monitor trigger and observer.
data ExecTrace
ExecTrace :: [(String, [Maybe [Output]])] -> [(String, [Output])] -> ExecTrace

-- | Map from trigger names to their optional output, which is a list of
--   strings representing their values. The output may be <a>Nothing</a> if
--   the guard for the trigger was false. The order is important, since we
--   compare the arg lists between the interpreter and backends.
[interpTriggers] :: ExecTrace -> [(String, [Maybe [Output]])]

-- | Map from observer names to their outputs.
[interpObservers] :: ExecTrace -> [(String, [Output])]

-- | Evaluate a specification for a number of steps.
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


-- | Pretty-print the results of a simulation.
module Copilot.Core.Interpret.Render

-- | Render an execution trace as a table, formatted to faciliate
--   readability.
renderAsTable :: ExecTrace -> String

-- | Render an execution trace as using comma-separate value (CSV) format.
renderAsCSV :: ExecTrace -> String


-- | An interpreter for Copilot specifications.
module Copilot.Core.Interpret

-- | Output format for the results of a Copilot spec interpretation.
data Format
Table :: Format
CSV :: Format

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