Internal.hs

{-# LANGUAGE ScopedTypeVariables #-}

module C.Operator.Internal where

import Control.Arrow (first, second, (***))
import Control.Exception (assert)
import Data.Kind qualified as Hs
import Data.Nat (Nat (..))
import Data.Vec.Lazy (Vec (..))
import Data.Void qualified as Absurd
import GHC.Generics (Generic)

import C.Type

--------------------------------------------------------------------------------

-- | **Internal implementation detail**
--
-- How is a C operator, when instantiated at a particular type, implemented?
type OpImpl :: Nat -> Hs.Type
data OpImpl n
  = -- | Convert arguments with the given conversions and then apply
    -- the implied function (e.g. addition for the 'Add' class)
    -- at the resulting type.
    ConvertThenOp
      {argumentConversions :: !(Vec n [Conversion])}
  | -- | Add an integral value and a pointer.
    AddIntegralAndPtr
  | -- | Add a pointer and an integral value.
    AddPtrAndIntegral
  | -- | Get the difference between two pointers.
    SubPtrAndPtr
  | -- | Subtract an integral value from a pointer.
    SubPtrAndIntegral
  deriving stock (Generic, Show)

data Conversion
  = FromIntegralTo {fromIntegralTo :: !(Type Absurd.Void)}
  | RealToFracTo {realToFracTo :: !(Type Absurd.Void)}
  | PtrToInt
  deriving stock (Generic, Show)

--------------------------------------------------------------------------------

type Op :: Nat -> Hs.Type
data Op arity where
  UnaryOp :: UnaryOp -> Op (S Z)
  BinaryOp :: BinaryOp -> Op (S (S Z))

data UnaryOp
  = -- | @+@
    UnaryPlus
  | -- | @-@
    UnaryMinus
  | -- | @!@
    LogicalNot
  | -- | @~@
    BitwiseNot
  deriving stock (Bounded, Enum, Eq, Ord, Show)

data BinaryOp
  = -- | @*@
    Mult
  | -- | @/@
    Div
  | -- | @%@
    Rem
  | -- | @+@
    Add
  | -- | @-@
    Sub
  | -- | @<<@
    ShiftLeft
  | -- | @>>@
    ShiftRight
  | -- | @<@
    RelLT
  | -- | @<=@
    RelLE
  | -- | @>@
    RelGT
  | -- | @>=@
    RelGE
  | -- | @==@
    RelEQ
  | -- | @!=@
    RelNE
  | -- | @&@
    BitwiseAnd
  | -- | @^@
    BitwiseXor
  | -- | @|@
    BitwiseOr
  | -- | @&&@
    LogicalAnd
  | -- | @||@
    LogicalOr
  deriving stock (Bounded, Enum, Eq, Ord, Show)

pprOp :: Op arity -> String
pprOp = \case
  UnaryOp op ->
    case op of
      UnaryPlus -> "+"
      UnaryMinus -> "-"
      LogicalNot -> "!"
      BitwiseNot -> "~"
  BinaryOp op ->
    case op of
      Mult -> "*"
      Div -> "/"
      Rem -> "%"
      Add -> "+"
      Sub -> "-"
      ShiftLeft -> "<<"
      ShiftRight -> ">>"
      RelLT -> "<"
      RelLE -> "<="
      RelGT -> ">"
      RelGE -> ">="
      RelEQ -> "=="
      RelNE -> "!="
      BitwiseAnd -> "&"
      BitwiseXor -> "^"
      BitwiseOr -> "|"
      LogicalAnd -> "&&"
      LogicalOr -> "||"

pprOpApp :: forall arity. Op arity -> Vec arity String -> String
pprOpApp op args =
  case op of
    UnaryOp{} -> unary
    BinaryOp{} -> binary
 where
  unary :: (arity ~ S Z) => String
  unary =
    case args of
      a ::: VNil ->
        pprOp op ++ a
  binary :: (arity ~ S (S Z)) => String
  binary =
    case args of
      a ::: b ::: VNil ->
        a ++ pprOp op ++ b

--------------------------------------------------------------------------------

opResTypeAndImpl
  :: forall arity a
   . (Eq a) => Platform -> Op arity -> Vec arity (Type a) -> Maybe (Type a, OpImpl arity)
opResTypeAndImpl plat op args =
  case op of
    UnaryOp o ->
      case o of
        UnaryPlus -> unary unaryPlusType
        UnaryMinus -> unary unaryMinusType
        LogicalNot -> unary unaryLogicalType
        BitwiseNot -> unary integralUnaryType
    BinaryOp o ->
      case o of
        Mult -> binary binaryMultiplicativeType
        Div -> binary binaryMultiplicativeType
        Rem -> binary integralBinaryType
        Add -> binary binaryAddType
        Sub -> binary binarySubType
        ShiftLeft -> binary shiftType
        ShiftRight -> binary shiftType
        RelLT -> binary binaryRelType
        RelLE -> binary binaryRelType
        RelGT -> binary binaryRelType
        RelGE -> binary binaryRelType
        RelEQ -> binary binaryEqType
        RelNE -> binary binaryEqType
        BitwiseAnd -> binary integralBinaryType
        BitwiseXor -> binary integralBinaryType
        BitwiseOr -> binary integralBinaryType
        LogicalAnd -> binary binaryLogicalType
        LogicalOr -> binary binaryLogicalType
 where
  unary :: (arity ~ S Z) => (Platform -> Type a -> Maybe r) -> Maybe r
  unary f =
    case args of
      a ::: VNil ->
        f plat a
  binary :: (arity ~ S (S Z)) => (Platform -> Type a -> Type a -> Maybe r) -> Maybe r
  binary f =
    case args of
      a ::: b ::: VNil ->
        f plat a b

--------------------------------------------------------------------------------

-- | Result type of unary @+@
unaryPlusType :: Platform -> Type a -> Maybe (Type a, OpImpl (S Z))
unaryPlusType plat = \case
  Arithmetic ty ->
    Just $ mkArithConv1 $ arithmeticPromotion plat ty
  Ptr{} ->
    -- The C++ standard allows unary plus on pointers, but the C standard doesn't.
    Nothing
  Void -> Nothing

-- | Result type of unary @-@
unaryMinusType :: Platform -> Type a -> Maybe (Type a, OpImpl (S Z))
unaryMinusType plat = \case
  Arithmetic ty ->
    Just $ mkArithConv1 $ arithmeticPromotion plat ty
  Ptr{} -> Nothing
  Void -> Nothing

-- | Result type of binary @+@
binaryAddType :: Platform -> Type a -> Type a -> Maybe (Type a, OpImpl (S (S Z)))
binaryAddType plat (Arithmetic a1) (Arithmetic a2) =
  Just $ mkArithConv2 $ arithmeticConversion plat a1 a2
binaryAddType _ (Arithmetic (Integral{})) ptr@(Ptr{}) =
  Just (ptr, AddIntegralAndPtr)
binaryAddType _ ptr@(Ptr{}) (Arithmetic (Integral{})) =
  Just (ptr, AddPtrAndIntegral)
binaryAddType _ _ _ =
  Nothing

-- | Result type of binary @-@
binarySubType :: (Eq a) => Platform -> Type a -> Type a -> Maybe (Type a, OpImpl (S (S Z)))
binarySubType plat (Arithmetic a1) (Arithmetic a2) =
  Just $ mkArithConv2 $ arithmeticConversion plat a1 a2
binarySubType _ ptr@(Ptr{}) (Arithmetic (Integral{})) =
  Just (ptr, SubPtrAndIntegral)
binarySubType _ (Ptr ty1) (Ptr ty2)
  | ty1 == ty2 =
      -- TODO: do we want to be more lenient in allowing subtraction of pointers
      -- with different pointee types, e.g. allow @(x :: Ptr Void) - (y :: Ptr Int)@?
      Just (Arithmetic $ Integral $ IntLike PtrDiff, SubPtrAndPtr)
binarySubType _ _ _ =
  Nothing

-- | Result type for multiplication and division (integral and floating-point)
binaryMultiplicativeType :: Platform -> Type a -> Type a -> Maybe (Type a, OpImpl (S (S Z)))
binaryMultiplicativeType plat (Arithmetic a1) (Arithmetic a2) =
  Just $ mkArithConv2 $ arithmeticConversion plat a1 a2
binaryMultiplicativeType _ _ _ = Nothing

-- | Result type for bitwise not operator
integralUnaryType :: Platform -> Type a -> Maybe (Type a, OpImpl (S Z))
integralUnaryType plat (Arithmetic a1)
  | Integral{} <- a1 =
      Just $ mkArithConv1 $ arithmeticPromotion plat a1
integralUnaryType _ _ = Nothing

-- | Type for integral remainder and binary bitwise logic operators
integralBinaryType :: Platform -> Type a -> Type a -> Maybe (Type a, OpImpl (S (S Z)))
integralBinaryType plat (Arithmetic a1) (Arithmetic a2)
  | Integral{} <- a1
  , Integral{} <- a2 =
      Just $ mkArithConv2 $ arithmeticConversion plat a1 a2
integralBinaryType _ _ _ = Nothing

-- | Type for binary shift operators
shiftType
  :: Platform
  -> Type a
  -- ^ type of the value being shifted
  -> Type a
  -- ^ type of the shift amount
  -> Maybe (Type a, OpImpl (S (S Z)))
shiftType plat (Arithmetic a1@(Integral{})) (Arithmetic a2@(Integral{})) =
  let (i1, c1) = arithmeticPromotion plat a1
      (_, c2) = arithmeticPromotion plat a2
   in Just (Arithmetic i1, ConvertThenOp (c1 ::: c2 ::: VNil))
shiftType _ _ _ =
  Nothing

intType, uintType :: Type a
intType = Arithmetic $ Integral $ IntLike $ Int Signed
uintType = Arithmetic $ Integral $ IntLike $ Int Unsigned

convertToInt :: Platform -> Type a -> Maybe [Conversion]
convertToInt _ = \case
  Arithmetic a -> Just $ case a of
    Integral i ->
      case i of
        IntLike (Int Signed) -> []
        _ -> [FromIntegralTo intType]
    FloatLike{} ->
      [RealToFracTo intType]
  Ptr{} ->
    Just [PtrToInt]
  _ ->
    Nothing

-- | Type for logical not operation @!@.
unaryLogicalType :: Platform -> Type a -> Maybe (Type a, OpImpl (S Z))
unaryLogicalType plat a = do
  _conv <- convertToInt plat a
  return $ (intType, ConvertThenOp ([] ::: VNil))

-- | Type for binary equality operators @==@ and @!=@.
binaryEqType :: (Eq a) => Platform -> Type a -> Type a -> Maybe (Type a, OpImpl (S (S Z)))
binaryEqType plat (Arithmetic a1) (Arithmetic a2) =
  Just $ mkArithConv2 (Integral $ IntLike $ Int Signed, snd $ arithmeticConversion plat a1 a2)
binaryEqType _ (Ptr ty1) (Ptr ty2)
  | ty1 == ty2 =
      -- TODO: does the C standard allow "Ptr Int" == "Ptr Void"?
      Just (intType, ConvertThenOp ([] ::: [] ::: VNil))
binaryEqType _ _ _ = Nothing

-- | Type for binary logical operators @&&@ and @||@.
binaryLogicalType :: Platform -> Type a -> Type a -> Maybe (Type a, OpImpl (S (S Z)))
binaryLogicalType plat a1 a2 = do
  _c1 <- convertToInt plat a1
  _c2 <- convertToInt plat a2
  return (intType, ConvertThenOp ([] ::: [] ::: VNil))

-- | Type for binary comparison operators @<@, @<=@, @>@, @>=@.
binaryRelType :: (Eq a) => Platform -> Type a -> Type a -> Maybe (Type a, OpImpl (S (S Z)))
binaryRelType plat (Arithmetic a1) (Arithmetic a2) =
  Just $ mkArithConv2 (Integral $ IntLike $ Int Signed, snd $ arithmeticConversion plat a1 a2)
binaryRelType _ (Ptr ty1) (Ptr ty2)
  | ty1 == ty2 =
      -- TODO: C is a bit more lenient than requiring the inner types to
      -- match exactly.
      Just (intType, ConvertThenOp ([] ::: [] ::: VNil))
binaryRelType _ _ _ = Nothing

mkArithConv1 :: (ArithmeticType, [Conversion]) -> (Type a, OpImpl (S Z))
mkArithConv1 =
  (Arithmetic *** (\a -> ConvertThenOp (a ::: VNil)))

mkArithConv2
  :: (ArithmeticType, ([Conversion], [Conversion])) -> (Type a, OpImpl (S (S Z)))
mkArithConv2 =
  (Arithmetic *** (\(a, b) -> ConvertThenOp (a ::: b ::: VNil)))

--------------------------------------------------------------------------------

arithmeticPromotion :: Platform -> ArithmeticType -> (ArithmeticType, [Conversion])
arithmeticPromotion _ f@(FloatLike{}) =
  (f, [])
arithmeticPromotion plat (Integral i) =
  first (Integral . IntLike) $ integralPromotion plat i

integralPromotion :: Platform -> IntegralType -> (IntLikeType, [Conversion])
-- C standard: Promotion from integral types (non bit-field case).
--
-- If the integer conversion rank of T is lower than that of int:
--
--   1. promote T to int if int can represent all the values of T,
--   2. otherwise promote T to unsigned int
integralPromotion plat (IntLike i)
  | intLikeTypeConversionRank plat i < intLikeTypeConversionRank plat (Int Signed) =
      if intLikeTypeFitsInInt plat i then
        (Int Signed, [FromIntegralTo intType])
      else
        (Int Unsigned, [FromIntegralTo uintType])
  | otherwise =
      (i, [])
integralPromotion plat (CharLike c) =
  assert
    (charLikeTypeSizeInBits plat c < intLikeTypeSizeInBits plat (Int Signed))
    (Int Signed, [FromIntegralTo intType])
integralPromotion _ Bool =
  (Int Signed, [FromIntegralTo intType])

--------------------------------------------------------------------------------
-- Arithmetic conversion

arithmeticConversion
  :: Platform
  -> ArithmeticType
  -> ArithmeticType
  -> (ArithmeticType, ([Conversion], [Conversion]))
arithmeticConversion plat (Integral i1) (Integral i2) =
  -- Both arguments are integral: do integral promotion then integral conversion.
  let
    (j1, c1) = integralPromotion plat i1
    (j2, c2) = integralPromotion plat i2
    (r, (d1, d2)) = integralArithmeticConversion plat j1 j2
   in
    (Integral $ IntLike r, (c1 ++ d1, c2 ++ d2))
-- At least one of the arguments is of floating-point type:
-- pick the largest floating-point type.
arithmeticConversion _ (FloatLike f1) (FloatLike f2) =
  ( FloatLike (max f1 f2)
  , (if f2 > f1 then [rf f2] else [], if f1 > f2 then [rf f1] else [])
  )
 where
  rf f = RealToFracTo $ Arithmetic $ FloatLike f
arithmeticConversion _ f@(FloatLike{}) (Integral{}) =
  (f, ([], [FromIntegralTo (Arithmetic f)]))
arithmeticConversion _ (Integral{}) f@(FloatLike{}) =
  (f, ([FromIntegralTo (Arithmetic f)], []))

integralArithmeticConversion
  :: Platform -> IntLikeType -> IntLikeType -> (IntLikeType, ([Conversion], [Conversion]))
integralArithmeticConversion plat t1 t2
  -- The following rules are applied to determine the arithmetic conversion result type 'C':
  --
  --   1. If 'T1' and 'T2' are the same type, 'C' is that type.
  | t1 == t2 =
      (t1, ([], []))
  --   2. If T1 and T2 are both signed integer types or both unsigned integer types,
  --      C is the type of greater integer conversion rank.
  | s1 == s2 =
      if rk1 >= rk2 then
        (t1, ([], [FromIntegralTo (Arithmetic $ Integral $ IntLike t1)]))
      else
        (t2, ([FromIntegralTo (Arithmetic $ Integral $ IntLike t2)], []))
  | otherwise =
      --   3. Otherwise, the types are of different signs.
      --      Implement the logic in 'integralArithmeticConversion_differentSigns'.
      case s1 of
        Signed ->
          integralArithmeticConversion_differentSigns plat (t1, rk1) (t2, rk2)
        Unsigned ->
          second (\(c1, c2) -> (c2, c1)) $
            integralArithmeticConversion_differentSigns plat (t2, rk2) (t1, rk1)
 where
  s1, s2 :: Sign
  s1 = intLikeTypeSign t1
  s2 = intLikeTypeSign t2
  rk1, rk2 :: IntegerConversionRank
  rk1 = intLikeTypeConversionRank plat t1
  rk2 = intLikeTypeConversionRank plat t2

integralArithmeticConversion_differentSigns
  :: Platform
  -> (IntLikeType, IntegerConversionRank)
  -- ^ the signed type
  -> (IntLikeType, IntegerConversionRank)
  -- ^ the unsigned type
  -> (IntLikeType, ([Conversion], [Conversion]))
integralArithmeticConversion_differentSigns plat s@(t_s, rk_s) u@(t_u, rk_u)
  -- Implement the following rules to determine the arithmetic conversion
  -- result type C for signed type S and unsigned type U:
  --
  --   1. If the rank of U is greater than or equal to the rank of S, C is U.
  | rk_u >= rk_s =
      (t_u, ([FromIntegralTo (Arithmetic $ Integral $ IntLike t_u)], []))
  -- Otherwise, S has (strictly) greater rank than U.
  --
  --   2. If S can represent all of the values of U, C is S.
  | unsignedFitsInSigned plat t_u t_s =
      (t_s, ([], [FromIntegralTo (Arithmetic $ Integral $ IntLike t_s)]))
  --   3. Otherwise, C is the unsigned integer type corresponding to S.
  | otherwise =
      ( \iTy ->
          let ty = Arithmetic $ Integral $ IntLike iTy
           in (iTy, ([FromIntegralTo ty], [FromIntegralTo ty]))
      )
        $ case t_s of
          Short{} -> Short Unsigned
          Int{} -> Int Unsigned
          Long{} -> Long Unsigned
          LongLong{} -> LongLong Unsigned
          _ ->
            -- Should never happen, because any unsigned type of rank strictly
            -- less than that of ptrdiff_t fits into ptrdiff_t.
            error $
              unlines
                [ "integralArithmeticConversion_differentSigns: extended type"
                , "ty: " ++ show t_s
                , "s: " ++ show s
                , "u: " ++ show u
                ]

-- | Does the given unsigned type fit into the given signed type?
unsignedFitsInSigned
  :: Platform
  -> IntLikeType
  -- ^ the unsigned type
  -> IntLikeType
  -- ^ the signed type
  -> Bool
unsignedFitsInSigned plat u s =
  intLikeTypeSizeInBits plat s > intLikeTypeSizeInBits plat u

--------------------------------------------------------------------------------