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