-- 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, 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-core
@version 2.2.0

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)

module Copilot.Core.Random.Weights
type Depth = Int
data Weights
Weights :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> Weights
[maxExprDepth] :: Weights -> Int
[maxBuffSize] :: Weights -> Int
[maxTriggers] :: Weights -> Int
[maxTrigArgs] :: Weights -> Int
[maxExtVars] :: Weights -> Int
[maxObservers] :: Weights -> Int
[numStreams] :: Weights -> Int
[constFreq] :: Weights -> Int
[extVarFreq] :: Weights -> Int
[drop0Freq] :: Weights -> Int
[dropFreq] :: Weights -> Int
[externFreq] :: Weights -> Int
[op1Freq] :: Weights -> Int
[op2Freq] :: Weights -> Int
[op3Freq] :: Weights -> Int
[boolFreq] :: Weights -> Int
[int8Freq] :: Weights -> Int
[int16Freq] :: Weights -> Int
[int32Freq] :: Weights -> Int
[int64Freq] :: Weights -> Int
[word8Freq] :: Weights -> Int
[word16Freq] :: Weights -> Int
[word32Freq] :: Weights -> Int
[word64Freq] :: Weights -> Int
[floatFreq] :: Weights -> Int
[doubleFreq] :: Weights -> Int
[divModFreq] :: Weights -> Bool
simpleWeights :: Weights


-- | 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 :: EqualType t => t a -> a -> Dynamic t
fromDyn :: EqualType t => t a -> Dynamic t -> Maybe a
toDynF :: EqualType t => 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
class 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
instance GHC.Classes.Eq Copilot.Core.Type.SimpleType
instance Copilot.Core.Type.Equality.EqualType Copilot.Core.Type.Type
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


-- | Initial values for give types.
module Copilot.Core.Type.Uninitialized
uninitialized :: Type a -> 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

module Copilot.Core.Operators
data Op1 a b
Not :: Op1 Bool Bool
Abs :: Type a -> Op1 a a
Sign :: Type a -> Op1 a a
Recip :: Type a -> Op1 a a
Exp :: Type a -> Op1 a a
Sqrt :: Type a -> Op1 a a
Log :: Type a -> Op1 a a
Sin :: Type a -> Op1 a a
Tan :: Type a -> Op1 a a
Cos :: Type a -> Op1 a a
Asin :: Type a -> Op1 a a
Atan :: Type a -> Op1 a a
Acos :: Type a -> Op1 a a
Sinh :: Type a -> Op1 a a
Tanh :: Type a -> Op1 a a
Cosh :: Type a -> Op1 a a
Asinh :: Type a -> Op1 a a
Atanh :: Type a -> Op1 a a
Acosh :: Type a -> Op1 a a
BwNot :: Type a -> Op1 a a
Cast :: Type a -> Type b -> Op1 a b

-- | Binary operators.
data Op2 a b c
And :: Op2 Bool Bool Bool
Or :: Op2 Bool Bool Bool
Add :: Type a -> Op2 a a a
Sub :: Type a -> Op2 a a a
Mul :: Type a -> Op2 a a a
Mod :: Type a -> Op2 a a a
Div :: Type a -> Op2 a a a
Fdiv :: Type a -> Op2 a a a
Pow :: Type a -> Op2 a a a
Logb :: Type a -> Op2 a a a
Eq :: Type a -> Op2 a a Bool
Ne :: Type a -> Op2 a a Bool
Le :: Type a -> Op2 a a Bool
Ge :: Type a -> Op2 a a Bool
Lt :: Type a -> Op2 a a Bool
Gt :: Type a -> Op2 a a Bool
BwAnd :: Type a -> Op2 a a a
BwOr :: Type a -> Op2 a a a
BwXor :: Type a -> Op2 a a a
BwShiftL :: Type a -> Type b -> Op2 a b a
BwShiftR :: Type a -> Type b -> Op2 a b a

-- | 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 :: Type a -> a -> Expr a
Drop :: Type a -> DropIdx -> Id -> Expr a
Local :: Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b
Var :: Type a -> Name -> Expr a
ExternVar :: Type a -> Name -> Maybe [a] -> Expr a
ExternFun :: Type a -> Name -> [UExpr] -> Maybe (Expr a) -> Maybe Tag -> Expr a
ExternArray :: Type a -> Type b -> Name -> Int -> Expr a -> Maybe [[b]] -> Maybe Tag -> Expr b
ExternStruct :: Type a -> Name -> [(Name, UExpr)] -> Maybe Tag -> Expr a
GetField :: Type a -> Type b -> Expr a -> Name -> Expr b
Op1 :: Op1 a b -> Expr a -> Expr b
Op2 :: Op2 a b c -> Expr a -> Expr b -> Expr c
Op3 :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d
Label :: 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 expression for Struct args
data SExpr
SExpr :: String -> UExpr -> SExpr
[sname] :: SExpr -> String
[uexpr] :: SExpr -> UExpr

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

-- | Struct representation as a bit array.
data StructData
StructData :: Name -> [(Name, UExpr)] -> StructData
[structName] :: StructData -> Name
[structFields] :: StructData -> [(Name, UExpr)]

module Copilot.Core.External
data ExtVar
ExtVar :: Name -> UType -> ExtVar
[externVarName] :: ExtVar -> Name
[externVarType] :: ExtVar -> UType
data ExtArray
ExtArray :: Name -> Type b -> Expr a -> Type a -> Int -> Maybe Tag -> ExtArray
[externArrayName] :: ExtArray -> Name
[externArrayElemType] :: ExtArray -> Type b
[externArrayIdx] :: ExtArray -> Expr a
[externArrayIdxType] :: ExtArray -> Type a
[externArraySize] :: ExtArray -> Int
[externArrayTag] :: ExtArray -> Maybe Tag
data ExtFun
ExtFun :: Name -> Type a -> [UExpr] -> Maybe Tag -> ExtFun
[externFunName] :: ExtFun -> Name
[externFunType] :: ExtFun -> Type a
[externFunArgs] :: ExtFun -> [UExpr]
[externFunTag] :: ExtFun -> Maybe Tag
data ExtStruct
ExtStruct :: Name -> [(Name, UExpr)] -> Maybe Tag -> ExtStruct
[externStructName] :: ExtStruct -> Name
[externStructArgs] :: ExtStruct -> [(Name, UExpr)]
[externStructTag] :: ExtStruct -> Maybe Tag
externVars :: Spec -> [ExtVar]
externArrays :: Spec -> [ExtArray]
externFuns :: Spec -> [ExtFun]
externStructs :: Spec -> [ExtStruct]


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

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

module Copilot.Core.Random.Gen

-- | <tt>runGen</tt> takes a <tt>Gen a</tt>, a max depth of the expression,
--   the weights, and the standard random generator.
data Gen a
runGen :: Gen a -> Depth -> Weights -> StdGen -> a
randomFromType :: Type a -> Gen a
oneOf :: [Gen a] -> Gen a

-- | Takes a list of pairs (weight, Gen), and choose the Gen based on the
--   weights. To get the frequency of choosing a Gen, sum up all the
--   weights, and choose c between 1 and the total. Now recurse down the
--   list, choosing an item only when c &lt;= weight. If not, subtract the
--   current weight from c.
freq :: [(Int, Gen a)] -> Gen a
choose :: Random a => (a, a) -> Gen a
elements :: [a] -> Gen a
depth :: Gen Depth
weights :: Gen Weights
incDepth :: Gen a -> Gen a
randomReplicate :: Int -> Type a -> Gen [a]
instance GHC.Base.Functor Copilot.Core.Random.Gen.Gen
instance GHC.Base.Applicative Copilot.Core.Random.Gen.Gen
instance GHC.Base.Monad Copilot.Core.Random.Gen.Gen

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.Type.Read
data ReadWit a
ReadWit :: ReadWit a
readWit :: Type a -> ReadWit a
readWithType :: Type a -> String -> 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 tagless interpreter for Copilot specifications.
module Copilot.Core.Interpret.Eval
type Env nm = [(nm, DynamicF [] Type)]
type Output = String
data ExecTrace
ExecTrace :: Map String [Maybe [Output]] -> Map String [Output] -> ExecTrace
[interpTriggers] :: ExecTrace -> Map String [Maybe [Output]]
[interpObservers] :: ExecTrace -> Map 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.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


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


-- | Random spec generator.
module Copilot.Core.Random
randomSpec :: Int -> Weights -> StdGen -> Spec


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


-- | Generates a C99 header from a copilot-specification. The functionality
--   provided by the header must be implemented by back-ends targetting
--   C99.
module Copilot.Compile.Header.C99
genC99Header :: Maybe String -> FilePath -> Spec -> IO ()
c99HeaderName :: Maybe String -> String