{-# 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 )

-- * 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 [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]
  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, [Decln]
cVars) = State [Decln] Expr -> [Decln] -> (Expr, [Decln])
forall s a. State s a -> s -> (a, s)
runState (Expr a -> State [Decln] Expr
forall a. Expr a -> State [Decln] Expr
transExpr Expr a
expr) [Decln]
forall a. Monoid a => a
mempty

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

    -- Output value, and any variable declarations needed
    (Expr
cExpr, [Decln]
varDecls) = State [Decln] Expr -> [Decln] -> (Expr, [Decln])
forall s a. State s a -> s -> (a, s)
runState (Expr a -> State [Decln] Expr
forall a. Expr a -> State [Decln] Expr
transExpr Expr a
expr) [Decln]
forall a. Monoid a => a
mempty

    -- Copy expression to output argument
    stmts :: [Stmt]
stmts = [ 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] -> [Trigger] -> [External] -> C.FunDef
mkStep :: CSettings -> [Stream] -> [Trigger] -> [External] -> FunDef
mkStep CSettings
cSettings [Stream]
streams [Trigger]
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
$ (Trigger -> ([Decln], Stmt)) -> [Trigger] -> [([Decln], Stmt)]
forall a b. (a -> b) -> [a] -> [b]
map Trigger -> ([Decln], Stmt)
mkTriggerCheck [Trigger]
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 :: Trigger -> ([C.Decln], C.Stmt)
    mkTriggerCheck :: Trigger -> ([Decln], Stmt)
mkTriggerCheck (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 { uExprType :: ()
uExprType = Type a
ty }) 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
name) []

            -- 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.
            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 { uExprType :: ()
uExprType = Type a
ty }) =
                  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
name)

                -- 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 { uExprType :: ()
uExprType = Type a
ty }) =
                  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
name)

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