-- 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
--   https://copilot-language.github.io.
@package copilot-core
@version 4.7.1

-- | 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 :: Nat) t. KnownNat n => [t] -> Array n t

-- | Return the elements of an array.
arrayElems :: forall (n :: Nat) a. Array n a -> [a]

-- | Update element of array to given element.
--   
--   PRE: the second argument denotes a valid index in the array.
arrayUpdate :: forall (n :: Nat) a. Array n a -> Int -> a -> Array n a
instance GHC.Internal.Show.Show t => GHC.Internal.Show.Show (Copilot.Core.Type.Array.Array n t)

-- | 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 a
[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 :: Nat) t. (KnownNat n, Typed t) => Type t -> Type (Array n t)
[Struct] :: forall a. (Typed a, Struct a) => a -> Type a

-- | A typed expression, from which we can obtain the two type
--   representations used by Copilot: Type and SimpleType.
class (Show a, Typeable a) => Typed a
typeOf :: Typed a => Type a
simpleType :: Typed a => Type a -> SimpleType

-- | A default implementation of typeOf that leverages
--   Generic. In order to use this, make sure you derive a
--   Generic instance for your data type and then define
--   typeOf = typeOfDefault in its Typed
--   instance.
typeOfDefault :: (Typed a, Struct a, Generic a, GTypedStruct (Rep a)) => Type a

-- | A untyped type (no phantom type).
data UType
UType :: Type a -> UType

-- | 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] :: forall t. Type t -> SimpleType
[SStruct] :: SimpleType

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

-- | Return the length of an array from its type
typeLength :: forall (n :: Nat) 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 default implementation of toValues that leverages
--   Generic. In order to use this, make sure you derive a
--   Generic instance for your data type and then define
--   toValues = toValuesDefault in its Struct
--   instance.
toValuesDefault :: (Generic a, GStruct (Rep 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

-- | A default implementation of typeName that leverages
--   Generic. In order to use this, make sure you derive a
--   Generic instance for your data type and then define
--   typeName = typeNameDefault in its Struct
--   instance.
--   
--   This generates a struct name that consists of the name of the original
--   Haskell data type, but converted to snake_case.
typeNameDefault :: (Generic a, GDatatype (Rep 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 :: Symbol) 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 :: Symbol) t. (Struct a, KnownSymbol s) => (a -> Field s t) -> String

-- | Update the value of a struct field. This is only used by the Copilot
--   interpreter.
--   
--   If you do not plan to use the interpreter, you can omit an
--   implementation of this method. If you do so, it is recommended that
--   you derive a Generic instance for the struct data type. This is
--   because in a future release, the default implementation of
--   updateField (which will be picked if there is not a manually
--   written implementation) will be changed to require a Generic
--   instance.
--   
--   In order to implement updateField, pick one of the following
--   approaches:
--   
--   
--   
- Derive a Generic instance for the struct data type and then
--   define updateField = updateFieldDefault in the
--   Struct instance.
--   
- Manually implement updateField by doing the following for
--   each Field in a struct:
--   
--   
--   
--   
- Check that the name of the Field matches the name of the
--   supplied Value (using sameSymbol).
--   
- Check that the type of the Field matches the Type of
--   the supplied Value (using testEquality).
--   
- If both (1) and (2) succeed, update the corresponding struct field
--   using a record update.
--   
--   
--   For a complete end-to-end example that demonstrates how to manually
--   implement updateField and use it in the Copilot interpreter,
--   see the examples/StructsUpdateField.hs example in the
--   copilot library.
updateField :: Struct a => a -> Value t -> a

-- | A default implementation of updateField that leverages
--   Generic. In order to use this, make sure you derive a
--   Generic instance for your data type and then define
--   updateField = updateFieldDefault in its
--   Struct instance.
updateFieldDefault :: (Generic a, GStruct (Rep a)) => a -> Value t -> a
instance GHC.Classes.Eq Copilot.Core.Type.SimpleType
instance GHC.Classes.Eq Copilot.Core.Type.UType
instance GHC.Internal.Generics.Datatype d => Copilot.Core.Type.GDatatype (GHC.Internal.Generics.D1 d _f)
instance (Copilot.Core.Type.GStruct f, Copilot.Core.Type.GStruct g) => Copilot.Core.Type.GStruct (f GHC.Internal.Generics.:*: g)
instance (GHC.Internal.TypeLits.KnownSymbol name, Copilot.Core.Type.Typed ty, c GHC.Types.~ Copilot.Core.Type.Field name ty) => Copilot.Core.Type.GStruct (GHC.Internal.Generics.K1 _i c)
instance Copilot.Core.Type.GStruct f => Copilot.Core.Type.GStruct (GHC.Internal.Generics.M1 _i _c f)
instance Copilot.Core.Type.GStruct GHC.Internal.Generics.U1
instance (Copilot.Core.Type.GTypedStruct f, Copilot.Core.Type.GTypedStruct g) => Copilot.Core.Type.GTypedStruct (f GHC.Internal.Generics.:*: g)
instance (c GHC.Types.~ Copilot.Core.Type.Field name ty) => Copilot.Core.Type.GTypedStruct (GHC.Internal.Generics.K1 _i c)
instance Copilot.Core.Type.GTypedStruct f => Copilot.Core.Type.GTypedStruct (GHC.Internal.Generics.M1 _i _c f)
instance Copilot.Core.Type.GTypedStruct GHC.Internal.Generics.U1
instance (GHC.Internal.TypeLits.KnownSymbol s, GHC.Internal.Show.Show t) => GHC.Internal.Show.Show (Copilot.Core.Type.Field s t)
instance GHC.Internal.Show.Show (Copilot.Core.Type.Type a)
instance (Copilot.Core.Type.Typed t, Copilot.Core.Type.Struct t) => GHC.Internal.Show.Show t
instance GHC.Internal.Data.Type.Equality.TestEquality Copilot.Core.Type.Type
instance (GHC.Internal.Data.Typeable.Internal.Typeable t, Copilot.Core.Type.Typed t, GHC.Internal.TypeNats.KnownNat n) => Copilot.Core.Type.Typed (Copilot.Core.Type.Array.Array n t)
instance Copilot.Core.Type.Typed GHC.Types.Bool
instance Copilot.Core.Type.Typed GHC.Types.Double
instance Copilot.Core.Type.Typed GHC.Types.Float
instance Copilot.Core.Type.Typed GHC.Internal.Int.Int16
instance Copilot.Core.Type.Typed GHC.Internal.Int.Int32
instance Copilot.Core.Type.Typed GHC.Internal.Int.Int64
instance Copilot.Core.Type.Typed GHC.Internal.Int.Int8
instance Copilot.Core.Type.Typed GHC.Internal.Word.Word16
instance Copilot.Core.Type.Typed GHC.Internal.Word.Word32
instance Copilot.Core.Type.Typed GHC.Internal.Word.Word64
instance Copilot.Core.Type.Typed GHC.Internal.Word.Word8

module Copilot.Core.Operators

-- | Unary operators.
data Op1 a b
[Not] :: Op1 Bool Bool
[Abs] :: forall a. Num a => Type a -> Op1 a a
[Sign] :: forall a. Num a => Type a -> Op1 a a
[Recip] :: forall a. Fractional a => Type a -> Op1 a a
[Exp] :: forall a. Floating a => Type a -> Op1 a a
[Sqrt] :: forall a. Floating a => Type a -> Op1 a a
[Log] :: forall a. Floating a => Type a -> Op1 a a
[Sin] :: forall a. Floating a => Type a -> Op1 a a
[Tan] :: forall a. Floating a => Type a -> Op1 a a
[Cos] :: forall a. Floating a => Type a -> Op1 a a
[Asin] :: forall a. Floating a => Type a -> Op1 a a
[Atan] :: forall a. Floating a => Type a -> Op1 a a
[Acos] :: forall a. Floating a => Type a -> Op1 a a
[Sinh] :: forall a. Floating a => Type a -> Op1 a a
[Tanh] :: forall a. Floating a => Type a -> Op1 a a
[Cosh] :: forall a. Floating a => Type a -> Op1 a a
[Asinh] :: forall a. Floating a => Type a -> Op1 a a
[Atanh] :: forall a. Floating a => Type a -> Op1 a a
[Acosh] :: forall a. Floating a => Type a -> Op1 a a
[Ceiling] :: forall a. RealFrac a => Type a -> Op1 a a
[Floor] :: forall a. RealFrac a => Type a -> Op1 a a
[BwNot] :: forall a. Bits a => Type a -> Op1 a a
[Cast] :: forall a b. (Integral a, Num b) => Type a -> Type b -> Op1 a b
[GetField] :: forall (s :: Symbol) a b. 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] :: forall a. Num a => Type a -> Op2 a a a
[Sub] :: forall a. Num a => Type a -> Op2 a a a
[Mul] :: forall a. Num a => Type a -> Op2 a a a
[Mod] :: forall a. Integral a => Type a -> Op2 a a a
[Div] :: forall a. Integral a => Type a -> Op2 a a a
[Fdiv] :: forall a. Fractional a => Type a -> Op2 a a a
[Pow] :: forall a. Floating a => Type a -> Op2 a a a
[Logb] :: forall a. Floating a => Type a -> Op2 a a a
[Atan2] :: forall a. RealFloat a => Type a -> Op2 a a a
[Eq] :: forall a. Eq a => Type a -> Op2 a a Bool
[Ne] :: forall a. Eq a => Type a -> Op2 a a Bool
[Le] :: forall a. Ord a => Type a -> Op2 a a Bool
[Ge] :: forall a. Ord a => Type a -> Op2 a a Bool
[Lt] :: forall a. Ord a => Type a -> Op2 a a Bool
[Gt] :: forall a. Ord a => Type a -> Op2 a a Bool
[BwAnd] :: forall a. Bits a => Type a -> Op2 a a a
[BwOr] :: forall a. Bits a => Type a -> Op2 a a a
[BwXor] :: forall a. Bits a => Type a -> Op2 a a a
[BwShiftL] :: forall a b. (Bits a, Integral b) => Type a -> Type b -> Op2 a b a
[BwShiftR] :: forall a b. (Bits a, Integral b) => Type a -> Type b -> Op2 a b a
[Index] :: forall (n :: Nat) c. Type (Array n c) -> Op2 (Array n c) Word32 c
[UpdateField] :: forall b (s :: Symbol) a. (Typeable b, KnownSymbol s, Show b) => Type a -> Type b -> (a -> Field s b) -> Op2 a b a

-- | Ternary operators.
data Op3 a b c d
[Mux] :: forall b. Type b -> Op3 Bool b b b
[UpdateArray] :: forall (n :: Nat) c. Type (Array n c) -> Op3 (Array n c) Word32 c (Array n c)

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] :: forall a. Typeable a => Type a -> a -> Expr a
[Drop] :: forall a. Typeable a => Type a -> DropIdx -> Id -> Expr a
[Local] :: forall a1 a. Typeable a1 => Type a1 -> Type a -> Name -> Expr a1 -> Expr a -> Expr a
[Var] :: forall a. Typeable a => Type a -> Name -> Expr a
[ExternVar] :: forall a. Typeable a => Type a -> Name -> Maybe [a] -> Expr a
[Op1] :: forall a1 a. Typeable a1 => Op1 a1 a -> Expr a1 -> Expr a
[Op2] :: forall a1 b a. (Typeable a1, Typeable b) => Op2 a1 b a -> Expr a1 -> Expr b -> Expr a
[Op3] :: forall a1 b c a. (Typeable a1, Typeable b, Typeable c) => Op3 a1 b c a -> Expr a1 -> Expr b -> Expr c -> Expr a
[Label] :: forall a. 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

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

-- | 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 Spec. 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., Trigger) 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 -> Prop -> Property
[propertyName] :: Property -> Name
[propertyProp] :: Property -> Prop

-- | A proposition, representing a boolean stream that is existentially or
--   universally quantified over time.
data Prop
Forall :: Expr Bool -> Prop
Exists :: Expr Bool -> Prop

-- | Extract the underlying stream from a quantified proposition.
--   
--   Think carefully before using this function, as this function will
--   remove the quantifier from a proposition. Universally quantified
--   streams usually require separate treatment from existentially
--   quantified ones, so carelessly using this function to remove
--   quantifiers can result in hard-to-spot soundness bugs.
extractProp :: Prop -> Expr Bool

-- | The following articles might also be useful:
--   
--   
--   
- Carette, Jacques and Kiselyov, Oleg and Shan, Chung-chieh,
--   "Finally tagless, partially evaluated: Tagless staged
--   interpreters for simpler typed languages", Journal of
--   Functional Programming vol. 19, p. 509-543, 2009.
--   
- Guillemette, Louis-Julien and Monnier, Stefan, "Type-Safe Code
--   Transformations in Haskell", Electronic Notes in Theoretical
--   Computer Science vol. 174, p. 23-39, 2007.
--   
--   
--   For examples of how to traverse a Copilot specification see the source
--   code of the interpreter (copilot-interpreter) and the
--   pretty-printer (copilot-prettyprinter).
module Copilot.Core
