{-# 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, modify )
import qualified Data.List.NonEmpty  as NonEmpty
import qualified Language.C99.Simple as C

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

-- Internal imports
import Copilot.Compile.C99.Error ( impossible )
import Copilot.Compile.C99.Name  ( exCpyName, streamAccessorName )
import Copilot.Compile.C99.Type  ( transLocalVarDeclType, 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
  Expr
e1' <- Expr a1 -> State FunEnv Expr
forall a. Expr a -> State FunEnv Expr
transExpr Expr a1
e1
  let cTy1 :: Type
cTy1     = Type a1 -> Type
forall a. Type a -> Type
transLocalVarDeclType Type a1
ty1
      initExpr :: Maybe Init
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
  (FunEnv -> FunEnv) -> StateT FunEnv Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (FunEnv -> FunEnv -> FunEnv
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])

  Expr a -> State FunEnv Expr
forall a. Expr a -> State FunEnv Expr
transExpr Expr a
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 Id
sId) = do
  let accessVar :: Name
accessVar = Id -> Name
streamAccessorName Id
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
  Expr
e' <- Expr a1 -> State FunEnv Expr
forall a. Expr a -> State FunEnv Expr
transExpr Expr a1
e
  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
$ Op1 a1 a -> Expr -> Expr
forall a b. Op1 a b -> Expr -> Expr
transOp1 Op1 a1 a
op Expr
e'

transExpr (Op2 Op2 a1 b a
op Expr a1
e1 Expr b
e2) = do
  Expr
e1' <- Expr a1 -> State FunEnv Expr
forall a. Expr a -> State FunEnv Expr
transExpr Expr a1
e1
  Expr
e2' <- Expr b -> State FunEnv Expr
forall a. Expr a -> State FunEnv Expr
transExpr Expr b
e2
  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
$ Op2 a1 b a -> Expr -> Expr -> Expr
forall a b c. Op2 a b c -> Expr -> Expr -> Expr
transOp2 Op2 a1 b a
op Expr
e1' Expr
e2'

transExpr (Op3 Op3 a1 b c a
op Expr a1
e1 Expr b
e2 Expr c
e3) = do
  Expr
e1' <- Expr a1 -> State FunEnv Expr
forall a. Expr a -> State FunEnv Expr
transExpr Expr a1
e1
  Expr
e2' <- Expr b -> State FunEnv Expr
forall a. Expr a -> State FunEnv Expr
transExpr Expr b
e2
  Expr
e3' <- Expr c -> State FunEnv Expr
forall a. Expr a -> State FunEnv Expr
transExpr Expr c
e3
  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
$ Op3 a1 b c a -> Expr -> Expr -> Expr -> Expr
forall a b c d. Op3 a b c d -> Expr -> Expr -> Expr -> Expr
transOp3 Op3 a1 b c a
op Expr
e1' Expr
e2' Expr
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.
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

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

-- | 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 = [C.Decln]

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