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


-- | A compiler for Copilot targeting C99.
--   
--   This package is a back-end from Copilot to C.
--   
--   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-c99
@version 3.4


-- | Auxiliary helper functions to generate C99 code.
module Copilot.Compile.C99.Util

-- | Auxiliary type used to collect all the declarations of all the
--   variables used in a function to be generated, since variable
--   declarations are always listed first at the top of the function body.
type FunEnv = ([Decln], [Ident])

-- | <tt>tell</tt> equivalent for <a>State</a>.
statetell :: Monoid m => m -> State m ()

-- | Generate fresh variable name based on a given one.
fresh :: String -> [String] -> String

-- | Collect all the names from a list of C99 declarations.
names :: [Decln] -> [String]

-- | Turn a stream id into a suitable C variable name.
streamname :: Id -> String

-- | Turn a stream id into the global varname for indices.
indexname :: Id -> String

-- | Add a postfix for copies of external variables the name.
excpyname :: String -> String

-- | Turn stream id into name of its generator function.
generatorname :: Id -> String

-- | Turn the name of a trigger into a guard generator.
guardname :: String -> String

-- | Turn a trigger name into a an trigger argument name.
argname :: String -> Int -> String

-- | Enumerate all argument names based on trigger name.
argnames :: String -> [String]

-- | Define a C expression that calls a function with arguments.
funcall :: Ident -> [Expr] -> Expr


-- | Translate Copilot Core expressions and operators to C99.
module Copilot.Compile.C99.Translate

-- | Translates a Copilot Core expression into a C99 expression.
transexpr :: Expr a -> State FunEnv Expr

-- | Translates a Copilot unary operator and its argument into a C99
--   expression.
transop1 :: Op1 a b -> Expr -> Expr

-- | Translates a Copilot binary operator and its arguments into a C99
--   expression.
transop2 :: Op2 a b c -> Expr -> Expr -> Expr

-- | Translates a Copilot ternary operator and its arguments into a C99
--   expression.
transop3 :: Op3 a b c d -> Expr -> Expr -> Expr -> Expr

-- | Transform a Copilot Core literal, based on its value and type, into a
--   C99 literal.
constty :: Type a -> a -> Expr

-- | Explicitly cast a C99 value to a type.
explicitty :: Type a -> Expr -> Expr

-- | Translate a Copilot type to a C99 type.
transtype :: Type a -> Type

-- | Translate a Copilot type intro a C typename
transtypename :: Type a -> TypeName


-- | Represent information about externs needed in the generation of C99
--   code for stream declarations and triggers.
module Copilot.Compile.C99.External

-- | Representation of external variables.
data External
External :: String -> String -> Type a -> External
[extname] :: External -> String
[extcpyname] :: External -> String
[exttype] :: External -> Type a

-- | Union over lists of External, we solely base the equality on the
--   extname's.
extunion :: [External] -> [External] -> [External]

-- | Collect all external variables from the streams and triggers.
--   
--   Although Copilot specifications can contain also properties and
--   theorems, the C99 backend currently only generates code for streams
--   and triggers.
gatherexts :: [Stream] -> [Trigger] -> [External]


-- | High-level translation of Copilot Core into C99.
module Copilot.Compile.C99.CodeGen

-- | Write a declaration for a generator function.
gendecln :: String -> Type a -> Decln

-- | Write a generator function for a stream.
genfun :: String -> Expr a -> Type a -> FunDef

-- | Make a extern declaration of a variable.
mkextdecln :: External -> Decln

-- | Make a declaration for a copy of an external variable.
mkextcpydecln :: External -> Decln

-- | Make a C buffer variable and initialise it with the stream buffer.
mkbuffdecln :: Id -> Type a -> [a] -> Decln

-- | Make a C index variable and initialise it to 0.
mkindexdecln :: Id -> Decln

-- | Writes the step function, that updates all streams.
mkstep :: [Stream] -> [Trigger] -> [External] -> FunDef

-- | Write a struct declaration based on its definition.
mkstructdecln :: Struct a => Type a -> Decln

-- | Write a forward struct declaration.
mkstructforwdecln :: Struct a => Type a -> Decln

-- | List all types of an expression, returns items uniquely.
exprtypes :: Typeable a => Expr a -> [UType]

-- | List all types of a type, returns items uniquely.
typetypes :: Typeable a => Type a -> [UType]

-- | Collect all expression of a list of streams and triggers and wrap them
--   into an UEXpr.
gatherexprs :: [Stream] -> [Trigger] -> [UExpr]


-- | Compile Copilot specifications to C99 code.
module Copilot.Compile.C99.Compile

-- | Compile a specification to a .h and a .c file.
--   
--   The first argument is used as prefix for the .h and .c files
--   generated.
compile :: String -> Spec -> IO ()


-- | Compile Copilot specifications to C99 code.
module Copilot.Compile.C99

-- | Compile a specification to a .h and a .c file.
--   
--   The first argument is used as prefix for the .h and .c files
--   generated.
compile :: String -> Spec -> IO ()