    {-# LANGUAGE GADTs #-}

    -- | Translate Copilot Core expressions and operators to C99.
    module Copilot.Compile.C99.Expr
        ( transExpr
        , constArray
        )
      where

    -- External imports
    import           Control.Monad.State ( State, get, modify )
    import qualified Data.List.NonEmpty  as NonEmpty
    import qualified Language.C99.Simple as C

    -- Internal imports: Copilot
    import Copilot.Core ( Array, Expr (..), Field (..), Op1 (..), Op2 (..),
                          Op3 (..), Type (..), Value (..), accessorName,
                          arrayElems, toValues, typeLength, typeSize )

    -- Internal imports
    import Copilot.Compile.C99.Error ( impossible )
    import Copilot.Compile.C99.Name  ( exCpyName, streamAccessorName )
    import Copilot.Compile.C99.Type  ( transLocalVarDeclType, transType,
                                       transTypeName )

    -- | Translates a Copilot Core expression into a C99 expression.
    transExpr :: Expr a -> State FunEnv C.Expr
    transExpr :: forall a. Expr a -> State FunEnv Expr
    transExpr (Const Type a
    ty a
    x) = Expr -> State FunEnv Expr
    forall a. a -> StateT FunEnv Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> State FunEnv Expr) -> Expr -> State FunEnv Expr
    forall a b. (a -> b) -> a -> b
    $ Type a -> a -> Expr
    forall a. Type a -> a -> Expr
    constTy Type a
    ty a
    x

    transExpr (Local Type a1
    ty1 Type a
    _ Name
    name Expr a1
    e1 Expr a
    e2) = do
      e1' <- Expr a1 -> State FunEnv Expr
    forall a. Expr a -> State FunEnv Expr
    transExpr Expr a1
    e1
      let cTy1     = Type a1 -> Type
    forall a. Type a -> Type
    transLocalVarDeclType Type a1
    ty1
          initExpr = 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
    e1'

      -- Add new decl to the tail of the fun env
      modify (\(Int
    i, [Decln]
    x, [Stmt]
    y)
                 -> (Int
    i, [Decln]
    x [Decln] -> [Decln] -> [Decln]
    forall a. [a] -> [a] -> [a]
    ++ [Maybe StorageSpec -> Type -> Name -> Maybe Init -> Decln
    C.VarDecln Maybe StorageSpec
    forall a. Maybe a
    Nothing Type
    cTy1 Name
    name Maybe Init
    initExpr], [Stmt]
    y)
             )

      transExpr e2

    transExpr (Var Type a
    _ Name
    n) = Expr -> State FunEnv Expr
    forall a. a -> StateT FunEnv Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> State FunEnv Expr) -> Expr -> State FunEnv Expr
    forall a b. (a -> b) -> a -> b
    $ Name -> Expr
    C.Ident Name
    n

    transExpr (Drop Type a
    _ DropIdx
    amount Int
    sId) = do
      let accessVar :: Name
    accessVar = Int -> Name
    streamAccessorName Int
    sId
          index :: Expr
    index     = Integer -> Expr
    C.LitInt (DropIdx -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral DropIdx
    amount)
      Expr -> State FunEnv Expr
    forall a. a -> StateT FunEnv Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> State FunEnv Expr) -> Expr -> State FunEnv Expr
    forall a b. (a -> b) -> a -> b
    $ Name -> [Expr] -> Expr
    funCall Name
    accessVar [Expr
    index]

    transExpr (ExternVar Type a
    _ Name
    name Maybe [a]
    _) = Expr -> State FunEnv Expr
    forall a. a -> StateT FunEnv Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> State FunEnv Expr) -> Expr -> State FunEnv Expr
    forall a b. (a -> b) -> a -> b
    $ Name -> Expr
    C.Ident (Name -> Name
    exCpyName Name
    name)

    transExpr (Label Type a
    _ Name
    _ Expr a
    e) = Expr a -> State FunEnv Expr
    forall a. Expr a -> State FunEnv Expr
    transExpr Expr a
    e -- ignore label

    transExpr (Op1 Op1 a1 a
    op Expr a1
    e) = do
      e' <- Expr a1 -> State FunEnv Expr
    forall a. Expr a -> State FunEnv Expr
    transExpr Expr a1
    e
      return $ transOp1 op e'

    transExpr (Op2 (UpdateField ty1 :: Type a1
    ty1@(Struct a1
    _) Type b
    ty2 a1 -> Field s b
    f) Expr a1
    e1 Expr b
    e2) = do
      -- Translating a struct update Op requires initializing a variable to the
      -- "old" value, updating the field, and returning the new value.
      e1' <- Expr a1 -> State FunEnv Expr
    forall a. Expr a -> State FunEnv Expr
    transExpr Expr a1
    e1
      e2' <- transExpr e2

      -- Variable to hold the updated struct
      (i, _, _) <- get
      let varName = Name
    "_v" Name -> Name -> Name
    forall a. [a] -> [a] -> [a]
    ++ Int -> Name
    forall a. Show a => a -> Name
    show Int
    i
      modify (\(Int
    i, [Decln]
    x, [Stmt]
    y) -> (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1, [Decln]
    x, [Stmt]
    y))

      -- Add new var decl
      let initDecl = Maybe StorageSpec -> Type -> Name -> Maybe Init -> Decln
    C.VarDecln Maybe StorageSpec
    forall a. Maybe a
    Nothing Type
    cTy1 Name
    varName Maybe Init
    forall a. Maybe a
    Nothing
          cTy1     = Type a1 -> Type
    forall a. Type a -> Type
    transLocalVarDeclType Type a1
    ty1
      modify (\(Int
    i, [Decln]
    x, [Stmt]
    y) -> (Int
    i, [Decln]
    x [Decln] -> [Decln] -> [Decln]
    forall a. [a] -> [a] -> [a]
    ++ [Decln
    initDecl], [Stmt]
    y))

      -- Initialize the var to the same value as the original struct
      let initStmt = Expr -> Stmt
    C.Expr
                   (Expr -> Stmt) -> Expr -> Stmt
    forall a b. (a -> b) -> a -> b
    $ AssignOp -> Expr -> Expr -> Expr
    C.AssignOp
                       AssignOp
    C.Assign
                       (Name -> Expr
    C.Ident Name
    varName)
                       Expr
    e1'

      -- Update field f with given value e2.
      let updateStmt = case Type b
    ty2 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 Expr
    e2' Expr
    size
              where
                dest :: Expr
    dest = Expr -> Name -> Expr
    C.Dot (Name -> Expr
    C.Ident Name
    varName) ((a1 -> Field s b) -> Name
    forall a (s :: Symbol) t.
    (Struct a, KnownSymbol s) =>
    (a -> Field s t) -> Name
    accessorName a1 -> Field s b
    f)
                size :: Expr
    size = Integer -> Expr
    C.LitInt
                           (Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ Type (Array n t) -> Int
    forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
    typeSize Type b
    Type (Array n t)
    ty2)
                           Expr -> Expr -> Expr
    C..* TypeName -> Expr
    C.SizeOfType (Type -> TypeName
    C.TypeName (Type b -> Type
    forall a. Type a -> Type
    tyElemName Type b
    ty2))

            Type b
    _       -> Expr -> Stmt
    C.Expr
                     (Expr -> Stmt) -> Expr -> Stmt
    forall a b. (a -> b) -> a -> b
    $ AssignOp -> Expr -> Expr -> Expr
    C.AssignOp
                         AssignOp
    C.Assign
                         (Expr -> Name -> Expr
    C.Dot (Name -> Expr
    C.Ident Name
    varName) ((a1 -> Field s b) -> Name
    forall a (s :: Symbol) t.
    (Struct a, KnownSymbol s) =>
    (a -> Field s t) -> Name
    accessorName a1 -> Field s b
    f))
                         Expr
    e2'

      modify (\(Int
    i, [Decln]
    x, [Stmt]
    y) -> (Int
    i, [Decln]
    x, [Stmt]
    y [Stmt] -> [Stmt] -> [Stmt]
    forall a. [a] -> [a] -> [a]
    ++ [ Stmt
    initStmt, Stmt
    updateStmt ]))

      return $ C.Ident varName

    transExpr (Op2 Op2 a1 b a
    op Expr a1
    e1 Expr b
    e2) = do
      e1' <- Expr a1 -> State FunEnv Expr
    forall a. Expr a -> State FunEnv Expr
    transExpr Expr a1
    e1
      e2' <- transExpr e2
      return $ transOp2 op e1' e2'

    transExpr e :: Expr a
    e@(Op3 (UpdateArray arrTy :: Type (Array n c)
    arrTy@(Array Type t
    ty2)) Expr a1
    e1 Expr b
    e2 Expr c
    e3) = do
      e1' <- Expr a1 -> State FunEnv Expr
    forall a. Expr a -> State FunEnv Expr
    transExpr Expr a1
    e1
      e2' <- transExpr e2
      e3' <- transExpr e3

      -- Variable to hold the updated array
      (i, _, _) <- get
      let varName = Name
    "_v" Name -> Name -> Name
    forall a. [a] -> [a] -> [a]
    ++ Int -> Name
    forall a. Show a => a -> Name
    show Int
    i
      modify (\(Int
    i, [Decln]
    x, [Stmt]
    y) -> (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1, [Decln]
    x, [Stmt]
    y))

      -- Add new var decl
      let initDecl = Maybe StorageSpec -> Type -> Name -> Maybe Init -> Decln
    C.VarDecln Maybe StorageSpec
    forall a. Maybe a
    Nothing Type
    cTy1 Name
    varName Maybe Init
    forall a. Maybe a
    Nothing
          cTy1     = Type (Array n c) -> Type
    forall a. Type a -> Type
    transType Type (Array n c)
    arrTy
      modify (\(Int
    i, [Decln]
    x, [Stmt]
    y) -> (Int
    i, [Decln]
    x [Decln] -> [Decln] -> [Decln]
    forall a. [a] -> [a] -> [a]
    ++ [Decln
    initDecl], [Stmt]
    y))

      let size :: Type (Array n t) -> C.Expr
          size arrTy :: Type (Array n t)
    arrTy@(Array Type t
    ty) = Integer -> Expr
    C.LitInt (Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ Type (Array n t) -> Int
    forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
    typeLength Type (Array n t)
    arrTy)
                             Expr -> Expr -> Expr
    C..* TypeName -> Expr
    C.SizeOfType (Type -> TypeName
    C.TypeName (Type -> TypeName) -> Type -> TypeName
    forall a b. (a -> b) -> a -> b
    $ Type t -> Type
    forall a. Type a -> Type
    transType Type t
    ty)

      -- Initialize the var to the same value as the original array
      let initStmt = Expr -> Stmt
    C.Expr (Expr -> Stmt) -> Expr -> Stmt
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr -> Expr -> Expr
    memcpy (Name -> Expr
    C.Ident Name
    varName) Expr
    e1' (Type (Array n c) -> Expr
    forall (n :: Nat) t. Type (Array n t) -> Expr
    size Type (Array n c)
    arrTy)

      -- Update element of array
      let updateStmt = case Type t
    ty2 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 Expr
    e3' Expr
    size
              where
                dest :: Expr
    dest = Expr -> Expr -> Expr
    C.Index (Name -> Expr
    C.Ident Name
    varName) Expr
    e2'
                size :: Expr
    size = Integer -> Expr
    C.LitInt
                           (Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ Type (Array n t) -> Int
    forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
    typeSize Type t
    Type (Array n t)
    ty2)
                           Expr -> Expr -> Expr
    C..* TypeName -> Expr
    C.SizeOfType (Type -> TypeName
    C.TypeName (Type t -> Type
    forall a. Type a -> Type
    tyElemName Type t
    ty2))

            Type t
    _ -> Expr -> Stmt
    C.Expr
               (Expr -> Stmt) -> Expr -> Stmt
    forall a b. (a -> b) -> a -> b
    $ AssignOp -> Expr -> Expr -> Expr
    C.AssignOp
                     AssignOp
    C.Assign
                     (Expr -> Expr -> Expr
    C.Index (Name -> Expr
    C.Ident Name
    varName) Expr
    e2')
                     Expr
    e3'

      modify (\(Int
    i, [Decln]
    x, [Stmt]
    y) -> (Int
    i, [Decln]
    x, [Stmt]
    y [Stmt] -> [Stmt] -> [Stmt]
    forall a. [a] -> [a] -> [a]
    ++ [ Stmt
    initStmt, Stmt
    updateStmt ]))

      return $ C.Ident varName

    transExpr (Op3 Op3 a1 b c a
    op Expr a1
    e1 Expr b
    e2 Expr c
    e3) = do
      e1' <- Expr a1 -> State FunEnv Expr
    forall a. Expr a -> State FunEnv Expr
    transExpr Expr a1
    e1
      e2' <- transExpr e2
      e3' <- transExpr e3
      return $ transOp3 op e1' e2' e3'

    -- | Translates a Copilot unary operator and its argument into a C99
    -- expression.
    transOp1 :: Op1 a b -> C.Expr -> C.Expr
    transOp1 :: forall a b. Op1 a b -> Expr -> Expr
    transOp1 Op1 a b
    op Expr
    e =
      -- There are three types of ways in which a function in Copilot Core can be
      -- translated into C:
      --
      -- 1) Direct translation (perfect 1-to-1 mapping)
      -- 2) Type-directed translation (1-to-many mapping, choice based on type)
      -- 3) Desugaring/complex (expands to complex expression)
      case Op1 a b
    op of
        Op1 a b
    Not           -> Expr -> Expr
    (C..!) Expr
    e
        Abs      Type a
    ty   -> Type a -> Expr -> Expr
    forall a. Type a -> Expr -> Expr
    transAbs Type a
    ty Expr
    e
        Sign     Type a
    ty   -> Type a -> Expr -> Expr
    forall a. Type a -> Expr -> Expr
    transSign Type a
    ty Expr
    e
        Recip    Type a
    ty   -> Type a -> Integer -> Expr
    forall a. Type a -> Integer -> Expr
    constNumTy Type a
    ty Integer
    1 Expr -> Expr -> Expr
    C../ Expr
    e
        Acos     Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "acos") [Expr
    e]
        Asin     Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "asin") [Expr
    e]
        Atan     Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "atan") [Expr
    e]
        Cos      Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "cos") [Expr
    e]
        Sin      Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "sin") [Expr
    e]
        Tan      Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "tan") [Expr
    e]
        Acosh    Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "acosh") [Expr
    e]
        Asinh    Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "asinh") [Expr
    e]
        Atanh    Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "atanh") [Expr
    e]
        Cosh     Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "cosh") [Expr
    e]
        Sinh     Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "sinh") [Expr
    e]
        Tanh     Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "tanh") [Expr
    e]
        Exp      Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "exp") [Expr
    e]
        Log      Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "log") [Expr
    e]
        Sqrt     Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "sqrt") [Expr
    e]
        Ceiling  Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "ceil") [Expr
    e]
        Floor    Type a
    ty   -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "floor") [Expr
    e]
        BwNot    Type a
    _    -> Expr -> Expr
    (C..~) Expr
    e
        Cast     Type a
    _ Type b
    ty -> TypeName -> Expr -> Expr
    C.Cast (Type b -> TypeName
    forall a. Type a -> TypeName
    transTypeName Type b
    ty) Expr
    e
        GetField (Struct a
    _)  Type b
    _ a -> Field s b
    f -> Expr -> Name -> Expr
    C.Dot Expr
    e ((a -> Field s b) -> Name
    forall a (s :: Symbol) t.
    (Struct a, KnownSymbol s) =>
    (a -> Field s t) -> Name
    accessorName a -> Field s b
    f)

    -- | Translates a Copilot binary operator and its arguments into a C99
    -- expression.
    --
    -- PRE: op is not a struct update operation (i.e., 'UpdateField').
    transOp2 :: Op2 a b c -> C.Expr -> C.Expr -> C.Expr
    transOp2 :: forall a b c. Op2 a b c -> Expr -> Expr -> Expr
    transOp2 Op2 a b c
    op Expr
    e1 Expr
    e2 = case Op2 a b c
    op of
      Op2 a b c
    And               -> Expr
    e1 Expr -> Expr -> Expr
    C..&& Expr
    e2
      Op2 a b c
    Or                -> Expr
    e1 Expr -> Expr -> Expr
    C..|| Expr
    e2
      Add         Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C..+  Expr
    e2
      Sub         Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C..-  Expr
    e2
      Mul         Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C..*  Expr
    e2
      Mod         Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C..%  Expr
    e2
      Div         Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C../  Expr
    e2
      Fdiv        Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C../  Expr
    e2
      Pow         Type a
    ty    -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "pow") [Expr
    e1, Expr
    e2]
      Logb        Type a
    ty    -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "log") [Expr
    e2] Expr -> Expr -> Expr
    C../
                           Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "log") [Expr
    e1]
      Atan2       Type a
    ty    -> Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "atan2") [Expr
    e1, Expr
    e2]
      Eq          Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C..== Expr
    e2
      Ne          Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C..!= Expr
    e2
      Le          Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C..<= Expr
    e2
      Ge          Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C..>= Expr
    e2
      Lt          Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C..<  Expr
    e2
      Gt          Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C..>  Expr
    e2
      BwAnd       Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C..&  Expr
    e2
      BwOr        Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C..|  Expr
    e2
      BwXor       Type a
    _     -> Expr
    e1 Expr -> Expr -> Expr
    C..^  Expr
    e2
      BwShiftL    Type a
    _ Type b
    _   -> Expr
    e1 Expr -> Expr -> Expr
    C..<< Expr
    e2
      BwShiftR    Type a
    _ Type b
    _   -> Expr
    e1 Expr -> Expr -> Expr
    C..>> Expr
    e2
      Index       Type (Array n c)
    _     -> Expr -> Expr -> Expr
    C.Index Expr
    e1 Expr
    e2
      UpdateField Type a
    _ Type b
    _ a -> Field s b
    _ -> Name -> Name -> Expr
    forall a. Name -> Name -> a
    impossible Name
    "transOp2" Name
    "copilot-c99"

    -- | Translates a Copilot ternary operator and its arguments into a C99
    -- expression.
    transOp3 :: Op3 a b c d -> C.Expr -> C.Expr -> C.Expr -> C.Expr
    transOp3 :: forall a b c d. Op3 a b c d -> Expr -> Expr -> Expr -> Expr
    transOp3 Op3 a b c d
    op Expr
    e1 Expr
    e2 Expr
    e3 = case Op3 a b c d
    op of
      Mux         Type b
    _ -> Expr -> Expr -> Expr -> Expr
    C.Cond Expr
    e1 Expr
    e2 Expr
    e3
      UpdateArray Type (Array n c)
    _ -> Name -> Name -> Expr
    forall a. Name -> Name -> a
    impossible Name
    "transOp3" Name
    "copilot-c99"

    -- | Translate @'Abs' e@ in Copilot Core into a C99 expression.
    --
    -- This function produces a portable implementation of abs in C99 that works
    -- for the type given, provided that the output fits in a variable of the same
    -- type (which may not be true, for example, for signed integers in the lower
    -- end of their type range). If the absolute value is out of range, the
    -- behavior is undefined.
    --
    -- PRE: The type given is a Num type (floating-point number, or a
    -- signed/unsigned integer of fixed size).
    transAbs :: Type a -> C.Expr -> C.Expr
    transAbs :: forall a. Type a -> Expr -> Expr
    transAbs Type a
    ty Expr
    e
        -- Abs for floats/doubles is called fabs in C99's math.h.
        | Type a -> Bool
    forall a. Type a -> Bool
    typeIsFloating Type a
    ty
        = Name -> [Expr] -> Expr
    funCall (Type a -> Name -> Name
    forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    "fabs") [Expr
    e]

        -- C99 provides multiple implementations of abs, depending on the type of
        -- the arguments. For integers, it provides C99 abs, labs, and llabs, which
        -- take, respectively, an int, a long int, and a long long int.
        --
        -- However, the code produced by Copilot uses types with fixed width (e.g.,
        -- int16_t), and there is no guarantee that, for example, 32-bit int or
        -- 64-bit int will fit in a C int (only guaranteed to be 16 bits).
        -- Consequently, this function provides a portable version of abs for signed
        -- and unsigned ints implemented using shift and xor. For example, for a
        -- value x of type int32_t, the absolute value is:
        -- (x + (x >> sizeof(int32_t)-1)) ^ (x >> sizeof(int32_t)-1))
        | Bool
    otherwise
        = (Expr
    e Expr -> Expr -> Expr
    C..+ (Expr
    e Expr -> Expr -> Expr
    C..>> Expr
    tyBitSizeMinus1)) Expr -> Expr -> Expr
    C..^ (Expr
    e Expr -> Expr -> Expr
    C..>> Expr
    tyBitSizeMinus1)
      where
        -- Size of an integer type in bits, minus one. It's easier to hard-code
        -- them than to try and generate the right expressions in C using sizeof.
        --
        -- PRE: the type 'ty' is a signed or unsigned integer type.
        tyBitSizeMinus1 :: C.Expr
        tyBitSizeMinus1 :: Expr
    tyBitSizeMinus1 = case Type a
    ty of
          Type a
    Int8   -> Integer -> Expr
    C.LitInt Integer
    7
          Type a
    Int16  -> Integer -> Expr
    C.LitInt Integer
    15
          Type a
    Int32  -> Integer -> Expr
    C.LitInt Integer
    31
          Type a
    Int64  -> Integer -> Expr
    C.LitInt Integer
    63
          Type a
    Word8  -> Integer -> Expr
    C.LitInt Integer
    7
          Type a
    Word16 -> Integer -> Expr
    C.LitInt Integer
    15
          Type a
    Word32 -> Integer -> Expr
    C.LitInt Integer
    31
          Type a
    Word64 -> Integer -> Expr
    C.LitInt Integer
    63
          Type a
    _      -> Name -> Name -> Name -> Expr
    forall a. Name -> Name -> a
    impossible
                      Name
    "transAbs"
                      Name
    "copilot-c99"
                      Name
    "Abs applied to unexpected types."

    -- | Translate @'Sign' e@ in Copilot Core into a C99 expression.
    --
    -- Sign is is translated as @e > 0 ? 1 : (e < 0 ? -1 : e)@, that is:
    --
    -- 1. If @e@ is positive, return @1@.
    --
    -- 2. If @e@ is negative, return @-1@.
    --
    -- 3. Otherwise, return @e@. This handles the case where @e@ is @0@ when the
    --    type is an integral type. If the type is a floating-point type, it also
    --    handles the cases where @e@ is @-0@ or @NaN@.
    --
    -- This implementation is modeled after how GHC implements 'signum'
    -- <https://gitlab.haskell.org/ghc/ghc/-/blob/aed98ddaf72cc38fb570d8415cac5de9d8888818/libraries/base/GHC/Float.hs#L523-L525 here>.
    transSign :: Type a -> C.Expr -> C.Expr
    transSign :: forall a. Type a -> Expr -> Expr
    transSign Type a
    ty Expr
    e = Expr -> Expr
    positiveCase (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    negativeCase Expr
    e
      where
        -- If @e@ is positive, return @1@, otherwise fall back to argument.
        --
        -- Produces the following code, where @<arg>@ is the argument to this
        -- function:
        -- @
        -- e > 0 ? 1 : <arg>
        -- @
        positiveCase :: C.Expr  -- ^ Value returned if @e@ is not positive.
                     -> C.Expr
        positiveCase :: Expr -> Expr
    positiveCase =
          Expr -> Expr -> Expr -> Expr
    C.Cond (BinaryOp -> Expr -> Expr -> Expr
    C.BinaryOp BinaryOp
    C.GT Expr
    e (Type a -> Integer -> Expr
    forall a. Type a -> Integer -> Expr
    constNumTy Type a
    ty Integer
    0)) (Type a -> Integer -> Expr
    forall a. Type a -> Integer -> Expr
    constNumTy Type a
    ty Integer
    1)

        -- If @e@ is negative, return @1@, otherwise fall back to argument.
        --
        -- Produces the following code, where @<arg>@ is the argument to this
        -- function:
        -- @
        -- e < 0 ? -1 : <arg>
        -- @
        negativeCase :: C.Expr  -- ^ Value returned if @e@ is not negative.
                     -> C.Expr
        negativeCase :: Expr -> Expr
    negativeCase =
          Expr -> Expr -> Expr -> Expr
    C.Cond (BinaryOp -> Expr -> Expr -> Expr
    C.BinaryOp BinaryOp
    C.LT Expr
    e (Type a -> Integer -> Expr
    forall a. Type a -> Integer -> Expr
    constNumTy Type a
    ty Integer
    0)) (Type a -> Integer -> Expr
    forall a. Type a -> Integer -> Expr
    constNumTy Type a
    ty (-Integer
    1))

    -- | Transform a Copilot Core literal, based on its value and type, into a C99
    -- literal.
    constTy :: Type a -> a -> C.Expr
    constTy :: forall a. Type a -> a -> Expr
    constTy Type a
    ty = case Type a
    ty of
      Type a
    Bool      -> a -> Expr
    Bool -> Expr
    C.LitBool
      Type a
    Int8      -> Type a -> Expr -> Expr
    forall a. Type a -> Expr -> Expr
    explicitTy Type a
    ty (Expr -> Expr) -> (a -> Expr) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Expr
    C.LitInt (Integer -> Expr) -> (a -> Integer) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral
      Type a
    Int16     -> Type a -> Expr -> Expr
    forall a. Type a -> Expr -> Expr
    explicitTy Type a
    ty (Expr -> Expr) -> (a -> Expr) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Expr
    C.LitInt (Integer -> Expr) -> (a -> Integer) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral
      Type a
    Int32     -> Type a -> Expr -> Expr
    forall a. Type a -> Expr -> Expr
    explicitTy Type a
    ty (Expr -> Expr) -> (a -> Expr) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Expr
    C.LitInt (Integer -> Expr) -> (a -> Integer) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral
      Type a
    Int64     -> Type a -> Expr -> Expr
    forall a. Type a -> Expr -> Expr
    explicitTy Type a
    ty (Expr -> Expr) -> (a -> Expr) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Expr
    C.LitInt (Integer -> Expr) -> (a -> Integer) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral
      Type a
    Word8     -> Type a -> Expr -> Expr
    forall a. Type a -> Expr -> Expr
    explicitTy Type a
    ty (Expr -> Expr) -> (a -> Expr) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Expr
    C.LitInt (Integer -> Expr) -> (a -> Integer) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral
      Type a
    Word16    -> Type a -> Expr -> Expr
    forall a. Type a -> Expr -> Expr
    explicitTy Type a
    ty (Expr -> Expr) -> (a -> Expr) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Expr
    C.LitInt (Integer -> Expr) -> (a -> Integer) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral
      Type a
    Word32    -> Type a -> Expr -> Expr
    forall a. Type a -> Expr -> Expr
    explicitTy Type a
    ty (Expr -> Expr) -> (a -> Expr) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Expr
    C.LitInt (Integer -> Expr) -> (a -> Integer) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral
      Type a
    Word64    -> Type a -> Expr -> Expr
    forall a. Type a -> Expr -> Expr
    explicitTy Type a
    ty (Expr -> Expr) -> (a -> Expr) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Expr
    C.LitInt (Integer -> Expr) -> (a -> Integer) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral
      Type a
    Float     -> Type a -> Expr -> Expr
    forall a. Type a -> Expr -> Expr
    explicitTy Type a
    ty (Expr -> Expr) -> (a -> Expr) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Expr
    Float -> Expr
    C.LitFloat
      Type a
    Double    -> Type a -> Expr -> Expr
    forall a. Type a -> Expr -> Expr
    explicitTy Type a
    ty (Expr -> Expr) -> (a -> Expr) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Expr
    Double -> Expr
    C.LitDouble
      Struct a
    _  -> TypeName -> NonEmpty InitItem -> Expr
    C.InitVal (Type a -> TypeName
    forall a. Type a -> TypeName
    transTypeName Type a
    ty) (NonEmpty InitItem -> Expr)
    -> (a -> NonEmpty InitItem) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Value a] -> NonEmpty InitItem
    forall a. [Value a] -> NonEmpty InitItem
    constStruct ([Value a] -> NonEmpty InitItem)
    -> (a -> [Value a]) -> a -> NonEmpty InitItem
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> [Value a]
    forall a. Struct a => a -> [Value a]
    toValues
      Array Type t
    ty' -> TypeName -> NonEmpty InitItem -> Expr
    C.InitVal (Type a -> TypeName
    forall a. Type a -> TypeName
    transTypeName Type a
    ty) (NonEmpty InitItem -> Expr)
    -> (a -> NonEmpty InitItem) -> a -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type t -> [t] -> NonEmpty InitItem
    forall a. Type a -> [a] -> NonEmpty InitItem
    constArray Type t
    ty' ([t] -> NonEmpty InitItem) -> (a -> [t]) -> a -> NonEmpty InitItem
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> [t]
    Array n t -> [t]
    forall (n :: Nat) a. Array n a -> [a]
    arrayElems

    -- | Transform a Copilot Core literal, based on its value and type, into a C99
    -- initializer.
    constInit :: Type a -> a -> C.Init
    constInit :: forall a. Type a -> a -> Init
    constInit Type a
    ty a
    val = case Type a
    ty of
      -- We include two special cases for Struct and Array to avoid using constTy
      -- on them.
      --
      -- In the default case (i.e., InitExpr (constTy ty val)), constant
      -- initializations are explicitly cast. However, doing so 1) may result in
      -- incorrect values for arrays, and 2) will be considered a non-constant
      -- expression in the case of arrays and structs, and thus not allowed as the
      -- initialization value for a global variable.
      --
      -- In particular, wrt. (1), for example, the nested array:
      --   [[0, 1], [2, 3]] :: Array 2 (Array 2 Int32)
      --
      -- with explicit casts, will be initialized in C as:
      --   { (int32_t[2]){(int32_t)(0), (int32_t)(1)},
      --     (int32_t[2]){(int32_t)(2), (int32_t)(3)} }
      --
      -- Due to the additional (int32_t[2]) casts, a C compiler will interpret the
      -- whole expression as an array of two int32_t's (as opposed to a nested
      -- array). This can either lead to compile-time errors (if you're lucky) or
      -- incorrect runtime semantics (if you're unlucky).
      Array Type t
    ty' -> NonEmpty InitItem -> Init
    C.InitList (NonEmpty InitItem -> Init) -> NonEmpty InitItem -> Init
    forall a b. (a -> b) -> a -> b
    $ Type t -> [t] -> NonEmpty InitItem
    forall a. Type a -> [a] -> NonEmpty InitItem
    constArray Type t
    ty' ([t] -> NonEmpty InitItem) -> [t] -> NonEmpty InitItem
    forall a b. (a -> b) -> a -> b
    $ Array n t -> [t]
    forall (n :: Nat) a. Array n a -> [a]
    arrayElems a
    Array n t
    val

      -- We use InitArray to initialize a struct because the syntax used for
      -- initializing arrays and structs is compatible. For instance, {1, 2} works
      -- both for initializing an int array of length 2 as well as a struct with
      -- two int fields, although the two expressions are conceptually different
      -- (structs can also be initialized as { .a = 1, .b = 2}.
      Struct a
    _  -> NonEmpty InitItem -> Init
    C.InitList (NonEmpty InitItem -> Init) -> NonEmpty InitItem -> Init
    forall a b. (a -> b) -> a -> b
    $ [Value a] -> NonEmpty InitItem
    forall a. [Value a] -> NonEmpty InitItem
    constStruct (a -> [Value a]
    forall a. Struct a => a -> [Value a]
    toValues a
    val)
      Type a
    _         -> Expr -> Init
    C.InitExpr (Expr -> Init) -> Expr -> Init
    forall a b. (a -> b) -> a -> b
    $ Type a -> a -> Expr
    forall a. Type a -> a -> Expr
    constTy Type a
    ty a
    val

    -- | Transform a Copilot Core struct field into a C99 initializer.
    constFieldInit :: Value a -> C.InitItem
    constFieldInit :: forall a. Value a -> InitItem
    constFieldInit (Value Type t
    ty (Field t
    val)) = Maybe Name -> Init -> InitItem
    C.InitItem Maybe Name
    forall a. Maybe a
    Nothing (Init -> InitItem) -> Init -> InitItem
    forall a b. (a -> b) -> a -> b
    $ Type t -> t -> Init
    forall a. Type a -> a -> Init
    constInit Type t
    ty t
    val

    -- | Transform a Copilot Struct, based on the struct fields, into a list of C99
    -- initializer values.
    constStruct :: [Value a] -> NonEmpty.NonEmpty C.InitItem
    constStruct :: forall a. [Value a] -> NonEmpty InitItem
    constStruct [Value a]
    val = [InitItem] -> NonEmpty InitItem
    forall a. HasCallStack => [a] -> NonEmpty a
    NonEmpty.fromList ([InitItem] -> NonEmpty InitItem)
    -> [InitItem] -> NonEmpty InitItem
    forall a b. (a -> b) -> a -> b
    $ (Value a -> InitItem) -> [Value a] -> [InitItem]
    forall a b. (a -> b) -> [a] -> [b]
    map Value a -> InitItem
    forall a. Value a -> InitItem
    constFieldInit [Value a]
    val

    -- | Transform a Copilot Array, based on the element values and their type,
    -- into a list of C99 initializer values.
    constArray :: Type a -> [a] -> NonEmpty.NonEmpty C.InitItem
    constArray :: forall a. Type a -> [a] -> NonEmpty InitItem
    constArray Type a
    ty =
      [InitItem] -> NonEmpty InitItem
    forall a. HasCallStack => [a] -> NonEmpty a
    NonEmpty.fromList ([InitItem] -> NonEmpty InitItem)
    -> ([a] -> [InitItem]) -> [a] -> NonEmpty InitItem
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> InitItem) -> [a] -> [InitItem]
    forall a b. (a -> b) -> [a] -> [b]
    map (Maybe Name -> Init -> InitItem
    C.InitItem Maybe Name
    forall a. Maybe a
    Nothing (Init -> InitItem) -> (a -> Init) -> a -> InitItem
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type a -> a -> Init
    forall a. Type a -> a -> Init
    constInit Type a
    ty)

    -- | Explicitly cast a C99 value to a type.
    explicitTy :: Type a -> C.Expr -> C.Expr
    explicitTy :: forall a. Type a -> Expr -> Expr
    explicitTy Type a
    ty = TypeName -> Expr -> Expr
    C.Cast (Type a -> TypeName
    forall a. Type a -> TypeName
    transTypeName Type a
    ty)

    -- Translate a literal number of type @ty@ into a C99 literal.
    --
    -- PRE: The type of PRE is numeric (integer or floating-point), that
    -- is, not boolean, struct or array.
    constNumTy :: Type a -> Integer -> C.Expr
    constNumTy :: forall a. Type a -> Integer -> Expr
    constNumTy Type a
    ty =
      case Type a
    ty of
        Type a
    Float  -> Float -> Expr
    C.LitFloat (Float -> Expr) -> (Integer -> Float) -> Integer -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Float
    forall a. Num a => Integer -> a
    fromInteger
        Type a
    Double -> Double -> Expr
    C.LitDouble (Double -> Expr) -> (Integer -> Double) -> Integer -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Double
    forall a. Num a => Integer -> a
    fromInteger
        Type a
    _      -> Integer -> Expr
    C.LitInt

    -- | Provide a specialized function name in C99 for a function given the type
    -- of its arguments, and its "family" name.
    --
    -- C99 provides multiple variants of the same conceptual function, based on the
    -- types. Depending on the function, common variants exist for signed/unsigned
    -- arguments, long or short types, float or double. The C99 standard uses the
    -- same mechanism to name most such functions: the default variant works for
    -- double, and there are additional variants for float and long double. For
    -- example, the sin function operates on double, while sinf operates on float,
    -- and sinl operates on long double.
    --
    -- This function only knows how to provide specialized names for functions in
    -- math.h that provide a default version for a double argument and vary for
    -- floats. It won't change the function name given if the variation is based on
    -- the return type, if the function is defined elsewhere, or for other types.
    specializeMathFunName :: Type a -> String -> String
    specializeMathFunName :: forall a. Type a -> Name -> Name
    specializeMathFunName Type a
    ty Name
    s
        -- The following function pattern matches based on the variants available
        -- for a specific function.
        --
        -- Do not assume that a function you need implemented follows the same
        -- standard as others: check whether it is present in the standard.
        | Name -> Bool
    isMathFPArgs Name
    s
        , Type a
    Float <- Type a
    ty
        = Name
    s Name -> Name -> Name
    forall a. [a] -> [a] -> [a]
    ++ Name
    "f"

        | Bool
    otherwise
        = Name
    s
      where
        -- True if the function family name is part of math.h and follows the
        -- standard rule of providing multiple variants for floating point numbers
        -- based on the type of their arguments.
        --
        -- Note: nan is not in this list because the names of its variants are
        -- determined by the return type.
        --
        -- For details, see:
        -- "B.11 Mathematics <math.h>" in the C99 standard
        isMathFPArgs :: String -> Bool
        isMathFPArgs :: Name -> Bool
    isMathFPArgs = (Name -> [Name] -> Bool) -> [Name] -> Name -> Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Name -> [Name] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    elem
           [ Name
    "acos",   Name
    "asin",     Name
    "atan",      Name
    "atan2",      Name
    "cos",    Name
    "sin"
           , Name
    "tan",    Name
    "acosh",    Name
    "asinh",     Name
    "atanh",      Name
    "cosh",   Name
    "sinh"
           , Name
    "tanh",   Name
    "exp",      Name
    "exp2",      Name
    "expm1",      Name
    "frexp",  Name
    "ilogb"
           , Name
    "ldexp",  Name
    "log",      Name
    "log10",     Name
    "log1p",      Name
    "log2",   Name
    "logb"
           , Name
    "modf",   Name
    "scalbn",   Name
    "scalbln",   Name
    "cbrt",       Name
    "fabs",   Name
    "hypot"
           , Name
    "pow",    Name
    "sqrt",     Name
    "erf",       Name
    "erfc",       Name
    "lgamma", Name
    "tgamma"
           , Name
    "ceil",   Name
    "floor",    Name
    "nearbyint", Name
    "rint",       Name
    "lrint",  Name
    "llrint"
           , Name
    "round",  Name
    "lround",   Name
    "llround",   Name
    "trunc",      Name
    "fmod",   Name
    "remainder"
           , Name
    "remquo", Name
    "copysign", Name
    "nextafter", Name
    "nexttoward", Name
    "fdim"
           , Name
    "fmax",   Name
    "fmin",     Name
    "fma"
           ]

    -- * Auxiliary functions

    -- | True if the type given is a floating point number.
    typeIsFloating :: Type a -> Bool
    typeIsFloating :: forall a. Type a -> Bool
    typeIsFloating Type a
    Float  = Bool
    True
    typeIsFloating Type a
    Double = Bool
    True
    typeIsFloating Type a
    _      = Bool
    False

    -- | 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 = (Int, [C.Decln], [C.Stmt])

    -- | Define a C expression that calls a function with arguments.
    funCall :: C.Ident   -- ^ Function name
            -> [C.Expr]  -- ^ Arguments
            -> C.Expr
    funCall :: Name -> [Expr] -> Expr
    funCall Name
    name = Expr -> [Expr] -> Expr
    C.Funcall (Name -> Expr
    C.Ident Name
    name)

    -- 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 (Name -> Expr
    C.Ident Name
    "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