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

-- 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]
_) =
  let ifcArgId :: Id
ifcArgId = 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
ifcArgName in
  CExpr -> Id -> CExpr
BS.CSelect
    (CExpr -> Id -> CExpr
BS.CSelect
      (Id -> CExpr
BS.CVar Id
ifcArgId)
      (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))
    (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
forall a b. (Real a, Fractional b) => a -> b
realToFrac
    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))

-- | 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 intentionally does not support negative literal syntax (e.g.,
    -- -42.5), so we must create negative floating-point literals using the
    -- `negate` function.
    | 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
    | 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]

-- | 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") []