{-# LANGUAGE GADTs #-}
-- | Compile Copilot specifications to C99 code.
module Copilot.Compile.C99.Compile
  ( compile
  , compileWith
  ) where

-- External imports
import           Data.List           ( nub, nubBy, union )
import           Data.Maybe          ( mapMaybe )
import           Data.Type.Equality  ( testEquality, (:~:)(Refl) )
import           Data.Typeable       ( Typeable )
import           Language.C99.Pretty ( pretty )
import qualified Language.C99.Simple as C
import           System.Directory    ( createDirectoryIfMissing )
import           System.Exit         ( exitFailure )
import           System.FilePath     ( (</>) )
import           System.IO           ( hPutStrLn, stderr )
import           Text.PrettyPrint    ( render )

-- Internal imports: Copilot
import Copilot.Core ( Expr (..), Spec (..), Stream (..), Struct (..),
                      Trigger (..), Type (..), UExpr (..), UType (..),
                      Value (..) )

-- Internal imports
import Copilot.Compile.C99.CodeGen        ( mkAccessDecln, mkBuffDecln,
                                            mkExtCpyDecln, mkExtDecln,
                                            mkGenFun, mkGenFunArray,
                                            mkIndexDecln, mkStep,
                                            mkStructDecln, mkStructForwDecln )
import Copilot.Compile.C99.External       ( External, gatherExts )
import Copilot.Compile.C99.Name           ( argNames, generatorName,
                                            generatorOutputArgName, guardName )
import Copilot.Compile.C99.Settings       ( CSettings,
                                            cSettingsOutputDirectory,
                                            cSettingsStepFunctionName,
                                            mkDefaultCSettings )
import Copilot.Compile.C99.Type           ( transType )
import Copilot.Compile.C99.Representation ( UniqueTrigger (..),
                                            mkUniqueTriggers )

-- | Compile a specification to a .h and a .c file.
--
-- The first argument is the settings for the C code generated.
--
-- The second argument is used as prefix for the .h and .c files generated.
compileWith :: CSettings -> String -> Spec -> IO ()
compileWith :: CSettings -> Name -> Spec -> IO ()
compileWith CSettings
cSettings 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 C 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 cFile :: Name
cFile = Doc -> Name
render (Doc -> Name) -> Doc -> Name
forall a b. (a -> b) -> a -> b
$ TransUnit -> Doc
forall a. Pretty a => a -> Doc
pretty (TransUnit -> Doc) -> TransUnit -> Doc
forall a b. (a -> b) -> a -> b
$ TransUnit -> TransUnit
C.translate (TransUnit -> TransUnit) -> TransUnit -> TransUnit
forall a b. (a -> b) -> a -> b
$ CSettings -> Spec -> TransUnit
compileC CSettings
cSettings Spec
spec
           hFile :: Name
hFile = Doc -> Name
render (Doc -> Name) -> Doc -> Name
forall a b. (a -> b) -> a -> b
$ TransUnit -> Doc
forall a. Pretty a => a -> Doc
pretty (TransUnit -> Doc) -> TransUnit -> Doc
forall a b. (a -> b) -> a -> b
$ TransUnit -> TransUnit
C.translate (TransUnit -> TransUnit) -> TransUnit -> TransUnit
forall a b. (a -> b) -> a -> b
$ CSettings -> Spec -> TransUnit
compileH CSettings
cSettings Spec
spec
           typeDeclnsFile :: Name
typeDeclnsFile = TransUnit -> Name
safeCRender (TransUnit -> Name) -> TransUnit -> Name
forall a b. (a -> b) -> a -> b
$ CSettings -> Spec -> TransUnit
compileTypeDeclns CSettings
cSettings Spec
spec

           cMacros :: Name
cMacros = [Name] -> Name
unlines [ Name
"#include <stdint.h>"
                             , Name
"#include <stdbool.h>"
                             , Name
"#include <string.h>"
                             , Name
"#include <stdlib.h>"
                             , Name
"#include <math.h>"
                             , Name
""
                             , Name
"#include \"" Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
prefix Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
"_types.h\""
                             , Name
"#include \"" Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
prefix Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
".h\""
                             , Name
""
                             ]

       let dir :: Name
dir = CSettings -> Name
cSettingsOutputDirectory CSettings
cSettings
       Bool -> Name -> IO ()
createDirectoryIfMissing Bool
True Name
dir
       Name -> Name -> IO ()
writeFile (Name
dir Name -> Name -> Name
</> Name
prefix Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
".c") (Name -> IO ()) -> Name -> IO ()
forall a b. (a -> b) -> a -> b
$ Name
cMacros Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
cFile
       Name -> Name -> IO ()
writeFile (Name
dir Name -> Name -> Name
</> Name
prefix Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
".h") Name
hFile
       Name -> Name -> IO ()
writeFile (Name
dir Name -> Name -> Name
</> Name
prefix Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
"_types.h") Name
typeDeclnsFile
  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 .h and a .c file.
--
-- The first argument is used as prefix for the .h and .c files generated.
compile :: String -> Spec -> IO ()
compile :: Name -> Spec -> IO ()
compile = CSettings -> Name -> Spec -> IO ()
compileWith CSettings
mkDefaultCSettings

-- | Generate the .c file from a 'Spec'.
--
-- The generated C file has the following structure:
--
-- * Include .h file.
-- * Declarations of global buffers and indices.
-- * Generator functions for streams, guards and trigger arguments.
-- * Declaration of the @step()@ function.
compileC :: CSettings -> Spec -> C.TransUnit
compileC :: CSettings -> Spec -> TransUnit
compileC CSettings
cSettings Spec
spec = [Decln] -> [FunDef] -> TransUnit
C.TransUnit [Decln]
declns [FunDef]
funs
  where
    declns :: [Decln]
declns =  [External] -> [Decln]
mkExts [External]
exts
           [Decln] -> [Decln] -> [Decln]
forall a. [a] -> [a] -> [a]
++ [Stream] -> [Decln]
mkGlobals [Stream]
streams

    funs :: [FunDef]
funs =  [Stream] -> [UniqueTrigger] -> [FunDef]
mkGenFuns [Stream]
streams [UniqueTrigger]
uniqueTriggers
         [FunDef] -> [FunDef] -> [FunDef]
forall a. [a] -> [a] -> [a]
++ [CSettings -> [Stream] -> [UniqueTrigger] -> [External] -> FunDef
mkStep CSettings
cSettings [Stream]
streams [UniqueTrigger]
uniqueTriggers [External]
exts]

    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

    -- Make declarations for copies of external variables.
    mkExts :: [External] -> [C.Decln]
    mkExts :: [External] -> [Decln]
mkExts = (External -> Decln) -> [External] -> [Decln]
forall a b. (a -> b) -> [a] -> [b]
map External -> Decln
mkExtCpyDecln

    -- Make buffer and index declarations for streams.
    mkGlobals :: [Stream] -> [C.Decln]
    mkGlobals :: [Stream] -> [Decln]
mkGlobals [Stream]
streamList =  (Stream -> Decln) -> [Stream] -> [Decln]
forall a b. (a -> b) -> [a] -> [b]
map Stream -> Decln
buffDecln [Stream]
streamList
                         [Decln] -> [Decln] -> [Decln]
forall a. [a] -> [a] -> [a]
++ (Stream -> Decln) -> [Stream] -> [Decln]
forall a b. (a -> b) -> [a] -> [b]
map Stream -> Decln
indexDecln [Stream]
streamList
      where
        buffDecln :: Stream -> Decln
buffDecln  (Stream Id
sId [a]
buff Expr a
_ Type a
ty) = Id -> Type a -> [a] -> Decln
forall a. Id -> Type a -> [a] -> Decln
mkBuffDecln  Id
sId Type a
ty [a]
buff
        indexDecln :: Stream -> Decln
indexDecln (Stream Id
sId [a]
_    Expr a
_ Type a
_ ) = Id -> Decln
mkIndexDecln Id
sId

    -- Make generator functions, including trigger arguments.
    mkGenFuns :: [Stream] -> [UniqueTrigger] -> [C.FunDef]
    mkGenFuns :: [Stream] -> [UniqueTrigger] -> [FunDef]
mkGenFuns [Stream]
streamList [UniqueTrigger]
triggerList =  (Stream -> FunDef) -> [Stream] -> [FunDef]
forall a b. (a -> b) -> [a] -> [b]
map Stream -> FunDef
accessDecln [Stream]
streamList
                                     [FunDef] -> [FunDef] -> [FunDef]
forall a. [a] -> [a] -> [a]
++ (Stream -> FunDef) -> [Stream] -> [FunDef]
forall a b. (a -> b) -> [a] -> [b]
map Stream -> FunDef
streamGen [Stream]
streamList
                                     [FunDef] -> [FunDef] -> [FunDef]
forall a. [a] -> [a] -> [a]
++ (UniqueTrigger -> [FunDef]) -> [UniqueTrigger] -> [FunDef]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap UniqueTrigger -> [FunDef]
triggerGen [UniqueTrigger]
triggerList
      where
        accessDecln :: Stream -> C.FunDef
        accessDecln :: Stream -> FunDef
accessDecln (Stream Id
sId [a]
buff Expr a
_ Type a
ty) = Id -> Type a -> [a] -> FunDef
forall a. Id -> Type a -> [a] -> FunDef
mkAccessDecln Id
sId Type a
ty [a]
buff

        streamGen :: Stream -> C.FunDef
        streamGen :: Stream -> FunDef
streamGen (Stream Id
sId [a]
_ Expr a
expr Type a
ty) =
          Name -> Name -> Expr a -> Type a -> FunDef
forall a. Name -> Name -> Expr a -> Type a -> FunDef
exprGen (Id -> Name
generatorName Id
sId) (Id -> Name
generatorOutputArgName Id
sId) Expr a
expr Type a
ty

        triggerGen :: UniqueTrigger -> [C.FunDef]
        triggerGen :: UniqueTrigger -> [FunDef]
triggerGen (UniqueTrigger Name
uniqueName (Trigger Name
_name Expr Bool
guard [UExpr]
args)) = FunDef
guardDef FunDef -> [FunDef] -> [FunDef]
forall a. a -> [a] -> [a]
: [FunDef]
argDefs
          where
            guardDef :: FunDef
guardDef = Name -> Expr Bool -> Type Bool -> FunDef
forall a. Name -> Expr a -> Type a -> FunDef
mkGenFun (Name -> Name
guardName Name
uniqueName) Expr Bool
guard Type Bool
Bool
            argDefs :: [FunDef]
argDefs  = (Name -> UExpr -> FunDef) -> [Name] -> [UExpr] -> [FunDef]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> UExpr -> FunDef
argGen (Name -> [Name]
argNames Name
uniqueName) [UExpr]
args

            argGen :: String -> UExpr -> C.FunDef
            argGen :: Name -> UExpr -> FunDef
argGen Name
argName (UExpr Type a
ty Expr a
expr) =
              Name -> Name -> Expr a -> Type a -> FunDef
forall a. Name -> Name -> Expr a -> Type a -> FunDef
exprGen Name
argName (Name
argName Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
"_output") Expr a
expr Type a
ty

        -- Create a function that calculates the current value generated by an
        -- expression `expr` of type `ty`. The generator treats arrays
        -- specially, and the function takes an output array as a parameter.
        -- The second identifier `outputArrName` is not used if `expr` is not an
        -- array.
        exprGen :: C.Ident -> C.Ident -> Expr a -> Type a -> C.FunDef
        exprGen :: forall a. Name -> Name -> Expr a -> Type a -> FunDef
exprGen Name
funName Name
outputArrName Expr a
expr ty :: Type a
ty@(Array Type t
_) =
          Name -> Name -> Expr a -> Type a -> FunDef
forall a. Name -> Name -> Expr a -> Type a -> FunDef
mkGenFunArray Name
funName Name
outputArrName Expr a
expr Type a
ty
        exprGen Name
funName Name
_ Expr a
expr Type a
ty =
          Name -> Expr a -> Type a -> FunDef
forall a. Name -> Expr a -> Type a -> FunDef
mkGenFun Name
funName Expr a
expr Type a
ty

-- | Generate the .h file from a 'Spec'.
compileH :: CSettings -> Spec -> C.TransUnit
compileH :: CSettings -> Spec -> TransUnit
compileH CSettings
cSettings Spec
spec = [Decln] -> [FunDef] -> TransUnit
C.TransUnit [Decln]
declns []
  where
    declns :: [Decln]
declns =  [UExpr] -> [Decln]
mkStructForwDeclns [UExpr]
exprs
           [Decln] -> [Decln] -> [Decln]
forall a. [a] -> [a] -> [a]
++ [External] -> [Decln]
mkExts [External]
exts
           [Decln] -> [Decln] -> [Decln]
forall a. [a] -> [a] -> [a]
++ [Trigger] -> [Decln]
extFunDeclns [Trigger]
triggers
           [Decln] -> [Decln] -> [Decln]
forall a. [a] -> [a] -> [a]
++ [Decln
stepDecln]

    exprs :: [UExpr]
exprs    = [Stream] -> [Trigger] -> [UExpr]
gatherExprs [Stream]
streams [Trigger]
triggers
    exts :: [External]
exts     = [Stream] -> [Trigger] -> [External]
gatherExts [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)

    mkStructForwDeclns :: [UExpr] -> [C.Decln]
    mkStructForwDeclns :: [UExpr] -> [Decln]
mkStructForwDeclns [UExpr]
es = (UType -> Maybe Decln) -> [UType] -> [Decln]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe UType -> Maybe Decln
mkDecln [UType]
uTypes
      where
        mkDecln :: UType -> Maybe Decln
mkDecln (UType Type a
ty) = case Type a
ty of
          Struct a
_ -> Decln -> Maybe Decln
forall a. a -> Maybe a
Just (Decln -> Maybe Decln) -> Decln -> Maybe Decln
forall a b. (a -> b) -> a -> b
$ Type a -> Decln
forall a. Struct a => Type a -> Decln
mkStructForwDecln Type a
ty
          Type a
_        -> Maybe Decln
forall a. Maybe a
Nothing

        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

    -- Make declarations for external variables.
    mkExts :: [External] -> [C.Decln]
    mkExts :: [External] -> [Decln]
mkExts = (External -> Decln) -> [External] -> [Decln]
forall a b. (a -> b) -> [a] -> [b]
map External -> Decln
mkExtDecln

    extFunDeclns :: [Trigger] -> [C.Decln]
    extFunDeclns :: [Trigger] -> [Decln]
extFunDeclns = (Trigger -> Decln) -> [Trigger] -> [Decln]
forall a b. (a -> b) -> [a] -> [b]
map Trigger -> Decln
extFunDecln
      where
        extFunDecln :: Trigger -> C.Decln
        extFunDecln :: Trigger -> Decln
extFunDecln (Trigger Name
name Expr Bool
_ [UExpr]
args) = Maybe StorageSpec -> Type -> Name -> [Param] -> Decln
C.FunDecln Maybe StorageSpec
forall a. Maybe a
Nothing Type
cTy Name
name [Param]
params
          where
            cTy :: Type
cTy    = TypeSpec -> Type
C.TypeSpec TypeSpec
C.Void
            params :: [Param]
params = (Name -> UExpr -> Param) -> [Name] -> [UExpr] -> [Param]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> UExpr -> Param
mkParam (Name -> [Name]
argNames Name
name) [UExpr]
args

            mkParam :: Name -> UExpr -> Param
mkParam Name
paramName (UExpr Type a
ty Expr a
_) = Type -> Name -> Param
C.Param (Type a -> Type
forall {a}. Type a -> Type
mkParamTy Type a
ty) Name
paramName

            -- Special case for Struct, to pass struct arguments by reference.
            -- Arrays are also passed by reference, but using C's array type
            -- does that automatically.
            mkParamTy :: Type a -> Type
mkParamTy Type a
ty =
              case Type a
ty of
                Struct a
_ -> Type -> Type
C.Ptr (Type a -> Type
forall {a}. Type a -> Type
transType Type a
ty)
                Type a
_        -> Type a -> Type
forall {a}. Type a -> Type
transType Type a
ty

    -- Declaration for the step function.
    stepDecln :: C.Decln
    stepDecln :: Decln
stepDecln = Maybe StorageSpec -> Type -> Name -> [Param] -> Decln
C.FunDecln Maybe StorageSpec
forall a. Maybe a
Nothing (TypeSpec -> Type
C.TypeSpec TypeSpec
C.Void)
                    (CSettings -> Name
cSettingsStepFunctionName CSettings
cSettings) []

-- | Generate a C translation unit that contains all type declarations needed
-- by the Copilot specification.
compileTypeDeclns :: CSettings -> Spec -> C.TransUnit
compileTypeDeclns :: CSettings -> Spec -> TransUnit
compileTypeDeclns CSettings
_cSettings Spec
spec = [Decln] -> [FunDef] -> TransUnit
C.TransUnit [Decln]
declns []
  where
    declns :: [Decln]
declns = [UExpr] -> [Decln]
mkTypeDeclns [UExpr]
exprs

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

    -- Generate type declarations.
    mkTypeDeclns :: [UExpr] -> [C.Decln]
    mkTypeDeclns :: [UExpr] -> [Decln]
mkTypeDeclns [UExpr]
es = (UType -> Maybe Decln) -> [UType] -> [Decln]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe UType -> Maybe Decln
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 Decln
mkTypeDecln (UType Type a
ty) = case Type a
ty of
          Struct a
_ -> Decln -> Maybe Decln
forall a. a -> Maybe a
Just (Decln -> Maybe Decln) -> Decln -> Maybe Decln
forall a b. (a -> b) -> a -> b
$ Type a -> Decln
forall a. Struct a => Type a -> Decln
mkStructDecln Type a
ty
          Type a
_        -> Maybe Decln
forall a. Maybe a
Nothing

-- * Auxiliary definitions

-- | Render a C.TransUnit to a String, accounting for the case in which the
-- translation unit is empty.
safeCRender :: C.TransUnit -> String
safeCRender :: TransUnit -> Name
safeCRender (C.TransUnit [] []) = Name
""
safeCRender TransUnit
transUnit           = Doc -> Name
render (Doc -> Name) -> Doc -> Name
forall a b. (a -> b) -> a -> b
$ TransUnit -> Doc
forall a. Pretty a => a -> Doc
pretty (TransUnit -> Doc) -> TransUnit -> Doc
forall a b. (a -> b) -> a -> b
$ TransUnit -> TransUnit
C.translate TransUnit
transUnit

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