{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Translate Copilot Core expressions and operators to Bluespec.
module Copilot.Compile.Bluespec.Expr
  ( transExpr
  , cIndexVector
  , cLit
  , constTy
  , genVector
  ) where

-- External imports
import Data.Foldable (foldl')
import Data.String (IsString (..))
import qualified Language.Bluespec.Classic.AST as BS
import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS
import Numeric.Floating.IEEE.NaN (isSignaling, setPayloadSignaling, setPayload, getPayload)
import GHC.Float (double2Float, castFloatToWord32, castDoubleToWord64, float2Double)

-- Internal imports: Copilot
import Copilot.Core

-- Internal imports
import Copilot.Compile.Bluespec.Error (impossible)
import Copilot.Compile.Bluespec.Name
import Copilot.Compile.Bluespec.Type

-- | Translates a Copilot Core expression into a Bluespec expression.
transExpr :: Expr a -> BS.CExpr
transExpr :: forall a. Expr a -> CExpr
transExpr (Const Type a
ty a
x) = Type a -> a -> CExpr
forall a. Type a -> a -> CExpr
constTy Type a
ty a
x

transExpr (Local Type a1
ty1 Type a
_ Name
name Expr a1
e1 Expr a
e2) =
  let nameId :: Id
nameId = Position -> FString -> Id
BS.mkId Position
BS.NoPos (FString -> Id) -> FString -> Id
forall a b. (a -> b) -> a -> b
$ Name -> FString
forall a. IsString a => Name -> a
fromString Name
name
      e1' :: CExpr
e1'    = Expr a1 -> CExpr
forall a. Expr a -> CExpr
transExpr Expr a1
e1
      ty1' :: CType
ty1'   = Type a1 -> CType
forall a. Type a -> CType
transType Type a1
ty1
      e2' :: CExpr
e2'    = Expr a -> CExpr
forall a. Expr a -> CExpr
transExpr Expr a
e2 in
  [CDefl] -> CExpr -> CExpr
BS.Cletrec
    [ CDef -> [CQual] -> CDefl
BS.CLValueSign
        (Id -> CQType -> [CClause] -> CDef
BS.CDef Id
nameId ([CPred] -> CType -> CQType
BS.CQType [] CType
ty1') [[CPat] -> [CQual] -> CExpr -> CClause
BS.CClause [] [] CExpr
e1'])
        []
    ]
    CExpr
e2'

transExpr (Var Type a
_ Name
n) = Id -> CExpr
BS.CVar (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> FString -> Id
BS.mkId Position
BS.NoPos (FString -> Id) -> FString -> Id
forall a b. (a -> b) -> a -> b
$ Name -> FString
forall a. IsString a => Name -> a
fromString Name
n

transExpr (Drop Type a
_ DropIdx
amount Id
sid) =
  let accessVar :: Name
accessVar = Id -> Name
streamAccessorName Id
sid
      index :: Literal
index     = IntLit -> Literal
BS.LInt (IntLit -> Literal) -> IntLit -> Literal
forall a b. (a -> b) -> a -> b
$ Integer -> IntLit
BS.ilDec (Integer -> IntLit) -> Integer -> IntLit
forall a b. (a -> b) -> a -> b
$ DropIdx -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral DropIdx
amount in
  CExpr -> [CExpr] -> CExpr
BS.CApply (Id -> CExpr
BS.CVar (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> FString -> Id
BS.mkId Position
BS.NoPos (FString -> Id) -> FString -> Id
forall a b. (a -> b) -> a -> b
$ Name -> FString
forall a. IsString a => Name -> a
fromString Name
accessVar)
            [CLiteral -> CExpr
BS.CLit (CLiteral -> CExpr) -> CLiteral -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Literal -> CLiteral
BS.CLiteral Position
BS.NoPos Literal
index]

transExpr (ExternVar Type a
_ Name
name Maybe [a]
_) =
  CExpr -> Id -> CExpr
BS.CSelect
    (Id -> CExpr
BS.CVar (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> FString -> Id
BS.mkId Position
BS.NoPos (FString -> Id) -> FString -> Id
forall a b. (a -> b) -> a -> b
$ Name -> FString
forall a. IsString a => Name -> a
fromString (Name -> FString) -> Name -> FString
forall a b. (a -> b) -> a -> b
$ Name -> Name
wireName Name
name)
    (Position -> Id
BS.id_read Position
BS.NoPos)

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

transExpr (Op1 Op1 a1 a
op Expr a1
e) = Op1 a1 a -> CExpr -> CExpr
forall a b. Op1 a b -> CExpr -> CExpr
transOp1 Op1 a1 a
op (Expr a1 -> CExpr
forall a. Expr a -> CExpr
transExpr Expr a1
e)

transExpr (Op2 Op2 a1 b a
op Expr a1
e1 Expr b
e2) = Op2 a1 b a -> CExpr -> CExpr -> CExpr
forall a b c. Op2 a b c -> CExpr -> CExpr -> CExpr
transOp2 Op2 a1 b a
op (Expr a1 -> CExpr
forall a. Expr a -> CExpr
transExpr Expr a1
e1) (Expr b -> CExpr
forall a. Expr a -> CExpr
transExpr Expr b
e2)

transExpr (Op3 Op3 a1 b c a
op Expr a1
e1 Expr b
e2 Expr c
e3) =
  Op3 a1 b c a -> CExpr -> CExpr -> CExpr -> CExpr
forall a b c d. Op3 a b c d -> CExpr -> CExpr -> CExpr -> CExpr
transOp3 Op3 a1 b c a
op (Expr a1 -> CExpr
forall a. Expr a -> CExpr
transExpr Expr a1
e1) (Expr b -> CExpr
forall a. Expr a -> CExpr
transExpr Expr b
e2) (Expr c -> CExpr
forall a. Expr a -> CExpr
transExpr Expr c
e3)

-- | Translates a Copilot unary operator and its argument into a Bluespec
-- function.
transOp1 :: Op1 a b -> BS.CExpr -> BS.CExpr
transOp1 :: forall a b. Op1 a b -> CExpr -> CExpr
transOp1 Op1 a b
op CExpr
e =
  case Op1 a b
op of
    Op1 a b
Not         -> Id -> CExpr
app Id
BS.idNot
    Abs     Type a
_ty -> Id -> CExpr
app (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"abs"
    Sign     Type a
ty -> Type a -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
transSign Type a
ty CExpr
e
    -- Bluespec's Arith class does not have a `recip` method corresponding to
    -- Haskell's `recip` in the `Fractional` class, so we implement it
    -- ourselves.
    Recip    Type a
ty -> CExpr -> [CExpr] -> CExpr
BS.CApply
                     (Id -> CExpr
BS.CVar (Position -> Id
BS.idSlashAt Position
BS.NoPos))
                     [Type a -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constNumTy Type a
ty Integer
1, CExpr
e]
    BwNot   Type a
_ty -> Id -> CExpr
app (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Id
BS.idInvertAt Position
BS.NoPos

    Cast Type a
fromTy Type b
toTy -> Type a -> Type b -> CExpr -> CExpr
forall a b. Type a -> Type b -> CExpr -> CExpr
transCast Type a
fromTy Type b
toTy CExpr
e
    GetField (Struct a
_)  Type b
_ a -> Field s b
f -> CExpr -> Id -> CExpr
BS.CSelect CExpr
e (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> FString -> Id
BS.mkId Position
BS.NoPos (FString -> Id) -> FString -> Id
forall a b. (a -> b) -> a -> b
$
                                Name -> FString
forall a. IsString a => Name -> a
fromString (Name -> FString) -> Name -> FString
forall a b. (a -> b) -> a -> b
$ Name -> Name
lowercaseName (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ (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
    GetField Type a
_ Type b
_ a -> Field s b
_ -> Name -> Name -> CExpr
forall a. Name -> Name -> a
impossible Name
"transOp1" Name
"copilot-bluespec"

    -- BDPI-supported operations
    Sqrt    Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"sqrt"
    Exp     Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"exp"
    Log     Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"log"
    Acos    Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"acos"
    Asin    Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"asin"
    Atan    Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"atan"
    Cos     Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"cos"
    Sin     Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"sin"
    Tan     Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"tan"
    Acosh   Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"acosh"
    Asinh   Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"asinh"
    Atanh   Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"atanh"
    Cosh    Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"cosh"
    Sinh    Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"sinh"
    Tanh    Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"tanh"
    Ceiling Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"ceiling"
    Floor   Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"floor"
  where
    app :: BS.Id -> BS.CExpr
    app :: Id -> CExpr
app Id
i = CExpr -> [CExpr] -> CExpr
BS.CApply (Id -> CExpr
BS.CVar Id
i) [CExpr
e]

    appFP :: forall t. Type t -> String -> BS.CExpr
    appFP :: forall t. Type t -> Name -> CExpr
appFP Type t
ty Name
funPrefix = Id -> CExpr
app (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Type t -> Name -> Id
forall a. Type a -> Name -> Id
fpFunId Type t
ty Name
funPrefix

-- | Translates a Copilot binary operator and its arguments into a Bluespec
-- function.
transOp2 :: Op2 a b c -> BS.CExpr -> BS.CExpr -> BS.CExpr
transOp2 :: forall a b c. Op2 a b c -> CExpr -> CExpr -> CExpr
transOp2 Op2 a b c
op CExpr
e1 CExpr
e2 =
  case Op2 a b c
op of
    Op2 a b c
And          -> Id -> CExpr
app Id
BS.idAnd
    Op2 a b c
Or           -> Id -> CExpr
app (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Id
BS.idOrAt Position
BS.NoPos
    Add      Type a
_ty -> Id -> CExpr
app Id
BS.idPlus
    Sub      Type a
_ty -> Id -> CExpr
app Id
BS.idMinus
    Mul      Type a
_ty -> Id -> CExpr
app (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Id
BS.idStarAt Position
BS.NoPos
    Mod      Type a
_ty -> Id -> CExpr
app (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Id
BS.idPercentAt Position
BS.NoPos
    Div      Type a
_ty -> Id -> CExpr
app (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Id
BS.idSlashAt Position
BS.NoPos
    Fdiv     Type a
_ty -> Id -> CExpr
app (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Id
BS.idSlashAt Position
BS.NoPos
    Eq       Type a
_   -> Id -> CExpr
app Id
BS.idEqual
    Ne       Type a
_   -> Id -> CExpr
app Id
BS.idNotEqual
    Le       Type a
ty  -> Type a -> CExpr -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr -> CExpr
transLe Type a
ty CExpr
e1 CExpr
e2
    Ge       Type a
ty  -> Type a -> CExpr -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr -> CExpr
transGe Type a
ty CExpr
e1 CExpr
e2
    Lt       Type a
ty  -> Type a -> CExpr -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr -> CExpr
transLt Type a
ty CExpr
e1 CExpr
e2
    Gt       Type a
ty  -> Type a -> CExpr -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr -> CExpr
transGt Type a
ty CExpr
e1 CExpr
e2
    BwAnd    Type a
_   -> Id -> CExpr
app (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Id
BS.idBitAndAt Position
BS.NoPos
    BwOr     Type a
_   -> Id -> CExpr
app (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Id
BS.idBitOrAt Position
BS.NoPos
    BwXor    Type a
_   -> Id -> CExpr
app (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Id
BS.idCaretAt Position
BS.NoPos
    BwShiftL Type a
_ Type b
_ -> Id -> CExpr
app (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Id
BS.idLshAt Position
BS.NoPos
    BwShiftR Type a
_ Type b
_ -> Id -> CExpr
app (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Id
BS.idRshAt Position
BS.NoPos
    Index    Type (Array n c)
_   -> CExpr -> CExpr -> CExpr
cIndexVector CExpr
e1 CExpr
e2
    UpdateField (Struct a
_) Type b
_ a -> Field s b
f ->
      let field :: BS.FString
          field :: FString
field = Name -> FString
forall a. IsString a => Name -> a
fromString (Name -> FString) -> Name -> FString
forall a b. (a -> b) -> a -> b
$ Name -> Name
lowercaseName (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ (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 in
      CExpr -> [(Id, CExpr)] -> CExpr
BS.CStructUpd CExpr
e1 [(Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
field, CExpr
e2)]
    UpdateField Type a
_ Type b
_ a -> Field s b
_ -> Name -> Name -> CExpr
forall a. Name -> Name -> a
impossible Name
"transOp2" Name
"copilot-bluespec"

    -- BDPI-supported operations
    Pow      Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"pow"
    Logb     Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"logb"
    Atan2    Type a
ty -> Type a -> Name -> CExpr
forall t. Type t -> Name -> CExpr
appFP Type a
ty Name
"atan2"
  where
    app :: BS.Id -> BS.CExpr
    app :: Id -> CExpr
app Id
i = CExpr -> [CExpr] -> CExpr
BS.CApply (Id -> CExpr
BS.CVar Id
i) [CExpr
e1, CExpr
e2]

    appFP :: forall t. Type t -> String -> BS.CExpr
    appFP :: forall t. Type t -> Name -> CExpr
appFP Type t
ty Name
funPrefix = Id -> CExpr
app (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Type t -> Name -> Id
forall a. Type a -> Name -> Id
fpFunId Type t
ty Name
funPrefix

-- | Translates a Copilot ternary operator and its arguments into a Bluespec
-- function.
transOp3 :: Op3 a b c d -> BS.CExpr -> BS.CExpr -> BS.CExpr -> BS.CExpr
transOp3 :: forall a b c d. Op3 a b c d -> CExpr -> CExpr -> CExpr -> CExpr
transOp3 Op3 a b c d
op CExpr
e1 CExpr
e2 CExpr
e3 =
  case Op3 a b c d
op of
    Mux Type b
_ -> Position -> CExpr -> CExpr -> CExpr -> CExpr
BS.Cif Position
BS.NoPos CExpr
e1 CExpr
e2 CExpr
e3
    UpdateArray Type (Array n c)
_ -> CExpr -> CExpr -> CExpr -> CExpr
cUpdateVector CExpr
e1 CExpr
e2 CExpr
e3

-- | Translate @'Sign' e@ in Copilot Core into a Bluespec expression.
--
-- @signum e@ is translated as:
--
-- @
-- if e > 0 then 1 else (if e < 0 then negate 1 else 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 -> BS.CExpr -> BS.CExpr
transSign :: forall a. Type a -> CExpr -> CExpr
transSign Type a
ty CExpr
e = CExpr -> CExpr
positiveCase (CExpr -> CExpr) -> CExpr -> CExpr
forall a b. (a -> b) -> a -> b
$ CExpr -> CExpr
negativeCase CExpr
e
  where
    -- If @e@ is positive, return @1@, otherwise fall back to the argument.
    --
    -- Produces the following code, where @<arg>@ is the argument to this
    -- function:
    -- @
    -- if e > 0 then 1 else <arg>
    -- @
    positiveCase :: BS.CExpr  -- ^ Value returned if @e@ is not positive.
                 -> BS.CExpr
    positiveCase :: CExpr -> CExpr
positiveCase =
      Position -> CExpr -> CExpr -> CExpr -> CExpr
BS.Cif Position
BS.NoPos (Type a -> CExpr -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr -> CExpr
transGt Type a
ty CExpr
e (Type a -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constNumTy Type a
ty Integer
0)) (Type a -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constNumTy Type a
ty Integer
1)

    -- If @e@ is negative, return @1@, otherwise fall back to the argument.
    --
    -- Produces the following code, where @<arg>@ is the argument to this
    -- function:
    -- @
    -- if e < 0 then negate 1 else <arg>
    -- @
    negativeCase :: BS.CExpr  -- ^ Value returned if @e@ is not negative.
                 -> BS.CExpr
    negativeCase :: CExpr -> CExpr
negativeCase =
      Position -> CExpr -> CExpr -> CExpr -> CExpr
BS.Cif Position
BS.NoPos (Type a -> CExpr -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr -> CExpr
transLt Type a
ty CExpr
e (Type a -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constNumTy Type a
ty Integer
0)) (Type a -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constNumTy Type a
ty (-Integer
1))

-- | Translate a Copilot @x < y@ expression into Bluespec. We will generate
-- different code depending on whether the arguments have a floating-point type
-- or not.
transLt :: Type a
        -- ^ The type of the arguments.
        -> BS.CExpr -> BS.CExpr -> BS.CExpr
transLt :: forall a. Type a -> CExpr -> CExpr -> CExpr
transLt Type a
ty CExpr
e1 CExpr
e2
  | Type a -> Bool
forall a. Type a -> Bool
typeIsFloating Type a
ty
  = Id -> CExpr -> CExpr -> CExpr
transLtOrGtFP (Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"LT") CExpr
e1 CExpr
e2
  | Bool
otherwise
  = CExpr -> [CExpr] -> CExpr
BS.CApply (Id -> CExpr
BS.CVar (Position -> Id
BS.idLtAt Position
BS.NoPos)) [CExpr
e1, CExpr
e2]

-- | Translate a Copilot @x > y@ expression into Bluespec. We will generate
-- different code depending on whether the arguments have a floating-point type
-- or not.
transGt :: Type a
        -- ^ The type of the arguments.
        -> BS.CExpr -> BS.CExpr -> BS.CExpr
transGt :: forall a. Type a -> CExpr -> CExpr -> CExpr
transGt Type a
ty CExpr
e1 CExpr
e2
  | Type a -> Bool
forall a. Type a -> Bool
typeIsFloating Type a
ty
  = Id -> CExpr -> CExpr -> CExpr
transLtOrGtFP (Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"GT") CExpr
e1 CExpr
e2
  | Bool
otherwise
  = CExpr -> [CExpr] -> CExpr
BS.CApply (Id -> CExpr
BS.CVar (Position -> Id
BS.idGtAt Position
BS.NoPos)) [CExpr
e1, CExpr
e2]

-- | Translate a Copilot @x <= y@ expression into Bluespec. We will generate
-- different code depending on whether the arguments have a floating-point type
-- or not.
transLe :: Type a
        -- ^ The type of the arguments.
        -> BS.CExpr -> BS.CExpr -> BS.CExpr
transLe :: forall a. Type a -> CExpr -> CExpr -> CExpr
transLe Type a
ty CExpr
e1 CExpr
e2
  | Type a -> Bool
forall a. Type a -> Bool
typeIsFloating Type a
ty
  = Id -> CExpr -> CExpr -> CExpr
transLeOrGeFP (Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"LT") CExpr
e1 CExpr
e2
  | Bool
otherwise
  = CExpr -> [CExpr] -> CExpr
BS.CApply (Id -> CExpr
BS.CVar (Position -> Id
BS.idLtEqAt Position
BS.NoPos)) [CExpr
e1, CExpr
e2]

-- | Translate a Copilot @x >= y@ expression into Bluespec. We will generate
-- different code depending on whether the arguments have a floating-point type
-- or not.
transGe :: Type a
        -- ^ The type of the arguments.
        -> BS.CExpr -> BS.CExpr -> BS.CExpr
transGe :: forall a. Type a -> CExpr -> CExpr -> CExpr
transGe Type a
ty CExpr
e1 CExpr
e2
  | Type a -> Bool
forall a. Type a -> Bool
typeIsFloating Type a
ty
  = Id -> CExpr -> CExpr -> CExpr
transLeOrGeFP (Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"GT") CExpr
e1 CExpr
e2
  | Bool
otherwise
  = CExpr -> [CExpr] -> CExpr
BS.CApply (Id -> CExpr
BS.CVar (Position -> Id
BS.idGtEqAt Position
BS.NoPos)) [CExpr
e1, CExpr
e2]

-- | Translate a Copilot floating-point comparison involving @<@ or @>@ into a
-- Bluespec expression. Specifically, @x < y@ is translated to:
--
-- @
-- compareFP x y == LT
-- @
--
-- @x > y@ is translated similarly, except that @GT@ is used instead of @LT@.
--
-- See the comments on 'compareFPExpr' for why we translate floating-point
-- comparison operators this way.
transLtOrGtFP :: BS.Id
                 -- ^ A @Disorder@ label, which we check against the result of
                 -- calling @compareFP@. This should be either @LT@ or @GT@.
              -> BS.CExpr -> BS.CExpr -> BS.CExpr
transLtOrGtFP :: Id -> CExpr -> CExpr -> CExpr
transLtOrGtFP Id
disorderLabel CExpr
e1 CExpr
e2 =
  CExpr -> [CExpr] -> CExpr
BS.CApply
    (Id -> CExpr
BS.CVar Id
BS.idEqual)
    [CExpr -> CExpr -> CExpr
compareFPExpr CExpr
e1 CExpr
e2, Id -> [CExpr] -> CExpr
BS.CCon Id
disorderLabel []]

-- | Translate a Copilot floating-point comparison involving @<=@ or @>=@ into
-- a Bluespec expression. Specifically, @x <= y@ is translated to:
--
-- @
-- let _c = compareFP x y
-- in (_c == LT) || (_c == EQ)
-- @
--
-- @x >= y@ is translated similarly, except that @GT@ is used instead of @LT@.
--
-- See the comments on 'compareFPExpr' for why we translate floating-point
-- comparison operators this way.
transLeOrGeFP :: BS.Id
                 -- ^ A @Disorder@ label, which we check against the result of
                 -- calling @compareFP@. This should be either @LT@ or @GT@.
              -> BS.CExpr -> BS.CExpr -> BS.CExpr
transLeOrGeFP :: Id -> CExpr -> CExpr -> CExpr
transLeOrGeFP Id
disorderLabel CExpr
e1 CExpr
e2 =
  [CDefl] -> CExpr -> CExpr
BS.Cletrec
    [Id -> [CClause] -> [CQual] -> CDefl
BS.CLValue Id
c [[CPat] -> [CQual] -> CExpr -> CClause
BS.CClause [] [] (CExpr -> CExpr -> CExpr
compareFPExpr CExpr
e1 CExpr
e2)] []]
    (CExpr -> [CExpr] -> CExpr
BS.CApply
      (Id -> CExpr
BS.CVar (Position -> Id
BS.idOrAt Position
BS.NoPos))
      [ CExpr -> [CExpr] -> CExpr
BS.CApply
          (Id -> CExpr
BS.CVar Id
BS.idEqual)
          [Id -> CExpr
BS.CVar Id
c, Id -> [CExpr] -> CExpr
BS.CCon Id
disorderLabel []]
      , CExpr -> [CExpr] -> CExpr
BS.CApply
          (Id -> CExpr
BS.CVar Id
BS.idEqual)
          [Id -> CExpr
BS.CVar Id
c, Id -> [CExpr] -> CExpr
BS.CCon (Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"EQ") []]
      ])
  where
    c :: Id
c = Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"_c"

-- | Generate an expression of the form @compareFP x y@. This is used to power
-- the translations of the Copilot @<@, @<=@, @>@, and @>=@ floating-point
-- operators to Bluespec.
--
-- Translating these operators using @compareFP@ is a somewhat curious design
-- choice, given that Bluespec already defines its own versions of these
-- operators. Unfortunately, we cannot directly use the Bluespec versions of
-- these operators, as they are defined in such a way that they will call
-- @error@ when one of the arguments is a NaN value. This would pose two
-- problems:
--
-- 1. This would differ from the semantics of Copilot, where @x < y@ will return
--    @False@ (instead of erroring) when one of the arguments is NaN. (Similarly
--    for the other floating-point comparison operators.)
--
-- 2. Moreover, if you have a Bluespec program that calls @x < y@, where the
--    value of @x@ or @y@ is derived from a register, then @bsc@ will always
--    fail to compile the code. This is because Bluespec must generate hardware
--    for all possible code paths in @<@, and because one of the code paths
--    calls @error@, this will cause compilation to result in an error. (See
--    https://github.com/B-Lang-org/bsc/discussions/711#discussioncomment-10003586
--    for a more detailed explanation.)
--
-- As such, we avoid using Bluespec's comparison operators and instead translate
-- Copilot's comparison operators to expressions derived from @compareFP@.
-- Unlike Bluespec's other comparison operators, calling @compareFP@ will never
-- result in an error.
compareFPExpr :: BS.CExpr -> BS.CExpr -> BS.CExpr
compareFPExpr :: CExpr -> CExpr -> CExpr
compareFPExpr CExpr
e1 CExpr
e2 =
  CExpr -> [CExpr] -> CExpr
BS.CApply
    (Id -> CExpr
BS.CVar (Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"compareFP"))
    [CExpr
e1, CExpr
e2]

-- | Bluespec does not have a general-purpose casting operation, so we must
-- handle casts on a case-by-case basis.
transCast :: Type a -> Type b -> BS.CExpr -> BS.CExpr
transCast :: forall a b. Type a -> Type b -> CExpr -> CExpr
transCast Type a
fromTy Type b
toTy =
  case (Type a
fromTy, Type b
toTy) of
    -----
    -- "safe" casts that cannot lose information
    -----

    (Type a
Bool,  Type b
Bool)    -> CExpr -> CExpr
forall a. a -> a
id
    (Type a
Bool,  Type b
Word8)   -> CExpr -> CExpr
upcastBool
    (Type a
Bool,  Type b
Word16)  -> CExpr -> CExpr
upcastBool
    (Type a
Bool,  Type b
Word32)  -> CExpr -> CExpr
upcastBool
    (Type a
Bool,  Type b
Word64)  -> CExpr -> CExpr
upcastBool
    (Type a
Bool,  Type b
Int8)    -> CExpr -> CExpr
upcastBool
    (Type a
Bool,  Type b
Int16)   -> CExpr -> CExpr
upcastBool
    (Type a
Bool,  Type b
Int32)   -> CExpr -> CExpr
upcastBool
    (Type a
Bool,  Type b
Int64)   -> CExpr -> CExpr
upcastBool

    (Type a
Int8,  Type b
Int8)    -> CExpr -> CExpr
forall a. a -> a
id
    (Type a
Int8,  Type b
Int16)   -> CExpr -> CExpr
upcast
    (Type a
Int8,  Type b
Int32)   -> CExpr -> CExpr
upcast
    (Type a
Int8,  Type b
Int64)   -> CExpr -> CExpr
upcast
    (Type a
Int16, Type b
Int16)   -> CExpr -> CExpr
forall a. a -> a
id
    (Type a
Int16, Type b
Int32)   -> CExpr -> CExpr
upcast
    (Type a
Int16, Type b
Int64)   -> CExpr -> CExpr
upcast
    (Type a
Int32, Type b
Int32)   -> CExpr -> CExpr
forall a. a -> a
id
    (Type a
Int32, Type b
Int64)   -> CExpr -> CExpr
upcast
    (Type a
Int64, Type b
Int64)   -> CExpr -> CExpr
forall a. a -> a
id

    (Type a
Word8,  Type b
Int16)  -> Type Word16 -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
unpackPackUpcast Type Word16
Word16
    (Type a
Word8,  Type b
Int32)  -> Type DropIdx -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
unpackPackUpcast Type DropIdx
Word32
    (Type a
Word8,  Type b
Int64)  -> Type Word64 -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
unpackPackUpcast Type Word64
Word64
    (Type a
Word8,  Type b
Word8)  -> CExpr -> CExpr
forall a. a -> a
id
    (Type a
Word8,  Type b
Word16) -> CExpr -> CExpr
upcast
    (Type a
Word8,  Type b
Word32) -> CExpr -> CExpr
upcast
    (Type a
Word8,  Type b
Word64) -> CExpr -> CExpr
upcast
    (Type a
Word16, Type b
Int32)  -> Type DropIdx -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
unpackPackUpcast Type DropIdx
Word32
    (Type a
Word16, Type b
Int64)  -> Type Word64 -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
unpackPackUpcast Type Word64
Word64
    (Type a
Word16, Type b
Word16) -> CExpr -> CExpr
forall a. a -> a
id
    (Type a
Word16, Type b
Word32) -> CExpr -> CExpr
upcast
    (Type a
Word16, Type b
Word64) -> CExpr -> CExpr
upcast
    (Type a
Word32, Type b
Int64)  -> Type Word64 -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
unpackPackUpcast Type Word64
Word64
    (Type a
Word32, Type b
Word32) -> CExpr -> CExpr
forall a. a -> a
id
    (Type a
Word32, Type b
Word64) -> CExpr -> CExpr
upcast
    (Type a
Word64, Type b
Word64) -> CExpr -> CExpr
forall a. a -> a
id

    -----
    -- "unsafe" casts, which may lose information
    -----

    -- unsigned truncations
    (Type a
Word64, Type b
Word32) -> CExpr -> CExpr
downcast
    (Type a
Word64, Type b
Word16) -> CExpr -> CExpr
downcast
    (Type a
Word64, Type b
Word8)  -> CExpr -> CExpr
downcast
    (Type a
Word32, Type b
Word16) -> CExpr -> CExpr
downcast
    (Type a
Word32, Type b
Word8)  -> CExpr -> CExpr
downcast
    (Type a
Word16, Type b
Word8)  -> CExpr -> CExpr
downcast

    -- signed truncations
    (Type a
Int64, Type b
Int32)   -> CExpr -> CExpr
downcast
    (Type a
Int64, Type b
Int16)   -> CExpr -> CExpr
downcast
    (Type a
Int64, Type b
Int8)    -> CExpr -> CExpr
downcast
    (Type a
Int32, Type b
Int16)   -> CExpr -> CExpr
downcast
    (Type a
Int32, Type b
Int8)    -> CExpr -> CExpr
downcast
    (Type a
Int16, Type b
Int8)    -> CExpr -> CExpr
downcast

    -- signed integer to float
    (Type a
Int64, Type b
Float)   -> CExpr -> CExpr
castIntegralToFloatingPoint
    (Type a
Int32, Type b
Float)   -> CExpr -> CExpr
castIntegralToFloatingPoint
    (Type a
Int16, Type b
Float)   -> CExpr -> CExpr
castIntegralToFloatingPoint
    (Type a
Int8,  Type b
Float)   -> CExpr -> CExpr
castIntegralToFloatingPoint

    -- unsigned integer to float
    (Type a
Word64, Type b
Float)  -> CExpr -> CExpr
castIntegralToFloatingPoint
    (Type a
Word32, Type b
Float)  -> CExpr -> CExpr
castIntegralToFloatingPoint
    (Type a
Word16, Type b
Float)  -> CExpr -> CExpr
castIntegralToFloatingPoint
    (Type a
Word8,  Type b
Float)  -> CExpr -> CExpr
castIntegralToFloatingPoint

    -- signed integer to double
    (Type a
Int64, Type b
Double)  -> CExpr -> CExpr
castIntegralToFloatingPoint
    (Type a
Int32, Type b
Double)  -> CExpr -> CExpr
castIntegralToFloatingPoint
    (Type a
Int16, Type b
Double)  -> CExpr -> CExpr
castIntegralToFloatingPoint
    (Type a
Int8,  Type b
Double)  -> CExpr -> CExpr
castIntegralToFloatingPoint

    -- unsigned integer to double
    (Type a
Word64, Type b
Double) -> CExpr -> CExpr
castIntegralToFloatingPoint
    (Type a
Word32, Type b
Double) -> CExpr -> CExpr
castIntegralToFloatingPoint
    (Type a
Word16, Type b
Double) -> CExpr -> CExpr
castIntegralToFloatingPoint
    (Type a
Word8,  Type b
Double) -> CExpr -> CExpr
castIntegralToFloatingPoint

    -- unsigned to signed conversion
    (Type a
Word64, Type b
Int64)  -> CExpr -> CExpr
unpackPack
    (Type a
Word32, Type b
Int32)  -> CExpr -> CExpr
unpackPack
    (Type a
Word16, Type b
Int16)  -> CExpr -> CExpr
unpackPack
    (Type a
Word8,  Type b
Int8)   -> CExpr -> CExpr
unpackPack

    -- signed to unsigned conversion
    (Type a
Int64, Type b
Word64)  -> CExpr -> CExpr
unpackPack
    (Type a
Int32, Type b
Word32)  -> CExpr -> CExpr
unpackPack
    (Type a
Int16, Type b
Word16)  -> CExpr -> CExpr
unpackPack
    (Type a
Int8,  Type b
Word8)   -> CExpr -> CExpr
unpackPack

    (Type a, Type b)
_ -> Name -> Name -> CExpr -> CExpr
forall a. Name -> Name -> a
impossible Name
"transCast" Name
"copilot-bluespec"
  where
    -- unpackPack :: (Bits fromTy n, Bits toTy n) => fromTy -> toTy
    -- unpackPack e = (unpack (pack e)) :: toTy
    --
    -- The most basic cast. Used when fromTy and toTy are both integral types
    -- with the same number of bits.
    unpackPack :: BS.CExpr -> BS.CExpr
    unpackPack :: CExpr -> CExpr
unpackPack CExpr
e = Type b -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
withTypeAnnotation Type b
toTy (CExpr -> CExpr) -> CExpr -> CExpr
forall a b. (a -> b) -> a -> b
$
                   CExpr -> [CExpr] -> CExpr
BS.CApply
                     (Id -> CExpr
BS.CVar Id
BS.idUnpack)
                     [CExpr -> [CExpr] -> CExpr
BS.CApply (Id -> CExpr
BS.CVar Id
BS.idPack) [CExpr
e]]

    -- upcastBool :: (Add k 1 n, Bits toTy n) => Bool -> toTy
    -- upcastBool b = (unpack (extend (pack b))) :: toTy
    --
    -- Cast a Bool to a `Bits 1` value, extend it to `Bits n`, and then
    -- convert it back to an integral type.
    upcastBool :: BS.CExpr -> BS.CExpr
    upcastBool :: CExpr -> CExpr
upcastBool CExpr
e = Type b -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
withTypeAnnotation Type b
toTy (CExpr -> CExpr) -> CExpr -> CExpr
forall a b. (a -> b) -> a -> b
$
                   CExpr -> [CExpr] -> CExpr
BS.CApply
                     (Id -> CExpr
BS.CVar Id
BS.idUnpack)
                     [CExpr -> [CExpr] -> CExpr
BS.CApply CExpr
extendExpr [CExpr -> [CExpr] -> CExpr
BS.CApply (Id -> CExpr
BS.CVar Id
BS.idPack) [CExpr
e]]]

    -- upcast :: (BitExtend m n x) => x m -> x n
    -- upcast e = (extend e) :: ty
    --
    -- Convert a narrower integral type to a wider integral type (e.g.,
    -- `UInt 8` to `UInt 64` or `Int 8` to `Int 64`). Note that the `extend`
    -- operation is smart enough to choose between sign-extension and
    -- zero-extension depending on whether `x m` (i.e., fromTy) is a signed
    -- or unsigned type, respectively.
    upcast :: BS.CExpr -> BS.CExpr
    upcast :: CExpr -> CExpr
upcast CExpr
e = Type b -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
withTypeAnnotation Type b
toTy (CExpr -> CExpr) -> CExpr -> CExpr
forall a b. (a -> b) -> a -> b
$ CExpr -> [CExpr] -> CExpr
BS.CApply CExpr
extendExpr [CExpr
e]

    -- downcast :: (BitExtend m n x) => x n -> x m
    -- downcast e = (truncate e) :: ty
    --
    -- Convert a wider integral type to a narrow integral type (e.g.,
    -- `UInt 64` to `UInt 8` or `Int 64` to `Int 8`) by truncating the most
    -- significant bits.
    downcast :: BS.CExpr -> BS.CExpr
    downcast :: CExpr -> CExpr
downcast CExpr
e = Type b -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
withTypeAnnotation Type b
toTy (CExpr -> CExpr) -> CExpr -> CExpr
forall a b. (a -> b) -> a -> b
$ CExpr -> [CExpr] -> CExpr
BS.CApply CExpr
truncateExpr [CExpr
e]

    -- Apply upcast followed by unpackPack. This requires supplying the type to
    -- upcast to for type disambiguation purposes.
    unpackPackUpcast :: Type a -> BS.CExpr -> BS.CExpr
    unpackPackUpcast :: forall a. Type a -> CExpr -> CExpr
unpackPackUpcast Type a
upcastTy CExpr
e = CExpr -> CExpr
unpackPack (CExpr -> CExpr) -> CExpr -> CExpr
forall a b. (a -> b) -> a -> b
$
      Type a -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
withTypeAnnotation Type a
upcastTy (CExpr -> CExpr) -> CExpr -> CExpr
forall a b. (a -> b) -> a -> b
$ CExpr -> [CExpr] -> CExpr
BS.CApply CExpr
extendExpr [CExpr
e]

    -- castIntegralToFloatingPoint :: (FixedFloatCVT fromTy toTy) => fromTy toTy
    -- castIntegralToFloatingPoint e =
    --   ((vFixedToFloat e (0 :: UInt 64) Rnd_Nearest_Even).fst) :: tfl
    --
    -- While FloatingPoint does have a Bits instance, we don't want to convert
    -- an integral type to a FloatingPoint type using the Bits class, as the
    -- bit representation of an integral value differs quite a bit from the bit
    -- representation of a FloatingPoint value. Instead, we use the
    -- special-purpose FixedFloatCVT class for this task.
    castIntegralToFloatingPoint :: BS.CExpr -> BS.CExpr
    castIntegralToFloatingPoint :: CExpr -> CExpr
castIntegralToFloatingPoint CExpr
e =
      Type b -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
withTypeAnnotation Type b
toTy (CExpr -> CExpr) -> CExpr -> CExpr
forall a b. (a -> b) -> a -> b
$
      CExpr -> Id -> CExpr
BS.CSelect
        (CExpr -> [CExpr] -> CExpr
BS.CApply
          (Id -> CExpr
BS.CVar (Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"vFixedToFloat"))
          [ CExpr
e
          , Type Word64 -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constNumTy Type Word64
Word64 Integer
0
          , CExpr
fpRM
          ])
        Id
BS.idPrimFst

    extendExpr :: CExpr
extendExpr   = Id -> CExpr
BS.CVar (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"extend"
    truncateExpr :: CExpr
truncateExpr = Id -> CExpr
BS.CVar (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"truncate"

-- | Transform a Copilot Core literal, based on its value and type, into a
-- Bluespec expression.
constTy :: Type a -> a -> BS.CExpr
constTy :: forall a. Type a -> a -> CExpr
constTy Type a
ty =
  case Type a
ty of
    -- The treatment of scalar types is relatively straightforward. Note that
    -- Bool is an enum, so we must construct it using a CCon rather than with
    -- a CLit.
    Type a
Bool      -> \a
v -> Id -> [CExpr] -> CExpr
BS.CCon (if a
Bool
v then Id
BS.idTrue else Id
BS.idFalse) []
    Type a
Int8      -> Type a -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constInt Type a
ty (Integer -> CExpr) -> (a -> Integer) -> a -> CExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall a. Integral a => a -> Integer
toInteger
    Type a
Int16     -> Type a -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constInt Type a
ty (Integer -> CExpr) -> (a -> Integer) -> a -> CExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall a. Integral a => a -> Integer
toInteger
    Type a
Int32     -> Type a -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constInt Type a
ty (Integer -> CExpr) -> (a -> Integer) -> a -> CExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall a. Integral a => a -> Integer
toInteger
    Type a
Int64     -> Type a -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constInt Type a
ty (Integer -> CExpr) -> (a -> Integer) -> a -> CExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall a. Integral a => a -> Integer
toInteger
    Type a
Word8     -> Type a -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constInt Type a
ty (Integer -> CExpr) -> (a -> Integer) -> a -> CExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall a. Integral a => a -> Integer
toInteger
    Type a
Word16    -> Type a -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constInt Type a
ty (Integer -> CExpr) -> (a -> Integer) -> a -> CExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall a. Integral a => a -> Integer
toInteger
    Type a
Word32    -> Type a -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constInt Type a
ty (Integer -> CExpr) -> (a -> Integer) -> a -> CExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall a. Integral a => a -> Integer
toInteger
    Type a
Word64    -> Type a -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constInt Type a
ty (Integer -> CExpr) -> (a -> Integer) -> a -> CExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall a. Integral a => a -> Integer
toInteger
    Type a
Float     -> Type a -> Double -> CExpr
forall ty. Type ty -> Double -> CExpr
constFP Type a
ty (Double -> CExpr) -> (a -> Double) -> a -> CExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Double
Float -> Double
nanSafeFloat2Double
    Type a
Double    -> Type a -> Double -> CExpr
forall ty. Type ty -> Double -> CExpr
constFP Type a
ty

    -- Translating a Copilot array literal to a Bluespec Vector is somewhat
    -- involved. Given a Copilot array {x_0, ..., x_(n-1)}, the
    -- corresponding Bluespec Vector will look something like:
    --
    --   let arr = update (... (update newVector 0 x_0)) (n-1) x_(n-1)
    --
    -- We use the `update` function instead of the := syntax (e.g.,
    -- { array_temp[0] := x; array_temp[1] := y; ...}) so that we can construct
    -- a Vector in a pure context.
    Array Type t
ty' -> Type t -> [t] -> CExpr
forall a. Type a -> [a] -> CExpr
constVector Type t
ty' ([t] -> CExpr) -> (a -> [t]) -> a -> CExpr
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

    -- Converting a Copilot struct { field_0 = x_0, ..., field_(n-1) = x_(n-1) }
    -- to a Bluespec struct is quite straightforward, given Bluespec's struct
    -- initialization syntax.
    Struct a
s -> \a
v ->
      Maybe Bool -> Id -> [(Id, CExpr)] -> CExpr
BS.CStruct
        (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True)
        (Position -> FString -> Id
BS.mkId Position
BS.NoPos (FString -> Id) -> FString -> Id
forall a b. (a -> b) -> a -> b
$ Name -> FString
forall a. IsString a => Name -> a
fromString (Name -> FString) -> Name -> FString
forall a b. (a -> b) -> a -> b
$ Name -> Name
uppercaseName (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ a -> Name
forall a. Struct a => a -> Name
typeName a
s)
        ((Value a -> (Id, CExpr)) -> [Value a] -> [(Id, CExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Value Type t
ty'' field :: Field s t
field@(Field t
val)) ->
               ( Position -> FString -> Id
BS.mkId Position
BS.NoPos (FString -> Id) -> FString -> Id
forall a b. (a -> b) -> a -> b
$ Name -> FString
forall a. IsString a => Name -> a
fromString
                                  (Name -> FString) -> Name -> FString
forall a b. (a -> b) -> a -> b
$ Name -> Name
lowercaseName
                                  (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ Field s t -> Name
forall (s :: Symbol) t. KnownSymbol s => Field s t -> Name
fieldName Field s t
field
               , Type t -> t -> CExpr
forall a. Type a -> a -> CExpr
constTy Type t
ty'' t
val
               ))
             (a -> [Value a]
forall a. Struct a => a -> [Value a]
toValues a
v))
  where
    -- Convert a Float to a Double. This function takes care to preserve
    -- special floating-point values, such as negative zero, infinity, and NaN
    -- values.
    nanSafeFloat2Double :: Float -> Double
    nanSafeFloat2Double :: Float -> Double
nanSafeFloat2Double Float
x
        -- float2Double does not preserve the payloads of NaN values, so we
        -- include special cases for translating NaNs.
        | Float -> Bool
forall a. RealFloat a => a -> Bool
isNaN Float
x Bool -> Bool -> Bool
&& Float -> Bool
forall a. RealFloatNaN a => a -> Bool
isSignaling Float
x = Double -> Double
forall a. RealFloatNaN a => a -> a
setPayloadSignaling Double
payload
        | Float -> Bool
forall a. RealFloat a => a -> Bool
isNaN Float
x                  = Double -> Double
forall a. RealFloatNaN a => a -> a
setPayload Double
payload
        | Bool
otherwise                = Float -> Double
float2Double Float
x
      where
        payload :: Double
        payload :: Double
payload = Float -> Double
float2Double (Float -> Double) -> Float -> Double
forall a b. (a -> b) -> a -> b
$ Float -> Float
forall a. RealFloatNaN a => a -> a
getPayload Float
x

-- | Transform a list of Copilot Core expressions of a given 'Type' into a
-- Bluespec @Vector@ expression.
constVector :: Type a -> [a] -> BS.CExpr
constVector :: forall a. Type a -> [a] -> CExpr
constVector Type a
ty = (Id -> a -> CExpr) -> [a] -> CExpr
forall a. (Id -> a -> CExpr) -> [a] -> CExpr
genVector (\Id
_ -> Type a -> a -> CExpr
forall a. Type a -> a -> CExpr
constTy Type a
ty)

-- | Transform a list of Copilot Core expressions into a Bluespec @Vector@
-- expression. When invoking @genVector f es@, where @es@ has length @n@, the
-- resulting @Vector@ will consist of
-- @[f 0 (es !! 0), f 1 (es !! 1), ..., f (n-1) (es !! (n-1))]@.
genVector :: (Int -> a -> BS.CExpr) -> [a] -> BS.CExpr
genVector :: forall a. (Id -> a -> CExpr) -> [a] -> CExpr
genVector Id -> a -> CExpr
f [a]
vec =
  (Id, CExpr) -> CExpr
forall a b. (a, b) -> b
snd ((Id, CExpr) -> CExpr) -> (Id, CExpr) -> CExpr
forall a b. (a -> b) -> a -> b
$
  ((Id, CExpr) -> a -> (Id, CExpr))
-> (Id, CExpr) -> [a] -> (Id, CExpr)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
    (\(!Id
i, !CExpr
v) a
x ->
      ( Id
iId -> Id -> Id
forall a. Num a => a -> a -> a
+Id
1
      , CExpr -> CExpr -> CExpr -> CExpr
cUpdateVector
          CExpr
v
          (Literal -> CExpr
cLit (IntLit -> Literal
BS.LInt (Integer -> IntLit
BS.ilDec (Id -> Integer
forall a. Integral a => a -> Integer
toInteger Id
i))))
          (Id -> a -> CExpr
f Id
i a
x)
      ))
    (Id
0, Id -> CExpr
BS.CVar (Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"newVector"))
    [a]
vec

-- | Translate a literal number of type @ty@ into a Bluespec expression.
--
-- PRE: The type of PRE is numeric (integer or floating-point), that
-- is, not boolean, struct or array.
constNumTy :: Type a -> Integer -> BS.CExpr
constNumTy :: forall a. Type a -> Integer -> CExpr
constNumTy Type a
ty =
  case Type a
ty of
    Type a
Float  -> Type a -> Double -> CExpr
forall ty. Type ty -> Double -> CExpr
constFP Type a
ty (Double -> CExpr) -> (Integer -> Double) -> Integer -> CExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Double
forall a. Num a => Integer -> a
fromInteger
    Type a
Double -> Type a -> Double -> CExpr
forall ty. Type ty -> Double -> CExpr
constFP Type a
ty (Double -> CExpr) -> (Integer -> Double) -> Integer -> CExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Double
forall a. Num a => Integer -> a
fromInteger
    Type a
_      -> Type a -> Integer -> CExpr
forall a. Type a -> Integer -> CExpr
constInt Type a
ty

-- | Translate a Copilot integer literal into a Bluespec expression.
constInt :: Type a -> Integer -> BS.CExpr
constInt :: forall a. Type a -> Integer -> CExpr
constInt Type a
ty Integer
i
    -- Bluespec intentionally does not support negative literal syntax (e.g.,
    -- -42), so we must create negative integer literals using the `negate`
    -- function.
    | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0    = Type a -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
withTypeAnnotation Type a
ty (CExpr -> CExpr) -> CExpr -> CExpr
forall a b. (a -> b) -> a -> b
$ Literal -> CExpr
cLit (Literal -> CExpr) -> Literal -> CExpr
forall a b. (a -> b) -> a -> b
$ IntLit -> Literal
BS.LInt (IntLit -> Literal) -> IntLit -> Literal
forall a b. (a -> b) -> a -> b
$ Integer -> IntLit
BS.ilDec Integer
i
    | Bool
otherwise = Type a -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
withTypeAnnotation Type a
ty (CExpr -> CExpr) -> CExpr -> CExpr
forall a b. (a -> b) -> a -> b
$
                  CExpr -> [CExpr] -> CExpr
BS.CApply
                    (Id -> CExpr
BS.CVar (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Id
BS.idNegateAt Position
BS.NoPos)
                    [Literal -> CExpr
cLit (Literal -> CExpr) -> Literal -> CExpr
forall a b. (a -> b) -> a -> b
$ IntLit -> Literal
BS.LInt (IntLit -> Literal) -> IntLit -> Literal
forall a b. (a -> b) -> a -> b
$ Integer -> IntLit
BS.ilDec (Integer -> IntLit) -> Integer -> IntLit
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
negate Integer
i]

-- | Translate a Copilot floating-point literal into a Bluespec expression.
constFP :: Type ty -> Double -> BS.CExpr
constFP :: forall ty. Type ty -> Double -> CExpr
constFP Type ty
ty Double
d
    -- Bluespec internally represents all IEEE floating-point values as structs 
    -- so special symbols have to be called for constructing special values,
    -- e.g. NaN, inf, and -0.0. See
    -- https://github.com/B-Lang-org/bsc/blob/main/src/Libraries/Base3-Math/FloatingPoint.bsv#L441
    | Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
d = CExpr -> [CExpr] -> CExpr
BS.CApply 
                       (Id -> CExpr
BS.CVar (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"infinity") 
                       [ if Double
d Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
0
                           then Id -> [CExpr] -> CExpr
BS.CCon Id
BS.idTrue [] 
                           else Id -> [CExpr] -> CExpr
BS.CCon Id
BS.idFalse []
                       ]
                      
    | Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
d      = let 
                       cexpr :: CExpr
cexpr = CExpr -> CQType -> CExpr
BS.CHasType 
                                 ( CLiteral -> CExpr
BS.CLit (CLiteral -> CExpr) -> CLiteral -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Literal -> CLiteral
BS.CLiteral Position
BS.NoPos (Literal -> CLiteral) -> Literal -> CLiteral
forall a b. (a -> b) -> a -> b
$ IntLit -> Literal
BS.LInt (IntLit -> Literal) -> IntLit -> Literal
forall a b. (a -> b) -> a -> b
$
                                     Maybe Integer -> Integer -> Integer -> IntLit
BS.IntLit Maybe Integer
forall a. Maybe a
Nothing Integer
10 Integer
cval
                                 )
                                 ( [CPred] -> CType -> CQType
BS.CQType [] (CType -> CQType) -> CType -> CQType
forall a b. (a -> b) -> a -> b
$ TyCon -> CType
BS.TCon (TyCon -> CType) -> TyCon -> CType
forall a b. (a -> b) -> a -> b
$ 
                                     Id -> Maybe Kind -> TISort -> TyCon
BS.TyCon 
                                       (Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
ctype) 
                                       Maybe Kind
forall a. Maybe a
Nothing 
                                       TISort
BS.TIabstract
                                 )
                       cval :: Integer
cval = case Type ty
ty of 
                         Type ty
Float  -> DropIdx -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (DropIdx -> Integer) -> DropIdx -> Integer
forall a b. (a -> b) -> a -> b
$ 
                                     Float -> DropIdx
castFloatToWord32 (Float -> DropIdx) -> Float -> DropIdx
forall a b. (a -> b) -> a -> b
$ Double -> Float
uncastDoubleNaNToFloat Double
d
                         Type ty
Double -> Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Integer) -> Word64 -> Integer
forall a b. (a -> b) -> a -> b
$ 
                                     Double -> Word64
castDoubleToWord64 Double
d
                         Type ty
_      -> Name -> Name -> Integer
forall a. Name -> Name -> a
impossible Name
"constFP" Name
"copilot-bluespec"
                       ctype :: FString
ctype = case Type ty
ty of 
                         Type ty
Float  -> FString
"Bit 32"
                         Type ty
Double -> FString
"Bit 64"
                         Type ty
_      -> Name -> Name -> FString
forall a. Name -> Name -> a
impossible Name
"constFP" Name
"copilot-bluespec"
                     in CExpr -> [CExpr] -> CExpr
BS.CApply (Id -> CExpr
BS.CVar (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"unpack") [CExpr
cexpr]
    | Double
d Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
0       = CExpr -> [CExpr] -> CExpr
BS.CApply 
                       (Id -> CExpr
BS.CVar (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"zero") 
                       [ if Double -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero Double
d 
                           then Id -> [CExpr] -> CExpr
BS.CCon Id
BS.idTrue [] 
                           else Id -> [CExpr] -> CExpr
BS.CCon Id
BS.idFalse []
                       ]
    | Double
d Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double
0        = Type ty -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
withTypeAnnotation Type ty
ty (CExpr -> CExpr) -> CExpr -> CExpr
forall a b. (a -> b) -> a -> b
$ Literal -> CExpr
cLit (Literal -> CExpr) -> Literal -> CExpr
forall a b. (a -> b) -> a -> b
$ Double -> Literal
BS.LReal Double
d
    -- Bluespec intentionally does not support negative literal syntax (e.g.,
    -- -42.5), so we must create negative floating-point literals using the
    -- `negate` function.
    | Bool
otherwise    = Type ty -> CExpr -> CExpr
forall a. Type a -> CExpr -> CExpr
withTypeAnnotation Type ty
ty (CExpr -> CExpr) -> CExpr -> CExpr
forall a b. (a -> b) -> a -> b
$
                     CExpr -> [CExpr] -> CExpr
BS.CApply
                       (Id -> CExpr
BS.CVar (Id -> CExpr) -> Id -> CExpr
forall a b. (a -> b) -> a -> b
$ Position -> Id
BS.idNegateAt Position
BS.NoPos)
                       [Literal -> CExpr
cLit (Literal -> CExpr) -> Literal -> CExpr
forall a b. (a -> b) -> a -> b
$ Double -> Literal
BS.LReal (Double -> Literal) -> Double -> Literal
forall a b. (a -> b) -> a -> b
$ Double -> Double
forall a. Num a => a -> a
negate Double
d]

-- Because NaNs are specially placed as bit-representations by `constfp` and `constfp` requires Doubles as inputs,
--  we need to convert NaN doubles safely into NaN floats. GHC Double2Float does not preserve signal nor payload 
--  internals of NaNs so in this case we need a special conversion.
uncastDoubleNaNToFloat :: Double -> Float
uncastDoubleNaNToFloat :: Double -> Float
uncastDoubleNaNToFloat Double
nan = if (Double -> Bool
forall a. RealFloatNaN a => a -> Bool
isSignaling Double
nan) 
              then (Float -> Float
forall a. RealFloatNaN a => a -> a
setPayloadSignaling Float
payload) 
              else (Float -> Float
forall a. RealFloatNaN a => a -> a
setPayload Float
payload)
              where 
                payload :: Float
payload = Double -> Float
double2Float (Double -> Float) -> Double -> Float
forall a b. (a -> b) -> a -> b
$ Double -> Double
forall a. RealFloatNaN a => a -> a
getPayload Double
nan

-- | Create a Bluespec expression consisting of a literal.
cLit :: BS.Literal -> BS.CExpr
cLit :: Literal -> CExpr
cLit = CLiteral -> CExpr
BS.CLit (CLiteral -> CExpr) -> (Literal -> CLiteral) -> Literal -> CExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Position -> Literal -> CLiteral
BS.CLiteral Position
BS.NoPos

-- | Create a Bluespec expression that indexes into a @Vector@.
cIndexVector :: BS.CExpr -> BS.CExpr -> BS.CExpr
cIndexVector :: CExpr -> CExpr -> CExpr
cIndexVector CExpr
vec CExpr
idx =
  CExpr -> [CExpr] -> CExpr
BS.CApply (Id -> CExpr
BS.CVar (Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"select")) [CExpr
vec, CExpr
idx]

-- | Create a Bluespec expression that updates a @Vector@ element at a
-- particular index.
cUpdateVector :: BS.CExpr -> BS.CExpr -> BS.CExpr -> BS.CExpr
cUpdateVector :: CExpr -> CExpr -> CExpr -> CExpr
cUpdateVector CExpr
vec CExpr
idx CExpr
newElem =
  CExpr -> [CExpr] -> CExpr
BS.CApply
    (Id -> CExpr
BS.CVar (Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"update"))
    [CExpr
vec, CExpr
idx, CExpr
newElem]

-- | Create a Bluespec identifier for a floating-point function that Bluespec
-- imports using BDPI.
fpFunId :: Type a -> String -> BS.Id
fpFunId :: forall a. Type a -> Name -> Id
fpFunId Type a
ty Name
funPrefix =
    Position -> FString -> Id
BS.mkId Position
BS.NoPos (FString -> Id) -> FString -> Id
forall a b. (a -> b) -> a -> b
$ Name -> FString
forall a. IsString a => Name -> a
fromString (Name -> FString) -> Name -> FString
forall a b. (a -> b) -> a -> b
$ Name
"bs_fp_" Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
funName
  where
    funName :: String
    funName :: Name
funName =
      case Type a
ty of
        Type a
Float  -> Name
funPrefix Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
"f"
        Type a
Double -> Name
funPrefix
        Type a
_      -> Name -> Name -> Name
forall a. Name -> Name -> a
impossible Name
"fpFunId" Name
"copilot-bluespec"

-- | Explicitly annotate an expression with a type signature. This is necessary
-- to prevent expressions from having ambiguous types in certain situations.
withTypeAnnotation :: Type a -> BS.CExpr -> BS.CExpr
withTypeAnnotation :: forall a. Type a -> CExpr -> CExpr
withTypeAnnotation Type a
ty CExpr
e = CExpr
e CExpr -> CQType -> CExpr
`BS.CHasType` [CPred] -> CType -> CQType
BS.CQType [] (Type a -> CType
forall a. Type a -> CType
transType Type a
ty)

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

-- | We assume round-near-even throughout, but this variable can be changed if
-- needed. This matches the behavior of @fpRM@ in @copilot-theorem@'s
-- @Copilot.Theorem.What4.Translate@ module.
fpRM :: BS.CExpr
fpRM :: CExpr
fpRM = Id -> [CExpr] -> CExpr
BS.CCon (Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"Rnd_Nearest_Even") []