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

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 [safe] Eq SimpleType
instance [safe] Typed Double
instance [safe] Typed Float
instance [safe] Typed Word64
instance [safe] Typed Word32
instance [safe] Typed Word16
instance [safe] Typed Word8
instance [safe] Typed Int64
instance [safe] Typed Int32
instance [safe] Typed Int16
instance [safe] Typed Int8
instance [safe] Typed Bool
instance [safe] EqualType Type


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

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

-- | 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 lost of anomymous streams, a list of observers,
--   and a list of triggers.
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

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
externVars :: Spec -> [ExtVar]
externArrays :: Spec -> [ExtArray]
externFuns :: Spec -> [ExtFun]


-- | Sets a unique tags for each external array/function 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 [safe] Monad Gen
instance [safe] Functor 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 [safe] 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 Typeable InterpException
instance Show ExecTrace
instance Exception InterpException
instance Show 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 Show 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


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