{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}

-- | Compile Copilot specifications to Bluespec code.
module Copilot.Compile.Bluespec.Compile
  ( compile
  , compileWith
  ) where

-- External imports
import Data.List                      (nub, nubBy, union)
import Data.Maybe                     (catMaybes, maybeToList)
import Data.String                    (IsString (..))
import Data.Type.Equality             (testEquality, (:~:)(Refl))
import Data.Typeable                  (Typeable)
import qualified Language.Bluespec.Classic.AST as BS
import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS
import qualified Language.Bluespec.Classic.AST.Builtin.Types as BS
import Text.PrettyPrint.HughesPJClass (Pretty (..), render)
import System.Directory               (createDirectoryIfMissing)
import System.Exit                    (exitFailure)
import System.FilePath                ((</>))
import System.IO                      (hPutStrLn, stderr)

-- Internal imports: Copilot
import Copilot.Core

-- Internal imports
import Copilot.Compile.Bluespec.CodeGen
import Copilot.Compile.Bluespec.External
import Copilot.Compile.Bluespec.FloatingPoint
import Copilot.Compile.Bluespec.Name
import Copilot.Compile.Bluespec.Representation
import Copilot.Compile.Bluespec.Settings

-- | Compile a specification to a Bluespec file.
--
-- The first argument is the settings for the Bluespec code generated.
--
-- The second argument is used as a module name and the prefix for the .bs files
-- that are generated.
compileWith :: BluespecSettings -> String -> Spec -> IO ()
compileWith :: BluespecSettings -> Name -> Spec -> IO ()
compileWith BluespecSettings
bsSettings Name
prefix Spec
spec
  | [Trigger] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Trigger]
triggers
  = do Handle -> Name -> IO ()
hPutStrLn Handle
stderr (Name -> IO ()) -> Name -> IO ()
forall a b. (a -> b) -> a -> b
$
         Name
"Copilot error: attempt at compiling empty specification.\n"
         Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
"You must define at least one trigger to generate Bluespec monitors."
       IO ()
forall a. IO a
exitFailure

  | [Trigger] -> Bool
incompatibleTriggers [Trigger]
triggers
  = do Handle -> Name -> IO ()
hPutStrLn Handle
stderr (Name -> IO ()) -> Name -> IO ()
forall a b. (a -> b) -> a -> b
$
         Name
"Copilot error: attempt at compiling specification with conflicting "
         Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
"trigger definitions.\n"
         Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
"Multiple triggers have the same name, but different argument "
         Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
"types.\n"
       IO ()
forall a. IO a
exitFailure

  | Bool
otherwise
  = do let typesBsFile :: Name
typesBsFile = Doc -> Name
render (Doc -> Name) -> Doc -> Name
forall a b. (a -> b) -> a -> b
$ CPackage -> Doc
forall a. Pretty a => a -> Doc
pPrint (CPackage -> Doc) -> CPackage -> Doc
forall a b. (a -> b) -> a -> b
$ BluespecSettings -> Name -> Spec -> CPackage
compileTypesBS BluespecSettings
bsSettings Name
prefix Spec
spec
           ifcBsFile :: Name
ifcBsFile   = Doc -> Name
render (Doc -> Name) -> Doc -> Name
forall a b. (a -> b) -> a -> b
$ CPackage -> Doc
forall a. Pretty a => a -> Doc
pPrint (CPackage -> Doc) -> CPackage -> Doc
forall a b. (a -> b) -> a -> b
$ BluespecSettings -> Name -> Spec -> CPackage
compileIfcBS   BluespecSettings
bsSettings Name
prefix Spec
spec
           bsFile :: Name
bsFile      = Doc -> Name
render (Doc -> Name) -> Doc -> Name
forall a b. (a -> b) -> a -> b
$ CPackage -> Doc
forall a. Pretty a => a -> Doc
pPrint (CPackage -> Doc) -> CPackage -> Doc
forall a b. (a -> b) -> a -> b
$ BluespecSettings -> Name -> Spec -> CPackage
compileBS      BluespecSettings
bsSettings Name
prefix Spec
spec

       let dir :: Name
dir = BluespecSettings -> Name
bluespecSettingsOutputDirectory BluespecSettings
bsSettings
       Bool -> Name -> IO ()
createDirectoryIfMissing Bool
True Name
dir
       Name -> Name -> IO ()
writeFile (Name
dir Name -> Name -> Name
</> Name -> Name
specTypesPkgName Name
prefix Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
".bs") Name
typesBsFile
       Name -> Name -> IO ()
writeFile (Name
dir Name -> Name -> Name
</> Name -> Name
specIfcPkgName Name
prefix Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
".bs") Name
ifcBsFile
       Name -> Name -> IO ()
writeFile (Name
dir Name -> Name -> Name
</> Name
"bs_fp.c") Name
copilotBluespecFloatingPointC
       Name -> Name -> IO ()
writeFile (Name
dir Name -> Name -> Name
</> Name
"BluespecFP.bsv") Name
copilotBluespecFloatingPointBSV
       Name -> Name -> IO ()
writeFile (Name
dir Name -> Name -> Name
</> Name
prefix Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
".bs") Name
bsFile
  where
    triggers :: [Trigger]
triggers = Spec -> [Trigger]
specTriggers Spec
spec

    -- Check that two triggers do no conflict, that is: if their names are
    -- equal, the types of their arguments should be equal as well.
    incompatibleTriggers :: [Trigger] -> Bool
    incompatibleTriggers :: [Trigger] -> Bool
incompatibleTriggers = (Trigger -> Trigger -> Bool) -> [Trigger] -> Bool
forall a. (a -> a -> Bool) -> [a] -> Bool
pairwiseAny Trigger -> Trigger -> Bool
conflict
      where
        conflict :: Trigger -> Trigger -> Bool
        conflict :: Trigger -> Trigger -> Bool
conflict t1 :: Trigger
t1@(Trigger Name
name1 Expr Bool
_ [UExpr]
_) t2 :: Trigger
t2@(Trigger Name
name2 Expr Bool
_ [UExpr]
_) =
          Name
name1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
name2 Bool -> Bool -> Bool
&& Bool -> Bool
not (Trigger -> Trigger -> Bool
compareTrigger Trigger
t1 Trigger
t2)

        -- True if the function holds for any pair of elements. We assume that
        -- the function is commutative.
        pairwiseAny :: (a -> a -> Bool) -> [a] -> Bool
        pairwiseAny :: forall a. (a -> a -> Bool) -> [a] -> Bool
pairwiseAny a -> a -> Bool
_ []     = Bool
False
        pairwiseAny a -> a -> Bool
_ (a
_:[]) = Bool
False
        pairwiseAny a -> a -> Bool
f (a
x:[a]
xs) = (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (a -> a -> Bool
f a
x) [a]
xs Bool -> Bool -> Bool
|| (a -> a -> Bool) -> [a] -> Bool
forall a. (a -> a -> Bool) -> [a] -> Bool
pairwiseAny a -> a -> Bool
f [a]
xs

-- | Compile a specification to a Bluespec.
--
-- The first argument is used as a prefix for the generated .bs files.
compile :: String -> Spec -> IO ()
compile :: Name -> Spec -> IO ()
compile = BluespecSettings -> Name -> Spec -> IO ()
compileWith BluespecSettings
mkDefaultBluespecSettings

-- | Generate a @<prefix>.bs@ file from a 'Spec'. This is the main payload of
-- the Bluespec backend.
--
-- The generated Bluespec file will import a handful of files from the standard
-- library, as well as the following generated files:
--
-- * @<prefix>Ifc.bs@, which defines the interface containing the trigger
--   functions and external variables.
--
-- * @<prefix>Types.bs@, which defines any structs used in the 'Spec'.
--
-- It will also generate a @mk<prefix> :: Module <prefix>Ifc -> Module Empty@
-- function, which defines the module structure for this 'Spec'. The
-- @mk<prefix>@ function has the following structure:
--
-- * First, bind the argument of type @Module <prefix>Ifc@ so that trigger
--   functions can be invoked and external variables can be used.
--
-- * Next, declare stream buffers and indices.
--
-- * Next, declare generator functions for streams, accessor functions for
--   streams, and guard functions for triggers.
--
-- * Next, declare rules for each trigger function.
--
-- * Finally, declare a single rule that updates the stream buffers and
--   indices.
compileBS :: BluespecSettings -> String -> Spec -> BS.CPackage
compileBS :: BluespecSettings -> Name -> Spec -> CPackage
compileBS BluespecSettings
_bsSettings Name
prefix Spec
spec =
    Id
-> Either [CExport] [CExport]
-> [CImport]
-> [CFixity]
-> [CDefn]
-> [CInclude]
-> CPackage
BS.CPackage
      (Position -> FString -> Id
BS.mkId Position
BS.NoPos (Name -> FString
forall a. IsString a => Name -> a
fromString Name
prefix))
      ([CExport] -> Either [CExport] [CExport]
forall a b. b -> Either a b
Right [])
      ([CImport]
stdLibImports [CImport] -> [CImport] -> [CImport]
forall a. [a] -> [a] -> [a]
++ [CImport]
genImports)
      []
      [CDefn
moduleDef]
      []
  where
    -- import <prefix>Types
    -- import <prefix>Ifc
    genImports :: [BS.CImport]
    genImports :: [CImport]
genImports =
      [ Bool -> Id -> CImport
BS.CImpId Bool
False (Id -> CImport) -> Id -> CImport
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
specTypesPkgName Name
prefix
      , Bool -> Id -> CImport
BS.CImpId Bool
False (Id -> CImport) -> Id -> CImport
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
specIfcPkgName Name
prefix
      , Bool -> Id -> CImport
BS.CImpId Bool
False (Id -> CImport) -> Id -> CImport
forall a b. (a -> b) -> a -> b
$ Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"BluespecFP"
      ]

    moduleDef :: BS.CDefn
    moduleDef :: CDefn
moduleDef = CDef -> CDefn
BS.CValueSign (CDef -> CDefn) -> CDef -> CDefn
forall a b. (a -> b) -> a -> b
$
      Id -> CQType -> [CClause] -> CDef
BS.CDef
        (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
"mk" Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
prefix)
        -- :: Module <prefix>Ifc -> Module Empty
        ([CPred] -> CType -> CQType
BS.CQType
          []
          (CType
BS.tArrow
            CType -> CType -> CType
`BS.TAp` (CType
BS.tModule CType -> CType -> CType
`BS.TAp` CType
ifcTy)
            CType -> CType -> CType
`BS.TAp` (CType
BS.tModule CType -> CType -> CType
`BS.TAp` CType
emptyTy)))
        [ [CPat] -> [CQual] -> CExpr -> CClause
BS.CClause [Id -> CPat
BS.CPVar Id
ifcModId] [] (CExpr -> CClause) -> CExpr -> CClause
forall a b. (a -> b) -> a -> b
$
          Position -> [CMStmt] -> CExpr
BS.Cmodule Position
BS.NoPos ([CMStmt] -> CExpr) -> [CMStmt] -> CExpr
forall a b. (a -> b) -> a -> b
$
              CStmt -> CMStmt
BS.CMStmt
                (CPat -> Maybe CExpr -> [(Position, PProp)] -> CExpr -> CStmt
BS.CSBind (Id -> CPat
BS.CPVar Id
ifcArgId) Maybe CExpr
forall a. Maybe a
Nothing [] (Id -> CExpr
BS.CVar Id
ifcModId))
            CMStmt -> [CMStmt] -> [CMStmt]
forall a. a -> [a] -> [a]
: (CStmt -> CMStmt) -> [CStmt] -> [CMStmt]
forall a b. (a -> b) -> [a] -> [b]
map CStmt -> CMStmt
BS.CMStmt [CStmt]
mkGlobals [CMStmt] -> [CMStmt] -> [CMStmt]
forall a. [a] -> [a] -> [a]
++
            [ CStmt -> CMStmt
BS.CMStmt (CStmt -> CMStmt) -> CStmt -> CMStmt
forall a b. (a -> b) -> a -> b
$ [CDefl] -> CStmt
BS.CSletrec [CDefl]
genFuns
            , CExpr -> CMStmt
BS.CMrules (CExpr -> CMStmt) -> CExpr -> CMStmt
forall a b. (a -> b) -> a -> b
$ [CSchedulePragma] -> [CRule] -> CExpr
BS.Crules [] [CRule]
rules
            ]
        ]

    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
    ifcModId :: Id
ifcModId = Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"ifcMod"

    rules :: [BS.CRule]
    rules :: [CRule]
rules = (UniqueTrigger -> CRule) -> [UniqueTrigger] -> [CRule]
forall a b. (a -> b) -> [a] -> [b]
map UniqueTrigger -> CRule
mkTriggerRule [UniqueTrigger]
uniqueTriggers [CRule] -> [CRule] -> [CRule]
forall a. [a] -> [a] -> [a]
++ Maybe CRule -> [CRule]
forall a. Maybe a -> [a]
maybeToList ([Stream] -> Maybe CRule
mkStepRule [Stream]
streams)

    streams :: [Stream]
streams        = Spec -> [Stream]
specStreams Spec
spec
    triggers :: [Trigger]
triggers       = Spec -> [Trigger]
specTriggers Spec
spec
    uniqueTriggers :: [UniqueTrigger]
uniqueTriggers = [Trigger] -> [UniqueTrigger]
mkUniqueTriggers [Trigger]
triggers
    exts :: [External]
exts           = [Stream] -> [Trigger] -> [External]
gatherExts [Stream]
streams [Trigger]
triggers

    ifcId :: Id
ifcId     = 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
specIfcName Name
prefix
    ifcFields :: [CField]
ifcFields = [Trigger] -> [External] -> [CField]
mkSpecIfcFields [Trigger]
triggers [External]
exts
    ifcTy :: CType
ifcTy     = TyCon -> CType
BS.TCon (BS.TyCon
                  { tcon_name :: Id
BS.tcon_name = Id
ifcId
                  , tcon_kind :: Maybe Kind
BS.tcon_kind = Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
BS.KStar
                  , tcon_sort :: TISort
BS.tcon_sort = StructSubType -> [Id] -> TISort
BS.TIstruct
                                     ([IfcPragma] -> StructSubType
BS.SInterface [])
                                     ((CField -> Id) -> [CField] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map CField -> Id
BS.cf_name [CField]
ifcFields)
                  })

    emptyTy :: CType
emptyTy = TyCon -> CType
BS.TCon (BS.TyCon
                { tcon_name :: Id
BS.tcon_name = Id
BS.idEmpty
                , tcon_kind :: Maybe Kind
BS.tcon_kind = Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
BS.KStar
                , tcon_sort :: TISort
BS.tcon_sort = StructSubType -> [Id] -> TISort
BS.TIstruct ([IfcPragma] -> StructSubType
BS.SInterface []) []
                })

    -- Make buffer and index declarations for streams.
    mkGlobals :: [BS.CStmt]
    mkGlobals :: [CStmt]
mkGlobals = (Stream -> [CStmt]) -> [Stream] -> [CStmt]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Stream -> [CStmt]
buffDecln [Stream]
streams [CStmt] -> [CStmt] -> [CStmt]
forall a. [a] -> [a] -> [a]
++ (Stream -> CStmt) -> [Stream] -> [CStmt]
forall a b. (a -> b) -> [a] -> [b]
map Stream -> CStmt
indexDecln [Stream]
streams
      where
        buffDecln :: Stream -> [CStmt]
buffDecln  (Stream Id
sId [a]
buff Expr a
_ Type a
ty) = Id -> Type a -> [a] -> [CStmt]
forall a. Id -> Type a -> [a] -> [CStmt]
mkBuffDecln  Id
sId Type a
ty [a]
buff
        indexDecln :: Stream -> CStmt
indexDecln (Stream Id
sId [a]
_    Expr a
_ Type a
_ ) = Id -> CStmt
mkIndexDecln Id
sId

    -- Make generator functions, including trigger arguments.
    genFuns :: [BS.CDefl]
    genFuns :: [CDefl]
genFuns =  (Stream -> CDefl) -> [Stream] -> [CDefl]
forall a b. (a -> b) -> [a] -> [b]
map Stream -> CDefl
accessDecln [Stream]
streams
            [CDefl] -> [CDefl] -> [CDefl]
forall a. [a] -> [a] -> [a]
++ (Stream -> CDefl) -> [Stream] -> [CDefl]
forall a b. (a -> b) -> [a] -> [b]
map Stream -> CDefl
streamGen [Stream]
streams
            [CDefl] -> [CDefl] -> [CDefl]
forall a. [a] -> [a] -> [a]
++ (UniqueTrigger -> [CDefl]) -> [UniqueTrigger] -> [CDefl]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap UniqueTrigger -> [CDefl]
triggerGen [UniqueTrigger]
uniqueTriggers
      where
        accessDecln :: Stream -> BS.CDefl
        accessDecln :: Stream -> CDefl
accessDecln (Stream Id
sId [a]
buff Expr a
_ Type a
ty) = Id -> Type a -> [a] -> CDefl
forall a. Id -> Type a -> [a] -> CDefl
mkAccessDecln Id
sId Type a
ty [a]
buff

        streamGen :: Stream -> BS.CDefl
        streamGen :: Stream -> CDefl
streamGen (Stream Id
sId [a]
_ Expr a
expr Type a
ty) = Name -> Expr a -> Type a -> CDefl
forall a. Name -> Expr a -> Type a -> CDefl
mkGenFun (Id -> Name
generatorName Id
sId) Expr a
expr Type a
ty

        triggerGen :: UniqueTrigger -> [BS.CDefl]
        triggerGen :: UniqueTrigger -> [CDefl]
triggerGen (UniqueTrigger Name
uniqueName (Trigger Name
_name Expr Bool
guard [UExpr]
args)) =
            CDefl
guardDef CDefl -> [CDefl] -> [CDefl]
forall a. a -> [a] -> [a]
: [CDefl]
argDefs
          where
            guardDef :: CDefl
guardDef = Name -> Expr Bool -> Type Bool -> CDefl
forall a. Name -> Expr a -> Type a -> CDefl
mkGenFun (Name -> Name
guardName Name
uniqueName) Expr Bool
guard Type Bool
Bool
            argDefs :: [CDefl]
argDefs  = ((Name, UExpr) -> CDefl) -> [(Name, UExpr)] -> [CDefl]
forall a b. (a -> b) -> [a] -> [b]
map (Name, UExpr) -> CDefl
argGen ([Name] -> [UExpr] -> [(Name, UExpr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Name -> [Name]
argNames Name
uniqueName) [UExpr]
args)

            argGen :: (String, UExpr) -> BS.CDefl
            argGen :: (Name, UExpr) -> CDefl
argGen (Name
argName, UExpr Type a
ty Expr a
expr) = Name -> Expr a -> Type a -> CDefl
forall a. Name -> Expr a -> Type a -> CDefl
mkGenFun Name
argName Expr a
expr Type a
ty

-- | Generate a @<prefix>Ifc.bs@ file from a 'Spec'. This contains the
-- definition of the @<prefix>Ifc@ interface, which declares the types of all
-- trigger functions and external variables. This is put in a separate file so
-- that larger applications can use it separately.
compileIfcBS :: BluespecSettings -> String -> Spec -> BS.CPackage
compileIfcBS :: BluespecSettings -> Name -> Spec -> CPackage
compileIfcBS BluespecSettings
_bsSettings Name
prefix Spec
spec =
    Id
-> Either [CExport] [CExport]
-> [CImport]
-> [CFixity]
-> [CDefn]
-> [CInclude]
-> CPackage
BS.CPackage
      Id
ifcPkgId
      ([CExport] -> Either [CExport] [CExport]
forall a b. b -> Either a b
Right [])
      ([CImport]
stdLibImports [CImport] -> [CImport] -> [CImport]
forall a. [a] -> [a] -> [a]
++ [CImport]
genImports)
      []
      [CDefn
ifcDef]
      []
  where
    -- import <prefix>Types
    genImports :: [BS.CImport]
    genImports :: [CImport]
genImports =
      [ Bool -> Id -> CImport
BS.CImpId Bool
False (Id -> CImport) -> Id -> CImport
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
specTypesPkgName Name
prefix
      ]

    ifcId :: Id
ifcId     = 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
specIfcName Name
prefix
    ifcPkgId :: Id
ifcPkgId  = 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
specIfcPkgName Name
prefix
    ifcFields :: [CField]
ifcFields = [Trigger] -> [External] -> [CField]
mkSpecIfcFields [Trigger]
triggers [External]
exts

    streams :: [Stream]
streams  = Spec -> [Stream]
specStreams Spec
spec
    exts :: [External]
exts     = [Stream] -> [Trigger] -> [External]
gatherExts [Stream]
streams [Trigger]
triggers

    -- Remove duplicates due to multiple guards for the same trigger.
    triggers :: [Trigger]
triggers = (Trigger -> Trigger -> Bool) -> [Trigger] -> [Trigger]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy Trigger -> Trigger -> Bool
compareTrigger (Spec -> [Trigger]
specTriggers Spec
spec)

    ifcDef :: BS.CDefn
    ifcDef :: CDefn
ifcDef = Bool
-> StructSubType
-> IdK
-> [Id]
-> [CField]
-> [CTypeclass]
-> CDefn
BS.Cstruct
               Bool
True
               ([IfcPragma] -> StructSubType
BS.SInterface [])
               (Id -> IdK
BS.IdK Id
ifcId)
               [] -- No type variables
               [CField]
ifcFields
               [] -- No derived instances

-- | Generate a @<prefix>Types.bs@ file from a 'Spec'. This declares the types
-- of any structs used by the Copilot specification. This is put in a separate
-- file so that larger applications can more easily substitute their own struct
-- definitions if desired.
compileTypesBS :: BluespecSettings -> String -> Spec -> BS.CPackage
compileTypesBS :: BluespecSettings -> Name -> Spec -> CPackage
compileTypesBS BluespecSettings
_bsSettings Name
prefix Spec
spec =
    Id
-> Either [CExport] [CExport]
-> [CImport]
-> [CFixity]
-> [CDefn]
-> [CInclude]
-> CPackage
BS.CPackage
      Id
typesId
      ([CExport] -> Either [CExport] [CExport]
forall a b. b -> Either a b
Right [])
      [CImport]
stdLibImports
      []
      [CDefn]
structDefs
      []
  where
    typesId :: Id
typesId = 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
specTypesPkgName Name
prefix

    structDefs :: [CDefn]
structDefs = [UExpr] -> [CDefn]
mkTypeDeclns [UExpr]
exprs

    exprs :: [UExpr]
exprs    = [Stream] -> [Trigger] -> [UExpr]
gatherExprs [Stream]
streams [Trigger]
triggers
    streams :: [Stream]
streams  = Spec -> [Stream]
specStreams Spec
spec

    -- Remove duplicates due to multiple guards for the same trigger.
    triggers :: [Trigger]
triggers = (Trigger -> Trigger -> Bool) -> [Trigger] -> [Trigger]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy Trigger -> Trigger -> Bool
compareTrigger (Spec -> [Trigger]
specTriggers Spec
spec)

    -- Generate type declarations.
    mkTypeDeclns :: [UExpr] -> [BS.CDefn]
    mkTypeDeclns :: [UExpr] -> [CDefn]
mkTypeDeclns [UExpr]
es = [Maybe CDefn] -> [CDefn]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe CDefn] -> [CDefn]) -> [Maybe CDefn] -> [CDefn]
forall a b. (a -> b) -> a -> b
$ (UType -> Maybe CDefn) -> [UType] -> [Maybe CDefn]
forall a b. (a -> b) -> [a] -> [b]
map UType -> Maybe CDefn
mkTypeDecln [UType]
uTypes
      where
        uTypes :: [UType]
uTypes = [UType] -> [UType]
forall a. Eq a => [a] -> [a]
nub ([UType] -> [UType]) -> [UType] -> [UType]
forall a b. (a -> b) -> a -> b
$ (UExpr -> [UType]) -> [UExpr] -> [UType]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(UExpr Type a
_ Expr a
e) -> Expr a -> [UType]
forall a. Typeable a => Expr a -> [UType]
exprTypes Expr a
e) [UExpr]
es

        mkTypeDecln :: UType -> Maybe CDefn
mkTypeDecln (UType Type a
ty) = case Type a
ty of
          Struct a
x -> CDefn -> Maybe CDefn
forall a. a -> Maybe a
Just (CDefn -> Maybe CDefn) -> CDefn -> Maybe CDefn
forall a b. (a -> b) -> a -> b
$ a -> CDefn
forall a. Struct a => a -> CDefn
mkStructDecln a
x
          Type a
_        -> Maybe CDefn
forall a. Maybe a
Nothing

-- | Imports from the Bluespec standard library.
stdLibImports :: [BS.CImport]
stdLibImports :: [CImport]
stdLibImports =
  [ Bool -> Id -> CImport
BS.CImpId Bool
False (Id -> CImport) -> Id -> CImport
forall a b. (a -> b) -> a -> b
$ Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"FloatingPoint"
  , Bool -> Id -> CImport
BS.CImpId Bool
False (Id -> CImport) -> Id -> CImport
forall a b. (a -> b) -> a -> b
$ Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"Vector"
  ]

-- ** Obtain information from Copilot Core Exprs and Types.

-- | List all types of an expression, returns items uniquely.
exprTypes :: Typeable a => Expr a -> [UType]
exprTypes :: forall a. Typeable a => Expr a -> [UType]
exprTypes Expr a
e = case Expr a
e of
  Const Type a
ty a
_            -> Type a -> [UType]
forall a. Typeable a => Type a -> [UType]
typeTypes Type a
ty
  Local Type a1
ty1 Type a
ty2 Name
_ Expr a1
e1 Expr a
e2 -> Type a1 -> [UType]
forall a. Typeable a => Type a -> [UType]
typeTypes Type a1
ty1 [UType] -> [UType] -> [UType]
forall a. Eq a => [a] -> [a] -> [a]
`union` Type a -> [UType]
forall a. Typeable a => Type a -> [UType]
typeTypes Type a
ty2
                             [UType] -> [UType] -> [UType]
forall a. Eq a => [a] -> [a] -> [a]
`union` Expr a1 -> [UType]
forall a. Typeable a => Expr a -> [UType]
exprTypes Expr a1
e1 [UType] -> [UType] -> [UType]
forall a. Eq a => [a] -> [a] -> [a]
`union` Expr a -> [UType]
forall a. Typeable a => Expr a -> [UType]
exprTypes Expr a
e2
  Var Type a
ty Name
_              -> Type a -> [UType]
forall a. Typeable a => Type a -> [UType]
typeTypes Type a
ty
  Drop Type a
ty DropIdx
_ Id
_           -> Type a -> [UType]
forall a. Typeable a => Type a -> [UType]
typeTypes Type a
ty
  ExternVar Type a
ty Name
_ Maybe [a]
_      -> Type a -> [UType]
forall a. Typeable a => Type a -> [UType]
typeTypes Type a
ty
  Op1 Op1 a1 a
_ Expr a1
e1              -> Expr a1 -> [UType]
forall a. Typeable a => Expr a -> [UType]
exprTypes Expr a1
e1
  Op2 Op2 a1 b a
_ Expr a1
e1 Expr b
e2           -> Expr a1 -> [UType]
forall a. Typeable a => Expr a -> [UType]
exprTypes Expr a1
e1 [UType] -> [UType] -> [UType]
forall a. Eq a => [a] -> [a] -> [a]
`union` Expr b -> [UType]
forall a. Typeable a => Expr a -> [UType]
exprTypes Expr b
e2
  Op3 Op3 a1 b c a
_ Expr a1
e1 Expr b
e2 Expr c
e3        -> Expr a1 -> [UType]
forall a. Typeable a => Expr a -> [UType]
exprTypes Expr a1
e1 [UType] -> [UType] -> [UType]
forall a. Eq a => [a] -> [a] -> [a]
`union` Expr b -> [UType]
forall a. Typeable a => Expr a -> [UType]
exprTypes Expr b
e2
                             [UType] -> [UType] -> [UType]
forall a. Eq a => [a] -> [a] -> [a]
`union` Expr c -> [UType]
forall a. Typeable a => Expr a -> [UType]
exprTypes Expr c
e3
  Label Type a
ty Name
_ Expr a
_          -> Type a -> [UType]
forall a. Typeable a => Type a -> [UType]
typeTypes Type a
ty

-- | List all types of a type, returns items uniquely.
typeTypes :: Typeable a => Type a -> [UType]
typeTypes :: forall a. Typeable a => Type a -> [UType]
typeTypes Type a
ty = case Type a
ty of
  Array Type t
ty' -> Type t -> [UType]
forall a. Typeable a => Type a -> [UType]
typeTypes Type t
ty' [UType] -> [UType] -> [UType]
forall a. Eq a => [a] -> [a] -> [a]
`union` [Type a -> UType
forall a. Typeable a => Type a -> UType
UType Type a
ty]
  Struct a
x  -> (Value a -> [UType]) -> [Value a] -> [UType]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Value Type t
ty' Field s t
_) -> Type t -> [UType]
forall a. Typeable a => Type a -> [UType]
typeTypes Type t
ty') (a -> [Value a]
forall a. Struct a => a -> [Value a]
toValues a
x)
                 [UType] -> [UType] -> [UType]
forall a. Eq a => [a] -> [a] -> [a]
`union` [Type a -> UType
forall a. Typeable a => Type a -> UType
UType Type a
ty]
  Type a
_         -> [Type a -> UType
forall a. Typeable a => Type a -> UType
UType Type a
ty]

-- | Collect all expression of a list of streams and triggers and wrap them
-- into an UEXpr.
gatherExprs :: [Stream] -> [Trigger] -> [UExpr]
gatherExprs :: [Stream] -> [Trigger] -> [UExpr]
gatherExprs [Stream]
streams [Trigger]
triggers =  (Stream -> UExpr) -> [Stream] -> [UExpr]
forall a b. (a -> b) -> [a] -> [b]
map Stream -> UExpr
streamUExpr [Stream]
streams
                             [UExpr] -> [UExpr] -> [UExpr]
forall a. [a] -> [a] -> [a]
++ (Trigger -> [UExpr]) -> [Trigger] -> [UExpr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Trigger -> [UExpr]
triggerUExpr [Trigger]
triggers
  where
    streamUExpr :: Stream -> UExpr
streamUExpr  (Stream Id
_ [a]
_ Expr a
expr Type a
ty)   = Type a -> Expr a -> UExpr
forall a. Typeable a => Type a -> Expr a -> UExpr
UExpr Type a
ty Expr a
expr
    triggerUExpr :: Trigger -> [UExpr]
triggerUExpr (Trigger Name
_ Expr Bool
guard [UExpr]
args) = Type Bool -> Expr Bool -> UExpr
forall a. Typeable a => Type a -> Expr a -> UExpr
UExpr Type Bool
Bool Expr Bool
guard UExpr -> [UExpr] -> [UExpr]
forall a. a -> [a] -> [a]
: [UExpr]
args

-- | We consider triggers to be equal, if their names match and the number and
-- types of arguments.
compareTrigger :: Trigger -> Trigger -> Bool
compareTrigger :: Trigger -> Trigger -> Bool
compareTrigger (Trigger Name
name1 Expr Bool
_ [UExpr]
args1) (Trigger Name
name2 Expr Bool
_ [UExpr]
args2)
  = Name
name1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
name2 Bool -> Bool -> Bool
&& [UExpr] -> [UExpr] -> Bool
compareArguments [UExpr]
args1 [UExpr]
args2

  where
    compareArguments :: [UExpr] -> [UExpr] -> Bool
    compareArguments :: [UExpr] -> [UExpr] -> Bool
compareArguments []     []     = Bool
True
    compareArguments []     [UExpr]
_      = Bool
False
    compareArguments [UExpr]
_      []     = Bool
False
    compareArguments (UExpr
x:[UExpr]
xs) (UExpr
y:[UExpr]
ys) = UExpr -> UExpr -> Bool
compareUExpr UExpr
x UExpr
y Bool -> Bool -> Bool
&& [UExpr] -> [UExpr] -> Bool
compareArguments [UExpr]
xs [UExpr]
ys

    compareUExpr :: UExpr -> UExpr -> Bool
    compareUExpr :: UExpr -> UExpr -> Bool
compareUExpr (UExpr Type a
ty1 Expr a
_) (UExpr Type a
ty2 Expr a
_)
      | Just a :~: a
Refl <- Type a -> Type a -> Maybe (a :~: a)
forall a b. Type a -> Type b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Type a
ty1 Type a
ty2 = Bool
True
      | Bool
otherwise                         = Bool
False