{-# 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
           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
"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. See the @copilot-bluespec/DESIGN.md@ document for a
-- high-level description of what this file contains.
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
ifcDef
      , CDefn
mkModuleDefPragma
      , CDefn
mkModuleDef
      , CDefn
ifcRulesDef
      , CDefn
mkModuleRulesDef
      , CDefn
addModuleRulesDef
      ]
      []
  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
      , 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"
      ]

    -- interface <prefix>Ifc {-# always_ready, always_enabled #-} =
    --   ...
    ifcDef :: BS.CDefn
    ifcDef :: CDefn
ifcDef = Bool
-> StructSubType -> IdK -> [Id] -> CFields -> [CTypeclass] -> CDefn
BS.Cstruct
               Bool
True
               ([IfcPragma] -> StructSubType
BS.SInterface [IfcPragma
BS.PIAlwaysRdy, IfcPragma
BS.PIAlwaysEnabled])
               (Id -> IdK
BS.IdK Id
ifcId)
               [] -- No type variables
               CFields
ifcFields
               [] -- No derived instances

    -- {-# properties mkFibs = { verilog } #-}
    mkModuleDefPragma :: BS.CDefn
    mkModuleDefPragma :: CDefn
mkModuleDefPragma = Pragma -> CDefn
BS.CPragma (Pragma -> CDefn) -> Pragma -> CDefn
forall a b. (a -> b) -> a -> b
$ Id -> [PProp] -> Pragma
BS.Pproperties Id
mkModuleDefId [PProp
BS.PPverilog]

    -- mk<prefix> :: Module <prefix>Ifc
    -- mk<prefix> =
    --   module
    --     ...
    mkModuleDef :: BS.CDefn
    mkModuleDef :: CDefn
mkModuleDef = CDef -> CDefn
BS.CValueSign (CDef -> CDefn) -> CDef -> CDefn
forall a b. (a -> b) -> a -> b
$
      Id -> CQType -> [CClause] -> CDef
BS.CDef
        Id
mkModuleDefId
        ([CPred] -> CType -> CQType
BS.CQType [] (CType
BS.tModule CType -> CType -> CType
`BS.TAp` CType
ifcTy))
        [ [CPat] -> [CQual] -> CExpr -> CClause
BS.CClause [] [] (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
$
              [CMStmt]
wireGlobalStmts [CMStmt] -> [CMStmt] -> [CMStmt]
forall a. [a] -> [a] -> [a]
++ [CMStmt]
genFunStmts [CMStmt] -> [CMStmt] -> [CMStmt]
forall a. [a] -> [a] -> [a]
++ [CMStmt]
ruleIfcStmts
        ]
      where
        wireGlobalStmts :: [BS.CMStmt]
        wireGlobalStmts :: [CMStmt]
wireGlobalStmts = (CStmt -> CMStmt) -> [CStmt] -> [CMStmt]
forall a b. (a -> b) -> [a] -> [b]
map CStmt -> CMStmt
BS.CMStmt ([CStmt]
mkExtWires [CStmt] -> [CStmt] -> [CStmt]
forall a. [a] -> [a] -> [a]
++ [CStmt]
mkGlobals)

        genFunStmts :: [BS.CMStmt]
        genFunStmts :: [CMStmt]
genFunStmts =
          -- language-bluespec's pretty-printer will error if it encounters a
          -- CSletrec with an empty list of definitions, so avoid generating a
          -- CSletrec if there are no streams.
          [ CStmt -> CMStmt
BS.CMStmt (CStmt -> CMStmt) -> CStmt -> CMStmt
forall a b. (a -> b) -> a -> b
$ [CDefl] -> CStmt
BS.CSletrec [CDefl]
genFuns | Bool -> Bool
not ([CDefl] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CDefl]
genFuns) ]

        ruleIfcStmts :: [BS.CMStmt]
        ruleIfcStmts :: [CMStmt]
ruleIfcStmts =
          [ CExpr -> CMStmt
BS.CMrules (CExpr -> CMStmt) -> CExpr -> CMStmt
forall a b. (a -> b) -> a -> b
$ [CSchedulePragma] -> [CRule] -> CExpr
BS.Crules [] ([CRule] -> CExpr) -> [CRule] -> CExpr
forall a b. (a -> b) -> a -> b
$ Maybe CRule -> [CRule]
forall a. Maybe a -> [a]
maybeToList (Maybe CRule -> [CRule]) -> Maybe CRule -> [CRule]
forall a b. (a -> b) -> a -> b
$ [Stream] -> Maybe CRule
mkStepRule [Stream]
streams
          , CExpr -> CMStmt
BS.CMinterface (CExpr -> CMStmt) -> CExpr -> CMStmt
forall a b. (a -> b) -> a -> b
$ Position -> Maybe Id -> [CDefl] -> CExpr
BS.Cinterface Position
BS.NoPos (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
ifcId) [CDefl]
ifcMethodImpls
          ]

    -- interface <prefix>RulesIfc =
    --   ...
    ifcRulesDef :: BS.CDefn
    ifcRulesDef :: CDefn
ifcRulesDef =
      Bool
-> StructSubType -> IdK -> [Id] -> CFields -> [CTypeclass] -> CDefn
BS.Cstruct
        Bool
True
        ([IfcPragma] -> StructSubType
BS.SInterface [])
        (Id -> IdK
BS.IdK Id
ifcRulesId)
        [] -- No type variables
        CFields
ifcRulesFields
        [] -- No derived instances

    -- mk<prefix>Rules :: <prefix>Ifc -> <prefix>RulesIfc -> Rules
    -- mk<prefix>Rules ifc ifcRules =
    --   rules
    --     ...
    mkModuleRulesDef :: BS.CDefn
    mkModuleRulesDef :: CDefn
mkModuleRulesDef =
      CDef -> CDefn
BS.CValueSign (CDef -> CDefn) -> CDef -> CDefn
forall a b. (a -> b) -> a -> b
$
        Id -> CQType -> [CClause] -> CDef
BS.CDef
          Id
mkModuleRulesDefId
          ([CPred] -> CType -> CQType
BS.CQType [] CType
mkModuleRulesType)
          [ [CPat] -> [CQual] -> CExpr -> CClause
BS.CClause
              ((Id -> CPat) -> [Id] -> [CPat]
forall a b. (a -> b) -> [a] -> [b]
map Id -> CPat
BS.CPVar [Id
ifcArgId, Id
ifcRulesArgId])
              []
              ([CSchedulePragma] -> [CRule] -> CExpr
BS.Crules [] [CRule]
moduleRules)
          ]
      where
        -- <prefix>Ifc -> <prefix>RulesIfc -> Rules
        mkModuleRulesType :: BS.CType
        mkModuleRulesType :: CType
mkModuleRulesType =
          CType
BS.tArrow CType -> CType -> CType
`BS.TAp` CType
ifcTy CType -> CType -> CType
`BS.TAp`
            (CType
BS.tArrow CType -> CType -> CType
`BS.TAp` CType
ifcRulesTy CType -> CType -> CType
`BS.TAp` CType
BS.tRules)

        -- rules
        --   ...
        moduleRules :: [BS.CRule]
        moduleRules :: [CRule]
moduleRules = (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]
++ (External -> CRule) -> [External] -> [CRule]
forall a b. (a -> b) -> [a] -> [b]
map External -> CRule
mkExtRule [External]
exts

    -- add<prefix>Rules :: <prefix>Ifc -> <prefix>RulesIfc -> Module Empty
    -- add<prefix>Rules ifc ifcRules = addRules (mk<prefix>Rules ifc ifcRules)
    addModuleRulesDef :: BS.CDefn
    addModuleRulesDef :: CDefn
addModuleRulesDef =
      CDef -> CDefn
BS.CValueSign (CDef -> CDefn) -> CDef -> CDefn
forall a b. (a -> b) -> a -> b
$
        Id -> CQType -> [CClause] -> CDef
BS.CDef
          Id
addModuleRulesDefId
          ([CPred] -> CType -> CQType
BS.CQType [] CType
addModuleRulesType)
          [ [CPat] -> [CQual] -> CExpr -> CClause
BS.CClause
              ((Id -> CPat) -> [Id] -> [CPat]
forall a b. (a -> b) -> [a] -> [b]
map Id -> CPat
BS.CPVar [Id
ifcArgId, Id
ifcRulesArgId])
              []
              CExpr
addModuleRulesExpr
          ]
      where
        -- <prefix>Ifc -> <prefix>RulesIfc -> Module Empty
        addModuleRulesType :: BS.CType
        addModuleRulesType :: CType
addModuleRulesType =
          CType
BS.tArrow CType -> CType -> CType
`BS.TAp` CType
ifcTy CType -> CType -> CType
`BS.TAp`
           (CType
BS.tArrow CType -> CType -> CType
`BS.TAp` CType
ifcRulesTy CType -> CType -> CType
`BS.TAp`
             (CType
BS.tModule CType -> CType -> CType
`BS.TAp` CType
emptyTy))

        -- addRules (mk<prefix>Rules ifc ifcRules)
        addModuleRulesExpr :: BS.CExpr
        addModuleRulesExpr :: CExpr
addModuleRulesExpr =
          CExpr -> [CExpr] -> CExpr
BS.CApply
           (Id -> CExpr
BS.CVar (Position -> Id
BS.idAddRules Position
BS.NoPos))
           [CExpr -> [CExpr] -> CExpr
BS.CApply
             (Id -> CExpr
BS.CVar Id
mkModuleRulesDefId)
             ((Id -> CExpr) -> [Id] -> [CExpr]
forall a b. (a -> b) -> [a] -> [b]
map Id -> CExpr
BS.CVar [Id
ifcArgId, Id
ifcRulesArgId])]

    mkModuleDefId :: Id
mkModuleDefId =
      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
    mkModuleRulesDefId :: Id
mkModuleRulesDefId =
      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 Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
"Rules"
    addModuleRulesDefId :: Id
addModuleRulesDefId =
      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
"add" Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
prefix Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
"Rules"

    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

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

    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
    ifcRulesArgId :: Id
ifcRulesArgId = 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
ifcRulesArgName

    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 :: CFields
ifcFields = [UniqueTrigger] -> [External] -> CFields
mkSpecIfcFields [UniqueTrigger]
uniqueTriggers [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) -> CFields -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map CField -> Id
BS.cf_name CFields
ifcFields)
                  })

    ifcRulesId :: Id
ifcRulesId     = 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
specIfcRulesName Name
prefix
    ifcRulesFields :: CFields
ifcRulesFields = [Trigger] -> [External] -> CFields
mkSpecIfcRulesFields [Trigger]
triggersNoDups [External]
exts

    ifcRulesTy :: CType
ifcRulesTy =
      TyCon -> CType
BS.TCon (TyCon -> CType) -> TyCon -> CType
forall a b. (a -> b) -> a -> b
$
        BS.TyCon
          { tcon_name :: Id
BS.tcon_name = Id
ifcRulesId
          , 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) -> CFields -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map CField -> Id
BS.cf_name CFields
ifcRulesFields)
          }

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

    -- Bind @Wire@ variables for each extern stream.
    mkExtWires :: [BS.CStmt]
    mkExtWires :: [CStmt]
mkExtWires = (External -> CStmt) -> [External] -> [CStmt]
forall a b. (a -> b) -> [a] -> [b]
map External -> CStmt
extWireStmt [External]
exts
      where
        extWireStmt :: External -> BS.CStmt
        extWireStmt :: External -> CStmt
extWireStmt (External Name
name Type a
ty) = Name -> Type a -> CStmt
forall a. Name -> Type a -> CStmt
mkExtWireDecln Name
name Type a
ty

    -- 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 for streams.
    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
      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

    -- Make interface methods for @<prefix>Ifc@.
    ifcMethodImpls :: [BS.CDefl]
    ifcMethodImpls :: [CDefl]
ifcMethodImpls =
        (UniqueTrigger -> [CDefl]) -> [UniqueTrigger] -> [CDefl]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap UniqueTrigger -> [CDefl]
triggerMethodImpls [UniqueTrigger]
uniqueTriggers
          [CDefl] -> [CDefl] -> [CDefl]
forall a. [a] -> [a] -> [a]
++ (External -> CDefl) -> [External] -> [CDefl]
forall a b. (a -> b) -> [a] -> [b]
map External -> CDefl
extMethodImpl [External]
exts
      where
        -- interface
        --   ext val = ext_wire := val
        extMethodImpl :: External -> BS.CDefl
        extMethodImpl :: External -> CDefl
extMethodImpl (External Name
name Type a
_) =
            Id -> [CClause] -> [CQual] -> CDefl
BS.CLValue Id
extMethodId [CClause
extMethodClause] []
          where
            extMethodId :: Id
extMethodId = Position -> FString -> Id
BS.mkId Position
BS.NoPos (Name -> FString
forall a. IsString a => Name -> a
fromString Name
name)
            valId :: Id
valId       = Position -> FString -> Id
BS.mkId Position
BS.NoPos FString
"val"

            -- ext val = ext_wire := val
            extMethodClause :: BS.CClause
            extMethodClause :: CClause
extMethodClause =
              [CPat] -> [CQual] -> CExpr -> CClause
BS.CClause
               [Id -> CPat
BS.CPVar Id
valId]
               []
               (Position -> CExpr -> CExpr -> CExpr
BS.Cwrite
                 Position
BS.NoPos
                 (Id -> CExpr
BS.CVar (Position -> FString -> Id
BS.mkId Position
BS.NoPos (Name -> FString
forall a. IsString a => Name -> a
fromString (Name -> Name
wireName Name
name))))
                 (Id -> CExpr
BS.CVar Id
valId))

        -- interface
        --   trig_guard = ...
        --   trig_arg0 = ...
        --   ...
        --   trig_arg(n-1) = ...
        triggerMethodImpls :: UniqueTrigger -> [BS.CDefl]
        triggerMethodImpls :: UniqueTrigger -> [CDefl]
triggerMethodImpls UniqueTrigger
uniqueTrigger = CDefl
guardDef CDefl -> [CDefl] -> [CDefl]
forall a. a -> [a] -> [a]
: [CDefl]
argDefs
          where
            UniqueTrigger Name
uniqueName (Trigger Name
_name Expr Bool
guard [UExpr]
args) = UniqueTrigger
uniqueTrigger

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