    {-# LANGUAGE GADTs #-}

    -- | High-level translation of Copilot Core into C99.
    module Copilot.Compile.C99.CodeGen
        (
          -- * Externs
          mkExtCpyDecln
        , mkExtDecln

          -- * Type declarations
        , mkStructDecln
        , mkStructForwDecln

          -- * Ring buffers
        , mkBuffDecln
        , mkIndexDecln
        , mkAccessDecln

          -- * Stream generators
        , mkGenFun
        , mkGenFunArray

          -- * Monitor processing
        , mkStep
        )
      where

    -- External imports
    import           Control.Monad.State ( runState )
    import           Data.List           ( unzip4 )
    import qualified Data.List.NonEmpty  as NonEmpty
    import qualified Language.C99.Simple as C

    -- Internal imports: Copilot
    import Copilot.Core ( Expr (..), Id, Stream (..), Struct (..), Trigger (..),
                          Type (..), UExpr (..), Value (..), fieldName, typeSize )

    -- Internal imports
    import Copilot.Compile.C99.Error          ( impossible )
    import Copilot.Compile.C99.Expr           ( constArray, transExpr )
    import Copilot.Compile.C99.External       ( External (..) )
    import Copilot.Compile.C99.Name           ( argNames, argTempNames,
                                                generatorName, guardName,
                                                indexName, streamAccessorName,
                                                streamName )
    import Copilot.Compile.C99.Settings       ( CSettings,
                                                cSettingsStepFunctionName )
    import Copilot.Compile.C99.Type           ( transType )
    import Copilot.Compile.C99.Representation ( UniqueTrigger (..) )

    -- * Externs

    -- | Make a extern declaration of a variable.
    mkExtDecln :: External -> C.Decln
    mkExtDecln :: External -> Decln
    mkExtDecln (External String
    name String
    _ Type a
    ty) = Decln
    decln
      where
        decln :: Decln
    decln = Maybe StorageSpec -> Type -> String -> Maybe Init -> Decln
    C.VarDecln (StorageSpec -> Maybe StorageSpec
    forall a. a -> Maybe a
    Just StorageSpec
    C.Extern) Type
    cTy String
    name Maybe Init
    forall a. Maybe a
    Nothing
        cTy :: Type
    cTy   = Type a -> Type
    forall a. Type a -> Type
    transType Type a
    ty

    -- | Make a declaration for a copy of an external variable.
    mkExtCpyDecln :: External -> C.Decln
    mkExtCpyDecln :: External -> Decln
    mkExtCpyDecln (External String
    _name String
    cpyName Type a
    ty) = Decln
    decln
      where
        decln :: Decln
    decln = Maybe StorageSpec -> Type -> String -> Maybe Init -> Decln
    C.VarDecln (StorageSpec -> Maybe StorageSpec
    forall a. a -> Maybe a
    Just StorageSpec
    C.Static) Type
    cTy String
    cpyName Maybe Init
    forall a. Maybe a
    Nothing
        cTy :: Type
    cTy   = Type a -> Type
    forall a. Type a -> Type
    transType Type a
    ty

    -- * Type declarations

    -- | Write a struct declaration based on its definition.
    mkStructDecln :: Struct a => Type a -> C.Decln
    mkStructDecln :: forall a. Struct a => Type a -> Decln
    mkStructDecln (Struct a
    x) = Type -> Decln
    C.TypeDecln Type
    struct
      where
        struct :: Type
    struct = TypeSpec -> Type
    C.TypeSpec (TypeSpec -> Type) -> TypeSpec -> Type
    forall a b. (a -> b) -> a -> b
    $ Maybe String -> NonEmpty FieldDecln -> TypeSpec
    C.StructDecln (String -> Maybe String
    forall a. a -> Maybe a
    Just (String -> Maybe String) -> String -> Maybe String
    forall a b. (a -> b) -> a -> b
    $ a -> String
    forall a. Struct a => a -> String
    typeName a
    x) NonEmpty FieldDecln
    fields
        fields :: NonEmpty FieldDecln
    fields = [FieldDecln] -> NonEmpty FieldDecln
    forall a. HasCallStack => [a] -> NonEmpty a
    NonEmpty.fromList ([FieldDecln] -> NonEmpty FieldDecln)
    -> [FieldDecln] -> NonEmpty FieldDecln
    forall a b. (a -> b) -> a -> b
    $ (Value a -> FieldDecln) -> [Value a] -> [FieldDecln]
    forall a b. (a -> b) -> [a] -> [b]
    map Value a -> FieldDecln
    forall a. Value a -> FieldDecln
    mkField (a -> [Value a]
    forall a. Struct a => a -> [Value a]
    toValues a
    x)

        mkField :: Value a -> C.FieldDecln
        mkField :: forall a. Value a -> FieldDecln
    mkField (Value Type t
    ty Field s t
    field) = Type -> String -> FieldDecln
    C.FieldDecln (Type t -> Type
    forall a. Type a -> Type
    transType Type t
    ty) (Field s t -> String
    forall (s :: Symbol) t. KnownSymbol s => Field s t -> String
    fieldName Field s t
    field)

    -- | Write a forward struct declaration.
    mkStructForwDecln :: Struct a => Type a -> C.Decln
    mkStructForwDecln :: forall a. Struct a => Type a -> Decln
    mkStructForwDecln (Struct a
    x) = Type -> Decln
    C.TypeDecln Type
    struct
      where
        struct :: Type
    struct = TypeSpec -> Type
    C.TypeSpec (TypeSpec -> Type) -> TypeSpec -> Type
    forall a b. (a -> b) -> a -> b
    $ String -> TypeSpec
    C.Struct (a -> String
    forall a. Struct a => a -> String
    typeName a
    x)

    -- * Ring buffers

    -- | Make a C buffer variable and initialise it with the stream buffer.
    mkBuffDecln :: Id -> Type a -> [a] -> C.Decln
    mkBuffDecln :: forall a. Id -> Type a -> [a] -> Decln
    mkBuffDecln Id
    sId Type a
    ty [a]
    xs = Maybe StorageSpec -> Type -> String -> Maybe Init -> Decln
    C.VarDecln (StorageSpec -> Maybe StorageSpec
    forall a. a -> Maybe a
    Just StorageSpec
    C.Static) Type
    cTy String
    name Maybe Init
    initVals
      where
        name :: String
    name     = Id -> String
    streamName Id
    sId
        cTy :: Type
    cTy      = Type -> Maybe Expr -> Type
    C.Array (Type a -> Type
    forall a. Type a -> Type
    transType Type a
    ty) (Expr -> Maybe Expr
    forall a. a -> Maybe a
    Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
    forall a b. (a -> b) -> a -> b
    $ Integer -> Expr
    C.LitInt (Integer -> Expr) -> Integer -> Expr
    forall a b. (a -> b) -> a -> b
    $ Id -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Id
    buffSize)
        buffSize :: Id
    buffSize = [a] -> Id
    forall a. [a] -> Id
    forall (t :: * -> *) a. Foldable t => t a -> Id
    length [a]
    xs
        initVals :: Maybe Init
    initVals = Init -> Maybe Init
    forall a. a -> Maybe a
    Just (Init -> Maybe Init) -> Init -> Maybe Init
    forall a b. (a -> b) -> a -> b
    $ NonEmpty InitItem -> Init
    C.InitList (NonEmpty InitItem -> Init) -> NonEmpty InitItem -> Init
    forall a b. (a -> b) -> a -> b
    $ Type a -> [a] -> NonEmpty InitItem
    forall a. Type a -> [a] -> NonEmpty InitItem
    constArray Type a
    ty [a]
    xs

    -- | Make a C index variable and initialise it to 0.
    mkIndexDecln :: Id -> C.Decln
    mkIndexDecln :: Id -> Decln
    mkIndexDecln Id
    sId = Maybe StorageSpec -> Type -> String -> Maybe Init -> Decln
    C.VarDecln (StorageSpec -> Maybe StorageSpec
    forall a. a -> Maybe a
    Just StorageSpec
    C.Static) Type
    cTy String
    name Maybe Init
    initVal
      where
        name :: String
    name    = Id -> String
    indexName Id
    sId
        cTy :: Type
    cTy     = TypeSpec -> Type
    C.TypeSpec (TypeSpec -> Type) -> TypeSpec -> Type
    forall a b. (a -> b) -> a -> b
    $ String -> TypeSpec
    C.TypedefName String
    "size_t"
        initVal :: Maybe Init
    initVal = Init -> Maybe Init
    forall a. a -> Maybe a
    Just (Init -> Maybe Init) -> Init -> Maybe Init
    forall a b. (a -> b) -> a -> b
    $ Expr -> Init
    C.InitExpr (Expr -> Init) -> Expr -> Init
    forall a b. (a -> b) -> a -> b
    $ Integer -> Expr
    C.LitInt Integer
    0

    -- | Define an accessor functions for the ring buffer associated with a stream.
    mkAccessDecln :: Id -> Type a -> [a] -> C.FunDef
    mkAccessDecln :: forall a. Id -> Type a -> [a] -> FunDef
    mkAccessDecln Id
    sId Type a
    ty [a]
    xs =
        Maybe StorageSpec
    -> Type -> String -> [Param] -> [Decln] -> [Stmt] -> FunDef
    C.FunDef Maybe StorageSpec
    static Type
    cTy String
    name [Param]
    params [] [Maybe Expr -> Stmt
    C.Return (Expr -> Maybe Expr
    forall a. a -> Maybe a
    Just Expr
    expr)]
      where
        static :: Maybe StorageSpec
    static     = StorageSpec -> Maybe StorageSpec
    forall a. a -> Maybe a
    Just StorageSpec
    C.Static
        cTy :: Type
    cTy        = Type -> Type
    C.decay (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Type a -> Type
    forall a. Type a -> Type
    transType Type a
    ty
        name :: String
    name       = Id -> String
    streamAccessorName Id
    sId

        -- We cast the buffer length to a size_t to make sure that there are no
        -- implicit conversions. This is a requirement for compliance with MISRA C
        -- (Rule 10.4).
        buffLength :: Expr
    buffLength = TypeName -> Expr -> Expr
    C.Cast TypeName
    sizeT (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Integer -> Expr
    C.LitInt (Integer -> Expr) -> Integer -> Expr
    forall a b. (a -> b) -> a -> b
    $ Id -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Id -> Integer) -> Id -> Integer
    forall a b. (a -> b) -> a -> b
    $ [a] -> Id
    forall a. [a] -> Id
    forall (t :: * -> *) a. Foldable t => t a -> Id
    length [a]
    xs
        sizeT :: TypeName
    sizeT      = Type -> TypeName
    C.TypeName (Type -> TypeName) -> Type -> TypeName
    forall a b. (a -> b) -> a -> b
    $ TypeSpec -> Type
    C.TypeSpec (TypeSpec -> Type) -> TypeSpec -> Type
    forall a b. (a -> b) -> a -> b
    $ String -> TypeSpec
    C.TypedefName String
    "size_t"
        params :: [Param]
    params     = [Type -> String -> Param
    C.Param (TypeSpec -> Type
    C.TypeSpec (TypeSpec -> Type) -> TypeSpec -> Type
    forall a b. (a -> b) -> a -> b
    $ String -> TypeSpec
    C.TypedefName String
    "size_t") String
    "x"]
        index :: Expr
    index      = (String -> Expr
    C.Ident (Id -> String
    indexName Id
    sId) Expr -> Expr -> Expr
    C..+ String -> Expr
    C.Ident String
    "x") Expr -> Expr -> Expr
    C..% Expr
    buffLength
        expr :: Expr
    expr       = Expr -> Expr -> Expr
    C.Index (String -> Expr
    C.Ident (Id -> String
    streamName Id
    sId)) Expr
    index

    -- * Stream generators

    -- | Write a generator function for a stream.
    mkGenFun :: String -> Expr a -> Type a -> C.FunDef
    mkGenFun :: forall a. String -> Expr a -> Type a -> FunDef
    mkGenFun String
    name Expr a
    expr Type a
    ty =
        Maybe StorageSpec
    -> Type -> String -> [Param] -> [Decln] -> [Stmt] -> FunDef
    C.FunDef Maybe StorageSpec
    static Type
    cTy String
    name [] [Decln]
    cVars [Stmt]
    stmts
      where
        static :: Maybe StorageSpec
    static             = StorageSpec -> Maybe StorageSpec
    forall a. a -> Maybe a
    Just StorageSpec
    C.Static
        cTy :: Type
    cTy                = Type -> Type
    C.decay (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Type a -> Type
    forall a. Type a -> Type
    transType Type a
    ty
        (Expr
    cExpr, FunEnv
    state')    = State FunEnv Expr -> FunEnv -> (Expr, FunEnv)
    forall s a. State s a -> s -> (a, s)
    runState (Expr a -> State FunEnv Expr
    forall a. Expr a -> State FunEnv Expr
    transExpr Expr a
    expr) (Id
    0, [Decln]
    forall a. Monoid a => a
    mempty, [Stmt]
    forall a. Monoid a => a
    mempty)
        (Id
    _, [Decln]
    cVars, [Stmt]
    stmts') = FunEnv
    state'
        stmts :: [Stmt]
    stmts              = [Stmt]
    stmts' [Stmt] -> [Stmt] -> [Stmt]
    forall a. [a] -> [a] -> [a]
    ++ [Maybe Expr -> Stmt
    C.Return (Maybe Expr -> Stmt) -> Maybe Expr -> Stmt
    forall a b. (a -> b) -> a -> b
    $ Expr -> Maybe Expr
    forall a. a -> Maybe a
    Just Expr
    cExpr]

    -- | Write a generator function for a stream that returns an array.
    mkGenFunArray :: String -> String -> Expr a -> Type a -> C.FunDef
    mkGenFunArray :: forall a. String -> String -> Expr a -> Type a -> FunDef
    mkGenFunArray String
    name String
    nameArg Expr a
    expr ty :: Type a
    ty@(Array Type t
    _) =
        Maybe StorageSpec
    -> Type -> String -> [Param] -> [Decln] -> [Stmt] -> FunDef
    C.FunDef Maybe StorageSpec
    static Type
    funType String
    name [ Param
    outputParam ] [Decln]
    varDecls [Stmt]
    stmts
      where
        static :: Maybe StorageSpec
    static  = StorageSpec -> Maybe StorageSpec
    forall a. a -> Maybe a
    Just StorageSpec
    C.Static
        funType :: Type
    funType = TypeSpec -> Type
    C.TypeSpec TypeSpec
    C.Void

        -- The output value is an array
        outputParam :: Param
    outputParam = Type -> String -> Param
    C.Param Type
    cArrayType String
    nameArg
        cArrayType :: Type
    cArrayType  = Type a -> Type
    forall a. Type a -> Type
    transType Type a
    ty

        -- Statements to execute as part of the generator. They include statements
        -- related to calculating the values of intermediate expressions, and
        -- statements related to copying the final value to the destination array.
        stmts :: [Stmt]
    stmts = [Stmt]
    stmts' [Stmt] -> [Stmt] -> [Stmt]
    forall a. [a] -> [a] -> [a]
    ++ [ Stmt
    copyStmt ]

        -- Output value, variable declarations needed, and other statements that
        -- must be executed to calculate intermediate values.
        (Expr
    cExpr, FunEnv
    state')       = State FunEnv Expr -> FunEnv -> (Expr, FunEnv)
    forall s a. State s a -> s -> (a, s)
    runState (Expr a -> State FunEnv Expr
    forall a. Expr a -> State FunEnv Expr
    transExpr Expr a
    expr) (Id
    0, [Decln]
    forall a. Monoid a => a
    mempty, [Stmt]
    forall a. Monoid a => a
    mempty)
        (Id
    _, [Decln]
    varDecls, [Stmt]
    stmts') = FunEnv
    state'

        -- Copy expression to output argument.
        copyStmt :: Stmt
    copyStmt = Expr -> Stmt
    C.Expr (Expr -> Stmt) -> Expr -> Stmt
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr -> Expr -> Expr
    memcpy (String -> Expr
    C.Ident String
    nameArg) Expr
    cExpr Expr
    size
        size :: Expr
    size     = Integer -> Expr
    C.LitInt (Id -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Id -> Integer) -> Id -> Integer
    forall a b. (a -> b) -> a -> b
    $ Type (Array n t) -> Id
    forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Id
    typeSize Type a
    Type (Array n t)
    ty)
                     Expr -> Expr -> Expr
    C..* TypeName -> Expr
    C.SizeOfType (Type -> TypeName
    C.TypeName (Type -> TypeName) -> Type -> TypeName
    forall a b. (a -> b) -> a -> b
    $ Type a -> Type
    forall a. Type a -> Type
    tyElemName Type a
    ty)

    mkGenFunArray String
    _name String
    _nameArg Expr a
    _expr Type a
    _ty =
      String -> String -> FunDef
    forall a. String -> String -> a
    impossible String
    "mkGenFunArray" String
    "copilot-c99"

    -- * Monitor processing

    -- | Define the step function that updates all streams.
    mkStep :: CSettings -> [Stream] -> [UniqueTrigger] -> [External] -> C.FunDef
    mkStep :: CSettings -> [Stream] -> [UniqueTrigger] -> [External] -> FunDef
    mkStep CSettings
    cSettings [Stream]
    streams [UniqueTrigger]
    triggers [External]
    exts =
        Maybe StorageSpec
    -> Type -> String -> [Param] -> [Decln] -> [Stmt] -> FunDef
    C.FunDef Maybe StorageSpec
    forall a. Maybe a
    Nothing Type
    void (CSettings -> String
    cSettingsStepFunctionName CSettings
    cSettings) [] [Decln]
    declns [Stmt]
    stmts
      where
        void :: Type
    void = TypeSpec -> Type
    C.TypeSpec TypeSpec
    C.Void

        declns :: [Decln]
    declns =  [Decln]
    streamDeclns
               [Decln] -> [Decln] -> [Decln]
    forall a. [a] -> [a] -> [a]
    ++ [[Decln]] -> [Decln]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Decln]]
    triggerDeclns

        stmts :: [Stmt]
    stmts  =  (External -> Stmt) -> [External] -> [Stmt]
    forall a b. (a -> b) -> [a] -> [b]
    map External -> Stmt
    mkExCopy [External]
    exts
               [Stmt] -> [Stmt] -> [Stmt]
    forall a. [a] -> [a] -> [a]
    ++ [Stmt]
    triggerStmts
               [Stmt] -> [Stmt] -> [Stmt]
    forall a. [a] -> [a] -> [a]
    ++ [Stmt]
    tmpAssigns
               [Stmt] -> [Stmt] -> [Stmt]
    forall a. [a] -> [a] -> [a]
    ++ [Stmt]
    bufferUpdates
               [Stmt] -> [Stmt] -> [Stmt]
    forall a. [a] -> [a] -> [a]
    ++ [Stmt]
    indexUpdates

        ([Decln]
    streamDeclns, [Stmt]
    tmpAssigns, [Stmt]
    bufferUpdates, [Stmt]
    indexUpdates) =
          [(Decln, Stmt, Stmt, Stmt)] -> ([Decln], [Stmt], [Stmt], [Stmt])
    forall a b c d. [(a, b, c, d)] -> ([a], [b], [c], [d])
    unzip4 ([(Decln, Stmt, Stmt, Stmt)] -> ([Decln], [Stmt], [Stmt], [Stmt]))
    -> [(Decln, Stmt, Stmt, Stmt)] -> ([Decln], [Stmt], [Stmt], [Stmt])
    forall a b. (a -> b) -> a -> b
    $ (Stream -> (Decln, Stmt, Stmt, Stmt))
    -> [Stream] -> [(Decln, Stmt, Stmt, Stmt)]
    forall a b. (a -> b) -> [a] -> [b]
    map Stream -> (Decln, Stmt, Stmt, Stmt)
    mkUpdateGlobals [Stream]
    streams
        ([[Decln]]
    triggerDeclns, [Stmt]
    triggerStmts) =
          [([Decln], Stmt)] -> ([[Decln]], [Stmt])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([([Decln], Stmt)] -> ([[Decln]], [Stmt]))
    -> [([Decln], Stmt)] -> ([[Decln]], [Stmt])
    forall a b. (a -> b) -> a -> b
    $ (UniqueTrigger -> ([Decln], Stmt))
    -> [UniqueTrigger] -> [([Decln], Stmt)]
    forall a b. (a -> b) -> [a] -> [b]
    map UniqueTrigger -> ([Decln], Stmt)
    mkTriggerCheck [UniqueTrigger]
    triggers

        -- Update the value of a variable with the result of calling a function that
        -- generates the next value in a stream expression. If the type of the
        -- variable is an array, then we cannot perform a direct C assignment, so
        -- we instead pass the variable as an output array to the function.
        updateVar :: C.Ident -> C.Ident -> Type a -> C.Expr
        updateVar :: forall a. String -> String -> Type a -> Expr
    updateVar String
    varName String
    genName (Array Type t
    _) =
          Expr -> [Expr] -> Expr
    C.Funcall (String -> Expr
    C.Ident String
    genName) [String -> Expr
    C.Ident String
    varName]
        updateVar String
    varName String
    genName Type a
    _ =
          AssignOp -> Expr -> Expr -> Expr
    C.AssignOp AssignOp
    C.Assign (String -> Expr
    C.Ident String
    varName) (Expr -> [Expr] -> Expr
    C.Funcall (String -> Expr
    C.Ident String
    genName) [])

        -- Write code to update global stream buffers and index.
        mkUpdateGlobals :: Stream -> (C.Decln, C.Stmt, C.Stmt, C.Stmt)
        mkUpdateGlobals :: Stream -> (Decln, Stmt, Stmt, Stmt)
    mkUpdateGlobals (Stream Id
    sId [a]
    buff Expr a
    _expr Type a
    ty) =
          (Decln
    tmpDecln, Stmt
    tmpAssign, Stmt
    bufferUpdate, Stmt
    indexUpdate)
            where
              tmpDecln :: Decln
    tmpDecln = Maybe StorageSpec -> Type -> String -> Maybe Init -> Decln
    C.VarDecln Maybe StorageSpec
    forall a. Maybe a
    Nothing Type
    cTy String
    tmpVar Maybe Init
    forall a. Maybe a
    Nothing

              tmpAssign :: Stmt
    tmpAssign = Expr -> Stmt
    C.Expr (Expr -> Stmt) -> Expr -> Stmt
    forall a b. (a -> b) -> a -> b
    $ String -> String -> Type a -> Expr
    forall a. String -> String -> Type a -> Expr
    updateVar String
    tmpVar (Id -> String
    generatorName Id
    sId) Type a
    ty

              bufferUpdate :: Stmt
    bufferUpdate = case Type a
    ty of
                Array Type t
    _ -> Expr -> Stmt
    C.Expr (Expr -> Stmt) -> Expr -> Stmt
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr -> Expr -> Expr
    memcpy Expr
    dest (String -> Expr
    C.Ident String
    tmpVar) Expr
    size
                  where
                    dest :: Expr
    dest = Expr -> Expr -> Expr
    C.Index Expr
    buffVar Expr
    indexVar
                    size :: Expr
    size = Integer -> Expr
    C.LitInt
                               (Id -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Id -> Integer) -> Id -> Integer
    forall a b. (a -> b) -> a -> b
    $ Type (Array n t) -> Id
    forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Id
    typeSize Type a
    Type (Array n t)
    ty)
                               Expr -> Expr -> Expr
    C..* TypeName -> Expr
    C.SizeOfType (Type -> TypeName
    C.TypeName (Type a -> Type
    forall a. Type a -> Type
    tyElemName Type a
    ty))
                Type a
    _       -> Expr -> Stmt
    C.Expr (Expr -> Stmt) -> Expr -> Stmt
    forall a b. (a -> b) -> a -> b
    $
                               Expr -> Expr -> Expr
    C.Index Expr
    buffVar Expr
    indexVar Expr -> Expr -> Expr
    C..= String -> Expr
    C.Ident String
    tmpVar

              indexUpdate :: Stmt
    indexUpdate = Expr -> Stmt
    C.Expr (Expr -> Stmt) -> Expr -> Stmt
    forall a b. (a -> b) -> a -> b
    $ Expr
    indexVar Expr -> Expr -> Expr
    C..= (Expr
    incIndex Expr -> Expr -> Expr
    C..% Expr
    buffLength)
                where
                  -- We cast the buffer length and the literal one to a size_t to
                  -- make sure that there are no implicit conversions. This is a
                  -- requirement for compliance with MISRA C (Rule 10.4).
                  buffLength :: Expr
    buffLength = TypeName -> Expr -> Expr
    C.Cast TypeName
    sizeT (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Integer -> Expr
    C.LitInt (Integer -> Expr) -> Integer -> Expr
    forall a b. (a -> b) -> a -> b
    $ Id -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Id -> Integer) -> Id -> Integer
    forall a b. (a -> b) -> a -> b
    $ [a] -> Id
    forall a. [a] -> Id
    forall (t :: * -> *) a. Foldable t => t a -> Id
    length [a]
    buff
                  incIndex :: Expr
    incIndex   = Expr
    indexVar Expr -> Expr -> Expr
    C..+ TypeName -> Expr -> Expr
    C.Cast TypeName
    sizeT (Integer -> Expr
    C.LitInt Integer
    1)
                  sizeT :: TypeName
    sizeT      = Type -> TypeName
    C.TypeName (Type -> TypeName) -> Type -> TypeName
    forall a b. (a -> b) -> a -> b
    $ TypeSpec -> Type
    C.TypeSpec (TypeSpec -> Type) -> TypeSpec -> Type
    forall a b. (a -> b) -> a -> b
    $ String -> TypeSpec
    C.TypedefName String
    "size_t"

              tmpVar :: String
    tmpVar   = Id -> String
    streamName Id
    sId String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "_tmp"
              buffVar :: Expr
    buffVar  = String -> Expr
    C.Ident (String -> Expr) -> String -> Expr
    forall a b. (a -> b) -> a -> b
    $ Id -> String
    streamName Id
    sId
              indexVar :: Expr
    indexVar = String -> Expr
    C.Ident (String -> Expr) -> String -> Expr
    forall a b. (a -> b) -> a -> b
    $ Id -> String
    indexName Id
    sId
              cTy :: Type
    cTy      = Type a -> Type
    forall a. Type a -> Type
    transType Type a
    ty

        -- Make code that copies an external variable to its local one.
        mkExCopy :: External -> C.Stmt
        mkExCopy :: External -> Stmt
    mkExCopy (External String
    name String
    cpyName Type a
    ty) = Expr -> Stmt
    C.Expr (Expr -> Stmt) -> Expr -> Stmt
    forall a b. (a -> b) -> a -> b
    $ case Type a
    ty of
          Array Type t
    _ -> Expr -> Expr -> Expr -> Expr
    memcpy Expr
    exVar Expr
    locVar Expr
    size
            where
              exVar :: Expr
    exVar  = String -> Expr
    C.Ident String
    cpyName
              locVar :: Expr
    locVar = String -> Expr
    C.Ident String
    name
              size :: Expr
    size   = Integer -> Expr
    C.LitInt (Id -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Id -> Integer) -> Id -> Integer
    forall a b. (a -> b) -> a -> b
    $ Type (Array n t) -> Id
    forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Id
    typeSize Type a
    Type (Array n t)
    ty)
                         Expr -> Expr -> Expr
    C..* TypeName -> Expr
    C.SizeOfType (Type -> TypeName
    C.TypeName (Type a -> Type
    forall a. Type a -> Type
    tyElemName Type a
    ty))

          Type a
    _       -> String -> Expr
    C.Ident String
    cpyName Expr -> Expr -> Expr
    C..= String -> Expr
    C.Ident String
    name

        -- Make if-statement to check the guard, call the handler if necessary.
        -- This returns two things:
        --
        -- * A list of Declns for temporary variables, one for each argument that
        --   the handler function accepts. For example, if a handler function takes
        --   three arguments, the list of Declns might look something like this:
        --
        --   @
        --   int8_t   handler_arg_temp0;
        --   int16_t  handler_arg_temp1;
        --   struct s handler_arg_temp2;
        --   @
        --
        -- * A Stmt representing the if-statement. Continuing the example above,
        --   the if-statement would look something like this:
        --
        --   @
        --   if (handler_guard()) {
        --     handler_arg_temp0 = handler_arg0();
        --     handler_arg_temp1 = handler_arg1();
        --     handler_arg_temp2 = handler_arg2();
        --     handler(handler_arg_temp0, handler_arg_temp1, &handler_arg_temp2);
        --   }
        --   @
        --
        -- We create temporary variables because:
        --
        -- 1. We want to pass structs by reference intead of by value. To this end,
        --    we use C's & operator to obtain a reference to a temporary variable
        --    of a struct type and pass that to the handler function.
        --
        -- 2. Assigning a struct to a temporary variable defensively ensures that
        --    any modifications that the handler called makes to the struct argument
        --    will not affect the internals of the monitoring code.
        mkTriggerCheck :: UniqueTrigger -> ([C.Decln], C.Stmt)
        mkTriggerCheck :: UniqueTrigger -> ([Decln], Stmt)
    mkTriggerCheck (UniqueTrigger String
    uniqueName (Trigger String
    name Expr Bool
    _guard [UExpr]
    args)) =
            ([Decln]
    aTmpDeclns, Stmt
    triggerCheckStmt)
          where
            aTmpDeclns :: [C.Decln]
            aTmpDeclns :: [Decln]
    aTmpDeclns = (UExpr -> String -> Decln) -> [UExpr] -> [String] -> [Decln]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith UExpr -> String -> Decln
    declare [UExpr]
    args [String]
    aTempNames
              where
                declare :: UExpr -> C.Ident -> C.Decln
                declare :: UExpr -> String -> Decln
    declare (UExpr Type a
    ty Expr a
    _) String
    tmpVar =
                  Maybe StorageSpec -> Type -> String -> Maybe Init -> Decln
    C.VarDecln Maybe StorageSpec
    forall a. Maybe a
    Nothing (Type a -> Type
    forall a. Type a -> Type
    transType Type a
    ty) String
    tmpVar Maybe Init
    forall a. Maybe a
    Nothing

            triggerCheckStmt :: C.Stmt
            triggerCheckStmt :: Stmt
    triggerCheckStmt = Expr -> [Stmt] -> Stmt
    C.If Expr
    guard' [Stmt]
    fireTrigger
              where
                guard' :: Expr
    guard' = Expr -> [Expr] -> Expr
    C.Funcall (String -> Expr
    C.Ident (String -> Expr) -> String -> Expr
    forall a b. (a -> b) -> a -> b
    $ String -> String
    guardName String
    uniqueName) []

                -- The body of the if-statement. This consists of statements that
                -- assign the values of the temporary variables, following by a
                -- final statement that passes the temporary variables to the
                -- handler function.
                -- Note that we call 'name' here instead of 'uniqueName', as 'name'
                -- is the name of the actual external function.
                fireTrigger :: [Stmt]
    fireTrigger =  (Expr -> Stmt) -> [Expr] -> [Stmt]
    forall a b. (a -> b) -> [a] -> [b]
    map Expr -> Stmt
    C.Expr [Expr]
    argAssigns
                            [Stmt] -> [Stmt] -> [Stmt]
    forall a. [a] -> [a] -> [a]
    ++ [Expr -> Stmt
    C.Expr (Expr -> Stmt) -> Expr -> Stmt
    forall a b. (a -> b) -> a -> b
    $
                                   Expr -> [Expr] -> Expr
    C.Funcall (String -> Expr
    C.Ident String
    name)
                                             ((String -> UExpr -> Expr) -> [String] -> [UExpr] -> [Expr]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith String -> UExpr -> Expr
    passArg [String]
    aTempNames [UExpr]
    args)]
                  where
                    -- List of assignments of values of temporary variables.
                    argAssigns :: [C.Expr]
                    argAssigns :: [Expr]
    argAssigns = (String -> String -> UExpr -> Expr)
    -> [String] -> [String] -> [UExpr] -> [Expr]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 String -> String -> UExpr -> Expr
    assign [String]
    aTempNames [String]
    aArgNames [UExpr]
    args

                    assign :: C.Ident -> C.Ident -> UExpr -> C.Expr
                    assign :: String -> String -> UExpr -> Expr
    assign String
    aTempName String
    aArgName (UExpr Type a
    ty Expr a
    _) =
                      String -> String -> Type a -> Expr
    forall a. String -> String -> Type a -> Expr
    updateVar String
    aTempName String
    aArgName Type a
    ty

                    aArgNames :: [C.Ident]
                    aArgNames :: [String]
    aArgNames = Id -> [String] -> [String]
    forall a. Id -> [a] -> [a]
    take ([UExpr] -> Id
    forall a. [a] -> Id
    forall (t :: * -> *) a. Foldable t => t a -> Id
    length [UExpr]
    args) (String -> [String]
    argNames String
    uniqueName)

                    -- Build an expression to pass a temporary variable as argument
                    -- to a trigger handler.
                    --
                    -- We need to pass a reference to the variable in some cases,
                    -- so we also need the type of the expression, which is enclosed
                    -- in the second argument, an UExpr.
                    passArg :: String -> UExpr -> C.Expr
                    passArg :: String -> UExpr -> Expr
    passArg String
    aTempName (UExpr Type a
    ty Expr a
    _) =
                      case Type a
    ty of
                        -- Special case for Struct to pass reference to temporary
                        -- struct variable to handler. (See the comments for
                        -- mktriggercheck for details.)
                        Struct a
    _ -> UnaryOp -> Expr -> Expr
    C.UnaryOp UnaryOp
    C.Ref (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ String -> Expr
    C.Ident String
    aTempName
                        Type a
    _        -> String -> Expr
    C.Ident String
    aTempName

            aTempNames :: [String]
            aTempNames :: [String]
    aTempNames = Id -> [String] -> [String]
    forall a. Id -> [a] -> [a]
    take ([UExpr] -> Id
    forall a. [a] -> Id
    forall (t :: * -> *) a. Foldable t => t a -> Id
    length [UExpr]
    args) (String -> [String]
    argTempNames String
    uniqueName)

    -- * Auxiliary functions

    -- Write a call to the memcpy function.
    memcpy :: C.Expr -> C.Expr -> C.Expr -> C.Expr
    memcpy :: Expr -> Expr -> Expr -> Expr
    memcpy Expr
    dest Expr
    src Expr
    size = Expr -> [Expr] -> Expr
    C.Funcall (String -> Expr
    C.Ident String
    "memcpy") [Expr
    dest, Expr
    src, Expr
    size]

    -- Translate a Copilot type to a C99 type, handling arrays especially.
    --
    -- If the given type is an array (including multi-dimensional arrays), the
    -- type is that of the elements in the array. Otherwise, it is just the
    -- equivalent representation of the given type in C.
    tyElemName :: Type a -> C.Type
    tyElemName :: forall a. Type a -> Type
    tyElemName Type a
    ty = case Type a
    ty of
      Array Type t
    ty' -> Type t -> Type
    forall a. Type a -> Type
    tyElemName Type t
    ty'
      Type a
    _         -> Type a -> Type
    forall a. Type a -> Type
    transType Type a
    ty