-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Rank2Types                #-}
{-# LANGUAGE Trustworthy               #-}

-- | Internal Copilot Core representation of Copilot externs.
module Copilot.Core.External
  ( ExtVar (..)
  , externVars
  ) where

import Copilot.Core.Expr
import Copilot.Core.Type
import Copilot.Core.Spec
import Data.DList (DList, empty, singleton, append, concat, toList)
import Data.List (nubBy)
import Prelude hiding (all, concat, foldr)

import Data.Typeable    (Typeable)

-- | An extern variable declaration, together with the type of the underlying
-- extern.
data ExtVar = ExtVar
  { ExtVar -> Name
externVarName :: Name
  , ExtVar -> UType
externVarType :: UType }

-- | List of all externs used in a specification.
externVars :: Spec -> [ExtVar]
externVars :: Spec -> [ExtVar]
externVars = (ExtVar -> ExtVar -> Bool) -> [ExtVar] -> [ExtVar]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy ExtVar -> ExtVar -> Bool
eqExt ([ExtVar] -> [ExtVar]) -> (Spec -> [ExtVar]) -> Spec -> [ExtVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DList ExtVar -> [ExtVar]
forall a. DList a -> [a]
toList (DList ExtVar -> [ExtVar])
-> (Spec -> DList ExtVar) -> Spec -> [ExtVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Expr a -> DList ExtVar) -> Spec -> DList ExtVar
forall b. (forall a. Expr a -> DList b) -> Spec -> DList b
all forall a. Expr a -> DList ExtVar
externVarsExpr
  where
  eqExt :: ExtVar -> ExtVar -> Bool
  eqExt :: ExtVar -> ExtVar -> Bool
eqExt ExtVar { externVarName :: ExtVar -> Name
externVarName = Name
name1 } ExtVar { externVarName :: ExtVar -> Name
externVarName = Name
name2 } =
    Name
name1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
name2

-- | Extract all externs used in a Copilot expression.
externVarsExpr :: Expr a -> DList ExtVar
externVarsExpr :: Expr a -> DList ExtVar
externVarsExpr Expr a
e0 = case Expr a
e0 of
  Const  Type a
_ a
_                -> DList ExtVar
forall a. DList a
empty
  Drop   Type a
_ DropIdx
_ Id
_              -> DList ExtVar
forall a. DList a
empty
  Local Type a
_ Type a
_ Name
_ Expr a
e1 Expr a
e2         -> Expr a -> DList ExtVar
forall a. Expr a -> DList ExtVar
externVarsExpr Expr a
e1 DList ExtVar -> DList ExtVar -> DList ExtVar
forall a. DList a -> DList a -> DList a
`append` Expr a -> DList ExtVar
forall a. Expr a -> DList ExtVar
externVarsExpr Expr a
e2
  Var Type a
_ Name
_                   -> DList ExtVar
forall a. DList a
empty
  ExternVar Type a
t Name
name Maybe [a]
_        -> ExtVar -> DList ExtVar
forall a. a -> DList a
singleton (Name -> UType -> ExtVar
ExtVar Name
name (Type a -> UType
forall a. Typeable a => Type a -> UType
UType Type a
t))
  Op1 Op1 a a
_ Expr a
e                   -> Expr a -> DList ExtVar
forall a. Expr a -> DList ExtVar
externVarsExpr Expr a
e
  Op2 Op2 a b a
_ Expr a
e1 Expr b
e2               -> Expr a -> DList ExtVar
forall a. Expr a -> DList ExtVar
externVarsExpr Expr a
e1 DList ExtVar -> DList ExtVar -> DList ExtVar
forall a. DList a -> DList a -> DList a
`append` Expr b -> DList ExtVar
forall a. Expr a -> DList ExtVar
externVarsExpr Expr b
e2
  Op3 Op3 a b c a
_ Expr a
e1 Expr b
e2 Expr c
e3            -> Expr a -> DList ExtVar
forall a. Expr a -> DList ExtVar
externVarsExpr Expr a
e1 DList ExtVar -> DList ExtVar -> DList ExtVar
forall a. DList a -> DList a -> DList a
`append`
                               Expr b -> DList ExtVar
forall a. Expr a -> DList ExtVar
externVarsExpr Expr b
e2 DList ExtVar -> DList ExtVar -> DList ExtVar
forall a. DList a -> DList a -> DList a
`append`
                               Expr c -> DList ExtVar
forall a. Expr a -> DList ExtVar
externVarsExpr Expr c
e3
  Label Type a
_ Name
_ Expr a
e               -> Expr a -> DList ExtVar
forall a. Expr a -> DList ExtVar
externVarsExpr Expr a
e

-- | Extract all expressions used in an untyped Copilot expression.
externVarsUExpr :: UExpr -> DList ExtVar
externVarsUExpr :: UExpr -> DList ExtVar
externVarsUExpr UExpr { uExprExpr :: ()
uExprExpr = Expr a
e } = Expr a -> DList ExtVar
forall a. Expr a -> DList ExtVar
externVarsExpr Expr a
e

-- | Apply a function to all expressions in a specification, concatenating the
-- results.
all :: (forall a . Expr a -> DList b) -> Spec -> DList b
all :: (forall a. Expr a -> DList b) -> Spec -> DList b
all forall a. Expr a -> DList b
f Spec
spec =
  [DList b] -> DList b
forall a. [DList a] -> DList a
concat ((Stream -> DList b) -> [Stream] -> [DList b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Stream -> DList b
allStream) (Spec -> [Stream]
specStreams   Spec
spec)) DList b -> DList b -> DList b
forall a. DList a -> DList a -> DList a
`append`
  [DList b] -> DList b
forall a. [DList a] -> DList a
concat ((Trigger -> DList b) -> [Trigger] -> [DList b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Trigger -> DList b
allTrigger  (Spec -> [Trigger]
specTriggers  Spec
spec)) DList b -> DList b -> DList b
forall a. DList a -> DList a -> DList a
`append`
  [DList b] -> DList b
forall a. [DList a] -> DList a
concat ((Observer -> DList b) -> [Observer] -> [DList b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Observer -> DList b
allObserver (Spec -> [Observer]
specObservers Spec
spec))

  where

  allStream :: Stream -> DList b
allStream
    Stream { streamExpr :: ()
streamExpr = Expr a
e } = Expr a -> DList b
forall a. Expr a -> DList b
f Expr a
e

  allTrigger :: Trigger -> DList b
allTrigger
    Trigger
      { triggerGuard :: Trigger -> Expr Bool
triggerGuard = Expr Bool
e
      , triggerArgs :: Trigger -> [UExpr]
triggerArgs = [UExpr]
args } = Expr Bool -> DList b
forall a. Expr a -> DList b
f Expr Bool
e DList b -> DList b -> DList b
forall a. DList a -> DList a -> DList a
`append` [DList b] -> DList b
forall a. [DList a] -> DList a
concat ((UExpr -> DList b) -> [UExpr] -> [DList b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UExpr -> DList b
allUExpr [UExpr]
args)

  allUExpr :: UExpr -> DList b
allUExpr
    (UExpr Type a
_ Expr a
e1) = Expr a -> DList b
forall a. Expr a -> DList b
f Expr a
e1

  allObserver :: Observer -> DList b
allObserver
    Observer { observerExpr :: ()
observerExpr = Expr a
e } = Expr a -> DList b
forall a. Expr a -> DList b
f Expr a
e