    {-# LANGUAGE ExistentialQuantification #-}

    -- | Represent information about externs needed in the generation of C99 code
    -- for stream declarations and triggers.
    module Copilot.Compile.C99.External
        ( External(..)
        , gatherExts
        )
      where

    -- External imports
    import Data.List  (unionBy)

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

    -- Internal imports
    import Copilot.Compile.C99.Name ( exCpyName )

    -- | Representation of external variables.
    data External = forall a. External
      { External -> String
    extName    :: String
      , External -> String
    extCpyName :: String
      , ()
    extType    :: Type a
      }

    -- | Collect all external variables from the streams and triggers.
    --
    -- Although Copilot specifications can contain also properties and theorems,
    -- the C99 backend currently only generates code for streams and triggers.
    gatherExts :: [Stream] -> [Trigger] -> [External]
    gatherExts :: [Stream] -> [Trigger] -> [External]
    gatherExts [Stream]
    streams [Trigger]
    triggers = [External]
    streamsExts [External] -> [External] -> [External]
    `extUnion` [External]
    triggersExts
      where
        streamsExts :: [External]
    streamsExts  = (Stream -> [External] -> [External])
    -> [External] -> [Stream] -> [External]
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ([External] -> [External] -> [External]
    extUnion ([External] -> [External] -> [External])
    -> (Stream -> [External]) -> Stream -> [External] -> [External]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Stream -> [External]
    streamExts) [External]
    forall a. Monoid a => a
    mempty [Stream]
    streams
        triggersExts :: [External]
    triggersExts = (Trigger -> [External] -> [External])
    -> [External] -> [Trigger] -> [External]
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ([External] -> [External] -> [External]
    extUnion ([External] -> [External] -> [External])
    -> (Trigger -> [External]) -> Trigger -> [External] -> [External]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Trigger -> [External]
    triggerExts) [External]
    forall a. Monoid a => a
    mempty [Trigger]
    triggers

        streamExts :: Stream -> [External]
        streamExts :: Stream -> [External]
    streamExts (Stream Id
    _ [a]
    _ Expr a
    expr Type a
    _) = Expr a -> [External]
    forall a. Expr a -> [External]
    exprExts Expr a
    expr

        triggerExts :: Trigger -> [External]
        triggerExts :: Trigger -> [External]
    triggerExts (Trigger String
    _ Expr Bool
    guard [UExpr]
    args) = [External]
    guardExts [External] -> [External] -> [External]
    `extUnion` [External]
    argExts
          where
            guardExts :: [External]
    guardExts = Expr Bool -> [External]
    forall a. Expr a -> [External]
    exprExts Expr Bool
    guard
            argExts :: [External]
    argExts   = (UExpr -> [External]) -> [UExpr] -> [External]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap UExpr -> [External]
    uExprExts [UExpr]
    args

        uExprExts :: UExpr -> [External]
        uExprExts :: UExpr -> [External]
    uExprExts (UExpr Type a
    _ Expr a
    expr) = Expr a -> [External]
    forall a. Expr a -> [External]
    exprExts Expr a
    expr

        exprExts :: Expr a -> [External]
        exprExts :: forall a. Expr a -> [External]
    exprExts (Local Type a1
    _ Type a
    _ String
    _ Expr a1
    e1 Expr a
    e2)   = Expr a1 -> [External]
    forall a. Expr a -> [External]
    exprExts Expr a1
    e1 [External] -> [External] -> [External]
    `extUnion` Expr a -> [External]
    forall a. Expr a -> [External]
    exprExts Expr a
    e2
        exprExts (ExternVar Type a
    ty String
    name Maybe [a]
    _) = [String -> String -> Type a -> External
    forall a. String -> String -> Type a -> External
    External String
    name (String -> String
    exCpyName String
    name) Type a
    ty]
        exprExts (Op1 Op1 a1 a
    _ Expr a1
    e)             = Expr a1 -> [External]
    forall a. Expr a -> [External]
    exprExts Expr a1
    e
        exprExts (Op2 Op2 a1 b a
    _ Expr a1
    e1 Expr b
    e2)         = Expr a1 -> [External]
    forall a. Expr a -> [External]
    exprExts Expr a1
    e1 [External] -> [External] -> [External]
    `extUnion` Expr b -> [External]
    forall a. Expr a -> [External]
    exprExts Expr b
    e2
        exprExts (Op3 Op3 a1 b c a
    _ Expr a1
    e1 Expr b
    e2 Expr c
    e3)      = Expr a1 -> [External]
    forall a. Expr a -> [External]
    exprExts Expr a1
    e1 [External] -> [External] -> [External]
    `extUnion` Expr b -> [External]
    forall a. Expr a -> [External]
    exprExts Expr b
    e2
                                           [External] -> [External] -> [External]
    `extUnion` Expr c -> [External]
    forall a. Expr a -> [External]
    exprExts Expr c
    e3
        exprExts (Label Type a
    _ String
    _ Expr a
    e)         = Expr a -> [External]
    forall a. Expr a -> [External]
    exprExts Expr a
    e
        exprExts Expr a
    _                     = []

        -- | Union over lists of External, we solely base the equality on the
        -- extName's.
        extUnion :: [External] -> [External] -> [External]
        extUnion :: [External] -> [External] -> [External]
    extUnion = (External -> External -> Bool)
    -> [External] -> [External] -> [External]
    forall a. (a -> a -> Bool) -> [a] -> [a] -> [a]
    unionBy (\External
    a External
    b -> External -> String
    extName External
    a String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == External -> String
    extName External
    b)